%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP119-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Thu Sep 24 12:32:33 PM UTC 2026
% Result : Unsatisfiable 19.04s 12.83s
% Output : CNFRefutation 19.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 3
% Syntax : Number of formulae : 182 ( 182 unt; 0 def)
% Number of atoms : 182 ( 181 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 298 ( 298 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Y,X,Z] : multiply(Y,multiply(multiply(Y,multiply(multiply(Y,Y),multiply(X,Z))),multiply(Z,multiply(Z,Z)))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
multiply(identity,identity) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
multiply(a,multiply(a,multiply(a,a))) != identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2)))) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
multiply(identity,identity) = identity,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f6,plain,
multiply(a,multiply(a,multiply(a,a))) != identity,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f11,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f12,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1)))) = X0,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f13,plain,
! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,multiply(identity,identity)))) = identity,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f15,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),multiply(identity,identity))) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f16,plain,
! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,identity))) = identity,
inference(forward_demodulation,[status(thm)],[f5,f13]) ).
fof(f17,plain,
! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)) = identity,
inference(forward_demodulation,[status(thm)],[f5,f16]) ).
fof(f18,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f15]) ).
fof(f28,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X1),identity)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(paramodulation,[status(thm)],[f18,f18]) ).
fof(f29,plain,
! [X0] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,identity))),identity)) = X0,
inference(paramodulation,[status(thm)],[f5,f18]) ).
fof(f62,plain,
! [X0,X1] : multiply(X0,multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X0,X1))),multiply(multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))),multiply(multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))))) = multiply(X1,multiply(X1,X1)),
inference(paramodulation,[status(thm)],[f11,f4]) ).
fof(f65,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
inference(paramodulation,[status(thm)],[f11,f18]) ).
fof(f116,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f65]) ).
fof(f117,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f116]) ).
fof(f118,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f117]) ).
fof(f119,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f118]) ).
fof(f120,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,multiply(identity,identity))))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f119]) ).
fof(f121,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,identity)))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f120]) ).
fof(f122,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,identity))),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f121]) ).
fof(f123,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f122]) ).
fof(f124,plain,
! [X0] : multiply(identity,multiply(multiply(identity,X0),identity)) = multiply(identity,multiply(identity,multiply(X0,identity))),
inference(paramodulation,[status(thm)],[f29,f29]) ).
fof(f131,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))) = X0,
inference(backward_demodulation,[status(thm)],[f124,f29]) ).
fof(f143,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))) = X0,
inference(forward_demodulation,[status(thm)],[f124,f131]) ).
fof(f148,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
inference(paramodulation,[status(thm)],[f143,f11]) ).
fof(f161,plain,
! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(identity,X0),identity)),identity)) = X0,
inference(paramodulation,[status(thm)],[f5,f123]) ).
fof(f168,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),
inference(paramodulation,[status(thm)],[f17,f123]) ).
fof(f169,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),identity),
inference(paramodulation,[status(thm)],[f18,f123]) ).
fof(f178,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity))) = X0,
inference(forward_demodulation,[status(thm)],[f124,f161]) ).
fof(f191,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),
inference(forward_demodulation,[status(thm)],[f5,f168]) ).
fof(f192,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))) = X1,
inference(backward_demodulation,[status(thm)],[f169,f18]) ).
fof(f274,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(X0,X1))),identity),identity))) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(paramodulation,[status(thm)],[f11,f178]) ).
fof(f293,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(X0,X1))),identity),identity))) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(forward_demodulation,[status(thm)],[f5,f274]) ).
fof(f294,plain,
! [X0,X1] : multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(forward_demodulation,[status(thm)],[f178,f293]) ).
fof(f295,plain,
! [X0,X1] : multiply(multiply(identity,multiply(identity,identity)),multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(forward_demodulation,[status(thm)],[f5,f294]) ).
fof(f296,plain,
! [X0,X1] : multiply(multiply(identity,identity),multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(forward_demodulation,[status(thm)],[f5,f295]) ).
fof(f297,plain,
! [X0,X1] : multiply(identity,multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(forward_demodulation,[status(thm)],[f5,f296]) ).
fof(f347,plain,
! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,identity))),identity)),identity)) = multiply(multiply(identity,X0),identity),
inference(paramodulation,[status(thm)],[f124,f123]) ).
fof(f389,plain,
! [X0] : multiply(identity,multiply(X0,identity)) = multiply(multiply(identity,X0),identity),
inference(forward_demodulation,[status(thm)],[f123,f347]) ).
fof(f440,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity))) = multiply(identity,X1),
inference(paramodulation,[status(thm)],[f389,f192]) ).
fof(f491,plain,
! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
inference(paramodulation,[status(thm)],[f11,f12]) ).
fof(f510,plain,
! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))),
inference(paramodulation,[status(thm)],[f12,f123]) ).
fof(f513,plain,
! [X0,X1] : multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f491]) ).
fof(f514,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f513]) ).
fof(f515,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f514]) ).
fof(f516,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f515]) ).
fof(f554,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))),
inference(forward_demodulation,[status(thm)],[f5,f510]) ).
fof(f558,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))),
inference(forward_demodulation,[status(thm)],[f389,f554]) ).
fof(f581,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),identity)) = multiply(X0,identity),
inference(paramodulation,[status(thm)],[f516,f389]) ).
fof(f582,plain,
! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),
inference(paramodulation,[status(thm)],[f516,f123]) ).
fof(f596,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity))) = multiply(X0,identity),
inference(forward_demodulation,[status(thm)],[f389,f581]) ).
fof(f597,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),
inference(forward_demodulation,[status(thm)],[f5,f582]) ).
fof(f599,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),
inference(forward_demodulation,[status(thm)],[f389,f597]) ).
fof(f719,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),identity)) = multiply(identity,X1),
inference(paramodulation,[status(thm)],[f28,f440]) ).
fof(f730,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(identity,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity)),X2))),
inference(paramodulation,[status(thm)],[f440,f11]) ).
fof(f757,plain,
! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity)),X2))),
inference(forward_demodulation,[status(thm)],[f297,f730]) ).
fof(f766,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,X1)),identity))) = multiply(identity,multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(X1,identity))))),
inference(paramodulation,[status(thm)],[f719,f440]) ).
fof(f799,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,X1)),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),
inference(forward_demodulation,[status(thm)],[f5,f766]) ).
fof(f830,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))) = multiply(X0,multiply(multiply(X0,X0),identity)),
inference(paramodulation,[status(thm)],[f191,f143]) ).
fof(f1021,plain,
! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(X0,identity),identity)),identity)) = multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity)),
inference(paramodulation,[status(thm)],[f596,f123]) ).
fof(f1022,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(paramodulation,[status(thm)],[f596,f11]) ).
fof(f1036,plain,
! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(multiply(X0,identity),identity)),identity)) = multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity)),
inference(forward_demodulation,[status(thm)],[f5,f1021]) ).
fof(f1038,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity)),
inference(forward_demodulation,[status(thm)],[f389,f1036]) ).
fof(f1039,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1022]) ).
fof(f1040,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1039]) ).
fof(f1041,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1040]) ).
fof(f1042,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1041]) ).
fof(f1043,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1042]) ).
fof(f1044,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1043]) ).
fof(f1045,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1044]) ).
fof(f1046,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1045]) ).
fof(f1047,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
inference(forward_demodulation,[status(thm)],[f1038,f1046]) ).
fof(f1048,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))))))) = multiply(X0,multiply(multiply(X0,X1),identity)),
inference(forward_demodulation,[status(thm)],[f28,f1047]) ).
fof(f1341,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1)))))),identity),identity))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
inference(paramodulation,[status(thm)],[f599,f599]) ).
fof(f1351,plain,
! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),identity)),identity)) = multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),
inference(paramodulation,[status(thm)],[f599,f123]) ).
fof(f1360,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),identity)),identity))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
inference(forward_demodulation,[status(thm)],[f389,f1341]) ).
fof(f1361,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),identity),identity)))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
inference(forward_demodulation,[status(thm)],[f389,f1360]) ).
fof(f1362,plain,
! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X1),identity),identity))),X2))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
inference(backward_demodulation,[status(thm)],[f1406,f11]) ).
fof(f1374,plain,
! [X0,X1] : multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity)))))) = multiply(X0,multiply(multiply(X0,X1),identity)),
inference(backward_demodulation,[status(thm)],[f1406,f1048]) ).
fof(f1375,plain,
! [X0,X1] : multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
inference(backward_demodulation,[status(thm)],[f1406,f148]) ).
fof(f1406,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
inference(forward_demodulation,[status(thm)],[f143,f1361]) ).
fof(f1440,plain,
! [X0,X1] : multiply(identity,multiply(multiply(X0,identity),identity)) = multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),
inference(forward_demodulation,[status(thm)],[f123,f1351]) ).
fof(f1639,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity))) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
inference(paramodulation,[status(thm)],[f143,f558]) ).
fof(f1663,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f389,f1639]) ).
fof(f1664,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,identity))) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f1663]) ).
fof(f1665,plain,
! [X0] : multiply(identity,multiply(identity,identity)) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f1664]) ).
fof(f1666,plain,
! [X0] : multiply(identity,identity) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f1665]) ).
fof(f1668,plain,
! [X0] : identity = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f1666]) ).
fof(f1784,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity)) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))),
inference(paramodulation,[status(thm)],[f1668,f123]) ).
fof(f1942,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))),
inference(forward_demodulation,[status(thm)],[f5,f1784]) ).
fof(f2363,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),identity),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(paramodulation,[status(thm)],[f62,f1440]) ).
fof(f2368,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(paramodulation,[status(thm)],[f62,f389]) ).
fof(f2633,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),identity),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f5,f2363]) ).
fof(f2634,plain,
! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0)),identity)),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f389,f2633]) ).
fof(f2635,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f389,f2634]) ).
fof(f2636,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(identity,identity)),multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f5,f2635]) ).
fof(f2637,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f5,f2636]) ).
fof(f2638,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f5,f2637]) ).
fof(f2639,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(identity,X0),identity)),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f389,f2638]) ).
fof(f2640,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity)))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f389,f2639]) ).
fof(f2645,plain,
! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
inference(backward_demodulation,[status(thm)],[f2646,f1406]) ).
fof(f2646,plain,
! [X0] : multiply(identity,X0) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
inference(forward_demodulation,[status(thm)],[f143,f2640]) ).
fof(f2681,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f5,f2368]) ).
fof(f2682,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f5,f2681]) ).
fof(f2683,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f5,f2682]) ).
fof(f2684,plain,
! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f5,f2683]) ).
fof(f2708,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
inference(backward_demodulation,[status(thm)],[f2645,f1362]) ).
fof(f2735,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity)))))) = multiply(X0,multiply(multiply(X0,X1),identity)),
inference(backward_demodulation,[status(thm)],[f2645,f1374]) ).
fof(f2736,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
inference(backward_demodulation,[status(thm)],[f2645,f1375]) ).
fof(f2769,plain,
! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity))),multiply(identity,X2))),
inference(backward_demodulation,[status(thm)],[f2708,f757]) ).
fof(f2803,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(X1,identity))) = multiply(X0,multiply(multiply(X0,X1),identity)),
inference(forward_demodulation,[status(thm)],[f143,f2735]) ).
fof(f2806,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2))) = multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),
inference(backward_demodulation,[status(thm)],[f2810,f2708]) ).
fof(f2810,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),X1)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
inference(forward_demodulation,[status(thm)],[f143,f2736]) ).
fof(f2832,plain,
! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(X0,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))),multiply(identity,X2))),
inference(forward_demodulation,[status(thm)],[f799,f2769]) ).
fof(f2841,plain,
! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(X0,multiply(multiply(identity,X1),multiply(identity,X2))),
inference(forward_demodulation,[status(thm)],[f143,f2832]) ).
fof(f2947,plain,
! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),identity)),identity)) = multiply(multiply(X0,X1),multiply(identity,X2)),
inference(paramodulation,[status(thm)],[f2806,f123]) ).
fof(f3026,plain,
! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(X1,X2)) = multiply(multiply(X0,X1),multiply(identity,X2)),
inference(forward_demodulation,[status(thm)],[f123,f2947]) ).
fof(f3150,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity)),identity)) = multiply(multiply(X0,identity),multiply(X1,identity)),
inference(paramodulation,[status(thm)],[f2803,f123]) ).
fof(f3203,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity)),
inference(backward_demodulation,[status(thm)],[f3218,f1942]) ).
fof(f3218,plain,
! [X0,X1] : multiply(multiply(X0,X1),identity) = multiply(multiply(X0,identity),multiply(X1,identity)),
inference(forward_demodulation,[status(thm)],[f123,f3150]) ).
fof(f3231,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),multiply(multiply(X0,identity),multiply(X0,identity))),identity),
inference(forward_demodulation,[status(thm)],[f3218,f3203]) ).
fof(f3232,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),multiply(multiply(X0,X0),identity)),identity),
inference(forward_demodulation,[status(thm)],[f3218,f3231]) ).
fof(f3233,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity),
inference(forward_demodulation,[status(thm)],[f3218,f3232]) ).
fof(f3282,plain,
! [X0,X1] : multiply(multiply(multiply(X0,identity),multiply(X0,identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),identity)) = X1,
inference(paramodulation,[status(thm)],[f3218,f123]) ).
fof(f3391,plain,
! [X0,X1] : multiply(multiply(multiply(X0,X0),identity),multiply(multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),identity)) = X1,
inference(forward_demodulation,[status(thm)],[f3218,f3282]) ).
fof(f3392,plain,
! [X0,X1] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),identity) = X1,
inference(forward_demodulation,[status(thm)],[f3218,f3391]) ).
fof(f3483,plain,
! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X2)),identity)),identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),X2)),identity),
inference(paramodulation,[status(thm)],[f3392,f169]) ).
fof(f3487,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))) = multiply(multiply(X2,X2),multiply(multiply(X2,multiply(multiply(X2,identity),X1)),identity)),
inference(paramodulation,[status(thm)],[f3392,f192]) ).
fof(f3489,plain,
! [X0,X1] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))) = multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),
inference(paramodulation,[status(thm)],[f3392,f143]) ).
fof(f3596,plain,
! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),X1)),identity),
inference(forward_demodulation,[status(thm)],[f3392,f3483]) ).
fof(f3603,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity)))),
inference(backward_demodulation,[status(thm)],[f3489,f3487]) ).
fof(f4554,plain,
! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(identity,multiply(X1,X2))),identity)),identity)) = multiply(multiply(identity,X1),multiply(identity,X2)),
inference(paramodulation,[status(thm)],[f2841,f123]) ).
fof(f4718,plain,
! [X0,X1] : multiply(identity,multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(identity,X1)),
inference(forward_demodulation,[status(thm)],[f123,f4554]) ).
fof(f4878,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),
inference(paramodulation,[status(thm)],[f2646,f558]) ).
fof(f4969,plain,
! [X0] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(backward_demodulation,[status(thm)],[f4971,f2684]) ).
fof(f4971,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))) = multiply(multiply(identity,multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),
inference(forward_demodulation,[status(thm)],[f3233,f4878]) ).
fof(f4979,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity))) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f389,f4969]) ).
fof(f4980,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f389,f4979]) ).
fof(f4999,plain,
! [X0] : multiply(X0,multiply(multiply(X0,X0),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
inference(forward_demodulation,[status(thm)],[f830,f4980]) ).
fof(f5010,plain,
! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity)) = multiply(multiply(identity,X0),identity),
inference(paramodulation,[status(thm)],[f2646,f4999]) ).
fof(f5015,plain,
! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity)) = multiply(X0,X0),
inference(paramodulation,[status(thm)],[f4999,f123]) ).
fof(f5020,plain,
! [X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X1))),identity) = multiply(multiply(X0,identity),multiply(X1,multiply(multiply(X1,X1),identity))),
inference(paramodulation,[status(thm)],[f4999,f3218]) ).
fof(f5029,plain,
! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity)) = multiply(identity,multiply(X0,identity)),
inference(forward_demodulation,[status(thm)],[f389,f5010]) ).
fof(f5208,plain,
! [X0,X1,X2] : multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),X2))),identity) = multiply(multiply(X0,identity),multiply(multiply(X1,X1),multiply(multiply(X1,X2),identity))),
inference(paramodulation,[status(thm)],[f3596,f3218]) ).
fof(f5661,plain,
! [X0] : multiply(identity,multiply(multiply(identity,identity),identity)) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(paramodulation,[status(thm)],[f2645,f1440]) ).
fof(f5752,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,identity))) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f389,f5661]) ).
fof(f5753,plain,
! [X0] : multiply(identity,multiply(identity,identity)) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f5752]) ).
fof(f5754,plain,
! [X0] : multiply(identity,identity) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f5753]) ).
fof(f5755,plain,
! [X0] : identity = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f5,f5754]) ).
fof(f5756,plain,
! [X0] : identity = multiply(identity,multiply(multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))))),multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f4718,f5755]) ).
fof(f5757,plain,
! [X0] : identity = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f3026,f5756]) ).
fof(f5758,plain,
! [X0] : identity = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f2645,f5757]) ).
fof(f5759,plain,
! [X0] : identity = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),
inference(forward_demodulation,[status(thm)],[f143,f5758]) ).
fof(f5760,plain,
! [X0] : identity = multiply(identity,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity)),
inference(forward_demodulation,[status(thm)],[f5208,f5759]) ).
fof(f7011,plain,
! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(paramodulation,[status(thm)],[f5760,f123]) ).
fof(f7071,plain,
! [X0] : multiply(multiply(identity,multiply(identity,multiply(identity,identity))),identity) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f3218,f7011]) ).
fof(f7072,plain,
! [X0] : multiply(identity,multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f389,f7071]) ).
fof(f7073,plain,
! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity))) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f389,f7072]) ).
fof(f7074,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f389,f7073]) ).
fof(f7075,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,identity))) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f5,f7074]) ).
fof(f7076,plain,
! [X0] : multiply(identity,multiply(identity,identity)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f5,f7075]) ).
fof(f7077,plain,
! [X0] : multiply(identity,identity) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f5,f7076]) ).
fof(f7079,plain,
! [X0] : multiply(multiply(X0,X0),identity) = multiply(X0,X0),
inference(backward_demodulation,[status(thm)],[f7085,f5015]) ).
fof(f7085,plain,
! [X0] : identity = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(forward_demodulation,[status(thm)],[f5,f7077]) ).
fof(f7098,plain,
! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))) = multiply(identity,multiply(X0,identity)),
inference(backward_demodulation,[status(thm)],[f7079,f5029]) ).
fof(f7107,plain,
! [X0] : identity = multiply(multiply(X0,multiply(X0,multiply(X0,X0))),identity),
inference(backward_demodulation,[status(thm)],[f7079,f7085]) ).
fof(f7149,plain,
! [X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X1))),identity) = multiply(multiply(X0,identity),multiply(X1,multiply(X1,X1))),
inference(backward_demodulation,[status(thm)],[f7079,f5020]) ).
fof(f7199,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))) = X0,
inference(backward_demodulation,[status(thm)],[f7268,f143]) ).
fof(f7264,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))) = multiply(identity,multiply(identity,multiply(identity,X1))),
inference(backward_demodulation,[status(thm)],[f7268,f3603]) ).
fof(f7268,plain,
! [X0] : multiply(identity,X0) = multiply(identity,multiply(X0,identity)),
inference(forward_demodulation,[status(thm)],[f2646,f7098]) ).
fof(f7341,plain,
! [X0] : identity = multiply(multiply(X0,identity),multiply(X0,multiply(X0,X0))),
inference(backward_demodulation,[status(thm)],[f7149,f7107]) ).
fof(f7390,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f7268,f7199]) ).
fof(f7596,plain,
! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))) = multiply(identity,multiply(identity,multiply(identity,X0))),
inference(forward_demodulation,[status(thm)],[f3603,f7264]) ).
fof(f7597,plain,
! [X0] : multiply(X0,identity) = multiply(identity,multiply(identity,multiply(identity,X0))),
inference(forward_demodulation,[status(thm)],[f7390,f7596]) ).
fof(f7678,plain,
! [X0] : multiply(X0,identity) = X0,
inference(forward_demodulation,[status(thm)],[f7390,f7597]) ).
fof(f7777,plain,
identity != identity,
inference(backward_demodulation,[status(thm)],[f7780,f6]) ).
fof(f7780,plain,
! [X0] : identity = multiply(X0,multiply(X0,multiply(X0,X0))),
inference(forward_demodulation,[status(thm)],[f7678,f7341]) ).
fof(f8659,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f7777]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP119-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/10.38 % Computer : n026.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Sun Sep 20 20:00:47 UTC 2026
% 0.09/10.39 % CPUTime :
% 0.09/10.39 % Drodi V4.1.1
% 19.04/12.83 % Refutation found
% 19.04/12.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 19.04/12.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.85/14.09 % Elapsed time: 3.487055 seconds
% 14.85/14.09 % CPU time: 16.116665 seconds
% 14.85/14.09 % Total memory used: 404.392 MB
% 14.85/14.09 % Net memory used: 391.363 MB
%------------------------------------------------------------------------------