%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP697-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:37:11 PM UTC 2026
% Result : Unsatisfiable 0.23s 1.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP697-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.49 % Computer : n018.cluster.edu
% 0.18/0.49 % Model : x86_64 x86_64
% 0.18/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49 % Memory : 8046.5625MB
% 0.18/0.49 % OS : Linux 6.8.0-71-generic
% 0.18/0.49 % CPULimit : 300
% 0.18/0.49 % WCLimit : 300
% 0.18/0.49 % DateTime : Sun Sep 20 20:35:42 UTC 2026
% 0.18/0.50 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 0.23/1.08 % Refutation found
% 0.23/1.08 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.23/1.08 % SZS output start CNFRefutation for theBenchmark
% 0.23/1.08 fof(f1,axiom,(
% 0.23/1.08 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f2,axiom,(
% 0.23/1.08 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f3,axiom,(
% 0.23/1.08 (![A,B]: (mult(rd(A,B),B) = A ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f4,axiom,(
% 0.23/1.08 (![A,B]: (rd(mult(A,B),B) = A ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f5,axiom,(
% 0.23/1.08 (![A]: (mult(A,unit) = A ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f6,axiom,(
% 0.23/1.08 (![A]: (mult(unit,A) = A ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f7,axiom,(
% 0.23/1.08 (![A,B]: (mult(A,i(mult(B,A))) = i(B) ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f8,axiom,(
% 0.23/1.08 (![A,B,C]: (mult(A,mult(B,C)) = mult(rd(mult(A,B),A),mult(A,C)) ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f9,axiom,(
% 0.23/1.08 (![A,B,C]: (mult(mult(A,B),C) = mult(mult(A,C),ld(C,mult(B,C))) ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f10,axiom,(
% 0.23/1.08 (![A]: (mult(i(A),A) = unit ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f11,axiom,(
% 0.23/1.08 (![A]: (mult(A,i(A)) = unit ))),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f12,negated_conjecture,(
% 0.23/1.08 mult(mult(a,b),mult(b,mult(c,b))) != mult(mult(a,mult(b,mult(b,c))),b) ),
% 0.23/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.23/1.08 fof(f13,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f1])).
% 0.23/1.08 fof(f14,plain,(
% 0.23/1.08 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f2])).
% 0.23/1.08 fof(f15,plain,(
% 0.23/1.08 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f3])).
% 0.23/1.08 fof(f16,plain,(
% 0.23/1.08 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f4])).
% 0.23/1.08 fof(f17,plain,(
% 0.23/1.08 ![X0]: (mult(X0,unit)=X0)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f5])).
% 0.23/1.08 fof(f18,plain,(
% 0.23/1.08 ![X0]: (mult(unit,X0)=X0)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f6])).
% 0.23/1.08 fof(f19,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,i(mult(X1,X0)))=i(X1))),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f7])).
% 0.23/1.08 fof(f20,plain,(
% 0.23/1.08 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(rd(mult(X0,X1),X0),mult(X0,X2)))),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f8])).
% 0.23/1.08 fof(f21,plain,(
% 0.23/1.08 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X2),ld(X2,mult(X1,X2))))),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f9])).
% 0.23/1.08 fof(f22,plain,(
% 0.23/1.08 ![X0]: (mult(i(X0),X0)=unit)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f10])).
% 0.23/1.08 fof(f23,plain,(
% 0.23/1.08 ![X0]: (mult(X0,i(X0))=unit)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f11])).
% 0.23/1.08 fof(f24,plain,(
% 0.23/1.08 ~mult(mult(a,b),mult(b,mult(c,b)))=mult(mult(a,mult(b,mult(b,c))),b)),
% 0.23/1.08 inference(cnf_transformation,[status(thm)],[f12])).
% 0.23/1.08 fof(f25,definition,(
% 0.23/1.08 sF1_fnc=mult(a,b)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.23/1.08 fof(f26,definition,(
% 0.23/1.08 sF3_fnc=mult(c,b)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.23/1.08 fof(f27,definition,(
% 0.23/1.08 sF2_fnc=mult(b,sF3_fnc)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.23/1.08 fof(f28,definition,(
% 0.23/1.08 sF0_fnc=mult(sF1_fnc,sF2_fnc)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.23/1.08 fof(f29,definition,(
% 0.23/1.08 sF7_fnc=mult(b,c)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 0.23/1.08 fof(f30,definition,(
% 0.23/1.08 sF6_fnc=mult(b,sF7_fnc)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 0.23/1.08 fof(f31,definition,(
% 0.23/1.08 sF5_fnc=mult(a,sF6_fnc)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 0.23/1.08 fof(f32,definition,(
% 0.23/1.08 sF4_fnc=mult(sF5_fnc,b)),
% 0.23/1.08 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 0.23/1.08 fof(f33,plain,(
% 0.23/1.08 ~sF0_fnc=sF4_fnc),
% 0.23/1.08 inference(definition_folding,[],[f24,f32,f31,f30,f29,f28,f27,f26,f25])).
% 0.23/1.08 fof(f52,plain,(
% 0.23/1.08 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f15,f14])).
% 0.23/1.08 fof(f62,plain,(
% 0.23/1.08 rd(sF3_fnc,b)=c),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f26,f16])).
% 0.23/1.08 fof(f64,plain,(
% 0.23/1.08 ![X0]: (rd(X0,X0)=unit)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f18,f16])).
% 0.23/1.08 fof(f65,plain,(
% 0.23/1.08 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f13,f16])).
% 0.23/1.08 fof(f81,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,i(X1))=i(rd(X1,X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f15,f19])).
% 0.23/1.08 fof(f90,plain,(
% 0.23/1.08 ![X0,X1]: (ld(X0,i(X1))=i(mult(X1,X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f19,f14])).
% 0.23/1.08 fof(f96,plain,(
% 0.23/1.08 ![X0]: (i(rd(X0,X0))=unit)),
% 0.23/1.08 inference(backward_demodulation,[status(thm)],[f81,f23])).
% 0.23/1.08 fof(f104,plain,(
% 0.23/1.08 i(unit)=unit),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f64,f96])).
% 0.23/1.08 fof(f130,plain,(
% 0.23/1.08 ![X0,X1,X2]: (mult(X0,mult(X1,ld(X0,X2)))=mult(rd(mult(X0,X1),X0),X2))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f13,f20])).
% 0.23/1.08 fof(f178,plain,(
% 0.23/1.08 ![X0]: (mult(mult(a,X0),b)=mult(sF1_fnc,ld(b,mult(X0,b))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f25,f21])).
% 0.23/1.08 fof(f217,plain,(
% 0.23/1.08 ![X0,X1]: (mult(mult(i(X0),X1),X0)=mult(unit,ld(X0,mult(X1,X0))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f22,f21])).
% 0.23/1.08 fof(f218,plain,(
% 0.23/1.08 ![X0]: (rd(unit,X0)=i(X0))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f22,f16])).
% 0.23/1.08 fof(f219,plain,(
% 0.23/1.08 ![X0]: (ld(i(X0),unit)=X0)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f22,f14])).
% 0.23/1.08 fof(f221,plain,(
% 0.23/1.08 ![X0,X1]: (mult(mult(i(X0),X1),X0)=ld(X0,mult(X1,X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f18,f217])).
% 0.23/1.08 fof(f268,plain,(
% 0.23/1.08 ![X0,X1]: (X0=i(rd(X1,rd(X0,i(X1)))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f15,f81])).
% 0.23/1.08 fof(f270,plain,(
% 0.23/1.08 ![X0]: (mult(X0,unit)=i(rd(unit,X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f104,f81])).
% 0.23/1.08 fof(f277,plain,(
% 0.23/1.08 ![X0,X1]: (ld(X0,i(rd(X1,X0)))=i(X1))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f81,f14])).
% 0.23/1.08 fof(f278,plain,(
% 0.23/1.08 ![X0]: (X0=i(rd(unit,X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f17,f270])).
% 0.23/1.08 fof(f280,plain,(
% 0.23/1.08 ![X0]: (X0=i(i(X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f218,f278])).
% 0.23/1.08 fof(f290,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,X1)=i(rd(i(X1),X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f280,f81])).
% 0.23/1.08 fof(f291,plain,(
% 0.23/1.08 ![X0]: (ld(X0,unit)=i(X0))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f280,f219])).
% 0.23/1.08 fof(f318,plain,(
% 0.23/1.08 ![X0,X1]: (rd(i(X0),X1)=i(mult(X1,X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f290,f280])).
% 0.23/1.08 fof(f325,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,X1)=i(ld(X1,i(X0))))),
% 0.23/1.08 inference(backward_demodulation,[status(thm)],[f328,f290])).
% 0.23/1.08 fof(f328,plain,(
% 0.23/1.08 ![X0,X1]: (rd(i(X0),X1)=ld(X0,i(X1)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f90,f318])).
% 0.23/1.08 fof(f343,plain,(
% 0.23/1.08 ![X0,X1]: (rd(X0,rd(X1,i(X0)))=i(X1))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f268,f280])).
% 0.23/1.08 fof(f368,plain,(
% 0.23/1.08 ld(c,i(b))=i(sF7_fnc)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f29,f90])).
% 0.23/1.08 fof(f369,plain,(
% 0.23/1.08 ld(sF3_fnc,i(b))=i(sF2_fnc)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f27,f90])).
% 0.23/1.08 fof(f375,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),i(X1))=i(i(rd(X0,X1))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f81,f90])).
% 0.23/1.08 fof(f387,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),i(X1))=rd(X0,X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f280,f375])).
% 0.23/1.08 fof(f393,plain,(
% 0.23/1.08 ![X0,X1]: (mult(i(X0),X1)=i(ld(X1,X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f280,f325])).
% 0.23/1.08 fof(f406,plain,(
% 0.23/1.08 ![X0,X1]: (mult(i(ld(X0,X1)),X1)=ld(X1,mult(X0,X1)))),
% 0.23/1.08 inference(backward_demodulation,[status(thm)],[f393,f221])).
% 0.23/1.08 fof(f413,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(X0,ld(X1,X0)))=ld(X0,mult(X1,X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f393,f406])).
% 0.23/1.08 fof(f517,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,mult(X1,ld(X0,unit)))=rd(mult(X0,X1),X0))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f17,f130])).
% 0.23/1.08 fof(f551,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,mult(X1,i(X0)))=rd(mult(X0,X1),X0))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f291,f517])).
% 0.23/1.08 fof(f552,plain,(
% 0.23/1.08 ![X0,X1]: (mult(X0,i(rd(X0,X1)))=rd(mult(X0,X1),X0))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f81,f551])).
% 0.23/1.08 fof(f553,plain,(
% 0.23/1.08 ![X0,X1]: (i(rd(rd(X0,X1),X0))=rd(mult(X0,X1),X0))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f81,f552])).
% 0.23/1.08 fof(f595,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),X1)=rd(X0,i(X1)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f343,f52])).
% 0.23/1.08 fof(f646,plain,(
% 0.23/1.08 ![X0,X1,X2]: (ld(i(X0),ld(X1,i(X2)))=rd(X0,mult(X2,X1)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f90,f387])).
% 0.23/1.08 fof(f738,plain,(
% 0.23/1.08 ![X0,X1]: (ld(ld(i(X0),X1),X0)=i(X1))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f595,f52])).
% 0.23/1.08 fof(f1045,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(i(rd(i(X0),X1)),X0))=rd(mult(i(X0),X1),i(X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f595,f553])).
% 0.23/1.08 fof(f1063,plain,(
% 0.23/1.08 ![X0,X1]: (ld(X0,rd(mult(X0,X1),X0))=i(rd(X0,X1)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f553,f277])).
% 0.23/1.08 fof(f1072,plain,(
% 0.23/1.08 ![X0,X1]: (rd(rd(X0,X1),X0)=i(rd(mult(X0,X1),X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f553,f280])).
% 0.23/1.08 fof(f1074,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(i(ld(X0,i(X1))),X0))=rd(mult(i(X0),X1),i(X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f1045])).
% 0.23/1.08 fof(f1075,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(mult(X0,X1),X1))=rd(mult(i(X1),X0),i(X1)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f325,f1074])).
% 0.23/1.08 fof(f1076,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(mult(X0,X1),X1))=ld(i(mult(i(X1),X0)),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f595,f1075])).
% 0.23/1.08 fof(f1077,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(mult(X0,X1),X1))=ld(ld(X0,i(i(X1))),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f90,f1076])).
% 0.23/1.08 fof(f1078,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(mult(X0,X1),X1))=ld(ld(X0,X1),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f280,f1077])).
% 0.23/1.08 fof(f1121,plain,(
% 0.23/1.08 ![X0,X1]: (ld(X0,rd(X1,X0))=i(rd(X0,ld(X0,X1))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f13,f1063])).
% 0.23/1.08 fof(f1176,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(X0,X1))=ld(ld(rd(X0,X1),X1),X1))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f15,f1078])).
% 0.23/1.08 fof(f1575,plain,(
% 0.23/1.08 ![X0,X1]: (rd(X0,i(ld(X1,X0)))=ld(rd(X1,X0),X0))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f1176,f65])).
% 0.23/1.08 fof(f1613,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),ld(X1,X0))=ld(rd(X1,X0),X0))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f595,f1575])).
% 0.23/1.08 fof(f1633,plain,(
% 0.23/1.08 ![X0,X1]: (rd(rd(X0,i(X1)),X0)=i(rd(i(rd(X1,X0)),X0)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f81,f1072])).
% 0.23/1.08 fof(f1665,plain,(
% 0.23/1.08 ![X0,X1]: (rd(ld(i(X0),X1),X0)=i(rd(i(rd(X1,X0)),X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f595,f1633])).
% 0.23/1.08 fof(f1666,plain,(
% 0.23/1.08 ![X0,X1]: (rd(ld(i(X0),X1),X0)=i(ld(rd(X1,X0),i(X0))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f1665])).
% 0.23/1.08 fof(f1668,plain,(
% 0.23/1.08 ![X0,X1]: (rd(ld(i(X0),X1),X0)=mult(X0,rd(X1,X0)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f325,f1666])).
% 0.23/1.08 fof(f1714,plain,(
% 0.23/1.08 i(ld(i(b),i(sF2_fnc)))=ld(i(b),mult(sF3_fnc,i(b)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f369,f413])).
% 0.23/1.08 fof(f1761,plain,(
% 0.23/1.08 mult(sF2_fnc,i(b))=ld(i(b),mult(sF3_fnc,i(b)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f325,f1714])).
% 0.23/1.08 fof(f1762,plain,(
% 0.23/1.08 i(rd(b,sF2_fnc))=ld(i(b),mult(sF3_fnc,i(b)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f81,f1761])).
% 0.23/1.08 fof(f1763,plain,(
% 0.23/1.08 i(rd(b,sF2_fnc))=ld(i(b),i(rd(b,sF3_fnc)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f81,f1762])).
% 0.23/1.08 fof(f1764,plain,(
% 0.23/1.08 i(rd(b,sF2_fnc))=rd(b,rd(b,sF3_fnc))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f387,f1763])).
% 0.23/1.08 fof(f1838,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),rd(i(X1),i(X0)))=i(rd(i(X0),rd(X0,X1))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f387,f1121])).
% 0.23/1.08 fof(f1887,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),ld(X1,i(i(X0))))=i(rd(i(X0),rd(X0,X1))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f1838])).
% 0.23/1.08 fof(f1888,plain,(
% 0.23/1.08 ![X0,X1]: (rd(X0,mult(i(X0),X1))=i(rd(i(X0),rd(X0,X1))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f646,f1887])).
% 0.23/1.08 fof(f1889,plain,(
% 0.23/1.08 ![X0,X1]: (rd(X0,i(ld(X1,X0)))=i(rd(i(X0),rd(X0,X1))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f393,f1888])).
% 0.23/1.08 fof(f1890,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(X0),ld(X1,X0))=i(rd(i(X0),rd(X0,X1))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f595,f1889])).
% 0.23/1.08 fof(f1891,plain,(
% 0.23/1.08 ![X0,X1]: (ld(rd(X0,X1),X1)=i(rd(i(X1),rd(X1,X0))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f1613,f1890])).
% 0.23/1.08 fof(f1892,plain,(
% 0.23/1.08 ![X0,X1]: (ld(rd(X0,X1),X1)=i(ld(X1,i(rd(X1,X0)))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f1891])).
% 0.23/1.08 fof(f1894,plain,(
% 0.23/1.08 ![X0,X1]: (ld(rd(X0,X1),X1)=mult(rd(X1,X0),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f325,f1892])).
% 0.23/1.08 fof(f2634,plain,(
% 0.23/1.08 ![X0,X1]: (rd(ld(rd(X0,X1),X1),X1)=rd(X1,X0))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f1894,f16])).
% 0.23/1.08 fof(f2781,plain,(
% 0.23/1.08 ![X0,X1]: (rd(ld(X0,X1),X1)=rd(X1,mult(X0,X1)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f16,f2634])).
% 0.23/1.08 fof(f2966,plain,(
% 0.23/1.08 ![X0,X1]: (ld(i(ld(X0,i(X1))),X1)=rd(i(X1),mult(X0,i(X1))))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f595,f2781])).
% 0.23/1.08 fof(f2988,plain,(
% 0.23/1.08 rd(i(sF7_fnc),i(b))=rd(i(b),mult(c,i(b)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f368,f2781])).
% 0.23/1.08 fof(f3008,plain,(
% 0.23/1.08 ![X0,X1]: (ld(mult(X0,X1),X0)=rd(i(X0),mult(X1,i(X0))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f325,f2966])).
% 0.23/1.08 fof(f3009,plain,(
% 0.23/1.08 ![X0,X1]: (ld(mult(X0,X1),X0)=ld(X0,i(mult(X1,i(X0)))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f3008])).
% 0.23/1.08 fof(f3010,plain,(
% 0.23/1.08 ![X0,X1]: (ld(mult(X0,X1),X0)=ld(X0,ld(i(X0),i(X1))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f90,f3009])).
% 0.23/1.08 fof(f3015,plain,(
% 0.23/1.08 ![X0,X1]: (ld(mult(X0,X1),X0)=ld(X0,rd(X0,X1)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f387,f3010])).
% 0.23/1.08 fof(f3078,plain,(
% 0.23/1.08 ld(sF7_fnc,i(i(b)))=rd(i(b),mult(c,i(b)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f2988])).
% 0.23/1.08 fof(f3079,plain,(
% 0.23/1.08 ld(sF7_fnc,b)=rd(i(b),mult(c,i(b)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f280,f3078])).
% 0.23/1.08 fof(f3080,plain,(
% 0.23/1.08 ld(sF7_fnc,b)=ld(b,i(mult(c,i(b))))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f3079])).
% 0.23/1.08 fof(f3081,plain,(
% 0.23/1.08 ld(sF7_fnc,b)=ld(b,ld(i(b),i(c)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f90,f3080])).
% 0.23/1.08 fof(f3082,plain,(
% 0.23/1.08 ld(sF7_fnc,b)=ld(b,rd(b,c))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f387,f3081])).
% 0.23/1.08 fof(f4017,plain,(
% 0.23/1.08 ![X0,X1]: (i(ld(ld(i(X0),X1),X0))=ld(ld(mult(X0,rd(X1,X0)),X0),X0))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f1668,f1176])).
% 0.23/1.08 fof(f4100,plain,(
% 0.23/1.08 ![X0,X1]: (i(i(X0))=ld(ld(mult(X1,rd(X0,X1)),X1),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f738,f4017])).
% 0.23/1.08 fof(f4101,plain,(
% 0.23/1.08 ![X0,X1]: (X0=ld(ld(mult(X1,rd(X0,X1)),X1),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f280,f4100])).
% 0.23/1.08 fof(f4102,plain,(
% 0.23/1.08 ![X0,X1]: (X0=ld(ld(X1,rd(X1,rd(X0,X1))),X1))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f3015,f4101])).
% 0.23/1.08 fof(f4119,plain,(
% 0.23/1.08 sF3_fnc=ld(ld(b,rd(b,c)),b)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f62,f4102])).
% 0.23/1.08 fof(f4158,plain,(
% 0.23/1.08 sF3_fnc=ld(ld(sF7_fnc,b),b)),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f3082,f4119])).
% 0.23/1.08 fof(f4243,plain,(
% 0.23/1.08 rd(b,sF3_fnc)=ld(sF7_fnc,b)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f4158,f65])).
% 0.23/1.08 fof(f4252,plain,(
% 0.23/1.08 i(rd(b,sF2_fnc))=rd(b,ld(sF7_fnc,b))),
% 0.23/1.08 inference(backward_demodulation,[status(thm)],[f4243,f1764])).
% 0.23/1.08 fof(f4258,plain,(
% 0.23/1.08 i(rd(b,sF2_fnc))=sF7_fnc),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f65,f4252])).
% 0.23/1.08 fof(f4809,plain,(
% 0.23/1.08 rd(b,sF2_fnc)=i(sF7_fnc)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f4258,f280])).
% 0.23/1.08 fof(f4890,plain,(
% 0.23/1.08 i(rd(i(sF7_fnc),b))=rd(mult(b,sF2_fnc),b)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f4809,f553])).
% 0.23/1.08 fof(f4903,plain,(
% 0.23/1.08 i(ld(sF7_fnc,i(b)))=rd(mult(b,sF2_fnc),b)),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f328,f4890])).
% 0.23/1.08 fof(f4904,plain,(
% 0.23/1.08 mult(b,sF7_fnc)=rd(mult(b,sF2_fnc),b)),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f325,f4903])).
% 0.23/1.08 fof(f4905,plain,(
% 0.23/1.08 sF6_fnc=rd(mult(b,sF2_fnc),b)),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f30,f4904])).
% 0.23/1.08 fof(f5939,plain,(
% 0.23/1.08 mult(sF6_fnc,b)=mult(b,sF2_fnc)),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f4905,f15])).
% 0.23/1.08 fof(f6097,plain,(
% 0.23/1.08 mult(mult(a,sF6_fnc),b)=mult(sF1_fnc,ld(b,mult(b,sF2_fnc)))),
% 0.23/1.08 inference(paramodulation,[status(thm)],[f5939,f178])).
% 0.23/1.08 fof(f6113,plain,(
% 0.23/1.08 mult(sF5_fnc,b)=mult(sF1_fnc,ld(b,mult(b,sF2_fnc)))),
% 0.23/1.08 inference(forward_demodulation,[status(thm)],[f31,f6097])).
% 2.49/1.12 fof(f6114,plain,(
% 2.49/1.12 sF4_fnc=mult(sF1_fnc,ld(b,mult(b,sF2_fnc)))),
% 2.49/1.12 inference(forward_demodulation,[status(thm)],[f32,f6113])).
% 2.49/1.12 fof(f6115,plain,(
% 2.49/1.12 sF4_fnc=mult(sF1_fnc,sF2_fnc)),
% 2.49/1.12 inference(forward_demodulation,[status(thm)],[f14,f6114])).
% 2.49/1.12 fof(f6116,plain,(
% 2.49/1.12 sF4_fnc=sF0_fnc),
% 2.49/1.12 inference(forward_demodulation,[status(thm)],[f28,f6115])).
% 2.49/1.12 fof(f6117,plain,(
% 2.49/1.12 $false),
% 2.49/1.12 inference(forward_subsumption_resolution,[status(thm)],[f6116,f33])).
% 2.49/1.12 % SZS output end CNFRefutation for theBenchmark.p
% 2.49/1.14 % Elapsed time: 0.619959 seconds
% 2.49/1.14 % CPU time: 4.540808 seconds
% 2.49/1.14 % Total memory used: 102.075 MB
% 2.49/1.14 % Net memory used: 100.633 MB
%------------------------------------------------------------------------------