%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP727-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:35:14 PM UTC 2026
% Result : Unsatisfiable 9.57s 6.69s
% Output : CNFRefutation 10.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 14
% Syntax : Number of formulae : 93 ( 93 unt; 2 def)
% Number of atoms : 93 ( 92 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-3 aty)
% Number of variables : 162 ( 162 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [A] : mult(A,unit) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] : mult(A,i(A)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : mult(i(A),A) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B] : i(mult(A,B)) = mult(i(A),i(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] : mult(i(A),mult(A,B)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] : rd(mult(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] : mult(rd(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B,C] : mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B,C] : mult(mult(A,B),C) = mult(mult(A,mult(B,C)),asoc(A,B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] : op_t(A,B) = mult(i(B),mult(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B,C,D,E] : asoc(asoc(A,B,C),D,E) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
asoc(a,b,asoc(c,d,e)) != unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,plain,
! [X0] : mult(X0,unit) = X0,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f24,plain,
! [X0] : mult(X0,i(X0)) = unit,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f25,plain,
! [X0] : mult(i(X0),X0) = unit,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f26,plain,
! [X0,X1] : i(mult(X0,X1)) = mult(i(X0),i(X1)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f27,plain,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f28,plain,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f29,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f30,plain,
! [X0,X1,X2] : mult(mult(X0,mult(X1,X0)),X2) = mult(X0,mult(X1,mult(X0,X2))),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f31,plain,
! [X0,X1,X2] : mult(mult(X0,X1),X2) = mult(mult(X0,mult(X1,X2)),asoc(X0,X1,X2)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f34,plain,
! [X0,X1] : op_t(X0,X1) = mult(i(X1),mult(X0,X1)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f41,plain,
! [X0,X1,X2,X3,X4] : asoc(asoc(X0,X1,X2),X3,X4) = unit,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f42,plain,
asoc(a,b,asoc(c,d,e)) != unit,
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f43,definition,
sF1_fnc = asoc(c,d,e),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f44,definition,
sF0_fnc = asoc(a,b,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f45,plain,
sF0_fnc != unit,
inference(definition_folding,[],[f42,f44,f43]) ).
fof(f56,plain,
! [X0,X1] : asoc(sF1_fnc,X0,X1) = unit,
inference(paramodulation,[status(thm)],[f43,f41]) ).
fof(f67,plain,
! [X0,X1] : mult(mult(sF1_fnc,X0),X1) = mult(mult(sF1_fnc,mult(X0,X1)),unit),
inference(paramodulation,[status(thm)],[f56,f31]) ).
fof(f80,plain,
! [X0,X1] : mult(mult(sF1_fnc,X0),X1) = mult(sF1_fnc,mult(X0,X1)),
inference(forward_demodulation,[status(thm)],[f23,f67]) ).
fof(f288,plain,
! [X0] : rd(unit,X0) = i(X0),
inference(paramodulation,[status(thm)],[f25,f28]) ).
fof(f290,plain,
! [X0] : rd(unit,i(X0)) = X0,
inference(paramodulation,[status(thm)],[f24,f28]) ).
fof(f293,plain,
! [X0] : i(i(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f288,f290]) ).
fof(f326,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = X1,
inference(paramodulation,[status(thm)],[f293,f27]) ).
fof(f328,plain,
! [X0,X1] : mult(i(rd(X0,X1)),X0) = X1,
inference(paramodulation,[status(thm)],[f29,f27]) ).
fof(f331,plain,
! [X0,X1,X2] : mult(i(mult(X0,mult(X1,X2))),mult(mult(X0,X1),X2)) = asoc(X0,X1,X2),
inference(paramodulation,[status(thm)],[f31,f27]) ).
fof(f341,plain,
! [X0,X1] : rd(X0,mult(X1,X0)) = i(X1),
inference(paramodulation,[status(thm)],[f27,f28]) ).
fof(f477,plain,
! [X0,X1] : rd(X0,X1) = i(rd(X1,X0)),
inference(paramodulation,[status(thm)],[f328,f28]) ).
fof(f623,plain,
! [X0,X1,X2] : i(mult(rd(X0,X1),X2)) = mult(rd(X1,X0),i(X2)),
inference(paramodulation,[status(thm)],[f477,f26]) ).
fof(f627,plain,
! [X0,X1] : i(mult(X0,i(X1))) = mult(i(X0),X1),
inference(paramodulation,[status(thm)],[f293,f26]) ).
fof(f630,plain,
! [X0,X1] : mult(X0,i(mult(X0,X1))) = i(X1),
inference(paramodulation,[status(thm)],[f26,f326]) ).
fof(f633,plain,
! [X0,X1] : rd(i(X0),i(mult(X1,X0))) = i(i(X1)),
inference(paramodulation,[status(thm)],[f26,f341]) ).
fof(f639,plain,
! [X0,X1,X2] : mult(mult(X0,i(X1)),i(X2)) = mult(mult(X0,i(mult(X1,X2))),asoc(X0,i(X1),i(X2))),
inference(paramodulation,[status(thm)],[f26,f31]) ).
fof(f650,plain,
! [X0,X1] : rd(i(X0),i(mult(X1,X0))) = X1,
inference(forward_demodulation,[status(thm)],[f293,f633]) ).
fof(f671,plain,
! [X0,X1,X2] : mult(mult(X0,X1),X2) = mult(X0,mult(rd(X1,X0),mult(X0,X2))),
inference(paramodulation,[status(thm)],[f29,f30]) ).
fof(f814,plain,
! [X0] : unit = mult(sF1_fnc,mult(X0,i(mult(sF1_fnc,X0)))),
inference(paramodulation,[status(thm)],[f24,f80]) ).
fof(f963,plain,
! [X0] : rd(unit,mult(X0,i(mult(sF1_fnc,X0)))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f814,f28]) ).
fof(f1004,plain,
! [X0] : i(mult(X0,i(mult(sF1_fnc,X0)))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f288,f963]) ).
fof(f1005,plain,
! [X0] : mult(i(X0),mult(sF1_fnc,X0)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f627,f1004]) ).
fof(f1006,plain,
! [X0] : op_t(sF1_fnc,X0) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f34,f1005]) ).
fof(f1435,plain,
! [X0,X1] : rd(i(X0),i(X1)) = rd(X1,X0),
inference(paramodulation,[status(thm)],[f29,f650]) ).
fof(f1515,plain,
! [X0,X1] : rd(i(X0),X1) = rd(i(X1),X0),
inference(paramodulation,[status(thm)],[f293,f1435]) ).
fof(f1629,plain,
! [X0,X1] : mult(rd(i(X0),X1),X0) = i(X1),
inference(paramodulation,[status(thm)],[f1515,f29]) ).
fof(f1742,plain,
! [X0,X1] : mult(X0,op_t(X1,X0)) = mult(X1,X0),
inference(paramodulation,[status(thm)],[f34,f326]) ).
fof(f1828,plain,
! [X0] : mult(X0,sF1_fnc) = mult(sF1_fnc,X0),
inference(paramodulation,[status(thm)],[f1006,f1742]) ).
fof(f1913,plain,
! [X0] : X0 = mult(sF1_fnc,rd(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f29,f1828]) ).
fof(f1939,plain,
! [X0] : rd(sF1_fnc,mult(sF1_fnc,X0)) = i(X0),
inference(paramodulation,[status(thm)],[f1828,f341]) ).
fof(f1946,plain,
! [X0,X1] : mult(mult(X0,sF1_fnc),X1) = mult(sF1_fnc,mult(X0,X1)),
inference(paramodulation,[status(thm)],[f1828,f80]) ).
fof(f2011,plain,
! [X0] : mult(sF1_fnc,i(X0)) = i(rd(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f1913,f630]) ).
fof(f2017,plain,
! [X0] : rd(X0,rd(X0,sF1_fnc)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f1913,f28]) ).
fof(f2025,plain,
! [X0] : mult(sF1_fnc,i(X0)) = rd(sF1_fnc,X0),
inference(forward_demodulation,[status(thm)],[f477,f2011]) ).
fof(f2348,plain,
! [X0] : mult(sF1_fnc,X0) = i(rd(i(X0),sF1_fnc)),
inference(paramodulation,[status(thm)],[f2017,f1629]) ).
fof(f2360,plain,
! [X0] : mult(sF1_fnc,X0) = rd(sF1_fnc,i(X0)),
inference(forward_demodulation,[status(thm)],[f477,f2348]) ).
fof(f2608,plain,
! [X0,X1] : mult(rd(sF1_fnc,X0),X1) = mult(sF1_fnc,mult(i(X0),X1)),
inference(paramodulation,[status(thm)],[f2025,f80]) ).
fof(f6183,plain,
! [X0,X1] : mult(i(mult(X0,mult(X1,sF1_fnc))),mult(mult(X0,sF1_fnc),X1)) = asoc(X0,sF1_fnc,X1),
inference(paramodulation,[status(thm)],[f1828,f331]) ).
fof(f6208,plain,
! [X0,X1] : mult(i(mult(X0,mult(sF1_fnc,X1))),mult(mult(X0,X1),sF1_fnc)) = asoc(X0,X1,sF1_fnc),
inference(paramodulation,[status(thm)],[f1828,f331]) ).
fof(f6228,plain,
! [X0,X1] : mult(i(mult(X0,mult(X1,sF1_fnc))),mult(sF1_fnc,mult(X0,X1))) = asoc(X0,X1,sF1_fnc),
inference(paramodulation,[status(thm)],[f1828,f331]) ).
fof(f6337,plain,
! [X0,X1] : mult(i(mult(X0,mult(X1,sF1_fnc))),mult(sF1_fnc,mult(X0,X1))) = asoc(X0,sF1_fnc,X1),
inference(forward_demodulation,[status(thm)],[f1946,f6183]) ).
fof(f6352,plain,
! [X0,X1] : mult(i(mult(X0,mult(sF1_fnc,X1))),mult(sF1_fnc,mult(X0,X1))) = asoc(X0,X1,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f1828,f6208]) ).
fof(f6375,plain,
sF0_fnc = asoc(a,sF1_fnc,b),
inference(backward_demodulation,[status(thm)],[f6377,f44]) ).
fof(f6377,plain,
! [X0,X1] : asoc(X0,sF1_fnc,X1) = asoc(X0,X1,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f6337,f6228]) ).
fof(f7560,plain,
! [X0,X1] : mult(mult(sF1_fnc,i(X0)),i(X1)) = mult(sF1_fnc,mult(i(mult(X0,X1)),asoc(sF1_fnc,i(X0),i(X1)))),
inference(paramodulation,[status(thm)],[f80,f639]) ).
fof(f7670,plain,
! [X0,X1] : mult(sF1_fnc,mult(i(X0),i(X1))) = mult(sF1_fnc,mult(i(mult(X0,X1)),asoc(sF1_fnc,i(X0),i(X1)))),
inference(forward_demodulation,[status(thm)],[f80,f7560]) ).
fof(f7671,plain,
! [X0,X1] : mult(rd(sF1_fnc,X0),i(X1)) = mult(sF1_fnc,mult(i(mult(X0,X1)),asoc(sF1_fnc,i(X0),i(X1)))),
inference(forward_demodulation,[status(thm)],[f2608,f7670]) ).
fof(f7672,plain,
! [X0,X1] : i(mult(rd(X0,sF1_fnc),X1)) = mult(sF1_fnc,mult(i(mult(X0,X1)),asoc(sF1_fnc,i(X0),i(X1)))),
inference(forward_demodulation,[status(thm)],[f623,f7671]) ).
fof(f7673,plain,
! [X0,X1] : i(mult(rd(X0,sF1_fnc),X1)) = mult(rd(sF1_fnc,mult(X0,X1)),asoc(sF1_fnc,i(X0),i(X1))),
inference(forward_demodulation,[status(thm)],[f2608,f7672]) ).
fof(f7674,plain,
! [X0,X1] : i(mult(rd(X0,sF1_fnc),X1)) = mult(rd(sF1_fnc,mult(X0,X1)),unit),
inference(forward_demodulation,[status(thm)],[f56,f7673]) ).
fof(f7676,plain,
! [X0,X1] : i(mult(rd(X0,sF1_fnc),X1)) = rd(sF1_fnc,mult(X0,X1)),
inference(forward_demodulation,[status(thm)],[f23,f7674]) ).
fof(f9748,plain,
! [X0,X1] : mult(mult(i(X0),sF1_fnc),X1) = mult(i(X0),mult(mult(sF1_fnc,X0),mult(i(X0),X1))),
inference(paramodulation,[status(thm)],[f2360,f671]) ).
fof(f9822,plain,
! [X0,X1] : rd(sF1_fnc,mult(mult(sF1_fnc,X0),X1)) = i(mult(rd(X0,sF1_fnc),mult(sF1_fnc,X1))),
inference(paramodulation,[status(thm)],[f671,f1939]) ).
fof(f9985,plain,
! [X0,X1] : mult(sF1_fnc,mult(i(X0),X1)) = mult(i(X0),mult(mult(sF1_fnc,X0),mult(i(X0),X1))),
inference(forward_demodulation,[status(thm)],[f1946,f9748]) ).
fof(f9986,plain,
! [X0,X1] : mult(rd(sF1_fnc,X0),X1) = mult(i(X0),mult(mult(sF1_fnc,X0),mult(i(X0),X1))),
inference(forward_demodulation,[status(thm)],[f2608,f9985]) ).
fof(f9987,plain,
! [X0,X1] : mult(rd(sF1_fnc,X0),X1) = mult(i(X0),mult(sF1_fnc,mult(X0,mult(i(X0),X1)))),
inference(forward_demodulation,[status(thm)],[f80,f9986]) ).
fof(f9990,plain,
! [X0,X1] : mult(rd(sF1_fnc,mult(X0,mult(sF1_fnc,X1))),mult(X0,X1)) = asoc(X0,X1,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f9994,f6352]) ).
fof(f9994,plain,
! [X0,X1] : mult(rd(sF1_fnc,X0),X1) = mult(i(X0),mult(sF1_fnc,X1)),
inference(forward_demodulation,[status(thm)],[f326,f9987]) ).
fof(f10159,plain,
! [X0,X1] : rd(sF1_fnc,mult(sF1_fnc,mult(X0,X1))) = i(mult(rd(X0,sF1_fnc),mult(sF1_fnc,X1))),
inference(forward_demodulation,[status(thm)],[f80,f9822]) ).
fof(f10160,plain,
! [X0,X1] : i(mult(X0,X1)) = i(mult(rd(X0,sF1_fnc),mult(sF1_fnc,X1))),
inference(forward_demodulation,[status(thm)],[f1939,f10159]) ).
fof(f10162,plain,
! [X0,X1] : i(mult(X0,X1)) = rd(sF1_fnc,mult(X0,mult(sF1_fnc,X1))),
inference(forward_demodulation,[status(thm)],[f7676,f10160]) ).
fof(f10340,plain,
! [X0,X1] : mult(i(mult(X0,X1)),mult(X0,X1)) = asoc(X0,X1,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f10162,f9990]) ).
fof(f10342,plain,
! [X0,X1] : asoc(X0,sF1_fnc,X1) = unit,
inference(backward_demodulation,[status(thm)],[f10352,f6377]) ).
fof(f10352,plain,
! [X0,X1] : unit = asoc(X0,X1,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f25,f10340]) ).
fof(f10471,plain,
sF0_fnc = unit,
inference(backward_demodulation,[status(thm)],[f10342,f6375]) ).
fof(f10585,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10471,f45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP727-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n017.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Sun Sep 20 20:31:47 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 9.57/6.69 % Refutation found
% 9.57/6.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.57/6.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.13/6.76 % Elapsed time: 1.376364 seconds
% 10.13/6.76 % CPU time: 10.811315 seconds
% 10.13/6.76 % Total memory used: 270.929 MB
% 10.13/6.76 % Net memory used: 265.578 MB
%------------------------------------------------------------------------------