%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO007-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:43 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO007-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n006.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 13:46:57 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.35 % Drodi V4.1.1
% 0.13/0.58 % Refutation found
% 0.13/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.58 fof(f1,axiom,(
% 0.13/0.58 (![X,Y]: (add(X,Y) = add(Y,X) ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f2,axiom,(
% 0.13/0.58 (![X,Y]: (multiply(X,Y) = multiply(Y,X) ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f3,axiom,(
% 0.13/0.58 (![X,Y,Z]: (add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f4,axiom,(
% 0.13/0.58 (![X,Y,Z]: (multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f5,axiom,(
% 0.13/0.58 (![X]: (add(X,additive_identity) = X ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f6,axiom,(
% 0.13/0.58 (![X]: (multiply(X,multiplicative_identity) = X ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f7,axiom,(
% 0.13/0.58 (![X]: (add(X,inverse(X)) = multiplicative_identity ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f8,axiom,(
% 0.13/0.58 (![X]: (multiply(X,inverse(X)) = additive_identity ))),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f9,negated_conjecture,(
% 0.13/0.58 multiply(a,multiply(b,c)) != multiply(multiply(a,b),c) ),
% 0.13/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.58 fof(f10,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.58 fof(f11,plain,(
% 0.13/0.58 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.58 fof(f12,plain,(
% 0.13/0.58 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X0,X1),add(X0,X2)))),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.58 fof(f13,plain,(
% 0.13/0.58 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X0,X1),multiply(X0,X2)))),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.58 fof(f14,plain,(
% 0.13/0.58 ![X0]: (add(X0,additive_identity)=X0)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.58 fof(f15,plain,(
% 0.13/0.58 ![X0]: (multiply(X0,multiplicative_identity)=X0)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.58 fof(f16,plain,(
% 0.13/0.58 ![X0]: (add(X0,inverse(X0))=multiplicative_identity)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.58 fof(f17,plain,(
% 0.13/0.58 ![X0]: (multiply(X0,inverse(X0))=additive_identity)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.58 fof(f18,plain,(
% 0.13/0.58 ~multiply(a,multiply(b,c))=multiply(multiply(a,b),c)),
% 0.13/0.58 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.58 fof(f19,definition,(
% 0.13/0.58 sF1_fnc=multiply(b,c)),
% 0.13/0.58 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.13/0.58 fof(f20,definition,(
% 0.13/0.58 sF0_fnc=multiply(a,sF1_fnc)),
% 0.13/0.58 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.13/0.58 fof(f21,definition,(
% 0.13/0.58 sF3_fnc=multiply(a,b)),
% 0.13/0.58 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.13/0.58 fof(f22,definition,(
% 0.13/0.58 sF2_fnc=multiply(sF3_fnc,c)),
% 0.13/0.58 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.13/0.58 fof(f23,plain,(
% 0.13/0.58 ~sF0_fnc=sF2_fnc),
% 0.13/0.58 inference(definition_folding,[],[f18,f22,f21,f20,f19])).
% 0.13/0.58 fof(f24,plain,(
% 0.13/0.58 sF2_fnc=multiply(c,sF3_fnc)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f11,f22])).
% 0.13/0.58 fof(f37,plain,(
% 0.13/0.58 ![X0]: (multiply(multiplicative_identity,X0)=X0)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f11,f15])).
% 0.13/0.58 fof(f56,plain,(
% 0.13/0.58 inverse(multiplicative_identity)=additive_identity),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f37,f17])).
% 0.13/0.58 fof(f61,plain,(
% 0.13/0.58 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X0,X2),add(X0,X1)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f11,f12])).
% 0.13/0.58 fof(f64,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(inverse(X0),X1))=multiply(multiplicative_identity,add(X0,X1)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f16,f12])).
% 0.13/0.58 fof(f66,plain,(
% 0.13/0.58 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X1,X0),add(X0,X2)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f10,f12])).
% 0.13/0.58 fof(f69,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X1,inverse(X0)))=multiply(add(X0,X1),multiplicative_identity))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f16,f12])).
% 0.13/0.58 fof(f70,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X1,additive_identity))=multiply(add(X0,X1),X0))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f14,f12])).
% 0.13/0.58 fof(f76,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(inverse(X0),X1))=add(X0,X1))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f37,f64])).
% 0.13/0.58 fof(f78,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X1,inverse(X0)))=add(X0,X1))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f15,f69])).
% 0.13/0.58 fof(f79,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X1,additive_identity))=multiply(X0,add(X0,X1)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f11,f70])).
% 0.13/0.58 fof(f82,plain,(
% 0.13/0.58 ![X0]: (add(X0,inverse(X0))=add(X0,multiplicative_identity))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f15,f76])).
% 0.13/0.58 fof(f93,plain,(
% 0.13/0.58 ![X0]: (multiplicative_identity=add(X0,multiplicative_identity))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f16,f82])).
% 0.13/0.58 fof(f101,plain,(
% 0.13/0.58 ![X0]: (multiplicative_identity=add(multiplicative_identity,X0))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f10,f93])).
% 0.13/0.58 fof(f129,plain,(
% 0.13/0.58 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=add(X0,multiply(X2,X1)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f12,f61])).
% 0.13/0.58 fof(f172,plain,(
% 0.13/0.58 ![X0]: (add(X0,multiply(additive_identity,additive_identity))=multiply(X0,X0))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f14,f79])).
% 0.13/0.58 fof(f213,plain,(
% 0.13/0.58 ![X0]: (add(X0,additive_identity)=add(X0,X0))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f17,f78])).
% 0.13/0.58 fof(f229,plain,(
% 0.13/0.58 ![X0]: (X0=add(X0,X0))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f14,f213])).
% 0.13/0.58 fof(f251,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X0,X1))=multiply(add(X0,X1),X0))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f229,f61])).
% 0.13/0.58 fof(f252,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X1,X0))=multiply(X0,add(X0,X1)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f229,f61])).
% 0.13/0.58 fof(f255,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X0,X1))=multiply(X0,add(X0,X1)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f11,f251])).
% 0.13/0.58 fof(f298,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X0,X1))=add(X0,multiply(X1,additive_identity)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f79,f255])).
% 0.13/0.58 fof(f310,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X0,X1))=multiply(X0,add(X1,X0)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f10,f255])).
% 0.13/0.58 fof(f444,plain,(
% 0.13/0.58 ![X0]: (add(inverse(X0),multiply(inverse(X0),X0))=multiply(inverse(X0),multiplicative_identity))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f16,f310])).
% 0.13/0.58 fof(f484,plain,(
% 0.13/0.58 ![X0]: (add(inverse(X0),multiply(X0,additive_identity))=multiply(inverse(X0),multiplicative_identity))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f298,f444])).
% 0.13/0.58 fof(f485,plain,(
% 0.13/0.58 ![X0]: (add(inverse(X0),multiply(X0,additive_identity))=inverse(X0))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f15,f484])).
% 0.13/0.58 fof(f502,plain,(
% 0.13/0.58 ![X0]: (add(inverse(X0),multiply(additive_identity,X0))=inverse(X0))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f11,f485])).
% 0.13/0.58 fof(f553,plain,(
% 0.13/0.58 ![X0]: (add(multiply(additive_identity,X0),multiply(multiply(additive_identity,X0),inverse(X0)))=multiply(multiply(additive_identity,X0),inverse(X0)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f502,f310])).
% 0.13/0.58 fof(f580,plain,(
% 0.13/0.58 ![X0]: (add(multiply(additive_identity,X0),multiply(inverse(X0),additive_identity))=multiply(multiply(additive_identity,X0),inverse(X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f298,f553])).
% 0.13/0.58 fof(f581,plain,(
% 0.13/0.58 ![X0]: (add(multiply(additive_identity,X0),multiply(additive_identity,inverse(X0)))=multiply(multiply(additive_identity,X0),inverse(X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f129,f580])).
% 0.13/0.58 fof(f582,plain,(
% 0.13/0.58 ![X0]: (multiply(additive_identity,add(X0,inverse(X0)))=multiply(multiply(additive_identity,X0),inverse(X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f13,f581])).
% 0.13/0.58 fof(f583,plain,(
% 0.13/0.58 ![X0]: (multiply(additive_identity,multiplicative_identity)=multiply(multiply(additive_identity,X0),inverse(X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f16,f582])).
% 0.13/0.58 fof(f584,plain,(
% 0.13/0.58 ![X0]: (additive_identity=multiply(multiply(additive_identity,X0),inverse(X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f15,f583])).
% 0.13/0.58 fof(f585,plain,(
% 0.13/0.58 ![X0]: (additive_identity=multiply(inverse(X0),multiply(additive_identity,X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f11,f584])).
% 0.13/0.58 fof(f602,plain,(
% 0.13/0.58 additive_identity=multiply(additive_identity,multiply(additive_identity,multiplicative_identity))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f56,f585])).
% 0.13/0.58 fof(f613,plain,(
% 0.13/0.58 ![X0]: (add(X0,additive_identity)=multiply(X0,X0))),
% 0.13/0.58 inference(backward_demodulation,[status(thm)],[f626,f172])).
% 0.13/0.58 fof(f626,plain,(
% 0.13/0.58 additive_identity=multiply(additive_identity,additive_identity)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f15,f602])).
% 0.13/0.58 fof(f668,plain,(
% 0.13/0.58 ![X0]: (X0=multiply(X0,X0))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f14,f613])).
% 0.13/0.58 fof(f872,plain,(
% 0.13/0.58 ![X0]: (multiply(a,add(b,X0))=add(sF3_fnc,multiply(a,X0)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f21,f13])).
% 0.13/0.58 fof(f873,plain,(
% 0.13/0.58 ![X0]: (multiply(a,add(sF1_fnc,X0))=add(sF0_fnc,multiply(a,X0)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f20,f13])).
% 0.13/0.58 fof(f881,plain,(
% 0.13/0.58 ![X0,X1]: (multiply(X0,add(multiplicative_identity,X1))=add(X0,multiply(X0,X1)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f15,f13])).
% 0.13/0.58 fof(f882,plain,(
% 0.13/0.58 ![X0,X1]: (multiply(X0,add(X0,X1))=add(X0,multiply(X0,X1)))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f668,f13])).
% 0.13/0.58 fof(f890,plain,(
% 0.13/0.58 ![X0]: (multiply(c,add(X0,sF3_fnc))=add(multiply(c,X0),sF2_fnc))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f24,f13])).
% 0.13/0.58 fof(f924,plain,(
% 0.13/0.58 ![X0,X1]: (multiply(X0,multiplicative_identity)=add(X0,multiply(X0,X1)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f101,f881])).
% 0.13/0.58 fof(f926,plain,(
% 0.13/0.58 ![X0,X1]: (X0=multiply(X0,add(X1,X0)))),
% 0.13/0.58 inference(backward_demodulation,[status(thm)],[f933,f310])).
% 0.13/0.58 fof(f933,plain,(
% 0.13/0.58 ![X0,X1]: (X0=add(X0,multiply(X0,X1)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f15,f924])).
% 0.13/0.58 fof(f934,plain,(
% 0.13/0.58 ![X0,X1]: (add(X0,multiply(X1,X0))=X0)),
% 0.13/0.58 inference(backward_demodulation,[status(thm)],[f937,f252])).
% 0.13/0.58 fof(f937,plain,(
% 0.13/0.58 ![X0,X1]: (multiply(X0,add(X0,X1))=X0)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f933,f882])).
% 0.13/0.58 fof(f943,plain,(
% 0.13/0.58 ![X0]: (multiply(c,add(X0,sF3_fnc))=add(sF2_fnc,multiply(c,X0)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f10,f890])).
% 0.13/0.58 fof(f1504,plain,(
% 0.13/0.58 a=add(a,sF3_fnc)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f21,f933])).
% 0.13/0.58 fof(f1506,plain,(
% 0.13/0.58 b=add(b,sF1_fnc)),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f19,f933])).
% 0.13/0.58 fof(f1600,plain,(
% 0.13/0.58 ![X0]: (add(a,multiply(X0,sF3_fnc))=multiply(add(X0,a),a))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f1504,f66])).
% 0.13/0.58 fof(f1611,plain,(
% 0.13/0.58 ![X0]: (add(a,multiply(X0,sF3_fnc))=multiply(a,add(X0,a)))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f11,f1600])).
% 0.13/0.58 fof(f1612,plain,(
% 0.13/0.58 ![X0]: (add(a,multiply(X0,sF3_fnc))=a)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f926,f1611])).
% 0.13/0.58 fof(f1624,plain,(
% 0.13/0.58 multiply(a,b)=add(sF3_fnc,multiply(a,sF1_fnc))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f1506,f872])).
% 0.13/0.58 fof(f1641,plain,(
% 0.13/0.58 sF3_fnc=add(sF3_fnc,multiply(a,sF1_fnc))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f21,f1624])).
% 0.13/0.58 fof(f1642,plain,(
% 0.13/0.58 sF3_fnc=add(sF3_fnc,sF0_fnc)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f20,f1641])).
% 0.13/0.58 fof(f1643,plain,(
% 0.13/0.58 sF3_fnc=add(sF0_fnc,sF3_fnc)),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f10,f1642])).
% 0.13/0.58 fof(f1693,plain,(
% 0.13/0.58 multiply(c,sF3_fnc)=add(sF2_fnc,multiply(c,sF0_fnc))),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f1643,f943])).
% 0.13/0.58 fof(f1704,plain,(
% 0.13/0.58 sF2_fnc=add(sF2_fnc,multiply(c,sF0_fnc))),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f24,f1693])).
% 0.13/0.58 fof(f1734,plain,(
% 0.13/0.58 add(sF3_fnc,sF2_fnc)=sF3_fnc),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f24,f934])).
% 0.13/0.58 fof(f1739,plain,(
% 0.13/0.58 add(b,sF3_fnc)=b),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f21,f934])).
% 0.13/0.58 fof(f1740,plain,(
% 0.13/0.58 add(sF1_fnc,sF0_fnc)=sF1_fnc),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f20,f934])).
% 0.13/0.58 fof(f1742,plain,(
% 0.13/0.58 add(c,sF1_fnc)=c),
% 0.13/0.58 inference(paramodulation,[status(thm)],[f19,f934])).
% 0.13/0.58 fof(f1772,plain,(
% 0.13/0.58 add(sF2_fnc,sF3_fnc)=sF3_fnc),
% 0.13/0.58 inference(forward_demodulation,[status(thm)],[f10,f1734])).
% 0.13/0.58 fof(f1773,plain,(
% 0.13/0.58 add(sF0_fnc,sF1_fnc)=sF1_fnc),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f10,f1740])).
% 0.13/0.59 fof(f1793,plain,(
% 0.13/0.59 multiply(sF0_fnc,sF1_fnc)=sF0_fnc),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1773,f937])).
% 0.13/0.59 fof(f1810,plain,(
% 0.13/0.59 ![X0]: (multiply(sF0_fnc,add(X0,sF1_fnc))=add(multiply(sF0_fnc,X0),sF0_fnc))),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1793,f13])).
% 0.13/0.59 fof(f1813,plain,(
% 0.13/0.59 ![X0]: (multiply(sF0_fnc,add(X0,sF1_fnc))=add(sF0_fnc,multiply(sF0_fnc,X0)))),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f10,f1810])).
% 0.13/0.59 fof(f1814,plain,(
% 0.13/0.59 ![X0]: (multiply(sF0_fnc,add(X0,sF1_fnc))=sF0_fnc)),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f933,f1813])).
% 0.13/0.59 fof(f1844,plain,(
% 0.13/0.59 multiply(sF2_fnc,sF3_fnc)=sF2_fnc),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1772,f937])).
% 0.13/0.59 fof(f1870,plain,(
% 0.13/0.59 multiply(c,b)=add(sF2_fnc,multiply(c,b))),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1739,f943])).
% 0.13/0.59 fof(f1882,plain,(
% 0.13/0.59 multiply(b,c)=add(sF2_fnc,multiply(c,b))),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f11,f1870])).
% 0.13/0.59 fof(f1883,plain,(
% 0.13/0.59 sF1_fnc=add(sF2_fnc,multiply(c,b))),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f19,f1882])).
% 0.13/0.59 fof(f1884,plain,(
% 0.13/0.59 sF1_fnc=add(sF2_fnc,multiply(b,c))),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f129,f1883])).
% 0.13/0.59 fof(f1885,plain,(
% 0.13/0.59 sF1_fnc=add(sF2_fnc,sF1_fnc)),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f19,f1884])).
% 0.13/0.59 fof(f1886,plain,(
% 0.13/0.59 sF1_fnc=add(sF1_fnc,sF2_fnc)),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f10,f1885])).
% 0.13/0.59 fof(f1903,plain,(
% 0.13/0.59 multiply(a,sF1_fnc)=add(sF0_fnc,multiply(a,sF2_fnc))),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1886,f873])).
% 0.13/0.59 fof(f1914,plain,(
% 0.13/0.59 sF0_fnc=add(sF0_fnc,multiply(a,sF2_fnc))),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f20,f1903])).
% 0.13/0.59 fof(f2966,plain,(
% 0.13/0.59 add(a,sF2_fnc)=a),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1844,f1612])).
% 0.13/0.59 fof(f3065,plain,(
% 0.13/0.59 sF2_fnc=multiply(sF2_fnc,a)),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f2966,f926])).
% 0.13/0.59 fof(f3077,plain,(
% 0.13/0.59 sF0_fnc=add(sF0_fnc,sF2_fnc)),
% 0.13/0.59 inference(backward_demodulation,[status(thm)],[f3078,f1914])).
% 0.13/0.59 fof(f3078,plain,(
% 0.13/0.59 sF2_fnc=multiply(a,sF2_fnc)),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f11,f3065])).
% 0.13/0.59 fof(f4599,plain,(
% 0.13/0.59 multiply(sF0_fnc,c)=sF0_fnc),
% 0.13/0.59 inference(paramodulation,[status(thm)],[f1742,f1814])).
% 0.13/0.59 fof(f4624,plain,(
% 0.13/0.59 sF2_fnc=add(sF2_fnc,sF0_fnc)),
% 0.13/0.59 inference(backward_demodulation,[status(thm)],[f4625,f1704])).
% 0.13/0.59 fof(f4625,plain,(
% 0.13/0.59 multiply(c,sF0_fnc)=sF0_fnc),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f11,f4599])).
% 0.13/0.59 fof(f4642,plain,(
% 0.13/0.59 sF2_fnc=add(sF0_fnc,sF2_fnc)),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f10,f4624])).
% 0.13/0.59 fof(f4643,plain,(
% 0.13/0.59 sF2_fnc=sF0_fnc),
% 0.13/0.59 inference(forward_demodulation,[status(thm)],[f3077,f4642])).
% 0.13/0.59 fof(f4644,plain,(
% 0.13/0.59 $false),
% 0.13/0.59 inference(forward_subsumption_resolution,[status(thm)],[f4643,f23])).
% 0.13/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.61 % Elapsed time: 0.259112 seconds
% 0.13/0.61 % CPU time: 1.824426 seconds
% 0.13/0.61 % Total memory used: 31.579 MB
% 0.13/0.61 % Net memory used: 30.988 MB
%------------------------------------------------------------------------------