summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNickSmallbone <>2021-04-07 14:51:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2021-04-07 14:51:00 (GMT)
commit645622117e2ffbe4ac7649efb84fa1d5bef68d99 (patch)
treea7b28a9409dfb4c36178be1cf3d4cc32831af2f1
parentc42f93101a73db02cc601001eb82ad795d268bfb (diff)
version 2.3.1HEAD2.3.1master
-rw-r--r--executable/SequentialMain.hs61
-rw-r--r--tests/ROB027-1-pretty.p56
-rw-r--r--tests/ROB027-1.p2
-rw-r--r--tests/append-rev-ascii.p4
-rw-r--r--tests/append-rev.p2
-rw-r--r--tests/factor.p52
-rw-r--r--tests/gmv.p74
-rw-r--r--tests/gmv1-ascii.p19
-rw-r--r--tests/gmv1.p46
-rw-r--r--tests/gmv10-ascii.p19
-rw-r--r--tests/gmv10.p46
-rw-r--r--tests/gmv11-ascii.p19
-rw-r--r--tests/gmv11.p46
-rw-r--r--tests/gmv12-ascii.p19
-rw-r--r--tests/gmv12.p46
-rw-r--r--tests/gmv13-ascii.p19
-rw-r--r--tests/gmv13.p46
-rw-r--r--tests/gmv14-ascii.p19
-rw-r--r--tests/gmv14.p46
-rw-r--r--tests/gmv15-ascii.p19
-rw-r--r--tests/gmv15.p46
-rw-r--r--tests/gmv2-ascii.p19
-rw-r--r--tests/gmv2.p46
-rw-r--r--tests/gmv3-ascii.p19
-rw-r--r--tests/gmv3.p46
-rw-r--r--tests/gmv4-ascii.p19
-rw-r--r--tests/gmv4.p46
-rw-r--r--tests/gmv5-ascii.p19
-rw-r--r--tests/gmv5.p46
-rw-r--r--tests/gmv6-ascii.p19
-rw-r--r--tests/gmv6.p46
-rw-r--r--tests/gmv7-ascii.p19
-rw-r--r--tests/gmv7.p46
-rw-r--r--tests/gmv8-ascii.p19
-rw-r--r--tests/gmv8.p46
-rw-r--r--tests/gmv9-ascii.p19
-rw-r--r--tests/gmv9.p46
-rw-r--r--tests/group_plain.p14
-rw-r--r--tests/veroff-short.p11
-rw-r--r--twee.cabal4
40 files changed, 1191 insertions, 64 deletions
diff --git a/executable/SequentialMain.hs b/executable/SequentialMain.hs
index dae2da5..8128825 100644
--- a/executable/SequentialMain.hs
+++ b/executable/SequentialMain.hs
@@ -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.Options
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 @@ data Constant =
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 @@ data TweeContext =
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 @@ runTwee globals (TSTPFlags tstp) horn precedence config MainFlags{..} later obli
| 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 @@ runTwee globals (TSTPFlags tstp) horn precedence config MainFlags{..} later obli
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,29 +825,30 @@ presentToJukebox ctx toEquation axioms goals Presentation{..} =
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
-- same decoding at the Jukebox level.
diff --git a/tests/ROB027-1-pretty.p b/tests/ROB027-1-pretty.p
new file mode 100644
index 0000000..9e3f315
--- /dev/null
+++ b/tests/ROB027-1-pretty.p
@@ -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)))))))).
diff --git a/tests/ROB027-1.p b/tests/ROB027-1.p
index 835fa1f..4f8575a 100644
--- a/tests/ROB027-1.p
+++ b/tests/ROB027-1.p
@@ -53,4 +53,4 @@ cnf(sos04,axiom,(
%----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)))))))).
diff --git a/tests/append-rev-ascii.p b/tests/append-rev-ascii.p
new file mode 100644
index 0000000..2a46154
--- /dev/null
+++ b/tests/append-rev-ascii.p
@@ -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)))).
diff --git a/tests/append-rev.p b/tests/append-rev.p
index a3ba312..d7d4b2b 100644
--- a/tests/append-rev.p
+++ b/tests/append-rev.p
@@ -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))).
diff --git a/tests/factor.p b/tests/factor.p
index 0989c34..54d1ab3 100644
--- a/tests/factor.p
+++ b/tests/factor.p
@@ -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).
+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(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))).
diff --git a/tests/gmv.p b/tests/gmv.p
new file mode 100644
index 0000000..9352ed9
--- /dev/null
+++ b/tests/gmv.p
@@ -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).
diff --git a/tests/gmv1-ascii.p b/tests/gmv1-ascii.p
new file mode 100644
index 0000000..b20ff25
--- /dev/null
+++ b/tests/gmv1-ascii.p
@@ -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).
diff --git a/tests/gmv1.p b/tests/gmv1.p
new file mode 100644
index 0000000..f55a359
--- /dev/null
+++ b/tests/gmv1.p
@@ -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).
+
+
+
diff --git a/tests/gmv10-ascii.p b/tests/gmv10-ascii.p
new file mode 100644
index 0000000..b474a1a
--- /dev/null
+++ b/tests/gmv10-ascii.p
@@ -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').
diff --git a/tests/gmv10.p b/tests/gmv10.p
new file mode 100644
index 0000000..d2a6055
--- /dev/null
+++ b/tests/gmv10.p
@@ -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').
+
diff --git a/tests/gmv11-ascii.p b/tests/gmv11-ascii.p
new file mode 100644
index 0000000..bf863ef
--- /dev/null
+++ b/tests/gmv11-ascii.p
@@ -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')).
diff --git a/tests/gmv11.p b/tests/gmv11.p
new file mode 100644
index 0000000..0ce5d4f
--- /dev/null
+++ b/tests/gmv11.p
@@ -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').
+
diff --git a/tests/gmv12-ascii.p b/tests/gmv12-ascii.p
new file mode 100644
index 0000000..97b0f58
--- /dev/null
+++ b/tests/gmv12-ascii.p
@@ -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)).
diff --git a/tests/gmv12.p b/tests/gmv12.p
new file mode 100644
index 0000000..ae2ddc8
--- /dev/null
+++ b/tests/gmv12.p
@@ -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).
diff --git a/tests/gmv13-ascii.p b/tests/gmv13-ascii.p
new file mode 100644
index 0000000..aaf5a6e
--- /dev/null
+++ b/tests/gmv13-ascii.p
@@ -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)).
diff --git a/tests/gmv13.p b/tests/gmv13.p
new file mode 100644
index 0000000..7218c8e
--- /dev/null
+++ b/tests/gmv13.p
@@ -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).
diff --git a/tests/gmv14-ascii.p b/tests/gmv14-ascii.p
new file mode 100644
index 0000000..5037673
--- /dev/null
+++ b/tests/gmv14-ascii.p
@@ -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))).
diff --git a/tests/gmv14.p b/tests/gmv14.p
new file mode 100644
index 0000000..42fefe6
--- /dev/null
+++ b/tests/gmv14.p
@@ -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)).
diff --git a/tests/gmv15-ascii.p b/tests/gmv15-ascii.p
new file mode 100644
index 0000000..13bc44d
--- /dev/null
+++ b/tests/gmv15-ascii.p
@@ -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)).
diff --git a/tests/gmv15.p b/tests/gmv15.p
new file mode 100644
index 0000000..24db2f1
--- /dev/null
+++ b/tests/gmv15.p
@@ -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).
diff --git a/tests/gmv2-ascii.p b/tests/gmv2-ascii.p
new file mode 100644
index 0000000..efcc9f3
--- /dev/null
+++ b/tests/gmv2-ascii.p
@@ -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)).
diff --git a/tests/gmv2.p b/tests/gmv2.p
new file mode 100644
index 0000000..7f817a6
--- /dev/null
+++ b/tests/gmv2.p
@@ -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).
+
+
+
diff --git a/tests/gmv3-ascii.p b/tests/gmv3-ascii.p
new file mode 100644
index 0000000..0e27084
--- /dev/null
+++ b/tests/gmv3-ascii.p
@@ -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)).
diff --git a/tests/gmv3.p b/tests/gmv3.p
new file mode 100644
index 0000000..fbe1757
--- /dev/null
+++ b/tests/gmv3.p
@@ -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).
+
+
+
diff --git a/tests/gmv4-ascii.p b/tests/gmv4-ascii.p
new file mode 100644
index 0000000..fd5555f
--- /dev/null
+++ b/tests/gmv4-ascii.p
@@ -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))).
diff --git a/tests/gmv4.p b/tests/gmv4.p
new file mode 100644
index 0000000..0c17289
--- /dev/null
+++ b/tests/gmv4.p
@@ -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)).
+
+
diff --git a/tests/gmv5-ascii.p b/tests/gmv5-ascii.p
new file mode 100644
index 0000000..eb80332
--- /dev/null
+++ b/tests/gmv5-ascii.p
@@ -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))).
diff --git a/tests/gmv5.p b/tests/gmv5.p
new file mode 100644
index 0000000..eb5c4bb
--- /dev/null
+++ b/tests/gmv5.p
@@ -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)).
+
+
diff --git a/tests/gmv6-ascii.p b/tests/gmv6-ascii.p
new file mode 100644
index 0000000..0b42fd9
--- /dev/null
+++ b/tests/gmv6-ascii.p
@@ -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))).
diff --git a/tests/gmv6.p b/tests/gmv6.p
new file mode 100644
index 0000000..69416aa
--- /dev/null
+++ b/tests/gmv6.p
@@ -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)).
+
+
diff --git a/tests/gmv7-ascii.p b/tests/gmv7-ascii.p
new file mode 100644
index 0000000..fd2dc98
--- /dev/null
+++ b/tests/gmv7-ascii.p
@@ -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))).
diff --git a/tests/gmv7.p b/tests/gmv7.p
new file mode 100644
index 0000000..7c1d8af
--- /dev/null
+++ b/tests/gmv7.p
@@ -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)).
+
+
diff --git a/tests/gmv8-ascii.p b/tests/gmv8-ascii.p
new file mode 100644
index 0000000..4dd769b
--- /dev/null
+++ b/tests/gmv8-ascii.p
@@ -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'))).
diff --git a/tests/gmv8.p b/tests/gmv8.p
new file mode 100644
index 0000000..2759448
--- /dev/null
+++ b/tests/gmv8.p
@@ -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')).
+
diff --git a/tests/gmv9-ascii.p b/tests/gmv9-ascii.p
new file mode 100644
index 0000000..1af0cc7
--- /dev/null
+++ b/tests/gmv9-ascii.p
@@ -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').
diff --git a/tests/gmv9.p b/tests/gmv9.p
new file mode 100644
index 0000000..edfa234
--- /dev/null
+++ b/tests/gmv9.p
@@ -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').
+
diff --git a/tests/group_plain.p b/tests/group_plain.p
new file mode 100644
index 0000000..f48264e
--- /dev/null
+++ b/tests/group_plain.p
@@ -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).
diff --git a/tests/veroff-short.p b/tests/veroff-short.p
new file mode 100644
index 0000000..8c0b66a
--- /dev/null
+++ b/tests/veroff-short.p
@@ -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))).
diff --git a/twee.cabal b/twee.cabal
index 140e4b4..1dfa66a 100644
--- a/twee.cabal
+++ b/twee.cabal
@@ -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 @@ executable twee
other-modules: SequentialMain
default-language: Haskell2010
build-depends: base < 5,
- twee-lib == 2.3,
+ twee-lib == 2.3.1,
containers,
pretty,
split,