%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP179-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 01:25:33 PM UTC 2026
% Result : Unsatisfiable 24.74s 3.55s
% Output : CNFRefutation 24.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 20
% Syntax : Number of clauses : 186 ( 186 unt; 0 nHn; 100 RR)
% Number of literals : 186 ( 185 equ; 7 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 141 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t15,axiom,
sF0 = inverse(a),
introduced(definition) ).
cnf(t20,plain,
inverse(a) = sF0,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sF1 = inverse(b),
introduced(definition) ).
cnf(t21,plain,
inverse(b) = sF1,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sF2 = greatest_lower_bound(inverse(a),inverse(b)),
introduced(definition) ).
cnf(t4,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t8909,plain,
sF2 = greatest_lower_bound(inverse(b),inverse(a)),
inference(step,[status(thm)],[t17,t33]) ).
cnf(t8910,plain,
sF2 = greatest_lower_bound(sF1,inverse(a)),
inference(step,[status(thm)],[t8909,t21]) ).
cnf(t8911,plain,
sF2 = greatest_lower_bound(sF1,sF0),
inference(step,[status(thm)],[t8910,t20]) ).
cnf(t8912,plain,
sF2 = greatest_lower_bound(sF0,sF1),
inference(step,[status(thm)],[t8911,t33]) ).
cnf(t66,plain,
greatest_lower_bound(sF0,sF1) = sF2,
inference(orient,[status(thm)],[t8912]) ).
cnf(t6,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t70,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t18,axiom,
sF3 = least_upper_bound(a,b),
introduced(definition) ).
cnf(t25,plain,
least_upper_bound(a,b) = sF3,
inference(orient,[status(thm)],[t18]) ).
cnf(t8913,plain,
least_upper_bound(b,a) = sF3,
inference(step,[status(thm)],[t25,t70]) ).
cnf(t71,plain,
least_upper_bound(b,a) = sF3,
inference(rw,[status(thm)],[t8913]) ).
cnf(t80,plain,
least_upper_bound(b,a) = sF3,
inference(orient,[status(thm)],[t71]) ).
cnf(t19,axiom,
sF4 = inverse(least_upper_bound(a,b)),
introduced(definition) ).
cnf(t8907,plain,
sF4 = inverse(sF3),
inference(step,[status(thm)],[t19,t25]) ).
cnf(t31,plain,
inverse(sF3) = sF4,
inference(orient,[status(thm)],[t8907]) ).
cnf(t10,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t3,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t32,plain,
identity = multiply(sF4,sF3),
inference(cp,[status(thm)],[t26,t31]) ).
cnf(t34,plain,
multiply(sF4,sF3) = identity,
inference(orient,[status(thm)],[t32]) ).
cnf(t65,plain,
multiply(sF4,multiply(sF3,X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t61,t34]) ).
cnf(t2,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t8918,plain,
multiply(sF4,multiply(sF3,X1)) = X1,
inference(step,[status(thm)],[t65,t24]) ).
cnf(t159,plain,
multiply(sF4,multiply(sF3,X1)) = X1,
inference(orient,[status(thm)],[t8918]) ).
cnf(t14,axiom,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t243,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t247,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(multiply(X1,X2),identity),
inference(cp,[status(thm)],[t243,t26]) ).
cnf(t9244,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(identity,multiply(X1,X2)),
inference(step,[status(thm)],[t247,t70]) ).
cnf(t7545,plain,
multiply(least_upper_bound(X1,inverse(X2)),X2) = least_upper_bound(identity,multiply(X1,X2)),
inference(orient,[status(thm)],[t9244]) ).
cnf(t9,axiom,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t83,plain,
least_upper_bound(b,least_upper_bound(a,X1)) = least_upper_bound(sF3,X1),
inference(cp,[status(thm)],[t53,t80]) ).
cnf(t208,plain,
least_upper_bound(b,least_upper_bound(a,X1)) = least_upper_bound(sF3,X1),
inference(orient,[status(thm)],[t83]) ).
cnf(t7,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t41,plain,
X1 = least_upper_bound(X1,greatest_lower_bound(X2,X1)),
inference(cp,[status(thm)],[t40,t33]) ).
cnf(t103,plain,
least_upper_bound(X1,greatest_lower_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t41]) ).
cnf(t62,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t61,t26]) ).
cnf(t8980,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t62,t24]) ).
cnf(t1060,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t8980]) ).
cnf(t1062,plain,
X1 = multiply(inverse(inverse(X1)),identity),
inference(cp,[status(thm)],[t1060,t26]) ).
cnf(t2122,plain,
multiply(inverse(inverse(X1)),identity) = X1,
inference(orient,[status(thm)],[t1062]) ).
cnf(t1078,plain,
multiply(X1,X2) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t1060,t1060]) ).
cnf(t2136,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t1078]) ).
cnf(t9052,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t2122,t2136]) ).
cnf(t2137,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[t9052]) ).
cnf(t2180,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t2137]) ).
cnf(t2197,plain,
inverse(inverse(X1)) = multiply(X1,identity),
inference(cp,[status(thm)],[t2180,t2136]) ).
cnf(t9075,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t2197,t2180]) ).
cnf(t2248,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t9075]) ).
cnf(t11,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t91,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t93,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(multiply(inverse(X1),X2),identity),
inference(cp,[status(thm)],[t91,t26]) ).
cnf(t9004,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t93,t33]) ).
cnf(t1532,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t9004]) ).
cnf(t8,axiom,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t44,plain,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t0,axiom,
greatest_lower_bound(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
greatest_lower_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t46,plain,
greatest_lower_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,X2),
inference(cp,[status(thm)],[t44,t22]) ).
cnf(t114,plain,
greatest_lower_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t46]) ).
cnf(t117,plain,
greatest_lower_bound(sF0,sF1) = greatest_lower_bound(sF0,sF2),
inference(cp,[status(thm)],[t114,t66]) ).
cnf(t8915,plain,
sF2 = greatest_lower_bound(sF0,sF2),
inference(step,[status(thm)],[t117,t66]) ).
cnf(t118,plain,
greatest_lower_bound(sF0,sF2) = sF2,
inference(orient,[status(thm)],[t8915]) ).
cnf(t1541,plain,
greatest_lower_bound(identity,multiply(inverse(sF2),sF0)) = multiply(inverse(sF2),sF2),
inference(cp,[status(thm)],[t1532,t118]) ).
cnf(t12,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t128,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t27,plain,
identity = multiply(sF0,a),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t29,plain,
multiply(sF0,a) = identity,
inference(orient,[status(thm)],[t27]) ).
cnf(t63,plain,
multiply(sF0,multiply(a,X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t61,t29]) ).
cnf(t8916,plain,
multiply(sF0,multiply(a,X1)) = X1,
inference(step,[status(thm)],[t63,t24]) ).
cnf(t149,plain,
multiply(sF0,multiply(a,X1)) = X1,
inference(orient,[status(thm)],[t8916]) ).
cnf(t1067,plain,
multiply(a,X1) = multiply(inverse(sF0),X1),
inference(cp,[status(thm)],[t1060,t149]) ).
cnf(t1139,plain,
multiply(inverse(sF0),X1) = multiply(a,X1),
inference(orient,[status(thm)],[t1067]) ).
cnf(t1141,plain,
multiply(a,sF0) = identity,
inference(cp,[status(thm)],[t1139,t26]) ).
cnf(t1159,plain,
multiply(a,sF0) = identity,
inference(orient,[status(thm)],[t1141]) ).
cnf(t1162,plain,
multiply(greatest_lower_bound(a,X1),sF0) = greatest_lower_bound(identity,multiply(X1,sF0)),
inference(cp,[status(thm)],[t128,t1159]) ).
cnf(t2286,plain,
greatest_lower_bound(identity,multiply(X1,sF0)) = multiply(greatest_lower_bound(a,X1),sF0),
inference(orient,[status(thm)],[t1162]) ).
cnf(t9262,plain,
multiply(greatest_lower_bound(a,inverse(sF2)),sF0) = multiply(inverse(sF2),sF2),
inference(step,[status(thm)],[t1541,t2286]) ).
cnf(t9263,plain,
multiply(greatest_lower_bound(a,inverse(sF2)),sF0) = identity,
inference(step,[status(thm)],[t9262,t26]) ).
cnf(t8667,plain,
multiply(greatest_lower_bound(a,inverse(sF2)),sF0) = identity,
inference(orient,[status(thm)],[t9263]) ).
cnf(t8680,plain,
sF0 = multiply(inverse(greatest_lower_bound(a,inverse(sF2))),identity),
inference(cp,[status(thm)],[t1060,t8667]) ).
cnf(t9264,plain,
sF0 = inverse(greatest_lower_bound(a,inverse(sF2))),
inference(step,[status(thm)],[t8680,t2180]) ).
cnf(t8697,plain,
inverse(greatest_lower_bound(a,inverse(sF2))) = sF0,
inference(orient,[status(thm)],[t9264]) ).
cnf(t8703,plain,
greatest_lower_bound(a,inverse(sF2)) = inverse(sF0),
inference(cp,[status(thm)],[t2248,t8697]) ).
cnf(t2194,plain,
inverse(sF0) = multiply(a,identity),
inference(cp,[status(thm)],[t2180,t1139]) ).
cnf(t9067,plain,
inverse(sF0) = a,
inference(step,[status(thm)],[t2194,t2180]) ).
cnf(t2212,plain,
inverse(sF0) = a,
inference(orient,[status(thm)],[t9067]) ).
cnf(t9265,plain,
greatest_lower_bound(a,inverse(sF2)) = a,
inference(step,[status(thm)],[t8703,t2212]) ).
cnf(t8710,plain,
greatest_lower_bound(a,inverse(sF2)) = a,
inference(orient,[status(thm)],[t9265]) ).
cnf(t8715,plain,
inverse(sF2) = least_upper_bound(inverse(sF2),a),
inference(cp,[status(thm)],[t103,t8710]) ).
cnf(t9268,plain,
inverse(sF2) = least_upper_bound(a,inverse(sF2)),
inference(step,[status(thm)],[t8715,t70]) ).
cnf(t8738,plain,
least_upper_bound(a,inverse(sF2)) = inverse(sF2),
inference(orient,[status(thm)],[t9268]) ).
cnf(t8741,plain,
least_upper_bound(sF3,inverse(sF2)) = least_upper_bound(b,inverse(sF2)),
inference(cp,[status(thm)],[t208,t8738]) ).
cnf(t8749,plain,
least_upper_bound(b,inverse(sF2)) = least_upper_bound(sF3,inverse(sF2)),
inference(orient,[status(thm)],[t8741]) ).
cnf(t8761,plain,
least_upper_bound(identity,multiply(b,sF2)) = multiply(least_upper_bound(sF3,inverse(sF2)),sF2),
inference(cp,[status(thm)],[t7545,t8749]) ).
cnf(t13,axiom,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t186,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t28,plain,
identity = multiply(sF1,b),
inference(cp,[status(thm)],[t26,t21]) ).
cnf(t30,plain,
multiply(sF1,b) = identity,
inference(orient,[status(thm)],[t28]) ).
cnf(t64,plain,
multiply(sF1,multiply(b,X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t61,t30]) ).
cnf(t8917,plain,
multiply(sF1,multiply(b,X1)) = X1,
inference(step,[status(thm)],[t64,t24]) ).
cnf(t154,plain,
multiply(sF1,multiply(b,X1)) = X1,
inference(orient,[status(thm)],[t8917]) ).
cnf(t1068,plain,
multiply(b,X1) = multiply(inverse(sF1),X1),
inference(cp,[status(thm)],[t1060,t154]) ).
cnf(t1235,plain,
multiply(inverse(sF1),X1) = multiply(b,X1),
inference(orient,[status(thm)],[t1068]) ).
cnf(t1237,plain,
multiply(b,sF1) = identity,
inference(cp,[status(thm)],[t1235,t26]) ).
cnf(t1255,plain,
multiply(b,sF1) = identity,
inference(orient,[status(thm)],[t1237]) ).
cnf(t1261,plain,
multiply(b,least_upper_bound(sF1,X1)) = least_upper_bound(identity,multiply(b,X1)),
inference(cp,[status(thm)],[t186,t1255]) ).
cnf(t2500,plain,
least_upper_bound(identity,multiply(b,X1)) = multiply(b,least_upper_bound(sF1,X1)),
inference(orient,[status(thm)],[t1261]) ).
cnf(t9269,plain,
multiply(b,least_upper_bound(sF1,sF2)) = multiply(least_upper_bound(sF3,inverse(sF2)),sF2),
inference(step,[status(thm)],[t8761,t2500]) ).
cnf(t107,plain,
sF1 = least_upper_bound(sF1,sF2),
inference(cp,[status(thm)],[t103,t66]) ).
cnf(t111,plain,
least_upper_bound(sF1,sF2) = sF1,
inference(orient,[status(thm)],[t107]) ).
cnf(t9270,plain,
multiply(b,sF1) = multiply(least_upper_bound(sF3,inverse(sF2)),sF2),
inference(step,[status(thm)],[t9269,t111]) ).
cnf(t9271,plain,
identity = multiply(least_upper_bound(sF3,inverse(sF2)),sF2),
inference(step,[status(thm)],[t9270,t1255]) ).
cnf(t9272,plain,
identity = least_upper_bound(identity,multiply(sF3,sF2)),
inference(step,[status(thm)],[t9271,t7545]) ).
cnf(t1069,plain,
multiply(sF3,X1) = multiply(inverse(sF4),X1),
inference(cp,[status(thm)],[t1060,t159]) ).
cnf(t1280,plain,
multiply(inverse(sF4),X1) = multiply(sF3,X1),
inference(orient,[status(thm)],[t1069]) ).
cnf(t1282,plain,
multiply(sF3,sF4) = identity,
inference(cp,[status(thm)],[t1280,t26]) ).
cnf(t1300,plain,
multiply(sF3,sF4) = identity,
inference(orient,[status(thm)],[t1282]) ).
cnf(t1306,plain,
multiply(sF3,least_upper_bound(sF4,X1)) = least_upper_bound(identity,multiply(sF3,X1)),
inference(cp,[status(thm)],[t186,t1300]) ).
cnf(t2685,plain,
least_upper_bound(identity,multiply(sF3,X1)) = multiply(sF3,least_upper_bound(sF4,X1)),
inference(orient,[status(thm)],[t1306]) ).
cnf(t9273,plain,
identity = multiply(sF3,least_upper_bound(sF4,sF2)),
inference(step,[status(thm)],[t9272,t2685]) ).
cnf(t1307,plain,
multiply(sF3,least_upper_bound(X1,sF4)) = least_upper_bound(multiply(sF3,X1),identity),
inference(cp,[status(thm)],[t186,t1300]) ).
cnf(t9099,plain,
multiply(sF3,least_upper_bound(X1,sF4)) = least_upper_bound(identity,multiply(sF3,X1)),
inference(step,[status(thm)],[t1307,t70]) ).
cnf(t9100,plain,
multiply(sF3,least_upper_bound(X1,sF4)) = multiply(sF3,least_upper_bound(sF4,X1)),
inference(step,[status(thm)],[t9099,t2685]) ).
cnf(t2836,plain,
multiply(sF3,least_upper_bound(X1,sF4)) = multiply(sF3,least_upper_bound(sF4,X1)),
inference(orient,[status(thm)],[t9100]) ).
cnf(t9274,plain,
identity = multiply(sF3,least_upper_bound(sF2,sF4)),
inference(step,[status(thm)],[t9273,t2836]) ).
cnf(t69,plain,
greatest_lower_bound(sF0,greatest_lower_bound(sF1,X1)) = greatest_lower_bound(sF2,X1),
inference(cp,[status(thm)],[t44,t66]) ).
cnf(t164,plain,
greatest_lower_bound(sF0,greatest_lower_bound(sF1,X1)) = greatest_lower_bound(sF2,X1),
inference(orient,[status(thm)],[t69]) ).
cnf(t156,plain,
multiply(sF1,greatest_lower_bound(X1,multiply(b,X2))) = greatest_lower_bound(multiply(sF1,X1),X2),
inference(cp,[status(thm)],[t91,t154]) ).
cnf(t3819,plain,
multiply(sF1,greatest_lower_bound(X1,multiply(b,X2))) = greatest_lower_bound(multiply(sF1,X1),X2),
inference(orient,[status(thm)],[t156]) ).
cnf(t1303,plain,
multiply(greatest_lower_bound(sF3,X1),sF4) = greatest_lower_bound(identity,multiply(X1,sF4)),
inference(cp,[status(thm)],[t128,t1300]) ).
cnf(t2663,plain,
greatest_lower_bound(identity,multiply(X1,sF4)) = multiply(greatest_lower_bound(sF3,X1),sF4),
inference(orient,[status(thm)],[t1303]) ).
cnf(t3830,plain,
greatest_lower_bound(multiply(sF1,identity),sF4) = multiply(sF1,multiply(greatest_lower_bound(sF3,b),sF4)),
inference(cp,[status(thm)],[t3819,t2663]) ).
cnf(t9137,plain,
greatest_lower_bound(sF4,multiply(sF1,identity)) = multiply(sF1,multiply(greatest_lower_bound(sF3,b),sF4)),
inference(step,[status(thm)],[t3830,t33]) ).
cnf(t9138,plain,
greatest_lower_bound(sF4,sF1) = multiply(sF1,multiply(greatest_lower_bound(sF3,b),sF4)),
inference(step,[status(thm)],[t9137,t2180]) ).
cnf(t9139,plain,
greatest_lower_bound(sF1,sF4) = multiply(sF1,multiply(greatest_lower_bound(sF3,b),sF4)),
inference(step,[status(thm)],[t9138,t33]) ).
cnf(t5,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t82,plain,
b = greatest_lower_bound(b,sF3),
inference(cp,[status(thm)],[t35,t80]) ).
cnf(t8914,plain,
b = greatest_lower_bound(sF3,b),
inference(step,[status(thm)],[t82,t33]) ).
cnf(t84,plain,
greatest_lower_bound(sF3,b) = b,
inference(orient,[status(thm)],[t8914]) ).
cnf(t9140,plain,
greatest_lower_bound(sF1,sF4) = multiply(sF1,multiply(b,sF4)),
inference(step,[status(thm)],[t9139,t84]) ).
cnf(t9141,plain,
greatest_lower_bound(sF1,sF4) = sF4,
inference(step,[status(thm)],[t9140,t154]) ).
cnf(t3854,plain,
greatest_lower_bound(sF1,sF4) = sF4,
inference(orient,[status(thm)],[t9141]) ).
cnf(t3860,plain,
greatest_lower_bound(sF2,sF4) = greatest_lower_bound(sF0,sF4),
inference(cp,[status(thm)],[t164,t3854]) ).
cnf(t151,plain,
multiply(sF0,greatest_lower_bound(X1,multiply(a,X2))) = greatest_lower_bound(multiply(sF0,X1),X2),
inference(cp,[status(thm)],[t91,t149]) ).
cnf(t3319,plain,
multiply(sF0,greatest_lower_bound(X1,multiply(a,X2))) = greatest_lower_bound(multiply(sF0,X1),X2),
inference(orient,[status(thm)],[t151]) ).
cnf(t3329,plain,
greatest_lower_bound(multiply(sF0,identity),sF4) = multiply(sF0,multiply(greatest_lower_bound(sF3,a),sF4)),
inference(cp,[status(thm)],[t3319,t2663]) ).
cnf(t9117,plain,
greatest_lower_bound(sF4,multiply(sF0,identity)) = multiply(sF0,multiply(greatest_lower_bound(sF3,a),sF4)),
inference(step,[status(thm)],[t3329,t33]) ).
cnf(t9118,plain,
greatest_lower_bound(sF4,sF0) = multiply(sF0,multiply(greatest_lower_bound(sF3,a),sF4)),
inference(step,[status(thm)],[t9117,t2180]) ).
cnf(t9119,plain,
greatest_lower_bound(sF0,sF4) = multiply(sF0,multiply(greatest_lower_bound(sF3,a),sF4)),
inference(step,[status(thm)],[t9118,t33]) ).
cnf(t36,plain,
a = greatest_lower_bound(a,sF3),
inference(cp,[status(thm)],[t35,t25]) ).
cnf(t8908,plain,
a = greatest_lower_bound(sF3,a),
inference(step,[status(thm)],[t36,t33]) ).
cnf(t38,plain,
greatest_lower_bound(sF3,a) = a,
inference(orient,[status(thm)],[t8908]) ).
cnf(t9120,plain,
greatest_lower_bound(sF0,sF4) = multiply(sF0,multiply(a,sF4)),
inference(step,[status(thm)],[t9119,t38]) ).
cnf(t9121,plain,
greatest_lower_bound(sF0,sF4) = sF4,
inference(step,[status(thm)],[t9120,t149]) ).
cnf(t3350,plain,
greatest_lower_bound(sF0,sF4) = sF4,
inference(orient,[status(thm)],[t9121]) ).
cnf(t9144,plain,
greatest_lower_bound(sF2,sF4) = sF4,
inference(step,[status(thm)],[t3860,t3350]) ).
cnf(t3882,plain,
greatest_lower_bound(sF2,sF4) = sF4,
inference(orient,[status(thm)],[t9144]) ).
cnf(t3884,plain,
sF2 = least_upper_bound(sF2,sF4),
inference(cp,[status(thm)],[t40,t3882]) ).
cnf(t3938,plain,
least_upper_bound(sF2,sF4) = sF2,
inference(orient,[status(thm)],[t3884]) ).
cnf(t9275,plain,
identity = multiply(sF3,sF2),
inference(step,[status(thm)],[t9274,t3938]) ).
cnf(t8763,plain,
multiply(sF3,sF2) = identity,
inference(orient,[status(thm)],[t9275]) ).
cnf(t8769,plain,
sF2 = multiply(sF4,identity),
inference(cp,[status(thm)],[t159,t8763]) ).
cnf(t9276,plain,
sF2 = sF4,
inference(step,[status(thm)],[t8769,t2180]) ).
cnf(t8800,plain,
sF4 = sF2,
inference(orient,[status(thm)],[t9276]) ).
cnf(t9277,plain,
inverse(sF3) = sF2,
inference(step,[status(thm)],[t31,t8800]) ).
cnf(t8801,plain,
inverse(sF3) = sF2,
inference(orient,[status(thm)],[t9277]) ).
cnf(goal_0,negated_conjecture,
greatest_lower_bound(inverse(a),inverse(b)) != inverse(least_upper_bound(a,b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
greatest_lower_bound(sF0,inverse(b)) != inverse(least_upper_bound(a,b)),
inference(rw,[status(thm)],[goal_0,t20]) ).
cnf(g0_1,plain,
greatest_lower_bound(sF0,sF1) != inverse(least_upper_bound(a,b)),
inference(rw,[status(thm)],[g0_0,t21]) ).
cnf(g0_2,plain,
sF2 != inverse(least_upper_bound(a,b)),
inference(rw,[status(thm)],[g0_1,t66]) ).
cnf(g0_3,plain,
sF2 != inverse(least_upper_bound(b,a)),
inference(rw,[status(thm)],[g0_2,t70]) ).
cnf(g0_4,plain,
sF2 != inverse(sF3),
inference(rw,[status(thm)],[g0_3,t80]) ).
cnf(g0_5,plain,
sF2 != sF2,
inference(rw,[status(thm)],[g0_4,t8801]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP179-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 13:55:32 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 24.74/3.55 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.74/3.55 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------