%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP705-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 : n019.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:13 PM UTC 2026
% Result : Unsatisfiable 90.53s 11.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP705-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:34:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 90.53/11.87 % Refutation found
% 90.53/11.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 90.53/11.87 % SZS output start CNFRefutation for theBenchmark
% 90.53/11.87 fof(f1,axiom,(
% 90.53/11.87 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f2,axiom,(
% 90.53/11.87 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f3,axiom,(
% 90.53/11.87 (![A,B]: (mult(rd(A,B),B) = A ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f4,axiom,(
% 90.53/11.87 (![A,B]: (rd(mult(A,B),B) = A ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f5,axiom,(
% 90.53/11.87 (![A]: (mult(A,unit) = A ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f6,axiom,(
% 90.53/11.87 (![A]: (mult(unit,A) = A ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f7,axiom,(
% 90.53/11.87 (![A,B,C]: (mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C) ))),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f9,axiom,(
% 90.53/11.87 mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = unit ),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f10,negated_conjecture,(
% 90.53/11.87 mult(op_a,mult(op_b,a)) != mult(mult(op_a,op_b),a) ),
% 90.53/11.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 90.53/11.87 fof(f11,plain,(
% 90.53/11.87 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f1])).
% 90.53/11.87 fof(f12,plain,(
% 90.53/11.87 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f2])).
% 90.53/11.87 fof(f13,plain,(
% 90.53/11.87 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f3])).
% 90.53/11.87 fof(f14,plain,(
% 90.53/11.87 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f4])).
% 90.53/11.87 fof(f15,plain,(
% 90.53/11.87 ![X0]: (mult(X0,unit)=X0)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f5])).
% 90.53/11.87 fof(f16,plain,(
% 90.53/11.87 ![X0]: (mult(unit,X0)=X0)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f6])).
% 90.53/11.87 fof(f17,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,X2)))=mult(mult(mult(X0,X1),X1),X2))),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f7])).
% 90.53/11.87 fof(f19,plain,(
% 90.53/11.87 mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))))=unit),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f9])).
% 90.53/11.87 fof(f20,plain,(
% 90.53/11.87 ~mult(op_a,mult(op_b,a))=mult(mult(op_a,op_b),a)),
% 90.53/11.87 inference(cnf_transformation,[status(thm)],[f10])).
% 90.53/11.87 fof(f58,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,ld(mult(mult(X0,X1),X1),X2))))=X2)),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f11,f17])).
% 90.53/11.87 fof(f59,plain,(
% 90.53/11.87 ![X0,X1]: (mult(X0,mult(X1,mult(X1,unit)))=mult(mult(X0,X1),X1))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f15,f17])).
% 90.53/11.87 fof(f60,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(mult(X0,X1),mult(X1,mult(X1,X2)))=mult(mult(X0,mult(X1,mult(X1,X1))),X2))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f17,f17])).
% 90.53/11.87 fof(f62,plain,(
% 90.53/11.87 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),X1),mult(X2,mult(X2,X3)))=mult(mult(mult(X0,mult(X1,mult(X1,X2))),X2),X3))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f17,f17])).
% 90.53/11.87 fof(f63,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(rd(X0,X1),mult(X1,mult(X1,X2)))=mult(mult(X0,X1),X2))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f13,f17])).
% 90.53/11.87 fof(f64,plain,(
% 90.53/11.87 ![X0,X1]: (mult(unit,mult(X0,mult(X0,X1)))=mult(mult(X0,X0),X1))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f16,f17])).
% 90.53/11.87 fof(f71,plain,(
% 90.53/11.87 ![X0,X1]: (mult(X0,mult(X1,X1))=mult(mult(X0,X1),X1))),
% 90.53/11.87 inference(forward_demodulation,[status(thm)],[f15,f59])).
% 90.53/11.87 fof(f74,plain,(
% 90.53/11.87 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,X3)))))=mult(mult(mult(X0,mult(X1,mult(X1,X2))),X2),X3))),
% 90.53/11.87 inference(forward_demodulation,[status(thm)],[f17,f62])).
% 90.53/11.87 fof(f75,plain,(
% 90.53/11.87 ![X0,X1]: (mult(X0,mult(X0,X1))=mult(mult(X0,X0),X1))),
% 90.53/11.87 inference(forward_demodulation,[status(thm)],[f16,f64])).
% 90.53/11.87 fof(f85,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,X2)))=mult(mult(X0,mult(X1,X1)),X2))),
% 90.53/11.87 inference(backward_demodulation,[status(thm)],[f71,f17])).
% 90.53/11.87 fof(f304,plain,(
% 90.53/11.87 ld(op_b,unit)=mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f19,f12])).
% 90.53/11.87 fof(f540,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(mult(X0,X0),mult(X1,mult(X1,X2)))=mult(mult(X0,mult(X0,mult(X1,X1))),X2))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f75,f85])).
% 90.53/11.87 fof(f546,plain,(
% 90.53/11.87 ![X0,X1,X2,X3]: (mult(X0,mult(mult(X1,mult(X2,X2)),mult(mult(X1,mult(X2,X2)),X3)))=mult(mult(X0,mult(X1,mult(X2,mult(X2,mult(X1,mult(X2,X2)))))),X3))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f85,f85])).
% 90.53/11.87 fof(f575,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(mult(X0,mult(X1,X1)),mult(X2,X2))=mult(mult(X0,mult(X1,mult(X1,X2))),X2))),
% 90.53/11.87 inference(paramodulation,[status(thm)],[f85,f71])).
% 90.53/11.87 fof(f582,plain,(
% 90.53/11.87 ![X0,X1,X2]: (mult(X0,mult(X0,mult(X1,mult(X1,X2))))=mult(mult(X0,mult(X0,mult(X1,X1))),X2))),
% 90.53/11.87 inference(forward_demodulation,[status(thm)],[f75,f540])).
% 90.53/11.87 fof(f588,plain,(
% 90.53/11.87 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X2,mult(X2,mult(mult(X1,mult(X2,X2)),X3)))))=mult(mult(X0,mult(X1,mult(X2,mult(X2,mult(X1,mult(X2,X2)))))),X3))),
% 90.53/11.87 inference(forward_demodulation,[status(thm)],[f85,f546])).
% 90.53/11.87 fof(f589,plain,(
% 90.53/11.87 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X2,mult(X2,mult(X1,mult(X2,mult(X2,X3)))))))=mult(mult(X0,mult(X1,mult(X2,mult(X2,mult(X1,mult(X2,X2)))))),X3))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f85,f588])).
% 90.53/11.88 fof(f616,plain,(
% 90.53/11.88 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,mult(X2,X2))))=mult(mult(X0,mult(X1,mult(X1,X2))),X2))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f85,f575])).
% 90.53/11.88 fof(f718,plain,(
% 90.53/11.88 ![X0,X1,X2]: (mult(X0,mult(X1,mult(X1,ld(mult(X0,mult(X1,X1)),X2))))=X2)),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f71,f58])).
% 90.53/11.88 fof(f915,plain,(
% 90.53/11.88 ![X0,X1,X2,X3]: (mult(mult(mult(X0,mult(X1,X1)),X2),mult(X2,mult(X2,X3)))=mult(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,X2))))),X3))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f85,f60])).
% 90.53/11.88 fof(f971,plain,(
% 90.53/11.88 ![X0,X1,X2,X3]: (mult(mult(X0,mult(X1,mult(X1,X2))),mult(X2,mult(X2,X3)))=mult(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,X2))))),X3))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f85,f915])).
% 90.53/11.88 fof(f1122,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0)))))=mult(mult(unit,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),X0))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f19,f74])).
% 90.53/11.88 fof(f1132,plain,(
% 90.53/11.88 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),X1)))))=mult(mult(mult(X0,unit),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f19,f74])).
% 90.53/11.88 fof(f1140,plain,(
% 90.53/11.88 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1)))))=mult(mult(mult(X0,mult(op_b,unit)),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),X1))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f19,f74])).
% 90.53/11.88 fof(f1157,plain,(
% 90.53/11.88 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,mult(mult(mult(X1,mult(X2,mult(X2,X3))),X3),ld(mult(X0,mult(mult(mult(X1,mult(X2,mult(X2,X3))),X3),mult(mult(X1,mult(X2,mult(X2,X3))),X3))),X4))))))))=X4)),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f74,f718])).
% 90.53/11.88 fof(f1200,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0)))))=mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f16,f1122])).
% 90.53/11.88 fof(f1207,plain,(
% 90.53/11.88 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),X1)))))=mult(mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f15,f1132])).
% 90.53/11.88 fof(f1224,plain,(
% 90.53/11.88 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1)))))=mult(mult(mult(X0,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),X1))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f15,f1140])).
% 90.53/11.88 fof(f1257,plain,(
% 90.53/11.88 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,ld(mult(X0,mult(mult(mult(X1,mult(X2,mult(X2,X3))),X3),mult(mult(X1,mult(X2,mult(X2,X3))),X3))),X4))))))))))))=X4)),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f74,f1157])).
% 90.53/11.88 fof(f1258,plain,(
% 90.53/11.88 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,ld(mult(X0,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,mult(mult(X1,mult(X2,mult(X2,X3))),X3))))))),X4))))))))))))=X4)),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f74,f1257])).
% 90.53/11.88 fof(f1392,plain,(
% 90.53/11.88 ![X0,X1,X2]: (mult(rd(X0,X1),mult(X1,X2))=mult(mult(X0,X1),ld(X1,X2)))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f11,f63])).
% 90.53/11.88 fof(f12785,plain,(
% 90.53/11.88 ![X0,X1]: (mult(rd(X0,X1),X1)=mult(mult(X0,X1),ld(X1,unit)))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f15,f1392])).
% 90.53/11.88 fof(f12951,plain,(
% 90.53/11.88 ![X0,X1]: (X0=mult(mult(X0,X1),ld(X1,unit)))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f13,f12785])).
% 90.53/11.88 fof(f13137,plain,(
% 90.53/11.88 ![X0,X1]: (rd(X0,X1)=mult(X0,ld(X1,unit)))),
% 90.53/11.88 inference(paramodulation,[status(thm)],[f13,f12951])).
% 90.53/11.88 fof(f48030,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,op_b))),mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0)))))))=mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f971,f1200])).
% 90.53/11.88 fof(f48031,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0))))))))))=mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f582,f48030])).
% 90.53/11.88 fof(f48032,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,op_b))),mult(op_b,mult(op_b,X0))))))))))))=mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f971,f48031])).
% 90.53/11.88 fof(f48033,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X0)))))))))))))))=mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))),X0))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f582,f48032])).
% 90.53/11.88 fof(f48034,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X0)))))))))))))))=mult(mult(op_b,mult(op_b,mult(op_b,op_b))),mult(op_b,mult(op_b,X0))))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f971,f48033])).
% 90.53/11.88 fof(f48035,plain,(
% 90.53/11.88 ![X0]: (mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X0)))))))))))))))=mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X0)))))))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f582,f48034])).
% 90.53/11.88 fof(f66492,plain,(
% 90.53/11.88 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),X1)))))))))))=mult(mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1))),
% 90.53/11.88 inference(forward_demodulation,[status(thm)],[f589,f1207])).
% 90.53/11.88 fof(f66493,plain,(
% 90.53/11.88 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1)))))))))))))))))=mult(mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f589,f66492])).
% 72.09/12.03 fof(f66494,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))))))=mult(mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f48035,f66493])).
% 72.09/12.03 fof(f87596,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),X1))))))))))))=mult(mult(mult(X0,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f66494,f1224])).
% 72.09/12.03 fof(f87597,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1)))))))))))))))))))=mult(mult(mult(X0,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f66494,f87596])).
% 72.09/12.03 fof(f87598,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))))))))=mult(mult(mult(X0,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f48035,f87597])).
% 72.09/12.03 fof(f87599,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))))))))=mult(mult(mult(X0,op_b),ld(op_b,unit)),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f304,f87598])).
% 72.09/12.03 fof(f87600,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))))))))=mult(rd(mult(X0,op_b),op_b),X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f13137,f87599])).
% 72.09/12.03 fof(f87602,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))))))))=mult(X0,X1))),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f14,f87600])).
% 72.09/12.03 fof(f101159,plain,(
% 72.09/12.03 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,ld(mult(X0,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,mult(X1,mult(X2,mult(X2,mult(X3,X3)))))))))),X4))))))))))))=X4)),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f616,f1258])).
% 72.09/12.03 fof(f101195,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,ld(mult(X0,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))))),X1)))=X1)),
% 72.09/12.03 inference(paramodulation,[status(thm)],[f87602,f101159])).
% 72.09/12.03 fof(f102126,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,ld(mult(X0,op_b),X1)))=X1)),
% 72.09/12.03 inference(forward_demodulation,[status(thm)],[f87602,f101195])).
% 72.09/12.03 fof(f105902,plain,(
% 72.09/12.03 ![X0,X1]: (mult(X0,mult(op_b,X1))=mult(mult(X0,op_b),X1))),
% 72.09/12.03 inference(paramodulation,[status(thm)],[f12,f102126])).
% 72.09/12.03 fof(f106786,plain,(
% 72.09/12.03 ~mult(op_a,mult(op_b,a))=mult(op_a,mult(op_b,a))),
% 72.09/12.03 inference(backward_demodulation,[status(thm)],[f105902,f20])).
% 72.09/12.03 fof(f107219,plain,(
% 72.09/12.03 $false),
% 72.09/12.03 inference(trivial_equality_resolution,[status(thm)],[f106786])).
% 72.09/12.03 % SZS output end CNFRefutation for theBenchmark.p
% 60.54/13.27 % Elapsed time: 12.668346 seconds
% 60.54/13.27 % CPU time: 43.202092 seconds
% 60.54/13.27 % Total memory used: 603.933 MB
% 60.54/13.27 % Net memory used: 593.350 MB
%------------------------------------------------------------------------------