twee 2.3.1 → 2.4
raw patch · 53 files changed
+813/−1354 lines, 53 filesdep ~jukeboxdep ~twee-lib
Dependency ranges changed: jukebox, twee-lib
Files
- executable/SequentialMain.hs +148/−55
- misc/BestTwee.hs +119/−68
- misc/Test.hs +228/−0
- misc/print_trace.pl +50/−0
- misc/test.hs +0/−161
- tests/GRP196-1.p +40/−0
- tests/RNG025-buggy.p +9/−0
- tests/append-rev-ascii.p +0/−4
- tests/blah.p +0/−5
- tests/db.p +0/−28
- tests/db2.p +0/−29
- tests/gmv1-ascii.p +0/−19
- tests/gmv1.p +0/−46
- tests/gmv10-ascii.p +0/−19
- tests/gmv10.p +0/−46
- tests/gmv11-ascii.p +0/−19
- tests/gmv11.p +0/−46
- tests/gmv12-ascii.p +0/−19
- tests/gmv12.p +0/−46
- tests/gmv13-ascii.p +0/−19
- tests/gmv13.p +0/−46
- tests/gmv14-ascii.p +0/−19
- tests/gmv14.p +0/−46
- tests/gmv15-ascii.p +0/−19
- tests/gmv15.p +0/−46
- tests/gmv2-ascii.p +0/−19
- tests/gmv2.p +0/−46
- tests/gmv3-ascii.p +0/−19
- tests/gmv3.p +0/−46
- tests/gmv4-ascii.p +0/−19
- tests/gmv4.p +0/−46
- tests/gmv5-ascii.p +0/−19
- tests/gmv5.p +0/−46
- tests/gmv6-ascii.p +0/−19
- tests/gmv6.p +0/−46
- tests/gmv7-ascii.p +0/−19
- tests/gmv7.p +0/−46
- tests/gmv8-ascii.p +0/−19
- tests/gmv8.p +0/−46
- tests/gmv9-ascii.p +0/−19
- tests/gmv9.p +0/−46
- tests/group_plain.p +0/−14
- tests/loop-ascii.p +0/−6
- tests/rellat_appendixa.p +27/−0
- tests/rellat_appendixb.p +28/−0
- tests/rellat_appendixb_easier.p +30/−0
- tests/rellat_appendixc.p +30/−0
- tests/rellat_theorem34_6.p +32/−0
- tests/rellat_theorem34_6a.p +29/−0
- tests/rellat_theorem34_6b.p +29/−0
- tests/y-easy.p +0/−3
- tests/y-encoded.p +5/−0
- twee.cabal +9/−6
executable/SequentialMain.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DerivingVia #-}+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DeriveAnyClass #-} {-# OPTIONS_GHC -flate-specialise #-} module SequentialMain(main) where @@ -32,9 +32,10 @@ import System.IO import System.Exit import qualified Data.Set as Set-import qualified Twee.Label as Label+import qualified Data.Label as Label import System.Console.ANSI import Data.Symbol+import Twee.Profile data MainFlags = MainFlags {@@ -45,14 +46,19 @@ flags_flip_ordering :: Bool, flags_give_up_on_saturation :: Bool, flags_flatten_goals :: Bool,+ flags_flatten_nonground :: Bool, flags_flatten_goals_lightly :: Bool, flags_flatten_all :: Bool, flags_eliminate :: [String],- flags_backwards_goal :: Int }+ flags_backwards_goal :: Int,+ flags_flatten_backwards_goal :: Int,+ flags_equals_transformation :: Bool,+ flags_distributivity_heuristic :: Bool,+ flags_kbo_weight0 :: Bool } parseMainFlags :: OptionParser MainFlags parseMainFlags =- MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal+ MainFlags <$> proof <*> trace <*> formal <*> explain <*> flipOrdering <*> giveUp <*> flatten <*> flattenNonGround <*> flattenLightly <*> flattenAll <*> eliminate <*> backwardsGoal <*> flattenBackwardsGoal <*> equalsTransformation <*> distributivityHeuristic <*> kboWeight0 where proof = inGroup "Output options" $@@ -76,6 +82,10 @@ expert $ inGroup "Term order options" $ bool "flip-ordering" ["Make more common function symbols smaller (off by default)."] False+ kboWeight0 =+ expert $+ inGroup "Term order options" $+ bool "kbo-weight0" ["Give functions of arity >= 2 a weight of 0."] False giveUp = expert $ inGroup "Output options" $@@ -84,6 +94,10 @@ expert $ inGroup "Completion heuristics" $ bool "flatten-goal" ["Flatten goal by adding new axioms (on by default)."] True+ flattenNonGround =+ expert $+ inGroup "Completion heuristics" $+ bool "flatten-nonground" ["Flatten even non-ground clauses (off by default)."] False flattenLightly = expert $ inGroup "Completion heuristics" $@@ -96,6 +110,18 @@ expert $ inGroup "Completion heuristics" $ flag "backwards-goal" ["Try rewriting backwards from the goal this many times (0 by default)."] 0 argNum+ flattenBackwardsGoal =+ expert $+ inGroup "Completion heuristics" $+ flag "flatten-backwards-goal" ["Try rewriting backwards from the goal this many times when flattening (0 by default)."] 0 argNum+ equalsTransformation =+ expert $+ inGroup "Completion heuristics" $+ bool "equals-transformation" ["Apply the 'equals transformation' even to ground goals (off by default)."] False+ distributivityHeuristic =+ expert $+ inGroup "Completion heuristics" $+ bool "distributivity-heuristic" ["Treat distributive operators specially (off by default)."] False eliminate = inGroup "Proof presentation" $ concat <$>@@ -282,8 +308,7 @@ con_size :: !Integer, con_weight :: !Integer, con_bonus :: !Bool }- deriving (Eq, Ord)- deriving Labelled via AutoLabel Constant+ deriving (Eq, Ord, Labelled) data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int deriving (Eq, Ord)@@ -345,10 +370,17 @@ ctx_type :: Type } -- Convert back and forth between Twee and Jukebox.-tweeConstant :: HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Constant-tweeConstant flags TweeContext{..} prec fun+tweeConstant :: MainFlags -> HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Constant+tweeConstant MainFlags{..} flags TweeContext{..} prec fun | fun == ctx_minimal = Minimal- | otherwise = Constant prec fun (Jukebox.arity fun) 1 1 (bonus fun)+ | otherwise =+ Constant {+ con_prec = prec,+ con_id = fun,+ con_arity = Jukebox.arity fun,+ con_size = if flags_kbo_weight0 && Jukebox.arity fun >= 2 then 0 else 1,+ con_weight = 1,+ con_bonus = bonus fun } where bonus fun = (isIfeq fun && encoding flags /= Asymmetric2) ||@@ -378,13 +410,13 @@ jukeboxFunction _ Constant{..} = con_id jukeboxFunction TweeContext{..} Minimal = ctx_minimal -tweeTerm :: HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term Constant-tweeTerm flags ctx prec t = build (tm t)+tweeTerm :: MainFlags -> HornFlags -> TweeContext -> (Jukebox.Function -> Precedence) -> Jukebox.Term -> Term Constant+tweeTerm flags horn ctx prec t = build (tm t) where tm (Jukebox.Var (x ::: _)) = var (V (fromIntegral (Label.labelNum (Label.label x)))) tm (f :@: ts) =- app (fun (tweeConstant flags ctx (prec f) f)) (map tm ts)+ app (fun (tweeConstant flags horn ctx (prec f) f)) (map tm ts) jukeboxTerm :: TweeContext -> Term Constant -> Jukebox.Term jukeboxTerm TweeContext{..} (Var (V x)) =@@ -416,45 +448,102 @@ ctx_equals = equals, ctx_type = ty } -flattenGoals :: Bool -> Bool -> Problem Clause -> Problem Clause-flattenGoals flattenAll full prob =+flattenGoals :: Int -> Bool -> Bool -> Bool -> Problem Clause -> Problem Clause+flattenGoals backwardsGoal flattenNonGround flattenAll full prob = run prob $ \prob -> do- cs <- concat <$> mapM flatten prob- return $- prob ++- [ Input{tag = "flattening", kind = Jukebox.Ax Definition,- what = c, source = Unknown }- | c <- cs ]+ let ts = usort $ extraTerms prob+ cs <- mapM define ts+ return (prob ++ cs) where- flatten Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} =- liftM2 (++) (flat x) (flat y)- flatten Input{what = Clause (Bind _ [Pos (x Jukebox.:=: y)])}- | flattenAll =- liftM2 (++) (flat x) (flat y)- flatten _ = return []+ extraTerms prob = concatMap (input prob) prob+ input prob Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])} =+ concatMap term (backwards backwardsGoal prob x) +++ concatMap term (backwards backwardsGoal prob y)+ input _ Input{what = Clause (Bind _ [Pos (x Jukebox.:=: y)])}+ | flattenAll = term x ++ term y+ input _ _ = [] - flat (f :@: ts)- | not (all isVar ts) || usort ts /= ts = do- name <- newName f- let vs = Jukebox.vars ts- g = name ::: FunType (map typ vs) (typ f)- c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)]- css <- if full then concat <$> mapM flat ts else return []- return (c:css)- flat _ = return []+ term t@(_f :@: ts) =+ [ t+ | ground t || flattenNonGround,+ not (all isVar ts) || usort ts /= sort ts ] +++ if full then concatMap term ts else []+ term _ = [] isVar (Jukebox.Var _) = True isVar _ = False + define (f :@: ts) = do+ name <- newName f+ let vs = Jukebox.vars ts+ g = name ::: FunType (map typ vs) (typ f)+ c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: f :@: ts)]+ return Input{tag = "flattening", kind = Jukebox.Ax Definition,+ what = c, source = Unknown }++ backwards 0 _ t = [t]+ backwards n cs t =+ t:+ [ v+ | Input{what = Clause (Bind _ [Pos (x0 Jukebox.:=: y0)])} <- cs,+ (x, y) <- [(x0, y0), (y0, x0)],+ (s, k) <- contexts t,+ sub <- maybeToList (Jukebox.match x s),+ let u = k (Jukebox.subst sub y),+ ground u,+ v <- backwards (n-1) cs u ]++addDistributivityHeuristic :: Problem Clause -> Problem Clause+addDistributivityHeuristic prob =+ run prob $ \prob -> do+ cs <- mapM add prob+ return (prob ++ catMaybes cs)++ where+ add Input{what = Clause (Bind _ [Pos (t Jukebox.:=: u)])} =+ case checkDistributivity t u `mplus` checkDistributivity u t of+ Just (f, g, ty) -> do+ name <- newName (base f ++ "_" ++ base g)+ x <- Jukebox.Var <$> newSymbol "X" ty+ y <- Jukebox.Var <$> newSymbol "Y" ty+ z <- Jukebox.Var <$> newSymbol "Z" ty+ Just <$> define name (g :@: [f :@: [x, y], z])+ _ -> return Nothing+ add _ = return Nothing++ checkDistributivity+ (f1 :@: [Jukebox.Var x1, g1 :@: [Jukebox.Var y1, Jukebox.Var z1]])+ (g2 :@: [f2 :@: [Jukebox.Var x2, Jukebox.Var y2],+ f3 :@: [Jukebox.Var x3, Jukebox.Var z2]])+ | f1 == f2 && f2 == f3 && g1 == g2 &&+ x1 == x2 && x2 == x3 && y1 == y2 && z1 == z2 =+ Just (f1, g1, Jukebox.typ x1)+ + checkDistributivity+ (f1 :@: [g1 :@: [Jukebox.Var x1, Jukebox.Var y1], Jukebox.Var z1])+ (g2 :@: [f2 :@: [Jukebox.Var x2, Jukebox.Var z2],+ f3 :@: [Jukebox.Var y2, Jukebox.Var z3]])+ | f1 == f2 && f2 == f3 && g1 == g2 &&+ x1 == x2 && y1 == y2 && z1 == z2 && z2 == z3 =+ Just (f1, g1, Jukebox.typ x1)+ checkDistributivity _ _ = Nothing++ define name t = do+ let vs = Jukebox.vars t+ g = name ::: FunType (map typ vs) (typ t)+ c = clause [Pos (g :@: map Jukebox.Var vs Jukebox.:=: t)]+ return Input{tag = "distributivity_heuristic", kind = Jukebox.Ax Definition,+ what = c, source = Unknown }+ -- Encode existentials so that all goals are ground.-addNarrowing :: TweeContext -> Problem Clause -> Problem Clause-addNarrowing TweeContext{..} prob =+addNarrowing :: Bool -> TweeContext -> Problem Clause -> Problem Clause+addNarrowing alwaysNarrow TweeContext{..} prob = unchanged ++ equalityClauses where (unchanged, nonGroundGoals) = partitionEithers (map f prob) where f inp@Input{what = Clause (Bind _ [Neg (x Jukebox.:=: y)])}- | not (ground x) || not (ground y) =+ | not (ground x) || not (ground y) || alwaysNarrow = Right (inp, (x, y)) f inp = Left inp @@ -483,7 +572,7 @@ let form = And (map (Literal . snd) equalityLiterals) in ForAll (Bind (Set.fromList (vars form)) form), source =- Inference "encode_existential" "esa"+ inference "encode_existential" "esa" (map (fmap toForm . fst) nonGroundGoals) } input tag form =@@ -492,7 +581,7 @@ kind = Conj Conjecture, what = clause [form], source =- Inference "split_conjunct" "thm" [justification] }+ inference "split_conjunct" "thm" [justification] } in [input tag form | (tag, form) <- equalityLiterals] @@ -527,15 +616,18 @@ identify inp = Left inp runTwee :: GlobalFlags -> TSTPFlags -> HornFlags -> [String] -> Config Constant -> MainFlags -> (IO () -> IO ()) -> Problem Clause -> IO Answer-runTwee globals (TSTPFlags tstp) horn precedence config MainFlags{..} later obligs = {-# SCC runTwee #-} do+runTwee globals (TSTPFlags tstp) horn precedence config flags@MainFlags{..} later obligs = {-# SCC runTwee #-} do let -- Encode whatever needs encoding in the problem- obligs'- | flags_flatten_goals_lightly = flattenGoals False False obligs- | flags_flatten_all = flattenGoals True True obligs- | flags_flatten_goals = flattenGoals False True obligs+ obligs1+ | flags_flatten_goals_lightly = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False False obligs+ | flags_flatten_all = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground True True obligs+ | flags_flatten_goals = flattenGoals flags_flatten_backwards_goal flags_flatten_nonground False True obligs | otherwise = obligs- ctx = makeContext obligs'+ obligs2+ | flags_distributivity_heuristic = addDistributivityHeuristic obligs1+ | otherwise = obligs1+ ctx = makeContext obligs2 lowercaseSkolem x | hasLabel "skolem" x = withRenamer x $ \s i ->@@ -543,7 +635,7 @@ Renaming xss xs -> Renaming (map (map toLower) xss) (map toLower xs) | otherwise = x- prob = prettyNames (mapName lowercaseSkolem (addNarrowing ctx obligs'))+ prob = prettyNames (mapName lowercaseSkolem (addNarrowing flags_equals_transformation ctx obligs2)) (unsortedAxioms0, goals0) <- case identifyProblem ctx prob of@@ -568,7 +660,7 @@ -- Translate everything to Twee. toEquation (t, u) =- canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u)+ canonicalise (tweeTerm flags horn ctx prec t :=: tweeTerm flags horn ctx prec u) axiomCompare ax1 ax2 | ax1' `simplerThan` ax2' = LT@@ -707,7 +799,7 @@ Just inp -> go inp where go Input{source = Unknown} = []- go Input{source = Inference _ _ inps} = concatMap go inps+ go Input{source = Inference _ _ inps} = concatMap (go . inputValue) inps go inp@Input{source = FromFile _ _} = [inp] when flags_explain_encoding $ do@@ -758,7 +850,7 @@ KBO.size (rhs rule), rhs rule) actives = sortBy (comparing (score . active_rule)) $- IntMap.elems (st_active_ids state')+ IntMap.elems (st_active_set state') when (tstp && configIsComplete config) $ do putStrLn "% SZS output start Saturation"@@ -802,7 +894,7 @@ kind = Jukebox.Ax Jukebox.Axiom, what = false, source =- Inference "resolution" "thm"+ inference "resolution" "thm" [-- A proof of t != u existentialHack pg_goal_hint (fromJust (lookup pg_number goals)), -- A proof of t = u@@ -831,7 +923,7 @@ kind = Jukebox.Ax Jukebox.Axiom, what = jukeboxEquation (equation (certify p)), source =- Inference name "thm" sources }+ inference name "thm" sources } where (name, sources) = unpack p @@ -861,7 +953,7 @@ -- if not, try its ancestors. find inp | ok inp = [inp] find Input{source = Inference _ _ inps} =- concatMap find inps+ concatMap (find . inputValue) inps find _ = [] ok inp =@@ -877,7 +969,7 @@ main = do hSetBuffering stdout LineBuffering- join . parseCommandLineWithExtraArgs+ stampM (intern "twee") . join . parseCommandLineWithExtraArgs ["--no-conjunctive-conjectures", "--no-split"] #ifdef VERSION_twee "Twee, an equational theorem prover" . version ("twee version " ++ VERSION_twee) $@@ -898,6 +990,7 @@ expert (toFof <$> clausifyBox <*> pure (tags True)) =>>= expert clausifyBox =>>= expert oneConjectureBox) <*> (runTwee <$> globalFlags <*> tstpFlags <*> expert hornFlags <*> parsePrecedence)))+ profile where combine horn config main encode prove later prob0 = do res <- horn prob0@@ -909,5 +1002,5 @@ isUnitEquality [Neg (_ Jukebox.:=: _)] = True isUnitEquality _ = False isUnit = all isUnitEquality (map (toLiterals . what) prob0)- main' = if isUnit then main else main{flags_formal_proof = False}+ main' = if isUnit then main{flags_explain_encoding = False} else main{flags_formal_proof = False} encode prob >>= prove config main' later
misc/BestTwee.hs view
@@ -1,3 +1,6 @@+{-# LANGUAGE TemplateHaskell #-}+module Main where+ import MaxCover import System.FilePath import System.FilePath.Glob@@ -7,6 +10,9 @@ import Data.List import Data.Maybe import Data.Time.Clock+import qualified Data.Map as Map+import Data.Map(Map)+import Data.FileEmbed solvedInTime :: NominalDiffTime -> FilePath -> String -> IO Bool solvedInTime timeLimit dir prob = do@@ -18,31 +24,45 @@ return (diffUTCTime outTime errTime <= timeLimit) notE :: [(String, Double)]-notE = [- ("LAT168-1", 0.30), ("LAT171-1", 0.43), ("ALG240-1", 0.48), ("LAT174-1", 0.65), ("GRP768-1", 0.70),- ("LAT142-1", 0.70), ("GRP505-1", 0.74), ("LAT145-1", 0.74), ("LAT164-1", 0.74), ("RNG025-5", 0.74),- ("GRP506-1", 0.78), ("GRP507-1", 0.78), ("LAT018-1", 0.78), ("LAT148-1", 0.78), ("LAT153-1", 0.78),- ("LAT155-1", 0.78), ("RNG025-4", 0.78), ("GRP508-1", 0.83), ("KLE151-10", 0.83), ("LAT162-1", 0.83),- ("ALG246-1", 0.87), ("GRP024-5", 0.87), ("GRP766-1", 0.87), ("LAT146-1", 0.87), ("LAT159-1", 0.87),- ("LAT160-1", 0.87), ("LAT170-1", 0.87), ("LAT177-1", 0.87), ("REL022-2", 0.87), ("COL042-10", 0.91),- ("GRP196-1", 0.91), ("GRP666-3", 0.91), ("GRP666-4", 0.91), ("GRP666-5", 0.91), ("LAT156-1", 0.91),- ("LAT157-1", 0.91), ("LAT169-1", 0.91), ("LCL148-10", 0.91), ("REL020-2", 0.91), ("REL021-1", 0.91),- ("REL021-2", 0.91), ("REL022-1", 0.91), ("REL029-1", 0.91), ("REL033-1", 0.91), ("REL033-3", 0.91),- ("REL034-1", 0.91), ("REL034-2", 0.91), ("REL035-1", 0.91), ("REL035-2", 0.91), ("REL036-1", 0.91),- ("GRP164-1", 0.96), ("GRP164-2", 0.96), ("GRP666-2", 0.96), ("GRP678-1", 0.96), ("GRP721-1", 0.96),- ("GRP725-1", 0.96), ("KLE110-10", 0.96), ("LAT072-1", 0.96), ("LAT076-1", 0.96), ("LAT140-1", 0.96),- ("LAT141-1", 0.96), ("LAT144-1", 0.96), ("LAT147-1", 0.96), ("LAT149-1", 0.96), ("LAT151-1", 0.96),- ("LAT158-1", 0.96), ("LAT163-1", 0.96), ("LAT167-1", 0.96), ("LAT172-1", 0.96), ("LAT173-1", 0.96),- ("LAT175-1", 0.96), ("LAT176-1", 0.96), ("LAT183-10", 0.96), ("LAT186-10", 0.96), ("LCL927-10", 0.96),- ("REL020-1", 0.96), ("REL040-1", 0.96), ("REL040-3", 0.96), ("GRP177-1", 1.00), ("GRP724-1", 1.00),- ("LAT074-1", 1.00), ("LAT075-1", 1.00), ("LAT077-1", 1.00), ("LAT078-1", 1.00), ("LAT079-1", 1.00),- ("LAT139-1", 1.00), ("LAT161-1", 1.00), ("LCL220-10", 1.00), ("LCL330-10", 1.00), ("LCL348-10", 1.00),- ("REL032-1", 1.00), ("REL032-2", 1.00), ("REL038-1", 1.00), ("REL039-1", 1.00), ("ROB007-1", 1.00),- ("ROB033-1", 1.00)]+notE = filter (\(x, _) -> '+' `notElem` x) [+ ("GRP702+1", 0.06), ("GRP715+1", 0.06), ("GRP660+2", 0.12), ("GRP660+3", 0.12),+ ("GRP665+1", 0.12), ("GRP700+1", 0.12), ("GRP658+1", 0.18), ("GRP659+1", 0.18),+ ("GRP656+1", 0.24), ("GRP657+1", 0.24), ("GRP660+1", 0.24), ("GRP682+1", 0.24),+ ("GRP683+1", 0.24), ("GRP685+1", 0.24), ("GRP703+1", 0.24), ("GRP704+1", 0.24),+ ("GRP710+1", 0.24), ("GRP777+1", 0.24), ("LCL897+1", 0.29), ("LAT168-1", 0.30),+ ("LAT171-1", 0.43), ("ALG240-1", 0.48), ("GRP654+2", 0.53), ("GRP654+3", 0.53),+ ("GRP655+2", 0.53), ("GRP655+3", 0.53), ("LAT174-1", 0.65), ("LAT142-1", 0.70),+ ("GRP654+1", 0.71), ("GRP655+1", 0.71), ("GRP505-1", 0.74), ("LAT145-1", 0.74),+ ("LAT164-1", 0.74), ("GRP506-1", 0.78), ("GRP507-1", 0.78), ("LAT018-1", 0.78),+ ("LAT148-1", 0.78), ("LAT153-1", 0.78), ("LAT155-1", 0.78), ("GRP508-1", 0.83),+ ("KLE151-10", 0.83), ("LAT162-1", 0.83), ("LAT146-1", 0.87), ("LAT159-1", 0.87),+ ("LAT160-1", 0.87), ("LAT170-1", 0.87), ("LAT177-1", 0.87), ("GRP664+1", 0.88),+ ("ALG441-10", 0.91), ("COL042-10", 0.91), ("GRP196-1", 0.91), ("GRP666-3", 0.91),+ ("GRP666-4", 0.91), ("GRP666-5", 0.91), ("LAT156-1", 0.91), ("LAT169-1", 0.91),+ ("LCL148-10", 0.91), ("GRP164-2", 0.96), ("GRP666-2", 0.96), ("GRP678-1", 0.96),+ ("GRP725-1", 0.96), ("KLE110-10", 0.96), ("LAT072-1", 0.96), ("LAT076-1", 0.96),+ ("LAT140-1", 0.96), ("LAT141-1", 0.96), ("LAT144-1", 0.96), ("LAT147-1", 0.96),+ ("LAT149-1", 0.96), ("LAT151-1", 0.96), ("LAT158-1", 0.96), ("LAT163-1", 0.96),+ ("LAT167-1", 0.96), ("LAT172-1", 0.96), ("LAT173-1", 0.96), ("LAT175-1", 0.96),+ ("LAT176-1", 0.96), ("LCL927-10", 0.96), ("REL040-1", 0.96), ("REL040-3", 0.96),+ ("ALG212+1", 1.00), ("ALG213+1", 1.00), ("GRP724-1", 1.00), ("KLE122-10", 1.00),+ ("LAT074-1", 1.00), ("LAT075-1", 1.00), ("LAT077-1", 1.00), ("LAT078-1", 1.00),+ ("LAT079-1", 1.00), ("LAT139-1", 1.00), ("LAT161-1", 1.00), ("LCL220-10", 1.00),+ ("LCL330-10", 1.00), ("LCL348-10", 1.00), ("REL032-2", 1.00), ("REL038-1", 1.00),+ ("REL039-1", 1.00)] +ratings :: Map String Double+ratings =+ Map.fromList+ [ (name, read rating)+ | [name, rating] <- map words (lines input)]+ where+ input = $(embedStringFile "ratings")+ problemBonus :: (Int, Int, Int, Int, Int, Int) -> String -> Int problemBonus (b0, b1, b2, b3, b4, b5) p =- case lookup p notE of+ ebonus *+ case Map.lookup p ratings of Nothing -> b0 Just x | x < 0.7 -> b1@@ -50,6 +70,11 @@ | x < 0.9 -> b3 | x < 0.95 -> b4 | otherwise -> b5+ where+ ebonus =+ case lookup p notE of+ Nothing -> 1+ Just _ -> 1 greatProblemsBonus :: (Int, Int, Int, Int, Int, Int) -> String -> [String] greatProblemsBonus b p =@@ -58,20 +83,27 @@ bonuses :: [(String, (Int, Int, Int, Int, Int, Int))] bonuses = [("no bonus", (1, 1, 1, 1, 1, 1)),- ("low bonus", (1, 1, 2, 3, 4, 5)),- ("medium bonus", (1, 2, 4, 6, 8, 10)),- ("high bonus", (0, 1, 2, 3, 4, 5)),- ("big fish", (0, 0, 0, 0, 1, 1))]+ ("low bonus", (1, 1, 2, 3, 5, 10)),+ --("medium bonus", (1, 2, 4, 6, 8, 10)),+ --("high bonus", (0, 1, 2, 3, 4, 5)),+ --("big fish", (0, 0, 0, 0, 1, 1)),+ ("rating 1", (0, 0, 0, 0, 0, 1))] readResults ok = do- filenames <- glob "out/twee-*/success"+ filenames <- glob "/home/nick/writing/twee/times/*-twee-casc-extra-*" fmap (filter (\(x, _) -> x `notElem` banned)) $ forM filenames $ \filename -> do- let directory = takeDirectory filename- let name = takeFileName directory- solved <- fmap (filter ok) $ lines <$> readFile filename- fast <- filterM (solvedInTime 120 directory) solved- slow <- filterM (solvedInTime 600 directory) solved- return (name, (fast, slow))+ let name = takeFileName filename+ let unpack xs = (takeBaseName name, read time :: Double) where [name, time] = words xs+ solved <- filter (ok . fst) . map unpack . lines <$> readFile filename+ let solvedInTime t = [name | (name, time) <- solved, time < t]+-- fast <- filterM (solvedInTime 120 directory) solved+-- med <- filterM (solvedInTime 240 directory) solved+-- slow <- filterM (solvedInTime 600 directory) solved+ let fast = solvedInTime 210+ let med = solvedInTime 300+ let slow = solvedInTime (1/0)+ + return (name, (fast, med, slow)) score results cover = length (usort (concat [probs | (name, probs) <- results, name `elem` cover]))@@ -85,37 +117,41 @@ find x = fromJust (lookup x results) main = do- probs <- lines <$> readFile "casc-j10"+ probs <- lines <$> readFile "unsat" results <- readResults (`elem` probs) let options =- [("fast", \(fast, _) -> (fast, []))]- --("slow", \(_, slow) -> ([], slow)),- --("fast and slow", id)]+ [("fast", \(fast, _, _) -> (fast, [], [])),+ ("med", \(_, med, _) -> ([], med, []))]+ --("slow", \(_, _, slow) -> ([], [], slow))]+ --("fast and med", \(fast, med, _) -> (fast, med, []))] - forM_ options $ \(option, f) -> do- forM_ bonuses $ \(bonus, b) -> do+ forM_ bonuses $ \(bonus, b) -> do+ forM_ options $ \(option, f) -> do let results1 = [ (name, map (++ "/fast") (concatMap (greatProblemsBonus b) fast) +++ map (++ "/med") (concatMap (greatProblemsBonus b) med) ++ map (++ "/slow") (concatMap (greatProblemsBonus b) slow)) | (name, res) <- results,- let (fast, slow) = f res ]+ let (fast, med, slow) = f res ] best = greedy results1 putStrLn (option ++ "/" ++ bonus ++ ":")- forM_ (zip3 [1..] best (inits best)) $ \(i, name, names) -> do- putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (levels results1 name names))+ forM_ (take 6 $ zip3 [1..] best (inits best)) $ \(i, name, names) -> do+ putStrLn (show i ++ ". " ++ name ++ " " ++ show (score results1 (name:names)) ++ ", useful at levels " ++ show (drop (length fixed) $ levels results1 name names)) putStrLn "" --- putStrLn "\nBest:"--- forM_ [1..8] $ \i -> do--- cover <- maxCover i results1--- putStrLn (show i ++ ": " ++ show (score results1 cover))--- forM_ cover $ \name -> putStrLn (" " ++ name)+{-+ putStrLn "Best:"+ forM_ [1..6] $ \i -> do+ cover <- maxCover i results1+ putStrLn (show i ++ ": " ++ show (score results1 cover))+ forM_ cover $ \name -> putStrLn (" " ++ name)+-} greedy [] = [] greedy results =@@ -131,27 +167,42 @@ Nothing -> Left (length probs) fixed :: [String]-fixed = [- "twee-200715-twee-goal-flip-lhs2",- "twee-200714-twee-goalagain",- "twee-200712-twee-ghc8.10",- "twee-200714-twee-goalagain-flip-lhs1",- "twee-200715-twee-goal-lhs4-var3",- "twee-200715-twee-goal-lhs6-var3",- "twee-200715-twee-goal-lhs2-var3",- "twee-200611-twee-flip-lhs9"]---fixed = [--- "twee-200612-twee-aggressive-renormalise-flip-lhs4",--- "twee-200612-twee-aggressive-renormalise-flip-lhs9",--- "twee-200611-twee-flip-lhs1",--- "twee-200611-twee-lhs4",--- "twee-200611-twee-lhs5",--- "twee-200612-twee-aggressive-renormalise-nodup",--- "twee-200611-twee-nosimp",--- "twee-200612-twee-aggressive-renormalise-nodepth"]+fixed = fixed_new+fixed_new = take 6 [+ "twee-210619-twee-casc-extra-lhsnormal-flatten",+ "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",+ "twee-210619-twee-casc-extra-depth-60",+ "twee-210619-twee-casc-extra-no-dup",+ "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm-kbo0",+ "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0"] +fixed_old = take 2 [+ "twee-210619-twee-casc-extra-no-dup",+ "twee-210621-twee-casc-extra-depth-60-kbo0",+ "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm",+ "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm-kbo0",+ "twee-210621-twee-casc-extra-complete-subsets-flatten",+ "twee-210619-twee-casc-extra-lhs9-flip-nogoal",+ "twee-210619-twee-casc-extra-no-dup-nogoal"]++{- attempt 2:+fixed = take 0 [+ "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0",+ "twee-210621-twee-casc-extra-depth-60-kbo0",+ "twee-210619-twee-casc-extra-complete-subsets",+ "twee-210621-twee-casc-extra-flatten-lhs9-kbo0",+ "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm",+ "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0"]+ -}++{- attempt 1:+ "twee-210621-twee-casc-extra-flatten-lhs9-kbo0",+ "twee-210619-twee-casc-extra-lhs9-nogoal-aggrnorm",+ "twee-210621-twee-casc-extra-depth-60-kbo0",+ "twee-210619-twee-casc-extra-complete-subsets",+ "twee-210619-twee-casc-extra-lhs9-flip-nogoal-kbo0",+ "twee-210619-twee-casc-extra-lhs5-flip-aggrnorm-kbo0"]+-}+ banned :: [String] banned = []--- "twee-200714-twee-goalagain",--- "twee-200714-twee-goalagain-flip-lhs1",--- "twee-200714-twee-goalagain-flip-lhs3"]
+ misc/Test.hs view
@@ -0,0 +1,228 @@+{-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts, UndecidableInstances, StandaloneDeriving, ScopedTypeVariables, TupleSections, DeriveGeneric, DerivingVia, DeriveAnyClass #-}+module Test where++import Twee.Constraints+import Twee.Term hiding (subst, canonicalise, F)+import Twee.Term.Core hiding (F)+import Test.QuickCheck hiding (Function, Fun)+import Test.QuickCheck.All+import Twee.Pretty+import Twee.CP+import Twee.Proof+import qualified Twee.KBO as Ord+import Text.PrettyPrint+import Twee.Base hiding (F)+import Twee.Rule+import Twee.Equation+import Control.Monad+import qualified Data.Map as Map+import Data.Maybe+import Data.Ord+import Data.List+import Data.Typeable+import qualified Twee.Index as Index+import Data.Int+import GHC.Generics+import Twee.Utils++data Func = F Int Integer deriving (Eq, Ord, Show)+ deriving Labelled via (AutoLabel Func)++instance Pretty Func where pPrint (F f _) = text "f" <#> int f+instance PrettyTerm Func+instance Arbitrary (Subst Func) where+ arbitrary = fmap fromJust (fmap listToSubst (liftM2 zip (fmap nub arbitrary) (infiniteListOf arbitrary)))+instance Arbitrary Func where+ arbitrary = F <$> choose (1, 1) <*> choose (1, 3)+instance Minimal Func where+ minimal = fun (F 0 1)+instance Ord.Sized Func where size (F _ n) = n+instance Ord.Weighted Func where argWeight _ = 1+instance Arity Func where+ arity (F 0 _) = 0+ arity (F 1 _) = 2+instance EqualsBonus Func++instance Arbitrary Var where arbitrary = fmap V (choose (0, 3))+instance (Labelled f, Ord f, Typeable f, Arbitrary f) => Arbitrary (Fun f) where+ arbitrary = fmap fun arbitrary++instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Term f) where+ arbitrary =+ sized $ \n ->+ oneof $+ [ build <$> var <$> arbitrary ] +++ [ do { f <- arbitrary; build <$> app f <$> vectorOf (arity f) (resize ((n-1) `div` arity f) arbitrary :: Gen (Term f)) } | n > 0 ]+ shrink (App f ts0) =+ ts ++ (build <$> app f <$> shrinkOne ts)+ where+ ts = unpack ts0+ shrinkOne [] = []+ shrinkOne (x:xs) =+ [ y:xs | y <- shrink x ] +++ [ x:ys | ys <- shrinkOne xs ]+ shrink _ = []++data Pair f = Pair (Term f) (Term f) deriving Show++instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Pair f) where+ arbitrary = liftM2 Pair arbitrary arbitrary+ shrink (Pair x y) =+ [ Pair x' y | x' <- shrink x ] +++ [ Pair x y' | y' <- shrink y ] +++ [ Pair x' y' | x' <- shrink x, y' <- shrink y ]++instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Equation f) where+ arbitrary = do+ Pair t u <- arbitrary+ return (t :=: u)+ shrink (t :=: u) = [t' :=: u' | Pair t' u' <- shrink (Pair t u)]++instance Ordered Func where+ lessIn = Ord.lessIn+ lessEq = Ord.lessEq+ lessEqSkolem = Ord.lessEqSkolem++instance Function f => Arbitrary (Model f) where+ arbitrary = fmap (modelFromOrder . map Variable . nub) arbitrary+ shrink = weakenModel++{-+prop_1 :: Model Func -> Pair Func -> Subst Func -> Property+prop_1 model (Pair t u) sub =+ counterexample ("Model: " ++ prettyShow model) $+ counterexample ("Subst: " ++ prettyShow sub) $+ conjoin $ do+ let cp = CriticalPair (t :=: u) 0 Nothing (axiom (Axiom 0 "dummy" (t :=: u)))+ r@(Rule _ t' u') <- map orient (map cp_eqn (split cp))+ return $+ counterexample ("LHS: " ++ prettyShow t') $+ counterexample ("RHS: " ++ prettyShow u') $+ counterexample ("Rule: " ++ prettyShow r) $+ counterexample ("Inst: " ++ prettyShow (Rule Oriented (subst sub t') (subst sub u'))) $+ counterexample ("Res: " ++ show (lessIn model (subst sub u') (subst sub t'))) $+ not (reducesInModel model r sub) || isJust (lessIn model (subst sub u') (subst sub t'))+-}++prop_2 :: Model Func -> Pair Func -> Bool+prop_2 model (Pair t u) =+ not (lessIn model t u == Just Strict && isJust (lessIn model u t))++prop_3 :: Pair Func -> Bool+prop_3 (Pair t u) =+ not (lessThan t u && lessEq u t)++prop_4 :: Pair Func -> Property+prop_4 (Pair t u) =+ t /= u ==> + not (lessEq t u && lessEq u t)++prop_5 :: Term Func -> Property+prop_5 t =+ lessEq t t .&&. not (lessThan t t)++prop_paths :: Term Func -> Property+prop_paths t =+ forAllShrink (choose (0, len t-1)) shrink $ \n ->+ counterexample (show (positionToPath t n)) $+ pathToPosition t (positionToPath t n) === n++prop_index :: [Term Func] -> Term Func -> Property+prop_index ts u =+ counterexample (show ts') $+ counterexample (show idx) $+ sort (catMaybes [fmap (,t) (match t u) | t <- ts']) ===+ sort (Index.matches u idx)+ where+ idx = foldr (\t -> Index.insert t t) Index.empty ts+ ts' = map canonicalise ts++newtype Terms f = Terms [Term f] deriving Show+instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (Terms f) where+ arbitrary = Terms <$> arbitrary+ shrink (Terms ts) =+ map Terms $+ filter (/= ts) $+ shrink ts ++ [canonicalise ts] ++ shrinkList (return . canonicalise) ts++newtype IndexOps f = IndexOps [IndexOp f] deriving Show+data IndexOp f = Add (Term f) | Delete (Term f) deriving Show++instance (Labelled f, Ord f, Typeable f, Arbitrary f, Arity f) => Arbitrary (IndexOps f) where+ arbitrary =+ sized $ \n -> IndexOps <$> take n <$> arbOps []+ where+ arbOps ts =+ frequency $+ [(2, do { t <- arbitrary; ops <- arbOps (t:ts); return (Add t:ops) })] +++ [(1, do { t <- elements ts; ops <- arbOps (delete t ts); return (Delete t:ops) }) | not (null ts)]+ shrink (IndexOps ops) =+ IndexOps <$> shrinkList shr ops+ where+ shr (Add t) = Add <$> shrink t+ shr (Delete t) = Delete <$> shrink t+++prop_index_invariant :: IndexOps Func -> Property+prop_index_invariant (IndexOps ops) =+ flip (foldr (counterexample . show)) idxs $+ property $ Index.invariant (last idxs)+ where+ idxs = scanl (\idx op -> applyIndex op idx) Index.empty ops+ applyIndex (Add t) = Index.insert t t+ applyIndex (Delete t) = Index.delete t t++deriving instance Eq Symbol+deriving instance Generic Symbol++instance Arbitrary Symbol where+ arbitrary =+ Symbol <$>+ arbitrary <*>+ fmap getLarge arbitrary <*>+ (fmap (fromIntegral . getLarge) (arbitrary :: Gen (Large Int32)) `suchThat` (> 0) `suchThat` (< 2^31))+ shrink s =+ filter ok (genericShrink s)+ where+ ok s = Twee.Term.Core.size s > 0++prop_symbol_1 :: Symbol -> Property+prop_symbol_1 s =+ withMaxSuccess 100000 $+ counterexample ("fun/index/size = " ++ show (isFun s, index s, Twee.Term.Core.size s)) $+ counterexample ("n = " ++ show (fromSymbol s)) $+ toSymbol (fromSymbol s) === twiddle s+ where+ twiddle s =+ s { index = fromIntegral (fromIntegral (index s) :: Int32) }++prop_symbol_2 :: Int64 -> Property+prop_symbol_2 n =+ withMaxSuccess 100000 $+ fromSymbol (toSymbol n) === n++prop_canonorder :: Equation Func -> Property+prop_canonorder eqn@(t :=: u) =+ let vs = usort (vars eqn) in+ forAll (shuffle vs) $ \ws swap (NonNegative n) ->+ let+ Just sub = listToSubst (zip vs [build (var (V (w + n))) | V w <- ws])+ eqn' = subst sub (if swap then u :=: t else t :=: u)+ in+ canonicalise (order eqn) === canonicalise (order eqn')++prop_canonorder2 :: Equation Func -> Equation Func -> Bool+prop_canonorder2 eqn1 eqn2 =+ eqn1 `simplerThan` eqn2 || eqn2 `simplerThan` eqn1 || order eqn1 == order eqn2++prop_canonorder3 :: Equation Func -> Property+prop_canonorder3 eq =+ let eq' = order eq in+ counterexample (show eq) $+ Ord.size (eqn_lhs eq') >= Ord.size (eqn_rhs eq')++return []+main = $forAllProperties (quickCheckWithResult stdArgs { maxSuccess = 1000000 })++--t :: Term Func+--t = build (app (fun (F 0)) [app (fun (F 1)) [var (V 0), var (V 1)], var (V 2)])
+ misc/print_trace.pl view
@@ -0,0 +1,50 @@+rules(Module, Rule, Used) :-+ %(Module:step(add(rule(_, Rule))); Module:step(add(rule(_, Rule, _, _)))),+ Module:step(add(rule(_, Rule, _, _))),+ (find_lemma(Module, Rule) -> Used=true; Used=false).++find_lemma(Module, Rule) :-+ copy_term(Rule, GroundRule), numbervars(GroundRule),+ clause(Module:lemma(GroundRule), true, Ref),+ clause(Module:lemma(Lemma), true, Ref),+ Rule =@= Lemma.++anywhere(Module, T) :-+ Module:goal(T); Module:axiom(T); rules(Module, T, _).++module_var(Module, X) :-+ anywhere(Module, T),+ term_variables(T, Xs),+ numbervars(Xs),+ member(X, Xs).++all_vars(Module, S) :-+ setof(X, module_var(Module, X), S).++module_func(Where, X/N) :-+ call(Where, T),+ sub_term(U, T),+ nonvar(U),+ functor(U, X, N),+ X \= '='.++module_func_with_count(Module, F, AxiomCount, GoalCount) :-+ module_func(anywhere(Module), F),+ once(setof(_, module_func(Module:axiom, F), S1); S1=[]),+ once(setof(_, module_func(Module:goal, F), S2); S2=[]),+ length(S1, AxiomCount),+ length(S2, GoalCount).++all_funcs(Module, S) :-+ setof(X/AxiomCount/GoalCount, module_func_with_count(Module, X, AxiomCount, GoalCount), S).++print_trace(Module) :-+ all_vars(Module, S),+ all_funcs(Module, T),+ writeln((vars, S)),+ writeln((funcs, T)),+ forall(Module:goal(Goal), (numbervars(Goal), writeln((goal, Goal)))),+ forall(Module:axiom(Axiom), (numbervars(Axiom), writeln((axiom, Axiom)))),+ forall(rules(Module, Rule, Used), (numbervars(Rule), writeln((Used, Rule)))).++init :- writeln(hello).
− misc/test.hs
@@ -1,161 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleInstances, FlexibleContexts, UndecidableInstances, StandaloneDeriving, ScopedTypeVariables, TupleSections, DeriveGeneric #-}-import Twee.Constraints-import Twee.Term hiding (subst, canonicalise, F)-import Twee.Term.Core hiding (F)-import Test.QuickCheck hiding (Function, Fun)-import Test.QuickCheck.All-import Twee.Pretty-import Twee.CP-import Twee.Proof-import qualified Twee.KBO as Ord-import Text.PrettyPrint-import Twee.Base hiding (F)-import Twee.Rule-import Twee.Equation-import Control.Monad-import qualified Data.Map as Map-import Data.Maybe-import Data.Ord-import Data.List-import Data.Typeable-import qualified Twee.Index as Index-import Data.Int-import GHC.Generics--newtype Func = F Int deriving (Eq, Ord, Show)--instance Pretty Func where pPrint (F f) = text "f" <> int f-instance PrettyTerm Func-instance Arbitrary (Subst Func) where- arbitrary = fmap fromJust (fmap listToSubst (liftM2 zip (fmap nub arbitrary) (infiniteListOf arbitrary)))-instance Arbitrary Func where- arbitrary = F <$> choose (1, 1)-instance Minimal Func where- minimal = fun (F 0)-instance Sized Func where size _ = 1-instance Arity Func where- arity (F 0) = 0- arity (F 1) = 2-instance Skolem Func-instance EqualsBonus Func--instance Arbitrary Var where arbitrary = fmap V (choose (0, 3))-instance (Ord f, Typeable f, Arbitrary f) => Arbitrary (Fun f) where- arbitrary = fmap fun arbitrary--instance (Ord f, Typeable f, Arbitrary f, Sized f, Arity f) => Arbitrary (Term f) where- arbitrary =- sized $ \n ->- oneof $- [ build <$> var <$> arbitrary ] ++- [ do { f <- arbitrary; build <$> app f <$> vectorOf (arity f) (resize ((n-1) `div` arity f) arbitrary :: Gen (Term f)) } | n > 0 ]- shrink (App f ts0) =- ts ++ (build <$> app f <$> shrinkOne ts)- where- ts = unpack ts0- shrinkOne [] = []- shrinkOne (x:xs) =- [ y:xs | y <- shrink x ] ++- [ x:ys | ys <- shrinkOne xs ]- shrink _ = []--data Pair f = Pair (Term f) (Term f) deriving Show--instance (Ord f, Typeable f, Arbitrary f, Arity f, Sized f) => Arbitrary (Pair f) where- arbitrary = liftM2 Pair arbitrary arbitrary- shrink (Pair x y) =- [ Pair x' y | x' <- shrink x ] ++- [ Pair x y' | y' <- shrink y ] ++- [ Pair x' y' | x' <- shrink x, y' <- shrink y ]--instance Ordered Func where- lessIn = Ord.lessIn- lessEq = Ord.lessEq--instance Function f => Arbitrary (Model f) where- arbitrary = fmap (modelFromOrder . map Variable . nub) arbitrary- shrink = weakenModel--prop_1 :: Model Func -> Pair Func -> Subst Func -> Property-prop_1 model (Pair t u) sub =- counterexample ("Model: " ++ prettyShow model) $- counterexample ("Subst: " ++ prettyShow sub) $- conjoin $ do- let cp = CriticalPair (t :=: u) 0 Nothing (axiom (Axiom 0 "dummy" (t :=: u)))- r@(Rule _ t' u') <- map orient (map cp_eqn (split cp))- return $- counterexample ("LHS: " ++ prettyShow t') $- counterexample ("RHS: " ++ prettyShow u') $- counterexample ("Rule: " ++ prettyShow r) $- counterexample ("Inst: " ++ prettyShow (Rule Oriented (subst sub t') (subst sub u'))) $- counterexample ("Res: " ++ show (lessIn model (subst sub u') (subst sub t'))) $- not (reducesInModel model r sub) || isJust (lessIn model (subst sub u') (subst sub t'))--prop_2 :: Model Func -> Pair Func -> Bool-prop_2 model (Pair t u) =- not (lessIn model t u == Just Strict && isJust (lessIn model u t))--prop_3 :: Pair Func -> Bool-prop_3 (Pair t u) =- not (lessThan t u && lessEq u t)--prop_4 :: Pair Func -> Property-prop_4 (Pair t u) =- t /= u ==> - not (lessEq t u && lessEq u t)--prop_5 :: Term Func -> Property-prop_5 t =- lessEq t t .&&. not (lessThan t t)--prop_paths :: Term Func -> Property-prop_paths t =- forAllShrink (choose (0, len t-1)) shrink $ \n ->- counterexample (show (positionToPath t n)) $- pathToPosition t (positionToPath t n) === n--deriving instance Ord f => Ord (Subst f)--prop_index :: [Term Func] -> Term Func -> Property-prop_index ts u =- counterexample (show ts) $- counterexample (show idx) $- sort (catMaybes [fmap (,t) (match t u) | t <- ts]) ===- sort (Index.matches u idx)- where- idx = foldr (\t -> Index.insert t t) Index.empty ts--deriving instance Eq Symbol-deriving instance Generic Symbol--instance Arbitrary Symbol where- arbitrary =- Symbol <$>- arbitrary <*>- fmap getLarge arbitrary <*>- (fmap (fromIntegral . getLarge) (arbitrary :: Gen (Large Int32)) `suchThat` (> 0) `suchThat` (< 2^31))- shrink s =- filter ok (genericShrink s)- where- ok s = Twee.Term.Core.size s > 0--prop_symbol_1 :: Symbol -> Property-prop_symbol_1 s =- withMaxSuccess 100000 $- counterexample ("fun/index/size = " ++ show (isFun s, index s, Twee.Term.Core.size s)) $- counterexample ("n = " ++ show (fromSymbol s)) $- toSymbol (fromSymbol s) === twiddle s- where- twiddle s =- s { index = fromIntegral (fromIntegral (index s) :: Int32) }--prop_symbol_2 :: Int64 -> Property-prop_symbol_2 n =- withMaxSuccess 100000 $- fromSymbol (toSymbol n) === n--return []-main = $forAllProperties (quickCheckWithResult stdArgs { maxSuccess = 1000000 })--t :: Term Func-t = build (app (fun (F 0)) [app (fun (F 1)) [var (V 0), var (V 1)], var (V 2)])
+ tests/GRP196-1.p view
@@ -0,0 +1,40 @@+%--------------------------------------------------------------------------+% File : GRP196-1 : TPTP v7.4.0. Released v2.2.0.+% Domain : Group Theory (Semigroups)+% Problem : In semigroups, xyyy=yyyx -> (uy)^9 = u^9v^9.+% Version : [MP96] (equality) axioms.+% English :++% Refs : [McC98] McCune (1998), Email to G. Sutcliffe+% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq+% : [McC95] McCune (1995), Four Challenge Problems in Equational L+% Source : [McC98]+% Names : CS-3 [MP96]+% : Problem B [McC95]++% Status : Unsatisfiable+% Rating : 0.88 v7.4.0, 0.91 v7.3.0, 0.89 v7.0.0, 0.95 v6.4.0, 1.00 v4.0.1, 0.93 v4.0.0, 0.92 v3.7.0, 0.89 v3.4.0, 1.00 v3.3.0, 0.93 v3.1.0, 1.00 v2.2.1+% Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 1 RR)+% Number of atoms : 3 ( 3 equality)+% Maximal clause size : 1 ( 1 average)+% Number of predicates : 1 ( 0 propositional; 2-2 arity)+% Number of functors : 3 ( 2 constant; 0-2 arity)+% Number of variables : 5 ( 0 singleton)+% Maximal term depth : 18 ( 8 average)+% SPC : CNF_UNS_RFO_PEQ_UEQ++% Comments : The problem was originally posed for cancellative semigroups,+% Otter does this with a nonstandard representation [MP96].+%--------------------------------------------------------------------------+%----Include semigroups axioms+include('Axioms/GRP008-0.ax').+%--------------------------------------------------------------------------+%----Hypothesis:+cnf(condition,hypothesis,+ ( '*'(X,'*'(Y,'*'(Y,Y))) = '*'(Y,'*'(Y,'*'(Y,X))) )).++%----Denial of conclusion:+cnf(prove_this,negated_conjecture,+ ( '*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,'*'(b,'*'(a,b))))))))))))))))) != '*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(a,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,'*'(b,b))))))))))))))))) )).++%--------------------------------------------------------------------------
+ tests/RNG025-buggy.p view
@@ -0,0 +1,9 @@+% SPASS solves this instantly, Twee takes ages!+cnf(axiom, axiom, multiply(U,add(V,W))=add(multiply(U,V),multiply(U,W))).+cnf(axiom, axiom, add(U,additive_inverse(add(additive_inverse(V),U)))=V).+cnf(axiom, axiom, add(U,additive_inverse(add(V,add(W,U))))=additive_inverse(add(V,W))).+cnf(axiom, axiom, add(additive_inverse(U),V)=additive_inverse(add(U,additive_inverse(V)))).+cnf(axiom, axiom, multiply(multiply(U,V),W)=add(associator(U,V,W),multiply(U,multiply(V,W)))).+cnf(axiom, axiom, additive_inverse(add(multiply(U,multiply(V,W)),add(multiply(U,multiply(X,W)),additive_inverse(add(multiply(multiply(U,V),W),multiply(multiply(U,X),W))))))=associator(U,add(V,X),W)).++cnf(conjecture, conjecture, add(associator(U,V,W),associator(U,X,W))=associator(U,add(V,X),W)).
− tests/append-rev-ascii.p
@@ -1,4 +0,0 @@-fof(rev_rev, axiom, ![X]: rev(rev(X))=X).-fof(app_assoc, axiom, ![X, Y, Z]: '++'(X, '++'(Y, Z))='++'('++'(X, Y), Z)).-fof(rev_app, axiom, ![X, Y]: '++'(rev(X), rev(Y))=rev('++'(Y, X))).-fof(conjecture, conjecture, '++'(a, rev(b))=rev('++'(b, rev(a)))).
− tests/blah.p
@@ -1,5 +0,0 @@-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(conjecture, negated_conjecture, '*'(a, b) != '*'(b, a)).
− tests/db.p
@@ -1,28 +0,0 @@-% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf-% appendix b. theorem 3.4, clause 8.-cnf(commutativity, axiom,- X ∧ Y = Y ∧ X).-cnf(associativity, axiom,- X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).-cnf(commutativity, axiom,- X ∨ Y = Y ∨ X).-cnf(associativity, axiom,- X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).-cnf(absorption, axiom,- X ∨ (X ∧ Y) = X).-cnf(absorption, axiom,- X ∧ (X ∨ Y) = X).-cnf('definition of upme', axiom,- upme(X,Y,Z) = X ∧ (Y ∨ Z)).-cnf('definition of lome', axiom,- lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).-%cnf('definition of upjo', axiom,-% upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).-%cnf('definition of lojo' axiom,-% lojo(X,Y,Z) = X ∨ (Y ∧ Z)).-cnf('upme property 1', axiom,- upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).-cnf('upme property 2', axiom,- upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).-fof(conjecture, conjecture,- upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)).
− tests/db2.p
@@ -1,29 +0,0 @@-% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf-% appendix b. theorem 3.4, clause 8.-cnf(commutativity, axiom,- X ∧ Y = Y ∧ X).-cnf(associativity, axiom,- X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).-cnf(commutativity, axiom,- X ∨ Y = Y ∨ X).-cnf(associativity, axiom,- X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).-cnf(absorption, axiom,- X ∨ (X ∧ Y) = X).-cnf(absorption, axiom,- X ∧ (X ∨ Y) = X).-cnf('definition of upme', axiom,- upme(X,Y,Z) = X ∧ (Y ∨ Z)).-cnf('definition of lome', axiom,- lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).-cnf('definition of upjo', axiom,- upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).-cnf('definition of lojo', axiom,- lojo(X,Y,Z) = X ∨ (Y ∧ Z)).-cnf('upme property 1', axiom,- ((a ∧ X1) ∧ (Y1 ∨ Z1)) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).-cnf('upme property 2', axiom,- X ∧ (Y ∨ Z) = (X ∧ (Y ∨ (a ∧ Z))) ∨ (X ∧ (Z ∨ (a ∧ Y)))).-fof(conjecture, conjecture,- a ∧ (x2 ∨ y2) = a ∧ (x2 ∨ z2) =>- x2 ∧ (y2 ∨ z2) = (x2 ∧ y2) ∨ (x2 ∧ z2)).
− tests/gmv1-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 1', conjecture, '@'(x, x)=x).
− tests/gmv1.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).--cnf('Goal 1', conjecture,- x @ x = x).- - -
− tests/gmv10-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 10', conjecture, '@'('\\'(x, '1'), '1')='1').
− tests/gmv10.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - -cnf('Goal 10', conjecture,- (x \ '1') @ '1' = '1').-
− tests/gmv11-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 11', conjecture, '@'('1', '\\'(x, '1'))='\\'(x, '1')).
− tests/gmv11.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - -cnf('Goal 11', conjecture,- '1' @ (x \ '1') = x \ '1').-
− tests/gmv12-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 12', conjecture, '@'('/'(x, '\\'(y, x)), 'or'(x, y))='or'(x, y)).
− tests/gmv12.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - - -cnf('Goal 12', conjecture,- (x / (y \ x)) @ (x ∨ y) = x ∨ y).
− tests/gmv13-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 13', conjecture, '@'('\\'('/'(x, y), x), 'or'(x, y))='or'(x, y)).
− tests/gmv13.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - - -cnf('Goal 13', conjecture,- ((x / y) \ x) @ (x ∨ y) = x ∨ y).
− tests/gmv14-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 14', conjecture, '@'('or'(x, y), '/'(x, '\\'(y, x)))='/'(x, '\\'(y, x))).
− tests/gmv14.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - - -cnf('Goal 14', conjecture,- (x ∨ y) @ (x / (y \ x)) = x / (y \ x)).
− tests/gmv15-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 15', conjecture, '@'('or'(x, y), '\\'('/'(x, y), x))='\\'('/'(x, y), x)).
− tests/gmv15.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - - -cnf('Goal 15', conjecture,- (x ∨ y) @ ((x / y) \ x) = (x / y) \ x).
− tests/gmv2-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 2', conjecture, '@'('@'(x, y), z)='@'(x, z)).
− tests/gmv2.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).--cnf('Goal 2', conjecture,- (x @ y) @ z = x @ z).- - -
− tests/gmv3-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 3', conjecture, '@'(x, '@'(y, z))='@'(x, z)).
− tests/gmv3.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).--cnf('Goal 3', conjecture,- x @ (y @ z) = x @ z).- - -
− tests/gmv4-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 4', conjecture, '@'('and'(x, y), 'and'(z, u))='and'('@'(x, z), '@'(y, u))).
− tests/gmv4.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- -cnf('Goal 4', conjecture,- (x ∧ y) @ (z ∧ u) = (x @ z) ∧ (y @ u)).- -
− tests/gmv5-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 5', conjecture, '@'('or'(x, y), 'or'(z, u))='or'('@'(x, z), '@'(y, u))).
− tests/gmv5.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- -cnf('Goal 5', conjecture,- (x ∨ y) @ (z ∨ u) = (x @ z) ∨ (y @ u)).- -
− tests/gmv6-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 6', conjecture, '@'('\\'(x, y), '\\'(z, u))='\\'('@'(x, z), '@'(y, u))).
− tests/gmv6.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- -cnf('Goal 6', conjecture,- (x \ y) @ (z \ u) = (x @ z) \ (y @ u)).- -
− tests/gmv7-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 7', conjecture, '@'('/'(x, y), '/'(z, u))='/'('@'(x, z), '@'(y, u))).
− tests/gmv7.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- -cnf('Goal 7', conjecture,- (x / y) @ (z / u) = (x @ z) / (y @ u)).- -
− tests/gmv8-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 8', conjecture, '@'('*'(x, '\\'(x, '1')), '1')='*'(x, '\\'(x, '1'))).
− tests/gmv8.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - -cnf('Goal 8', conjecture,- (x * (x \ '1')) @ '1' = x * (x \ '1')).-
− tests/gmv9-ascii.p
@@ -1,19 +0,0 @@-fof('Associativity-and', axiom, ![X, Y, Z]: 'and'('and'(X, Y), Z)='and'(X, 'and'(Y, Z))).-fof('Associativity-or', axiom, ![X, Y, Z]: 'or'('or'(X, Y), Z)='or'(X, 'or'(Y, Z))).-fof('Idempotence-and', axiom, ![X]: 'and'(X, X)=X).-fof('Idempotence-or', axiom, ![X]: 'or'(X, X)=X).-fof('Commutativity-and', axiom, ![X, Y]: 'and'(X, Y)='and'(Y, X)).-fof('Commutativity-or', axiom, ![X, Y]: 'or'(X, Y)='or'(Y, X)).-fof('Absorption a', axiom, ![X, Y]: 'or'('and'(X, Y), X)=X).-fof('Absorption b', axiom, ![X, Y]: 'and'('or'(X, Y), X)=X).-fof('Residual a', axiom, ![X, Y, Z]: 'or'('*'(X, 'and'('\\'(X, Z), Y)), Z)=Z).-fof('Residual b', axiom, ![X, Y, Z]: 'or'('*'('and'(Y, '/'(Z, X)), X), Z)=Z).-fof('Residual c', axiom, ![X, Y, Z]: 'and'('\\'(X, 'or'('*'(X, Y), Z)), Y)=Y).-fof('Residual d', axiom, ![X, Y, Z]: 'and'('/'('or'('*'(Y, X), Z), X), Y)=Y).-fof('Associativity-* (fusion)', axiom, ![X, Y, Z]: '*'('*'(X, Y), Z)='*'(X, '*'(Y, Z))).-fof('Left monoid unit', axiom, ![X]: '*'('1', X)=X).-fof('Right monoid unit', axiom, ![X]: '*'(X, '1')=X).-fof('GMV a', axiom, ![X, Y]: 'or'(X, Y)='/'(X, '\\'('or'(X, Y), X))).-fof('GMV b', axiom, ![X, Y]: 'or'(X, Y)='\\'('/'(X, 'or'(X, Y)), X)).-fof('Definition-@', axiom, ![X, Y]: '@'(X, Y)='*'('*'(X, '\\'(X, '1')), '\\'('\\'(Y, '1'), '1'))).-fof('Goal 9', conjecture, '@'('1', '*'(x, '\\'(x, '1')))='1').
− tests/gmv9.p
@@ -1,46 +0,0 @@-cnf('Associativity-∧', axiom,- (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)). -cnf('Associativity-∨', axiom,- (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).-cnf('Idempotence-∧', axiom,- X ∧ X = X).-cnf('Idempotence-∨', axiom,- X ∨ X = X).-cnf('Commutativity-∧', axiom,- X ∧ Y = Y ∧ X).-cnf('Commutativity-∨', axiom,- X ∨ Y = Y ∨ X).-cnf('Absorption a', axiom,- (X ∧ Y) ∨ X = X).-cnf('Absorption b', axiom,- (X ∨ Y) ∧ X = X).--cnf('Residual a', axiom,- (X * ((X \ Z) ∧ Y)) ∨ Z = Z).-cnf('Residual b', axiom,- ((Y ∧ (Z / X)) * X) ∨ Z = Z).-cnf('Residual c', axiom,- (X \ ((X * Y) ∨ Z)) ∧ Y = Y).-cnf('Residual d', axiom,- (((Y * X) ∨ Z) / X) ∧ Y = Y).--cnf('Associativity-* (fusion)', axiom,- (X * Y) * Z = X * (Y * Z)).-cnf('Left monoid unit', axiom,- '1' * X = X).-cnf('Right monoid unit', axiom,- X * '1' = X).--cnf('GMV a', axiom,- X ∨ Y = X / ((X ∨ Y) \ X)).-cnf('GMV b', axiom,- X ∨ Y = (X / (X ∨ Y)) \ X).--cnf('Definition-@', axiom,- X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).-- - -cnf('Goal 9', conjecture,- '1' @ (x * (x \ '1')) = '1').-
− tests/group_plain.p
@@ -1,14 +0,0 @@-cnf(associativity, axiom,- plus(X,plus(Y,Z))=plus(plus(X,Y),Z)).-cnf(plus_zero, axiom,- plus(zero, X) = X).-cnf(plus_zero, axiom,- plus(X, zero) = X).-cnf(minus_left, axiom,- plus(neg(X),X) = zero).-cnf(minus_right, axiom,- plus(X,neg(X)) = zero).-cnf(assumption, assumption,- plus(a, b) = a).-cnf(goal, conjecture,- b = zero).
− tests/loop-ascii.p
@@ -1,6 +0,0 @@-cnf(mult_ld, axiom, mult(X, back(X, Y)) = Y).-cnf(ld_mult, axiom, back(X, mult(X, Y)) = Y).-cnf(mult_rd, axiom, mult(slash(X, Y), Y) = X).-cnf(rd_mult, axiom, slash(mult(X, Y), Y) = X).-cnf(moufang, axiom, mult(X, mult(Y, mult(X, Z))) = mult(mult(mult(X, Y), X), Z)).-cnf(conjecture, conjecture, back(a, a) = slash(a, a)).
+ tests/rellat_appendixa.p view
@@ -0,0 +1,27 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% appendix a. theorem 3.4, clause 7.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).++fof(conjecture, conjecture,+ (![X1, Y1, W]:+ upme(a ∧ X1,Y1,W) ∨ (Y1 ∧ W) = (((a ∧ X1) ∧ Y1) ∨ W) ∧ (((a ∧ X1) ∧ W) ∨ Y1)) =>+ upme(a ∧ z1,z2,z3) = lome(a ∧ z1,z2,z3)).
+ tests/rellat_appendixb.p view
@@ -0,0 +1,28 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% appendix b. theorem 3.4, clause 8.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).+cnf(rh1, axiom,+ upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).+cnf(rh2, axiom,+ upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).+fof(conjecture, conjecture,+ upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)).
+ tests/rellat_appendixb_easier.p view
@@ -0,0 +1,30 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% appendix b. theorem 3.4, clause 8, assuming axiom rl1.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).+cnf(rh1, axiom,+ upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).+cnf(rh2, axiom,+ upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).+cnf(rl1, axiom,+ lome(X,Y,Z) = upme(X,upme(Y,X,Z),upme(Z,X,Y))).+fof(conjecture, conjecture,+ upme(a,x2,y2) = upme(a,x2,z2) => upme(x2,y2,z2) = lome(x2,y2,z2)).
+ tests/rellat_appendixc.p view
@@ -0,0 +1,30 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% appendix c. theorem 3.4, clause 9.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).+cnf(upme_property_1, axiom,+ upme(a ∧ X1,Y1,Z1) ∨ (Y1 ∧ Z1) = (((a ∧ X1) ∧ Y1) ∨ Z1) ∧ (((a ∧ X1) ∧ Z1) ∨ Y1)).+cnf(upme_property_2, axiom,+ upme(X,Y,Z) = upme(X,Y,a ∧ Z) ∨ upme(X,Z,a ∧ Y)).+fof(conjecture, conjecture,+ (upme(a,x2,y2) = upme(a,x2,z2) &+ upme(a,x2,y2) = upme(a,y2,z2)) =>+ upjo(x2,y2,z2) = lojo(x2,y2,z2)).
+ tests/rellat_theorem34_6.p view
@@ -0,0 +1,32 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% theorem 3.4, clause 6.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).+cnf(eq1, axiom,+ upme(a ∧ Z1,Z2,Z3) = lome(a ∧ Z1,Z2,Z3)).+cnf(qu2, axiom,+ upme(a,X2,Y2) = upme(a,X2,Z2) => upme(X2,Y2,Z2) = lome(X2,Y2,Z2)).+fof(rl1, conjecture,+ lome(x,y,z) =+ (x∧(y∧(x∨z)))∨(z∧(x∨y))).+%fof(rl2, conjecture,+% t∧(((x∨y)∧(x∨z))∨((u∨w)∧(u∨v))) =+% (t∧(((x∨y)∧(x∨z))∨(u∨(w∧v))))∨(t∧(((u∨w)∧(u∨v))∨(x∨(y∧z))))).
+ tests/rellat_theorem34_6a.p view
@@ -0,0 +1,29 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% theorem 3.4, clause 6.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).+cnf(eq1, axiom,+ upme(a ∧ Z1,Z2,Z3) = lome(a ∧ Z1,Z2,Z3)).+cnf(qu2, axiom,+ upme(a,X2,Y2) = upme(a,X2,Z2) => upme(X2,Y2,Z2) = lome(X2,Y2,Z2)).+fof(rl1, conjecture,+ lome(x,y,z) =+ x∧((y∧(x∨z))∨(z∧(x∨y)))).
+ tests/rellat_theorem34_6b.p view
@@ -0,0 +1,29 @@+% http://www.dcs.bbk.ac.uk/~szabolcs/rellat-jlamp-second-submission-2.pdf+% theorem 3.4, clause 6.+cnf(commutativity, axiom,+ X ∧ Y = Y ∧ X).+cnf(associativity, axiom,+ X ∧ (Y ∧ Z) = (X ∧ Y) ∧ Z).+cnf(commutativity, axiom,+ X ∨ Y = Y ∨ X).+cnf(associativity, axiom,+ X ∨ (Y ∨ Z) = (X ∨ Y) ∨ Z).+cnf(absorption, axiom,+ X ∨ (X ∧ Y) = X).+cnf(absorption, axiom,+ X ∧ (X ∨ Y) = X).+cnf(definition_of_upme, axiom,+ upme(X,Y,Z) = X ∧ (Y ∨ Z)).+cnf(definition_of_lome, axiom,+ lome(X,Y,Z) = (X ∧ Y) ∨ (X ∧ Z)).+cnf(definition_of_upjo, axiom,+ upjo(X,Y,Z) = (X ∨ Y) ∧ (X ∨ Z)).+cnf(definition_of_lojo, axiom,+ lojo(X,Y,Z) = X ∨ (Y ∧ Z)).+cnf(eq1, axiom,+ upme(a ∧ Z1,Z2,Z3) = lome(a ∧ Z1,Z2,Z3)).+cnf(qu2, axiom,+ upme(a,X2,Y2) = upme(a,X2,Z2) => upme(X2,Y2,Z2) = lome(X2,Y2,Z2)).+fof(rl2, conjecture,+ t∧(((x∨y)∧(x∨z))∨((u∨w)∧(u∨v))) =+ (t∧(((x∨y)∧(x∨z))∨(u∨(w∧v))))∨(t∧(((u∨w)∧(u∨v))∨(x∨(y∧z))))).
− tests/y-easy.p
@@ -1,3 +0,0 @@-fof(k_def, axiom, ![X, Y]: (k @ X) @ Y = X).-fof(s_def, axiom, ![X, Y, Z]: ((s @ X) @ Y) @ Z = (X @ Z) @ (Y @ Z)).-fof(conjecture, conjecture, ![F]: ?[X]: F @ X = X).
+ tests/y-encoded.p view
@@ -0,0 +1,5 @@+cnf(ifeq_axiom, axiom, ifeq(A, A, B, C)=B).+cnf(k_def, axiom, '@'('@'(k, X), Y)=X).+cnf(s_def, axiom, '@'('@'('@'(s, X), Y), Z)='@'('@'(X, Z), '@'(Y, Z))).+cnf(conjecture, negated_conjecture, ifeq('@'(Y, f(Y)), '@'(f(Y), '@'(Y, f(Y))), a, b)=b).+cnf(goal, negated_conjecture, a!=b).
twee.cabal view
@@ -1,5 +1,5 @@ name: twee-version: 2.3.1+version: 2.4 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -31,14 +31,17 @@ flag static description: Build a static binary. default: False+ manual: True flag static-cxx description: Build a binary which statically links against libstdc++. default: False+ manual: True -flag parallel- description: Build a special parallel version of Twee.- default: False+--flag parallel+-- description: Build a special parallel version of Twee.+-- default: False+-- manual: True executable twee -- if flag(parallel)@@ -52,11 +55,11 @@ other-modules: SequentialMain default-language: Haskell2010 build-depends: base < 5,- twee-lib == 2.3.1,+ twee-lib == 2.4, containers, pretty, split,- jukebox == 0.5.*,+ jukebox >= 0.5.4, ansi-terminal >= 0.9, symbol ghc-options: -W -fno-warn-incomplete-patterns