%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP727-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:15 PM UTC 2026
% Result : Unsatisfiable 3.23s 0.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP727-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n017.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 20:31:42 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 3.23/0.86 % Refutation found
% 3.23/0.86 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.23/0.86 % SZS output start CNFRefutation for theBenchmark
% 3.23/0.86 fof(f2,axiom,(
% 3.23/0.86 (![A]: (mult(A,unit) = A ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f3,axiom,(
% 3.23/0.86 (![A]: (mult(A,i(A)) = unit ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f4,axiom,(
% 3.23/0.86 (![A]: (mult(i(A),A) = unit ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f5,axiom,(
% 3.23/0.86 (![A,B]: (i(mult(A,B)) = mult(i(A),i(B)) ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f6,axiom,(
% 3.23/0.86 (![A,B]: (mult(i(A),mult(A,B)) = B ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f7,axiom,(
% 3.23/0.86 (![A,B]: (rd(mult(A,B),B) = A ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f8,axiom,(
% 3.23/0.86 (![A,B]: (mult(rd(A,B),B) = A ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f9,axiom,(
% 3.23/0.86 (![A,B,C]: (mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C))) ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f10,axiom,(
% 3.23/0.86 (![A,B,C]: (mult(mult(A,B),C) = mult(mult(A,mult(B,C)),asoc(A,B,C)) ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f11,axiom,(
% 3.23/0.86 (![A,B,C]: (op_l(A,B,C) = mult(i(mult(C,B)),mult(C,mult(B,A))) ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f13,axiom,(
% 3.23/0.86 (![A,B]: (op_t(A,B) = mult(i(B),mult(A,B)) ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f20,axiom,(
% 3.23/0.86 (![A,B,C,D,E]: (asoc(asoc(A,B,C),D,E) = unit ))),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f21,negated_conjecture,(
% 3.23/0.86 asoc(a,b,asoc(c,d,e)) != unit ),
% 3.23/0.86 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.23/0.86 fof(f23,plain,(
% 3.23/0.86 ![X0]: (mult(X0,unit)=X0)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f2])).
% 3.23/0.86 fof(f24,plain,(
% 3.23/0.86 ![X0]: (mult(X0,i(X0))=unit)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f3])).
% 3.23/0.86 fof(f25,plain,(
% 3.23/0.86 ![X0]: (mult(i(X0),X0)=unit)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f4])).
% 3.23/0.86 fof(f26,plain,(
% 3.23/0.86 ![X0,X1]: (i(mult(X0,X1))=mult(i(X0),i(X1)))),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f5])).
% 3.23/0.86 fof(f27,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(X0),mult(X0,X1))=X1)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f6])).
% 3.23/0.86 fof(f28,plain,(
% 3.23/0.86 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f7])).
% 3.23/0.86 fof(f29,plain,(
% 3.23/0.86 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f8])).
% 3.23/0.86 fof(f30,plain,(
% 3.23/0.86 ![X0,X1,X2]: (mult(mult(X0,mult(X1,X0)),X2)=mult(X0,mult(X1,mult(X0,X2))))),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f9])).
% 3.23/0.86 fof(f31,plain,(
% 3.23/0.86 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,mult(X1,X2)),asoc(X0,X1,X2)))),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f10])).
% 3.23/0.86 fof(f32,plain,(
% 3.23/0.86 ![X0,X1,X2]: (op_l(X0,X1,X2)=mult(i(mult(X2,X1)),mult(X2,mult(X1,X0))))),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f11])).
% 3.23/0.86 fof(f34,plain,(
% 3.23/0.86 ![X0,X1]: (op_t(X0,X1)=mult(i(X1),mult(X0,X1)))),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f13])).
% 3.23/0.86 fof(f41,plain,(
% 3.23/0.86 ![X0,X1,X2,X3,X4]: (asoc(asoc(X0,X1,X2),X3,X4)=unit)),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f20])).
% 3.23/0.86 fof(f42,plain,(
% 3.23/0.86 ~asoc(a,b,asoc(c,d,e))=unit),
% 3.23/0.86 inference(cnf_transformation,[status(thm)],[f21])).
% 3.23/0.86 fof(f43,definition,(
% 3.23/0.86 sF1_fnc=asoc(c,d,e)),
% 3.23/0.86 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.23/0.86 fof(f44,definition,(
% 3.23/0.86 sF0_fnc=asoc(a,b,sF1_fnc)),
% 3.23/0.86 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.23/0.86 fof(f45,plain,(
% 3.23/0.86 ~sF0_fnc=unit),
% 3.23/0.86 inference(definition_folding,[],[f42,f44,f43])).
% 3.23/0.86 fof(f56,plain,(
% 3.23/0.86 ![X0,X1]: (asoc(sF1_fnc,X0,X1)=unit)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f43,f41])).
% 3.23/0.86 fof(f67,plain,(
% 3.23/0.86 ![X0,X1]: (mult(mult(sF1_fnc,X0),X1)=mult(mult(sF1_fnc,mult(X0,X1)),unit))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f56,f31])).
% 3.23/0.86 fof(f71,plain,(
% 3.23/0.86 mult(mult(a,b),sF1_fnc)=mult(mult(a,mult(b,sF1_fnc)),sF0_fnc)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f44,f31])).
% 3.23/0.86 fof(f80,plain,(
% 3.23/0.86 ![X0,X1]: (mult(mult(sF1_fnc,X0),X1)=mult(sF1_fnc,mult(X0,X1)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f23,f67])).
% 3.23/0.86 fof(f286,plain,(
% 3.23/0.86 ![X0,X1,X2]: (rd(mult(mult(X0,X1),X2),asoc(X0,X1,X2))=mult(X0,mult(X1,X2)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f31,f28])).
% 3.23/0.86 fof(f288,plain,(
% 3.23/0.86 ![X0]: (rd(unit,X0)=i(X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f25,f28])).
% 3.23/0.86 fof(f290,plain,(
% 3.23/0.86 ![X0]: (rd(unit,i(X0))=X0)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f24,f28])).
% 3.23/0.86 fof(f291,plain,(
% 3.23/0.86 ![X0]: (rd(X0,unit)=X0)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f23,f28])).
% 3.23/0.86 fof(f293,plain,(
% 3.23/0.86 ![X0]: (i(i(X0))=X0)),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f288,f290])).
% 3.23/0.86 fof(f404,plain,(
% 3.23/0.86 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f293,f27])).
% 3.23/0.86 fof(f409,plain,(
% 3.23/0.86 ![X0,X1,X2]: (mult(i(mult(X0,mult(X1,X2))),mult(mult(X0,X1),X2))=asoc(X0,X1,X2))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f31,f27])).
% 3.23/0.86 fof(f419,plain,(
% 3.23/0.86 ![X0,X1]: (rd(X0,mult(X1,X0))=i(X1))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f27,f28])).
% 3.23/0.86 fof(f498,plain,(
% 3.23/0.86 ![X0,X1]: (rd(X0,X1)=i(rd(X1,X0)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f29,f419])).
% 3.23/0.86 fof(f523,plain,(
% 3.23/0.86 ![X0,X1]: (mult(rd(X0,X1),rd(X1,X0))=unit)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f498,f25])).
% 3.23/0.86 fof(f617,plain,(
% 3.23/0.86 ![X0,X1]: (i(mult(i(X0),X1))=mult(X0,i(X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f293,f26])).
% 3.23/0.86 fof(f619,plain,(
% 3.23/0.86 ![X0,X1,X2]: (i(mult(X0,rd(X1,X2)))=mult(i(X0),rd(X2,X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f498,f26])).
% 3.23/0.86 fof(f623,plain,(
% 3.23/0.86 ![X0,X1]: (mult(X0,i(mult(X0,X1)))=i(X1))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f26,f404])).
% 3.23/0.86 fof(f626,plain,(
% 3.23/0.86 ![X0,X1]: (rd(i(X0),i(mult(X1,X0)))=i(i(X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f26,f419])).
% 3.23/0.86 fof(f642,plain,(
% 3.23/0.86 ![X0,X1]: (rd(i(X0),i(mult(X1,X0)))=X1)),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f293,f626])).
% 3.23/0.86 fof(f825,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(mult(sF1_fnc,X0)),mult(sF1_fnc,mult(X0,X1)))=X1)),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f80,f27])).
% 3.23/0.86 fof(f826,plain,(
% 3.23/0.86 ![X0,X1]: (rd(mult(sF1_fnc,mult(X0,X1)),X1)=mult(sF1_fnc,X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f80,f28])).
% 3.23/0.86 fof(f860,plain,(
% 3.23/0.86 ![X0,X1]: (op_l(X0,X1,sF1_fnc)=X0)),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f32,f825])).
% 3.23/0.86 fof(f868,plain,(
% 3.23/0.86 ![X0,X1]: (rd(mult(sF1_fnc,X0),X1)=mult(sF1_fnc,rd(X0,X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f29,f826])).
% 3.23/0.86 fof(f908,plain,(
% 3.23/0.86 ![X0]: (rd(sF1_fnc,X0)=mult(sF1_fnc,rd(unit,X0)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f23,f868])).
% 3.23/0.86 fof(f912,plain,(
% 3.23/0.86 ![X0,X1]: (rd(X0,mult(sF1_fnc,X1))=i(mult(sF1_fnc,rd(X1,X0))))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f868,f498])).
% 3.23/0.86 fof(f918,plain,(
% 3.23/0.86 ![X0]: (rd(sF1_fnc,X0)=mult(sF1_fnc,i(X0)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f288,f908])).
% 3.23/0.86 fof(f920,plain,(
% 3.23/0.86 ![X0,X1]: (rd(X0,mult(sF1_fnc,X1))=mult(i(sF1_fnc),rd(X0,X1)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f619,f912])).
% 3.23/0.86 fof(f924,plain,(
% 3.23/0.86 ![X0,X1]: (rd(sF1_fnc,rd(X0,X1))=mult(sF1_fnc,rd(X1,X0)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f498,f918])).
% 3.23/0.86 fof(f925,plain,(
% 3.23/0.86 ![X0]: (rd(sF1_fnc,i(X0))=mult(sF1_fnc,X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f293,f918])).
% 3.23/0.86 fof(f928,plain,(
% 3.23/0.86 ![X0,X1]: (mult(rd(sF1_fnc,X0),X1)=mult(sF1_fnc,mult(i(X0),X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f918,f80])).
% 3.23/0.86 fof(f934,plain,(
% 3.23/0.86 ![X0]: (mult(i(sF1_fnc),rd(sF1_fnc,X0))=i(X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f918,f27])).
% 3.23/0.86 fof(f949,plain,(
% 3.23/0.86 ![X0]: (rd(sF1_fnc,mult(sF1_fnc,X0))=i(X0))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f920,f934])).
% 3.23/0.86 fof(f1063,plain,(
% 3.23/0.86 ![X0]: (rd(sF1_fnc,rd(sF1_fnc,X0))=i(i(X0)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f918,f949])).
% 3.23/0.86 fof(f1070,plain,(
% 3.23/0.86 ![X0]: (mult(sF1_fnc,rd(X0,sF1_fnc))=i(i(X0)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f924,f1063])).
% 3.23/0.86 fof(f1071,plain,(
% 3.23/0.86 ![X0]: (mult(sF1_fnc,rd(X0,sF1_fnc))=X0)),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f293,f1070])).
% 3.23/0.86 fof(f1250,plain,(
% 3.23/0.86 ![X0]: (mult(sF1_fnc,X0)=mult(X0,sF1_fnc))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f28,f1071])).
% 3.23/0.86 fof(f1254,plain,(
% 3.23/0.86 ![X0,X1]: (mult(X0,X1)=mult(sF1_fnc,mult(rd(X0,sF1_fnc),X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1071,f80])).
% 3.23/0.86 fof(f1259,plain,(
% 3.23/0.86 ![X0]: (mult(i(sF1_fnc),X0)=rd(X0,sF1_fnc))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1071,f27])).
% 3.23/0.86 fof(f1266,plain,(
% 3.23/0.86 mult(sF1_fnc,mult(a,b))=mult(mult(a,mult(b,sF1_fnc)),sF0_fnc)),
% 3.23/0.86 inference(backward_demodulation,[status(thm)],[f1250,f71])).
% 3.23/0.86 fof(f1376,plain,(
% 3.23/0.86 ![X0,X1]: (rd(i(X0),i(X1))=rd(X1,X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f29,f642])).
% 3.23/0.86 fof(f1528,plain,(
% 3.23/0.86 ![X0,X1]: (mult(rd(X0,X1),i(X0))=i(X1))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1376,f29])).
% 3.23/0.86 fof(f1721,plain,(
% 3.23/0.86 ![X0]: (mult(mult(sF1_fnc,X0),i(sF1_fnc))=i(i(X0)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f925,f1528])).
% 3.23/0.86 fof(f1753,plain,(
% 3.23/0.86 ![X0]: (mult(sF1_fnc,mult(X0,i(sF1_fnc)))=i(i(X0)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f80,f1721])).
% 3.23/0.86 fof(f1754,plain,(
% 3.23/0.86 ![X0]: (mult(sF1_fnc,mult(X0,i(sF1_fnc)))=X0)),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f293,f1753])).
% 3.23/0.86 fof(f1790,plain,(
% 3.23/0.86 ![X0]: (op_l(i(sF1_fnc),X0,sF1_fnc)=mult(i(mult(sF1_fnc,X0)),X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1754,f32])).
% 3.23/0.86 fof(f1797,plain,(
% 3.23/0.86 ![X0]: (mult(i(sF1_fnc),X0)=mult(X0,i(sF1_fnc)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1754,f27])).
% 3.23/0.86 fof(f1818,plain,(
% 3.23/0.86 ![X0]: (i(sF1_fnc)=mult(i(mult(sF1_fnc,X0)),X0))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f860,f1790])).
% 3.23/0.86 fof(f1843,plain,(
% 3.23/0.86 ![X0]: (rd(X0,sF1_fnc)=mult(X0,i(sF1_fnc)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f1259,f1797])).
% 3.23/0.86 fof(f2108,plain,(
% 3.23/0.86 ![X0]: (op_t(X0,sF1_fnc)=rd(mult(X0,sF1_fnc),sF1_fnc))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1259,f34])).
% 3.23/0.86 fof(f2139,plain,(
% 3.23/0.86 ![X0,X1]: (mult(X0,op_t(X1,X0))=mult(X1,X0))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f34,f404])).
% 3.23/0.86 fof(f2157,plain,(
% 3.23/0.86 ![X0]: (op_t(X0,sF1_fnc)=X0)),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f28,f2108])).
% 3.23/0.86 fof(f2323,plain,(
% 3.23/0.86 mult(i(mult(a,mult(b,sF1_fnc))),mult(sF1_fnc,mult(a,b)))=sF0_fnc),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1266,f27])).
% 3.23/0.86 fof(f2428,plain,(
% 3.23/0.86 ![X0,X1]: (mult(mult(X0,sF1_fnc),X1)=mult(sF1_fnc,mult(op_t(X0,sF1_fnc),X1)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f2139,f80])).
% 3.23/0.86 fof(f2472,plain,(
% 3.23/0.86 ![X0,X1]: (mult(mult(X0,sF1_fnc),X1)=mult(sF1_fnc,mult(X0,X1)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f2157,f2428])).
% 3.23/0.86 fof(f4467,plain,(
% 3.23/0.86 ![X0,X1]: (mult(mult(X0,i(sF1_fnc)),X1)=mult(X0,mult(i(mult(sF1_fnc,X0)),mult(X0,X1))))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1818,f30])).
% 3.23/0.86 fof(f4541,plain,(
% 3.23/0.86 ![X0,X1]: (mult(rd(X0,sF1_fnc),X1)=mult(X0,mult(i(mult(sF1_fnc,X0)),mult(X0,X1))))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f1843,f4467])).
% 3.23/0.86 fof(f4692,plain,(
% 3.23/0.86 ![X0,X1]: (rd(mult(i(sF1_fnc),X0),asoc(i(mult(sF1_fnc,X1)),X1,X0))=mult(i(mult(sF1_fnc,X1)),mult(X1,X0)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1818,f286])).
% 3.23/0.86 fof(f4764,plain,(
% 3.23/0.86 ![X0,X1]: (rd(rd(X0,sF1_fnc),asoc(i(mult(sF1_fnc,X1)),X1,X0))=mult(i(mult(sF1_fnc,X1)),mult(X1,X0)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f1259,f4692])).
% 3.23/0.86 fof(f6462,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(mult(X0,X1)),mult(mult(X0,sF1_fnc),rd(X1,sF1_fnc)))=asoc(X0,sF1_fnc,rd(X1,sF1_fnc)))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1071,f409])).
% 3.23/0.86 fof(f6464,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(mult(X0,mult(X1,sF1_fnc))),mult(mult(X0,sF1_fnc),X1))=asoc(X0,sF1_fnc,X1))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1250,f409])).
% 3.23/0.86 fof(f6529,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(mult(i(mult(sF1_fnc,X0)),mult(X0,X1))),mult(i(sF1_fnc),X1))=asoc(i(mult(sF1_fnc,X0)),X0,X1))),
% 3.23/0.86 inference(paramodulation,[status(thm)],[f1818,f409])).
% 3.23/0.86 fof(f6616,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(mult(X0,X1)),mult(sF1_fnc,mult(X0,rd(X1,sF1_fnc))))=asoc(X0,sF1_fnc,rd(X1,sF1_fnc)))),
% 3.23/0.86 inference(forward_demodulation,[status(thm)],[f2472,f6462])).
% 3.23/0.86 fof(f6619,plain,(
% 3.23/0.86 asoc(a,sF1_fnc,b)=sF0_fnc),
% 3.23/0.86 inference(backward_demodulation,[status(thm)],[f6620,f2323])).
% 3.23/0.86 fof(f6620,plain,(
% 3.23/0.86 ![X0,X1]: (mult(i(mult(X0,mult(X1,sF1_fnc))),mult(sF1_fnc,mult(X0,X1)))=asoc(X0,sF1_fnc,X1))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f2472,f6464])).
% 3.23/0.88 fof(f6692,plain,(
% 3.23/0.88 ![X0,X1]: (mult(mult(mult(sF1_fnc,X0),i(mult(X0,X1))),mult(i(sF1_fnc),X1))=asoc(i(mult(sF1_fnc,X0)),X0,X1))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f617,f6529])).
% 3.23/0.88 fof(f6693,plain,(
% 3.23/0.88 ![X0,X1]: (mult(mult(sF1_fnc,mult(X0,i(mult(X0,X1)))),mult(i(sF1_fnc),X1))=asoc(i(mult(sF1_fnc,X0)),X0,X1))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f80,f6692])).
% 3.23/0.88 fof(f6694,plain,(
% 3.23/0.88 ![X0,X1]: (mult(sF1_fnc,mult(mult(X0,i(mult(X0,X1))),mult(i(sF1_fnc),X1)))=asoc(i(mult(sF1_fnc,X0)),X0,X1))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f80,f6693])).
% 3.23/0.88 fof(f6695,plain,(
% 3.23/0.88 ![X0,X1]: (mult(sF1_fnc,mult(i(X0),mult(i(sF1_fnc),X0)))=asoc(i(mult(sF1_fnc,X1)),X1,X0))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f623,f6694])).
% 3.23/0.88 fof(f6696,plain,(
% 3.23/0.88 ![X0,X1]: (mult(rd(sF1_fnc,X0),mult(i(sF1_fnc),X0))=asoc(i(mult(sF1_fnc,X1)),X1,X0))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f928,f6695])).
% 3.23/0.88 fof(f6697,plain,(
% 3.23/0.88 ![X0,X1]: (mult(rd(sF1_fnc,X0),rd(X0,sF1_fnc))=asoc(i(mult(sF1_fnc,X1)),X1,X0))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f1259,f6696])).
% 3.23/0.88 fof(f6698,plain,(
% 3.23/0.88 ![X0,X1]: (rd(rd(X0,sF1_fnc),unit)=mult(i(mult(sF1_fnc,X1)),mult(X1,X0)))),
% 3.23/0.88 inference(backward_demodulation,[status(thm)],[f6700,f4764])).
% 3.23/0.88 fof(f6700,plain,(
% 3.23/0.88 ![X0,X1]: (unit=asoc(i(mult(sF1_fnc,X0)),X0,X1))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f523,f6697])).
% 3.23/0.88 fof(f6748,plain,(
% 3.23/0.88 ![X0,X1]: (mult(rd(X0,sF1_fnc),X1)=mult(X0,rd(X1,sF1_fnc)))),
% 3.23/0.88 inference(backward_demodulation,[status(thm)],[f6749,f4541])).
% 3.23/0.88 fof(f6749,plain,(
% 3.23/0.88 ![X0,X1]: (rd(X0,sF1_fnc)=mult(i(mult(sF1_fnc,X1)),mult(X1,X0)))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f291,f6698])).
% 3.23/0.88 fof(f6784,plain,(
% 3.23/0.88 ![X0,X1]: (mult(X0,X1)=mult(sF1_fnc,mult(X0,rd(X1,sF1_fnc))))),
% 3.23/0.88 inference(backward_demodulation,[status(thm)],[f6748,f1254])).
% 3.23/0.88 fof(f6795,plain,(
% 3.23/0.88 ![X0,X1]: (mult(i(mult(X0,X1)),mult(X0,X1))=asoc(X0,sF1_fnc,rd(X1,sF1_fnc)))),
% 3.23/0.88 inference(backward_demodulation,[status(thm)],[f6784,f6616])).
% 3.23/0.88 fof(f6802,plain,(
% 3.23/0.88 ![X0,X1]: (unit=asoc(X0,sF1_fnc,rd(X1,sF1_fnc)))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f25,f6795])).
% 3.23/0.88 fof(f6883,plain,(
% 3.23/0.88 ![X0,X1]: (unit=asoc(X0,sF1_fnc,mult(sF1_fnc,rd(X1,sF1_fnc))))),
% 3.23/0.88 inference(paramodulation,[status(thm)],[f868,f6802])).
% 3.23/0.88 fof(f6903,plain,(
% 3.23/0.88 unit=sF0_fnc),
% 3.23/0.88 inference(backward_demodulation,[status(thm)],[f6929,f6619])).
% 3.23/0.88 fof(f6929,plain,(
% 3.23/0.88 ![X0,X1]: (unit=asoc(X0,sF1_fnc,X1))),
% 3.23/0.88 inference(forward_demodulation,[status(thm)],[f1071,f6883])).
% 3.23/0.88 fof(f6948,plain,(
% 3.23/0.88 $false),
% 3.23/0.88 inference(forward_subsumption_resolution,[status(thm)],[f6903,f45])).
% 3.23/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.87/0.91 % Elapsed time: 0.536109 seconds
% 0.87/0.91 % CPU time: 4.040216 seconds
% 0.87/0.91 % Total memory used: 130.237 MB
% 0.87/0.91 % Net memory used: 128.326 MB
%------------------------------------------------------------------------------