diff --git a/executable/Main.hs b/executable/Main.hs --- a/executable/Main.hs +++ b/executable/Main.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-} +{-# OPTIONS_GHC -flate-specialise #-} import Control.Monad import Data.Char import Data.Either @@ -19,9 +20,9 @@ import Data.Maybe import Jukebox.Options import Jukebox.Toolbox -import Jukebox.Name hiding (lhs, rhs) +import Jukebox.Name hiding (lhs, rhs, label) import qualified Jukebox.Form as Jukebox -import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, Lemma) +import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, matchList) import Jukebox.Tools.EncodeTypes import Jukebox.TPTP.Print import Jukebox.Tools.HornToUnit @@ -34,11 +35,13 @@ data MainFlags = MainFlags { flags_proof :: Bool, - flags_trace :: Maybe (String, String) } + flags_trace :: Maybe (String, String), + flags_casc :: Bool, + flags_explain_encoding :: Bool } parseMainFlags :: OptionParser MainFlags parseMainFlags = - MainFlags <$> proof <*> trace + MainFlags <$> proof <*> trace <*> casc <*> explain where proof = inGroup "Output options" $ @@ -50,6 +53,15 @@ flag "trace" ["Write a Prolog-format execution trace to this file (off by default)."] Nothing ((\x y -> Just (x, y)) <$> argFile <*> argModule) + casc = + expert $ + inGroup "Output options" $ + bool "casc" ["Print output in CASC format (off by default)."] False + explain = + expert $ + inGroup "Output options" $ + bool "explain-encoding" ["In CASC mode, explain the conditional encoding (off by default)."] False + argModule = arg "" "expected a Prolog module name" Just parseConfig :: OptionParser (Config (Extended Constant)) @@ -178,7 +190,7 @@ instance PrettyTerm Constant where termStyle Constant{..} - | "$to_" `isPrefixOf` (base con_id) = invisible + | hasLabel "type_tag" con_id = invisible | any isAlphaNum (base con_id) = uncurried | otherwise = case con_arity of @@ -217,19 +229,24 @@ Main.isEquals fun isType :: Jukebox.Function -> Bool -isType fun = "$to_" `isPrefixOf` base (name fun) && Jukebox.arity fun == 1 +isType fun = + hasLabel "type_tag" (name fun) && Jukebox.arity fun == 1 isIfeq :: Jukebox.Function -> Bool -isIfeq fun = "$ifeq" `isPrefixOf` base (name fun) +isIfeq fun = + hasLabel "ifeq" (name fun) isEquals :: Jukebox.Function -> Bool -isEquals fun = "$equals" `isPrefixOf` base (name fun) +isEquals fun = + hasLabel "equals" (name fun) && Jukebox.arity fun == 2 isTrue :: Jukebox.Function -> Bool -isTrue fun = "$true" `isPrefixOf` base (name fun) +isTrue fun = + hasLabel "true" (name fun) && Jukebox.arity fun == 0 isFalse :: Jukebox.Function -> Bool -isFalse fun = "$false" `isPrefixOf` base (name fun) +isFalse fun = + hasLabel "false" (name fun) && Jukebox.arity fun == 0 jukeboxFunction :: TweeContext -> Extended Constant -> Jukebox.Function jukeboxFunction _ (Function Constant{..}) = con_id @@ -247,7 +264,7 @@ jukeboxTerm :: TweeContext -> Term (Extended Constant) -> Jukebox.Term jukeboxTerm TweeContext{..} (Var (V x)) = - Jukebox.Var (Unique (fromIntegral x) "X" defaultRenamer ::: ctx_type) + Jukebox.Var (Unique (fromIntegral x) "X" Nothing defaultRenamer ::: ctx_type) jukeboxTerm ctx@TweeContext{..} (App f t) = jukeboxFunction ctx (fun_value f) :@: map (jukeboxTerm ctx) ts where @@ -262,10 +279,10 @@ [ty] -> ty var <- newSymbol "X" ty - minimal <- newFunction "$constant" [] ty - true <- newFunction "$true" [] ty - false <- newFunction "$false" [] ty - equals <- newFunction "$equals" [ty, ty] ty + minimal <- newFunction (withLabel "minimal" (name "constant")) [] ty + true <- newFunction (withLabel "true" (name "true")) [] ty + false <- newFunction (withLabel "false" (name "false")) [] ty + equals <- newFunction (withLabel "equals" (name "equals")) [ty, ty] ty return TweeContext { ctx_var = var, @@ -360,7 +377,7 @@ let -- Encode whatever needs encoding in the problem ctx = makeContext obligs - prob = addNarrowing ctx obligs + prob = prettyNames (addNarrowing ctx obligs) (axioms0, goals0) <- case identifyProblem ctx prob of @@ -458,11 +475,54 @@ pres = present (cfg_proof_presentation config) (solutions state) sayTrace "" - forM_ (pres_lemmas pres) $ \Lemma{..} -> + forM_ (pres_lemmas pres) $ \p -> sayTrace $ show $ - traceApp "lemma" [traceEqn (equation lemma_proof)] <#> text "." + traceApp "lemma" [traceEqn (equation p)] <#> text "." - when tstp $ do + when (flags_casc main) $ do + putStrLn "% SZS output start Proof" + let + axiomForms = + Map.fromList + (zip (map axiom_number axioms) (map pre_form axioms0)) + goalForms = + Map.fromList + (zip (map goal_number goals) (map pre_form goals0)) + + findSource forms n = + case Map.lookup n forms of + Nothing -> [] + Just inp -> go inp + where + go Input{source = Unknown} = [] + go Input{source = Inference _ _ inps} = concatMap go inps + go inp@Input{source = FromFile _ _} = [inp] + + when (flags_explain_encoding main) $ do + putStrLn "Take the following subset of the input axioms:" + mapM_ putStrLn $ map (" " ++) $ lines $ showProblem $ + usortBy (comparing show) $ + (pres_axioms pres >>= findSource axiomForms . axiom_number) ++ + (pres_goals pres >>= findSource goalForms . pg_number) + + putStrLn "" + putStrLn "Now clausify the problem and encode Horn clauses using encoding 3 of" + putStrLn "http://www.cse.chalmers.se/~nicsma/papers/horn.pdf." + putStrLn "We repeatedly replace C & s=t => u=v by the two clauses:" + putStrLn " fresh(y, y, x1...xn) = u" + putStrLn " C => fresh(s, t, x1...xn) = v" + putStrLn "where fresh is a fresh function symbol and x1..xn are the free" + putStrLn "variables of u and v." + putStrLn "A predicate p(X) is encoded as p(X)=true (this is sound, because the" + putStrLn "input problem has no model of domain size 1)." + putStrLn "" + putStrLn "The encoding turns the above axioms into the following unit equations and goals:" + putStrLn "" + print $ pPrintPresentation (cfg_proof_presentation config) pres + putStrLn "% SZS output end Proof" + putStrLn "" + + when (tstp && not (flags_casc main)) $ do putStrLn "% SZS output start CNFRefutation" print $ pPrintProof $ presentToJukebox ctx (curry toEquation) @@ -472,10 +532,11 @@ putStrLn "% SZS output end CNFRefutation" putStrLn "" - putStrLn "The conjecture is true! Here is a proof." - putStrLn "" - print $ pPrintPresentation (cfg_proof_presentation config) pres - putStrLn "" + when (not (flags_casc main)) $ do + putStrLn "The conjecture is true! Here is a proof." + putStrLn "" + print $ pPrintPresentation (cfg_proof_presentation config) pres + putStrLn "" when (not (quiet globals) && not (solved state)) $ later $ do let @@ -510,7 +571,7 @@ return $ if solved state then Unsat Unsatisfiable Nothing - else if configIsComplete config then Sat Satisfiable Nothing + else if configIsComplete config && not (dropNonHorn horn) then Sat Satisfiable Nothing else NoAnswer GaveUp -- Transform a proof presentation into a Jukebox proof. @@ -543,7 +604,7 @@ | Axiom{..} <- pres_axioms ] lemma_proofs = - Map.fromList [(lemma_id, tstp lemma_proof) | Lemma{..} <- pres_lemmas] + Map.fromList [(p, tstp p) | p <- pres_lemmas] goal_proofs = Map.fromList [(pg_number, tstp pg_proof) | ProvedGoal{..} <- pres_goals] @@ -570,8 +631,8 @@ sources :: Derivation (Extended Constant) -> [Input Form] sources p = - [ fromJust (Map.lookup lemma_id lemma_proofs) - | Lemma{..} <- usortBy (comparing lemma_id) (usedLemmas p) ] ++ + [ fromJust (Map.lookup lemma lemma_proofs) + | lemma <- usort (usedLemmas p) ] ++ [ fromJust (Map.lookup axiom_number axiom_proofs) | Axiom{..} <- usort (usedAxioms p) ] diff --git a/tests/PUZ037-3-2.p b/tests/PUZ037-3-2.p new file mode 100644 --- /dev/null +++ b/tests/PUZ037-3-2.p @@ -0,0 +1,106 @@ +%-------------------------------------------------------------------------- +% File : PUZ037-3 : TPTP v7.2.0. Released v2.3.0. +% Domain : Puzzles +% Problem : Rubik's Cube +% Version : [HM98] axioms : Especial. +% Theorem formulation : Rotation in all three planes. +% English : Rubik's Cube is a 3x3x3 cube consisting of 27 subcubes with +% colored faces. The three layers perpendicular to any axis may +% be rotated independently. The object is to take a scrambled +% cube and unscramble it so that each side consists entirely +% of one color(Blue, White, Green, Yellow, Orange, Red). + +% Refs : [HM98] Huang & Myers (1998), Subgoal Strategies for Solving B +% Source : [HM98] +% Names : Rubik's Cube [HM98] + +% Status : Unsatisfiable +% Rating : 0.20 v7.2.0, 0.22 v7.1.0, 0.14 v6.4.0, 0.17 v6.3.0, 0.25 v6.2.0, 0.12 v6.1.0, 0.00 v5.5.0, 0.20 v5.4.0, 0.33 v5.0.0, 0.50 v4.1.0, 0.60 v3.7.0, 0.50 v3.5.0, 0.33 v3.1.0, 0.44 v2.7.0, 0.50 v2.6.0, 0.44 v2.5.0, 0.75 v2.4.0, 0.67 v2.3.0 +% Syntax : Number of clauses : 20 ( 0 non-Horn; 2 unit; 20 RR) +% Number of atoms : 38 ( 0 equality) +% Maximal clause size : 2 ( 2 average) +% Number of predicates : 1 ( 0 propositional; 54-54 arity) +% Number of functors : 6 ( 6 constant; 0-0 arity) +% Number of variables : 972 ( 0 singleton) +% Maximal term depth : 1 ( 1 average) +% SPC : CNF_UNS_EPR + +% Comments : mzy, mzy, bzy, byx, lzx rotations to solve. +%-------------------------------------------------------------------------- +cnf(a, axiom, + state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w) != + state(b,r,r,w,w,w,y,b,b,g,y,r,b,g,g,o,g,y,w,w,r,g,o,r,b,g,g,o,r,b,y,y,r,g,o,g,o,o,o,y,r,b,y,y,r,w,w,w,b,b,y,w,o,o)). + +cnf(txy,axiom, + ( state(W7,W6,W5,W8,A1,W4,W1,W2,W3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) + = state(W1,W8,W7,W2,A1,W6,W3,W4,W5,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) )). + +cnf(mxy,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) )). + +cnf(bxy,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5) )). + +cnf(fzy,axiom, + ( state(A1,A2,A3,A4,A5,A6,V1,U1,Y1,A7,A8,W1,V2,U2,Y2,X1,A9,B1,B2,B3,B4,B5,B6,W2,V3,U3,Y3,X2,B7,B8,B9,C1,C2,C3,C4,W3,V4,U4,Y4,X3,C5,C6,C7,C8,C9,V5,U5,Y5,D1,D2,D3,D4,D5,D6) + = state(A1,A2,A3,A4,A5,A6,X1,X2,X3,A7,A8,Y1,Y2,Y3,Y4,Y5,A9,B1,B2,B3,B4,B5,B6,U1,U2,U3,U4,U5,B7,B8,B9,C1,C2,C3,C4,V1,V2,V3,V4,V5,C5,C6,C7,C8,C9,W1,W2,W3,D1,D2,D3,D4,D5,D6) )). + +cnf(mzy,axiom, + ( state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6) + = state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) )). + +cnf(bzy,axiom, + ( state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4) + = state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) )). + +cnf(lzx,axiom, + ( state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7) + = state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) )). + +cnf(mzx,axiom, + ( state(A1,Y1,A2,A3,Y2,A4,A5,Y3,A6,A7,A8,A9,B1,X1,B2,B3,B4,B5,B6,X9,B7,B8,B9,C1,C2,X2,C3,C4,C5,C6,C7,X8,C8,C9,D1,D2,D3,X3,D4,D5,D6,D7,D8,X7,D9,E1,X4,E2,E3,X5,E4,E5,X6,E6) + = state(A1,X1,A2,A3,X2,A4,A5,X3,A6,A7,A8,A9,B1,X4,B2,B3,B4,B5,B6,Y3,B7,B8,B9,C1,C2,X5,C3,C4,C5,C6,C7,Y2,C8,C9,D1,D2,D3,X6,D4,D5,D6,D7,D8,Y1,D9,E1,X7,E2,E3,X8,E4,E5,X9,E6) )). + +cnf(rzx,axiom, + ( state(A1,A2,Y1,A3,A4,Y2,A5,A6,Y3,A7,A8,A9,B1,B2,X1,W1,W8,W7,X9,B3,B4,B5,B6,B7,B8,B9,X2,W2,C1,W6,X8,C2,C3,C4,C5,C6,C7,C8,X3,W3,W4,W5,X7,C9,D1,D2,D3,X4,D4,D5,X5,D6,D7,X6) + = state(A1,A2,X1,A3,A4,X2,A5,A6,X3,A7,A8,A9,B1,B2,X4,W3,W2,W1,Y3,B3,B4,B5,B6,B7,B8,B9,X5,W4,C1,W8,Y2,C2,C3,C4,C5,C6,C7,C8,X6,W5,W6,W7,Y1,C9,D1,D2,D3,X7,D4,D5,X8,D6,D7,X9) )). + +cnf(tyx,axiom, + ( state(W1,W8,W7,W2,A1,W6,W3,W4,W5,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) + = state(W7,W6,W5,W8,A1,W4,W1,W2,W3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) )). + +cnf(myx,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) )). + +cnf(byx,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) )). + +cnf(fyz,axiom, + ( state(A1,A2,A3,A4,A5,A6,X1,X2,X3,A7,A8,Y1,Y2,Y3,Y4,Y5,A9,B1,B2,B3,B4,B5,B6,U1,U2,U3,U4,U5,B7,B8,B9,C1,C2,C3,C4,V1,V2,V3,V4,V5,C5,C6,C7,C8,C9,W1,W2,W3,D1,D2,D3,D4,D5,D6) + = state(A1,A2,A3,A4,A5,A6,V1,U1,Y1,A7,A8,W1,V2,U2,Y2,X1,A9,B1,B2,B3,B4,B5,B6,W2,V3,U3,Y3,X2,B7,B8,B9,C1,C2,C3,C4,W3,V4,U4,Y4,X3,C5,C6,C7,C8,C9,V5,U5,Y5,D1,D2,D3,D4,D5,D6) )). + +cnf(myz,axiom, + ( state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) + = state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6) )). + +cnf(byz,axiom, + ( state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) + = state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4) )). + +cnf(lxz,axiom, + ( state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) + = state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7) )). + +cnf(mxz,axiom, + ( state(A1,X1,A2,A3,X2,A4,A5,X3,A6,A7,A8,A9,B1,X4,B2,B3,B4,B5,B6,Y3,B7,B8,B9,C1,C2,X5,C3,C4,C5,C6,C7,Y2,C8,C9,D1,D2,D3,X6,D4,D5,D6,D7,D8,Y1,D9,E1,X7,E2,E3,X8,E4,E5,X9,E6) + = state(A1,Y1,A2,A3,Y2,A4,A5,Y3,A6,A7,A8,A9,B1,X1,B2,B3,B4,B5,B6,X9,B7,B8,B9,C1,C2,X2,C3,C4,C5,C6,C7,X8,C8,C9,D1,D2,D3,X3,D4,D5,D6,D7,D8,X7,D9,E1,X4,E2,E3,X5,E4,E5,X6,E6) )). + +cnf(rxz,axiom, + ( state(A1,A2,X1,A3,A4,X2,A5,A6,X3,A7,A8,A9,B1,B2,X4,W3,W2,W1,Y3,B3,B4,B5,B6,B7,B8,B9,X5,W4,C1,W8,Y2,C2,C3,C4,C5,C6,C7,C8,X6,W5,W6,W7,Y1,C9,D1,D2,D3,X7,D4,D5,X8,D6,D7,X9) + = state(A1,A2,Y1,A3,A4,Y2,A5,A6,Y3,A7,A8,A9,B1,B2,X1,W1,W8,W7,X9,B3,B4,B5,B6,B7,B8,B9,X2,W2,C1,W6,X8,C2,C3,C4,C5,C6,C7,C8,X3,W3,W4,W5,X7,C9,D1,D2,D3,X4,D4,D5,X5,D6,D7,X6) )). + +%-------------------------------------------------------------------------- diff --git a/tests/PUZ037-3.p b/tests/PUZ037-3.p new file mode 100644 --- /dev/null +++ b/tests/PUZ037-3.p @@ -0,0 +1,110 @@ +%-------------------------------------------------------------------------- +% File : PUZ037-3 : TPTP v7.2.0. Released v2.3.0. +% Domain : Puzzles +% Problem : Rubik's Cube +% Version : [HM98] axioms : Especial. +% Theorem formulation : Rotation in all three planes. +% English : Rubik's Cube is a 3x3x3 cube consisting of 27 subcubes with +% colored faces. The three layers perpendicular to any axis may +% be rotated independently. The object is to take a scrambled +% cube and unscramble it so that each side consists entirely +% of one color(Blue, White, Green, Yellow, Orange, Red). + +% Refs : [HM98] Huang & Myers (1998), Subgoal Strategies for Solving B +% Source : [HM98] +% Names : Rubik's Cube [HM98] + +% Status : Unsatisfiable +% Rating : 0.20 v7.2.0, 0.22 v7.1.0, 0.14 v6.4.0, 0.17 v6.3.0, 0.25 v6.2.0, 0.12 v6.1.0, 0.00 v5.5.0, 0.20 v5.4.0, 0.33 v5.0.0, 0.50 v4.1.0, 0.60 v3.7.0, 0.50 v3.5.0, 0.33 v3.1.0, 0.44 v2.7.0, 0.50 v2.6.0, 0.44 v2.5.0, 0.75 v2.4.0, 0.67 v2.3.0 +% Syntax : Number of clauses : 20 ( 0 non-Horn; 2 unit; 20 RR) +% Number of atoms : 38 ( 0 equality) +% Maximal clause size : 2 ( 2 average) +% Number of predicates : 1 ( 0 propositional; 54-54 arity) +% Number of functors : 6 ( 6 constant; 0-0 arity) +% Number of variables : 972 ( 0 singleton) +% Maximal term depth : 1 ( 1 average) +% SPC : CNF_UNS_EPR + +% Comments : mzy, mzy, bzy, byx, lzx rotations to solve. +%-------------------------------------------------------------------------- +cnf(make_like_this,negated_conjecture, lhs != rhs). + +cnf(a, axiom, lhs = + state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w)). + +cnf(b, axiom, rhs = + state(b,r,r,w,w,w,y,b,b,g,y,r,b,g,g,o,g,y,w,w,r,g,o,r,b,g,g,o,r,b,y,y,r,g,o,g,o,o,o,y,r,b,y,y,r,w,w,w,b,b,y,w,o,o)). + +cnf(txy,axiom, + ( state(W7,W6,W5,W8,A1,W4,W1,W2,W3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) + = state(W1,W8,W7,W2,A1,W6,W3,W4,W5,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) )). + +cnf(mxy,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) )). + +cnf(bxy,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5) )). + +cnf(fzy,axiom, + ( state(A1,A2,A3,A4,A5,A6,V1,U1,Y1,A7,A8,W1,V2,U2,Y2,X1,A9,B1,B2,B3,B4,B5,B6,W2,V3,U3,Y3,X2,B7,B8,B9,C1,C2,C3,C4,W3,V4,U4,Y4,X3,C5,C6,C7,C8,C9,V5,U5,Y5,D1,D2,D3,D4,D5,D6) + = state(A1,A2,A3,A4,A5,A6,X1,X2,X3,A7,A8,Y1,Y2,Y3,Y4,Y5,A9,B1,B2,B3,B4,B5,B6,U1,U2,U3,U4,U5,B7,B8,B9,C1,C2,C3,C4,V1,V2,V3,V4,V5,C5,C6,C7,C8,C9,W1,W2,W3,D1,D2,D3,D4,D5,D6) )). + +cnf(mzy,axiom, + ( state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6) + = state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) )). + +cnf(bzy,axiom, + ( state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4) + = state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) )). + +cnf(lzx,axiom, + ( state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7) + = state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) )). + +cnf(mzx,axiom, + ( state(A1,Y1,A2,A3,Y2,A4,A5,Y3,A6,A7,A8,A9,B1,X1,B2,B3,B4,B5,B6,X9,B7,B8,B9,C1,C2,X2,C3,C4,C5,C6,C7,X8,C8,C9,D1,D2,D3,X3,D4,D5,D6,D7,D8,X7,D9,E1,X4,E2,E3,X5,E4,E5,X6,E6) + = state(A1,X1,A2,A3,X2,A4,A5,X3,A6,A7,A8,A9,B1,X4,B2,B3,B4,B5,B6,Y3,B7,B8,B9,C1,C2,X5,C3,C4,C5,C6,C7,Y2,C8,C9,D1,D2,D3,X6,D4,D5,D6,D7,D8,Y1,D9,E1,X7,E2,E3,X8,E4,E5,X9,E6) )). + +cnf(rzx,axiom, + ( state(A1,A2,Y1,A3,A4,Y2,A5,A6,Y3,A7,A8,A9,B1,B2,X1,W1,W8,W7,X9,B3,B4,B5,B6,B7,B8,B9,X2,W2,C1,W6,X8,C2,C3,C4,C5,C6,C7,C8,X3,W3,W4,W5,X7,C9,D1,D2,D3,X4,D4,D5,X5,D6,D7,X6) + = state(A1,A2,X1,A3,A4,X2,A5,A6,X3,A7,A8,A9,B1,B2,X4,W3,W2,W1,Y3,B3,B4,B5,B6,B7,B8,B9,X5,W4,C1,W8,Y2,C2,C3,C4,C5,C6,C7,C8,X6,W5,W6,W7,Y1,C9,D1,D2,D3,X7,D4,D5,X8,D6,D7,X9) )). + +cnf(tyx,axiom, + ( state(W1,W8,W7,W2,A1,W6,W3,W4,W5,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) + = state(W7,W6,W5,W8,A1,W4,W1,W2,W3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) )). + +cnf(myx,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) )). + +cnf(byx,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5) + = state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) )). + +cnf(fyz,axiom, + ( state(A1,A2,A3,A4,A5,A6,X1,X2,X3,A7,A8,Y1,Y2,Y3,Y4,Y5,A9,B1,B2,B3,B4,B5,B6,U1,U2,U3,U4,U5,B7,B8,B9,C1,C2,C3,C4,V1,V2,V3,V4,V5,C5,C6,C7,C8,C9,W1,W2,W3,D1,D2,D3,D4,D5,D6) + = state(A1,A2,A3,A4,A5,A6,V1,U1,Y1,A7,A8,W1,V2,U2,Y2,X1,A9,B1,B2,B3,B4,B5,B6,W2,V3,U3,Y3,X2,B7,B8,B9,C1,C2,C3,C4,W3,V4,U4,Y4,X3,C5,C6,C7,C8,C9,V5,U5,Y5,D1,D2,D3,D4,D5,D6) )). + +cnf(myz,axiom, + ( state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) + = state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6) )). + +cnf(byz,axiom, + ( state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) + = state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4) )). + +cnf(lxz,axiom, + ( state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) + = state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7) )). + +cnf(mxz,axiom, + ( state(A1,X1,A2,A3,X2,A4,A5,X3,A6,A7,A8,A9,B1,X4,B2,B3,B4,B5,B6,Y3,B7,B8,B9,C1,C2,X5,C3,C4,C5,C6,C7,Y2,C8,C9,D1,D2,D3,X6,D4,D5,D6,D7,D8,Y1,D9,E1,X7,E2,E3,X8,E4,E5,X9,E6) + = state(A1,Y1,A2,A3,Y2,A4,A5,Y3,A6,A7,A8,A9,B1,X1,B2,B3,B4,B5,B6,X9,B7,B8,B9,C1,C2,X2,C3,C4,C5,C6,C7,X8,C8,C9,D1,D2,D3,X3,D4,D5,D6,D7,D8,X7,D9,E1,X4,E2,E3,X5,E4,E5,X6,E6) )). + +cnf(rxz,axiom, + ( state(A1,A2,X1,A3,A4,X2,A5,A6,X3,A7,A8,A9,B1,B2,X4,W3,W2,W1,Y3,B3,B4,B5,B6,B7,B8,B9,X5,W4,C1,W8,Y2,C2,C3,C4,C5,C6,C7,C8,X6,W5,W6,W7,Y1,C9,D1,D2,D3,X7,D4,D5,X8,D6,D7,X9) + = state(A1,A2,Y1,A3,A4,Y2,A5,A6,Y3,A7,A8,A9,B1,B2,X1,W1,W8,W7,X9,B3,B4,B5,B6,B7,B8,B9,X2,W2,C1,W6,X8,C2,C3,C4,C5,C6,C7,C8,X3,W3,W4,W5,X7,C9,D1,D2,D3,X4,D4,D5,X5,D6,D7,X6) )). + +%-------------------------------------------------------------------------- diff --git a/tests/PUZ052-1.p b/tests/PUZ052-1.p new file mode 100644 --- /dev/null +++ b/tests/PUZ052-1.p @@ -0,0 +1,129 @@ +%-------------------------------------------------------------------------- +% File : PUZ052-1 : TPTP v7.2.0. Released v2.7.0. +% Domain : Puzzles +% Problem : Rubik's Cube unreachability +% Version : [HM98] axioms : Especial. +% Theorem formulation : Rotations in one plane only. +% English : Rubik's Cube is a 3x3x3 cube consisting of 27 subcubes with +% colored faces. The three layers perpendicular to any axis may +% be rotated independently. The object is to take a scrambled +% cube and unscramble it so that each side consists entirely +% of one color(Blue, White, Green, Yellow, Orange, Red). +% The objective here is unreachable: there are 10 b's and only +% 8 r's. + +% Refs : [HM98] Huang & Myers (1998), Subgoal Strategies for Solving B +% : [Cla03] Claessen (2003), Email to G. Sutcliffe +% Source : [Cla03] +% Names : + +% Status : Satisfiable +% Rating : 1.00 v2.7.0 +% Syntax : Number of clauses : 20 ( 0 non-Horn; 2 unit; 20 RR) +% Number of atoms : 38 ( 0 equality) +% Maximal clause size : 2 ( 2 average) +% Number of predicates : 1 ( 0 propositional; 54-54 arity) +% Number of functors : 6 ( 6 constant; 0-0 arity) +% Number of variables : 972 ( 0 singleton) +% Maximal term depth : 1 ( 1 average) +% SPC : CNF_SAT_EPR + +% Comments : Replaced one b by an r in make_like_this from PUZ037-1.p +% Model never found; a domain of size 2 should be enough though. +%-------------------------------------------------------------------------- +cnf(make_like_this,negated_conjecture, + ( state(b,b,b,b,b,b,b,b,b,b,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w) != + state(b,b,b,b,b,b,b,b,b,r,r,r,g,g,g,o,o,o,y,y,y,g,g,g,o,o,o,y,y,y,r,r,r,r,r,r,g,g,g,o,o,o,y,y,y,w,w,w,w,w,w,w,w,w) )). + +cnf(txy,axiom, + ( +state(W7,W6,W5,W8,A1,W4,W1,W2,W3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) += state(W1,W8,W7,W2,A1,W6,W3,W4,W5,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) )). + +cnf(mxy,axiom, + ( +state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) += + state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) )). + +cnf(bxy,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) + = +state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5) )). + +cnf(fzy,axiom, + ( state(A1,A2,A3,A4,A5,A6,V1,U1,Y1,A7,A8,W1,V2,U2,Y2,X1,A9,B1,B2,B3,B4,B5,B6,W2,V3,U3,Y3,X2,B7,B8,B9,C1,C2,C3,C4,W3,V4,U4,Y4,X3,C5,C6,C7,C8,C9,V5,U5,Y5,D1,D2,D3,D4,D5,D6) + = +state(A1,A2,A3,A4,A5,A6,X1,X2,X3,A7,A8,Y1,Y2,Y3,Y4,Y5,A9,B1,B2,B3,B4,B5,B6,U1,U2,U3,U4,U5,B7,B8,B9,C1,C2,C3,C4,V1,V2,V3,V4,V5,C5,C6,C7,C8,C9,W1,W2,W3,D1,D2,D3,D4,D5,D6) )). + +cnf(mzy,axiom, + ( state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6) + = +state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) )). + +cnf(bzy,axiom, + ( state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4) + = +state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) )). + +cnf(lzx,axiom, + ( state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7) + = +state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) )). + +cnf(mzx,axiom, + ( state(A1,Y1,A2,A3,Y2,A4,A5,Y3,A6,A7,A8,A9,B1,X1,B2,B3,B4,B5,B6,X9,B7,B8,B9,C1,C2,X2,C3,C4,C5,C6,C7,X8,C8,C9,D1,D2,D3,X3,D4,D5,D6,D7,D8,X7,D9,E1,X4,E2,E3,X5,E4,E5,X6,E6) + = +state(A1,X1,A2,A3,X2,A4,A5,X3,A6,A7,A8,A9,B1,X4,B2,B3,B4,B5,B6,Y3,B7,B8,B9,C1,C2,X5,C3,C4,C5,C6,C7,Y2,C8,C9,D1,D2,D3,X6,D4,D5,D6,D7,D8,Y1,D9,E1,X7,E2,E3,X8,E4,E5,X9,E6) )). + +cnf(rzx,axiom, + ( state(A1,A2,Y1,A3,A4,Y2,A5,A6,Y3,A7,A8,A9,B1,B2,X1,W1,W8,W7,X9,B3,B4,B5,B6,B7,B8,B9,X2,W2,C1,W6,X8,C2,C3,C4,C5,C6,C7,C8,X3,W3,W4,W5,X7,C9,D1,D2,D3,X4,D4,D5,X5,D6,D7,X6) + = +state(A1,A2,X1,A3,A4,X2,A5,A6,X3,A7,A8,A9,B1,B2,X4,W3,W2,W1,Y3,B3,B4,B5,B6,B7,B8,B9,X5,W4,C1,W8,Y2,C2,C3,C4,C5,C6,C7,C8,X6,W5,W6,W7,Y1,C9,D1,D2,D3,X7,D4,D5,X8,D6,D7,X9) )). + +cnf(tyx,axiom, + ( state(W1,W8,W7,W2,A1,W6,W3,W4,W5,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) + = +state(W7,W6,W5,W8,A1,W4,W1,W2,W3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7) )). + +cnf(myx,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) + = +state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,D7,D8,D9,E1,E2,E3,E4,E5,E6) )). + +cnf(byx,axiom, + ( state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,X1,X2,X3,X4,X5,X6,X7,X8,X9,Y1,Y2,Y3,W1,W2,W3,W8,D7,W4,W7,W6,W5) + = +state(A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,C1,C2,C3,C4,C5,C6,C7,C8,C9,D1,D2,D3,D4,D5,D6,Y1,Y2,Y3,X1,X2,X3,X4,X5,X6,X7,X8,X9,W7,W8,W1,W6,D7,W2,W5,W4,W3) )). + +cnf(fyz,axiom, + ( state(A1,A2,A3,A4,A5,A6,X1,X2,X3,A7,A8,Y1,Y2,Y3,Y4,Y5,A9,B1,B2,B3,B4,B5,B6,U1,U2,U3,U4,U5,B7,B8,B9,C1,C2,C3,C4,V1,V2,V3,V4,V5,C5,C6,C7,C8,C9,W1,W2,W3,D1,D2,D3,D4,D5,D6) + = +state(A1,A2,A3,A4,A5,A6,V1,U1,Y1,A7,A8,W1,V2,U2,Y2,X1,A9,B1,B2,B3,B4,B5,B6,W2,V3,U3,Y3,X2,B7,B8,B9,C1,C2,C3,C4,W3,V4,U4,Y4,X3,C5,C6,C7,C8,C9,V5,U5,Y5,D1,D2,D3,D4,D5,D6) )). + +cnf(myz,axiom, + ( state(A1,A2,A3,X1,X2,X3,A4,A5,A6,A7,Y3,A8,A9,B1,B2,B3,X4,B4,B5,B6,B7,B8,Y2,B9,C1,C2,C3,C4,X5,C5,C6,C7,C8,C9,Y1,D1,D2,D3,D4,D5,X6,D6,D7,D8,D9,E1,E2,E3,X9,X8,X7,E4,E5,E6) + = +state(A1,A2,A3,Y1,Y2,Y3,A4,A5,A6,A7,X9,A8,A9,B1,B2,B3,X1,B4,B5,B6,B7,B8,X8,B9,C1,C2,C3,C4,X2,C5,C6,C7,C8,C9,X7,D1,D2,D3,D4,D5,X3,D6,D7,D8,D9,E1,E2,E3,X6,X5,X4,E4,E5,E6) )). + +cnf(byz,axiom, + ( state(X1,X2,X3,A1,A2,A3,A4,A5,A6,Y3,A7,A8,A9,B1,B2,B3,B4,X4,W3,W2,W1,Y2,B5,B6,B7,B8,B9,C1,C2,X5,W4,C3,W8,Y1,C4,C5,C6,C7,C8,C9,D1,X6,W5,W6,W7,D2,D3,D4,D5,D6,D7,X9,X8,X7) + = +state(Y1,Y2,Y3,A1,A2,A3,A4,A5,A6,X9,A7,A8,A9,B1,B2,B3,B4,X1,W1,W8,W7,X8,B5,B6,B7,B8,B9,C1,C2,X2,W2,C3,W6,X7,C4,C5,C6,C7,C8,C9,D1,X3,W3,W4,W5,D2,D3,D4,D5,D6,D7,X6,X5,X4) )). + +cnf(lxz,axiom, + ( state(X1,A1,A2,X2,A3,A4,X3,A5,A6,W1,W2,W3,X4,A7,A8,A9,B1,B2,B3,B4,Y3,W8,B5,W4,X5,B6,B7,B8,B9,C1,C2,C3,Y2,W7,W6,W5,X6,C4,C5,C6,C7,C8,C9,D1,Y1,X7,D2,D3,X8,D4,D5,X9,D6,D7) + = +state(Y1,A1,A2,Y2,A3,A4,Y3,A5,A6,W7,W8,W1,X1,A7,A8,A9,B1,B2,B3,B4,X9,W6,B5,W2,X2,B6,B7,B8,B9,C1,C2,C3,X8,W5,W4,W3,X3,C4,C5,C6,C7,C8,C9,D1,X7,X4,D2,D3,X5,D4,D5,X6,D6,D7) )). + +cnf(mxz,axiom, + ( state(A1,X1,A2,A3,X2,A4,A5,X3,A6,A7,A8,A9,B1,X4,B2,B3,B4,B5,B6,Y3,B7,B8,B9,C1,C2,X5,C3,C4,C5,C6,C7,Y2,C8,C9,D1,D2,D3,X6,D4,D5,D6,D7,D8,Y1,D9,E1,X7,E2,E3,X8,E4,E5,X9,E6) + = +state(A1,Y1,A2,A3,Y2,A4,A5,Y3,A6,A7,A8,A9,B1,X1,B2,B3,B4,B5,B6,X9,B7,B8,B9,C1,C2,X2,C3,C4,C5,C6,C7,X8,C8,C9,D1,D2,D3,X3,D4,D5,D6,D7,D8,X7,D9,E1,X4,E2,E3,X5,E4,E5,X6,E6) )). + +cnf(rxz,axiom, + ( state(A1,A2,X1,A3,A4,X2,A5,A6,X3,A7,A8,A9,B1,B2,X4,W3,W2,W1,Y3,B3,B4,B5,B6,B7,B8,B9,X5,W4,C1,W8,Y2,C2,C3,C4,C5,C6,C7,C8,X6,W5,W6,W7,Y1,C9,D1,D2,D3,X7,D4,D5,X8,D6,D7,X9) + = +state(A1,A2,Y1,A3,A4,Y2,A5,A6,Y3,A7,A8,A9,B1,B2,X1,W1,W8,W7,X9,B3,B4,B5,B6,B7,B8,B9,X2,W2,C1,W6,X8,C2,C3,C4,C5,C6,C7,C8,X3,W3,W4,W5,X7,C9,D1,D2,D3,X4,D4,D5,X5,D6,D7,X6) )). + +%-------------------------------------------------------------------------- diff --git a/tests/ROB027-1.p b/tests/ROB027-1.p new file mode 100644 --- /dev/null +++ b/tests/ROB027-1.p @@ -0,0 +1,62 @@ +%-------------------------------------------------------------------------- +% File : ROB027-1 : TPTP v6.3.0. Released v1.2.0. +% Domain : Robbins Algebra +% Problem : -(-c) = c => Boolean +% Version : [Win90] (equality) axioms. +% Theorem formulation : Denies Huntington's axiom. +% English : If there are elements c and d such that c+d=d, then the +% algebra is Boolean. + +% Refs : [HMT71] Henkin et al. (1971), Cylindrical Algebras +% : [Win90] Winker (1990), Robbins Algebra: Conditions that make a +% : [Wos94] Wos (1994), Two Challenge Problems +% Source : [Wos94] +% Names : - [Wos94] + +% Status : Open +% Rating : 1.00 v2.0.0 +% Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 2 RR) +% Number of atoms : 5 ( 5 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 5 ( 3 constant; 0-2 arity) +% Number of variables : 7 ( 0 singleton) +% Maximal term depth : 6 ( 3 average) +% SPC : CNF_UNK_UEQ + +% Comments : Commutativity, associativity, and Huntington's axiom +% axiomatize Boolean algebra. +%-------------------------------------------------------------------------- +%----Include axioms for Robbins algebra +%-------------------------------------------------------------------------- +cnf(commutativity_of_add,axiom, + ( add(X,Y) = add(Y,X) )). + +cnf(associativity_of_add,axiom, + ( add(add(X,Y),Z) = add(X,add(Y,Z)) )). + +cnf(robbins_axiom,axiom, + ( negate(add(negate(add(X,Y)),negate(add(X,negate(Y))))) = X )). + +%-------------------------------------------------------------------------- +%-------------------------------------------------------------------------- +cnf(double_negation,hypothesis, + ( negate(negate(c)) = c )). + +cnf(prove_huntingtons_axiom,negated_conjecture, + goal_lhs != b). + +cnf(anb, axiom, goal_anb = add(a, negate(b))). +cnf(nanb, axiom, goal_nanb = add(negate(a), negate(b))). +cnf(n_nanb, axiom, goal_n_nanb = negate(goal_nanb)). +cnf(n_anb, axiom, goal_n_anb = negate(goal_anb)). +cnf(lhs, axiom, goal_lhs = add(goal_n_anb, goal_n_nanb)). + +%-------------------------------------------------------------------------- +%----Definition of g +cnf(sos04,axiom,( + g(A) = negate(add(A,negate(A))) )). + +%----Definition of h +cnf(sos05,axiom,( + h(A) = add(A,add(A,add(A,g(A)))) )). diff --git a/tests/db-goal.p b/tests/db-goal.p new file mode 100644 --- /dev/null +++ b/tests/db-goal.p @@ -0,0 +1,22 @@ +% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf +% appendix b. theorem 3.4, clause 8. +cnf(a, axiom, '^'(X, Y) = '^'(Y, X)). +cnf(a, axiom, '^'(X, '^'(Y, Z)) = '^'(Y, '^'(X, Z))). +cnf(a, axiom, '^'('^'(X, Y), Z) = '^'(X, '^'(Y, Z))). +cnf(a, axiom, v(X, Y) = v(Y, X)). +cnf(a, axiom, v(X, v(Y, Z)) = v(Y, v(X, Z))). +cnf(a, axiom, v(v(X, Y), Z) = v(X, v(Y, Z))). +cnf(a, axiom, v(X, '^'(X, Y)) = X). +cnf(a, axiom, '^'(X, v(X, Y)) = X). +cnf(a, axiom, upme(X,Y,Z) = '^'(X, v(Y, Z))). +cnf(a, axiom, lome(X,Y,Z) = v('^'(X, Y), '^'(X, Z))). +cnf(a, axiom, upjo(X,Y,Z) = '^'(v(X, Y), v(X, Z))). +cnf(a, axiom, lojo(X,Y,Z) = v(X, '^'(Y, Z))). +cnf(a, axiom, v(upme('^'(a, X1),Y1,Z1), '^'(Y1, Z1)) = '^'(v('^'('^'(a, X1), Y1), Z1), v('^'('^'(a, X1), Z1), Y1))). +cnf(a, axiom, upme(X,Y,Z) = v(upme(X,Y,'^'(a, Z)), upme(X,Z,'^'(a, Y)))). +cnf(c1, axiom, c1 = upme(a,x2,y2)). +cnf(c2, axiom, c2 = upme(a,x2,z2)). +cnf(c3, axiom, c3 = upme(x2,y2,z2)). +cnf(c4, axiom, c4 = lome(x2,y2,z2)). +fof(a, conjecture, c1 = c2 => c3 = c4). +%fof(a, conjecture, (upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2))). diff --git a/tests/group.p b/tests/group.p --- a/tests/group.p +++ b/tests/group.p @@ -1,15 +1,16 @@ -fof(identity, axiom, - ![X]: f(X, e) = X). -fof(right_inverse, axiom, - ![X]: f(X, i(X)) = e). +%fof(identity, axiom, +% ![X]: f(X, e) = X). +%fof(right_inverse, axiom, +% ![X]: f(X, i(X)) = e). fof(associativity, axiom, ![X, Y, Z]: f(X, f(Y, Z)) = f(f(X, Y), Z)). -%fof(left_inverse, conjecture, -% ![X]: f(i(X),X) = e). -%fof(left_identity, conjecture, -% ![X]: f(e, X) = X). +fof(left_inverse, axiom, + ![X]: f(i(X),X) = e). +fof(left_identity, axiom, + ![X]: f(e, X) = X). +cnf(a, axiom, a != b). -fof(inverse_distrib, axiom, - ![X,Y]: f(i(X),i(Y)) = i(f(X,Y))). -fof(commutativity, conjecture, - ![X,Y]: f(X,Y) = f(Y,X)). +%fof(inverse_distrib, axiom, +% ![X,Y]: f(i(X),i(Y)) = i(f(X,Y))). +%fof(commutativity, conjecture, +% ![X,Y]: f(X,Y) = f(Y,X)). diff --git a/tests/nand-goal.p b/tests/nand-goal.p new file mode 100644 --- /dev/null +++ b/tests/nand-goal.p @@ -0,0 +1,44 @@ +%-------------------------------------------------------------------------- +% File : LAT071-1 : TPTP v6.2.0. Released v2.6.0. +% Domain : Lattice Theory (Orthomodularlattices) +% Problem : Given single axiom OML-21C, prove associativity +% Version : [MRV03] (equality) axioms. +% English : Given a single axiom candidate OML-21C for orthomodular lattices +% (OML) in terms of the Sheffer Stroke, prove a Sheffer stroke form +% of associativity. + +% Refs : [MRV03] McCune et al. (2003), Sheffer Stroke Bases for Ortholatt +% Source : [MRV03] +% Names : OML-21C-associativity [MRV03] + +% Status : Open +% Rating : 1.00 v2.6.0 +% Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR) +% Number of atoms : 2 ( 2 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 4 ( 3 constant; 0-2 arity) +% Number of variables : 4 ( 2 singleton) +% Maximal term depth : 6 ( 4 average) +% SPC : CNF_UNK_UEQ + +% Comments : +%-------------------------------------------------------------------------- +%----Single axiom OML-21C +cnf(oml_21C,axiom, + ( f(f(B,A),f(f(f(f(B,A),A),f(C,A)),f(f(A,A),D))) = A )). + +cnf(a, axiom, f(z, f(z, z)) = k). +cnf(fbc, axiom, fbc=f(b,c)). +cnf(fba, axiom, fba=f(b,a)). +cnf(fbc2, axiom, fbc2=f(fbc,fbc)). +cnf(fba2, axiom, fba2=f(fba,fba)). +cnf(lhs, axiom, lhs=f(a,fbc2)). +cnf(rhs, axiom, rhs=f(c,fba2)). +cnf(comm, axiom, f(X,Y)=f(Y,X)). + +%----Denial of Sheffer stroke associativity +cnf(associativity,negated_conjecture, + lhs != rhs). + +%-------------------------------------------------------------------------- diff --git a/tests/ring-goal.p b/tests/ring-goal.p new file mode 100644 --- /dev/null +++ b/tests/ring-goal.p @@ -0,0 +1,11 @@ +cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_zero, axiom, '+'('0', X) = X). +cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). +cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(cube, axiom, X = '*'(X, '*'(X, X))). +cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). +cnf(lhs, axiom, lhs = '*'(a, b)). +cnf(rhs, axiom, rhs = '*'(b, a)). diff --git a/tests/ring2-cancel.p b/tests/ring2-cancel.p new file mode 100644 --- /dev/null +++ b/tests/ring2-cancel.p @@ -0,0 +1,9 @@ +cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_zero, axiom, '+'('0', X) = X). +cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). +cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(power_six, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, '*'(X, X)))))). +cnf(conjecture, negated_conjecture, '+'(x, x) != '0'). diff --git a/tests/ring2-goal.p b/tests/ring2-goal.p new file mode 100644 --- /dev/null +++ b/tests/ring2-goal.p @@ -0,0 +1,12 @@ +cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_zero, axiom, '+'('0', X) = X). +cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). +cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(power_six, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, '*'(X, X)))))). +cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). +cnf(lhs, axiom, lhs = '*'(a, b)). +cnf(rhs, axiom, rhs = '*'(b, a)). +cnf(a, axiom, '+'(X, X) = '0'). diff --git a/tests/ring3-goal.p b/tests/ring3-goal.p new file mode 100644 --- /dev/null +++ b/tests/ring3-goal.p @@ -0,0 +1,11 @@ +cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_zero, axiom, '+'('0', X) = X). +cnf(plus_neg, axiom, '+'(X, '-'(X)) = '0'). +cnf(times_assoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(power_four, axiom, X = '*'(X, '*'(X, '*'(X, X)))). +cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). +cnf(lhs, axiom, lhs = '*'(a, b)). +cnf(rhs, axiom, rhs = '*'(b, a)). diff --git a/tests/ring4-goal.p b/tests/ring4-goal.p new file mode 100644 --- /dev/null +++ b/tests/ring4-goal.p @@ -0,0 +1,11 @@ +cnf(plus_comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(plus_assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(plus_zero, axiom, '+'('0', X) = X). +cnf(plus_inv, axiom, '+'(X, '-'(X)) = '0'). +cnf(times_ssoc, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)). +cnf(distrib, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))). +cnf(distrib, axiom, '*'('+'(X, Y), Z) = '+'('*'(X, Z), '*'(Y, Z))). +cnf(power_five, axiom, X = '*'(X, '*'(X, '*'(X, '*'(X, X))))). +cnf(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)). +cnf(lhs, axiom, lhs = '*'(a, b)). +cnf(rhs, axiom, rhs = '*'(b, a)). diff --git a/tests/robbins-goal.p b/tests/robbins-goal.p new file mode 100644 --- /dev/null +++ b/tests/robbins-goal.p @@ -0,0 +1,6 @@ +cnf(comm, axiom, '+'(X, Y) = '+'(Y, X)). +cnf(assoc, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)). +cnf(funny, axiom, '-'('+'('-'('+'(X, Y)), '-'('+'(X, '-'(Y))))) = X). +cnf(ma, axiom, '-'(a) = ma). +cnf(mma, axiom, '-'(ma) = mma). +cnf(conjecture, negated_conjecture, mma != a). diff --git a/tests/veroff.p b/tests/veroff.p --- a/tests/veroff.p +++ b/tests/veroff.p @@ -7,4 +7,10 @@ cnf(associativity, axiom, f(f(X,W,Y),W,Z) = f(X,W,f(Y,W,Z))). -cnf(goal, axiom, f(f(a1,a2,a3),a4,a5) != f(f(a1,a4,a5),f(a2,a4,a5),f(a3,a4,a5))). +cnf(a123, axiom, f(a1,a2,a3) = f123). +cnf(a145, axiom, f(a1,a4,a5) = f145). +cnf(a245, axiom, f(a2,a4,a5) = f245). +cnf(a345, axiom, f(a3,a4,a5) = f345). +cnf(lhs, axiom, f(f123,a4,a5) = c1). +cnf(rhs, axiom, f(f145,f245,f345) = c2). +cnf(goal, axiom, c1 != c2). diff --git a/twee.cabal b/twee.cabal --- a/twee.cabal +++ b/twee.cabal @@ -1,5 +1,5 @@ name: twee -version: 2.1.5 +version: 2.2 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3 @@ -36,23 +36,16 @@ description: Build a binary which statically links against libstdc++. default: False -flag llvm - description: Build using LLVM backend for faster code. - default: False - executable twee main-is: executable/Main.hs default-language: Haskell2010 build-depends: base < 5, - twee-lib == 2.1.5, + twee-lib == 2.2, containers, pretty, split, - jukebox >= 0.3.5 - ghc-options: -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100 - - if flag(llvm) - ghc-options: -fllvm + jukebox == 0.4.* + ghc-options: -W -fno-warn-incomplete-patterns if flag(static) ghc-options: -optl -static