twee-2.3.1: tests/gmv2-ascii.p

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)).