%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG005-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 11:47:44 AM UTC 2026
% Result : Unsatisfiable 13.53s 2.27s
% Output : CNFRefutation 13.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 5
% Syntax : Number of formulae : 210 ( 210 unt; 0 def)
% Number of atoms : 210 ( 209 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 6 ( 2 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 : 571 ( 571 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] : difference(X,difference(Y,X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : difference(X,difference(X,Y)) = difference(Y,difference(Y,X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : difference(difference(X,Y),Z) = difference(difference(X,Z),difference(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : multiply(X,Y) = difference(X,difference(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
multiply(multiply(a,b),c) != multiply(a,multiply(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,plain,
! [X0,X1] : difference(X0,difference(X1,X0)) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f7,plain,
! [X0,X1] : difference(X0,difference(X0,X1)) = difference(X1,difference(X1,X0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f8,plain,
! [X0,X1,X2] : difference(difference(X0,X1),X2) = difference(difference(X0,X2),difference(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f9,plain,
! [X0,X1] : multiply(X0,X1) = difference(X0,difference(X0,X1)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
multiply(multiply(a,b),c) != multiply(a,multiply(b,c)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f16,plain,
! [X0,X1] : difference(X0,difference(X0,X1)) = multiply(X1,X0),
inference(backward_demodulation,[status(thm)],[f9,f7]) ).
fof(f17,plain,
multiply(c,multiply(a,b)) != multiply(a,multiply(b,c)),
inference(backward_demodulation,[status(thm)],[f18,f10]) ).
fof(f18,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f9,f16]) ).
fof(f23,plain,
! [X0,X1] : multiply(X0,difference(X0,X1)) = difference(X0,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f9,f9]) ).
fof(f26,plain,
! [X0] : multiply(X0,X0) = X0,
inference(paramodulation,[status(thm)],[f9,f6]) ).
fof(f27,plain,
! [X0,X1] : difference(difference(X0,X1),X1) = difference(X0,X1),
inference(paramodulation,[status(thm)],[f6,f6]) ).
fof(f28,plain,
! [X0,X1] : difference(difference(X0,X1),multiply(X0,X1)) = difference(X0,X1),
inference(paramodulation,[status(thm)],[f9,f6]) ).
fof(f31,plain,
! [X0,X1] : multiply(X0,difference(X1,X0)) = difference(X0,X0),
inference(paramodulation,[status(thm)],[f6,f9]) ).
fof(f35,plain,
! [X0,X1] : multiply(difference(X0,X1),X1) = difference(difference(X0,X1),difference(X0,X1)),
inference(paramodulation,[status(thm)],[f6,f31]) ).
fof(f36,plain,
! [X0,X1] : multiply(difference(X0,X1),multiply(X0,X1)) = difference(difference(X0,X1),difference(X0,X1)),
inference(paramodulation,[status(thm)],[f9,f31]) ).
fof(f38,plain,
! [X0,X1] : multiply(X0,difference(X1,X0)) = difference(difference(X1,X0),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f18,f35]) ).
fof(f39,plain,
! [X0,X1] : difference(X0,X0) = difference(difference(X1,X0),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f31,f38]) ).
fof(f40,plain,
! [X0,X1] : difference(X0,X0) = difference(difference(X1,X1),X0),
inference(forward_demodulation,[status(thm)],[f8,f39]) ).
fof(f41,plain,
! [X0,X1] : multiply(difference(X0,X1),multiply(X0,X1)) = difference(difference(X0,X0),X1),
inference(forward_demodulation,[status(thm)],[f8,f36]) ).
fof(f52,plain,
! [X0,X1] : multiply(difference(X0,X0),X1) = difference(difference(X0,X0),difference(X1,X1)),
inference(paramodulation,[status(thm)],[f40,f9]) ).
fof(f56,plain,
! [X0,X1] : multiply(X0,multiply(X0,difference(X1,X0))) = difference(difference(X0,X0),difference(X1,X0)),
inference(paramodulation,[status(thm)],[f6,f41]) ).
fof(f57,plain,
! [X0,X1] : multiply(multiply(X0,X1),multiply(X0,difference(X0,X1))) = difference(difference(X0,X0),difference(X0,X1)),
inference(paramodulation,[status(thm)],[f9,f41]) ).
fof(f68,plain,
! [X0,X1] : multiply(X0,difference(X0,X0)) = difference(difference(X0,X0),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f31,f56]) ).
fof(f69,plain,
! [X0,X1] : difference(X0,X0) = difference(difference(X0,X0),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f31,f68]) ).
fof(f70,plain,
! [X0,X1] : difference(X0,X0) = difference(difference(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f8,f69]) ).
fof(f71,plain,
! [X0,X1] : multiply(multiply(X0,X1),difference(X0,multiply(X0,X1))) = difference(difference(X0,X0),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f23,f57]) ).
fof(f72,plain,
! [X0,X1] : difference(multiply(X0,X1),multiply(X0,X1)) = difference(difference(X0,X0),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f31,f71]) ).
fof(f90,plain,
! [X0,X1] : difference(difference(X0,X1),difference(X0,X1)) = difference(difference(X0,X0),difference(X0,X1)),
inference(paramodulation,[status(thm)],[f70,f70]) ).
fof(f91,plain,
! [X0,X1] : difference(difference(X0,X0),difference(X0,X0)) = difference(difference(X1,X1),difference(X0,X0)),
inference(paramodulation,[status(thm)],[f40,f70]) ).
fof(f93,plain,
! [X0,X1] : difference(X0,X0) = difference(multiply(X0,X1),X0),
inference(paramodulation,[status(thm)],[f9,f70]) ).
fof(f100,plain,
! [X0,X1] : multiply(difference(X0,X1),X0) = difference(difference(X0,X1),difference(X0,X0)),
inference(paramodulation,[status(thm)],[f70,f9]) ).
fof(f101,plain,
! [X0,X1] : difference(multiply(X0,X1),multiply(X0,X1)) = difference(difference(X0,X0),X1),
inference(backward_demodulation,[status(thm)],[f102,f72]) ).
fof(f102,plain,
! [X0,X1] : difference(difference(X0,X0),X1) = difference(difference(X0,X0),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f8,f90]) ).
fof(f103,plain,
! [X0,X1] : difference(difference(X0,X0),X0) = difference(difference(X1,X1),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f102,f91]) ).
fof(f104,plain,
! [X0,X1] : difference(X0,X0) = difference(difference(X1,X1),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f70,f103]) ).
fof(f105,plain,
! [X0,X1] : difference(X0,X0) = multiply(difference(X1,X1),X0),
inference(forward_demodulation,[status(thm)],[f52,f104]) ).
fof(f111,plain,
! [X0,X1] : multiply(X0,difference(X0,X1)) = difference(difference(X0,X1),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f18,f100]) ).
fof(f112,plain,
! [X0,X1] : difference(X0,multiply(X0,X1)) = difference(difference(X0,X1),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f23,f111]) ).
fof(f119,plain,
! [X0,X1] : difference(X0,X0) = difference(multiply(X1,X0),X0),
inference(paramodulation,[status(thm)],[f18,f93]) ).
fof(f121,plain,
! [X0,X1] : difference(multiply(X0,X1),multiply(X0,X1)) = difference(difference(X0,X0),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f93,f70]) ).
fof(f126,plain,
! [X0,X1] : multiply(multiply(X0,X1),X0) = difference(multiply(X0,X1),difference(X0,X0)),
inference(paramodulation,[status(thm)],[f93,f9]) ).
fof(f129,plain,
! [X0,X1] : difference(difference(X0,X0),X1) = difference(difference(X0,X0),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f101,f121]) ).
fof(f133,plain,
! [X0,X1] : multiply(X0,multiply(X0,X1)) = difference(multiply(X0,X1),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f18,f126]) ).
fof(f147,plain,
! [X0,X1] : multiply(multiply(X0,X1),X1) = difference(multiply(X0,X1),difference(X1,X1)),
inference(paramodulation,[status(thm)],[f119,f9]) ).
fof(f158,plain,
! [X0,X1] : multiply(X0,multiply(X1,X0)) = difference(multiply(X1,X0),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f18,f147]) ).
fof(f173,plain,
! [X0,X1] : difference(X0,multiply(difference(X1,X1),X0)) = X0,
inference(paramodulation,[status(thm)],[f105,f6]) ).
fof(f209,plain,
! [X0,X1] : difference(difference(X0,X1),multiply(X1,X0)) = difference(X0,X1),
inference(paramodulation,[status(thm)],[f18,f28]) ).
fof(f214,plain,
! [X0,X1] : difference(multiply(X0,X1),difference(X0,X1)) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f28,f6]) ).
fof(f254,plain,
! [X0,X1] : difference(difference(X0,X0),multiply(X0,multiply(X0,X1))) = difference(multiply(X0,X1),X0),
inference(paramodulation,[status(thm)],[f93,f209]) ).
fof(f263,plain,
! [X0,X1] : difference(difference(multiply(X0,X1),difference(X0,X1)),difference(difference(X0,X0),X1)) = difference(multiply(X0,X1),difference(X0,X1)),
inference(paramodulation,[status(thm)],[f41,f209]) ).
fof(f275,plain,
! [X0,X1] : difference(multiply(X0,X1),difference(X1,X0)) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f209,f6]) ).
fof(f280,plain,
! [X0,X1] : difference(difference(X0,X0),multiply(X0,X1)) = difference(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f129,f254]) ).
fof(f281,plain,
! [X0,X1] : difference(difference(X0,X0),X1) = difference(multiply(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f129,f280]) ).
fof(f288,plain,
! [X0,X1] : multiply(difference(X0,X0),X1) = difference(X0,X0),
inference(backward_demodulation,[status(thm)],[f299,f52]) ).
fof(f299,plain,
! [X0,X1] : difference(difference(X0,X0),X1) = difference(X0,X0),
inference(forward_demodulation,[status(thm)],[f93,f281]) ).
fof(f323,plain,
! [X0,X1] : difference(multiply(X0,X1),difference(difference(X0,X0),X1)) = difference(multiply(X0,X1),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f214,f263]) ).
fof(f324,plain,
! [X0,X1] : difference(multiply(X0,X1),difference(X0,X0)) = difference(multiply(X0,X1),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f299,f323]) ).
fof(f325,plain,
! [X0,X1] : multiply(X0,multiply(X0,X1)) = difference(multiply(X0,X1),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f133,f324]) ).
fof(f329,plain,
! [X0,X1] : multiply(X0,multiply(X0,X1)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f214,f325]) ).
fof(f361,plain,
! [X0,X1] : difference(X0,difference(X1,X1)) = X0,
inference(backward_demodulation,[status(thm)],[f288,f173]) ).
fof(f379,plain,
! [X0,X1] : multiply(X0,multiply(X1,X0)) = multiply(X1,X0),
inference(backward_demodulation,[status(thm)],[f361,f158]) ).
fof(f380,plain,
! [X0,X1] : difference(X0,multiply(X0,X1)) = difference(X0,X1),
inference(backward_demodulation,[status(thm)],[f361,f112]) ).
fof(f470,plain,
! [X0,X1] : difference(X0,multiply(X1,X0)) = difference(X0,X1),
inference(paramodulation,[status(thm)],[f18,f380]) ).
fof(f834,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,X1),X2),difference(X3,X1)) = difference(difference(difference(X0,X3),X1),difference(X2,difference(X3,X1))),
inference(paramodulation,[status(thm)],[f8,f8]) ).
fof(f838,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),X1) = difference(difference(X0,X1),difference(X2,X1)),
inference(paramodulation,[status(thm)],[f27,f8]) ).
fof(f841,plain,
! [X0,X1,X2] : difference(difference(X0,X1),multiply(X0,X2)) = difference(difference(X0,X2),difference(X1,multiply(X0,X2))),
inference(paramodulation,[status(thm)],[f380,f8]) ).
fof(f843,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X2,X0)) = difference(X0,difference(X1,difference(X2,X0))),
inference(paramodulation,[status(thm)],[f6,f8]) ).
fof(f844,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X0,X2)) = difference(multiply(X0,X2),difference(X1,difference(X0,X2))),
inference(paramodulation,[status(thm)],[f9,f8]) ).
fof(f848,plain,
! [X0,X1,X2] : difference(difference(X0,multiply(X1,X2)),difference(X1,X2)) = difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f214,f8]) ).
fof(f858,plain,
! [X0,X1,X2] : difference(difference(X0,X1),multiply(X1,X2)) = difference(difference(X0,multiply(X1,X2)),difference(X1,X2)),
inference(paramodulation,[status(thm)],[f380,f8]) ).
fof(f861,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X1,X2)) = difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f9,f8]) ).
fof(f882,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(X2,X1)) = difference(difference(X0,X1),difference(difference(X0,X2),X1)),
inference(paramodulation,[status(thm)],[f8,f9]) ).
fof(f897,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),X1) = difference(difference(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f8,f838]) ).
fof(f919,plain,
! [X0,X1,X2] : difference(difference(X0,X1),multiply(X1,X2)) = difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f848,f858]) ).
fof(f924,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X1,X2)) = difference(difference(X0,X1),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f919,f861]) ).
fof(f957,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(X2,X1)) = difference(difference(X0,difference(X0,X2)),X1),
inference(forward_demodulation,[status(thm)],[f8,f882]) ).
fof(f963,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(X2,X1)) = difference(multiply(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f9,f957]) ).
fof(f982,plain,
! [X0,X1,X2] : difference(difference(difference(X0,multiply(X0,X1)),X2),difference(X1,multiply(X0,X1))) = difference(difference(X0,X1),difference(X2,difference(X1,multiply(X0,X1)))),
inference(paramodulation,[status(thm)],[f28,f834]) ).
fof(f993,plain,
! [X0,X1,X2,X3] : difference(difference(difference(multiply(X0,X1),X2),X3),difference(difference(X1,X0),X2)) = difference(difference(multiply(X0,X1),X2),difference(X3,difference(difference(X1,X0),X2))),
inference(paramodulation,[status(thm)],[f275,f834]) ).
fof(f1010,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),multiply(X1,X2)),difference(X2,X1)) = difference(difference(difference(X0,X2),X1),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f275,f834]) ).
fof(f1021,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),difference(X2,X1)) = difference(difference(difference(X0,X2),X1),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f9,f834]) ).
fof(f1072,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),difference(X1,multiply(X0,X1))) = difference(difference(X0,X1),difference(X2,difference(X1,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f380,f982]) ).
fof(f1073,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),difference(X1,X0)) = difference(difference(X0,X1),difference(X2,difference(X1,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f470,f1072]) ).
fof(f1074,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),difference(X1,X0)) = difference(difference(X0,X1),difference(X2,difference(X1,X0))),
inference(forward_demodulation,[status(thm)],[f470,f1073]) ).
fof(f1126,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),difference(X1,X2)),difference(X2,X1)) = difference(difference(difference(X0,X2),X1),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f924,f1010]) ).
fof(f1127,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),difference(X1,X2)),difference(X2,X1)) = difference(difference(difference(X0,X2),X1),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f924,f1126]) ).
fof(f1253,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X2,X0)) = difference(X0,difference(multiply(X0,X1),difference(X2,X0))),
inference(paramodulation,[status(thm)],[f380,f843]) ).
fof(f1266,plain,
! [X0,X1,X2] : difference(difference(multiply(X0,X1),X2),difference(X0,X1)) = difference(multiply(X0,X1),difference(X2,difference(difference(X0,X1),multiply(X0,X1)))),
inference(paramodulation,[status(thm)],[f28,f843]) ).
fof(f1331,plain,
! [X0,X1,X2] : difference(X0,difference(X1,difference(X2,X0))) = difference(X0,difference(multiply(X0,X1),difference(X2,X0))),
inference(forward_demodulation,[status(thm)],[f843,f1253]) ).
fof(f1357,plain,
! [X0,X1,X2] : difference(difference(multiply(X0,X1),X2),difference(X0,X1)) = difference(multiply(X0,X1),difference(X2,difference(X0,X1))),
inference(forward_demodulation,[status(thm)],[f28,f1266]) ).
fof(f1358,plain,
! [X0,X1,X2] : difference(difference(multiply(X0,X1),X2),difference(X0,X1)) = difference(difference(X0,X2),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f844,f1357]) ).
fof(f1822,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X1,multiply(X2,X1))) = difference(difference(X0,X1),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f379,f924]) ).
fof(f1851,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(X1,X2)) = difference(difference(X0,X1),difference(difference(X0,X1),difference(X1,X2))),
inference(paramodulation,[status(thm)],[f924,f9]) ).
fof(f1902,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),difference(X2,X1)) = difference(difference(difference(X0,X2),X1),difference(X1,X2)),
inference(backward_demodulation,[status(thm)],[f1906,f1021]) ).
fof(f1906,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X1,X2)) = difference(difference(X0,X1),multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f470,f1822]) ).
fof(f1941,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(X1,X2)) = multiply(difference(X0,X1),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f9,f1851]) ).
fof(f1958,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X0,multiply(X2,X0))) = difference(multiply(X2,X0),difference(X1,difference(X0,multiply(X2,X0)))),
inference(paramodulation,[status(thm)],[f379,f844]) ).
fof(f2001,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),difference(X3,difference(X1,X2))) = difference(difference(difference(X0,X3),difference(X1,X2)),difference(difference(X1,X3),difference(X1,X2))),
inference(paramodulation,[status(thm)],[f844,f834]) ).
fof(f2008,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X3,multiply(X0,X2))) = difference(multiply(X0,X2),difference(difference(X1,difference(X0,X2)),difference(X3,multiply(X0,X2)))),
inference(paramodulation,[status(thm)],[f844,f843]) ).
fof(f2019,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X0,X1))) = difference(multiply(X0,X1),difference(difference(X0,X2),difference(X0,X1))),
inference(paramodulation,[status(thm)],[f844,f9]) ).
fof(f2036,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X0,X2)) = difference(multiply(X2,X0),difference(X1,difference(X0,multiply(X2,X0)))),
inference(forward_demodulation,[status(thm)],[f470,f1958]) ).
fof(f2038,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X0,X2)) = difference(multiply(X2,X0),difference(X1,difference(X0,X2))),
inference(forward_demodulation,[status(thm)],[f470,f2036]) ).
fof(f2144,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),difference(X3,difference(X1,X2))) = difference(difference(difference(X0,X3),difference(X1,X3)),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f8,f2001]) ).
fof(f2145,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),difference(X3,difference(X1,X2))) = difference(difference(difference(X0,X1),X3),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f8,f2144]) ).
fof(f2168,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X0,X1))) = difference(difference(X0,difference(X0,X2)),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f844,f2019]) ).
fof(f2174,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X0,X1))) = difference(multiply(X0,X2),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f9,f2168]) ).
fof(f2355,plain,
! [X0,X1,X2] : difference(difference(multiply(X0,X1),X2),difference(X1,X0)) = difference(difference(X1,X2),difference(X1,X0)),
inference(paramodulation,[status(thm)],[f18,f1358]) ).
fof(f2393,plain,
! [X0,X1,X2,X3] : difference(difference(X0,difference(multiply(X1,X2),X3)),difference(X1,X2)) = difference(difference(X0,difference(X1,X2)),difference(difference(X1,X3),difference(X1,X2))),
inference(paramodulation,[status(thm)],[f1358,f8]) ).
fof(f2401,plain,
! [X0,X1,X2] : multiply(difference(multiply(X0,X1),X2),difference(X0,X1)) = difference(difference(multiply(X0,X1),X2),difference(difference(X0,X2),difference(X0,X1))),
inference(paramodulation,[status(thm)],[f1358,f9]) ).
fof(f2535,plain,
! [X0,X1,X2,X3] : difference(difference(X0,difference(multiply(X1,X2),X3)),difference(X1,X2)) = difference(difference(X0,difference(X1,X3)),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f8,f2393]) ).
fof(f2542,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(multiply(X0,X1),X2)) = difference(difference(multiply(X0,X1),X2),difference(difference(X0,X2),difference(X0,X1))),
inference(forward_demodulation,[status(thm)],[f18,f2401]) ).
fof(f2558,plain,
! [X0,X1,X2] : difference(multiply(multiply(X0,X1),X2),difference(X1,X0)) = difference(difference(X1,difference(multiply(X0,X1),X2)),difference(X1,X0)),
inference(paramodulation,[status(thm)],[f9,f2355]) ).
fof(f2579,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(difference(X0,X1),difference(X2,X1)),X3),difference(difference(X2,X0),X1)) = difference(difference(difference(X2,X1),X3),difference(difference(X2,X1),difference(X0,X1))),
inference(paramodulation,[status(thm)],[f8,f2355]) ).
fof(f2597,plain,
! [X0,X1,X2] : difference(difference(X0,difference(multiply(X1,X0),X2)),difference(X0,X1)) = difference(multiply(X0,X1),difference(difference(X0,X2),difference(X0,X1))),
inference(paramodulation,[status(thm)],[f2355,f844]) ).
fof(f2682,plain,
! [X0,X1,X2,X3] : difference(difference(difference(multiply(X0,X1),X2),X3),difference(difference(X1,X0),X2)) = difference(difference(difference(X1,X2),X3),difference(difference(X1,X2),difference(X0,X2))),
inference(forward_demodulation,[status(thm)],[f963,f2579]) ).
fof(f2683,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(X0,X1),X2),difference(X3,difference(difference(X1,X0),X2))) = difference(difference(difference(X1,X2),X3),difference(difference(X1,X2),difference(X0,X2))),
inference(forward_demodulation,[status(thm)],[f993,f2682]) ).
fof(f2685,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(X0,X1),X2),difference(X3,difference(difference(X1,X0),X2))) = difference(difference(difference(X1,X2),X3),difference(difference(X1,X0),X2)),
inference(forward_demodulation,[status(thm)],[f8,f2683]) ).
fof(f2732,plain,
! [X0,X1,X2] : difference(multiply(multiply(X0,X1),X2),difference(X1,X0)) = difference(multiply(X1,X0),difference(difference(X1,X2),difference(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2558,f2597]) ).
fof(f2733,plain,
! [X0,X1,X2] : difference(multiply(multiply(X0,X1),X2),difference(X1,X0)) = difference(difference(X1,difference(X1,X2)),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f844,f2732]) ).
fof(f2735,plain,
! [X0,X1,X2] : difference(multiply(multiply(X0,X1),X2),difference(X1,X0)) = difference(multiply(X1,X2),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f9,f2733]) ).
fof(f2801,plain,
! [X0,X1,X2] : difference(difference(difference(X0,multiply(X1,X2)),multiply(X1,X2)),difference(difference(X1,X2),multiply(X1,X2))) = difference(difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),difference(multiply(X1,X2),difference(X1,X2))),
inference(paramodulation,[status(thm)],[f214,f1127]) ).
fof(f2849,plain,
! [X0,X1,X2] : difference(difference(X0,difference(difference(X1,X2),difference(X2,X0))),difference(X0,X2)) = difference(multiply(X0,X2),difference(difference(difference(X1,X0),X2),difference(X2,X0))),
inference(paramodulation,[status(thm)],[f1127,f844]) ).
fof(f2988,plain,
! [X0,X1,X2] : difference(difference(difference(X0,multiply(X1,X2)),difference(X1,X2)),multiply(X1,X2)) = difference(difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),difference(multiply(X1,X2),difference(X1,X2))),
inference(forward_demodulation,[status(thm)],[f8,f2801]) ).
fof(f2989,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X1,X2)),multiply(X1,X2)) = difference(difference(difference(X0,difference(X1,X2)),multiply(X1,X2)),difference(multiply(X1,X2),difference(X1,X2))),
inference(forward_demodulation,[status(thm)],[f897,f2988]) ).
fof(f2990,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X1,X2)),multiply(X1,X2)) = difference(difference(difference(X0,X1),multiply(X1,X2)),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f2145,f2989]) ).
fof(f2991,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X1,X2)),multiply(X1,X2)) = difference(difference(difference(X0,X1),difference(X1,X2)),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f924,f2990]) ).
fof(f2996,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X1,X2)),multiply(X1,X2)) = difference(difference(X0,X1),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f27,f2991]) ).
fof(f3177,plain,
! [X0,X1,X2] : difference(difference(X0,difference(difference(X1,X2),difference(X2,X0))),difference(X0,X2)) = difference(difference(X2,difference(difference(X1,X0),X2)),difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f2038,f2849]) ).
fof(f3178,plain,
! [X0,X1,X2] : difference(difference(X0,difference(difference(X1,X2),difference(X2,X0))),difference(X0,X2)) = difference(X2,difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f6,f3177]) ).
fof(f3179,plain,
! [X0,X1,X2] : difference(difference(X0,difference(difference(X1,X2),difference(X2,X0))),difference(X0,X2)) = multiply(X2,X0),
inference(forward_demodulation,[status(thm)],[f9,f3178]) ).
fof(f3260,plain,
! [X0,X1,X2] : difference(difference(X0,difference(difference(X1,X2),difference(multiply(X2,X1),X0))),difference(X0,multiply(X2,X1))) = multiply(multiply(X2,X1),X0),
inference(paramodulation,[status(thm)],[f470,f3179]) ).
fof(f3261,plain,
! [X0,X1,X2] : difference(difference(X0,difference(difference(X1,X2),difference(multiply(X1,X2),X0))),difference(X0,multiply(X1,X2))) = multiply(multiply(X1,X2),X0),
inference(paramodulation,[status(thm)],[f380,f3179]) ).
fof(f3267,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),difference(difference(X3,multiply(X1,X2)),difference(difference(X1,X0),difference(X1,X2)))),difference(difference(X0,difference(X1,X2)),multiply(X1,X2))) = multiply(multiply(X1,X2),difference(X0,difference(X1,X2))),
inference(paramodulation,[status(thm)],[f844,f3179]) ).
fof(f3400,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),difference(difference(X3,multiply(X1,X2)),difference(difference(X1,X0),difference(X1,X2)))),difference(difference(X0,X1),difference(X1,X2))) = multiply(multiply(X1,X2),difference(X0,difference(X1,X2))),
inference(forward_demodulation,[status(thm)],[f2996,f3267]) ).
fof(f3401,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),difference(difference(X3,multiply(X1,X2)),difference(difference(X1,X0),difference(X1,X2)))),difference(difference(X0,X1),difference(X1,X2))) = difference(multiply(X1,X0),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f2174,f3400]) ).
fof(f3617,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(multiply(X0,X1),difference(multiply(X0,X1),X2))) = difference(multiply(multiply(X0,X1),X2),difference(difference(X0,difference(multiply(X0,X1),X2)),difference(X0,X1))),
inference(paramodulation,[status(thm)],[f9,f2542]) ).
fof(f3661,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(multiply(X0,X1),difference(X2,X0))) = difference(difference(multiply(X0,X1),difference(X2,X0)),difference(X0,difference(X0,X1))),
inference(paramodulation,[status(thm)],[f6,f2542]) ).
fof(f3765,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(multiply(X0,X1),X2)) = difference(multiply(multiply(X0,X1),X2),difference(difference(X0,difference(multiply(X0,X1),X2)),difference(X0,X1))),
inference(forward_demodulation,[status(thm)],[f9,f3617]) ).
fof(f3766,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(multiply(X0,X1),X2)) = difference(multiply(multiply(X0,X1),X2),difference(difference(X0,difference(X0,X2)),difference(X0,X1))),
inference(forward_demodulation,[status(thm)],[f2535,f3765]) ).
fof(f3767,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(multiply(X0,X1),X2)) = difference(multiply(multiply(X0,X1),X2),difference(multiply(X0,X2),difference(X0,X1))),
inference(forward_demodulation,[status(thm)],[f9,f3766]) ).
fof(f3881,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(multiply(X0,X1),difference(X2,X0))) = difference(difference(multiply(X0,X1),difference(X2,X0)),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f9,f3661]) ).
fof(f3882,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(multiply(X0,X1),difference(X2,X0))) = difference(multiply(X0,X1),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f70,f3881]) ).
fof(f4104,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(multiply(X0,X1),difference(X2,X0))) = difference(multiply(multiply(X0,X1),difference(X2,X0)),difference(difference(X0,X0),difference(X0,X1))),
inference(paramodulation,[status(thm)],[f31,f3767]) ).
fof(f4256,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(multiply(X0,X1),difference(X2,X0))) = difference(multiply(multiply(X0,X1),difference(X2,X0)),difference(X0,X0)),
inference(forward_demodulation,[status(thm)],[f299,f4104]) ).
fof(f4257,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),multiply(multiply(X0,X1),difference(X2,X0))) = multiply(multiply(X0,X1),difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f361,f4256]) ).
fof(f4471,plain,
! [X0,X1,X2] : multiply(difference(X0,multiply(X0,X1)),multiply(multiply(X0,X1),difference(X2,X0))) = multiply(multiply(X0,multiply(X0,X1)),difference(X2,X0)),
inference(paramodulation,[status(thm)],[f329,f4257]) ).
fof(f4623,plain,
! [X0,X1,X2] : multiply(difference(X0,multiply(X0,X1)),difference(multiply(X0,X1),difference(X2,X0))) = multiply(multiply(X0,multiply(X0,X1)),difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f1941,f4471]) ).
fof(f4624,plain,
! [X0,X1,X2] : multiply(difference(X0,X1),difference(multiply(X0,X1),difference(X2,X0))) = multiply(multiply(X0,multiply(X0,X1)),difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f380,f4623]) ).
fof(f4625,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),multiply(X0,X1)) = multiply(multiply(X0,multiply(X0,X1)),difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f3882,f4624]) ).
fof(f4626,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),multiply(X0,X1)) = multiply(multiply(X0,X1),difference(X2,X0)),
inference(forward_demodulation,[status(thm)],[f329,f4625]) ).
fof(f4736,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X1,X0))) = difference(multiply(multiply(X0,X1),X2),difference(X1,X0)),
inference(paramodulation,[status(thm)],[f275,f963]) ).
fof(f4762,plain,
! [X0,X1,X2] : multiply(difference(X0,difference(X1,X2)),multiply(X2,X1)) = difference(multiply(X0,multiply(X2,X1)),difference(X1,X2)),
inference(paramodulation,[status(thm)],[f275,f963]) ).
fof(f4763,plain,
! [X0,X1,X2] : multiply(difference(X0,difference(X1,X2)),multiply(X1,X2)) = difference(multiply(X0,multiply(X1,X2)),difference(X1,X2)),
inference(paramodulation,[status(thm)],[f214,f963]) ).
fof(f4815,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X1,X0))) = difference(multiply(X1,X2),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f2735,f4736]) ).
fof(f4842,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X1,X0))) = difference(multiply(X2,multiply(X0,X1)),difference(X1,X0)),
inference(forward_demodulation,[status(thm)],[f18,f4762]) ).
fof(f4844,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X0,X2)) = difference(multiply(X1,multiply(X2,X0)),difference(X0,X2)),
inference(forward_demodulation,[status(thm)],[f4815,f4842]) ).
fof(f4845,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),difference(X2,difference(X0,X1))) = difference(multiply(X2,multiply(X0,X1)),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f18,f4763]) ).
fof(f4847,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X0,X2)) = difference(multiply(X1,multiply(X0,X2)),difference(X0,X2)),
inference(forward_demodulation,[status(thm)],[f2174,f4845]) ).
fof(f4970,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X1,multiply(X0,X2))) = difference(difference(multiply(X0,X2),X1),difference(difference(X0,X2),difference(X1,multiply(X0,X2)))),
inference(paramodulation,[status(thm)],[f1358,f1074]) ).
fof(f5109,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X1,multiply(X0,X2))) = difference(difference(multiply(X0,X2),X1),difference(difference(X0,X1),multiply(X0,X2))),
inference(forward_demodulation,[status(thm)],[f841,f4970]) ).
fof(f5111,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X1,multiply(X0,X2))) = difference(multiply(X0,X2),difference(X1,difference(difference(X0,X1),multiply(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f843,f5109]) ).
fof(f6110,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(X0,X1),difference(difference(X2,multiply(X0,X1)),difference(multiply(X0,X1),multiply(X0,X1)))),multiply(multiply(X0,X1),difference(X3,X0))) = multiply(multiply(X0,X1),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f4626,f3179]) ).
fof(f6161,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(multiply(X1,X2),multiply(X1,X2))) = difference(difference(X0,X1),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f4626,f470]) ).
fof(f6458,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(X0,X1),difference(difference(X2,multiply(X0,X1)),multiply(X0,X1))),multiply(multiply(X0,X1),difference(X3,X0))) = multiply(multiply(X0,X1),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f8,f6110]) ).
fof(f6459,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),multiply(multiply(X0,X1),difference(X2,X0))) = multiply(multiply(X0,X1),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f6,f6458]) ).
fof(f6460,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X2,X0)) = multiply(multiply(X0,X1),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f380,f6459]) ).
fof(f6478,plain,
! [X0,X1,X2] : difference(X0,difference(X1,difference(X2,X0))) = difference(X0,multiply(X0,X1)),
inference(backward_demodulation,[status(thm)],[f6479,f1331]) ).
fof(f6479,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X2,X0)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f26,f6460]) ).
fof(f6605,plain,
! [X0,X1,X2] : difference(X0,X1) = difference(difference(X0,X1),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f361,f6161]) ).
fof(f6656,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),X2),difference(X2,X1)) = difference(difference(X0,X2),X1),
inference(backward_demodulation,[status(thm)],[f6721,f1902]) ).
fof(f6701,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),difference(difference(X3,multiply(X1,X2)),difference(difference(X1,X0),difference(X1,X2)))),difference(X0,X1)) = difference(multiply(X1,X0),difference(X1,X2)),
inference(backward_demodulation,[status(thm)],[f6721,f3401]) ).
fof(f6721,plain,
! [X0,X1,X2] : difference(X0,X1) = difference(difference(X0,X1),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f924,f6605]) ).
fof(f6956,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X3,multiply(X0,X2))) = difference(multiply(X0,X2),difference(X1,difference(X0,X2))),
inference(backward_demodulation,[status(thm)],[f6990,f2008]) ).
fof(f6957,plain,
! [X0,X1,X2] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X1,multiply(X0,X2))) = difference(multiply(X0,X2),X1),
inference(backward_demodulation,[status(thm)],[f6990,f5111]) ).
fof(f6969,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X1,X2)),difference(X0,multiply(X1,X2))) = multiply(multiply(X1,X2),X0),
inference(backward_demodulation,[status(thm)],[f6990,f3261]) ).
fof(f6970,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X1,X2)),difference(X0,multiply(X2,X1))) = multiply(multiply(X2,X1),X0),
inference(backward_demodulation,[status(thm)],[f6990,f3260]) ).
fof(f6990,plain,
! [X0,X1,X2] : difference(X0,difference(X1,difference(X2,X0))) = difference(X0,X1),
inference(forward_demodulation,[status(thm)],[f380,f6478]) ).
fof(f7113,plain,
! [X0,X1,X2] : difference(difference(X0,X1),X2) = difference(difference(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f6721,f6656]) ).
fof(f7189,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X1,X2)),difference(X0,X1)),difference(difference(X3,multiply(X1,X2)),difference(difference(X1,X0),difference(X1,X2)))) = difference(multiply(X1,X0),difference(X1,X2)),
inference(forward_demodulation,[status(thm)],[f7113,f6701]) ).
fof(f7293,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,X1),difference(X0,X2)),difference(X3,multiply(X0,X2))) = difference(difference(X0,X1),difference(X0,X2)),
inference(forward_demodulation,[status(thm)],[f844,f6956]) ).
fof(f7299,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(X0,X1),difference(X1,X2)),difference(difference(X3,multiply(X1,X2)),difference(difference(X1,X0),difference(X1,X2)))) = difference(multiply(X1,X0),difference(X1,X2)),
inference(backward_demodulation,[status(thm)],[f7350,f7189]) ).
fof(f7350,plain,
! [X0,X1,X2] : difference(difference(X0,X1),difference(X0,X2)) = difference(multiply(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f7293,f6957]) ).
fof(f7366,plain,
! [X0,X1,X2] : difference(multiply(X0,multiply(X1,X2)),difference(X1,X2)) = multiply(multiply(X1,X2),X0),
inference(forward_demodulation,[status(thm)],[f7350,f6969]) ).
fof(f7385,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X0,X2)) = multiply(multiply(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f4847,f7366]) ).
fof(f7386,plain,
! [X0,X1,X2] : difference(multiply(X0,multiply(X1,X2)),difference(X2,X1)) = multiply(multiply(X1,X2),X0),
inference(forward_demodulation,[status(thm)],[f7350,f6970]) ).
fof(f7387,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X0,X2)) = multiply(multiply(X2,X0),X1),
inference(forward_demodulation,[status(thm)],[f4844,f7386]) ).
fof(f7388,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(multiply(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f7385,f7387]) ).
fof(f7838,plain,
! [X0,X1,X2,X3] : difference(difference(difference(X0,difference(X0,X1)),difference(X2,multiply(X0,X1))),difference(difference(X0,X3),difference(X0,X1))) = difference(multiply(X0,X3),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f2685,f7299]) ).
fof(f7839,plain,
! [X0,X1,X2,X3] : difference(difference(multiply(X0,X1),difference(X2,multiply(X0,X1))),difference(difference(X0,X3),difference(X0,X1))) = difference(multiply(X0,X3),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f9,f7838]) ).
fof(f7840,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(difference(X0,X2),difference(X0,X1))) = difference(multiply(X0,X2),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f6,f7839]) ).
fof(f7841,plain,
! [X0,X1,X2] : difference(difference(X0,difference(X0,X1)),difference(X0,X2)) = difference(multiply(X0,X1),difference(X0,X2)),
inference(forward_demodulation,[status(thm)],[f844,f7840]) ).
fof(f7842,plain,
! [X0,X1,X2] : difference(multiply(X0,X1),difference(X0,X2)) = difference(multiply(X0,X2),difference(X0,X1)),
inference(forward_demodulation,[status(thm)],[f7350,f7841]) ).
fof(f7843,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = difference(multiply(X0,X1),difference(X0,X2)),
inference(forward_demodulation,[status(thm)],[f7385,f7842]) ).
fof(f7844,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(multiply(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f7385,f7843]) ).
fof(f9105,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(multiply(X1,X0),multiply(multiply(X0,X1),X2)),
inference(paramodulation,[status(thm)],[f329,f7388]) ).
fof(f9106,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X1,X0),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f26,f7388]) ).
fof(f9426,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X1,X0),X2),
inference(paramodulation,[status(thm)],[f18,f7844]) ).
fof(f9428,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(multiply(multiply(X1,X0),X2),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f9106,f7844]) ).
fof(f9527,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(multiply(X0,X1),X2),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f9426,f9428]) ).
fof(f9528,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X1,X0),multiply(multiply(X0,X1),X2)),
inference(forward_demodulation,[status(thm)],[f18,f9527]) ).
fof(f9529,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
inference(forward_demodulation,[status(thm)],[f9105,f9528]) ).
fof(f9530,plain,
multiply(a,multiply(c,b)) != multiply(a,multiply(b,c)),
inference(backward_demodulation,[status(thm)],[f9531,f17]) ).
fof(f9531,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X0,X2)),
inference(forward_demodulation,[status(thm)],[f9426,f9529]) ).
fof(f9742,plain,
multiply(a,multiply(b,c)) != multiply(a,multiply(b,c)),
inference(forward_demodulation,[status(thm)],[f18,f9530]) ).
fof(f9743,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f9742]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG005-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 12:55:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 13.53/2.27 % Refutation found
% 13.53/2.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 13.53/2.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.85/2.32 % Elapsed time: 1.952077 seconds
% 2.85/2.32 % CPU time: 15.274812 seconds
% 2.85/2.32 % Total memory used: 208.719 MB
% 2.85/2.32 % Net memory used: 201.004 MB
%------------------------------------------------------------------------------