%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:17:48 AM UTC 2026
% Result : Unsatisfiable 269.43s 38.68s
% Output : Refutation 269.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 2
% Syntax : Number of formulae : 154 ( 154 unt; 0 def)
% Number of atoms : 154 ( 153 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 23 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 510 ( 510 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f3,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X3)))),multiply(X2,inverse(X3))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f1,f1]) ).
fof(f4,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X2,
inference(superposition,[],[f1,f1]) ).
fof(f5,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X0)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f9,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(multiply(inverse(X0),X0))) = X0,
inference(superposition,[],[f4,f4]) ).
fof(f12,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X0)))),multiply(X3,inverse(X0)))),inverse(X0))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f1,f4]) ).
fof(f14,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(multiply(inverse(X3),multiply(inverse(X0),X0))))),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = X3,
inference(superposition,[],[f1,f4]) ).
fof(f74,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))),
inference(superposition,[],[f3,f3]) ).
fof(f79,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2))) = X1,
inference(superposition,[],[f1,f3]) ).
fof(f83,plain,
! [X2,X3,X0,X1,X4] : multiply(X4,inverse(multiply(inverse(X1),X2))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X4,inverse(X2)))))),inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(X2))))),
inference(superposition,[],[f1,f3]) ).
fof(f84,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),X2)))),multiply(X0,inverse(X2))) = X1,
inference(superposition,[],[f1,f3]) ).
fof(f120,plain,
! [X2,X3,X0,X1] : multiply(X2,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))),X3))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3))))),
inference(superposition,[],[f1,f84]) ).
fof(f144,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3))))) = multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,inverse(multiply(X2,inverse(X3))))),
inference(superposition,[],[f74,f84]) ).
fof(f213,plain,
! [X2,X0,X1,X6] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(multiply(X6,inverse(X2))),multiply(X6,inverse(X0))),
inference(superposition,[],[f144,f5]) ).
fof(f292,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(X3))) = multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),X2)))),multiply(X4,inverse(X2)))),inverse(X3))),
inference(superposition,[],[f213,f1]) ).
fof(f347,plain,
! [X2,X3,X0,X1,X4] : multiply(X4,inverse(X1)) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))))),multiply(X3,inverse(multiply(X4,inverse(X2)))))),inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(X2))))),
inference(superposition,[],[f1,f213]) ).
fof(f348,plain,
! [X2,X0,X1,X4] : multiply(X4,inverse(X1)) = multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2))),
inference(forward_demodulation,[],[f347,f120]) ).
fof(f422,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X4),X4)))))),inverse(multiply(inverse(inverse(multiply(inverse(X4),X4))),inverse(multiply(inverse(X4),X4)))))),inverse(multiply(inverse(X4),X4))),
inference(superposition,[],[f79,f348]) ).
fof(f465,plain,
! [X2,X3,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3) = X1,
inference(forward_demodulation,[],[f422,f79]) ).
fof(f592,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X2),X2)))),
inference(superposition,[],[f292,f1]) ).
fof(f668,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f592,f592]) ).
fof(f833,plain,
! [X2,X0] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),X2)))),X2) = X2,
inference(superposition,[],[f465,f668]) ).
fof(f882,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X0),X0)))),X2) = X2,
inference(superposition,[],[f833,f668]) ).
fof(f906,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X2),X2)))),X3) = X3,
inference(superposition,[],[f882,f882]) ).
fof(f931,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(X4),X4)))),inverse(X2))),inverse(X0)),
inference(superposition,[],[f213,f882]) ).
fof(f936,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(inverse(X2)),inverse(X0)),
inference(forward_demodulation,[],[f931,f882]) ).
fof(f944,plain,
! [X2,X3] : multiply(inverse(inverse(multiply(inverse(X2),X2))),X3) = X3,
inference(forward_demodulation,[],[f906,f882]) ).
fof(f950,plain,
! [X0,X1] : multiply(inverse(inverse(inverse(multiply(inverse(X0),X0)))),X1) = X1,
inference(superposition,[],[f944,f944]) ).
fof(f957,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = multiply(inverse(X1),X1),
inference(superposition,[],[f668,f944]) ).
fof(f958,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(inverse(multiply(inverse(X0),X0))))),X2) = X2,
inference(superposition,[],[f882,f944]) ).
fof(f1095,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = multiply(inverse(X1),X1),
inference(superposition,[],[f957,f944]) ).
fof(f1111,plain,
! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),X2) = X2,
inference(superposition,[],[f944,f957]) ).
fof(f1148,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(inverse(X3)),inverse(X2))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f213,f957]) ).
fof(f1152,plain,
! [X2,X3,X0] : multiply(inverse(inverse(X2)),inverse(X3)) = multiply(inverse(multiply(inverse(inverse(X3)),inverse(X2))),inverse(multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f1148,f936]) ).
fof(f1296,plain,
! [X0,X1] : multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),X1) = X1,
inference(superposition,[],[f944,f950]) ).
fof(f1297,plain,
! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(inverse(multiply(inverse(X0),X0)))),
inference(superposition,[],[f957,f950]) ).
fof(f1298,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = inverse(multiply(inverse(X1),X1)),
inference(superposition,[],[f957,f950]) ).
fof(f1401,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = inverse(inverse(multiply(inverse(X1),X1))),
inference(superposition,[],[f950,f1095]) ).
fof(f1414,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(inverse(X3)),inverse(X2))),inverse(inverse(multiply(inverse(X0),X0)))),
inference(superposition,[],[f213,f1095]) ).
fof(f1418,plain,
! [X2,X3,X0] : multiply(inverse(inverse(X2)),inverse(X3)) = multiply(inverse(multiply(inverse(inverse(X3)),inverse(X2))),inverse(inverse(multiply(inverse(X0),X0)))),
inference(forward_demodulation,[],[f1414,f936]) ).
fof(f1781,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(inverse(X3)),inverse(X2))),inverse(inverse(inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f213,f1297]) ).
fof(f1826,plain,
! [X2,X3,X0] : multiply(inverse(inverse(X2)),inverse(X3)) = multiply(inverse(multiply(inverse(inverse(X3)),inverse(X2))),inverse(inverse(inverse(multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f1781,f936]) ).
fof(f2377,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X4),X4)))))),inverse(multiply(inverse(X4),X4))))),
inference(superposition,[],[f348,f1298]) ).
fof(f2491,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(inverse(X0),X0))))),inverse(inverse(multiply(inverse(X4),X4))))),inverse(multiply(inverse(X4),X4))))),
inference(forward_demodulation,[],[f2377,f1111]) ).
fof(f2521,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X0),X0)))),inverse(inverse(multiply(inverse(X4),X4))))),inverse(multiply(inverse(X4),X4))))),
inference(forward_demodulation,[],[f2491,f936]) ).
fof(f2528,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(X2))),inverse(multiply(inverse(X4),X4))))),
inference(forward_demodulation,[],[f2521,f1418]) ).
fof(f2534,plain,
! [X2,X0,X1] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f2528,f1152]) ).
fof(f3007,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X4),X4)))))),inverse(multiply(inverse(X4),X4))))),
inference(superposition,[],[f348,f1401]) ).
fof(f3052,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X4),X4))))),
inference(forward_demodulation,[],[f3007,f2534]) ).
fof(f3108,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X4),X4))))),
inference(forward_demodulation,[],[f3052,f936]) ).
fof(f3116,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X0),X0)))),inverse(X2))),inverse(multiply(inverse(X4),X4))))),
inference(forward_demodulation,[],[f3108,f1152]) ).
fof(f3122,plain,
! [X2,X0,X1] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X0),X0)))))),
inference(forward_demodulation,[],[f3116,f1152]) ).
fof(f4195,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),
inference(superposition,[],[f12,f12]) ).
fof(f4318,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0))) = multiply(inverse(multiply(inverse(inverse(X0)),inverse(inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f12,f1111]) ).
fof(f4386,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))) = X5,
inference(superposition,[],[f14,f12]) ).
fof(f4388,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))) = X4,
inference(superposition,[],[f14,f12]) ).
fof(f4405,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = X4,
inference(forward_demodulation,[],[f4388,f1111]) ).
fof(f4407,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))) = X5,
inference(forward_demodulation,[],[f4386,f1111]) ).
fof(f4471,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0))) = multiply(inverse(inverse(inverse(multiply(inverse(X0),X0)))),inverse(X0)),
inference(forward_demodulation,[],[f4318,f1152]) ).
fof(f4589,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))),
inference(forward_demodulation,[],[f4195,f944]) ).
fof(f4608,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f4405,f2534]) ).
fof(f4610,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = X5,
inference(forward_demodulation,[],[f4407,f2534]) ).
fof(f4673,plain,
! [X2,X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0))),
inference(forward_demodulation,[],[f4471,f950]) ).
fof(f4791,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))),
inference(forward_demodulation,[],[f4589,f936]) ).
fof(f4810,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f4608,f944]) ).
fof(f4812,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f4610,f2534]) ).
fof(f4867,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0))),
inference(forward_demodulation,[],[f4673,f936]) ).
fof(f4984,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(inverse(inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),
inference(forward_demodulation,[],[f4791,f1826]) ).
fof(f5002,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f4810,f944]) ).
fof(f5004,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f4812,f2534]) ).
fof(f5172,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))))),
inference(forward_demodulation,[],[f4984,f1296]) ).
fof(f5190,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f5002,f936]) ).
fof(f5192,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5004,f944]) ).
fof(f5341,plain,
! [X2,X3,X0,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X2))),inverse(X2))),inverse(X2))))),
inference(forward_demodulation,[],[f5172,f936]) ).
fof(f5356,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(X2)))),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f5190,f1418]) ).
fof(f5358,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5192,f2534]) ).
fof(f5411,plain,
! [X2,X3,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(X2))),
inference(forward_demodulation,[],[f5341,f4867]) ).
fof(f5424,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(X2))),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f5356,f950]) ).
fof(f5426,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5358,f944]) ).
fof(f5445,plain,
! [X2,X5] : multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))) = multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2))),
inference(forward_demodulation,[],[f5411,f936]) ).
fof(f5458,plain,
! [X2,X0,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X2))),inverse(X2))),inverse(X2)))),inverse(X2))),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f5424,f936]) ).
fof(f5460,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5426,f936]) ).
fof(f5475,plain,
! [X2,X5] : multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2))) = multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),
inference(forward_demodulation,[],[f5445,f2534]) ).
fof(f5481,plain,
! [X2,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(X2))),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f5458,f4867]) ).
fof(f5483,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(inverse(inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5460,f1826]) ).
fof(f5493,plain,
! [X2,X5] : multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2))) = multiply(inverse(multiply(inverse(multiply(X5,inverse(inverse(inverse(multiply(inverse(X2),X2)))))),multiply(X5,inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))))),inverse(inverse(multiply(inverse(X2),X2)))),
inference(forward_demodulation,[],[f5475,f3122]) ).
fof(f5499,plain,
! [X2,X4] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X4,
inference(forward_demodulation,[],[f5481,f958]) ).
fof(f5501,plain,
! [X2,X3,X0,X1,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5483,f1296]) ).
fof(f5510,plain,
! [X2] : multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2))) = multiply(inverse(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(X2),X2)))),
inference(forward_demodulation,[],[f5493,f936]) ).
fof(f5514,plain,
! [X2,X4] : multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2))))) = X4,
inference(forward_demodulation,[],[f5499,f1152]) ).
fof(f5516,plain,
! [X2,X3,X0,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X2))),inverse(X2))),inverse(X2)))))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5501,f936]) ).
fof(f5521,plain,
! [X2] : multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2))) = multiply(inverse(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))),
inference(forward_demodulation,[],[f5510,f1418]) ).
fof(f5525,plain,
! [X2,X4] : inverse(multiply(inverse(X4),inverse(multiply(inverse(X2),X2)))) = X4,
inference(forward_demodulation,[],[f5514,f944]) ).
fof(f5526,plain,
! [X2,X3,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(X2)))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5516,f4867]) ).
fof(f5529,plain,
! [X2] : inverse(inverse(inverse(multiply(inverse(X2),X2)))) = multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2))),
inference(forward_demodulation,[],[f5521,f950]) ).
fof(f5532,plain,
! [X2,X3,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(X2)))),inverse(multiply(inverse(X5),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5526,f5525]) ).
fof(f5535,plain,
! [X2,X3,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(X2)))),X5),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5532,f5525]) ).
fof(f5537,plain,
! [X2,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(inverse(X2),X2))))),inverse(inverse(X2)))),X5),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5535,f936]) ).
fof(f5539,plain,
! [X2,X5] : multiply(multiply(inverse(inverse(inverse(inverse(multiply(inverse(X2),X2))))),X5),inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5537,f5529]) ).
fof(f5541,plain,
! [X2,X5] : multiply(X5,inverse(multiply(inverse(X2),X2))) = X5,
inference(forward_demodulation,[],[f5539,f1296]) ).
fof(f5575,plain,
! [X0,X1] : multiply(X1,inverse(inverse(multiply(inverse(X0),X0)))) = X1,
inference(superposition,[],[f5541,f1298]) ).
fof(f5578,plain,
! [X0,X1] : multiply(X1,multiply(inverse(X0),X0)) = X1,
inference(superposition,[],[f5541,f957]) ).
fof(f5615,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(X0)))) = X0,
inference(superposition,[],[f9,f5541]) ).
fof(f5694,plain,
! [X0,X1] : inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0)))),inverse(X0)))),inverse(X0)))) = X0,
inference(forward_demodulation,[],[f5615,f936]) ).
fof(f5750,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(X0)))) = X0,
inference(forward_demodulation,[],[f5694,f4867]) ).
fof(f5783,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(inverse(inverse(X0)),inverse(X0)))) = X0,
inference(forward_demodulation,[],[f5750,f5578]) ).
fof(f5808,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f5783,f5578]) ).
fof(f6060,plain,
! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1,
inference(superposition,[],[f5578,f5808]) ).
fof(f6101,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),inverse(inverse(X0)))),X3)),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))) = X0,
inference(superposition,[],[f14,f5578]) ).
fof(f6168,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),inverse(inverse(X0)))),X3)) = X0,
inference(forward_demodulation,[],[f6101,f5541]) ).
fof(f6201,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),X0)),X3)) = X0,
inference(forward_demodulation,[],[f6168,f5808]) ).
fof(f6218,plain,
! [X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X3))),inverse(X3))),inverse(X3)))),X0)),X3)) = X0,
inference(forward_demodulation,[],[f6201,f936]) ).
fof(f6232,plain,
! [X3,X0] : inverse(multiply(inverse(multiply(inverse(inverse(X3)),X0)),X3)) = X0,
inference(forward_demodulation,[],[f6218,f4867]) ).
fof(f6243,plain,
! [X3,X0] : inverse(multiply(inverse(multiply(X3,X0)),X3)) = X0,
inference(forward_demodulation,[],[f6232,f5808]) ).
fof(f9765,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(X1,X0)))) = X1,
inference(superposition,[],[f6243,f6243]) ).
fof(f9835,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,X0)),X1),
inference(superposition,[],[f5808,f6243]) ).
fof(f10180,plain,
! [X0,X1] : inverse(X0) = multiply(X1,inverse(multiply(X0,X1))),
inference(superposition,[],[f5808,f9765]) ).
fof(f11103,plain,
! [X2,X3,X0,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1)),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),
inference(superposition,[],[f10180,f12]) ).
fof(f11140,plain,
! [X2,X0,X1] : multiply(X2,inverse(X1)) = inverse(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))))),
inference(superposition,[],[f348,f10180]) ).
fof(f11191,plain,
! [X2,X0,X1] : multiply(X2,inverse(X1)) = multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))),
inference(forward_demodulation,[],[f11140,f5808]) ).
fof(f11208,plain,
! [X2,X3,X0,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1)),multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),
inference(forward_demodulation,[],[f11103,f5525]) ).
fof(f11240,plain,
! [X2,X0,X1] : multiply(X2,inverse(X1)) = inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))),
inference(forward_demodulation,[],[f11191,f5541]) ).
fof(f11246,plain,
! [X2,X3,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1)),multiply(inverse(inverse(X1)),inverse(inverse(multiply(inverse(X1),X1))))),
inference(forward_demodulation,[],[f11208,f936]) ).
fof(f11267,plain,
! [X2,X1] : multiply(X2,inverse(X1)) = inverse(multiply(inverse(inverse(X1)),inverse(X2))),
inference(forward_demodulation,[],[f11240,f936]) ).
fof(f11271,plain,
! [X2,X3,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1)),inverse(inverse(X1))),
inference(forward_demodulation,[],[f11246,f5575]) ).
fof(f11287,plain,
! [X2,X1] : multiply(X2,inverse(X1)) = inverse(multiply(X1,inverse(X2))),
inference(forward_demodulation,[],[f11267,f5808]) ).
fof(f11289,plain,
! [X2,X3,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1)),X1),
inference(forward_demodulation,[],[f11271,f5808]) ).
fof(f11303,plain,
! [X2,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X1))),inverse(X1))),inverse(X1)),X1),
inference(forward_demodulation,[],[f11289,f936]) ).
fof(f11315,plain,
! [X2,X1] : inverse(inverse(X2)) = multiply(multiply(multiply(X1,inverse(inverse(inverse(multiply(inverse(X2),X1))))),inverse(X1)),X1),
inference(forward_demodulation,[],[f11303,f11287]) ).
fof(f11326,plain,
! [X2,X1] : inverse(inverse(X2)) = multiply(multiply(multiply(X1,inverse(multiply(inverse(X2),X1))),inverse(X1)),X1),
inference(forward_demodulation,[],[f11315,f5808]) ).
fof(f11334,plain,
! [X2,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(inverse(X2)),inverse(X1)),X1),
inference(forward_demodulation,[],[f11326,f10180]) ).
fof(f11339,plain,
! [X2,X1] : multiply(multiply(X2,inverse(X1)),X1) = X2,
inference(forward_demodulation,[],[f11334,f5808]) ).
fof(f11358,plain,
! [X0,X1] : multiply(multiply(X1,X0),inverse(X0)) = X1,
inference(superposition,[],[f11339,f5808]) ).
fof(f11360,plain,
! [X0,X1] : multiply(inverse(X0),X1) = inverse(multiply(inverse(X1),X0)),
inference(superposition,[],[f11339,f9835]) ).
fof(f11660,plain,
! [X0,X1] : multiply(inverse(X1),inverse(X0)) = inverse(multiply(X0,X1)),
inference(superposition,[],[f10180,f11358]) ).
fof(f23252,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(inverse(X0),X1))) = multiply(multiply(inverse(X1),X0),inverse(X2)),
inference(superposition,[],[f11287,f11360]) ).
fof(f61330,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0))))))))),multiply(X3,inverse(multiply(X1,X0))))),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))),
inference(superposition,[],[f83,f5808]) ).
fof(f61591,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = inverse(multiply(multiply(inverse(multiply(X1,X0)),multiply(X1,X0)),multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0))))))))),multiply(X3,inverse(multiply(X1,X0)))))),
inference(forward_demodulation,[],[f61330,f11660]) ).
fof(f62105,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(inverse(multiply(X3,inverse(multiply(X1,X0)))),multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0))))))))),inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))),
inference(forward_demodulation,[],[f61591,f23252]) ).
fof(f62618,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(inverse(multiply(X3,inverse(multiply(X1,X0)))),multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0))))))))),
inference(forward_demodulation,[],[f62105,f5541]) ).
fof(f63131,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(inverse(inverse(multiply(X1,X0))),inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0)))))))),
inference(forward_demodulation,[],[f62618,f936]) ).
fof(f63632,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = inverse(multiply(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0)))))),inverse(multiply(X1,X0)))),
inference(forward_demodulation,[],[f63131,f11660]) ).
fof(f64133,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(multiply(X0,inverse(X0)))))))),
inference(forward_demodulation,[],[f63632,f11287]) ).
fof(f64634,plain,
! [X2,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(X0,inverse(X0))))))),
inference(forward_demodulation,[],[f64133,f5525]) ).
fof(f65135,plain,
! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),multiply(inverse(inverse(X2)),inverse(inverse(multiply(X0,inverse(X0)))))),
inference(forward_demodulation,[],[f64634,f936]) ).
fof(f65635,plain,
! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),inverse(multiply(inverse(multiply(X0,inverse(X0))),inverse(X2)))),
inference(forward_demodulation,[],[f65135,f11660]) ).
fof(f66130,plain,
! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),multiply(inverse(inverse(X2)),multiply(X0,inverse(X0)))),
inference(forward_demodulation,[],[f65635,f11360]) ).
fof(f66582,plain,
! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),inverse(inverse(X2))),
inference(forward_demodulation,[],[f66130,f6060]) ).
fof(f67019,plain,
! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),inverse(X0)))) = multiply(multiply(X1,X0),X2),
inference(forward_demodulation,[],[f66582,f5808]) ).
fof(f67401,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),X2) = multiply(X1,multiply(inverse(inverse(X0)),X2)),
inference(forward_demodulation,[],[f67019,f11360]) ).
fof(f67677,plain,
! [X2,X0,X1] : multiply(X1,multiply(X0,X2)) = multiply(multiply(X1,X0),X2),
inference(forward_demodulation,[],[f67401,f5808]) ).
fof(f69750,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(superposition,[],[f2,f67677]) ).
fof(f69828,plain,
$false,
inference(trivial_inequality_removal,[],[f69750]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n010.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:04:31 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.16/4.48 % (718080)Will run a generic schedule for satisfiability detection.
% 28.16/4.48 % (718089)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1908824773_2999 on theBenchmark for (2999ds/0Mi)
% 28.16/4.48 % TRYING [1]
% 28.16/4.48 % TRYING [2]
% 28.16/4.48 % TRYING [3]
% 28.16/4.48 % (718090)% WARNING: option uhcvi not known.
% 28.16/4.48 % (718090)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4158452582:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 28.16/4.48 % (718092)dis+10_1_sil=32000:sp=arity:random_seed=3005681003:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 28.16/4.48 % (718093)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3303850744:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 28.16/4.48 % (718094)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3059475072:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 28.16/4.48 % (718095)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1063529361:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 28.16/4.48 % TRYING [4]
% 28.16/4.48 % (718091)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3298533060:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 28.16/4.48 % (718092)Instruction limit reached!
% 28.16/4.48 % (718092)------------------------------
% 28.16/4.48 % (718092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.16/4.48 % (718092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/4.48 % (718092)CaDiCaL version: 2.1.3
% 28.16/4.48 % (718092)Termination reason: Instruction limit
% 28.16/4.48 % (718092)Termination phase: Saturation
% 28.16/4.48 % (718092)Time elapsed: 0.056 s
% 28.16/4.48 % (718092)Peak memory usage: 11 MB
% 28.16/4.48 % (718092)Instructions burned: 104 (million)
% 28.16/4.48 % (718093)Instruction limit reached!
% 28.16/4.48 % (718093)------------------------------
% 28.16/4.48 % (718093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.16/4.48 % (718093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/4.48 % (718093)CaDiCaL version: 2.1.3
% 28.16/4.48 % (718093)Termination reason: Instruction limit
% 28.16/4.48 % (718093)Termination phase: Saturation
% 28.16/4.48 % (718093)Time elapsed: 0.066 s
% 28.16/4.48 % (718093)Peak memory usage: 12 MB
% 28.16/4.48 % (718093)Instructions burned: 116 (million)
% 28.16/4.48 % (718094)Instruction limit reached!
% 28.16/4.48 % (718094)------------------------------
% 28.16/4.48 % (718094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.16/4.48 % (718094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/4.48 % (718094)CaDiCaL version: 2.1.3
% 28.16/4.48 % (718094)Termination reason: Instruction limit
% 28.16/4.48 % (718094)Termination phase: Saturation
% 28.16/4.48 % (718094)Time elapsed: 0.074 s
% 28.16/4.48 % (718094)Peak memory usage: 13 MB
% 28.16/4.48 % (718094)Instructions burned: 131 (million)
% 28.16/4.48 % (718114)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3733724470:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 28.16/4.48 % TRYING [1]
% 28.16/4.48 % TRYING [2]
% 28.16/4.48 % TRYING [3]
% 28.16/4.48 % (718115)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1139877773:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 28.16/4.48 % (718116)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=711669219:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 28.16/4.48 % (718095)Instruction limit reached!
% 28.16/4.48 % (718095)------------------------------
% 28.16/4.48 % (718095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.16/4.48 % (718095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.16/4.48 % (718095)CaDiCaL version: 2.1.3
% 28.16/4.48 % (718095)Termination reason: Instruction limit
% 28.16/4.48 % (718095)Termination phase: Saturation
% 28.16/4.48 % (718095)Time elapsed: 0.098 s
% 28.16/4.48 % (718095)Peak memory usage: 12 MB
% 28.16/4.48 % (718095)Instructions burned: 159 (million)
% 28.16/4.48 % TRYING [4]
% 28.16/4.48 % (718120)ott-21_1_sil=16000:fs=off:random_seed=3300049051:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 28.16/4.48 % (718115)Instruction limit reached!
% 28.16/4.48 % (718115)------------------------------
% 28.16/4.48 % (718115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.16/4.48 % (718115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718115)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718115)Termination reason: Instruction limit
% 54.63/8.18 % (718115)Termination phase: Saturation
% 54.63/8.18 % (718115)Time elapsed: 0.073 s
% 54.63/8.18 % (718115)Peak memory usage: 12 MB
% 54.63/8.18 % (718115)Instructions burned: 132 (million)
% 54.63/8.18 % (718122)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3200885984:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 54.63/8.18 % (718120)Instruction limit reached!
% 54.63/8.18 % (718120)------------------------------
% 54.63/8.18 % (718120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.63/8.18 % (718120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718120)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718120)Termination reason: Instruction limit
% 54.63/8.18 % (718120)Termination phase: Saturation
% 54.63/8.18 % (718120)Time elapsed: 0.089 s
% 54.63/8.18 % (718120)Peak memory usage: 11 MB
% 54.63/8.18 % (718120)Instructions burned: 182 (million)
% 54.63/8.18 % (718124)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2648100990:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 54.63/8.18 % TRYING [1]
% 54.63/8.18 % TRYING [2]
% 54.63/8.18 % TRYING [3]
% 54.63/8.18 % TRYING [4]
% 54.63/8.18 % (718122)Instruction limit reached!
% 54.63/8.18 % (718122)------------------------------
% 54.63/8.18 % (718122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.63/8.18 % (718122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718122)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718122)Termination reason: Instruction limit
% 54.63/8.18 % (718122)Termination phase: Saturation
% 54.63/8.18 % (718122)Time elapsed: 0.235 s
% 54.63/8.18 % (718122)Peak memory usage: 14 MB
% 54.63/8.18 % (718122)Instructions burned: 477 (million)
% 54.63/8.18 % (718116)Instruction limit reached!
% 54.63/8.18 % (718116)------------------------------
% 54.63/8.18 % (718116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.63/8.18 % (718116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718116)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718116)Termination reason: Instruction limit
% 54.63/8.18 % (718116)Termination phase: Saturation
% 54.63/8.18 % (718116)Time elapsed: 0.325 s
% 54.63/8.18 % (718116)Peak memory usage: 16 MB
% 54.63/8.18 % (718116)Instructions burned: 686 (million)
% 54.63/8.18 % (718139)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2638964516:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 54.63/8.18 % (718140)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2547625296:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 54.63/8.18 % TRYING [14]
% 54.63/8.18 % (718114)Instruction limit reached!
% 54.63/8.18 % (718114)------------------------------
% 54.63/8.18 % (718114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.63/8.18 % (718114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718114)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718114)Termination reason: Instruction limit
% 54.63/8.18 % (718114)Termination phase: Finite model building SAT solving
% 54.63/8.18 % (718114)Time elapsed: 0.421 s
% 54.63/8.18 % (718114)Peak memory usage: 12 MB
% 54.63/8.18 % (718114)Instructions burned: 714 (million)
% 54.63/8.18 % (718143)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1773527548:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 54.63/8.18 % (718140)Instruction limit reached!
% 54.63/8.18 % (718140)------------------------------
% 54.63/8.18 % (718140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.63/8.18 % (718140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718140)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718140)Termination reason: Instruction limit
% 54.63/8.18 % (718140)Termination phase: Finite model building constraint generation
% 54.63/8.18 % (718140)Time elapsed: 0.321 s
% 54.63/8.18 % (718140)Peak memory usage: 81 MB
% 54.63/8.18 % (718140)Instructions burned: 892 (million)
% 54.63/8.18 % (718124)Instruction limit reached!
% 54.63/8.18 % (718124)------------------------------
% 54.63/8.18 % (718124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.63/8.18 % (718124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.63/8.18 % (718124)CaDiCaL version: 2.1.3
% 54.63/8.18 % (718124)Termination reason: Instruction limit
% 143.77/20.73 % (718124)Termination phase: Finite model building SAT solving
% 143.77/20.73 % (718124)Time elapsed: 0.568 s
% 143.77/20.73 % (718124)Peak memory usage: 12 MB
% 143.77/20.73 % (718124)Instructions burned: 865 (million)
% 143.77/20.73 % (718145)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3678883649:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 143.77/20.73 % (718154)fmb+10_1_sil=64000:random_seed=1600933116:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 143.77/20.73 % TRYING [1]
% 143.77/20.73 % TRYING [2]
% 143.77/20.73 % TRYING [3]
% 143.77/20.73 % TRYING [4]
% 143.77/20.73 % (718143)Instruction limit reached!
% 143.77/20.73 % (718143)------------------------------
% 143.77/20.73 % (718143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.77/20.73 % (718143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.77/20.73 % (718143)CaDiCaL version: 2.1.3
% 143.77/20.73 % (718143)Termination reason: Instruction limit
% 143.77/20.73 % (718143)Termination phase: Saturation
% 143.77/20.73 % (718143)Time elapsed: 0.407 s
% 143.77/20.73 % (718143)Peak memory usage: 17 MB
% 143.77/20.73 % (718143)Instructions burned: 692 (million)
% 143.77/20.73 % (718158)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3714451737:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 143.77/20.73 % TRYING [20]
% 143.77/20.73 % (718139)Instruction limit reached!
% 143.77/20.73 % (718139)------------------------------
% 143.77/20.73 % (718139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.77/20.73 % (718139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.77/20.73 % (718139)CaDiCaL version: 2.1.3
% 143.77/20.73 % (718139)Termination reason: Instruction limit
% 143.77/20.73 % (718139)Termination phase: Saturation
% 143.77/20.73 % (718139)Time elapsed: 0.822 s
% 143.77/20.73 % (718139)Peak memory usage: 24 MB
% 143.77/20.73 % (718139)Instructions burned: 1179 (million)
% 143.77/20.73 % (718169)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1414271418:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 143.77/20.73 % TRYING [8]
% 143.77/20.73 % TRYING [5]
% 143.77/20.73 % (718145)Instruction limit reached!
% 143.77/20.73 % (718145)------------------------------
% 143.77/20.73 % (718145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.77/20.73 % (718145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.77/20.73 % (718145)CaDiCaL version: 2.1.3
% 143.77/20.73 % (718145)Termination reason: Instruction limit
% 143.77/20.73 % (718145)Termination phase: Saturation
% 143.77/20.73 % (718145)Time elapsed: 0.677 s
% 143.77/20.73 % (718145)Peak memory usage: 15 MB
% 143.77/20.73 % (718145)Instructions burned: 879 (million)
% 143.77/20.73 % (718174)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3743544369:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 143.77/20.73 % (718169)Instruction limit reached!
% 143.77/20.73 % (718169)------------------------------
% 143.77/20.73 % (718169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.77/20.73 % (718169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.77/20.73 % (718169)CaDiCaL version: 2.1.3
% 143.77/20.73 % (718169)Termination reason: Instruction limit
% 143.77/20.73 % (718169)Termination phase: Finite model building SAT solving
% 143.77/20.73 % (718169)Time elapsed: 0.522 s
% 143.77/20.73 % (718169)Peak memory usage: 40 MB
% 143.77/20.73 % (718169)Instructions burned: 921 (million)
% 143.77/20.73 % (718177)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=916524445:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 143.77/20.73 % (718177)Instruction limit reached!
% 143.77/20.73 % (718177)------------------------------
% 143.77/20.73 % (718177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.77/20.73 % (718177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.77/20.73 % (718177)CaDiCaL version: 2.1.3
% 143.77/20.73 % (718177)Termination reason: Instruction limit
% 143.77/20.73 % (718177)Termination phase: Saturation
% 143.77/20.73 % (718177)Time elapsed: 0.717 s
% 143.77/20.73 % (718177)Peak memory usage: 28 MB
% 143.77/20.73 % (718177)Instructions burned: 1474 (million)
% 143.77/20.73 % (718331)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=705174874:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 143.77/20.73 % TRYING [77]
% 143.77/20.73 % (718174)Instruction limit reached!
% 143.77/20.73 % (718174)------------------------------
% 143.77/20.73 % (718174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 143.77/20.73 % (718174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718174)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718174)Termination reason: Instruction limit
% 269.43/38.68 % (718174)Termination phase: Saturation
% 269.43/38.68 % (718174)Time elapsed: 2.522 s
% 269.43/38.68 % (718174)Peak memory usage: 43 MB
% 269.43/38.68 % (718174)Instructions burned: 5131 (million)
% 269.43/38.68 % (718333)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3396821318:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 269.43/38.68 % TRYING [16]
% 269.43/38.68 % (718333)Instruction limit reached!
% 269.43/38.68 % (718333)------------------------------
% 269.43/38.68 % (718333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718333)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718333)Termination reason: Instruction limit
% 269.43/38.68 % (718333)Termination phase: Finite model building constraint generation
% 269.43/38.68 % (718333)Time elapsed: 0.728 s
% 269.43/38.68 % (718333)Peak memory usage: 132 MB
% 269.43/38.68 % (718333)Instructions burned: 2175 (million)
% 269.43/38.68 % (718158)Instruction limit reached!
% 269.43/38.68 % (718158)------------------------------
% 269.43/38.68 % (718158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718158)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718158)Termination reason: Instruction limit
% 269.43/38.68 % (718158)Termination phase: Finite model building constraint generation
% 269.43/38.68 % (718158)Time elapsed: 3.821 s
% 269.43/38.68 % (718158)Peak memory usage: 644 MB
% 269.43/38.68 % (718158)Instructions burned: 9516 (million)
% 269.43/38.68 % (718335)ott-2_1_sil=16000:newcnf=on:random_seed=3736556332:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 269.43/38.68 % (718337)ott+10_1_sil=32000:tgt=ground:random_seed=4175690583:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 269.43/38.68 % (718331)Instruction limit reached!
% 269.43/38.68 % (718331)------------------------------
% 269.43/38.68 % (718331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718331)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718331)Termination reason: Instruction limit
% 269.43/38.68 % (718331)Termination phase: Finite model building constraint generation
% 269.43/38.68 % (718331)Time elapsed: 2.382 s
% 269.43/38.68 % (718331)Peak memory usage: 522 MB
% 269.43/38.68 % (718331)Instructions burned: 6327 (million)
% 269.43/38.68 % (718339)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2356428622:i=54282_2949 on theBenchmark for (2949ds/54282Mi)
% 269.43/38.68 % TRYING [1]
% 269.43/38.68 % TRYING [2]
% 269.43/38.68 % TRYING [3]
% 269.43/38.68 % TRYING [4]
% 269.43/38.68 % (718335)Instruction limit reached!
% 269.43/38.68 % (718335)------------------------------
% 269.43/38.68 % (718335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718335)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718335)Termination reason: Instruction limit
% 269.43/38.68 % (718335)Termination phase: Saturation
% 269.43/38.68 % (718335)Time elapsed: 0.469 s
% 269.43/38.68 % (718335)Peak memory usage: 20 MB
% 269.43/38.68 % (718335)Instructions burned: 870 (million)
% 269.43/38.68 % (718341)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3638349782:i=3512:aac=none_2946 on theBenchmark for (2946ds/3512Mi)
% 269.43/38.68 % (718341)Instruction limit reached!
% 269.43/38.68 % (718341)------------------------------
% 269.43/38.68 % (718341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718341)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718341)Termination reason: Instruction limit
% 269.43/38.68 % (718341)Termination phase: Saturation
% 269.43/38.68 % (718341)Time elapsed: 1.689 s
% 269.43/38.68 % (718341)Peak memory usage: 28 MB
% 269.43/38.68 % (718341)Instructions burned: 3512 (million)
% 269.43/38.68 % (718343)dis+21_1_sil=32000:sas=cadical:random_seed=2477732646:i=3773:amm=off_2929 on theBenchmark for (2929ds/3773Mi)
% 269.43/38.68 % TRYING [5]
% 269.43/38.68 % TRYING [5]
% 269.43/38.68 % (718337)Instruction limit reached!
% 269.43/38.68 % (718337)------------------------------
% 269.43/38.68 % (718337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718337)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718337)Termination reason: Instruction limit
% 269.43/38.68 % (718337)Termination phase: Saturation
% 269.43/38.68 % (718337)Time elapsed: 2.835 s
% 269.43/38.68 % (718337)Peak memory usage: 58 MB
% 269.43/38.68 % (718337)Instructions burned: 5115 (million)
% 269.43/38.68 % (718345)ott+11_1_sil=16000:gs=on:random_seed=505812940:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2922 on theBenchmark for (2922ds/2251Mi)
% 269.43/38.68 % (718343)Instruction limit reached!
% 269.43/38.68 % (718343)------------------------------
% 269.43/38.68 % (718343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718343)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718343)Termination reason: Instruction limit
% 269.43/38.68 % (718343)Termination phase: Saturation
% 269.43/38.68 % (718343)Time elapsed: 1.818 s
% 269.43/38.68 % (718343)Peak memory usage: 30 MB
% 269.43/38.68 % (718343)Instructions burned: 3774 (million)
% 269.43/38.68 % (718347)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=259461527:fmbsr=1.6:i=67534_2911 on theBenchmark for (2911ds/67534Mi)
% 269.43/38.68 % TRYING [7]
% 269.43/38.68 % (718345)Instruction limit reached!
% 269.43/38.68 % (718345)------------------------------
% 269.43/38.68 % (718345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718345)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718345)Termination reason: Instruction limit
% 269.43/38.68 % (718345)Termination phase: Saturation
% 269.43/38.68 % (718345)Time elapsed: 1.136 s
% 269.43/38.68 % (718345)Peak memory usage: 29 MB
% 269.43/38.68 % (718345)Instructions burned: 2251 (million)
% 269.43/38.68 % (718349)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1577568613:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2910 on theBenchmark for (2910ds/4591Mi)
% 269.43/38.68 % (718349)Instruction limit reached!
% 269.43/38.68 % (718349)------------------------------
% 269.43/38.68 % (718349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718349)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718349)Termination reason: Instruction limit
% 269.43/38.68 % (718349)Termination phase: Saturation
% 269.43/38.68 % (718349)Time elapsed: 1.845 s
% 269.43/38.68 % (718349)Peak memory usage: 34 MB
% 269.43/38.68 % (718349)Instructions burned: 4591 (million)
% 269.43/38.68 % (718351)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2530172504:i=29340_2892 on theBenchmark for (2892ds/29340Mi)
% 269.43/38.68 % (718154)Instruction limit reached!
% 269.43/38.68 % (718154)------------------------------
% 269.43/38.68 % (718154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718154)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718154)Termination reason: Instruction limit
% 269.43/38.68 % (718154)Termination phase: Finite model building SAT solving
% 269.43/38.68 % (718154)Time elapsed: 14.331 s
% 269.43/38.68 % (718154)Peak memory usage: 17 MB
% 269.43/38.68 % (718154)Instructions burned: 22062 (million)
% 269.43/38.68 % (718608)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2339501538:i=5211_2847 on theBenchmark for (2847ds/5211Mi)
% 269.43/38.68 % (718608)Instruction limit reached!
% 269.43/38.68 % (718608)------------------------------
% 269.43/38.68 % (718608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718608)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718608)Termination reason: Instruction limit
% 269.43/38.68 % (718608)Termination phase: Saturation
% 269.43/38.68 % (718608)Time elapsed: 2.920 s
% 269.43/38.68 % (718608)Peak memory usage: 35 MB
% 269.43/38.68 % (718608)Instructions burned: 5213 (million)
% 269.43/38.68 % (718772)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4188223471:i=5497:nm=2_2818 on theBenchmark for (2818ds/5497Mi)
% 269.43/38.68 % TRYING [17]
% 269.43/38.68 % (718772)Instruction limit reached!
% 269.43/38.68 % (718772)------------------------------
% 269.43/38.68 % (718772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718772)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718772)Termination reason: Instruction limit
% 269.43/38.68 % (718772)Termination phase: Finite model building constraint generation
% 269.43/38.68 % (718772)Time elapsed: 2.115 s
% 269.43/38.68 % (718772)Peak memory usage: 386 MB
% 269.43/38.68 % (718772)Instructions burned: 5497 (million)
% 269.43/38.68 % (718774)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1564321321:fmbsr=2:i=46332_2796 on theBenchmark for (2796ds/46332Mi)
% 269.43/38.68 % TRYING [15]
% 269.43/38.68 % (718091)Instruction limit reached!
% 269.43/38.68 % (718091)------------------------------
% 269.43/38.68 % (718091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718091)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718091)Termination reason: Instruction limit
% 269.43/38.68 % (718091)Termination phase: Saturation
% 269.43/38.68 % (718091)Time elapsed: 24.921 s
% 269.43/38.68 % (718091)Peak memory usage: 93 MB
% 269.43/38.68 % (718091)Instructions burned: 88025 (million)
% 269.43/38.68 % (718776)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1375417177:i=14071_2750 on theBenchmark for (2750ds/14071Mi)
% 269.43/38.68 % TRYING [12]
% 269.43/38.68 % (718351)Instruction limit reached!
% 269.43/38.68 % (718351)------------------------------
% 269.43/38.68 % (718351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718351)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718351)Termination reason: Instruction limit
% 269.43/38.68 % (718351)Termination phase: Saturation
% 269.43/38.68 % (718351)Time elapsed: 14.202 s
% 269.43/38.68 % (718351)Peak memory usage: 160 MB
% 269.43/38.68 % (718351)Instructions burned: 29341 (million)
% 269.43/38.68 % (718778)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=755336918:i=22565:add=on:rawr=on_2749 on theBenchmark for (2749ds/22565Mi)
% 269.43/38.68 % (718778)Instruction limit reached!
% 269.43/38.68 % (718778)------------------------------
% 269.43/38.68 % (718778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718778)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718778)Termination reason: Instruction limit
% 269.43/38.68 % (718778)Termination phase: Saturation
% 269.43/38.68 % (718778)Time elapsed: 7.158 s
% 269.43/38.68 % (718778)Peak memory usage: 49 MB
% 269.43/38.68 % (718778)Instructions burned: 22566 (million)
% 269.43/38.68 % (719043)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1478220078:i=8173:av=off_2677 on theBenchmark for (2677ds/8173Mi)
% 269.43/38.68 % (718776)Instruction limit reached!
% 269.43/38.68 % (718776)------------------------------
% 269.43/38.68 % (718776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (718776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (718776)CaDiCaL version: 2.1.3
% 269.43/38.68 % (718776)Termination reason: Instruction limit
% 269.43/38.68 % (718776)Termination phase: Finite model building SAT solving
% 269.43/38.68 % (718776)Time elapsed: 8.777 s
% 269.43/38.68 % (718776)Peak memory usage: 200 MB
% 269.43/38.68 % (718776)Instructions burned: 14073 (million)
% 269.43/38.68 % (719199)dis+10_16:1_sil=16000:random_seed=1416949336:i=9155:fsr=off_2661 on theBenchmark for (2661ds/9155Mi)
% 269.43/38.68 % (719043)Instruction limit reached!
% 269.43/38.68 % (719043)------------------------------
% 269.43/38.68 % (719043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (719043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (719043)CaDiCaL version: 2.1.3
% 269.43/38.68 % (719043)Termination reason: Instruction limit
% 269.43/38.68 % (719043)Termination phase: Saturation
% 269.43/38.68 % (719043)Time elapsed: 4.543 s
% 269.43/38.68 % (719043)Peak memory usage: 77 MB
% 269.43/38.68 % (719043)Instructions burned: 8174 (million)
% 269.43/38.68 % (719201)ott-3_8_sil=64000:random_seed=2354179863:i=20139:bs=on_2631 on theBenchmark for (2631ds/20139Mi)
% 269.43/38.68 % (719201) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-718080-719201"...
% 269.43/38.68 % (719201)...printing done.
% 269.43/38.68 % (719201)Refutation found. Thanks to Tanya!
% 269.43/38.68 % SZS status Unsatisfiable for theBenchmark
% 269.43/38.68 % SZS output start Proof for theBenchmark
% See solution above
% 269.43/38.68 % (719201)------------------------------
% 269.43/38.68 % (719201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 269.43/38.68 % (719201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 269.43/38.68 % (719201)CaDiCaL version: 2.1.3
% 269.43/38.68 % (719201)Termination reason: Refutation
% 269.43/38.68 % (719201)Time elapsed: 1.344 s
% 269.43/38.68 % (719201)Peak memory usage: 32 MB
% 269.43/38.68 % (719201)Instructions burned: 2413 (million)
% 269.43/38.68 % (718080)Success in time 38.253 s
% 269.43/38.68 % Vampire exiting
%------------------------------------------------------------------------------