%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG236-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 : n002.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 11:49:55 AM UTC 2026
% Result : Unsatisfiable 9.37s 1.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG236-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n002.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 13:12:02 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.43 % Drodi V4.1.1
% 9.37/1.66 % Refutation found
% 9.37/1.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.37/1.66 % SZS output start CNFRefutation for theBenchmark
% 9.37/1.66 fof(f1,axiom,(
% 9.37/1.66 (![A,B]: (mult(A,mult(B,mult(A,B))) = mult(A,B) ))),
% 9.37/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.37/1.66 fof(f2,axiom,(
% 9.37/1.66 (![A,B,C,D]: (mult(A,mult(B,mult(C,D))) = mult(C,mult(B,mult(A,D))) ))),
% 9.37/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.37/1.66 fof(f3,axiom,(
% 9.37/1.66 (![A,B,C,D]: (mult(mult(A,mult(B,mult(C,B))),D) = mult(A,mult(D,mult(mult(C,B),D))) ))),
% 9.37/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.37/1.66 fof(f4,negated_conjecture,(
% 9.37/1.66 mult(mult(a,b),mult(c,mult(d,e))) != mult(a,mult(c,mult(mult(d,b),e))) ),
% 9.37/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.37/1.66 fof(f5,plain,(
% 9.37/1.66 ![X0,X1]: (mult(X0,mult(X1,mult(X0,X1)))=mult(X0,X1))),
% 9.37/1.66 inference(cnf_transformation,[status(thm)],[f1])).
% 9.37/1.66 fof(f6,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X2,X3)))=mult(X2,mult(X1,mult(X0,X3))))),
% 9.37/1.66 inference(cnf_transformation,[status(thm)],[f2])).
% 9.37/1.66 fof(f7,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,mult(X1,mult(X2,X1))),X3)=mult(X0,mult(X3,mult(mult(X2,X1),X3))))),
% 9.37/1.66 inference(cnf_transformation,[status(thm)],[f3])).
% 9.37/1.66 fof(f8,plain,(
% 9.37/1.66 ~mult(mult(a,b),mult(c,mult(d,e)))=mult(a,mult(c,mult(mult(d,b),e)))),
% 9.37/1.66 inference(cnf_transformation,[status(thm)],[f4])).
% 9.37/1.66 fof(f22,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X3,X4))))=mult(X2,mult(X3,mult(X0,mult(X1,X4)))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f6,f6])).
% 9.37/1.66 fof(f24,plain,(
% 9.37/1.66 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(X2,mult(X1,mult(X0,mult(X1,X2)))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f5,f6])).
% 9.37/1.66 fof(f27,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X2,X3)))=mult(X2,mult(X1,mult(X0,mult(X3,mult(X2,X3))))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f5,f6])).
% 9.37/1.66 fof(f69,plain,(
% 9.37/1.66 ![X0,X1]: (mult(X0,mult(X1,mult(X0,X1)))=mult(mult(X0,X1),mult(X1,mult(X0,X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f24,f24])).
% 9.37/1.66 fof(f94,plain,(
% 9.37/1.66 ![X0,X1]: (mult(X0,X1)=mult(mult(X0,X1),mult(X1,mult(X0,X1))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f5,f69])).
% 9.37/1.66 fof(f111,plain,(
% 9.37/1.66 ![X0,X1]: (mult(X0,X1)=mult(X0,mult(X1,mult(mult(X0,X1),X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f6,f94])).
% 9.37/1.66 fof(f158,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,mult(X1,mult(X2,X1))),X3)=mult(X2,mult(X3,mult(mult(X0,X1),X3))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f6,f7])).
% 9.37/1.66 fof(f160,plain,(
% 9.37/1.66 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X0,mult(X2,mult(mult(X0,X1),X2))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f5,f7])).
% 9.37/1.66 fof(f161,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,mult(X1,X2)),X3)=mult(X0,mult(X3,mult(mult(X2,mult(X1,X2)),X3))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f94,f7])).
% 9.37/1.66 fof(f173,plain,(
% 9.37/1.66 ![X0,X1,X2]: (mult(mult(mult(mult(X0,X1),X2),mult(X1,mult(X0,X1))),X2)=mult(mult(X0,X1),X2))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f94,f7])).
% 9.37/1.66 fof(f223,plain,(
% 9.37/1.66 ![X0,X1]: (mult(X0,X1)=mult(mult(X0,X1),X1))),
% 9.37/1.66 inference(backward_demodulation,[status(thm)],[f160,f111])).
% 9.37/1.66 fof(f273,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,X1),mult(X2,mult(X3,X1)))=mult(X3,mult(X2,mult(X0,X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f223,f6])).
% 9.37/1.66 fof(f431,plain,(
% 9.37/1.66 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X1)=mult(mult(mult(X0,X1),X2),mult(X1,mult(X0,X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f160,f273])).
% 9.37/1.66 fof(f449,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,X1),mult(X2,mult(X3,X1)))=mult(X3,mult(mult(X2,mult(X3,X1)),mult(X0,X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f223,f273])).
% 9.37/1.66 fof(f459,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,X1),mult(X2,mult(X3,X1)))=mult(mult(X3,X1),mult(X2,mult(X0,X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f223,f273])).
% 9.37/1.66 fof(f495,plain,(
% 9.37/1.66 ![X0,X1,X2]: (mult(mult(mult(mult(X0,X1),X2),X1),X2)=mult(mult(X0,X1),X2))),
% 9.37/1.66 inference(backward_demodulation,[status(thm)],[f431,f173])).
% 9.37/1.66 fof(f517,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X2,X3)))=mult(X0,mult(mult(X1,mult(X0,X3)),mult(X2,X3))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f273,f449])).
% 9.37/1.66 fof(f527,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(X2,X3)))=mult(mult(X0,X3),mult(X1,mult(X2,X3))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f273,f459])).
% 9.37/1.66 fof(f621,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(mult(X0,X1),mult(X2,mult(mult(X3,X4),X1)))=mult(mult(mult(mult(X3,X4),X1),X4),mult(X2,mult(X0,X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f495,f273])).
% 9.37/1.66 fof(f669,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(mult(X0,X1),mult(X2,mult(X3,X4)))=mult(mult(mult(mult(X0,X1),X4),X1),mult(X2,mult(X3,X4))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f273,f621])).
% 9.37/1.66 fof(f686,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(X0,mult(X1,mult(mult(X2,X3),X1)))=mult(mult(mult(X0,X1),mult(X3,mult(X2,X3))),X1))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f7,f527])).
% 9.37/1.66 fof(f1120,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X1),mult(X4,mult(X3,X2)))=mult(X3,mult(X4,mult(mult(X0,X1),mult(X2,mult(X3,X2))))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f495,f27])).
% 9.37/1.66 fof(f1173,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X3,mult(X4,mult(X1,X4))))))=mult(mult(X0,mult(X3,mult(X4,mult(X1,X4)))),mult(X3,mult(X2,mult(X1,X4)))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f27,f527])).
% 9.37/1.66 fof(f1207,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(mult(X0,mult(X1,mult(mult(X2,X3),X1))),mult(X4,mult(X2,X3)))=mult(X2,mult(X4,mult(mult(X0,X1),mult(X3,mult(X2,X3))))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f686,f1120])).
% 9.37/1.66 fof(f1210,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(mult(X0,mult(X1,mult(mult(X2,X3),X1))),mult(X4,mult(X2,X3)))=mult(mult(X0,X1),mult(X4,mult(X2,X3))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f27,f1207])).
% 9.37/1.66 fof(f1260,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(X2,mult(X3,X4))))=mult(mult(X0,mult(X1,mult(X4,mult(X3,X4)))),mult(X1,mult(X2,mult(X3,X4)))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f27,f1173])).
% 9.37/1.66 fof(f1539,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(X0,mult(X1,mult(mult(X2,X3),X1))),X3)=mult(mult(X0,X1),mult(X3,mult(X2,X3))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f273,f158])).
% 9.37/1.66 fof(f2360,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),X1)=mult(X0,mult(X1,mult(mult(X3,mult(X2,X3)),X1))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f527,f161])).
% 9.37/1.66 fof(f2381,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(mult(X0,mult(X1,X2)),mult(X3,mult(X4,X5)))=mult(X0,mult(X3,mult(X4,mult(mult(X3,mult(X4,X5)),mult(mult(X2,mult(X1,X2)),X5))))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f22,f161])).
% 9.37/1.66 fof(f2397,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(mult(X0,mult(X1,X2)),mult(X3,mult(X4,mult(X5,mult(mult(X2,mult(X1,X2)),X5)))))=mult(X0,mult(mult(X3,mult(X4,mult(X5,mult(mult(X2,mult(X1,X2)),X5)))),mult(X4,mult(X3,mult(mult(X2,mult(X1,X2)),X5))))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f27,f161])).
% 9.37/1.66 fof(f2499,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(X0,mult(X1,mult(X2,mult(X3,mult(mult(X4,mult(X5,X4)),X3)))))=mult(mult(X0,mult(X3,mult(mult(X4,mult(X5,X4)),X3))),mult(X1,mult(mult(X2,mult(X5,X4)),X3))))),
% 9.37/1.66 inference(paramodulation,[status(thm)],[f161,f527])).
% 9.37/1.66 fof(f2545,plain,(
% 9.37/1.66 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),X1)=mult(mult(X0,mult(X2,X3)),X1))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f161,f2360])).
% 9.37/1.66 fof(f2573,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(mult(X0,mult(X1,X2)),mult(X3,mult(X4,X5)))=mult(X0,mult(X3,mult(X4,mult(X3,mult(mult(X2,mult(X1,X2)),X5))))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f517,f2381])).
% 9.37/1.66 fof(f2595,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(mult(X0,mult(X1,X2)),mult(X3,mult(mult(X4,mult(X1,X2)),X5)))=mult(X0,mult(mult(X3,mult(X4,mult(X5,mult(mult(X2,mult(X1,X2)),X5)))),mult(X4,mult(X3,mult(mult(X2,mult(X1,X2)),X5))))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f161,f2397])).
% 9.37/1.66 fof(f2596,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(mult(X0,mult(X1,X2)),mult(X3,mult(mult(X4,mult(X1,X2)),X5)))=mult(X0,mult(X3,mult(X4,mult(X3,mult(mult(X2,mult(X1,X2)),X5))))))),
% 9.37/1.66 inference(forward_demodulation,[status(thm)],[f1260,f2595])).
% 9.37/1.66 fof(f2597,plain,(
% 9.37/1.66 ![X0,X1,X2,X3,X4,X5]: (mult(mult(X0,mult(X1,X2)),mult(X3,mult(mult(X4,mult(X1,X2)),X5)))=mult(mult(X0,mult(X1,X2)),mult(X3,mult(X4,X5))))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f2573,f2596])).
% 9.37/1.68 fof(f2737,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4,X5]: (mult(X0,mult(X1,mult(mult(X2,mult(X3,X4)),X5)))=mult(mult(X0,mult(X5,mult(mult(X4,mult(X3,X4)),X5))),mult(X1,mult(mult(X2,mult(X3,X4)),X5))))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f161,f2499])).
% 9.37/1.68 fof(f2738,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4,X5]: (mult(X0,mult(X1,mult(mult(X2,mult(X3,X4)),X5)))=mult(mult(mult(X0,mult(X3,X4)),X5),mult(X1,mult(mult(X2,mult(X3,X4)),X5))))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f161,f2737])).
% 9.37/1.68 fof(f2739,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4,X5]: (mult(X0,mult(X1,mult(mult(X2,mult(X3,X4)),X5)))=mult(mult(X0,mult(X3,X4)),mult(X1,mult(X2,X5))))),
% 9.37/1.68 inference(backward_demodulation,[status(thm)],[f2740,f2597])).
% 9.37/1.68 fof(f2740,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4,X5]: (mult(X0,mult(X1,mult(mult(X2,mult(X3,X4)),X5)))=mult(mult(X0,mult(X3,X4)),mult(X1,mult(mult(X2,mult(X3,X4)),X5))))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f527,f2738])).
% 9.37/1.68 fof(f2799,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(mult(X2,mult(X3,mult(mult(X2,X4),X3))),X4)))=mult(mult(X0,X3),mult(X1,mult(X2,X4))))),
% 9.37/1.68 inference(backward_demodulation,[status(thm)],[f2739,f1210])).
% 9.37/1.68 fof(f2953,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(mult(X2,X3),mult(X4,mult(X2,X4)))))=mult(mult(X0,X3),mult(X1,mult(X2,X4))))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f1539,f2799])).
% 9.37/1.68 fof(f3117,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4]: (mult(mult(X0,mult(X1,mult(mult(X2,X3),X4))),X3)=mult(mult(X2,mult(X1,mult(X0,X4))),X3))),
% 9.37/1.68 inference(paramodulation,[status(thm)],[f6,f2545])).
% 9.37/1.68 fof(f3119,plain,(
% 9.37/1.68 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X1)=mult(mult(X0,mult(X2,mult(mult(X0,X1),X2))),X1))),
% 9.37/1.68 inference(paramodulation,[status(thm)],[f5,f2545])).
% 9.37/1.68 fof(f3270,plain,(
% 9.37/1.68 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X1)=mult(mult(X0,mult(X2,mult(X0,X2))),X1))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f3117,f3119])).
% 9.37/1.68 fof(f3281,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4]: (mult(mult(X0,X1),mult(X2,mult(X3,X4)))=mult(mult(mult(X0,X4),X1),mult(X2,mult(X3,X4))))),
% 9.37/1.68 inference(backward_demodulation,[status(thm)],[f3283,f669])).
% 9.37/1.68 fof(f3282,plain,(
% 9.37/1.68 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(mult(X0,X2),X1),mult(X2,mult(X0,X2))))),
% 9.37/1.68 inference(backward_demodulation,[status(thm)],[f3283,f431])).
% 9.37/1.68 fof(f3283,plain,(
% 9.37/1.68 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X1)=mult(mult(X0,X2),X1))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f5,f3270])).
% 9.37/1.68 fof(f3504,plain,(
% 9.37/1.68 ![X0,X1,X2,X3,X4]: (mult(X0,mult(X1,mult(mult(X2,X3),X4)))=mult(mult(X0,X3),mult(X1,mult(X2,X4))))),
% 9.37/1.68 inference(backward_demodulation,[status(thm)],[f3505,f2953])).
% 9.37/1.68 fof(f3505,plain,(
% 9.37/1.68 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X1),mult(X2,mult(X0,X2))))),
% 9.37/1.68 inference(forward_demodulation,[status(thm)],[f3281,f3282])).
% 9.37/1.68 fof(f3526,plain,(
% 9.37/1.68 ~mult(a,mult(c,mult(mult(d,b),e)))=mult(a,mult(c,mult(mult(d,b),e)))),
% 9.37/1.68 inference(backward_demodulation,[status(thm)],[f3504,f8])).
% 9.37/1.68 fof(f3645,plain,(
% 9.37/1.68 $false),
% 9.37/1.68 inference(trivial_equality_resolution,[status(thm)],[f3526])).
% 9.37/1.68 % SZS output end CNFRefutation for theBenchmark.p
% 30.00/33.24 % Elapsed time: 32.806846 seconds
% 30.00/33.24 % CPU time: 256.533761 seconds
% 30.00/33.24 % Total memory used: 131.538 GB
% 30.00/33.24 % Net memory used: 131.535 GB
%------------------------------------------------------------------------------