twee 2.3 → 2.3.1

raw patch · 40 files changed

+1191/−64 lines, 40 filesdep ~twee-lib

Dependency ranges changed: twee-lib

Files

• executable/SequentialMain.hs +30/−31
• tests/ROB027-1-pretty.p +56/−0
• tests/ROB027-1.p +1/−1
• tests/append-rev-ascii.p +4/−0
• tests/append-rev.p +1/−1
• tests/factor.p +23/−29
• tests/gmv.p +74/−0
• tests/gmv1-ascii.p +19/−0
• tests/gmv1.p +46/−0
• tests/gmv10-ascii.p +19/−0
• tests/gmv10.p +46/−0
• tests/gmv11-ascii.p +19/−0
• tests/gmv11.p +46/−0
• tests/gmv12-ascii.p +19/−0
• tests/gmv12.p +46/−0
• tests/gmv13-ascii.p +19/−0
• tests/gmv13.p +46/−0
• tests/gmv14-ascii.p +19/−0
• tests/gmv14.p +46/−0
• tests/gmv15-ascii.p +19/−0
• tests/gmv15.p +46/−0
• tests/gmv2-ascii.p +19/−0
• tests/gmv2.p +46/−0
• tests/gmv3-ascii.p +19/−0
• tests/gmv3.p +46/−0
• tests/gmv4-ascii.p +19/−0
• tests/gmv4.p +46/−0
• tests/gmv5-ascii.p +19/−0
• tests/gmv5.p +46/−0
• tests/gmv6-ascii.p +19/−0
• tests/gmv6.p +46/−0
• tests/gmv7-ascii.p +19/−0
• tests/gmv7.p +46/−0
• tests/gmv8-ascii.p +19/−0
• tests/gmv8.p +46/−0
• tests/gmv9-ascii.p +19/−0
• tests/gmv9.p +46/−0
• tests/group_plain.p +14/−0
• tests/veroff-short.p +11/−0
• twee.cabal +2/−2

@@ -1,4 +1,4 @@-{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards #-}+{-# LANGUAGE CPP, RecordWildCards, FlexibleInstances, PatternGuards, DerivingVia #-} {-# OPTIONS_GHC -flate-specialise #-} module SequentialMain(main) where @@ -24,7 +24,7 @@ import Jukebox.Toolbox import Jukebox.Name hiding (lhs, rhs, label) import qualified Jukebox.Form as Jukebox-import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size)+import Jukebox.Form hiding ((:=:), Var, Symbolic(..), Term, Axiom, size, Subst, subst) import Jukebox.Tools.EncodeTypes import Jukebox.TPTP.Print import Jukebox.Tools.HornToUnit@@ -283,14 +283,11 @@     con_weight :: !Integer,     con_bonus  :: !Bool }   deriving (Eq, Ord)+  deriving Labelled via AutoLabel Constant  data Precedence = Precedence !Bool !Bool !(Maybe Int) !Int   deriving (Eq, Ord) -instance Labelled Constant where-  label = fromIntegral . Label.labelNum . Label.label-  find = Label.find . Label.unsafeMkLabel . fromIntegral- instance KBO.Sized Constant where   size Minimal = 1   size Constant{..} = con_size@@ -351,9 +348,8 @@ tweeConstant :: HornFlags -> TweeContext -> Precedence -> Jukebox.Function -> Constant tweeConstant flags TweeContext{..} prec fun   | fun == ctx_minimal = Minimal-  | otherwise = Constant prec fun (Jukebox.arity fun) (sz fun) 1 (bonus fun)+  | otherwise = Constant prec fun (Jukebox.arity fun) 1 1 (bonus fun)   where-    sz fun = {-if isType fun then 0 else-} 1     bonus fun =       (isIfeq fun && encoding flags /= Asymmetric2) ||       SequentialMain.isEquals fun@@ -549,7 +545,7 @@       | otherwise = x     prob = prettyNames (mapName lowercaseSkolem (addNarrowing ctx obligs')) -  (axioms0, goals0) <-+  (unsortedAxioms0, goals0) <-     case identifyProblem ctx prob of       Left inp -> do         mapM_ (hPutStrLn stderr) [@@ -574,25 +570,27 @@     toEquation (t, u) =       canonicalise (tweeTerm horn ctx prec t :=: tweeTerm horn ctx prec u) +    axiomCompare ax1 ax2+      | ax1' `simplerThan` ax2' = LT+      | ax2' `simplerThan` ax1' = GT+      | otherwise = EQ+      where+        ax1' = toEquation (pre_eqn ax1)+        ax2' = toEquation (pre_eqn ax2)+    axioms0 = sortBy axiomCompare unsortedAxioms0+     goals =       [ goal n pre_name (toEquation pre_eqn)       | (n, PreEquation{..}) <- zip [1..] goals0 ]     axioms =       [ Axiom n pre_name (toEquation pre_eqn)-      | (n, PreEquation{..}) <- zip [1..] (sortBy axiomCompare axioms0) ]+      | (n, PreEquation{..}) <- zip [1..] axioms0 ]     defs =       [ axiom-      | (axiom, PreEquation{..}) <- zip axioms (sortBy axiomCompare axioms0),+      | (axiom, PreEquation{..}) <- zip axioms axioms0,         isDefinition pre_form ]     isDefinition Input{source = Unknown} = True     isDefinition inp = tag inp `elem` flags_eliminate-    axiomCompare ax1 ax2-      | ax1' `simplerThan` ax2' = LT-      | ax2' `simplerThan` ax1' = GT-      | otherwise = EQ-      where-        ax1' = toEquation (pre_eqn ax1)-        ax2' = toEquation (pre_eqn ax2)      withGoals = foldl' (addGoal config) (initialState config) goals     withAxioms = foldl' (addAxiom config) withGoals axioms@@ -827,28 +825,29 @@     tstp = deriv . derivation      deriv :: Derivation Constant -> Input Form-    deriv p@(Trans q r) = derivFrom (deriv r:sources q) p-    deriv p = derivFrom (sources p) p--    derivFrom :: [Input Form] -> Derivation Constant -> Input Form-    derivFrom sources p =+    deriv p =       Input {         tag = "step",         kind = Jukebox.Ax Jukebox.Axiom,         what = jukeboxEquation (equation (certify p)),         source =-          Inference "rw" "thm" sources }+          Inference name "thm" sources }+      where+        (name, sources) = unpack p +    unpack :: Derivation Constant -> (String, [Input Form])+    unpack (Refl _) = ("reflexivity", [])+    unpack (Symm p) = ("symmetry", [deriv p])+    unpack (Trans p q) = ("transitivity", [deriv p, deriv q])+    unpack (Cong _ ps) = ("congruence", [deriv p | p <- ps, let t :=: u = equation (certify p), t /= u])+    unpack (UseAxiom Axiom{..} _) =+      ("substitution", [fromJust (Map.lookup axiom_number axiom_proofs)])+    unpack (UseLemma lemma _) =+      ("substitution", [fromJust (Map.lookup lemma lemma_proofs)])+     jukeboxEquation :: Equation Constant -> Form     jukeboxEquation (t :=: u) =       toForm $ clause [Pos (jukeboxTerm ctx t Jukebox.:=: jukeboxTerm ctx u)]--    sources :: Derivation Constant -> [Input Form]-    sources p =-      [ fromJust (Map.lookup lemma lemma_proofs)-      | lemma <- usort (usedLemmas p) ] ++-      [ fromJust (Map.lookup axiom_number axiom_proofs)-      | Axiom{..} <- usort (usedAxioms p) ]      -- An ugly hack: since Twee.Proof decodes $true = $false into a     -- proof of the existentially quantified goal, we need to do the

@@ -0,0 +1,56 @@+%--------------------------------------------------------------------------+% 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,+    ( '+'(X,Y) = '+'(Y,X) )).++cnf(associativity_of_add,axiom,+    ( '+'('+'(X,Y),Z) = '+'(X,'+'(Y,Z)) )).++cnf(robbins_axiom,axiom,+    ( '-'('+'('-'('+'(X,Y)),'-'('+'(X,'-'(Y))))) = X )).++%--------------------------------------------------------------------------+%--------------------------------------------------------------------------+cnf(double_negation,hypothesis,+    ( '-'('-'(c)) = c )).++cnf(prove_huntingtons_axiom,negated_conjecture,+    '+'('-'('+'(a,'-'(b))),'-'('+'('-'(a),'-'(b)))) != b).++%--------------------------------------------------------------------------+%----Definition of g+cnf(sos04,axiom,(+    g(A) = '-'('+'(A,'-'(A))) )).++%----Definition of h+cnf(sos05,axiom,(+    h(A) = '+'(A,'+'(A,'+'(A,'-'('+'(A,'-'(A)))))))).

@@ -53,4 +53,4 @@  %----Definition of h cnf(sos05,axiom,(-    h(A) = add(A,add(A,add(A,g(A)))) )).+    h(A) = add(A,add(A,add(A,negate(add(A,negate(A)))))))).

@@ -0,0 +1,4 @@+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)))).

@@ -1,4 +1,4 @@ cnf(rev_rev, axiom, rev(rev(X)) = X). cnf(app_assoc, axiom, X ++ (Y ++ Z) = (X ++ Y) ++ Z). cnf(rev_app, axiom, rev(X) ++ rev(Y) = rev(Y ++ X)).-cnf(conjecture, conjecture, a ++ rev(b) = rev(b ++ rev(a))).+fof(conjecture, conjecture, ![A,B]: A ++ rev(B) = rev(B ++ rev(A))).

@@ -1,50 +1,44 @@ % Axioms about arithmetic. -cnf('commutativity of +', axiom,+cnf('commutativity_of_plus', axiom,     X + Y = Y + X).-cnf('associativity of +', axiom,+cnf('associativity_of_plus', axiom,     X + (Y + Z) = (X + Y) + Z).-cnf('commutativity of *', axiom,+cnf('commutativity_of_times', axiom,     X * Y = Y * X).-cnf('associativity of *', axiom,+cnf('associativity_of_times', axiom,     X * (Y * Z) = (X * Y) * Z).-cnf('plus 0', axiom,+cnf('plus_zero', axiom,     '0' + X = X).-cnf('times 0', axiom,+cnf('times_zero', axiom,     '0' * X = '0').-cnf('times 1', axiom,+cnf('times_one', axiom,     '1' * X = X). cnf('distributivity', axiom,     X * (Y + Z) = (X * Y) + (X * Z)). cnf('minus', axiom,     X + -X = '0'). -tff(square, type, '_²' : $i > $i).-tff(cube, type, '_³' : $i > $i).-cnf(square, axiom, X² = X*X).-cnf(cube, axiom, X³ = X*(X*X)).-%cnf(two, axiom, two = '1'+'1').-%cnf(three, axiom, three = '1'+two).-%cnf(four, axiom, four = '1'+three).-%cnf(five, axiom, five = '1'+four).-%cnf(six, axiom, six = '1'+five).-%cnf(seven, axiom, seven = '1'+six).-%cnf(eight, axiom, eight = '1'+seven).-%cnf(nine, axiom, nine = '1'+eight).-%cnf(minus_six, axiom, minus_four = -four).-%cnf(minus_six, axiom, minus_six = -six).--%fof(factoring, conjecture,-%    ?[A,B,C]: ![X]:-%      X³ + ((minus_six*(X²)) + ((nine*X) + minus_four)) = ((X +-%      -'1')*((X + -'1') * (X + -four)))).+cnf(two, axiom, two = '1'+'1').+cnf(three, axiom, three = '1'+two).+cnf(four, axiom, four = '1'+three).+cnf(five, axiom, five = '1'+four).+cnf(six, axiom, six = '1'+five).+cnf(seven, axiom, seven = '1'+six).+cnf(eight, axiom, eight = '1'+seven).+cnf(nine, axiom, nine = '1'+eight).+cnf(minus_six, axiom, minus_four = -four).+cnf(minus_six, axiom, minus_six = -six). -%cnf(a, conjecture, (-x)*y = -(y*x)).+fof(factoring, conjecture,+    ?[A,B,C]: ![X]:+      (X*(X*X)) + ((minus_six*(X*X)) + ((nine*X) + minus_four)) = ((X ++      -'1')*((X + -'1') * (X + -four)))).  fof(factoring, conjecture,     ?[A,B,C]: ![X]:-    X³ +-    (-(('1'+('1'+('1'+('1'+('1'+'1')))))*(X²)) ++    (X*(X*X)) ++    (-(('1'+('1'+('1'+('1'+('1'+'1')))))*(X*X)) +      ((('1'+('1'+('1'+('1'+('1'+('1'+('1'+('1'+'1'))))))))*X) +      -('1'+('1'+('1'+'1'))))) =     (X + -A)*((X + -B)*(X + -C))).

@@ -0,0 +1,74 @@+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).+cnf('Goal 2', conjecture,+    (x @ y) @ z = x @ z).+cnf('Goal 3', conjecture,+    x @ (y @ z) = x @ z).+  +cnf('Goal 4', conjecture,+    (x ∧ y) @ (z ∧ u) = (x @ z) ∧ (y @ u)).+cnf('Goal 5', conjecture,+    (x ∨ y) @ (z ∨ u) = (x @ z) ∨ (y @ u)).+cnf('Goal 6', conjecture,+    (x \ y) @ (z \ u) = (x @ z) \ (y @ u)).+cnf('Goal 7', conjecture,+    (x / y) @ (z / u) = (x @ z) / (y @ u)).+  +cnf('Goal 8', conjecture,+    (x * (x \ '1')) @ '1' = x * (x \ '1')).+cnf('Goal 9', conjecture,+    '1' @ (x * (x \ '1')) = '1').+cnf('Goal 10', conjecture,+    (x \ '1') @ '1' = '1').+cnf('Goal 11', conjecture,+    '1' @ (x \ '1') = x \ '1').+  +cnf('Goal 12', conjecture,+    (x / (y \ x)) @ (x ∨ y) = x ∨ y).+cnf('Goal 13', conjecture,+    ((x / y) \ x) @ (x ∨ y) = x ∨ y).+cnf('Goal 14', conjecture,+    (x ∨ y) @ (x / (y \ x)) = x / (y \ x)).+cnf('Goal 15', conjecture,+    (x ∨ y) @ ((x / y) \ x) = (x / y) \ x).

@@ -0,0 +1,19 @@+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).

@@ -0,0 +1,46 @@+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).+  +  +  

@@ -0,0 +1,19 @@+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').

@@ -0,0 +1,46 @@+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').+  

@@ -0,0 +1,19 @@+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')).

@@ -0,0 +1,46 @@+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').+  

@@ -0,0 +1,19 @@+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)).

@@ -0,0 +1,46 @@+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).

@@ -0,0 +1,19 @@+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)).

@@ -0,0 +1,46 @@+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).

@@ -0,0 +1,19 @@+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))).

@@ -0,0 +1,46 @@+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)).

@@ -0,0 +1,19 @@+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)).

@@ -0,0 +1,46 @@+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).

@@ -0,0 +1,19 @@+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)).

@@ -0,0 +1,46 @@+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).+  +  +  

@@ -0,0 +1,19 @@+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)).

@@ -0,0 +1,46 @@+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).+  +  +  

@@ -0,0 +1,19 @@+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))).

@@ -0,0 +1,46 @@+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)).+  +  

@@ -0,0 +1,19 @@+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))).

@@ -0,0 +1,46 @@+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)).+  +  

@@ -0,0 +1,19 @@+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))).

@@ -0,0 +1,46 @@+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)).+  +  

@@ -0,0 +1,19 @@+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))).

@@ -0,0 +1,46 @@+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)).+  +  

@@ -0,0 +1,19 @@+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'))).

@@ -0,0 +1,46 @@+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')).+  

@@ -0,0 +1,19 @@+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').

@@ -0,0 +1,46 @@+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').+  

@@ -0,0 +1,14 @@+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).

@@ -0,0 +1,11 @@+cnf(majority, axiom,+    f(X,X,Y) = X).+cnf('2a', axiom,+    f(X,Y,Z) = f(Z,X,Y)).+cnf('2b', axiom,+    f(X,Y,Z) = f(X,Z,Y)).+cnf(associativity, axiom,+    f(f(X,W,Y),W,Z) = f(X,W,f(Y,W,Z))).++cnf(dist_long, conjecture,+    f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w))).

@@ -1,5 +1,5 @@ name:                twee-version:             2.3+version:             2.3.1 synopsis:            An equational theorem prover homepage:            http://github.com/nick8325/twee license:             BSD3@@ -52,7 +52,7 @@   other-modules:       SequentialMain   default-language:    Haskell2010   build-depends:       base < 5,-                       twee-lib == 2.3,+                       twee-lib == 2.3.1,                        containers,                        pretty,                        split,