%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:06:34 PM UTC 2026
% Result : Unsatisfiable 25.45s 3.67s
% Output : CNFRefutation 25.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 13
% Syntax : Number of formulae : 131 ( 131 unt; 2 def)
% Number of atoms : 131 ( 130 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 166 ( 166 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] : multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : add(X,inverse(X)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : add(X,multiply(Y,Z)) = multiply(add(Y,X),add(Z,X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : multiply(X,inverse(X)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y] : add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] : add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : multiply(add(X,inverse(X)),multiply(add(X,Y),add(inverse(X),Y))) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] : multiply(add(X,inverse(Y)),multiply(add(X,Y),add(inverse(Y),Y))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] : multiply(add(X,inverse(Y)),multiply(add(X,X),add(inverse(Y),X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
multiply(add(a,b),b) != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,plain,
! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X1,X0),multiply(X2,X0)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
! [X0] : add(X0,inverse(X0)) = n1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f14,plain,
! [X0,X1,X2] : add(X0,multiply(X1,X2)) = multiply(add(X1,X0),add(X2,X0)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f15,plain,
! [X0] : multiply(X0,inverse(X0)) = n0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
! [X0,X1] : add(multiply(X0,inverse(X0)),add(multiply(X0,X1),multiply(inverse(X0),X1))) = X1,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f17,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),add(multiply(X0,X1),multiply(inverse(X1),X1))) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f18,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),X0))) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f19,plain,
! [X0,X1] : multiply(add(X0,inverse(X0)),multiply(add(X0,X1),add(inverse(X0),X1))) = X1,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
! [X0,X1] : multiply(add(X0,inverse(X1)),multiply(add(X0,X1),add(inverse(X1),X1))) = X0,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f21,plain,
! [X0,X1] : multiply(add(X0,inverse(X1)),multiply(add(X0,X0),add(inverse(X1),X0))) = X0,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f22,plain,
multiply(add(a,b),b) != b,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f23,definition,
sF1_fnc = add(a,b),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f24,definition,
sF0_fnc = multiply(sF1_fnc,b),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f25,plain,
sF0_fnc != b,
inference(definition_folding,[],[f22,f24,f23]) ).
fof(f36,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),multiply(multiply(X2,X1),X3)) = multiply(multiply(X1,add(X2,X0)),add(X3,multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f12,f14]) ).
fof(f37,plain,
! [X0] : add(b,multiply(a,X0)) = multiply(sF1_fnc,add(X0,b)),
inference(paramodulation,[status(thm)],[f23,f14]) ).
fof(f41,plain,
! [X0,X1,X2,X3] : multiply(add(X0,X1),add(add(X2,X1),X3)) = add(add(X1,multiply(X2,X0)),multiply(X3,add(X0,X1))),
inference(paramodulation,[status(thm)],[f14,f12]) ).
fof(f72,plain,
! [X0,X1,X2,X3] : add(multiply(X0,X1),multiply(multiply(X2,X1),multiply(X3,X1))) = multiply(multiply(X1,add(X2,X0)),multiply(X1,add(X3,X0))),
inference(paramodulation,[status(thm)],[f12,f36]) ).
fof(f266,plain,
! [X0,X1] : multiply(inverse(X0),add(X1,X0)) = add(multiply(X1,inverse(X0)),n0),
inference(paramodulation,[status(thm)],[f15,f12]) ).
fof(f267,plain,
! [X0,X1] : multiply(inverse(X0),add(X0,X1)) = add(n0,multiply(X1,inverse(X0))),
inference(paramodulation,[status(thm)],[f15,f12]) ).
fof(f394,plain,
! [X0] : multiply(inverse(inverse(X0)),n1) = add(multiply(X0,inverse(inverse(X0))),n0),
inference(paramodulation,[status(thm)],[f13,f266]) ).
fof(f504,plain,
! [X0,X1] : add(n0,add(multiply(X0,X1),multiply(inverse(X0),X1))) = X1,
inference(forward_demodulation,[status(thm)],[f15,f16]) ).
fof(f505,plain,
! [X0,X1] : add(n0,multiply(X0,add(X1,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f12,f504]) ).
fof(f506,plain,
! [X0] : add(n0,multiply(X0,n1)) = X0,
inference(forward_demodulation,[status(thm)],[f13,f505]) ).
fof(f518,plain,
! [X0,X1] : add(multiply(X0,n1),multiply(X1,n0)) = multiply(add(X1,multiply(X0,n1)),X0),
inference(paramodulation,[status(thm)],[f506,f14]) ).
fof(f562,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),multiply(X1,add(X0,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f12,f17]) ).
fof(f564,plain,
! [X0] : add(multiply(X0,inverse(inverse(X0))),add(n0,multiply(inverse(inverse(X0)),inverse(X0)))) = X0,
inference(paramodulation,[status(thm)],[f267,f562]) ).
fof(f585,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),multiply(X0,add(X0,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f12,f18]) ).
fof(f609,plain,
! [X0,X1] : multiply(n1,multiply(add(X0,X1),add(inverse(X0),X1))) = X1,
inference(forward_demodulation,[status(thm)],[f13,f19]) ).
fof(f610,plain,
! [X0,X1] : multiply(n1,add(X0,multiply(X1,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f14,f609]) ).
fof(f611,plain,
! [X0] : multiply(n1,add(X0,n0)) = X0,
inference(forward_demodulation,[status(thm)],[f15,f610]) ).
fof(f625,plain,
! [X0,X1] : multiply(add(X0,n0),add(X1,n1)) = add(multiply(X1,add(X0,n0)),X0),
inference(paramodulation,[status(thm)],[f611,f12]) ).
fof(f626,plain,
! [X0,X1] : multiply(add(X0,n0),add(n1,X1)) = add(X0,multiply(X1,add(X0,n0))),
inference(paramodulation,[status(thm)],[f611,f12]) ).
fof(f890,plain,
! [X0] : add(multiply(X0,n1),multiply(n0,n0)) = multiply(X0,X0),
inference(paramodulation,[status(thm)],[f506,f518]) ).
fof(f965,plain,
! [X0,X1] : add(multiply(add(X0,X1),n1),multiply(n0,n0)) = add(X1,multiply(X0,X0)),
inference(paramodulation,[status(thm)],[f14,f890]) ).
fof(f1014,plain,
! [X0,X1] : multiply(add(X0,inverse(X1)),add(X1,multiply(X0,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f14,f20]) ).
fof(f1038,plain,
! [X0,X1,X2] : multiply(add(X0,multiply(X1,inverse(X0))),add(add(X1,inverse(X0)),X2)) = add(X1,multiply(X2,add(X0,multiply(X1,inverse(X0))))),
inference(paramodulation,[status(thm)],[f1014,f12]) ).
fof(f1043,plain,
! [X0,X1] : multiply(add(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f14,f21]) ).
fof(f1068,plain,
! [X0,X1,X2] : multiply(add(X0,multiply(X0,inverse(X1))),add(add(X0,inverse(X1)),X2)) = add(X0,multiply(X2,add(X0,multiply(X0,inverse(X1))))),
inference(paramodulation,[status(thm)],[f1043,f12]) ).
fof(f1078,plain,
! [X0] : multiply(add(X0,n0),add(n1,n1)) = add(X0,X0),
inference(paramodulation,[status(thm)],[f611,f625]) ).
fof(f1131,plain,
! [X0,X1] : multiply(add(multiply(X0,X1),n0),add(n1,n1)) = multiply(X1,add(X0,X0)),
inference(paramodulation,[status(thm)],[f12,f1078]) ).
fof(f1163,plain,
! [X0] : multiply(inverse(X0),multiply(add(X0,n0),add(n1,n1))) = add(n0,multiply(X0,inverse(X0))),
inference(paramodulation,[status(thm)],[f1078,f267]) ).
fof(f1180,plain,
! [X0] : multiply(inverse(X0),multiply(add(X0,n0),add(n1,n1))) = add(n0,n0),
inference(forward_demodulation,[status(thm)],[f15,f1163]) ).
fof(f1185,plain,
! [X0] : add(n0,multiply(X0,n1)) = add(X0,multiply(n0,add(X0,n0))),
inference(paramodulation,[status(thm)],[f14,f626]) ).
fof(f1236,plain,
! [X0] : X0 = add(X0,multiply(n0,add(X0,n0))),
inference(forward_demodulation,[status(thm)],[f506,f1185]) ).
fof(f1330,plain,
! [X0,X1] : add(multiply(add(X0,multiply(X1,X0)),n1),multiply(n0,n0)) = multiply(X0,add(X1,X0)),
inference(paramodulation,[status(thm)],[f12,f965]) ).
fof(f2236,plain,
! [X0,X1] : multiply(inverse(multiply(X0,X1)),multiply(X1,add(X0,X0))) = add(n0,n0),
inference(paramodulation,[status(thm)],[f1131,f1180]) ).
fof(f2300,plain,
multiply(inverse(multiply(n0,n1)),n0) = add(n0,n0),
inference(paramodulation,[status(thm)],[f611,f2236]) ).
fof(f2716,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),multiply(X1,add(X0,inverse(X1)))) = add(X0,multiply(multiply(X0,inverse(X1)),add(X1,multiply(X0,inverse(X1))))),
inference(paramodulation,[status(thm)],[f14,f1038]) ).
fof(f2774,plain,
! [X0,X1] : X0 = add(X0,multiply(multiply(X0,inverse(X1)),add(X1,multiply(X0,inverse(X1))))),
inference(forward_demodulation,[status(thm)],[f562,f2716]) ).
fof(f3235,plain,
! [X0,X1] : add(multiply(X0,inverse(X1)),multiply(X0,add(X0,inverse(X1)))) = add(X0,multiply(multiply(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1))))),
inference(paramodulation,[status(thm)],[f14,f1068]) ).
fof(f3295,plain,
! [X0,X1] : X0 = add(X0,multiply(multiply(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1))))),
inference(forward_demodulation,[status(thm)],[f585,f3235]) ).
fof(f7163,plain,
! [X0,X1] : add(multiply(n0,n1),multiply(multiply(X0,n1),multiply(X1,n1))) = multiply(X0,multiply(n1,add(X1,n0))),
inference(paramodulation,[status(thm)],[f611,f72]) ).
fof(f7445,plain,
! [X0,X1] : add(multiply(n0,n1),multiply(multiply(X0,n1),multiply(X1,n1))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f611,f7163]) ).
fof(f9100,plain,
! [X0] : add(multiply(multiply(X0,n0),n1),multiply(n0,n0)) = multiply(multiply(n0,n1),add(multiply(X0,n1),multiply(n0,n1))),
inference(paramodulation,[status(thm)],[f7445,f1330]) ).
fof(f9143,plain,
! [X0] : add(multiply(multiply(X0,n0),n1),multiply(n0,n0)) = multiply(multiply(n0,n1),multiply(n1,add(X0,n0))),
inference(forward_demodulation,[status(thm)],[f12,f9100]) ).
fof(f9144,plain,
! [X0] : add(multiply(multiply(X0,n0),n1),multiply(n0,n0)) = multiply(multiply(n0,n1),X0),
inference(forward_demodulation,[status(thm)],[f611,f9143]) ).
fof(f10690,plain,
add(multiply(add(n0,n0),n1),multiply(n0,n0)) = multiply(multiply(n0,n1),inverse(multiply(n0,n1))),
inference(paramodulation,[status(thm)],[f2300,f9144]) ).
fof(f10727,plain,
add(multiply(add(n0,n0),n1),multiply(n0,n0)) = n0,
inference(forward_demodulation,[status(thm)],[f15,f10690]) ).
fof(f10750,plain,
add(n0,multiply(n0,n0)) = n0,
inference(paramodulation,[status(thm)],[f965,f10727]) ).
fof(f10844,plain,
! [X0] : add(multiply(n0,n0),multiply(X0,n0)) = multiply(add(X0,multiply(n0,n0)),n0),
inference(paramodulation,[status(thm)],[f10750,f14]) ).
fof(f10866,plain,
! [X0] : multiply(n0,add(n0,X0)) = multiply(add(X0,multiply(n0,n0)),n0),
inference(forward_demodulation,[status(thm)],[f12,f10844]) ).
fof(f11613,plain,
! [X0] : multiply(n0,add(n0,multiply(X0,n1))) = multiply(multiply(X0,X0),n0),
inference(paramodulation,[status(thm)],[f890,f10866]) ).
fof(f11656,plain,
! [X0] : multiply(n0,X0) = multiply(multiply(X0,X0),n0),
inference(forward_demodulation,[status(thm)],[f506,f11613]) ).
fof(f11679,plain,
multiply(n0,add(n1,n0)) = multiply(add(n1,multiply(n0,add(n1,n0))),n0),
inference(paramodulation,[status(thm)],[f626,f11656]) ).
fof(f11721,plain,
multiply(n0,add(n1,n0)) = multiply(n1,n0),
inference(forward_demodulation,[status(thm)],[f1236,f11679]) ).
fof(f13333,plain,
n1 = add(n1,multiply(n1,n0)),
inference(paramodulation,[status(thm)],[f11721,f1236]) ).
fof(f13344,plain,
! [X0] : multiply(add(n1,n0),add(add(X0,n0),n0)) = add(add(n0,multiply(X0,n1)),multiply(n1,n0)),
inference(paramodulation,[status(thm)],[f11721,f41]) ).
fof(f13383,plain,
! [X0] : add(n0,multiply(n1,add(X0,n0))) = add(add(n0,multiply(X0,n1)),multiply(n1,n0)),
inference(forward_demodulation,[status(thm)],[f14,f13344]) ).
fof(f13384,plain,
! [X0] : add(n0,X0) = add(add(n0,multiply(X0,n1)),multiply(n1,n0)),
inference(forward_demodulation,[status(thm)],[f611,f13383]) ).
fof(f13385,plain,
! [X0] : add(n0,X0) = add(X0,multiply(n1,n0)),
inference(forward_demodulation,[status(thm)],[f506,f13384]) ).
fof(f13473,plain,
n1 = add(n0,n1),
inference(backward_demodulation,[status(thm)],[f13385,f13333]) ).
fof(f13497,plain,
add(multiply(add(n0,n0),n1),multiply(n0,n0)) = multiply(n0,add(n1,n0)),
inference(paramodulation,[status(thm)],[f13385,f1330]) ).
fof(f13543,plain,
n0 = multiply(n0,add(n1,n0)),
inference(forward_demodulation,[status(thm)],[f10727,f13497]) ).
fof(f13544,plain,
n0 = multiply(n1,n0),
inference(forward_demodulation,[status(thm)],[f11721,f13543]) ).
fof(f13603,plain,
! [X0] : add(n0,X0) = add(X0,n0),
inference(backward_demodulation,[status(thm)],[f13544,f13385]) ).
fof(f13668,plain,
n1 = add(n1,n0),
inference(paramodulation,[status(thm)],[f13473,f13603]) ).
fof(f13752,plain,
! [X0] : multiply(n1,add(n0,X0)) = X0,
inference(paramodulation,[status(thm)],[f13603,f611]) ).
fof(f13799,plain,
! [X0] : multiply(add(X0,n0),n1) = add(X0,multiply(n0,add(X0,n0))),
inference(paramodulation,[status(thm)],[f13668,f626]) ).
fof(f13815,plain,
multiply(n1,n1) = n1,
inference(paramodulation,[status(thm)],[f13668,f611]) ).
fof(f13848,plain,
! [X0] : multiply(add(X0,n0),n1) = X0,
inference(forward_demodulation,[status(thm)],[f1236,f13799]) ).
fof(f14276,plain,
multiply(n1,n1) = inverse(n0),
inference(paramodulation,[status(thm)],[f13,f13752]) ).
fof(f14339,plain,
n1 = inverse(n0),
inference(forward_demodulation,[status(thm)],[f13815,f14276]) ).
fof(f16444,plain,
! [X0] : X0 = add(X0,multiply(multiply(X0,inverse(n0)),add(n0,multiply(X0,n1)))),
inference(paramodulation,[status(thm)],[f14339,f2774]) ).
fof(f16473,plain,
! [X0] : multiply(add(X0,inverse(n0)),add(n0,multiply(X0,n1))) = X0,
inference(paramodulation,[status(thm)],[f14339,f1014]) ).
fof(f16543,plain,
! [X0] : X0 = add(X0,multiply(multiply(X0,n1),add(n0,multiply(X0,n1)))),
inference(forward_demodulation,[status(thm)],[f14339,f16444]) ).
fof(f16544,plain,
! [X0] : X0 = add(X0,multiply(multiply(X0,n1),X0)),
inference(forward_demodulation,[status(thm)],[f506,f16543]) ).
fof(f16621,plain,
! [X0] : multiply(add(X0,n1),add(n0,multiply(X0,n1))) = X0,
inference(forward_demodulation,[status(thm)],[f14339,f16473]) ).
fof(f16622,plain,
! [X0] : multiply(add(X0,n1),X0) = X0,
inference(forward_demodulation,[status(thm)],[f506,f16621]) ).
fof(f16717,plain,
! [X0] : add(n1,multiply(add(X0,n1),X0)) = add(X0,n1),
inference(paramodulation,[status(thm)],[f14,f16622]) ).
fof(f16812,plain,
! [X0] : add(n1,X0) = add(X0,n1),
inference(forward_demodulation,[status(thm)],[f16622,f16717]) ).
fof(f20343,plain,
! [X0] : multiply(add(n1,X0),X0) = X0,
inference(paramodulation,[status(thm)],[f16812,f16622]) ).
fof(f23163,plain,
! [X0] : multiply(add(X0,n0),n1) = add(X0,multiply(multiply(multiply(n1,n1),n1),add(X0,n0))),
inference(paramodulation,[status(thm)],[f16544,f626]) ).
fof(f23247,plain,
! [X0] : X0 = add(X0,multiply(multiply(multiply(n1,n1),n1),add(X0,n0))),
inference(forward_demodulation,[status(thm)],[f13848,f23163]) ).
fof(f23248,plain,
! [X0] : X0 = add(X0,multiply(multiply(n1,n1),add(X0,n0))),
inference(forward_demodulation,[status(thm)],[f13815,f23247]) ).
fof(f23249,plain,
! [X0] : X0 = add(X0,multiply(n1,add(X0,n0))),
inference(forward_demodulation,[status(thm)],[f13815,f23248]) ).
fof(f23250,plain,
! [X0] : X0 = add(X0,X0),
inference(forward_demodulation,[status(thm)],[f611,f23249]) ).
fof(f23325,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,add(X0,X0)),
inference(paramodulation,[status(thm)],[f12,f23250]) ).
fof(f23465,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f23250,f23325]) ).
fof(f23646,plain,
! [X0] : X0 = multiply(X0,add(n1,X0)),
inference(paramodulation,[status(thm)],[f20343,f23465]) ).
fof(f23738,plain,
! [X0] : add(multiply(X0,inverse(inverse(X0))),add(n0,multiply(inverse(X0),inverse(inverse(X0))))) = X0,
inference(paramodulation,[status(thm)],[f23465,f564]) ).
fof(f24211,plain,
! [X0] : add(multiply(X0,inverse(inverse(X0))),add(n0,n0)) = X0,
inference(forward_demodulation,[status(thm)],[f15,f23738]) ).
fof(f24212,plain,
! [X0] : add(multiply(X0,inverse(inverse(X0))),n0) = X0,
inference(forward_demodulation,[status(thm)],[f23250,f24211]) ).
fof(f24213,plain,
! [X0] : multiply(inverse(inverse(X0)),n1) = X0,
inference(forward_demodulation,[status(thm)],[f394,f24212]) ).
fof(f28997,plain,
! [X0] : multiply(n1,inverse(inverse(X0))) = X0,
inference(paramodulation,[status(thm)],[f23465,f24213]) ).
fof(f29270,plain,
! [X0] : n1 = add(n1,multiply(multiply(n1,inverse(inverse(X0))),add(n1,X0))),
inference(paramodulation,[status(thm)],[f28997,f3295]) ).
fof(f29338,plain,
! [X0] : n1 = add(n1,multiply(X0,add(n1,X0))),
inference(forward_demodulation,[status(thm)],[f28997,f29270]) ).
fof(f29339,plain,
! [X0] : n1 = add(n1,X0),
inference(forward_demodulation,[status(thm)],[f23646,f29338]) ).
fof(f29413,plain,
! [X0] : X0 = multiply(X0,n1),
inference(backward_demodulation,[status(thm)],[f29339,f23646]) ).
fof(f29416,plain,
! [X0,X1] : multiply(add(X0,n0),n1) = add(X0,multiply(X1,add(X0,n0))),
inference(backward_demodulation,[status(thm)],[f29339,f626]) ).
fof(f29572,plain,
! [X0,X1] : X0 = add(X0,multiply(X1,add(X0,n0))),
inference(forward_demodulation,[status(thm)],[f13848,f29416]) ).
fof(f29677,plain,
! [X0] : add(X0,n0) = X0,
inference(backward_demodulation,[status(thm)],[f29413,f13848]) ).
fof(f29687,plain,
! [X0] : add(n0,X0) = X0,
inference(backward_demodulation,[status(thm)],[f29413,f506]) ).
fof(f30048,plain,
add(b,multiply(a,n0)) = multiply(sF1_fnc,b),
inference(paramodulation,[status(thm)],[f29687,f37]) ).
fof(f30226,plain,
add(b,multiply(a,n0)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f24,f30048]) ).
fof(f30267,plain,
! [X0] : n0 = multiply(X0,add(n0,n0)),
inference(paramodulation,[status(thm)],[f29687,f29572]) ).
fof(f30364,plain,
! [X0] : n0 = multiply(X0,n0),
inference(forward_demodulation,[status(thm)],[f29687,f30267]) ).
fof(f33005,plain,
add(b,n0) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f30364,f30226]) ).
fof(f33074,plain,
b = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f29677,f33005]) ).
fof(f33075,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f33074,f25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 13:48:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 25.45/3.67 % Refutation found
% 25.45/3.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 25.45/3.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.66/3.80 % Elapsed time: 3.411543 seconds
% 21.66/3.80 % CPU time: 26.490202 seconds
% 21.66/3.80 % Total memory used: 636.441 MB
% 21.66/3.80 % Net memory used: 630.139 MB
%------------------------------------------------------------------------------