%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:14:40 AM UTC 2026
% Result : Unsatisfiable 18.38s 6.21s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 4
% Syntax : Number of formulae : 306 ( 306 unt; 2 def)
% Number of atoms : 306 ( 305 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 564 ( 564 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(X5)),inverse(X3))))))),X5) = X4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(a,b) != multiply(b,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_4) ).
fof(f3,definition,
sF0 = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f4,plain,
multiply(a,b) = sF0,
inference(reorient_equations,[],[f3]) ).
fof(f5,definition,
sF1 = multiply(b,a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f6,plain,
multiply(b,a) = sF1,
inference(reorient_equations,[],[f5]) ).
fof(f7,plain,
sF0 != sF1,
inference(definition_folding,[],[f2,f6,f4]) ).
fof(f11,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(a,b)),sF1)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(superposition,[],[f1,f6]) ).
fof(f12,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(b,a)),sF0)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(superposition,[],[f1,f4]) ).
fof(f17,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X8)),multiply(X7,inverse(multiply(multiply(X0,inverse(inverse(X9))),inverse(X8))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))),X9),
inference(superposition,[],[f1,f1]) ).
fof(f19,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(forward_demodulation,[],[f12,f6]) ).
fof(f20,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(forward_demodulation,[],[f11,f4]) ).
fof(f37,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(X1)),inverse(b))))))),X1) = X0,
inference(superposition,[],[f20,f4]) ).
fof(f70,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X5)),multiply(X5,X4))),multiply(inverse(multiply(X6,X7)),multiply(X6,inverse(multiply(X2,inverse(X7))))))),X3) = inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X2,inverse(inverse(X3))),inverse(b))))))),
inference(superposition,[],[f17,f4]) ).
fof(f137,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(multiply(X4,inverse(X5)),inverse(inverse(X5))),inverse(X3))))))) = X4,
inference(superposition,[],[f1,f17]) ).
fof(f185,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(X5,X0),inverse(X0)),inverse(X4))))))) = X5,
inference(superposition,[],[f137,f137]) ).
fof(f219,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(X0,inverse(inverse(X5))),inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X5),
inference(superposition,[],[f37,f1]) ).
fof(f222,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(multiply(X8,X9)),multiply(X8,inverse(multiply(X4,inverse(X9))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(inverse(inverse(X5)))),inverse(X3))))))),inverse(b))))))),X5),
inference(superposition,[],[f37,f17]) ).
fof(f223,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),
inference(superposition,[],[f37,f37]) ).
fof(f235,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X5))),inverse(b))))))),inverse(inverse(X6))),inverse(X4))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),multiply(inverse(multiply(X9,X5)),multiply(X9,inverse(X0))))),X6),
inference(superposition,[],[f17,f37]) ).
fof(f236,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X3))),inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))))),X3),
inference(superposition,[],[f20,f37]) ).
fof(f237,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X3))),inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))))),X3),
inference(superposition,[],[f19,f37]) ).
fof(f238,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X5))),inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))),X5),
inference(superposition,[],[f1,f37]) ).
fof(f279,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X2,inverse(inverse(X3))),inverse(b))))))) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X2,inverse(inverse(X3))),inverse(b))))))),
inference(backward_demodulation,[],[f70,f238]) ).
fof(f366,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),multiply(inverse(multiply(X9,X5)),multiply(X9,inverse(X0))))),X6) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X5),inverse(inverse(X6))),inverse(X4))))))),
inference(backward_demodulation,[],[f235,f223]) ).
fof(f367,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))))),X3),
inference(backward_demodulation,[],[f236,f223]) ).
fof(f368,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(multiply(X0,inverse(X2))))))),X3),
inference(backward_demodulation,[],[f237,f223]) ).
fof(f402,plain,
! [X8,X6,X9,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(multiply(X8,X9)),multiply(X8,inverse(multiply(X4,inverse(X9))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X4,inverse(b))))))),inverse(X5)),inverse(b))))))),X5),
inference(backward_demodulation,[],[f222,f219]) ).
fof(f449,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X2,inverse(inverse(X3))),inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X2,inverse(b))))))),X3),
inference(forward_demodulation,[],[f279,f223]) ).
fof(f520,plain,
! [X0,X8,X6,X9,X7,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),multiply(inverse(multiply(X9,X5)),multiply(X9,inverse(X0))))),X6) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X5),inverse(b))))))),X6),
inference(forward_demodulation,[],[f366,f219]) ).
fof(f523,plain,
! [X8,X6,X9,X7,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(multiply(X8,X9)),multiply(X8,inverse(multiply(X4,inverse(X9))))))) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X4,inverse(b))))))),
inference(forward_demodulation,[],[f402,f37]) ).
fof(f626,plain,
! [X0,X5] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(X5,X0),inverse(X0)),inverse(b))))))) = X5,
inference(backward_demodulation,[],[f185,f523]) ).
fof(f746,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X0))))),X2),
inference(superposition,[],[f367,f37]) ).
fof(f758,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X0))))),X2),
inference(forward_demodulation,[],[f746,f223]) ).
fof(f774,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X0))))),X2),
inference(superposition,[],[f368,f37]) ).
fof(f776,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X1,inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(multiply(X1,inverse(X3))))),inverse(b))))))),X3)),X0))),X2),
inference(superposition,[],[f368,f37]) ).
fof(f784,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X1,inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),multiply(X1,inverse(X3))),X3)),X0))),X2),
inference(forward_demodulation,[],[f776,f223]) ).
fof(f786,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X0))))),X2),
inference(forward_demodulation,[],[f774,f223]) ).
fof(f806,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(inverse(X3)))),inverse(b))))))),inverse(b))))))),X3) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),
inference(superposition,[],[f449,f37]) ).
fof(f809,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),inverse(X3)),inverse(b))))))),X3),
inference(forward_demodulation,[],[f806,f223]) ).
fof(f814,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),
inference(forward_demodulation,[],[f809,f37]) ).
fof(f828,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sF0),multiply(a,inverse(X0))))),
inference(superposition,[],[f814,f37]) ).
fof(f843,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(multiply(b,a)),sF0)),multiply(inverse(sF0),multiply(a,inverse(X0))))),
inference(superposition,[],[f828,f4]) ).
fof(f845,plain,
! [X2,X3,X0] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(sF0),multiply(a,X0)))),
inference(superposition,[],[f828,f626]) ).
fof(f849,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))) = inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(sF0),multiply(a,inverse(X0))))),
inference(forward_demodulation,[],[f843,f6]) ).
fof(f851,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))) = inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(sF0),multiply(a,X0)))),
inference(superposition,[],[f849,f626]) ).
fof(f957,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X1,inverse(b))))))),X2),inverse(b))))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),X2)),X0))),X3),
inference(superposition,[],[f786,f37]) ).
fof(f989,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X1,inverse(b))))))),X2),inverse(b))))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),X2)),X0))),X3),
inference(forward_demodulation,[],[f957,f223]) ).
fof(f1483,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),inverse(X1)) = X0,
inference(superposition,[],[f37,f223]) ).
fof(f1508,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),b) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))),X1),inverse(X1)),
inference(superposition,[],[f1483,f1483]) ).
fof(f1514,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = multiply(multiply(X0,X2),inverse(X2)),
inference(superposition,[],[f1483,f626]) ).
fof(f1524,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X2,b)),multiply(X2,inverse(X0))))),X1),
inference(superposition,[],[f758,f1483]) ).
fof(f1566,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))) = multiply(multiply(multiply(X0,X2),X3),inverse(X3)),
inference(superposition,[],[f1514,f1514]) ).
fof(f1572,plain,
! [X0] : multiply(sF0,inverse(b)) = multiply(multiply(a,X0),inverse(X0)),
inference(superposition,[],[f1514,f4]) ).
fof(f1573,plain,
! [X0] : multiply(sF1,inverse(a)) = multiply(multiply(b,X0),inverse(X0)),
inference(superposition,[],[f1514,f6]) ).
fof(f1575,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,X3),inverse(X3)) = multiply(multiply(X2,multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1)),
inference(superposition,[],[f1514,f223]) ).
fof(f1645,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(X2,X3),X4),inverse(X4)) = multiply(multiply(multiply(X2,multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1)),inverse(inverse(X3))),
inference(superposition,[],[f1566,f223]) ).
fof(f1688,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))) = multiply(multiply(multiply(X0,X3),inverse(X3)),inverse(inverse(X2))),
inference(superposition,[],[f1566,f1566]) ).
fof(f1804,plain,
! [X2,X3,X0] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X3,b)),multiply(X3,X0)))),X2),
inference(superposition,[],[f1524,f626]) ).
fof(f1960,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,X0),X1)),multiply(sF0,inverse(b))))),X2),
inference(superposition,[],[f758,f1572]) ).
fof(f1993,plain,
! [X0,X8,X6,X9,X7,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),multiply(inverse(multiply(X9,X5)),multiply(X9,inverse(X0))))),X6) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,X0),X5)),multiply(sF0,inverse(b))))),X6),
inference(backward_demodulation,[],[f520,f1960]) ).
fof(f2005,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),X2)),X0))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,X1),X2)),multiply(sF0,inverse(b))))),X3),
inference(backward_demodulation,[],[f989,f1960]) ).
fof(f2116,plain,
! [X2,X3,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(X1,inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,multiply(X1,inverse(X3))),X3)),multiply(sF0,inverse(b))))),X2),
inference(backward_demodulation,[],[f784,f2005]) ).
fof(f2247,plain,
! [X2,X0,X1,X4] : multiply(multiply(multiply(X1,X2),inverse(X2)),inverse(X0)) = multiply(multiply(multiply(X1,X4),inverse(X4)),inverse(X0)),
inference(superposition,[],[f1688,f626]) ).
fof(f2404,plain,
! [X2,X0,X1,X4] : multiply(multiply(multiply(X1,X2),inverse(X2)),X0) = multiply(multiply(multiply(X1,X4),inverse(X4)),X0),
inference(superposition,[],[f2247,f626]) ).
fof(f2711,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(a,X0),inverse(b))))))),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,multiply(sF0,inverse(b))),X0)),multiply(sF0,inverse(b))))),X1),
inference(superposition,[],[f2116,f1572]) ).
fof(f2828,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))),X1),inverse(X1)),inverse(b)) = X0,
inference(superposition,[],[f1483,f1508]) ).
fof(f2901,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(b)))))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))),X2),inverse(X2)),inverse(b)),
inference(superposition,[],[f2828,f626]) ).
fof(f2904,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sF0),multiply(a,X0))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))))))),X3),inverse(X3)),inverse(b)),
inference(superposition,[],[f2828,f845]) ).
fof(f2905,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(sF0),multiply(a,X0))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))))))),X1),inverse(X1)),inverse(b)),
inference(superposition,[],[f2828,f851]) ).
fof(f2955,plain,
! [X0] : multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0))) = multiply(inverse(multiply(inverse(sF1),sF0)),multiply(inverse(sF0),multiply(a,X0))),
inference(forward_demodulation,[],[f2905,f2828]) ).
fof(f2956,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0))) = multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(sF0),multiply(a,X0))),
inference(forward_demodulation,[],[f2904,f2828]) ).
fof(f3010,plain,
! [X0] : inverse(multiply(inverse(sF1),sF0)) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0))),inverse(multiply(inverse(sF0),multiply(a,X0)))),inverse(b))))))),
inference(superposition,[],[f626,f2955]) ).
fof(f3017,plain,
inverse(multiply(inverse(sF1),sF0)) = inverse(multiply(inverse(sF0),sF1)),
inference(forward_demodulation,[],[f3010,f626]) ).
fof(f3190,plain,
! [X0] : multiply(inverse(sF1),sF0) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(sF0),sF1)))))),X0),inverse(X0)),inverse(b)),
inference(superposition,[],[f2828,f3017]) ).
fof(f3191,plain,
multiply(inverse(sF1),sF0) = multiply(inverse(sF0),sF1),
inference(forward_demodulation,[],[f3190,f2828]) ).
fof(f3368,plain,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0))),inverse(multiply(inverse(sF0),multiply(a,X0)))),inverse(b))))))),
inference(superposition,[],[f626,f2956]) ).
fof(f3377,plain,
! [X2,X1] : inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))) = inverse(multiply(inverse(sF0),sF1)),
inference(forward_demodulation,[],[f3368,f626]) ).
fof(f3435,plain,
! [X0,X6,X9,X5] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,X0),X5)),multiply(sF0,inverse(b))))),X6) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(X9,X5)),multiply(X9,inverse(X0))))),X6),
inference(backward_demodulation,[],[f1993,f3377]) ).
fof(f3554,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X1,X0)) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(sF0),sF1)))))),X2),inverse(X2)),inverse(b)),
inference(superposition,[],[f2828,f3377]) ).
fof(f3556,plain,
! [X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X1,X0)) = multiply(inverse(sF0),sF1),
inference(forward_demodulation,[],[f3554,f2828]) ).
fof(f3645,plain,
! [X2,X0,X1] : multiply(inverse(sF0),sF1) = multiply(inverse(multiply(inverse(X2),multiply(X0,X2))),multiply(multiply(X0,X1),inverse(X1))),
inference(superposition,[],[f3556,f1514]) ).
fof(f3650,plain,
! [X0,X1] : multiply(inverse(sF0),sF1) = multiply(inverse(multiply(inverse(b),multiply(multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(X0))))),X1),inverse(X1)))),X0),
inference(superposition,[],[f3556,f2828]) ).
fof(f3657,plain,
! [X0,X1] : multiply(inverse(sF0),sF1) = multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X1,X0)))),multiply(inverse(sF0),sF1)),
inference(superposition,[],[f3556,f3556]) ).
fof(f3658,plain,
multiply(inverse(sF0),sF1) = multiply(inverse(multiply(sF0,inverse(sF1))),multiply(inverse(sF0),sF1)),
inference(superposition,[],[f3556,f3191]) ).
fof(f3665,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))),inverse(multiply(inverse(sF0),sF1))))) = X0,
inference(superposition,[],[f1483,f3556]) ).
fof(f3668,plain,
! [X0] : multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(X0))),inverse(multiply(inverse(sF0),sF1))))),inverse(b)) = X0,
inference(superposition,[],[f2828,f3556]) ).
fof(f3672,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(X1,X0))),inverse(b))))))),
inference(superposition,[],[f626,f3556]) ).
fof(f3675,plain,
! [X2,X0,X1] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(X1,X0))) = multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2)),
inference(superposition,[],[f1514,f3556]) ).
fof(f3679,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X0,X1)),X2),inverse(X2)),X3) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(X1,X0))),X3),
inference(superposition,[],[f2404,f3556]) ).
fof(f3696,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(b)))))) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,X0)),inverse(multiply(inverse(sF0),sF1))))),inverse(b)),
inference(backward_demodulation,[],[f2901,f3679]) ).
fof(f3741,plain,
! [X0] : multiply(inverse(sF0),sF1) = multiply(inverse(multiply(inverse(b),multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(X0))),inverse(multiply(inverse(sF0),sF1))))))),X0),
inference(forward_demodulation,[],[f3650,f3675]) ).
fof(f3810,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(X1,X2),inverse(X2)))),inverse(b))))))),
inference(superposition,[],[f626,f3645]) ).
fof(f3826,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X0),multiply(X1,X0))) = inverse(multiply(inverse(X2),multiply(X1,X2))),
inference(forward_demodulation,[],[f3810,f3672]) ).
fof(f3893,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(a,X0))) = inverse(multiply(inverse(b),sF0)),
inference(superposition,[],[f3826,f4]) ).
fof(f3894,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(b,X0))) = inverse(multiply(inverse(a),sF1)),
inference(superposition,[],[f3826,f6]) ).
fof(f4040,plain,
inverse(multiply(sF0,inverse(sF1))) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),sF1))),inverse(b))))))),
inference(superposition,[],[f626,f3658]) ).
fof(f4043,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(multiply(sF0,inverse(sF1))),X0),X1),inverse(X1)) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),sF1))),inverse(inverse(X0))),
inference(superposition,[],[f1566,f3658]) ).
fof(f4059,plain,
inverse(multiply(sF0,inverse(sF1))) = inverse(multiply(sF1,inverse(sF0))),
inference(forward_demodulation,[],[f4040,f3672]) ).
fof(f4208,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(X1,X2)) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(X0),multiply(X1,X0))))),inverse(multiply(inverse(sF0),sF1))))),inverse(b)),
inference(superposition,[],[f3668,f3826]) ).
fof(f4209,plain,
! [X0] : multiply(inverse(X0),multiply(a,X0)) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(b),sF0)))),inverse(multiply(inverse(sF0),sF1))))),inverse(b)),
inference(superposition,[],[f3668,f3893]) ).
fof(f4210,plain,
! [X0] : multiply(inverse(X0),multiply(b,X0)) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(a),sF1)))),inverse(multiply(inverse(sF0),sF1))))),inverse(b)),
inference(superposition,[],[f3668,f3894]) ).
fof(f4211,plain,
multiply(sF1,inverse(sF0)) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(sF0,inverse(sF1))))),inverse(multiply(inverse(sF0),sF1))))),inverse(b)),
inference(superposition,[],[f3668,f4059]) ).
fof(f4241,plain,
multiply(sF0,inverse(sF1)) = multiply(sF1,inverse(sF0)),
inference(forward_demodulation,[],[f4211,f3668]) ).
fof(f4242,plain,
! [X0] : multiply(inverse(X0),multiply(b,X0)) = multiply(inverse(a),sF1),
inference(forward_demodulation,[],[f4210,f3668]) ).
fof(f4243,plain,
! [X0] : multiply(inverse(X0),multiply(a,X0)) = multiply(inverse(b),sF0),
inference(forward_demodulation,[],[f4209,f3668]) ).
fof(f4244,plain,
! [X2,X0,X1] : multiply(inverse(X0),multiply(X1,X0)) = multiply(inverse(X2),multiply(X1,X2)),
inference(forward_demodulation,[],[f4208,f3668]) ).
fof(f4335,plain,
! [X0,X1] : multiply(inverse(X0),multiply(multiply(b,X1),X0)) = multiply(inverse(inverse(X1)),multiply(sF1,inverse(a))),
inference(superposition,[],[f4244,f1573]) ).
fof(f4338,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(multiply(X0,X3),X2)) = multiply(inverse(inverse(X3)),multiply(multiply(X0,X1),inverse(X1))),
inference(superposition,[],[f4244,f1514]) ).
fof(f4351,plain,
! [X2,X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),X0)) = multiply(inverse(multiply(X2,X1)),multiply(inverse(sF0),sF1)),
inference(superposition,[],[f4244,f3556]) ).
fof(f4397,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(X2),X3),inverse(X3)),
inference(superposition,[],[f1514,f4244]) ).
fof(f4430,plain,
! [X0] : multiply(multiply(sF0,inverse(sF1)),inverse(inverse(sF0))) = multiply(multiply(sF1,X0),inverse(X0)),
inference(superposition,[],[f1514,f4241]) ).
fof(f4886,plain,
! [X2,X0,X1] : multiply(X0,multiply(inverse(sF0),sF1)) = multiply(inverse(X1),multiply(inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(X0,X2),inverse(X2)),inverse(b))))),inverse(multiply(inverse(sF0),sF1)))),X1)),
inference(superposition,[],[f4351,f626]) ).
fof(f4927,plain,
! [X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X1,inverse(multiply(inverse(sF0),sF1))),inverse(b))))),inverse(multiply(inverse(sF0),sF1)))),X0)) = X1,
inference(superposition,[],[f37,f4351]) ).
fof(f5533,plain,
! [X2,X0,X1] : multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,X2))) = multiply(multiply(inverse(a),sF1),inverse(multiply(b,X2))),
inference(superposition,[],[f4397,f4242]) ).
fof(f5534,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(X3,X2))) = multiply(multiply(inverse(X0),multiply(X1,X0)),inverse(multiply(X1,multiply(X2,X3)))),
inference(superposition,[],[f4397,f3556]) ).
fof(f5690,plain,
! [X2,X3] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(X3,X2))) = multiply(multiply(inverse(a),sF1),inverse(multiply(b,multiply(X2,X3)))),
inference(backward_demodulation,[],[f5534,f5533]) ).
fof(f13759,plain,
! [X0,X1] : inverse(multiply(multiply(X0,X1),inverse(multiply(X1,X0)))) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),sF1))),inverse(b))))))),
inference(superposition,[],[f626,f3657]) ).
fof(f13835,plain,
! [X0,X1] : inverse(multiply(multiply(X0,X1),inverse(multiply(X1,X0)))) = inverse(multiply(sF1,inverse(sF0))),
inference(forward_demodulation,[],[f13759,f3672]) ).
fof(f13895,plain,
! [X0,X1] : inverse(multiply(sF0,inverse(sF1))) = inverse(multiply(multiply(X0,X1),inverse(multiply(X1,X0)))),
inference(forward_demodulation,[],[f13835,f4241]) ).
fof(f14095,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(multiply(X1,X0))) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(multiply(sF0,inverse(sF1))))),inverse(multiply(inverse(sF0),sF1))))),inverse(b)),
inference(superposition,[],[f3668,f13895]) ).
fof(f14150,plain,
! [X0,X1] : multiply(sF0,inverse(sF1)) = multiply(multiply(X0,X1),inverse(multiply(X1,X0))),
inference(forward_demodulation,[],[f14095,f3668]) ).
fof(f14384,plain,
! [X0] : multiply(sF0,inverse(sF1)) = multiply(X0,inverse(multiply(inverse(b),multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(X0))),inverse(multiply(inverse(sF0),sF1)))))))),
inference(superposition,[],[f14150,f3668]) ).
fof(f14509,plain,
! [X2,X0,X1] : multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),inverse(X2))) = multiply(inverse(inverse(multiply(X0,X1))),multiply(sF0,inverse(sF1))),
inference(superposition,[],[f4338,f14150]) ).
fof(f14516,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(a,multiply(X0,X1)),X2)),multiply(sF0,inverse(b))))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(X1,X0),X2)),multiply(sF0,inverse(sF1))))),X3),
inference(superposition,[],[f3435,f14150]) ).
fof(f14518,plain,
! [X0,X1] : multiply(X0,X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b))))))),multiply(X1,X0)),
inference(superposition,[],[f37,f14150]) ).
fof(f14541,plain,
! [X2,X0,X1] : multiply(inverse(X0),multiply(multiply(X1,X2),X0)) = multiply(inverse(inverse(multiply(X2,X1))),multiply(sF0,inverse(sF1))),
inference(superposition,[],[f4244,f14150]) ).
fof(f14591,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(a,X0),inverse(b))))))),X1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(multiply(multiply(inverse(b),sF0),X0)),multiply(sF0,inverse(sF1))))),X1),
inference(backward_demodulation,[],[f2711,f14516]) ).
fof(f15206,plain,
! [X0] : multiply(inverse(b),multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(X0))),inverse(multiply(inverse(sF0),sF1)))))) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b))))))),X0),
inference(superposition,[],[f14518,f3668]) ).
fof(f15231,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b))))))),multiply(X0,X1)) = multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))))),
inference(superposition,[],[f14518,f14518]) ).
fof(f15263,plain,
multiply(inverse(sF0),sF1) = multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))),
inference(superposition,[],[f3556,f14518]) ).
fof(f15276,plain,
! [X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))),X0),
inference(superposition,[],[f4244,f14518]) ).
fof(f15296,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))),multiply(X0,X1)) = multiply(inverse(inverse(X1)),multiply(multiply(X0,X2),inverse(X2))),
inference(superposition,[],[f4338,f14518]) ).
fof(f15301,plain,
! [X0,X1] : multiply(inverse(multiply(X1,X0)),multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))),inverse(multiply(X0,X1))),
inference(superposition,[],[f4351,f14518]) ).
fof(f15302,plain,
multiply(inverse(b),sF0) = multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))),a),
inference(superposition,[],[f4243,f14518]) ).
fof(f15303,plain,
multiply(inverse(a),sF1) = multiply(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))),b),
inference(superposition,[],[f4242,f14518]) ).
fof(f15337,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(inverse(sF0),sF1)) = multiply(inverse(X2),multiply(inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b))))))))),X2)),
inference(superposition,[],[f4351,f14518]) ).
fof(f15342,plain,
! [X0,X1] : multiply(multiply(inverse(a),sF1),inverse(multiply(b,multiply(X0,X1)))) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))))))),
inference(superposition,[],[f5690,f14518]) ).
fof(f15381,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(X1,X0))) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(sF0,inverse(sF1)),inverse(b)))))))))),
inference(forward_demodulation,[],[f15342,f5690]) ).
fof(f15427,plain,
! [X0,X1] : multiply(X0,X1) = multiply(inverse(multiply(inverse(sF0),sF1)),multiply(X1,X0)),
inference(backward_demodulation,[],[f14518,f15263]) ).
fof(f15433,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF1),X0) = multiply(inverse(X1),multiply(X0,X1)),
inference(backward_demodulation,[],[f15276,f15263]) ).
fof(f15444,plain,
! [X2,X0,X1] : multiply(inverse(inverse(X1)),multiply(multiply(X0,X2),inverse(X2))) = multiply(multiply(inverse(sF0),sF1),multiply(X0,X1)),
inference(backward_demodulation,[],[f15296,f15263]) ).
fof(f15448,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(X0,X1))) = multiply(inverse(multiply(X1,X0)),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f15301,f15263]) ).
fof(f15449,plain,
multiply(inverse(b),sF0) = multiply(multiply(inverse(sF0),sF1),a),
inference(backward_demodulation,[],[f15302,f15263]) ).
fof(f15450,plain,
multiply(inverse(a),sF1) = multiply(multiply(inverse(sF0),sF1),b),
inference(backward_demodulation,[],[f15303,f15263]) ).
fof(f15455,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(inverse(sF0),sF1)) = multiply(inverse(X2),multiply(inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(sF0),sF1)))),X2)),
inference(backward_demodulation,[],[f15337,f15263]) ).
fof(f15488,plain,
! [X0,X1] : multiply(multiply(X1,X0),inverse(multiply(inverse(sF0),sF1))) = multiply(inverse(multiply(inverse(sF0),sF1)),multiply(X0,X1)),
inference(forward_demodulation,[],[f15231,f15263]) ).
fof(f15512,plain,
! [X0] : multiply(inverse(b),multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,inverse(X0))),inverse(multiply(inverse(sF0),sF1)))))) = multiply(inverse(multiply(inverse(sF0),sF1)),X0),
inference(forward_demodulation,[],[f15206,f15263]) ).
fof(f15563,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(X1,X0))) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(X1,X0),inverse(multiply(inverse(sF0),sF1))))),
inference(forward_demodulation,[],[f15381,f15263]) ).
fof(f15592,plain,
! [X1] : multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(X1,inverse(multiply(inverse(sF0),sF1))),inverse(b)))),inverse(sF0))),multiply(inverse(sF0),sF1)) = X1,
inference(backward_demodulation,[],[f4927,f15455]) ).
fof(f15594,plain,
! [X2,X0] : multiply(X0,multiply(inverse(sF0),sF1)) = multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(multiply(X0,X2),inverse(X2)),inverse(b)))),inverse(sF0))),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f4886,f15455]) ).
fof(f15794,plain,
! [X0,X1] : multiply(inverse(inverse(multiply(X0,X1))),multiply(sF0,inverse(sF1))) = multiply(multiply(inverse(sF0),sF1),multiply(X1,X0)),
inference(backward_demodulation,[],[f14509,f15444]) ).
fof(f15911,plain,
! [X2,X3,X0] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,X0)))),X2) = multiply(inverse(multiply(multiply(X3,X0),inverse(multiply(X3,b)))),X2),
inference(backward_demodulation,[],[f1804,f15427]) ).
fof(f16182,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(a,X0),inverse(b))))))),X1) = multiply(inverse(multiply(multiply(sF0,inverse(sF1)),inverse(multiply(multiply(inverse(b),sF0),X0)))),X1),
inference(backward_demodulation,[],[f14591,f15427]) ).
fof(f16203,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,X3),inverse(X3)) = multiply(multiply(X2,multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),multiply(inverse(multiply(multiply(a,inverse(multiply(X0,inverse(b)))),inverse(sF0))),X1)),
inference(backward_demodulation,[],[f1575,f15427]) ).
fof(f16205,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(X2,X3),X4),inverse(X4)) = multiply(multiply(multiply(X2,multiply(inverse(multiply(inverse(sF0),sF1)),multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),multiply(inverse(multiply(multiply(a,inverse(multiply(X0,inverse(b)))),inverse(sF0))),X1)),inverse(inverse(X3))),
inference(backward_demodulation,[],[f1645,f15427]) ).
fof(f16283,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(X0,inverse(X1)),inverse(b)))),inverse(sF0))),X1) = X0,
inference(backward_demodulation,[],[f37,f15427]) ).
fof(f16300,plain,
! [X0,X5] : inverse(multiply(multiply(a,inverse(multiply(multiply(multiply(X5,X0),inverse(X0)),inverse(b)))),inverse(sF0))) = X5,
inference(backward_demodulation,[],[f626,f15427]) ).
fof(f16308,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(multiply(inverse(sF0),multiply(a,X0)),inverse(multiply(inverse(sF0),sF1))))),inverse(b)) = multiply(multiply(a,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(b)))),inverse(sF0)),
inference(backward_demodulation,[],[f3696,f15427]) ).
fof(f16392,plain,
! [X0,X1] : multiply(X1,X0) = multiply(multiply(X1,X0),inverse(multiply(inverse(sF0),sF1))),
inference(forward_demodulation,[],[f15488,f15427]) ).
fof(f16416,plain,
! [X0] : multiply(inverse(sF0),sF1) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),X0)),X0),
inference(backward_demodulation,[],[f3741,f15512]) ).
fof(f16422,plain,
! [X0] : multiply(sF0,inverse(sF1)) = multiply(X0,inverse(multiply(inverse(multiply(inverse(sF0),sF1)),X0))),
inference(backward_demodulation,[],[f14384,f15512]) ).
fof(f16457,plain,
! [X0] : multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,inverse(X0))))),inverse(b)) = X0,
inference(backward_demodulation,[],[f3668,f15563]) ).
fof(f16464,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,inverse(multiply(X0,inverse(b))))))) = X0,
inference(backward_demodulation,[],[f3665,f15563]) ).
fof(f16488,plain,
! [X2,X0] : multiply(X0,multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(multiply(X0,X2),inverse(X2)),inverse(b))))))),
inference(forward_demodulation,[],[f15594,f15448]) ).
fof(f16490,plain,
! [X1] : multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,inverse(multiply(multiply(X1,inverse(multiply(inverse(sF0),sF1))),inverse(b))))))) = X1,
inference(forward_demodulation,[],[f15592,f15448]) ).
fof(f16777,plain,
! [X0,X1] : multiply(multiply(a,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(b)))),inverse(sF0)) = multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,X0)))),inverse(b)),
inference(forward_demodulation,[],[f16308,f15563]) ).
fof(f16834,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(X2,X3),X4),inverse(X4)) = multiply(multiply(multiply(X2,multiply(multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b)))),inverse(sF0))),multiply(inverse(multiply(multiply(a,inverse(multiply(X0,inverse(b)))),inverse(sF0))),X1)),inverse(inverse(X3))),
inference(forward_demodulation,[],[f16205,f15427]) ).
fof(f16835,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,X3),inverse(X3)) = multiply(multiply(X2,multiply(multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b)))),inverse(sF0))),multiply(inverse(multiply(multiply(a,inverse(multiply(X0,inverse(b)))),inverse(sF0))),X1)),
inference(forward_demodulation,[],[f16203,f15427]) ).
fof(f16852,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(sF0,inverse(sF1)),inverse(multiply(multiply(inverse(b),sF0),X0)))),X1) = multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(a,X0),inverse(b)))),inverse(sF0))),X1),
inference(forward_demodulation,[],[f16182,f15427]) ).
fof(f17119,plain,
! [X2,X3,X0] : multiply(inverse(multiply(multiply(X3,X0),inverse(multiply(X3,b)))),X2) = multiply(inverse(multiply(multiply(a,X0),inverse(sF0))),X2),
inference(forward_demodulation,[],[f15911,f15427]) ).
fof(f17211,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(multiply(sF0,inverse(sF1))),X0),X1),inverse(X1)) = multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))),
inference(backward_demodulation,[],[f4043,f16392]) ).
fof(f17248,plain,
! [X2,X0] : multiply(multiply(X0,X2),inverse(X2)) = multiply(X0,multiply(inverse(sF0),sF1)),
inference(forward_demodulation,[],[f16488,f16464]) ).
fof(f17250,plain,
! [X1] : multiply(X1,inverse(multiply(inverse(sF0),sF1))) = X1,
inference(forward_demodulation,[],[f16490,f16464]) ).
fof(f17574,plain,
multiply(sF1,inverse(a)) = multiply(b,multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f1573,f17248]) ).
fof(f17575,plain,
multiply(multiply(sF0,inverse(sF1)),inverse(inverse(sF0))) = multiply(sF1,multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f4430,f17248]) ).
fof(f17864,plain,
! [X5] : inverse(multiply(multiply(a,inverse(multiply(multiply(X5,multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0))) = X5,
inference(backward_demodulation,[],[f16300,f17248]) ).
fof(f17906,plain,
! [X0] : multiply(multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,X0)))),inverse(b)) = multiply(multiply(a,inverse(multiply(multiply(X0,multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0)),
inference(backward_demodulation,[],[f16777,f17248]) ).
fof(f17918,plain,
! [X2,X0,X1] : multiply(X2,multiply(inverse(sF0),sF1)) = multiply(multiply(X2,multiply(multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b)))),inverse(sF0))),multiply(inverse(multiply(multiply(a,inverse(multiply(X0,inverse(b)))),inverse(sF0))),X1)),
inference(backward_demodulation,[],[f16835,f17248]) ).
fof(f17944,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))) = multiply(multiply(inverse(multiply(sF0,inverse(sF1))),X0),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f17211,f17248]) ).
fof(f18083,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X2,multiply(multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b)))),inverse(sF0))),multiply(inverse(multiply(multiply(a,inverse(multiply(X0,inverse(b)))),inverse(sF0))),X1)),inverse(inverse(X3))) = multiply(multiply(X2,X3),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f16834,f17248]) ).
fof(f18428,plain,
! [X2,X3] : multiply(multiply(X2,X3),multiply(inverse(sF0),sF1)) = multiply(multiply(X2,multiply(inverse(sF0),sF1)),inverse(inverse(X3))),
inference(backward_demodulation,[],[f18083,f17918]) ).
fof(f18433,plain,
! [X0] : multiply(multiply(a,inverse(multiply(multiply(inverse(X0),multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0)) = X0,
inference(backward_demodulation,[],[f16457,f17906]) ).
fof(f19197,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF1),multiply(inverse(sF0),sF1)) = multiply(inverse(X1),multiply(inverse(X0),multiply(X1,X0))),
inference(superposition,[],[f15433,f15433]) ).
fof(f19212,plain,
! [X0,X1] : multiply(inverse(multiply(sF1,inverse(a))),multiply(inverse(X0),multiply(multiply(b,X1),X0))) = multiply(multiply(inverse(sF0),sF1),inverse(inverse(X1))),
inference(superposition,[],[f15433,f4335]) ).
fof(f19249,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(multiply(inverse(sF0),sF1),X2)) = multiply(inverse(X1),multiply(inverse(X0),multiply(X1,X0))),
inference(superposition,[],[f4244,f15433]) ).
fof(f20580,plain,
multiply(inverse(sF0),sF1) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),inverse(multiply(inverse(sF0),sF1)))),
inference(superposition,[],[f17250,f16416]) ).
fof(f20641,plain,
multiply(inverse(sF0),sF1) = inverse(inverse(multiply(inverse(sF0),sF1))),
inference(forward_demodulation,[],[f20580,f17250]) ).
fof(f21148,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),inverse(X0))) = multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(inverse(sF0),sF1),inverse(b)))),inverse(sF0))),X0),
inference(superposition,[],[f16283,f16416]) ).
fof(f22412,plain,
! [X0] : multiply(inverse(X0),multiply(multiply(inverse(sF0),sF1),X0)) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(superposition,[],[f4244,f15449]) ).
fof(f22438,plain,
multiply(multiply(inverse(sF0),sF1),multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(b),sF0),inverse(a)),
inference(superposition,[],[f17248,f15449]) ).
fof(f22459,plain,
! [X0,X1] : multiply(inverse(X1),multiply(inverse(X0),multiply(X1,X0))) = multiply(multiply(inverse(b),sF0),inverse(a)),
inference(backward_demodulation,[],[f19197,f22438]) ).
fof(f22484,plain,
! [X0,X1] : multiply(inverse(X1),multiply(inverse(X0),multiply(X1,X0))) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(backward_demodulation,[],[f19249,f22412]) ).
fof(f22500,plain,
multiply(inverse(a),multiply(inverse(b),sF0)) = multiply(multiply(inverse(b),sF0),inverse(a)),
inference(backward_demodulation,[],[f22459,f22484]) ).
fof(f22512,plain,
multiply(multiply(inverse(sF0),sF1),multiply(inverse(sF0),sF1)) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(backward_demodulation,[],[f22438,f22500]) ).
fof(f22601,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(a,inverse(multiply(inverse(sF0),sF1))),inverse(sF0))),X1) = multiply(inverse(multiply(X0,inverse(multiply(X0,b)))),X1),
inference(superposition,[],[f17119,f17250]) ).
fof(f22660,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(sF1))),X0) = multiply(inverse(multiply(multiply(a,b),inverse(sF0))),X0),
inference(superposition,[],[f17119,f14150]) ).
fof(f22907,plain,
! [X0] : multiply(inverse(multiply(sF0,inverse(sF1))),X0) = multiply(inverse(multiply(sF0,inverse(sF0))),X0),
inference(forward_demodulation,[],[f22660,f4]) ).
fof(f22945,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X0,b)))),X1) = multiply(inverse(multiply(a,inverse(sF0))),X1),
inference(forward_demodulation,[],[f22601,f17250]) ).
fof(f22961,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))) = multiply(multiply(inverse(multiply(sF0,inverse(sF0))),X0),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f17944,f22907]) ).
fof(f22966,plain,
multiply(inverse(sF0),sF1) = multiply(inverse(multiply(sF0,inverse(sF0))),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f3658,f22907]) ).
fof(f22976,plain,
multiply(inverse(sF0),sF1) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),sF0))),
inference(forward_demodulation,[],[f22966,f15448]) ).
fof(f23095,plain,
inverse(multiply(sF0,inverse(sF1))) = multiply(inverse(multiply(sF0,inverse(sF0))),inverse(multiply(inverse(sF0),sF1))),
inference(superposition,[],[f17250,f22907]) ).
fof(f23118,plain,
inverse(multiply(sF0,inverse(sF1))) = inverse(multiply(sF0,inverse(sF0))),
inference(forward_demodulation,[],[f23095,f17250]) ).
fof(f23306,plain,
inverse(multiply(sF1,inverse(sF0))) = inverse(multiply(multiply(a,inverse(multiply(multiply(inverse(sF0),sF1),inverse(b)))),inverse(sF0))),
inference(superposition,[],[f17864,f3556]) ).
fof(f23413,plain,
inverse(multiply(sF0,inverse(sF1))) = inverse(multiply(multiply(a,inverse(multiply(multiply(inverse(sF0),sF1),inverse(b)))),inverse(sF0))),
inference(forward_demodulation,[],[f23306,f4241]) ).
fof(f23420,plain,
inverse(multiply(multiply(a,inverse(multiply(multiply(inverse(sF0),sF1),inverse(b)))),inverse(sF0))) = inverse(multiply(sF0,inverse(sF0))),
inference(forward_demodulation,[],[f23413,f23118]) ).
fof(f23422,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(sF0),sF1)),inverse(X0))) = multiply(inverse(multiply(sF0,inverse(sF0))),X0),
inference(backward_demodulation,[],[f21148,f23420]) ).
fof(f23532,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(sF0),sF1),X1),multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(X0),multiply(multiply(inverse(sF0),sF1),X0)),inverse(inverse(X1))),
inference(superposition,[],[f18428,f15433]) ).
fof(f23705,plain,
! [X1] : multiply(multiply(multiply(inverse(sF0),sF1),X1),multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(a),multiply(inverse(b),sF0)),inverse(inverse(X1))),
inference(forward_demodulation,[],[f23532,f22412]) ).
fof(f25603,plain,
! [X0] : multiply(inverse(multiply(inverse(sF0),sF1)),inverse(X0)) = multiply(multiply(a,inverse(multiply(multiply(multiply(inverse(multiply(sF0,inverse(sF0))),X0),multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0)),
inference(superposition,[],[f18433,f23422]) ).
fof(f25675,plain,
! [X0] : multiply(inverse(multiply(inverse(sF0),sF1)),inverse(X0)) = multiply(multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))),inverse(b)))),inverse(sF0)),
inference(forward_demodulation,[],[f25603,f22961]) ).
fof(f27557,plain,
multiply(inverse(sF0),sF1) = multiply(inverse(multiply(a,inverse(sF0))),inverse(multiply(inverse(multiply(inverse(sF0),sF1)),b))),
inference(superposition,[],[f16416,f22945]) ).
fof(f27603,plain,
! [X0] : multiply(X0,inverse(multiply(X0,b))) = multiply(multiply(a,inverse(multiply(multiply(inverse(multiply(a,inverse(sF0))),multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0)),
inference(superposition,[],[f18433,f22945]) ).
fof(f27733,plain,
! [X0] : multiply(a,inverse(sF0)) = multiply(X0,inverse(multiply(X0,b))),
inference(forward_demodulation,[],[f27603,f18433]) ).
fof(f27841,plain,
multiply(a,inverse(sF0)) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),b)),inverse(multiply(inverse(sF0),sF1))),
inference(superposition,[],[f27733,f16416]) ).
fof(f27854,plain,
! [X0] : multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(a,inverse(sF0)),inverse(b)))),inverse(sF0))),multiply(X0,b)) = X0,
inference(superposition,[],[f16283,f27733]) ).
fof(f27883,plain,
! [X0] : multiply(inverse(multiply(X0,b)),X0) = multiply(inverse(multiply(inverse(sF0),sF1)),multiply(a,inverse(sF0))),
inference(superposition,[],[f15427,f27733]) ).
fof(f27893,plain,
! [X0] : multiply(X0,multiply(inverse(sF0),sF1)) = multiply(multiply(a,inverse(sF0)),inverse(inverse(multiply(X0,b)))),
inference(superposition,[],[f17248,f27733]) ).
fof(f27914,plain,
multiply(sF0,inverse(sF1)) = multiply(inverse(multiply(inverse(multiply(inverse(sF0),sF1)),b)),inverse(multiply(a,inverse(sF0)))),
inference(superposition,[],[f16422,f27733]) ).
fof(f27952,plain,
! [X0] : multiply(inverse(sF0),a) = multiply(inverse(multiply(X0,b)),X0),
inference(forward_demodulation,[],[f27883,f15427]) ).
fof(f27975,plain,
! [X0] : multiply(inverse(multiply(multiply(sF0,inverse(sF1)),inverse(multiply(multiply(inverse(b),sF0),inverse(sF0))))),multiply(X0,b)) = X0,
inference(forward_demodulation,[],[f27854,f16852]) ).
fof(f27980,plain,
multiply(a,inverse(sF0)) = inverse(multiply(inverse(multiply(inverse(sF0),sF1)),b)),
inference(forward_demodulation,[],[f27841,f17250]) ).
fof(f27993,plain,
! [X0] : multiply(inverse(multiply(multiply(sF0,inverse(sF1)),inverse(multiply(inverse(b),multiply(inverse(sF0),sF1))))),multiply(X0,b)) = X0,
inference(forward_demodulation,[],[f27975,f17248]) ).
fof(f27994,plain,
multiply(sF0,inverse(sF1)) = multiply(multiply(a,inverse(sF0)),inverse(multiply(a,inverse(sF0)))),
inference(backward_demodulation,[],[f27914,f27980]) ).
fof(f27995,plain,
multiply(inverse(sF0),sF1) = multiply(inverse(multiply(a,inverse(sF0))),multiply(a,inverse(sF0))),
inference(backward_demodulation,[],[f27557,f27980]) ).
fof(f28050,plain,
! [X0] : multiply(inverse(X0),multiply(inverse(multiply(b,multiply(inverse(sF0),sF1))),X0)) = multiply(inverse(sF0),a),
inference(superposition,[],[f4351,f27952]) ).
fof(f28057,plain,
! [X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(X1,b)),X0)) = multiply(inverse(X1),multiply(inverse(sF0),a)),
inference(superposition,[],[f4244,f27952]) ).
fof(f28107,plain,
inverse(multiply(inverse(multiply(inverse(sF0),sF1)),b)) = multiply(inverse(sF0),a),
inference(superposition,[],[f17250,f27952]) ).
fof(f28119,plain,
inverse(multiply(inverse(b),b)) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,inverse(multiply(inverse(sF0),a)))))),
inference(superposition,[],[f16464,f27952]) ).
fof(f28123,plain,
multiply(a,inverse(sF0)) = multiply(inverse(sF0),a),
inference(forward_demodulation,[],[f28107,f27980]) ).
fof(f28143,plain,
! [X0] : multiply(inverse(X0),multiply(inverse(multiply(sF1,inverse(a))),X0)) = multiply(inverse(sF0),a),
inference(forward_demodulation,[],[f28050,f17574]) ).
fof(f28154,plain,
! [X0] : multiply(a,inverse(sF0)) = multiply(inverse(multiply(X0,b)),X0),
inference(backward_demodulation,[],[f27952,f28123]) ).
fof(f28159,plain,
! [X0,X1] : multiply(inverse(X0),multiply(inverse(multiply(X1,b)),X0)) = multiply(inverse(X1),multiply(a,inverse(sF0))),
inference(backward_demodulation,[],[f28057,f28123]) ).
fof(f28174,plain,
inverse(multiply(inverse(b),b)) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,inverse(multiply(a,inverse(sF0))))))),
inference(backward_demodulation,[],[f28119,f28123]) ).
fof(f28188,plain,
! [X0] : multiply(a,inverse(sF0)) = multiply(inverse(X0),multiply(inverse(multiply(sF1,inverse(a))),X0)),
inference(forward_demodulation,[],[f28143,f28123]) ).
fof(f28293,plain,
! [X0] : inverse(multiply(inverse(X0),b)) = multiply(inverse(multiply(multiply(a,inverse(multiply(multiply(a,inverse(sF0)),inverse(b)))),inverse(sF0))),X0),
inference(superposition,[],[f16283,f28154]) ).
fof(f28313,plain,
! [X0] : inverse(multiply(inverse(X0),b)) = multiply(inverse(multiply(multiply(sF0,inverse(sF1)),inverse(multiply(multiply(inverse(b),sF0),inverse(sF0))))),X0),
inference(forward_demodulation,[],[f28293,f16852]) ).
fof(f28334,plain,
! [X0] : inverse(multiply(inverse(X0),b)) = multiply(inverse(multiply(multiply(sF0,inverse(sF1)),inverse(multiply(inverse(b),multiply(inverse(sF0),sF1))))),X0),
inference(forward_demodulation,[],[f28313,f17248]) ).
fof(f28342,plain,
! [X0] : inverse(multiply(inverse(multiply(X0,b)),b)) = X0,
inference(backward_demodulation,[],[f27993,f28334]) ).
fof(f28360,plain,
b = inverse(multiply(a,inverse(sF0))),
inference(superposition,[],[f28342,f28154]) ).
fof(f28416,plain,
! [X0] : multiply(multiply(a,inverse(multiply(multiply(X0,multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0)) = multiply(inverse(multiply(X0,b)),b),
inference(superposition,[],[f18433,f28342]) ).
fof(f28431,plain,
! [X0] : multiply(inverse(multiply(inverse(X0),b)),b) = X0,
inference(backward_demodulation,[],[f18433,f28416]) ).
fof(f28475,plain,
multiply(sF0,inverse(sF1)) = multiply(multiply(a,inverse(sF0)),b),
inference(backward_demodulation,[],[f27994,f28360]) ).
fof(f28476,plain,
multiply(inverse(sF0),sF1) = multiply(b,multiply(a,inverse(sF0))),
inference(backward_demodulation,[],[f27995,f28360]) ).
fof(f28480,plain,
inverse(multiply(inverse(b),b)) = multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),multiply(a,b)))),
inference(backward_demodulation,[],[f28174,f28360]) ).
fof(f28499,plain,
multiply(multiply(inverse(sF0),sF1),inverse(multiply(inverse(sF0),sF0))) = inverse(multiply(inverse(b),b)),
inference(forward_demodulation,[],[f28480,f4]) ).
fof(f28504,plain,
multiply(inverse(sF0),sF1) = inverse(multiply(inverse(b),b)),
inference(forward_demodulation,[],[f28499,f22976]) ).
fof(f28519,plain,
inverse(multiply(inverse(sF0),sF1)) = multiply(inverse(multiply(multiply(inverse(sF0),sF1),b)),b),
inference(superposition,[],[f28431,f20641]) ).
fof(f28534,plain,
! [X0,X1] : multiply(inverse(b),X0) = multiply(inverse(X1),multiply(inverse(multiply(inverse(X0),b)),X1)),
inference(superposition,[],[f4244,f28431]) ).
fof(f28557,plain,
! [X0] : multiply(inverse(multiply(inverse(sF0),sF1)),X0) = multiply(b,inverse(multiply(inverse(X0),b))),
inference(superposition,[],[f15427,f28431]) ).
fof(f28602,plain,
! [X0] : multiply(multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))),inverse(b)))),inverse(sF0)) = multiply(b,inverse(multiply(inverse(inverse(X0)),b))),
inference(backward_demodulation,[],[f25675,f28557]) ).
fof(f28612,plain,
multiply(a,inverse(sF0)) = inverse(multiply(b,inverse(multiply(inverse(b),b)))),
inference(backward_demodulation,[],[f27980,f28557]) ).
fof(f28635,plain,
! [X0] : multiply(inverse(b),X0) = multiply(inverse(inverse(X0)),multiply(a,inverse(sF0))),
inference(forward_demodulation,[],[f28534,f28159]) ).
fof(f28644,plain,
inverse(multiply(inverse(sF0),sF1)) = multiply(inverse(multiply(inverse(a),sF1)),b),
inference(forward_demodulation,[],[f28519,f15450]) ).
fof(f28660,plain,
multiply(a,inverse(sF0)) = inverse(multiply(b,multiply(inverse(sF0),sF1))),
inference(forward_demodulation,[],[f28612,f28504]) ).
fof(f28690,plain,
inverse(multiply(sF1,inverse(a))) = multiply(a,inverse(sF0)),
inference(forward_demodulation,[],[f28660,f17574]) ).
fof(f28703,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF1),inverse(inverse(X1))) = multiply(multiply(a,inverse(sF0)),multiply(inverse(X0),multiply(multiply(b,X1),X0))),
inference(backward_demodulation,[],[f19212,f28690]) ).
fof(f28705,plain,
! [X0] : multiply(a,inverse(sF0)) = multiply(inverse(X0),multiply(multiply(a,inverse(sF0)),X0)),
inference(backward_demodulation,[],[f28188,f28690]) ).
fof(f28848,plain,
! [X0] : multiply(b,multiply(inverse(sF0),sF1)) = multiply(inverse(X0),multiply(inverse(multiply(inverse(sF0),a)),X0)),
inference(superposition,[],[f4351,f28360]) ).
fof(f28885,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),X0) = multiply(b,multiply(X0,multiply(a,inverse(sF0)))),
inference(superposition,[],[f15433,f28360]) ).
fof(f28939,plain,
! [X0] : multiply(b,multiply(inverse(sF0),sF1)) = multiply(inverse(X0),multiply(inverse(multiply(a,inverse(sF0))),X0)),
inference(forward_demodulation,[],[f28848,f28123]) ).
fof(f28947,plain,
! [X0] : multiply(inverse(X0),multiply(b,X0)) = multiply(b,multiply(inverse(sF0),sF1)),
inference(forward_demodulation,[],[f28939,f28360]) ).
fof(f28949,plain,
! [X0] : multiply(sF1,inverse(a)) = multiply(inverse(X0),multiply(b,X0)),
inference(forward_demodulation,[],[f28947,f17574]) ).
fof(f28950,plain,
multiply(sF1,inverse(a)) = multiply(inverse(a),sF1),
inference(backward_demodulation,[],[f4242,f28949]) ).
fof(f28991,plain,
inverse(multiply(inverse(sF0),sF1)) = multiply(inverse(multiply(sF1,inverse(a))),b),
inference(backward_demodulation,[],[f28644,f28950]) ).
fof(f29000,plain,
inverse(multiply(inverse(sF0),sF1)) = multiply(multiply(a,inverse(sF0)),b),
inference(forward_demodulation,[],[f28991,f28690]) ).
fof(f29017,plain,
inverse(multiply(inverse(sF0),sF1)) = multiply(sF0,inverse(sF1)),
inference(forward_demodulation,[],[f29000,f28475]) ).
fof(f29026,plain,
! [X1] : multiply(X1,multiply(sF0,inverse(sF1))) = X1,
inference(backward_demodulation,[],[f17250,f29017]) ).
fof(f29027,plain,
multiply(inverse(sF0),sF1) = inverse(multiply(sF0,inverse(sF1))),
inference(backward_demodulation,[],[f20641,f29017]) ).
fof(f29029,plain,
! [X0] : multiply(multiply(sF0,inverse(sF1)),X0) = multiply(b,inverse(multiply(inverse(X0),b))),
inference(backward_demodulation,[],[f28557,f29017]) ).
fof(f29062,plain,
! [X0] : multiply(multiply(sF0,inverse(sF1)),inverse(X0)) = multiply(multiply(a,inverse(multiply(multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))),inverse(b)))),inverse(sF0)),
inference(backward_demodulation,[],[f28602,f29029]) ).
fof(f29067,plain,
multiply(inverse(sF0),sF1) = inverse(multiply(sF0,inverse(sF0))),
inference(backward_demodulation,[],[f23118,f29027]) ).
fof(f29070,plain,
! [X2,X0,X1] : multiply(inverse(X0),multiply(multiply(X1,X2),X0)) = inverse(inverse(multiply(X2,X1))),
inference(backward_demodulation,[],[f14541,f29026]) ).
fof(f29071,plain,
! [X0,X1] : inverse(inverse(multiply(X0,X1))) = multiply(multiply(inverse(sF0),sF1),multiply(X1,X0)),
inference(backward_demodulation,[],[f15794,f29026]) ).
fof(f29098,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),inverse(inverse(X0))) = multiply(multiply(multiply(inverse(sF0),sF1),X0),multiply(inverse(sF0),sF1)),
inference(backward_demodulation,[],[f22961,f29067]) ).
fof(f29241,plain,
inverse(inverse(multiply(sF1,inverse(sF0)))) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(backward_demodulation,[],[f22512,f29071]) ).
fof(f29341,plain,
! [X1] : multiply(multiply(inverse(sF0),sF1),inverse(inverse(X1))) = multiply(multiply(a,inverse(sF0)),inverse(inverse(multiply(X1,b)))),
inference(backward_demodulation,[],[f28703,f29070]) ).
fof(f29412,plain,
multiply(a,inverse(sF0)) = inverse(inverse(multiply(inverse(sF0),a))),
inference(backward_demodulation,[],[f28705,f29070]) ).
fof(f29470,plain,
! [X1] : multiply(multiply(inverse(sF0),sF1),inverse(inverse(X1))) = multiply(multiply(inverse(a),multiply(inverse(b),sF0)),inverse(inverse(X1))),
inference(backward_demodulation,[],[f23705,f29098]) ).
fof(f29503,plain,
inverse(inverse(multiply(sF0,inverse(sF1)))) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(forward_demodulation,[],[f29241,f4241]) ).
fof(f29606,plain,
multiply(a,inverse(sF0)) = inverse(inverse(multiply(a,inverse(sF0)))),
inference(forward_demodulation,[],[f29412,f28123]) ).
fof(f29654,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(sF0),sF1),inverse(inverse(X1))),
inference(forward_demodulation,[],[f29341,f27893]) ).
fof(f29757,plain,
inverse(multiply(inverse(sF0),sF1)) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(forward_demodulation,[],[f29503,f29027]) ).
fof(f29793,plain,
inverse(b) = multiply(a,inverse(sF0)),
inference(forward_demodulation,[],[f29606,f28360]) ).
fof(f29815,plain,
! [X0] : multiply(multiply(sF0,inverse(sF1)),inverse(X0)) = multiply(multiply(a,inverse(multiply(multiply(X0,multiply(inverse(sF0),sF1)),inverse(b)))),inverse(sF0)),
inference(backward_demodulation,[],[f29062,f29654]) ).
fof(f29819,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = multiply(multiply(inverse(a),multiply(inverse(b),sF0)),inverse(inverse(X1))),
inference(backward_demodulation,[],[f29470,f29654]) ).
fof(f29983,plain,
multiply(sF0,inverse(sF1)) = multiply(inverse(a),multiply(inverse(b),sF0)),
inference(forward_demodulation,[],[f29757,f29017]) ).
fof(f30032,plain,
multiply(inverse(sF0),sF1) = multiply(b,inverse(b)),
inference(backward_demodulation,[],[f28476,f29793]) ).
fof(f30036,plain,
! [X0] : multiply(inverse(b),X0) = multiply(inverse(inverse(X0)),inverse(b)),
inference(backward_demodulation,[],[f28635,f29793]) ).
fof(f30050,plain,
! [X0] : multiply(multiply(inverse(sF0),sF1),X0) = multiply(b,multiply(X0,inverse(b))),
inference(backward_demodulation,[],[f28885,f29793]) ).
fof(f30132,plain,
! [X0] : multiply(multiply(sF0,inverse(sF1)),inverse(X0)) = multiply(inverse(multiply(X0,b)),b),
inference(forward_demodulation,[],[f29815,f28416]) ).
fof(f30281,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = multiply(multiply(sF0,inverse(sF1)),inverse(inverse(X1))),
inference(backward_demodulation,[],[f29819,f29983]) ).
fof(f30517,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = multiply(b,multiply(inverse(inverse(X1)),inverse(b))),
inference(backward_demodulation,[],[f29654,f30050]) ).
fof(f30828,plain,
multiply(multiply(sF0,inverse(sF1)),inverse(inverse(sF0))) = multiply(sF1,multiply(b,inverse(b))),
inference(backward_demodulation,[],[f17575,f30032]) ).
fof(f31177,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = multiply(inverse(multiply(inverse(X1),b)),b),
inference(forward_demodulation,[],[f30281,f30132]) ).
fof(f31218,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = multiply(b,multiply(inverse(b),X1)),
inference(forward_demodulation,[],[f30517,f30036]) ).
fof(f31612,plain,
multiply(sF1,multiply(b,inverse(b))) = multiply(inverse(multiply(inverse(sF0),b)),b),
inference(forward_demodulation,[],[f30828,f30132]) ).
fof(f31886,plain,
! [X1] : multiply(X1,multiply(inverse(sF0),sF1)) = X1,
inference(forward_demodulation,[],[f31177,f28431]) ).
fof(f31919,plain,
! [X1] : multiply(X1,multiply(b,inverse(b))) = multiply(b,multiply(inverse(b),X1)),
inference(forward_demodulation,[],[f31218,f30032]) ).
fof(f32165,plain,
sF0 = multiply(sF1,multiply(b,inverse(b))),
inference(forward_demodulation,[],[f31612,f28431]) ).
fof(f32438,plain,
! [X1] : multiply(X1,multiply(b,inverse(b))) = X1,
inference(forward_demodulation,[],[f31886,f30032]) ).
fof(f32662,plain,
sF0 = multiply(b,multiply(inverse(b),sF1)),
inference(forward_demodulation,[],[f32165,f31919]) ).
fof(f32962,plain,
! [X1] : multiply(b,multiply(inverse(b),X1)) = X1,
inference(backward_demodulation,[],[f31919,f32438]) ).
fof(f33633,plain,
sF0 = sF1,
inference(backward_demodulation,[],[f32662,f32962]) ).
fof(f34229,plain,
$false,
inference(forward_subsumption_resolution,[],[f33633,f7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 10:09:06 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.38/6.21 % (3310606)Detected a unit-equality problem, will run specialized UEQ schedule.
% 18.38/6.21 % (3310662)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=780716320:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 18.38/6.21 % (3310662)Instruction limit reached!
% 18.38/6.21 % (3310662)------------------------------
% 18.38/6.21 % (3310662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310662)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310662)Termination reason: Instruction limit
% 18.38/6.21 % (3310662)Termination phase: Saturation
% 18.38/6.21 % (3310662)Time elapsed: 0.040 s
% 18.38/6.21 % (3310662)Peak memory usage: 88 MB
% 18.38/6.21 % (3310662)Instructions burned: 139 (million)
% 18.38/6.21 % (3310661)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3398225008:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 18.38/6.21 % (3310663)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=586748473:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 18.38/6.21 % (3310659)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=199609463:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 18.38/6.21 % (3310660)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3573545086:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 18.38/6.21 % (3310665)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1177511459:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 18.38/6.21 % (3310664)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2578115445:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 18.38/6.21 % (3310663)Instruction limit reached!
% 18.38/6.21 % (3310663)------------------------------
% 18.38/6.21 % (3310663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310663)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310663)Termination reason: Instruction limit
% 18.38/6.21 % (3310663)Termination phase: Saturation
% 18.38/6.21 % (3310663)Time elapsed: 0.094 s
% 18.38/6.21 % (3310663)Peak memory usage: 89 MB
% 18.38/6.21 % (3310663)Instructions burned: 183 (million)
% 18.38/6.21 % (3310671)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2190920078:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 18.38/6.21 % (3310674)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3628197208:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 18.38/6.21 % (3310664)Instruction limit reached!
% 18.38/6.21 % (3310664)------------------------------
% 18.38/6.21 % (3310664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310664)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310664)Termination reason: Instruction limit
% 18.38/6.21 % (3310664)Termination phase: Saturation
% 18.38/6.21 % (3310664)Time elapsed: 0.233 s
% 18.38/6.21 % (3310664)Peak memory usage: 90 MB
% 18.38/6.21 % (3310664)Instructions burned: 258 (million)
% 18.38/6.21 % (3310677)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2056818184:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 18.38/6.21 % (3310677)Instruction limit reached!
% 18.38/6.21 % (3310677)------------------------------
% 18.38/6.21 % (3310677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310677)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310677)Termination reason: Instruction limit
% 18.38/6.21 % (3310677)Termination phase: Saturation
% 18.38/6.21 % (3310677)Time elapsed: 0.191 s
% 18.38/6.21 % (3310677)Peak memory usage: 89 MB
% 18.38/6.21 % (3310677)Instructions burned: 216 (million)
% 18.38/6.21 % (3310665)Instruction limit reached!
% 18.38/6.21 % (3310665)------------------------------
% 18.38/6.21 % (3310665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310665)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310665)Termination reason: Instruction limit
% 18.38/6.21 % (3310665)Termination phase: Saturation
% 18.38/6.21 % (3310665)Time elapsed: 0.713 s
% 18.38/6.21 % (3310665)Peak memory usage: 95 MB
% 18.38/6.21 % (3310665)Instructions burned: 1187 (million)
% 18.38/6.21 % (3310694)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=3273967230:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 18.38/6.21 % (3310695)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=2716619577:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/12125Mi)
% 18.38/6.21 % (3310671)Instruction limit reached!
% 18.38/6.21 % (3310671)------------------------------
% 18.38/6.21 % (3310671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310671)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310671)Termination reason: Instruction limit
% 18.38/6.21 % (3310671)Termination phase: Saturation
% 18.38/6.21 % (3310671)Time elapsed: 0.837 s
% 18.38/6.21 % (3310671)Peak memory usage: 139 MB
% 18.38/6.21 % (3310671)Instructions burned: 2051 (million)
% 18.38/6.21 % (3310694)Instruction limit reached!
% 18.38/6.21 % (3310694)------------------------------
% 18.38/6.21 % (3310694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310694)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310694)Termination reason: Instruction limit
% 18.38/6.21 % (3310694)Termination phase: Saturation
% 18.38/6.21 % (3310694)Time elapsed: 0.174 s
% 18.38/6.21 % (3310694)Peak memory usage: 91 MB
% 18.38/6.21 % (3310694)Instructions burned: 318 (million)
% 18.38/6.21 % (3310698)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1780338481:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2988 on theBenchmark for (2988ds/2836Mi)
% 18.38/6.21 % (3310699)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3157182338:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2987 on theBenchmark for (2987ds/14534Mi)
% 18.38/6.21 % (3310698)Instruction limit reached!
% 18.38/6.21 % (3310698)------------------------------
% 18.38/6.21 % (3310698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310698)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310698)Termination reason: Instruction limit
% 18.38/6.21 % (3310698)Termination phase: Saturation
% 18.38/6.21 % (3310698)Time elapsed: 0.878 s
% 18.38/6.21 % (3310698)Peak memory usage: 111 MB
% 18.38/6.21 % (3310698)Instructions burned: 2837 (million)
% 18.38/6.21 % (3310855)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=808310321:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/11832Mi)
% 18.38/6.21 % (3310674)Instruction limit reached!
% 18.38/6.21 % (3310674)------------------------------
% 18.38/6.21 % (3310674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310674)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310674)Termination reason: Instruction limit
% 18.38/6.21 % (3310674)Termination phase: Saturation
% 18.38/6.21 % (3310674)Time elapsed: 2.839 s
% 18.38/6.21 % (3310674)Peak memory usage: 167 MB
% 18.38/6.21 % (3310674)Instructions burned: 4949 (million)
% 18.38/6.21 % (3310857)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=130122392:i=2279:fgj=on:bd=all_2967 on theBenchmark for (2967ds/2279Mi)
% 18.38/6.21 % (3310857)Instruction limit reached!
% 18.38/6.21 % (3310857)------------------------------
% 18.38/6.21 % (3310857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.38/6.21 % (3310857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.38/6.21 % (3310857)CaDiCaL version: 2.1.3
% 18.38/6.21 % (3310857)Termination reason: Instruction limit
% 18.38/6.21 % (3310857)Termination phase: Saturation
% 18.38/6.21 % (3310857)Time elapsed: 1.329 s
% 18.38/6.21 % (3310857)Peak memory usage: 139 MB
% 18.38/6.21 % (3310857)Instructions burned: 2280 (million)
% 18.38/6.21 % (3310859)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=267040828:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2952 on theBenchmark for (2952ds/6225Mi)
% 18.38/6.21 % (3310855)First to succeed.
% 18.38/6.21 % (3310855)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3310606"
% 18.38/6.21 % (3310855)Refutation found. Thanks to Tanya!
% 18.38/6.21 % SZS status Unsatisfiable for theBenchmark
% 18.38/6.21 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/6.40 % (3310855)------------------------------
% 0.20/6.40 % (3310855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/6.40 % (3310855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/6.40 % (3310855)CaDiCaL version: 2.1.3
% 0.20/6.40 % (3310855)Termination reason: Refutation
% 0.20/6.40 % (3310855)Time elapsed: 2.900 s
% 0.20/6.40 % (3310855)Peak memory usage: 171 MB
% 0.20/6.40 % (3310855)Instructions burned: 8795 (million)
% 0.20/6.40 % (3310855)------------------------------
% 0.20/6.40 % (3310855)------------------------------
% 0.20/6.40 % (3310606)Success in time 5.348 s
% 0.20/6.40 % Vampire exiting
%------------------------------------------------------------------------------