%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP186-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:33:02 PM UTC 2026
% Result : Unsatisfiable 209.28s 32.17s
% Output : CNFRefutation 38.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 23
% Syntax : Number of formulae : 172 ( 172 unt; 6 def)
% Number of atoms : 172 ( 171 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 144 ( 144 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : multiply(identity,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : multiply(inverse(X),X) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] : greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,Y] : least_upper_bound(X,Y) = least_upper_bound(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] : greatest_lower_bound(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(greatest_lower_bound(X,Y),Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z] : least_upper_bound(X,least_upper_bound(Y,Z)) = least_upper_bound(least_upper_bound(X,Y),Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] : least_upper_bound(X,greatest_lower_bound(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] : greatest_lower_bound(X,least_upper_bound(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X,Y,Z] : multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,Z] : multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Y,Z,X] : multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Y,Z,X] : multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
inverse(identity) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
! [X] : inverse(inverse(X)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
! [X,Y] : inverse(multiply(X,Y)) = multiply(inverse(Y),inverse(X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
least_upper_bound(multiply(a,b),identity) != multiply(a,inverse(greatest_lower_bound(a,inverse(b)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,plain,
! [X0] : multiply(identity,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f21,plain,
! [X0] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f23,plain,
! [X0,X1] : greatest_lower_bound(X0,X1) = greatest_lower_bound(X1,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
! [X0,X1] : least_upper_bound(X0,X1) = least_upper_bound(X1,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f25,plain,
! [X0,X1,X2] : greatest_lower_bound(X0,greatest_lower_bound(X1,X2)) = greatest_lower_bound(greatest_lower_bound(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f26,plain,
! [X0,X1,X2] : least_upper_bound(X0,least_upper_bound(X1,X2)) = least_upper_bound(least_upper_bound(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f29,plain,
! [X0,X1] : least_upper_bound(X0,greatest_lower_bound(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f30,plain,
! [X0,X1] : greatest_lower_bound(X0,least_upper_bound(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f31,plain,
! [X0,X1,X2] : multiply(X0,least_upper_bound(X1,X2)) = least_upper_bound(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f32,plain,
! [X0,X1,X2] : multiply(X0,greatest_lower_bound(X1,X2)) = greatest_lower_bound(multiply(X0,X1),multiply(X0,X2)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f33,plain,
! [X0,X1,X2] : multiply(least_upper_bound(X0,X1),X2) = least_upper_bound(multiply(X0,X2),multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f34,plain,
! [X0,X1,X2] : multiply(greatest_lower_bound(X0,X1),X2) = greatest_lower_bound(multiply(X0,X2),multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f35,plain,
inverse(identity) = identity,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f36,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f37,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(X0)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f38,plain,
least_upper_bound(multiply(a,b),identity) != multiply(a,inverse(greatest_lower_bound(a,inverse(b)))),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f39,definition,
sF1_fnc = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f40,definition,
sF0_fnc = least_upper_bound(sF1_fnc,identity),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f41,definition,
sF5_fnc = inverse(b),
introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition]) ).
fof(f42,definition,
sF4_fnc = greatest_lower_bound(a,sF5_fnc),
introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition]) ).
fof(f43,definition,
sF3_fnc = inverse(sF4_fnc),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f44,definition,
sF2_fnc = multiply(a,sF3_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f45,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f38,f44,f43,f42,f41,f40,f39]) ).
fof(f48,plain,
inverse(sF3_fnc) = sF4_fnc,
inference(paramodulation,[status(thm)],[f43,f36]) ).
fof(f49,plain,
inverse(sF5_fnc) = b,
inference(paramodulation,[status(thm)],[f41,f36]) ).
fof(f52,plain,
multiply(b,sF5_fnc) = identity,
inference(paramodulation,[status(thm)],[f49,f21]) ).
fof(f53,plain,
multiply(sF4_fnc,sF3_fnc) = identity,
inference(paramodulation,[status(thm)],[f48,f21]) ).
fof(f54,plain,
! [X0] : multiply(X0,inverse(X0)) = identity,
inference(paramodulation,[status(thm)],[f36,f21]) ).
fof(f57,plain,
multiply(sF5_fnc,b) = identity,
inference(paramodulation,[status(thm)],[f41,f21]) ).
fof(f62,plain,
sF0_fnc = least_upper_bound(identity,sF1_fnc),
inference(paramodulation,[status(thm)],[f40,f24]) ).
fof(f70,plain,
least_upper_bound(a,sF4_fnc) = a,
inference(paramodulation,[status(thm)],[f42,f29]) ).
fof(f71,plain,
! [X0,X1] : least_upper_bound(X0,greatest_lower_bound(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f23,f29]) ).
fof(f74,plain,
greatest_lower_bound(sF1_fnc,sF0_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f40,f30]) ).
fof(f76,plain,
! [X0,X1] : greatest_lower_bound(X0,least_upper_bound(X1,X0)) = X0,
inference(paramodulation,[status(thm)],[f24,f30]) ).
fof(f81,plain,
! [X0,X1] : multiply(identity,X0) = multiply(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f21,f22]) ).
fof(f83,plain,
! [X0] : multiply(sF2_fnc,X0) = multiply(a,multiply(sF3_fnc,X0)),
inference(paramodulation,[status(thm)],[f44,f22]) ).
fof(f84,plain,
! [X0] : multiply(sF1_fnc,X0) = multiply(a,multiply(b,X0)),
inference(paramodulation,[status(thm)],[f39,f22]) ).
fof(f87,plain,
! [X0,X1] : X0 = multiply(inverse(X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f20,f81]) ).
fof(f107,plain,
! [X0] : multiply(identity,X0) = multiply(b,multiply(sF5_fnc,X0)),
inference(paramodulation,[status(thm)],[f52,f22]) ).
fof(f108,plain,
! [X0] : X0 = multiply(b,multiply(sF5_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f20,f107]) ).
fof(f121,plain,
! [X0,X1] : multiply(identity,X0) = multiply(X1,multiply(inverse(X1),X0)),
inference(paramodulation,[status(thm)],[f54,f22]) ).
fof(f122,plain,
! [X0,X1] : X0 = multiply(X1,multiply(inverse(X1),X0)),
inference(forward_demodulation,[status(thm)],[f20,f121]) ).
fof(f125,plain,
! [X0] : multiply(identity,X0) = multiply(sF5_fnc,multiply(b,X0)),
inference(paramodulation,[status(thm)],[f57,f22]) ).
fof(f126,plain,
! [X0] : X0 = multiply(sF5_fnc,multiply(b,X0)),
inference(forward_demodulation,[status(thm)],[f20,f125]) ).
fof(f127,plain,
greatest_lower_bound(identity,sF0_fnc) = identity,
inference(paramodulation,[status(thm)],[f62,f30]) ).
fof(f131,plain,
least_upper_bound(sF5_fnc,sF4_fnc) = sF5_fnc,
inference(paramodulation,[status(thm)],[f42,f71]) ).
fof(f132,plain,
! [X0,X1] : least_upper_bound(least_upper_bound(X0,X1),X0) = least_upper_bound(X0,X1),
inference(paramodulation,[status(thm)],[f30,f71]) ).
fof(f138,plain,
greatest_lower_bound(sF0_fnc,sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f23,f74]) ).
fof(f158,plain,
! [X0,X1,X2] : greatest_lower_bound(X0,greatest_lower_bound(least_upper_bound(X1,X0),X2)) = greatest_lower_bound(X0,X2),
inference(paramodulation,[status(thm)],[f76,f25]) ).
fof(f162,plain,
least_upper_bound(sF0_fnc,identity) = sF0_fnc,
inference(paramodulation,[status(thm)],[f127,f71]) ).
fof(f173,plain,
! [X0] : least_upper_bound(sF1_fnc,least_upper_bound(identity,X0)) = least_upper_bound(sF0_fnc,X0),
inference(paramodulation,[status(thm)],[f40,f26]) ).
fof(f198,plain,
! [X0,X1] : multiply(inverse(X0),least_upper_bound(X0,X1)) = least_upper_bound(identity,multiply(inverse(X0),X1)),
inference(paramodulation,[status(thm)],[f21,f31]) ).
fof(f200,plain,
! [X0] : multiply(a,least_upper_bound(sF3_fnc,X0)) = least_upper_bound(sF2_fnc,multiply(a,X0)),
inference(paramodulation,[status(thm)],[f44,f31]) ).
fof(f231,plain,
! [X0,X1,X2] : multiply(X0,greatest_lower_bound(X1,X2)) = greatest_lower_bound(multiply(X0,X2),multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f23,f32]) ).
fof(f241,plain,
! [X0] : multiply(a,greatest_lower_bound(sF3_fnc,X0)) = greatest_lower_bound(sF2_fnc,multiply(a,X0)),
inference(paramodulation,[status(thm)],[f44,f32]) ).
fof(f249,plain,
! [X0,X1] : multiply(inverse(X0),greatest_lower_bound(X1,X0)) = greatest_lower_bound(multiply(inverse(X0),X1),identity),
inference(paramodulation,[status(thm)],[f21,f32]) ).
fof(f253,plain,
! [X0,X1] : multiply(X0,greatest_lower_bound(X1,inverse(X0))) = greatest_lower_bound(multiply(X0,X1),identity),
inference(paramodulation,[status(thm)],[f54,f32]) ).
fof(f260,plain,
! [X0,X1,X2] : multiply(X0,greatest_lower_bound(X1,X2)) = multiply(X0,greatest_lower_bound(X2,X1)),
inference(forward_demodulation,[status(thm)],[f32,f231]) ).
fof(f330,plain,
! [X0,X1] : multiply(least_upper_bound(identity,X0),X1) = least_upper_bound(X1,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f20,f33]) ).
fof(f332,plain,
! [X0] : multiply(least_upper_bound(a,X0),sF3_fnc) = least_upper_bound(sF2_fnc,multiply(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f44,f33]) ).
fof(f371,plain,
! [X0] : multiply(greatest_lower_bound(a,X0),sF3_fnc) = greatest_lower_bound(sF2_fnc,multiply(X0,sF3_fnc)),
inference(paramodulation,[status(thm)],[f44,f34]) ).
fof(f372,plain,
! [X0] : multiply(greatest_lower_bound(a,X0),b) = greatest_lower_bound(sF1_fnc,multiply(X0,b)),
inference(paramodulation,[status(thm)],[f39,f34]) ).
fof(f373,plain,
! [X0,X1] : multiply(greatest_lower_bound(X0,X1),inverse(X0)) = greatest_lower_bound(identity,multiply(X1,inverse(X0))),
inference(paramodulation,[status(thm)],[f54,f34]) ).
fof(f415,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),identity),
inference(paramodulation,[status(thm)],[f21,f87]) ).
fof(f425,plain,
! [X0,X1,X2] : multiply(inverse(X0),greatest_lower_bound(X1,multiply(X0,X2))) = greatest_lower_bound(multiply(inverse(X0),X1),X2),
inference(paramodulation,[status(thm)],[f87,f32]) ).
fof(f435,plain,
! [X0] : X0 = multiply(X0,identity),
inference(forward_demodulation,[status(thm)],[f36,f415]) ).
fof(f505,plain,
! [X0] : multiply(sF2_fnc,multiply(inverse(sF3_fnc),X0)) = multiply(a,X0),
inference(paramodulation,[status(thm)],[f122,f83]) ).
fof(f521,plain,
! [X0] : multiply(sF2_fnc,multiply(sF4_fnc,X0)) = multiply(a,X0),
inference(forward_demodulation,[status(thm)],[f48,f505]) ).
fof(f567,plain,
! [X0] : inverse(multiply(X0,sF4_fnc)) = multiply(sF3_fnc,inverse(X0)),
inference(paramodulation,[status(thm)],[f43,f37]) ).
fof(f568,plain,
! [X0] : inverse(multiply(X0,b)) = multiply(sF5_fnc,inverse(X0)),
inference(paramodulation,[status(thm)],[f41,f37]) ).
fof(f575,plain,
! [X0,X1] : inverse(X0) = multiply(X1,inverse(multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f37,f122]) ).
fof(f833,plain,
! [X0,X1] : least_upper_bound(X0,least_upper_bound(X1,X0)) = least_upper_bound(X0,X1),
inference(forward_demodulation,[status(thm)],[f26,f132]) ).
fof(f2389,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(inverse(X1),inverse(inverse(multiply(X1,X0)))),
inference(paramodulation,[status(thm)],[f37,f575]) ).
fof(f2452,plain,
! [X0,X1] : X0 = multiply(inverse(X1),inverse(inverse(multiply(X1,X0)))),
inference(forward_demodulation,[status(thm)],[f36,f2389]) ).
fof(f2453,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(multiply(X1,X0)),X1)),
inference(forward_demodulation,[status(thm)],[f37,f2452]) ).
fof(f2544,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,X0)),X1),
inference(paramodulation,[status(thm)],[f2453,f36]) ).
fof(f4985,plain,
! [X0,X1,X2] : inverse(greatest_lower_bound(X0,X1)) = multiply(inverse(multiply(X2,greatest_lower_bound(X1,X0))),X2),
inference(paramodulation,[status(thm)],[f260,f2544]) ).
fof(f5043,plain,
! [X0,X1] : inverse(greatest_lower_bound(X0,X1)) = inverse(greatest_lower_bound(X1,X0)),
inference(forward_demodulation,[status(thm)],[f2544,f4985]) ).
fof(f5157,plain,
multiply(inverse(sF0_fnc),sF0_fnc) = least_upper_bound(identity,multiply(inverse(sF0_fnc),identity)),
inference(paramodulation,[status(thm)],[f162,f198]) ).
fof(f5162,plain,
multiply(inverse(sF5_fnc),sF5_fnc) = least_upper_bound(identity,multiply(inverse(sF5_fnc),sF4_fnc)),
inference(paramodulation,[status(thm)],[f131,f198]) ).
fof(f5227,plain,
identity = least_upper_bound(identity,multiply(inverse(sF0_fnc),identity)),
inference(forward_demodulation,[status(thm)],[f21,f5157]) ).
fof(f5228,plain,
identity = least_upper_bound(identity,inverse(sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f435,f5227]) ).
fof(f5237,plain,
identity = least_upper_bound(identity,multiply(inverse(sF5_fnc),sF4_fnc)),
inference(forward_demodulation,[status(thm)],[f21,f5162]) ).
fof(f5238,plain,
identity = least_upper_bound(identity,multiply(b,sF4_fnc)),
inference(forward_demodulation,[status(thm)],[f49,f5237]) ).
fof(f5414,plain,
greatest_lower_bound(inverse(sF0_fnc),identity) = inverse(sF0_fnc),
inference(paramodulation,[status(thm)],[f5228,f76]) ).
fof(f5561,plain,
greatest_lower_bound(identity,inverse(sF0_fnc)) = inverse(sF0_fnc),
inference(paramodulation,[status(thm)],[f23,f5414]) ).
fof(f7297,plain,
multiply(inverse(inverse(sF0_fnc)),inverse(sF0_fnc)) = greatest_lower_bound(multiply(inverse(inverse(sF0_fnc)),identity),identity),
inference(paramodulation,[status(thm)],[f5561,f249]) ).
fof(f7379,plain,
inverse(multiply(sF0_fnc,inverse(sF0_fnc))) = greatest_lower_bound(multiply(inverse(inverse(sF0_fnc)),identity),identity),
inference(forward_demodulation,[status(thm)],[f37,f7297]) ).
fof(f7380,plain,
inverse(identity) = greatest_lower_bound(multiply(inverse(inverse(sF0_fnc)),identity),identity),
inference(forward_demodulation,[status(thm)],[f54,f7379]) ).
fof(f7381,plain,
identity = greatest_lower_bound(multiply(inverse(inverse(sF0_fnc)),identity),identity),
inference(forward_demodulation,[status(thm)],[f35,f7380]) ).
fof(f7382,plain,
identity = greatest_lower_bound(inverse(inverse(sF0_fnc)),identity),
inference(forward_demodulation,[status(thm)],[f435,f7381]) ).
fof(f7383,plain,
identity = greatest_lower_bound(sF0_fnc,identity),
inference(forward_demodulation,[status(thm)],[f36,f7382]) ).
fof(f8696,plain,
inverse(multiply(sF4_fnc,b)) = multiply(sF5_fnc,sF3_fnc),
inference(paramodulation,[status(thm)],[f43,f568]) ).
fof(f8849,plain,
! [X0] : multiply(identity,X0) = least_upper_bound(X0,multiply(multiply(b,sF4_fnc),X0)),
inference(paramodulation,[status(thm)],[f5238,f330]) ).
fof(f8966,plain,
! [X0] : X0 = least_upper_bound(X0,multiply(multiply(b,sF4_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f20,f8849]) ).
fof(f8967,plain,
! [X0] : X0 = least_upper_bound(X0,multiply(b,multiply(sF4_fnc,X0))),
inference(forward_demodulation,[status(thm)],[f22,f8966]) ).
fof(f9011,plain,
multiply(a,sF3_fnc) = least_upper_bound(sF2_fnc,multiply(sF4_fnc,sF3_fnc)),
inference(paramodulation,[status(thm)],[f70,f332]) ).
fof(f9051,plain,
sF2_fnc = least_upper_bound(sF2_fnc,multiply(sF4_fnc,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f44,f9011]) ).
fof(f9052,plain,
sF2_fnc = least_upper_bound(sF2_fnc,identity),
inference(forward_demodulation,[status(thm)],[f53,f9051]) ).
fof(f9073,plain,
sF2_fnc = least_upper_bound(identity,sF2_fnc),
inference(paramodulation,[status(thm)],[f24,f9052]) ).
fof(f9112,plain,
least_upper_bound(sF1_fnc,sF2_fnc) = least_upper_bound(sF0_fnc,sF2_fnc),
inference(paramodulation,[status(thm)],[f9073,f173]) ).
fof(f10704,plain,
least_upper_bound(sF2_fnc,least_upper_bound(sF0_fnc,sF2_fnc)) = least_upper_bound(sF2_fnc,sF1_fnc),
inference(paramodulation,[status(thm)],[f9112,f833]) ).
fof(f10712,plain,
least_upper_bound(sF2_fnc,sF0_fnc) = least_upper_bound(sF2_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f833,f10704]) ).
fof(f11608,plain,
multiply(sF4_fnc,sF3_fnc) = greatest_lower_bound(sF2_fnc,multiply(sF5_fnc,sF3_fnc)),
inference(paramodulation,[status(thm)],[f42,f371]) ).
fof(f11654,plain,
identity = greatest_lower_bound(sF2_fnc,multiply(sF5_fnc,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f53,f11608]) ).
fof(f13903,plain,
multiply(sF4_fnc,b) = greatest_lower_bound(sF1_fnc,multiply(sF5_fnc,b)),
inference(paramodulation,[status(thm)],[f42,f372]) ).
fof(f13956,plain,
multiply(sF4_fnc,b) = greatest_lower_bound(sF1_fnc,identity),
inference(forward_demodulation,[status(thm)],[f57,f13903]) ).
fof(f19467,plain,
multiply(a,sF3_fnc) = least_upper_bound(sF2_fnc,multiply(a,multiply(b,multiply(sF4_fnc,sF3_fnc)))),
inference(paramodulation,[status(thm)],[f8967,f200]) ).
fof(f19542,plain,
sF2_fnc = least_upper_bound(sF2_fnc,multiply(a,multiply(b,multiply(sF4_fnc,sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f44,f19467]) ).
fof(f19543,plain,
sF2_fnc = least_upper_bound(sF2_fnc,multiply(sF1_fnc,multiply(sF4_fnc,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f84,f19542]) ).
fof(f19544,plain,
sF2_fnc = least_upper_bound(sF2_fnc,multiply(sF1_fnc,identity)),
inference(forward_demodulation,[status(thm)],[f53,f19543]) ).
fof(f19545,plain,
sF2_fnc = least_upper_bound(sF2_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f435,f19544]) ).
fof(f19546,plain,
sF2_fnc = least_upper_bound(sF2_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f10712,f19545]) ).
fof(f19665,plain,
! [X0] : greatest_lower_bound(sF0_fnc,greatest_lower_bound(sF2_fnc,X0)) = greatest_lower_bound(sF0_fnc,X0),
inference(paramodulation,[status(thm)],[f19546,f158]) ).
fof(f33071,plain,
multiply(identity,inverse(sF2_fnc)) = greatest_lower_bound(identity,multiply(multiply(sF5_fnc,sF3_fnc),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f11654,f373]) ).
fof(f33328,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,multiply(multiply(sF5_fnc,sF3_fnc),inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f20,f33071]) ).
fof(f33329,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,multiply(sF5_fnc,multiply(sF3_fnc,inverse(sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f22,f33328]) ).
fof(f33330,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,multiply(sF5_fnc,inverse(multiply(sF2_fnc,sF4_fnc)))),
inference(forward_demodulation,[status(thm)],[f567,f33329]) ).
fof(f33331,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,inverse(multiply(multiply(sF2_fnc,sF4_fnc),b))),
inference(forward_demodulation,[status(thm)],[f568,f33330]) ).
fof(f33332,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,inverse(multiply(sF2_fnc,multiply(sF4_fnc,b)))),
inference(forward_demodulation,[status(thm)],[f22,f33331]) ).
fof(f33333,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,inverse(multiply(a,b))),
inference(forward_demodulation,[status(thm)],[f521,f33332]) ).
fof(f33334,plain,
inverse(sF2_fnc) = greatest_lower_bound(identity,inverse(sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f39,f33333]) ).
fof(f33959,plain,
multiply(sF1_fnc,inverse(sF2_fnc)) = greatest_lower_bound(multiply(sF1_fnc,identity),identity),
inference(paramodulation,[status(thm)],[f33334,f253]) ).
fof(f33981,plain,
multiply(sF1_fnc,inverse(sF2_fnc)) = greatest_lower_bound(sF1_fnc,identity),
inference(forward_demodulation,[status(thm)],[f435,f33959]) ).
fof(f140082,plain,
inverse(greatest_lower_bound(sF1_fnc,identity)) = multiply(sF5_fnc,sF3_fnc),
inference(forward_demodulation,[status(thm)],[f13956,f8696]) ).
fof(f140083,plain,
inverse(greatest_lower_bound(identity,sF1_fnc)) = multiply(sF5_fnc,sF3_fnc),
inference(paramodulation,[status(thm)],[f5043,f140082]) ).
fof(f176408,plain,
greatest_lower_bound(sF0_fnc,identity) = greatest_lower_bound(sF0_fnc,multiply(sF5_fnc,sF3_fnc)),
inference(paramodulation,[status(thm)],[f11654,f19665]) ).
fof(f176728,plain,
identity = greatest_lower_bound(sF0_fnc,multiply(sF5_fnc,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f7383,f176408]) ).
fof(f177117,plain,
multiply(inverse(sF5_fnc),identity) = greatest_lower_bound(multiply(inverse(sF5_fnc),sF0_fnc),sF3_fnc),
inference(paramodulation,[status(thm)],[f176728,f425]) ).
fof(f177218,plain,
inverse(sF5_fnc) = greatest_lower_bound(multiply(inverse(sF5_fnc),sF0_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f435,f177117]) ).
fof(f177219,plain,
b = greatest_lower_bound(multiply(inverse(sF5_fnc),sF0_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f49,f177218]) ).
fof(f177220,plain,
b = greatest_lower_bound(multiply(b,sF0_fnc),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f49,f177219]) ).
fof(f177429,plain,
b = greatest_lower_bound(sF3_fnc,multiply(b,sF0_fnc)),
inference(paramodulation,[status(thm)],[f23,f177220]) ).
fof(f179241,plain,
multiply(a,b) = greatest_lower_bound(sF2_fnc,multiply(a,multiply(b,sF0_fnc))),
inference(paramodulation,[status(thm)],[f177429,f241]) ).
fof(f179347,plain,
sF1_fnc = greatest_lower_bound(sF2_fnc,multiply(a,multiply(b,sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f39,f179241]) ).
fof(f179348,plain,
sF1_fnc = greatest_lower_bound(sF2_fnc,multiply(sF1_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f84,f179347]) ).
fof(f179954,plain,
greatest_lower_bound(sF0_fnc,sF1_fnc) = greatest_lower_bound(sF0_fnc,multiply(sF1_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f179348,f19665]) ).
fof(f180058,plain,
sF1_fnc = greatest_lower_bound(sF0_fnc,multiply(sF1_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f138,f179954]) ).
fof(f182916,plain,
multiply(sF1_fnc,inverse(sF0_fnc)) = greatest_lower_bound(identity,multiply(multiply(sF1_fnc,sF0_fnc),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f180058,f373]) ).
fof(f182963,plain,
multiply(sF1_fnc,inverse(sF0_fnc)) = greatest_lower_bound(identity,multiply(sF1_fnc,multiply(sF0_fnc,inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f22,f182916]) ).
fof(f182964,plain,
multiply(sF1_fnc,inverse(sF0_fnc)) = greatest_lower_bound(identity,multiply(sF1_fnc,identity)),
inference(forward_demodulation,[status(thm)],[f54,f182963]) ).
fof(f182965,plain,
multiply(sF1_fnc,inverse(sF0_fnc)) = greatest_lower_bound(identity,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f435,f182964]) ).
fof(f227294,plain,
inverse(inverse(sF2_fnc)) = multiply(inverse(greatest_lower_bound(sF1_fnc,identity)),sF1_fnc),
inference(paramodulation,[status(thm)],[f33981,f2544]) ).
fof(f227350,plain,
sF2_fnc = multiply(inverse(greatest_lower_bound(sF1_fnc,identity)),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f36,f227294]) ).
fof(f227351,plain,
sF2_fnc = multiply(multiply(sF5_fnc,sF3_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f140082,f227350]) ).
fof(f227352,plain,
sF2_fnc = multiply(sF5_fnc,multiply(sF3_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f22,f227351]) ).
fof(f227363,plain,
multiply(sF3_fnc,sF1_fnc) = multiply(b,sF2_fnc),
inference(paramodulation,[status(thm)],[f227352,f108]) ).
fof(f499281,plain,
inverse(inverse(sF0_fnc)) = multiply(inverse(greatest_lower_bound(identity,sF1_fnc)),sF1_fnc),
inference(paramodulation,[status(thm)],[f182965,f2544]) ).
fof(f499360,plain,
sF0_fnc = multiply(inverse(greatest_lower_bound(identity,sF1_fnc)),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f36,f499281]) ).
fof(f499361,plain,
sF0_fnc = multiply(multiply(sF5_fnc,sF3_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f140083,f499360]) ).
fof(f499362,plain,
sF0_fnc = multiply(sF5_fnc,multiply(sF3_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f22,f499361]) ).
fof(f499363,plain,
sF0_fnc = multiply(sF5_fnc,multiply(b,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f227363,f499362]) ).
fof(f499364,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f126,f499363]) ).
fof(f499365,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f499364,f45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP186-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/5.40 % Computer : n003.cluster.edu
% 0.13/5.40 % Model : x86_64 x86_64
% 0.13/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.40 % Memory : 8046.5625MB
% 0.13/5.40 % OS : Linux 6.8.0-71-generic
% 0.13/5.40 % CPULimit : 300
% 0.13/5.40 % WCLimit : 300
% 0.13/5.40 % DateTime : Sun Sep 20 20:06:51 UTC 2026
% 0.13/5.41 % CPUTime :
% 0.13/5.42 % Drodi V4.1.1
% 209.28/32.17 % Refutation found
% 209.28/32.17 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 209.28/32.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.04/32.48 % Elapsed time: 27.051611 seconds
% 11.04/32.48 % CPU time: 212.323117 seconds
% 11.04/32.48 % Total memory used: 841.306 MB
% 11.04/32.48 % Net memory used: 814.445 MB
%------------------------------------------------------------------------------