diff --git a/executable/SequentialMain.hs b/executable/SequentialMain.hs
--- 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.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
diff --git a/tests/ROB027-1-pretty.p b/tests/ROB027-1-pretty.p
new file mode 100644
--- /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
--- a/tests/ROB027-1.p
+++ b/tests/ROB027-1.p
@@ -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)))))))).
diff --git a/tests/append-rev-ascii.p b/tests/append-rev-ascii.p
new file mode 100644
--- /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
--- 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
--- 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).
-
-%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))).
diff --git a/tests/gmv.p b/tests/gmv.p
new file mode 100644
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- 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 @@
   other-modules:       SequentialMain
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.3,
+                       twee-lib == 2.3.1,
                        containers,
                        pretty,
                        split,