%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO008-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 : n008.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.21s 0.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : BOO008-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.66 % Computer : n008.cluster.edu
% 0.17/0.66 % Model : x86_64 x86_64
% 0.17/0.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.66 % Memory : 8046.5625MB
% 0.17/0.66 % OS : Linux 6.8.0-71-generic
% 0.17/0.66 % CPULimit : 300
% 0.17/0.66 % WCLimit : 300
% 0.17/0.66 % DateTime : Mon Sep 21 13:48:24 UTC 2026
% 0.17/0.67 % CPUTime :
% 0.17/0.68 % Drodi V4.1.1
% 0.21/0.91 % Refutation found
% 0.21/0.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/0.91 % SZS output start CNFRefutation for theBenchmark
% 0.21/0.91 fof(f1,axiom,(
% 0.21/0.91 (![X,Y]: (add(X,Y) = add(Y,X) ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f2,axiom,(
% 0.21/0.91 (![X,Y]: (multiply(X,Y) = multiply(Y,X) ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f3,axiom,(
% 0.21/0.91 (![X,Y,Z]: (add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f4,axiom,(
% 0.21/0.91 (![X,Y,Z]: (multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f5,axiom,(
% 0.21/0.91 (![X]: (add(X,additive_identity) = X ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f6,axiom,(
% 0.21/0.91 (![X]: (multiply(X,multiplicative_identity) = X ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f7,axiom,(
% 0.21/0.91 (![X]: (add(X,inverse(X)) = multiplicative_identity ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f8,axiom,(
% 0.21/0.91 (![X]: (multiply(X,inverse(X)) = additive_identity ))),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f9,negated_conjecture,(
% 0.21/0.91 add(a,add(b,c)) != add(add(a,b),c) ),
% 0.21/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/0.91 fof(f10,plain,(
% 0.21/0.91 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f1])).
% 0.21/0.91 fof(f11,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f2])).
% 0.21/0.91 fof(f12,plain,(
% 0.21/0.91 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X0,X1),add(X0,X2)))),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f3])).
% 0.21/0.91 fof(f13,plain,(
% 0.21/0.91 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X0,X1),multiply(X0,X2)))),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f4])).
% 0.21/0.91 fof(f14,plain,(
% 0.21/0.91 ![X0]: (add(X0,additive_identity)=X0)),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f5])).
% 0.21/0.91 fof(f15,plain,(
% 0.21/0.91 ![X0]: (multiply(X0,multiplicative_identity)=X0)),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f6])).
% 0.21/0.91 fof(f16,plain,(
% 0.21/0.91 ![X0]: (add(X0,inverse(X0))=multiplicative_identity)),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f7])).
% 0.21/0.91 fof(f17,plain,(
% 0.21/0.91 ![X0]: (multiply(X0,inverse(X0))=additive_identity)),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f8])).
% 0.21/0.91 fof(f18,plain,(
% 0.21/0.91 ~add(a,add(b,c))=add(add(a,b),c)),
% 0.21/0.91 inference(cnf_transformation,[status(thm)],[f9])).
% 0.21/0.91 fof(f19,definition,(
% 0.21/0.91 sF1_fnc=add(b,c)),
% 0.21/0.91 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.21/0.91 fof(f20,definition,(
% 0.21/0.91 sF0_fnc=add(a,sF1_fnc)),
% 0.21/0.91 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.21/0.91 fof(f21,definition,(
% 0.21/0.91 sF3_fnc=add(a,b)),
% 0.21/0.91 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.21/0.91 fof(f22,definition,(
% 0.21/0.91 sF2_fnc=add(sF3_fnc,c)),
% 0.21/0.91 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.21/0.91 fof(f23,plain,(
% 0.21/0.91 ~sF0_fnc=sF2_fnc),
% 0.21/0.91 inference(definition_folding,[],[f18,f22,f21,f20,f19])).
% 0.21/0.91 fof(f24,plain,(
% 0.21/0.91 sF2_fnc=add(c,sF3_fnc)),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f10,f22])).
% 0.21/0.91 fof(f33,plain,(
% 0.21/0.91 ![X0]: (add(additive_identity,X0)=X0)),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f10,f14])).
% 0.21/0.91 fof(f43,plain,(
% 0.21/0.91 ![X0]: (multiply(multiplicative_identity,X0)=X0)),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f11,f15])).
% 0.21/0.91 fof(f56,plain,(
% 0.21/0.91 inverse(multiplicative_identity)=additive_identity),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f43,f17])).
% 0.21/0.91 fof(f61,plain,(
% 0.21/0.91 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X0,X2),multiply(X0,X1)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f10,f13])).
% 0.21/0.91 fof(f64,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(inverse(X0),X1))=add(additive_identity,multiply(X0,X1)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f17,f13])).
% 0.21/0.91 fof(f66,plain,(
% 0.21/0.91 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X1,X0),multiply(X0,X2)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f11,f13])).
% 0.21/0.91 fof(f69,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X1,inverse(X0)))=add(multiply(X0,X1),additive_identity))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f17,f13])).
% 0.21/0.91 fof(f70,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X1,multiplicative_identity))=add(multiply(X0,X1),X0))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f15,f13])).
% 0.21/0.91 fof(f76,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(inverse(X0),X1))=multiply(X0,X1))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f33,f64])).
% 0.21/0.91 fof(f78,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X1,inverse(X0)))=multiply(X0,X1))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f14,f69])).
% 0.21/0.91 fof(f79,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X1,multiplicative_identity))=add(X0,multiply(X0,X1)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f10,f70])).
% 0.21/0.91 fof(f82,plain,(
% 0.21/0.91 ![X0]: (multiply(X0,inverse(X0))=multiply(X0,additive_identity))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f14,f76])).
% 0.21/0.91 fof(f93,plain,(
% 0.21/0.91 ![X0]: (additive_identity=multiply(X0,additive_identity))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f17,f82])).
% 0.21/0.91 fof(f101,plain,(
% 0.21/0.91 ![X0]: (additive_identity=multiply(additive_identity,X0))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f11,f93])).
% 0.21/0.91 fof(f129,plain,(
% 0.21/0.91 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=multiply(X0,add(X2,X1)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f13,f61])).
% 0.21/0.91 fof(f172,plain,(
% 0.21/0.91 ![X0]: (multiply(X0,add(multiplicative_identity,multiplicative_identity))=add(X0,X0))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f15,f79])).
% 0.21/0.91 fof(f212,plain,(
% 0.21/0.91 ![X0]: (multiply(X0,multiplicative_identity)=multiply(X0,X0))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f16,f78])).
% 0.21/0.91 fof(f228,plain,(
% 0.21/0.91 ![X0]: (X0=multiply(X0,X0))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f15,f212])).
% 0.21/0.91 fof(f250,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X0,X1))=add(multiply(X0,X1),X0))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f228,f61])).
% 0.21/0.91 fof(f251,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X1,X0))=add(X0,multiply(X0,X1)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f228,f61])).
% 0.21/0.91 fof(f254,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X0,X1))=add(X0,multiply(X0,X1)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f10,f250])).
% 0.21/0.91 fof(f297,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X0,X1))=multiply(X0,add(X1,multiplicative_identity)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f79,f254])).
% 0.21/0.91 fof(f309,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X0,X1))=add(X0,multiply(X1,X0)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f11,f254])).
% 0.21/0.91 fof(f443,plain,(
% 0.21/0.91 ![X0]: (multiply(inverse(X0),add(inverse(X0),X0))=add(inverse(X0),additive_identity))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f17,f309])).
% 0.21/0.91 fof(f483,plain,(
% 0.21/0.91 ![X0]: (multiply(inverse(X0),add(X0,multiplicative_identity))=add(inverse(X0),additive_identity))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f297,f443])).
% 0.21/0.91 fof(f484,plain,(
% 0.21/0.91 ![X0]: (multiply(inverse(X0),add(X0,multiplicative_identity))=inverse(X0))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f14,f483])).
% 0.21/0.91 fof(f501,plain,(
% 0.21/0.91 ![X0]: (multiply(inverse(X0),add(multiplicative_identity,X0))=inverse(X0))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f10,f484])).
% 0.21/0.91 fof(f552,plain,(
% 0.21/0.91 ![X0]: (multiply(add(multiplicative_identity,X0),add(add(multiplicative_identity,X0),inverse(X0)))=add(add(multiplicative_identity,X0),inverse(X0)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f501,f309])).
% 0.21/0.91 fof(f579,plain,(
% 0.21/0.91 ![X0]: (multiply(add(multiplicative_identity,X0),add(inverse(X0),multiplicative_identity))=add(add(multiplicative_identity,X0),inverse(X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f297,f552])).
% 0.21/0.91 fof(f580,plain,(
% 0.21/0.91 ![X0]: (multiply(add(multiplicative_identity,X0),add(multiplicative_identity,inverse(X0)))=add(add(multiplicative_identity,X0),inverse(X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f129,f579])).
% 0.21/0.91 fof(f581,plain,(
% 0.21/0.91 ![X0]: (add(multiplicative_identity,multiply(X0,inverse(X0)))=add(add(multiplicative_identity,X0),inverse(X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f12,f580])).
% 0.21/0.91 fof(f582,plain,(
% 0.21/0.91 ![X0]: (add(multiplicative_identity,additive_identity)=add(add(multiplicative_identity,X0),inverse(X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f17,f581])).
% 0.21/0.91 fof(f583,plain,(
% 0.21/0.91 ![X0]: (multiplicative_identity=add(add(multiplicative_identity,X0),inverse(X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f14,f582])).
% 0.21/0.91 fof(f584,plain,(
% 0.21/0.91 ![X0]: (multiplicative_identity=add(inverse(X0),add(multiplicative_identity,X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f10,f583])).
% 0.21/0.91 fof(f601,plain,(
% 0.21/0.91 multiplicative_identity=add(additive_identity,add(multiplicative_identity,multiplicative_identity))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f56,f584])).
% 0.21/0.91 fof(f612,plain,(
% 0.21/0.91 ![X0]: (multiply(X0,multiplicative_identity)=add(X0,X0))),
% 0.21/0.91 inference(backward_demodulation,[status(thm)],[f625,f172])).
% 0.21/0.91 fof(f625,plain,(
% 0.21/0.91 multiplicative_identity=add(multiplicative_identity,multiplicative_identity)),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f33,f601])).
% 0.21/0.91 fof(f667,plain,(
% 0.21/0.91 ![X0]: (X0=add(X0,X0))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f15,f612])).
% 0.21/0.91 fof(f871,plain,(
% 0.21/0.91 ![X0]: (add(a,multiply(b,X0))=multiply(sF3_fnc,add(a,X0)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f21,f12])).
% 0.21/0.91 fof(f872,plain,(
% 0.21/0.91 ![X0]: (add(a,multiply(sF1_fnc,X0))=multiply(sF0_fnc,add(a,X0)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f20,f12])).
% 0.21/0.91 fof(f880,plain,(
% 0.21/0.91 ![X0,X1]: (add(X0,multiply(additive_identity,X1))=multiply(X0,add(X0,X1)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f14,f12])).
% 0.21/0.91 fof(f881,plain,(
% 0.21/0.91 ![X0,X1]: (add(X0,multiply(X0,X1))=multiply(X0,add(X0,X1)))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f667,f12])).
% 0.21/0.91 fof(f889,plain,(
% 0.21/0.91 ![X0]: (add(c,multiply(X0,sF3_fnc))=multiply(add(c,X0),sF2_fnc))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f24,f12])).
% 0.21/0.91 fof(f923,plain,(
% 0.21/0.91 ![X0,X1]: (add(X0,additive_identity)=multiply(X0,add(X0,X1)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f101,f880])).
% 0.21/0.91 fof(f925,plain,(
% 0.21/0.91 ![X0,X1]: (X0=add(X0,multiply(X1,X0)))),
% 0.21/0.91 inference(backward_demodulation,[status(thm)],[f932,f309])).
% 0.21/0.91 fof(f932,plain,(
% 0.21/0.91 ![X0,X1]: (X0=multiply(X0,add(X0,X1)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f14,f923])).
% 0.21/0.91 fof(f933,plain,(
% 0.21/0.91 ![X0,X1]: (multiply(X0,add(X1,X0))=X0)),
% 0.21/0.91 inference(backward_demodulation,[status(thm)],[f936,f251])).
% 0.21/0.91 fof(f936,plain,(
% 0.21/0.91 ![X0,X1]: (add(X0,multiply(X0,X1))=X0)),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f932,f881])).
% 0.21/0.91 fof(f942,plain,(
% 0.21/0.91 ![X0]: (add(c,multiply(X0,sF3_fnc))=multiply(sF2_fnc,add(c,X0)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f11,f889])).
% 0.21/0.91 fof(f1503,plain,(
% 0.21/0.91 a=multiply(a,sF3_fnc)),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f21,f932])).
% 0.21/0.91 fof(f1505,plain,(
% 0.21/0.91 b=multiply(b,sF1_fnc)),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f19,f932])).
% 0.21/0.91 fof(f1599,plain,(
% 0.21/0.91 ![X0]: (multiply(a,add(X0,sF3_fnc))=add(multiply(X0,a),a))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f1503,f66])).
% 0.21/0.91 fof(f1610,plain,(
% 0.21/0.91 ![X0]: (multiply(a,add(X0,sF3_fnc))=add(a,multiply(X0,a)))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f10,f1599])).
% 0.21/0.91 fof(f1611,plain,(
% 0.21/0.91 ![X0]: (multiply(a,add(X0,sF3_fnc))=a)),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f925,f1610])).
% 0.21/0.91 fof(f1623,plain,(
% 0.21/0.91 add(a,b)=multiply(sF3_fnc,add(a,sF1_fnc))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f1505,f871])).
% 0.21/0.91 fof(f1640,plain,(
% 0.21/0.91 sF3_fnc=multiply(sF3_fnc,add(a,sF1_fnc))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f21,f1623])).
% 0.21/0.91 fof(f1641,plain,(
% 0.21/0.91 sF3_fnc=multiply(sF3_fnc,sF0_fnc)),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f20,f1640])).
% 0.21/0.91 fof(f1642,plain,(
% 0.21/0.91 sF3_fnc=multiply(sF0_fnc,sF3_fnc)),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f11,f1641])).
% 0.21/0.91 fof(f1692,plain,(
% 0.21/0.91 add(c,sF3_fnc)=multiply(sF2_fnc,add(c,sF0_fnc))),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f1642,f942])).
% 0.21/0.91 fof(f1703,plain,(
% 0.21/0.91 sF2_fnc=multiply(sF2_fnc,add(c,sF0_fnc))),
% 0.21/0.91 inference(forward_demodulation,[status(thm)],[f24,f1692])).
% 0.21/0.91 fof(f1733,plain,(
% 0.21/0.91 multiply(sF3_fnc,sF2_fnc)=sF3_fnc),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f24,f933])).
% 0.21/0.91 fof(f1738,plain,(
% 0.21/0.91 multiply(b,sF3_fnc)=b),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f21,f933])).
% 0.21/0.91 fof(f1739,plain,(
% 0.21/0.91 multiply(sF1_fnc,sF0_fnc)=sF1_fnc),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f20,f933])).
% 0.21/0.91 fof(f1741,plain,(
% 0.21/0.91 multiply(c,sF1_fnc)=c),
% 0.21/0.91 inference(paramodulation,[status(thm)],[f19,f933])).
% 0.21/0.91 fof(f1771,plain,(
% 0.21/0.91 multiply(sF2_fnc,sF3_fnc)=sF3_fnc),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f11,f1733])).
% 0.21/0.92 fof(f1772,plain,(
% 0.21/0.92 multiply(sF0_fnc,sF1_fnc)=sF1_fnc),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f11,f1739])).
% 0.21/0.92 fof(f1792,plain,(
% 0.21/0.92 add(sF0_fnc,sF1_fnc)=sF0_fnc),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1772,f936])).
% 0.21/0.92 fof(f1809,plain,(
% 0.21/0.92 ![X0]: (add(sF0_fnc,multiply(X0,sF1_fnc))=multiply(add(sF0_fnc,X0),sF0_fnc))),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1792,f12])).
% 0.21/0.92 fof(f1812,plain,(
% 0.21/0.92 ![X0]: (add(sF0_fnc,multiply(X0,sF1_fnc))=multiply(sF0_fnc,add(sF0_fnc,X0)))),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f11,f1809])).
% 0.21/0.92 fof(f1813,plain,(
% 0.21/0.92 ![X0]: (add(sF0_fnc,multiply(X0,sF1_fnc))=sF0_fnc)),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f932,f1812])).
% 0.21/0.92 fof(f1843,plain,(
% 0.21/0.92 add(sF2_fnc,sF3_fnc)=sF2_fnc),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1771,f936])).
% 0.21/0.92 fof(f1869,plain,(
% 0.21/0.92 add(c,b)=multiply(sF2_fnc,add(c,b))),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1738,f942])).
% 0.21/0.92 fof(f1881,plain,(
% 0.21/0.92 add(b,c)=multiply(sF2_fnc,add(c,b))),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f10,f1869])).
% 0.21/0.92 fof(f1882,plain,(
% 0.21/0.92 sF1_fnc=multiply(sF2_fnc,add(c,b))),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f19,f1881])).
% 0.21/0.92 fof(f1883,plain,(
% 0.21/0.92 sF1_fnc=multiply(sF2_fnc,add(b,c))),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f129,f1882])).
% 0.21/0.92 fof(f1884,plain,(
% 0.21/0.92 sF1_fnc=multiply(sF2_fnc,sF1_fnc)),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f19,f1883])).
% 0.21/0.92 fof(f1885,plain,(
% 0.21/0.92 sF1_fnc=multiply(sF1_fnc,sF2_fnc)),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f11,f1884])).
% 0.21/0.92 fof(f1902,plain,(
% 0.21/0.92 add(a,sF1_fnc)=multiply(sF0_fnc,add(a,sF2_fnc))),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1885,f872])).
% 0.21/0.92 fof(f1913,plain,(
% 0.21/0.92 sF0_fnc=multiply(sF0_fnc,add(a,sF2_fnc))),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f20,f1902])).
% 0.21/0.92 fof(f2965,plain,(
% 0.21/0.92 multiply(a,sF2_fnc)=a),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1843,f1611])).
% 0.21/0.92 fof(f3064,plain,(
% 0.21/0.92 sF2_fnc=add(sF2_fnc,a)),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f2965,f925])).
% 0.21/0.92 fof(f3076,plain,(
% 0.21/0.92 sF0_fnc=multiply(sF0_fnc,sF2_fnc)),
% 0.21/0.92 inference(backward_demodulation,[status(thm)],[f3077,f1913])).
% 0.21/0.92 fof(f3077,plain,(
% 0.21/0.92 sF2_fnc=add(a,sF2_fnc)),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f10,f3064])).
% 0.21/0.92 fof(f4598,plain,(
% 0.21/0.92 add(sF0_fnc,c)=sF0_fnc),
% 0.21/0.92 inference(paramodulation,[status(thm)],[f1741,f1813])).
% 0.21/0.92 fof(f4623,plain,(
% 0.21/0.92 sF2_fnc=multiply(sF2_fnc,sF0_fnc)),
% 0.21/0.92 inference(backward_demodulation,[status(thm)],[f4624,f1703])).
% 0.21/0.92 fof(f4624,plain,(
% 0.21/0.92 add(c,sF0_fnc)=sF0_fnc),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f10,f4598])).
% 0.21/0.92 fof(f4641,plain,(
% 0.21/0.92 sF2_fnc=multiply(sF0_fnc,sF2_fnc)),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f11,f4623])).
% 0.21/0.92 fof(f4642,plain,(
% 0.21/0.92 sF2_fnc=sF0_fnc),
% 0.21/0.92 inference(forward_demodulation,[status(thm)],[f3076,f4641])).
% 0.21/0.92 fof(f4643,plain,(
% 0.21/0.92 $false),
% 0.21/0.92 inference(forward_subsumption_resolution,[status(thm)],[f4642,f23])).
% 0.21/0.92 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/0.95 % Elapsed time: 0.265452 seconds
% 0.21/0.95 % CPU time: 1.862518 seconds
% 0.21/0.95 % Total memory used: 29.600 MB
% 0.21/0.95 % Net memory used: 29.010 MB
%------------------------------------------------------------------------------