%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO031-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 : n006.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:06:35 PM UTC 2026
% Result : Unsatisfiable 18.15s 3.18s
% Output : CNFRefutation 18.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 12
% Syntax : Number of formulae : 222 ( 222 unt; 0 def)
% Number of atoms : 222 ( 221 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 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 : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 577 ( 577 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] : add(multiply(X,Y),add(multiply(Y,Z),multiply(Z,X))) = multiply(add(X,Y),multiply(add(Y,Z),add(Z,X))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] : add(X,multiply(Y,multiply(X,Z))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : add(add(multiply(X,Y),multiply(Y,Z)),Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : multiply(add(X,inverse(X)),Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y,Z] : multiply(X,add(Y,add(X,Z))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : multiply(multiply(add(X,Y),add(Y,Z)),Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] : add(multiply(X,inverse(X)),Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] : add(X,inverse(X)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : multiply(X,inverse(X)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y,Z] : add(add(X,Y),Z) = add(X,add(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y,Z] : multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
multiply(a,add(b,c)) != add(multiply(b,a),multiply(c,a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))) = multiply(add(X0,X1),multiply(add(X1,X2),add(X2,X0))),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
! [X0,X1,X2] : add(X0,multiply(X1,multiply(X0,X2))) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f15,plain,
! [X0,X1,X2] : add(add(multiply(X0,X1),multiply(X1,X2)),X1) = X1,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f16,plain,
! [X0,X1] : multiply(add(X0,inverse(X0)),X1) = X1,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f17,plain,
! [X0,X1,X2] : multiply(X0,add(X1,add(X0,X2))) = X0,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f18,plain,
! [X0,X1,X2] : multiply(multiply(add(X0,X1),add(X1,X2)),X1) = X1,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f19,plain,
! [X0,X1] : add(multiply(X0,inverse(X0)),X1) = X1,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f20,plain,
! [X0] : add(X0,inverse(X0)) = n1,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f21,plain,
! [X0] : multiply(X0,inverse(X0)) = n0,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f22,plain,
! [X0,X1,X2] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f23,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f24,plain,
multiply(a,add(b,c)) != add(multiply(b,a),multiply(c,a)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f31,plain,
! [X0] : multiply(n1,X0) = X0,
inference(backward_demodulation,[status(thm)],[f20,f16]) ).
fof(f32,plain,
! [X0] : add(n0,X0) = X0,
inference(backward_demodulation,[status(thm)],[f21,f19]) ).
fof(f33,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,X2),X1)) = X1,
inference(backward_demodulation,[status(thm)],[f22,f15]) ).
fof(f34,plain,
! [X0,X1,X2] : multiply(add(X0,X1),multiply(add(X1,X2),X1)) = X1,
inference(backward_demodulation,[status(thm)],[f23,f18]) ).
fof(f35,plain,
! [X0,X1] : multiply(X0,add(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f14,f17]) ).
fof(f36,plain,
! [X0,X1] : add(X0,multiply(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f17,f14]) ).
fof(f42,plain,
! [X0,X1] : add(add(X0,X1),X1) = add(X0,X1),
inference(paramodulation,[status(thm)],[f35,f36]) ).
fof(f43,plain,
! [X0,X1] : multiply(multiply(X0,X1),X1) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f36,f35]) ).
fof(f47,plain,
! [X0,X1] : add(X0,add(X1,X1)) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f22,f42]) ).
fof(f48,plain,
! [X0,X1] : multiply(X0,multiply(X1,X1)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f23,f43]) ).
fof(f51,plain,
! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = add(X0,X0),
inference(paramodulation,[status(thm)],[f47,f35]) ).
fof(f56,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X0)),add(multiply(multiply(X1,X0),X2),multiply(X2,X0))) = multiply(X0,multiply(add(multiply(X1,X0),X2),add(X2,X0))),
inference(paramodulation,[status(thm)],[f36,f13]) ).
fof(f64,plain,
! [X0,X1,X2] : add(multiply(multiply(X0,X1),X2),add(multiply(X2,X1),multiply(X1,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),multiply(add(X2,X1),X1)),
inference(paramodulation,[status(thm)],[f36,f13]) ).
fof(f71,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X0)),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0))) = multiply(X0,multiply(add(multiply(X1,X0),X2),add(X2,X0))),
inference(forward_demodulation,[status(thm)],[f23,f56]) ).
fof(f86,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),multiply(add(X2,X1),X1)),
inference(forward_demodulation,[status(thm)],[f23,f64]) ).
fof(f89,plain,
! [X0] : add(multiply(X0,X0),add(multiply(X0,X0),multiply(X0,X0))) = multiply(add(X0,X0),add(X0,X0)),
inference(paramodulation,[status(thm)],[f13,f48]) ).
fof(f93,plain,
! [X0,X1] : add(multiply(X0,X0),multiply(X1,X0)) = multiply(X0,X0),
inference(paramodulation,[status(thm)],[f48,f36]) ).
fof(f95,plain,
! [X0] : add(multiply(X0,X0),multiply(X0,X0)) = multiply(add(X0,X0),add(X0,X0)),
inference(forward_demodulation,[status(thm)],[f47,f89]) ).
fof(f96,plain,
! [X0] : add(multiply(X0,X0),multiply(X0,X0)) = add(X0,X0),
inference(forward_demodulation,[status(thm)],[f51,f95]) ).
fof(f100,plain,
! [X0] : multiply(X0,X0) = add(X0,X0),
inference(backward_demodulation,[status(thm)],[f93,f96]) ).
fof(f109,plain,
! [X0,X1] : add(X0,add(multiply(X0,X1),multiply(X0,X1))) = X0,
inference(paramodulation,[status(thm)],[f100,f14]) ).
fof(f110,plain,
! [X0] : add(X0,add(X0,X0)) = X0,
inference(paramodulation,[status(thm)],[f100,f36]) ).
fof(f116,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f47,f109]) ).
fof(f117,plain,
! [X0] : multiply(X0,X0) = X0,
inference(backward_demodulation,[status(thm)],[f124,f100]) ).
fof(f124,plain,
! [X0] : add(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f47,f110]) ).
fof(f135,plain,
! [X0,X1] : multiply(X0,add(X0,X1)) = X0,
inference(paramodulation,[status(thm)],[f124,f17]) ).
fof(f137,plain,
! [X0,X1] : add(multiply(X0,X1),add(multiply(X1,X1),multiply(X1,X0))) = multiply(add(X0,X1),multiply(X1,add(X1,X0))),
inference(paramodulation,[status(thm)],[f124,f13]) ).
fof(f142,plain,
! [X0,X1] : add(multiply(X0,X1),add(X1,multiply(X1,X0))) = multiply(add(X0,X1),multiply(X1,add(X1,X0))),
inference(forward_demodulation,[status(thm)],[f117,f137]) ).
fof(f143,plain,
! [X0,X1] : add(multiply(X0,X1),X1) = multiply(add(X0,X1),multiply(X1,add(X1,X0))),
inference(forward_demodulation,[status(thm)],[f116,f142]) ).
fof(f145,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),add(multiply(X2,X1),X1)),
inference(backward_demodulation,[status(thm)],[f147,f86]) ).
fof(f147,plain,
! [X0,X1] : add(multiply(X0,X1),X1) = multiply(add(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f135,f143]) ).
fof(f156,plain,
! [X0,X1] : add(add(X0,X1),X0) = add(X0,X1),
inference(paramodulation,[status(thm)],[f135,f36]) ).
fof(f160,plain,
! [X0,X1] : add(X0,add(X1,X0)) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f22,f156]) ).
fof(f164,plain,
! [X0,X1,X2] : add(add(X0,X1),add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0)))) = add(X0,X1),
inference(paramodulation,[status(thm)],[f13,f116]) ).
fof(f172,plain,
! [X0,X1,X2] : add(multiply(multiply(X0,X1),X2),add(multiply(X2,X0),multiply(X0,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),multiply(add(X2,X0),X0)),
inference(paramodulation,[status(thm)],[f116,f13]) ).
fof(f173,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X1,X2)),multiply(multiply(X1,X2),X0))) = multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))),
inference(paramodulation,[status(thm)],[f116,f13]) ).
fof(f175,plain,
! [X0,X1] : multiply(multiply(X0,X1),X0) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f116,f35]) ).
fof(f177,plain,
! [X0,X1,X2] : add(X0,add(X1,add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))))) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f22,f164]) ).
fof(f178,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),multiply(add(X2,X0),X0)),
inference(forward_demodulation,[status(thm)],[f23,f172]) ).
fof(f179,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),add(multiply(X2,X0),X0)),
inference(forward_demodulation,[status(thm)],[f147,f178]) ).
fof(f180,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X1,X2)),multiply(X1,multiply(X2,X0)))) = multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))),
inference(forward_demodulation,[status(thm)],[f23,f173]) ).
fof(f182,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0))) = multiply(add(multiply(X0,X1),X2),add(multiply(X2,X1),X1)),
inference(backward_demodulation,[status(thm)],[f186,f145]) ).
fof(f184,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0))) = multiply(X0,multiply(add(multiply(X1,X0),X2),add(X2,X0))),
inference(backward_demodulation,[status(thm)],[f186,f71]) ).
fof(f186,plain,
! [X0,X1] : multiply(X0,multiply(X1,X0)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f23,f175]) ).
fof(f220,plain,
! [X0,X1] : add(multiply(X0,X1),multiply(X1,X0)) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f186,f36]) ).
fof(f408,plain,
! [X0,X1,X2] : add(X0,X1) = add(X0,add(multiply(X0,X2),X1)),
inference(paramodulation,[status(thm)],[f116,f22]) ).
fof(f409,plain,
! [X0,X1,X2] : add(X0,X1) = add(X0,add(multiply(X2,X0),X1)),
inference(paramodulation,[status(thm)],[f36,f22]) ).
fof(f410,plain,
! [X0,X1] : add(X0,X1) = add(X0,add(X0,X1)),
inference(paramodulation,[status(thm)],[f124,f22]) ).
fof(f421,plain,
! [X0,X1,X2] : add(multiply(add(X0,X1),X2),X2) = multiply(add(X0,add(X1,X2)),X2),
inference(paramodulation,[status(thm)],[f22,f147]) ).
fof(f428,plain,
! [X0,X1,X2] : multiply(X0,add(X1,add(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f22,f35]) ).
fof(f442,plain,
! [X0,X1,X2] : add(X0,add(X1,add(multiply(X1,X2),multiply(X2,X0)))) = add(X0,X1),
inference(backward_demodulation,[status(thm)],[f409,f177]) ).
fof(f469,plain,
! [X0,X1,X2] : add(X0,add(X1,multiply(X2,X0))) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f408,f442]) ).
fof(f484,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(X0,multiply(X1,add(X2,multiply(X0,X1)))),
inference(paramodulation,[status(thm)],[f35,f23]) ).
fof(f489,plain,
! [X0,X1,X2] : multiply(add(multiply(X0,X1),X1),X2) = multiply(add(X0,X1),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f147,f23]) ).
fof(f492,plain,
! [X0,X1,X2,X3] : multiply(X0,X1) = multiply(X0,multiply(add(X2,add(X0,X3)),X1)),
inference(paramodulation,[status(thm)],[f17,f23]) ).
fof(f493,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(X0,multiply(add(X0,X2),X1)),
inference(paramodulation,[status(thm)],[f135,f23]) ).
fof(f494,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(X0,multiply(add(X2,X0),X1)),
inference(paramodulation,[status(thm)],[f35,f23]) ).
fof(f495,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f117,f23]) ).
fof(f505,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X0,multiply(X1,X2))) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f23,f116]) ).
fof(f507,plain,
! [X0,X1,X2] : add(X0,multiply(X1,multiply(X2,X0))) = X0,
inference(paramodulation,[status(thm)],[f23,f36]) ).
fof(f532,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,X2),multiply(X1,multiply(X2,X0)))) = multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))),
inference(backward_demodulation,[status(thm)],[f495,f180]) ).
fof(f533,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,X1))) = multiply(add(multiply(X0,X1),X2),add(multiply(X2,X0),X0)),
inference(backward_demodulation,[status(thm)],[f495,f179]) ).
fof(f549,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))),
inference(forward_demodulation,[status(thm)],[f505,f532]) ).
fof(f553,plain,
! [X0] : multiply(inverse(X0),n0) = multiply(inverse(X0),X0),
inference(paramodulation,[status(thm)],[f21,f186]) ).
fof(f554,plain,
! [X0] : add(X0,n0) = X0,
inference(paramodulation,[status(thm)],[f21,f116]) ).
fof(f570,plain,
! [X0] : multiply(n0,X0) = n0,
inference(paramodulation,[status(thm)],[f554,f35]) ).
fof(f589,plain,
! [X0] : multiply(n1,X0) = multiply(X0,n1),
inference(paramodulation,[status(thm)],[f186,f31]) ).
fof(f591,plain,
! [X0] : n1 = add(n1,X0),
inference(paramodulation,[status(thm)],[f135,f31]) ).
fof(f592,plain,
! [X0] : n1 = add(X0,n1),
inference(paramodulation,[status(thm)],[f35,f31]) ).
fof(f606,plain,
! [X0] : X0 = multiply(X0,n1),
inference(forward_demodulation,[status(thm)],[f31,f589]) ).
fof(f745,plain,
! [X0,X1] : n0 = multiply(X0,multiply(n0,X1)),
inference(paramodulation,[status(thm)],[f14,f32]) ).
fof(f770,plain,
! [X0] : n0 = multiply(inverse(X0),X0),
inference(backward_demodulation,[status(thm)],[f773,f553]) ).
fof(f773,plain,
! [X0] : n0 = multiply(X0,n0),
inference(forward_demodulation,[status(thm)],[f570,f745]) ).
fof(f989,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,add(X1,X2)),multiply(add(X1,X2),X0))) = multiply(add(X0,X1),multiply(add(X1,X2),add(add(X1,X2),X0))),
inference(paramodulation,[status(thm)],[f410,f13]) ).
fof(f1025,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(X1,multiply(add(X1,X2),X0))) = multiply(add(X0,X1),multiply(add(X1,X2),add(add(X1,X2),X0))),
inference(forward_demodulation,[status(thm)],[f135,f989]) ).
fof(f1026,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(X1,multiply(add(X1,X2),X0))) = multiply(add(X0,X1),add(X1,X2)),
inference(forward_demodulation,[status(thm)],[f135,f1025]) ).
fof(f1137,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),add(X2,X0)) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f116,f428]) ).
fof(f1163,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0))) = multiply(X0,add(multiply(X1,X0),X2)),
inference(backward_demodulation,[status(thm)],[f1165,f184]) ).
fof(f1165,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X0))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f23,f1137]) ).
fof(f1263,plain,
! [X0,X1] : add(n0,add(multiply(X0,X1),X0)) = X0,
inference(paramodulation,[status(thm)],[f770,f33]) ).
fof(f1266,plain,
! [X0,X1,X2,X3] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X3),X2)) = X2,
inference(paramodulation,[status(thm)],[f23,f33]) ).
fof(f1268,plain,
! [X0,X1,X2] : add(add(multiply(X0,X1),X1),add(multiply(X1,X2),X1)) = X1,
inference(paramodulation,[status(thm)],[f147,f33]) ).
fof(f1311,plain,
! [X0,X1,X2,X3] : add(multiply(multiply(X0,X1),add(multiply(X1,X2),X1)),add(multiply(add(multiply(X1,X2),X1),X3),multiply(X3,multiply(X0,X1)))) = multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))),
inference(paramodulation,[status(thm)],[f33,f13]) ).
fof(f1318,plain,
! [X0,X1] : add(multiply(X0,X1),X0) = X0,
inference(forward_demodulation,[status(thm)],[f32,f1263]) ).
fof(f1321,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),X2) = X2,
inference(forward_demodulation,[status(thm)],[f1318,f1266]) ).
fof(f1325,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(X1,add(multiply(X1,X2),X1))) = X1,
inference(forward_demodulation,[status(thm)],[f22,f1268]) ).
fof(f1326,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(X1,multiply(X1,X2))) = X1,
inference(forward_demodulation,[status(thm)],[f160,f1325]) ).
fof(f1327,plain,
! [X0,X1] : X0 = multiply(add(X1,X0),X0),
inference(backward_demodulation,[status(thm)],[f1344,f147]) ).
fof(f1329,plain,
! [X0,X1,X2] : X0 = multiply(add(X1,add(X2,X0)),X0),
inference(backward_demodulation,[status(thm)],[f1344,f421]) ).
fof(f1337,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,X1))) = multiply(add(multiply(X0,X1),X2),X0),
inference(backward_demodulation,[status(thm)],[f1344,f533]) ).
fof(f1339,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(add(X2,X0),multiply(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1344,f489]) ).
fof(f1342,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0))) = multiply(add(multiply(X0,X1),X2),X1),
inference(backward_demodulation,[status(thm)],[f1344,f182]) ).
fof(f1344,plain,
! [X0,X1] : add(multiply(X0,X1),X1) = X1,
inference(forward_demodulation,[status(thm)],[f116,f1326]) ).
fof(f1405,plain,
! [X0,X1,X2,X3] : add(multiply(X0,multiply(X1,add(multiply(X1,X2),X1))),add(multiply(add(multiply(X1,X2),X1),X3),multiply(X3,multiply(X0,X1)))) = multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f23,f1311]) ).
fof(f1406,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),add(multiply(add(multiply(X1,X2),X1),X3),multiply(X3,multiply(X0,X1)))) = multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f35,f1405]) ).
fof(f1407,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),multiply(add(multiply(X1,X2),X1),X3)) = multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f469,f1406]) ).
fof(f1408,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(X1,multiply(add(add(multiply(X1,X3),X1),X2),add(X2,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f1318,f1407]) ).
fof(f1409,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(X1,multiply(add(multiply(X1,X3),add(X1,X2)),add(X2,multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f22,f1408]) ).
fof(f1410,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(X0,add(multiply(X0,X1),multiply(X1,X2))),
inference(backward_demodulation,[status(thm)],[f1411,f484]) ).
fof(f1411,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(X1,add(X2,multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f492,f1409]) ).
fof(f1419,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(X1,add(multiply(X1,X2),X0)),
inference(backward_demodulation,[status(thm)],[f1339,f549]) ).
fof(f1422,plain,
! [X0,X1,X2] : multiply(X0,X1) = add(multiply(multiply(X1,X2),X0),multiply(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1419,f1410]) ).
fof(f1424,plain,
! [X0,X1,X2] : multiply(X0,X1) = add(multiply(X1,multiply(X2,X0)),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f23,f1422]) ).
fof(f1428,plain,
! [X0,X1] : multiply(n1,multiply(add(X0,X1),X0)) = X0,
inference(paramodulation,[status(thm)],[f591,f34]) ).
fof(f1438,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(add(multiply(X1,multiply(X2,X0)),X3),multiply(X1,multiply(X2,X0)))) = multiply(X1,multiply(X2,X0)),
inference(paramodulation,[status(thm)],[f507,f34]) ).
fof(f1479,plain,
! [X0,X1] : multiply(add(X0,X1),X0) = X0,
inference(forward_demodulation,[status(thm)],[f31,f1428]) ).
fof(f1492,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,multiply(X2,X0))) = multiply(X1,multiply(X2,X0)),
inference(forward_demodulation,[status(thm)],[f1479,f1438]) ).
fof(f1830,plain,
! [X0,X1,X2] : add(X0,X1) = add(multiply(X2,X0),add(X0,X1)),
inference(paramodulation,[status(thm)],[f1344,f22]) ).
fof(f1842,plain,
! [X0,X1,X2] : add(X0,multiply(add(X0,X1),X2)) = multiply(add(X2,X0),add(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1830,f1026]) ).
fof(f1862,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))) = multiply(add(X0,X1),add(X2,multiply(add(X2,X0),X1))),
inference(backward_demodulation,[status(thm)],[f1842,f13]) ).
fof(f1946,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f36,f1327]) ).
fof(f2015,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(add(X0,X2),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f1479,f23]) ).
fof(f2135,plain,
! [X0,X1] : multiply(X0,multiply(X1,X0)) = multiply(multiply(X1,X0),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f186,f1946]) ).
fof(f2181,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1946,f2135]) ).
fof(f2182,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f23,f2181]) ).
fof(f2183,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1492,f2182]) ).
fof(f2216,plain,
! [X0,X1] : add(multiply(X0,n1),add(multiply(n1,X1),multiply(X1,X0))) = multiply(n1,add(X1,multiply(add(X1,X0),n1))),
inference(paramodulation,[status(thm)],[f592,f1862]) ).
fof(f2225,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X0)),add(multiply(multiply(X1,X0),X2),multiply(X2,X0))) = multiply(X0,add(X2,multiply(add(X2,X0),multiply(X1,X0)))),
inference(paramodulation,[status(thm)],[f36,f1862]) ).
fof(f2231,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(multiply(X1,X2),X1),multiply(X1,X0))) = multiply(add(X0,multiply(X1,X2)),X1),
inference(paramodulation,[status(thm)],[f14,f1862]) ).
fof(f2247,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(multiply(X0,X2),X0))) = multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f1318,f1862]) ).
fof(f2264,plain,
! [X0,X1,X2] : add(multiply(multiply(X0,X1),X2),add(multiply(X2,X1),multiply(X1,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),add(X1,multiply(X1,X2))),
inference(paramodulation,[status(thm)],[f36,f1862]) ).
fof(f2268,plain,
! [X0,X1,X2] : add(add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))),add(X0,X1)) = add(X0,X1),
inference(paramodulation,[status(thm)],[f1862,f1318]) ).
fof(f2316,plain,
! [X0,X1] : add(X0,add(multiply(n1,X1),multiply(X1,X0))) = multiply(n1,add(X1,multiply(add(X1,X0),n1))),
inference(forward_demodulation,[status(thm)],[f606,f2216]) ).
fof(f2317,plain,
! [X0,X1] : add(X0,multiply(n1,X1)) = multiply(n1,add(X1,multiply(add(X1,X0),n1))),
inference(forward_demodulation,[status(thm)],[f469,f2316]) ).
fof(f2318,plain,
! [X0,X1] : add(X0,X1) = multiply(n1,add(X1,multiply(add(X1,X0),n1))),
inference(forward_demodulation,[status(thm)],[f31,f2317]) ).
fof(f2319,plain,
! [X0,X1] : add(X0,X1) = add(X1,multiply(add(X1,X0),n1)),
inference(forward_demodulation,[status(thm)],[f31,f2318]) ).
fof(f2320,plain,
! [X0,X1] : add(X0,X1) = add(X1,add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f606,f2319]) ).
fof(f2349,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(multiply(X0,X1),X2),multiply(X2,X1))) = multiply(X1,add(X2,multiply(add(X2,X1),multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f1946,f2225]) ).
fof(f2350,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(X1,add(X2,multiply(add(X2,X1),multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f408,f2349]) ).
fof(f2369,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X1,multiply(X2,X1)),multiply(X1,X0))) = multiply(add(X0,multiply(X1,X2)),X1),
inference(forward_demodulation,[status(thm)],[f23,f2231]) ).
fof(f2370,plain,
! [X0,X1,X2] : multiply(add(X0,multiply(X1,X2)),X1) = multiply(add(multiply(X0,X1),X2),X1),
inference(backward_demodulation,[status(thm)],[f2371,f1342]) ).
fof(f2371,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0))) = multiply(add(X0,multiply(X1,X2)),X1),
inference(forward_demodulation,[status(thm)],[f1946,f2369]) ).
fof(f2452,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X0,multiply(X2,X0)))) = multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f23,f2247]) ).
fof(f2453,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0))) = multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1946,f2452]) ).
fof(f2454,plain,
! [X0,X1,X2] : multiply(X0,add(multiply(X1,X0),X2)) = multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1163,f2453]) ).
fof(f2518,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),X2),add(X1,multiply(X1,X2))),
inference(forward_demodulation,[status(thm)],[f23,f2264]) ).
fof(f2519,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X0,X1))) = multiply(add(multiply(X0,X1),X2),add(X1,multiply(X1,X2))),
inference(forward_demodulation,[status(thm)],[f1946,f2518]) ).
fof(f2520,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X0,X1))) = multiply(add(multiply(X0,X1),X2),X1),
inference(forward_demodulation,[status(thm)],[f116,f2519]) ).
fof(f2529,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(add(multiply(X1,X2),multiply(X2,X0)),add(X0,X1))) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f22,f2268]) ).
fof(f2530,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,X2),add(multiply(X2,X0),add(X0,X1)))) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f22,f2529]) ).
fof(f2533,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,X2),add(X0,X1))) = add(X0,X1),
inference(forward_demodulation,[status(thm)],[f1830,f2530]) ).
fof(f2558,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X0,X1))) = multiply(add(X0,multiply(X1,X2)),X1),
inference(backward_demodulation,[status(thm)],[f2370,f2520]) ).
fof(f2586,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),multiply(X2,X1)) = multiply(X2,X1),
inference(paramodulation,[status(thm)],[f186,f1321]) ).
fof(f2587,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),add(X2,add(X3,X1))) = add(X2,add(X3,X1)),
inference(paramodulation,[status(thm)],[f428,f1321]) ).
fof(f2615,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X0)) = multiply(X0,add(multiply(X1,X0),X2)),
inference(backward_demodulation,[status(thm)],[f2586,f1163]) ).
fof(f2617,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(X2,X0)) = add(X2,X0),
inference(backward_demodulation,[status(thm)],[f2587,f2533]) ).
fof(f2634,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X0)) = multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))),
inference(backward_demodulation,[status(thm)],[f2615,f2454]) ).
fof(f3006,plain,
! [X0,X1,X2] : add(multiply(X0,add(X0,X1)),add(multiply(add(X0,X1),X2),multiply(X2,X0))) = multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))),
inference(paramodulation,[status(thm)],[f2320,f1862]) ).
fof(f3081,plain,
! [X0,X1,X2] : add(X0,add(multiply(add(X0,X1),X2),multiply(X2,X0))) = multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f135,f3006]) ).
fof(f3082,plain,
! [X0,X1,X2] : add(X0,multiply(add(X0,X1),X2)) = multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f469,f3081]) ).
fof(f3083,plain,
! [X0,X1,X2] : add(X0,multiply(add(X0,X1),X2)) = multiply(add(X1,X0),add(X2,add(X0,multiply(add(X0,X1),X2)))),
inference(forward_demodulation,[status(thm)],[f1842,f3082]) ).
fof(f3084,plain,
! [X0,X1,X2] : add(X0,multiply(add(X0,X1),X2)) = multiply(add(X1,X0),add(X2,X0)),
inference(forward_demodulation,[status(thm)],[f469,f3083]) ).
fof(f3139,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(add(X2,X1),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f36,f1329]) ).
fof(f3176,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(X1,add(X2,multiply(X0,X1))),
inference(backward_demodulation,[status(thm)],[f3139,f2350]) ).
fof(f3899,plain,
! [X0,X1,X2] : add(multiply(multiply(add(X0,X1),X2),X0),multiply(X0,X2)) = multiply(multiply(add(X0,X1),X2),X0),
inference(paramodulation,[status(thm)],[f493,f220]) ).
fof(f3914,plain,
! [X0,X1,X2] : add(multiply(add(X0,X1),X2),multiply(X0,X2)) = multiply(add(X0,X1),X2),
inference(paramodulation,[status(thm)],[f493,f36]) ).
fof(f3973,plain,
! [X0,X1,X2] : add(multiply(add(X0,X1),multiply(X2,X0)),multiply(X0,X2)) = multiply(multiply(add(X0,X1),X2),X0),
inference(forward_demodulation,[status(thm)],[f23,f3899]) ).
fof(f3974,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(multiply(add(X0,X2),X1),X0),
inference(forward_demodulation,[status(thm)],[f2586,f3973]) ).
fof(f3975,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(add(X0,X2),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f23,f3974]) ).
fof(f5499,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X0,X1)),add(multiply(multiply(X0,X1),X2),multiply(X2,X0))) = multiply(add(X0,multiply(X0,X1)),add(X2,multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f1339,f1862]) ).
fof(f5596,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(multiply(X1,X0),X2),multiply(X2,X1))) = multiply(add(X1,multiply(X1,X0)),add(X2,multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2183,f5499]) ).
fof(f5597,plain,
! [X0,X1,X2] : add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X1))) = multiply(add(X1,multiply(X1,X0)),add(X2,multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f23,f5596]) ).
fof(f5598,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X1,multiply(X1,X0)),add(X2,multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f1424,f5597]) ).
fof(f5599,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = add(multiply(X1,X0),multiply(add(multiply(X1,X0),X1),X2)),
inference(forward_demodulation,[status(thm)],[f3084,f5598]) ).
fof(f5600,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = add(multiply(X1,X0),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f1318,f5599]) ).
fof(f6085,plain,
! [X0,X1,X2] : multiply(X0,add(X1,multiply(add(X1,X2),X0))) = multiply(X0,add(multiply(X2,X0),add(multiply(X0,X1),multiply(X1,X2)))),
inference(paramodulation,[status(thm)],[f1862,f494]) ).
fof(f6184,plain,
! [X0,X1,X2] : add(multiply(add(X0,X1),X2),multiply(X0,X2)) = multiply(X2,add(multiply(X1,X2),add(multiply(X2,X0),multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f3176,f6085]) ).
fof(f6185,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = multiply(X2,add(multiply(X1,X2),add(multiply(X2,X0),multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f3914,f6184]) ).
fof(f6187,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X2,X1),multiply(add(multiply(X2,X0),multiply(X0,X1)),X2)),
inference(forward_demodulation,[status(thm)],[f2615,f6185]) ).
fof(f6726,plain,
! [X0,X1,X2,X3] : add(multiply(X0,multiply(X1,X2)),add(X3,multiply(X0,X1))) = add(X3,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f23,f2617]) ).
fof(f6831,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X2,multiply(X1,X0)),X1),
inference(backward_demodulation,[status(thm)],[f6726,f2558]) ).
fof(f6832,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(add(multiply(X1,X2),X0),X1),
inference(backward_demodulation,[status(thm)],[f6726,f1337]) ).
fof(f6928,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0))) = add(multiply(X2,X1),multiply(X0,X1)),
inference(backward_demodulation,[status(thm)],[f6831,f2371]) ).
fof(f6929,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X2,X1),add(multiply(multiply(X0,X1),X2),multiply(X2,X0))),
inference(backward_demodulation,[status(thm)],[f6832,f6187]) ).
fof(f6935,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X2,X1),add(multiply(X0,multiply(X1,X2)),multiply(X2,X0))),
inference(forward_demodulation,[status(thm)],[f23,f6929]) ).
fof(f6938,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X2,X0),X1),
inference(backward_demodulation,[status(thm)],[f6940,f5600]) ).
fof(f6939,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X0)) = multiply(add(X0,X1),multiply(add(X1,X2),X0)),
inference(backward_demodulation,[status(thm)],[f6940,f2634]) ).
fof(f6940,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X2,X1),multiply(X2,X0)),
inference(forward_demodulation,[status(thm)],[f1424,f6935]) ).
fof(f6943,plain,
multiply(a,add(b,c)) != multiply(add(c,b),a),
inference(backward_demodulation,[status(thm)],[f6938,f24]) ).
fof(f6948,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0))) = multiply(add(X0,X2),X1),
inference(backward_demodulation,[status(thm)],[f6938,f6928]) ).
fof(f6951,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = multiply(add(X0,multiply(X2,X1)),X2),
inference(backward_demodulation,[status(thm)],[f6938,f6831]) ).
fof(f6956,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = multiply(X2,add(X0,multiply(X1,X2))),
inference(backward_demodulation,[status(thm)],[f6938,f3176]) ).
fof(f6970,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,X0)) = multiply(X0,add(X1,X2)),
inference(forward_demodulation,[status(thm)],[f3975,f6939]) ).
fof(f6979,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(X1,X2)) = multiply(add(X2,X0),X1),
inference(backward_demodulation,[status(thm)],[f6956,f1411]) ).
fof(f6994,plain,
! [X0,X1,X2] : add(multiply(X0,X1),multiply(add(X0,X1),X2)) = multiply(add(X0,X1),add(X2,multiply(add(X2,X0),X1))),
inference(backward_demodulation,[status(thm)],[f6979,f1862]) ).
fof(f7037,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),multiply(add(X0,X2),X1)) = multiply(add(X0,X2),X1),
inference(backward_demodulation,[status(thm)],[f6979,f6948]) ).
fof(f7634,plain,
! [X0,X1,X2] : add(multiply(X0,add(X0,X1)),multiply(add(X0,add(X0,X1)),X2)) = multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))),
inference(paramodulation,[status(thm)],[f2320,f6994]) ).
fof(f7655,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),multiply(add(X0,multiply(X1,X2)),X1)) = multiply(add(X0,multiply(X1,X2)),add(X1,multiply(X1,X2))),
inference(paramodulation,[status(thm)],[f2015,f6994]) ).
fof(f7833,plain,
! [X0,X1,X2] : add(X0,multiply(add(X0,add(X0,X1)),X2)) = multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f135,f7634]) ).
fof(f7834,plain,
! [X0,X1,X2] : add(X0,multiply(add(X1,X0),X2)) = multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f2320,f7833]) ).
fof(f7835,plain,
! [X0,X1,X2] : add(X0,multiply(add(X1,X0),X2)) = multiply(add(X1,X0),add(X2,add(X0,multiply(add(X0,X1),X2)))),
inference(forward_demodulation,[status(thm)],[f1842,f7834]) ).
fof(f7836,plain,
! [X0,X1,X2] : add(X0,multiply(add(X1,X0),X2)) = multiply(add(X1,X0),add(X2,X0)),
inference(forward_demodulation,[status(thm)],[f469,f7835]) ).
fof(f7909,plain,
! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),multiply(add(X0,X2),X1)) = multiply(add(X0,multiply(X1,X2)),add(X1,multiply(X1,X2))),
inference(forward_demodulation,[status(thm)],[f6951,f7655]) ).
fof(f7910,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = multiply(add(X0,multiply(X2,X1)),add(X2,multiply(X2,X1))),
inference(forward_demodulation,[status(thm)],[f7037,f7909]) ).
fof(f7911,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = add(multiply(X2,X1),multiply(add(X0,multiply(X2,X1)),X2)),
inference(forward_demodulation,[status(thm)],[f7836,f7910]) ).
fof(f7912,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = multiply(X2,add(X1,add(X0,multiply(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f6970,f7911]) ).
fof(f7914,plain,
! [X0,X1,X2] : multiply(add(X0,X1),X2) = multiply(X2,add(X1,X0)),
inference(forward_demodulation,[status(thm)],[f469,f7912]) ).
fof(f7915,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f6943,f7914]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n006.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 13:49:14 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 18.15/3.18 % Refutation found
% 18.15/3.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.15/3.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.20/3.28 % Elapsed time: 2.786996 seconds
% 8.20/3.28 % CPU time: 21.443226 seconds
% 8.20/3.28 % Total memory used: 177.127 MB
% 8.20/3.28 % Net memory used: 172.426 MB
%------------------------------------------------------------------------------