%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG236-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:05 AM UTC 2026
% Result : Unsatisfiable 11.79s 2.09s
% Output : CNFRefutation 11.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 4
% Syntax : Number of formulae : 112 ( 112 unt; 0 def)
% Number of atoms : 112 ( 111 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 416 ( 416 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : mult(A,mult(B,mult(A,B))) = mult(A,B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C,D] : mult(A,mult(B,mult(C,D))) = mult(C,mult(B,mult(A,D))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B,C,D] : mult(mult(A,mult(B,mult(C,B))),D) = mult(A,mult(D,mult(mult(C,B),D))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
mult(mult(a,b),mult(c,mult(d,e))) != mult(a,mult(c,mult(mult(d,b),e))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,plain,
! [X0,X1] : mult(X0,mult(X1,mult(X0,X1))) = mult(X0,X1),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f6,plain,
! [X0,X1,X2,X3] : mult(X0,mult(X1,mult(X2,X3))) = mult(X2,mult(X1,mult(X0,X3))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f7,plain,
! [X0,X1,X2,X3] : mult(mult(X0,mult(X1,mult(X2,X1))),X3) = mult(X0,mult(X3,mult(mult(X2,X1),X3))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f8,plain,
mult(mult(a,b),mult(c,mult(d,e))) != mult(a,mult(c,mult(mult(d,b),e))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f18,plain,
! [X0,X1] : mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))) = mult(X0,mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f5,f5]) ).
fof(f19,plain,
! [X0,X1] : mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))) = mult(X0,X1),
inference(forward_demodulation,[status(thm)],[f5,f18]) ).
fof(f21,plain,
! [X0,X1] : mult(X0,mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,mult(X1,mult(X0,X1))))) = mult(X0,mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f5,f19]) ).
fof(f27,plain,
! [X0,X1] : mult(X0,mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1))) = mult(X0,mult(X1,mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f5,f21]) ).
fof(f28,plain,
! [X0,X1] : mult(X0,mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1))) = mult(X0,X1),
inference(forward_demodulation,[status(thm)],[f5,f27]) ).
fof(f35,plain,
! [X0,X1] : mult(X0,mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1)))),mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))))) = mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))),
inference(paramodulation,[status(thm)],[f19,f28]) ).
fof(f49,plain,
! [X0,X1] : mult(X0,mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))))) = mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f19,f35]) ).
fof(f50,plain,
! [X0,X1] : mult(X0,mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))) = mult(X0,mult(mult(X1,mult(X0,X1)),mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f19,f49]) ).
fof(f51,plain,
! [X0,X1] : mult(X0,mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))) = mult(X0,X1),
inference(forward_demodulation,[status(thm)],[f19,f50]) ).
fof(f372,plain,
! [X0,X1,X2] : mult(X0,mult(X1,X2)) = mult(mult(mult(X2,mult(X1,X2)),mult(X1,X2)),mult(X1,mult(X0,mult(X1,X2)))),
inference(paramodulation,[status(thm)],[f28,f6]) ).
fof(f374,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(X2,mult(X3,X4)))) = mult(X2,mult(X3,mult(X0,mult(X1,X4)))),
inference(paramodulation,[status(thm)],[f6,f6]) ).
fof(f376,plain,
! [X0,X1,X2] : mult(X0,mult(X1,X2)) = mult(X2,mult(X1,mult(X0,mult(X1,X2)))),
inference(paramodulation,[status(thm)],[f5,f6]) ).
fof(f406,plain,
mult(d,mult(c,mult(mult(a,b),e))) != mult(a,mult(c,mult(mult(d,b),e))),
inference(paramodulation,[status(thm)],[f6,f8]) ).
fof(f486,plain,
! [X0,X1] : mult(mult(mult(mult(mult(X0,mult(X1,X0)),mult(X1,X0)),mult(X1,X0)),mult(X1,X0)),mult(X1,X0)) = mult(mult(mult(X0,mult(X1,X0)),mult(X1,X0)),mult(X1,X0)),
inference(paramodulation,[status(thm)],[f51,f372]) ).
fof(f490,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = mult(mult(mult(X0,mult(X1,X0)),mult(X1,X0)),mult(X1,X0)),
inference(paramodulation,[status(thm)],[f5,f372]) ).
fof(f492,plain,
! [X0,X1] : mult(X0,mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))) = mult(mult(mult(mult(X0,X1),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),
inference(paramodulation,[status(thm)],[f51,f372]) ).
fof(f600,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(mult(mult(X0,X1),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f51,f492]) ).
fof(f601,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X1),mult(mult(mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f490,f600]) ).
fof(f602,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X1),mult(mult(mult(X1,mult(X0,X1)),mult(X0,X1)),mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f486,f601]) ).
fof(f603,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X1),mult(X1,mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f490,f602]) ).
fof(f748,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,mult(X1,mult(mult(X0,X1),X1))),
inference(paramodulation,[status(thm)],[f6,f603]) ).
fof(f922,plain,
! [X0,X1] : mult(X0,mult(X1,mult(mult(X0,X1),X1))) = mult(mult(mult(X0,X1),X1),mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f748,f376]) ).
fof(f948,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(mult(X0,X1),X1),mult(X1,mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f748,f922]) ).
fof(f980,plain,
! [X0,X1] : mult(X0,X1) = mult(X0,mult(X1,mult(mult(mult(X0,X1),X1),X1))),
inference(paramodulation,[status(thm)],[f6,f948]) ).
fof(f2149,plain,
! [X0,X1,X2] : mult(mult(X0,X1),X2) = mult(X0,mult(X2,mult(mult(mult(X0,X1),X1),X2))),
inference(paramodulation,[status(thm)],[f748,f7]) ).
fof(f2152,plain,
! [X0,X1,X2] : mult(mult(X0,X1),X2) = mult(X0,mult(X2,mult(mult(X0,X1),X2))),
inference(paramodulation,[status(thm)],[f5,f7]) ).
fof(f2278,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f2149,f980]) ).
fof(f2741,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,mult(X3,X1))) = mult(X3,mult(X2,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f2278,f6]) ).
fof(f2824,plain,
! [X0,X1,X2,X3] : mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X1) = mult(mult(X3,X2),mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f7,f2741]) ).
fof(f2842,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,mult(X3,X1))) = mult(X3,mult(mult(X2,mult(X3,X1)),mult(X0,X1))),
inference(paramodulation,[status(thm)],[f2278,f2741]) ).
fof(f2852,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,mult(X3,X1))) = mult(mult(X3,X1),mult(X2,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f2278,f2741]) ).
fof(f2904,plain,
! [X0,X1,X2,X3] : mult(X0,mult(X1,mult(X2,X3))) = mult(X0,mult(mult(X1,mult(X0,X3)),mult(X2,X3))),
inference(forward_demodulation,[status(thm)],[f2741,f2842]) ).
fof(f2916,plain,
! [X0,X1,X2,X3] : mult(X0,mult(X1,mult(X2,X3))) = mult(mult(X0,X3),mult(X1,mult(X2,X3))),
inference(forward_demodulation,[status(thm)],[f2741,f2852]) ).
fof(f2981,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(mult(X1,X2),mult(X3,mult(X4,X2)))) = mult(mult(X0,mult(X4,X2)),mult(X4,mult(X3,mult(X1,X2)))),
inference(paramodulation,[status(thm)],[f2741,f2916]) ).
fof(f3049,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(X2,mult(X3,X4)))) = mult(mult(X0,mult(X3,X4)),mult(X3,mult(X2,mult(X1,X4)))),
inference(forward_demodulation,[status(thm)],[f2916,f2981]) ).
fof(f3109,plain,
! [X0,X1,X2] : mult(mult(mult(X0,X1),X2),X1) = mult(mult(mult(X0,X1),X2),mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f5,f2824]) ).
fof(f3295,plain,
! [X0,X1,X2] : mult(mult(mult(X0,X1),X2),X1) = mult(X0,mult(X1,mult(mult(mult(X0,X1),X2),X1))),
inference(paramodulation,[status(thm)],[f6,f3109]) ).
fof(f3307,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,X1),mult(X2,mult(X3,X4))),X1) = mult(mult(X3,mult(X2,mult(mult(X0,X1),X4))),mult(X1,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f6,f3109]) ).
fof(f3313,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X1))),X4),mult(X2,mult(X3,X1))) = mult(mult(mult(X0,mult(X2,mult(X3,X1))),X4),mult(mult(X2,mult(X3,X1)),mult(mult(X0,X1),mult(X2,mult(X3,X1))))),
inference(paramodulation,[status(thm)],[f2916,f3109]) ).
fof(f3330,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X1),X4),X1) = mult(mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X1),X4),mult(X1,mult(mult(X3,X2),mult(X1,mult(X0,X1))))),
inference(paramodulation,[status(thm)],[f2824,f3109]) ).
fof(f3348,plain,
! [X0,X1,X2,X3] : mult(mult(X0,mult(X1,mult(mult(X2,X3),X1))),mult(X3,mult(X2,X3))) = mult(X0,mult(mult(X3,mult(X2,X3)),mult(mult(mult(X2,X3),X1),X3))),
inference(paramodulation,[status(thm)],[f3109,f7]) ).
fof(f3357,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(mult(X1,X2),X3),mult(X2,mult(X1,X2)))) = mult(mult(X0,mult(X1,X2)),mult(mult(mult(X1,X2),X3),X2)),
inference(paramodulation,[status(thm)],[f3109,f2916]) ).
fof(f3414,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,mult(X1,mult(X2,X3))),X4),mult(X1,mult(X2,X3))) = mult(mult(mult(X0,mult(X1,mult(X2,X3))),X4),mult(mult(X1,mult(X2,X3)),mult(mult(X0,X3),mult(X1,mult(X2,X3))))),
inference(forward_demodulation,[status(thm)],[f2916,f3313]) ).
fof(f3415,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,mult(X1,mult(X2,X3))),X4),mult(X1,mult(X2,X3))) = mult(mult(mult(X0,mult(X1,mult(X2,X3))),X4),mult(X1,mult(mult(X0,X3),mult(X1,mult(X2,X3))))),
inference(forward_demodulation,[status(thm)],[f2916,f3414]) ).
fof(f3417,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,mult(X1,mult(X2,X3))),X4),mult(X1,mult(X2,X3))) = mult(mult(mult(X0,mult(X1,mult(X2,X3))),X4),mult(X1,mult(X0,mult(X1,mult(X2,X3))))),
inference(forward_demodulation,[status(thm)],[f2916,f3415]) ).
fof(f3440,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X4),X2) = mult(mult(mult(mult(mult(X3,X2),mult(X1,mult(X0,X1))),X2),X4),mult(X2,mult(mult(X0,X1),mult(X2,mult(X3,X2))))),
inference(forward_demodulation,[status(thm)],[f2824,f3330]) ).
fof(f3441,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X4),X2) = mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X4),mult(X2,mult(mult(X0,X1),mult(X2,mult(X3,X2))))),
inference(forward_demodulation,[status(thm)],[f2824,f3440]) ).
fof(f3442,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X4),X2) = mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X4),mult(X2,mult(X3,X2))),
inference(forward_demodulation,[status(thm)],[f3417,f3441]) ).
fof(f3481,plain,
! [X0,X1,X2,X3] : mult(mult(mult(X0,X1),mult(X2,mult(X3,X2))),X1) = mult(X3,mult(mult(X1,mult(X0,X1)),mult(mult(mult(X0,X1),X2),X1))),
inference(forward_demodulation,[status(thm)],[f3307,f3348]) ).
fof(f3483,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,mult(X3,X2))) = mult(X0,mult(mult(X2,mult(X3,X2)),mult(mult(mult(X3,X2),X1),X2))),
inference(forward_demodulation,[status(thm)],[f2824,f3481]) ).
fof(f3486,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,mult(X3,X2))) = mult(X0,mult(X2,mult(mult(mult(X3,X2),X1),X2))),
inference(backward_demodulation,[status(thm)],[f3487,f3483]) ).
fof(f3487,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(mult(X1,X2),X3),X2)) = mult(mult(X0,mult(X1,X2)),mult(mult(mult(X1,X2),X3),X2)),
inference(forward_demodulation,[status(thm)],[f3109,f3357]) ).
fof(f3515,plain,
! [X0,X1,X2] : mult(mult(mult(X0,X1),X2),X1) = mult(mult(X0,X2),mult(X1,mult(X0,X1))),
inference(backward_demodulation,[status(thm)],[f3486,f3295]) ).
fof(f3530,plain,
! [X0,X1,X2] : mult(mult(mult(X0,X1),X2),X1) = mult(X0,mult(X1,mult(mult(X0,X2),X1))),
inference(paramodulation,[status(thm)],[f6,f3515]) ).
fof(f3547,plain,
! [X0,X1,X2,X3] : mult(mult(mult(X0,mult(X1,X2)),X3),mult(X1,X2)) = mult(mult(X0,X3),mult(X1,mult(X0,mult(X1,X2)))),
inference(paramodulation,[status(thm)],[f2916,f3515]) ).
fof(f3557,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X0,X2))),X3),mult(X2,mult(X0,X2))) = mult(mult(mult(X0,X1),X3),mult(mult(X2,mult(X0,X2)),mult(mult(mult(X0,X2),X1),X2))),
inference(paramodulation,[status(thm)],[f3515,f3515]) ).
fof(f3558,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X3,X1))),X4),mult(X2,mult(X3,X1))) = mult(mult(mult(X0,X1),X4),mult(mult(X2,mult(X3,X1)),mult(X0,mult(X2,mult(X3,X1))))),
inference(paramodulation,[status(thm)],[f2916,f3515]) ).
fof(f3577,plain,
! [X0,X1,X2,X3] : mult(X0,mult(X1,mult(mult(X0,X2),mult(mult(X1,X3),X3)))) = mult(mult(mult(X0,mult(X1,X3)),X2),mult(X1,X3)),
inference(paramodulation,[status(thm)],[f3515,f374]) ).
fof(f3586,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),mult(X3,mult(X1,X3)))) = mult(mult(X0,mult(X1,X3)),mult(mult(mult(X1,X3),X2),X3)),
inference(paramodulation,[status(thm)],[f3515,f2916]) ).
fof(f3587,plain,
! [X0,X1,X2,X3] : mult(mult(X0,mult(X1,X2)),mult(mult(mult(X1,X2),X3),X2)) = mult(X2,mult(mult(X1,X3),mult(X0,mult(X1,X2)))),
inference(paramodulation,[status(thm)],[f3515,f2741]) ).
fof(f3657,plain,
! [X0,X1,X2] : mult(mult(mult(X0,X1),X2),X1) = mult(mult(X0,X2),X1),
inference(forward_demodulation,[status(thm)],[f2152,f3530]) ).
fof(f3690,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,X3)) = mult(mult(X0,X1),mult(X2,mult(X0,mult(X2,X3)))),
inference(forward_demodulation,[status(thm)],[f3657,f3547]) ).
fof(f3711,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),mult(X2,mult(X0,X2))),X3),X2) = mult(mult(mult(X0,X1),X3),mult(mult(X2,mult(X0,X2)),mult(mult(mult(X0,X2),X1),X2))),
inference(forward_demodulation,[status(thm)],[f3442,f3557]) ).
fof(f3712,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(mult(X0,X1),X2),X1),X3),X1) = mult(mult(mult(X0,X2),X3),mult(mult(X1,mult(X0,X1)),mult(mult(mult(X0,X1),X2),X1))),
inference(forward_demodulation,[status(thm)],[f3515,f3711]) ).
fof(f3713,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),X2),X3),X1) = mult(mult(mult(X0,X2),X3),mult(mult(X1,mult(X0,X1)),mult(mult(mult(X0,X1),X2),X1))),
inference(forward_demodulation,[status(thm)],[f3657,f3712]) ).
fof(f3714,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),X2),X3),X1) = mult(mult(mult(X0,X2),X3),mult(X1,mult(mult(mult(X0,X1),X2),X1))),
inference(forward_demodulation,[status(thm)],[f3487,f3713]) ).
fof(f3715,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),X2),X3),X1) = mult(mult(mult(mult(X0,X2),X3),X2),mult(X1,mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f3486,f3714]) ).
fof(f3717,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),X2),X3),X1) = mult(mult(mult(X0,X3),X2),mult(X1,mult(X0,X1))),
inference(forward_demodulation,[status(thm)],[f3657,f3715]) ).
fof(f3718,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,X1),X2),mult(X3,mult(X4,X1))) = mult(mult(mult(X0,X1),X2),mult(mult(X3,mult(X4,X1)),mult(X0,mult(X3,mult(X4,X1))))),
inference(forward_demodulation,[status(thm)],[f3657,f3558]) ).
fof(f3719,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,X1),X2),mult(X3,mult(X4,X1))) = mult(mult(mult(mult(X0,mult(X3,mult(X4,X1))),X2),X1),mult(X3,mult(X4,X1))),
inference(forward_demodulation,[status(thm)],[f3717,f3718]) ).
fof(f3720,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,X1),X2),mult(X3,mult(X4,X1))) = mult(mult(mult(X0,mult(X3,mult(X4,X1))),X2),mult(X3,mult(X4,X1))),
inference(forward_demodulation,[status(thm)],[f2916,f3719]) ).
fof(f3723,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(X0,X1),X2),mult(X3,mult(X4,X1))) = mult(mult(X0,X2),mult(X3,mult(X4,X1))),
inference(forward_demodulation,[status(thm)],[f3657,f3720]) ).
fof(f3772,plain,
! [X0,X1,X2,X3] : mult(X0,mult(X1,mult(mult(X0,X2),mult(X1,X3)))) = mult(mult(mult(X0,mult(X1,X3)),X2),mult(X1,X3)),
inference(forward_demodulation,[status(thm)],[f2278,f3577]) ).
fof(f3773,plain,
! [X0,X1,X2,X3] : mult(X0,mult(X1,mult(mult(X0,X2),mult(X1,X3)))) = mult(mult(X0,X2),mult(X1,X3)),
inference(forward_demodulation,[status(thm)],[f3657,f3772]) ).
fof(f3787,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(mult(X1,X2),X3),X2)) = mult(mult(X0,mult(X1,X2)),mult(mult(mult(X1,X2),X3),X2)),
inference(forward_demodulation,[status(thm)],[f3515,f3586]) ).
fof(f3788,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(mult(X0,mult(X1,X3)),mult(mult(mult(X1,X3),X2),X3)),
inference(forward_demodulation,[status(thm)],[f3657,f3787]) ).
fof(f3789,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(mult(X0,mult(X1,X3)),mult(mult(X1,X2),X3)),
inference(forward_demodulation,[status(thm)],[f3657,f3788]) ).
fof(f3790,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(mult(X1,X2),X3),X2)) = mult(X2,mult(mult(X1,X3),mult(X0,mult(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f3487,f3587]) ).
fof(f3791,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(X3,mult(mult(X1,X2),mult(X0,mult(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f3657,f3790]) ).
fof(f4029,plain,
! [X0,X1,X2,X3] : mult(mult(mult(X0,mult(X1,X2)),X3),mult(X1,mult(X0,mult(X1,X2)))) = mult(mult(X2,X3),mult(X1,mult(X0,mult(X1,X2)))),
inference(paramodulation,[status(thm)],[f376,f3657]) ).
fof(f4055,plain,
! [X0,X1,X2,X3,X4] : mult(mult(X0,X1),mult(X2,mult(mult(X3,X4),X1))) = mult(mult(mult(X3,X1),X4),mult(X2,mult(X0,X1))),
inference(paramodulation,[status(thm)],[f3657,f2741]) ).
fof(f4096,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,mult(X0,mult(X2,X3)))) = mult(mult(X3,X1),mult(X2,mult(X0,mult(X2,X3)))),
inference(forward_demodulation,[status(thm)],[f3723,f4029]) ).
fof(f4098,plain,
! [X0,X1,X2,X3] : mult(mult(X0,X1),mult(X2,X3)) = mult(mult(X3,X1),mult(X2,mult(X0,mult(X2,X3)))),
inference(forward_demodulation,[status(thm)],[f3690,f4096]) ).
fof(f4120,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(mult(X2,X3),X4))) = mult(mult(mult(X2,X4),X3),mult(X1,mult(X0,X4))),
inference(forward_demodulation,[status(thm)],[f2916,f4055]) ).
fof(f4173,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(X1,mult(mult(X0,X2),mult(mult(X1,X3),mult(X4,X5))))) = mult(mult(X0,X2),mult(X1,mult(X4,mult(mult(X1,X3),mult(X4,X5))))),
inference(paramodulation,[status(thm)],[f3773,f3773]) ).
fof(f4250,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(X1,mult(mult(X0,X2),mult(mult(X1,X3),mult(X4,X5))))) = mult(mult(X0,X2),mult(mult(X1,X3),mult(X4,X5))),
inference(forward_demodulation,[status(thm)],[f3773,f4173]) ).
fof(f4330,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),mult(X3,mult(X1,X0)))) = mult(mult(X3,mult(X1,X0)),mult(mult(X1,X2),mult(X3,mult(X1,X0)))),
inference(paramodulation,[status(thm)],[f376,f3791]) ).
fof(f4376,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),mult(X3,mult(X1,X0)))) = mult(mult(X3,mult(mult(X1,X2),X0)),mult(mult(X1,X2),mult(X3,mult(X1,X0)))),
inference(paramodulation,[status(thm)],[f3791,f2278]) ).
fof(f4422,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(mult(X0,mult(X1,X3)),mult(mult(X1,X2),mult(X0,mult(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f3791,f4330]) ).
fof(f4425,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(X0,mult(mult(X1,X2),mult(X0,mult(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f2916,f4422]) ).
fof(f4469,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(mult(X0,mult(mult(X1,X2),X3)),mult(mult(X1,X2),mult(X0,mult(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f3791,f4376]) ).
fof(f4471,plain,
! [X0,X1,X2,X3] : mult(X0,mult(mult(X1,X2),X3)) = mult(X0,mult(X1,mult(X0,mult(mult(X1,X2),X3)))),
inference(forward_demodulation,[status(thm)],[f3049,f4469]) ).
fof(f4563,plain,
! [X0,X1,X2,X3,X4] : mult(mult(X0,X1),mult(X2,mult(mult(X3,X4),X1))) = mult(mult(X3,X4),mult(mult(X2,mult(X3,X1)),mult(X0,X1))),
inference(paramodulation,[status(thm)],[f3789,f2741]) ).
fof(f4668,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(mult(X2,X3),X4))) = mult(mult(X2,X3),mult(mult(X1,mult(X2,X4)),mult(X0,X4))),
inference(forward_demodulation,[status(thm)],[f2916,f4563]) ).
fof(f4754,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(mult(mult(X1,X2),X3),mult(X4,mult(X5,X2)))) = mult(X0,mult(mult(mult(X1,X2),X3),mult(X0,mult(X5,mult(X4,mult(X1,X2)))))),
inference(paramodulation,[status(thm)],[f2741,f4425]) ).
fof(f4762,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(mult(X1,X2),mult(X3,mult(X4,mult(X3,X1))))) = mult(X0,mult(mult(X1,X2),mult(X0,mult(X4,mult(X3,X1))))),
inference(paramodulation,[status(thm)],[f376,f4425]) ).
fof(f4872,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(X1,mult(X2,mult(mult(X3,X4),X5)))) = mult(X0,mult(mult(mult(X3,X5),X4),mult(X0,mult(X1,mult(X2,mult(X3,X5)))))),
inference(forward_demodulation,[status(thm)],[f4120,f4754]) ).
fof(f4878,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(X1,mult(X2,mult(mult(X3,X4),X5)))) = mult(X0,mult(mult(X1,X4),mult(X2,mult(X3,X5)))),
inference(backward_demodulation,[status(thm)],[f4880,f4872]) ).
fof(f4880,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(mult(X1,X2),mult(X3,X4))) = mult(X0,mult(mult(X4,X2),mult(X0,mult(X1,mult(X3,X4))))),
inference(forward_demodulation,[status(thm)],[f4098,f4762]) ).
fof(f4967,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(X1,mult(X0,mult(mult(X1,X2),mult(mult(X3,X4),X5))))) = mult(mult(X0,X4),mult(mult(X1,X2),mult(X3,X5))),
inference(backward_demodulation,[status(thm)],[f4878,f4250]) ).
fof(f5067,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(mult(X2,X3),X4))) = mult(X2,mult(mult(X1,mult(X2,X4)),mult(mult(X0,X3),X4))),
inference(backward_demodulation,[status(thm)],[f5069,f4668]) ).
fof(f5069,plain,
! [X0,X1,X2,X3,X4,X5] : mult(X0,mult(mult(X1,X2),mult(mult(X3,X4),X5))) = mult(mult(X0,X4),mult(mult(X1,X2),mult(X3,X5))),
inference(forward_demodulation,[status(thm)],[f4471,f4967]) ).
fof(f5091,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(mult(X2,X3),X4))) = mult(X2,mult(X1,mult(mult(X0,X3),X4))),
inference(forward_demodulation,[status(thm)],[f2904,f5067]) ).
fof(f5092,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f406,f5091]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG236-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n011.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Mon Sep 21 13:09:25 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.48 % Drodi V4.1.1
% 11.79/2.09 % Refutation found
% 11.79/2.09 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.79/2.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 25.41/14.42 % Elapsed time: 13.939782 seconds
% 25.41/14.42 % CPU time: 80.485812 seconds
% 25.41/14.42 % Total memory used: 46.512 GB
% 25.41/14.42 % Net memory used: 46.509 GB
%------------------------------------------------------------------------------