%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP705-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 : n005.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:11 PM UTC 2026
% Result : Unsatisfiable 96.33s 12.55s
% Output : CNFRefutation 63.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 10
% Syntax : Number of formulae : 65 ( 65 unt; 4 def)
% Number of atoms : 65 ( 64 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 : 18 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 117 ( 117 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : mult(A,ld(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] : mult(A,unit) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : mult(unit,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B,C] : mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
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,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
mult(op_a,mult(op_b,a)) != mult(mult(op_a,op_b),a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,plain,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f15,plain,
! [X0] : mult(X0,unit) = X0,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f16,plain,
! [X0] : mult(unit,X0) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f17,plain,
! [X0,X1,X2] : mult(X0,mult(X1,mult(X1,X2))) = mult(mult(mult(X0,X1),X1),X2),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f19,plain,
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,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
mult(op_a,mult(op_b,a)) != mult(mult(op_a,op_b),a),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f21,definition,
sF1_fnc = mult(op_b,a),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f22,definition,
sF0_fnc = mult(op_a,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f23,definition,
sF3_fnc = mult(op_a,op_b),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f24,definition,
sF2_fnc = mult(sF3_fnc,a),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f25,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f20,f24,f23,f22,f21]) ).
fof(f26,plain,
! [X0,X1,X2] : mult(mult(X0,X1),mult(X1,mult(X1,X2))) = mult(mult(X0,mult(X1,mult(X1,X1))),X2),
inference(paramodulation,[status(thm)],[f17,f17]) ).
fof(f27,plain,
! [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),
inference(paramodulation,[status(thm)],[f17,f17]) ).
fof(f29,plain,
! [X0] : mult(op_a,mult(op_b,mult(op_b,X0))) = mult(mult(sF3_fnc,op_b),X0),
inference(paramodulation,[status(thm)],[f23,f17]) ).
fof(f32,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f17,f27]) ).
fof(f41,plain,
! [X0,X1,X2,X3] : mult(mult(mult(mult(X0,X1),X1),X2),mult(X2,mult(X2,X3))) = mult(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,X2))))),X3),
inference(paramodulation,[status(thm)],[f17,f26]) ).
fof(f57,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f17,f41]) ).
fof(f107,plain,
! [X0,X1,X2,X3,X4] : mult(mult(mult(mult(X0,mult(X1,mult(X1,X2))),X2),X3),mult(X3,mult(X3,X4))) = mult(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,X3))))))),X4),
inference(paramodulation,[status(thm)],[f32,f26]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4] : mult(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,X3))))),mult(X3,mult(X3,X4))) = mult(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,X3))))))),X4),
inference(forward_demodulation,[status(thm)],[f32,f107]) ).
fof(f298,plain,
! [X0,X1] : mult(X0,mult(X1,mult(X1,unit))) = mult(mult(X0,X1),X1),
inference(paramodulation,[status(thm)],[f17,f15]) ).
fof(f325,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = mult(mult(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f15,f298]) ).
fof(f369,plain,
! [X0,X1] : mult(unit,mult(X0,mult(X0,X1))) = mult(mult(X0,X0),X1),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f389,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = mult(mult(X0,X0),X1),
inference(forward_demodulation,[status(thm)],[f16,f369]) ).
fof(f395,plain,
! [X0,X1,X2] : mult(X0,mult(X1,mult(X1,ld(mult(mult(X0,X1),X1),X2)))) = X2,
inference(paramodulation,[status(thm)],[f17,f11]) ).
fof(f413,plain,
! [X0] : mult(op_a,mult(op_b,X0)) = mult(mult(sF3_fnc,op_b),ld(op_b,X0)),
inference(paramodulation,[status(thm)],[f11,f29]) ).
fof(f513,plain,
! [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),
inference(paramodulation,[status(thm)],[f19,f32]) ).
fof(f514,plain,
! [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),
inference(paramodulation,[status(thm)],[f19,f32]) ).
fof(f544,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f16,f513]) ).
fof(f545,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f15,f514]) ).
fof(f548,plain,
! [X0,X1,X2] : mult(X0,mult(X1,mult(X1,X2))) = mult(mult(X0,mult(X1,X1)),X2),
inference(backward_demodulation,[status(thm)],[f325,f17]) ).
fof(f1213,plain,
! [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),
inference(paramodulation,[status(thm)],[f548,f548]) ).
fof(f1285,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f548,f1213]) ).
fof(f1286,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f548,f1285]) ).
fof(f1902,plain,
! [X0,X1,X2] : mult(X0,mult(X1,mult(X1,ld(mult(X0,mult(X1,X1)),X2)))) = X2,
inference(forward_demodulation,[status(thm)],[f325,f395]) ).
fof(f1907,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,ld(mult(mult(mult(X0,mult(X1,mult(X1,X2))),X2),mult(X3,X3)),X4)))))))) = X4,
inference(paramodulation,[status(thm)],[f32,f1902]) ).
fof(f2019,plain,
! [X0,X1,X2,X3,X4] : mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,mult(X3,mult(X3,ld(mult(X0,mult(X1,mult(X1,mult(X2,mult(X2,mult(X3,X3)))))),X4)))))))) = X4,
inference(forward_demodulation,[status(thm)],[f32,f1907]) ).
fof(f58410,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f57,f544]) ).
fof(f58411,plain,
! [X0] : mult(op_b,mult(op_b,mult(op_b,mult(mult(op_b,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),
inference(forward_demodulation,[status(thm)],[f26,f58410]) ).
fof(f58412,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f389,f58411]) ).
fof(f58413,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f57,f58412]) ).
fof(f58414,plain,
! [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,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),
inference(forward_demodulation,[status(thm)],[f26,f58413]) ).
fof(f58415,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f389,f58414]) ).
fof(f58416,plain,
! [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))),
inference(forward_demodulation,[status(thm)],[f57,f58415]) ).
fof(f58417,plain,
! [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,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,X0))))),
inference(forward_demodulation,[status(thm)],[f26,f58416]) ).
fof(f58418,plain,
! [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)))))),
inference(forward_demodulation,[status(thm)],[f389,f58417]) ).
fof(f58675,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f1286,f545]) ).
fof(f58676,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f1286,f58675]) ).
fof(f58677,plain,
! [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),
inference(forward_demodulation,[status(thm)],[f58418,f58676]) ).
fof(f58678,plain,
! [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,op_b))))),mult(op_b,mult(op_b,X1))),
inference(forward_demodulation,[status(thm)],[f141,f58677]) ).
fof(f58679,plain,
! [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,op_b))),mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))),
inference(forward_demodulation,[status(thm)],[f57,f58678]) ).
fof(f58681,plain,
! [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,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,X1))))))),
inference(forward_demodulation,[status(thm)],[f26,f58679]) ).
fof(f111743,plain,
! [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,ld(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))),X1)))))))))) = mult(mult(X0,op_b),X1),
inference(paramodulation,[status(thm)],[f2019,f58681]) ).
fof(f113245,plain,
! [X0,X1] : mult(X0,mult(op_b,X1)) = mult(mult(X0,op_b),X1),
inference(forward_demodulation,[status(thm)],[f2019,f111743]) ).
fof(f113301,plain,
! [X0] : mult(op_a,mult(op_b,X0)) = mult(sF3_fnc,mult(op_b,ld(op_b,X0))),
inference(backward_demodulation,[status(thm)],[f113245,f413]) ).
fof(f113682,plain,
! [X0] : mult(op_a,mult(op_b,X0)) = mult(sF3_fnc,X0),
inference(forward_demodulation,[status(thm)],[f11,f113301]) ).
fof(f114648,plain,
mult(op_a,sF1_fnc) = mult(sF3_fnc,a),
inference(paramodulation,[status(thm)],[f21,f113682]) ).
fof(f114809,plain,
sF0_fnc = mult(sF3_fnc,a),
inference(forward_demodulation,[status(thm)],[f22,f114648]) ).
fof(f114810,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f24,f114809]) ).
fof(f114811,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f114810,f25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP705-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:34:18 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 96.33/12.55 % Refutation found
% 96.33/12.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 96.33/12.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 77.54/13.80 % Elapsed time: 13.228361 seconds
% 77.54/13.80 % CPU time: 73.086751 seconds
% 77.54/13.80 % Total memory used: 858.008 MB
% 77.54/13.80 % Net memory used: 841.587 MB
%------------------------------------------------------------------------------