%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP185-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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:37 PM UTC 2026
% Result : Unsatisfiable 6.59s 1.57s
% Output : CNFRefutation 6.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 19
% Syntax : Number of clauses : 228 ( 228 unt; 0 nHn; 122 RR)
% Number of literals : 228 ( 227 equ; 15 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 : 145 ( 24 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t94,plain,
least_upper_bound(least_upper_bound(X1,X2),X3) = least_upper_bound(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t18,axiom,
sFlat0 = multiply(a,b),
introduced(definition) ).
cnf(t79,plain,
multiply(a,b) = sFlat0,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat1 = least_upper_bound(multiply(a,b),identity),
introduced(definition) ).
cnf(t8,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t3917,plain,
sFlat1 = least_upper_bound(identity,multiply(a,b)),
inference(step,[status(thm)],[t19,t89]) ).
cnf(t3918,plain,
sFlat1 = least_upper_bound(identity,sFlat0),
inference(step,[status(thm)],[t3917,t79]) ).
cnf(t3919,plain,
sFlat1 = least_upper_bound(sFlat0,identity),
inference(step,[status(thm)],[t3918,t89]) ).
cnf(t104,plain,
least_upper_bound(sFlat0,identity) = sFlat1,
inference(orient,[status(thm)],[t3919]) ).
cnf(t105,plain,
least_upper_bound(sFlat0,least_upper_bound(identity,X1)) = least_upper_bound(sFlat1,X1),
inference(cp,[status(thm)],[t94,t104]) ).
cnf(t229,plain,
least_upper_bound(sFlat0,least_upper_bound(identity,X1)) = least_upper_bound(sFlat1,X1),
inference(orient,[status(thm)],[t105]) ).
cnf(t20,axiom,
sFlat2 = least_upper_bound(a,identity),
introduced(definition) ).
cnf(t3924,plain,
sFlat2 = least_upper_bound(identity,a),
inference(step,[status(thm)],[t20,t89]) ).
cnf(t110,plain,
least_upper_bound(identity,a) = sFlat2,
inference(orient,[status(thm)],[t3924]) ).
cnf(t21,axiom,
sFlat3 = least_upper_bound(b,identity),
introduced(definition) ).
cnf(t3926,plain,
sFlat3 = least_upper_bound(identity,b),
inference(step,[status(thm)],[t21,t89]) ).
cnf(t114,plain,
least_upper_bound(identity,b) = sFlat3,
inference(orient,[status(thm)],[t3926]) ).
cnf(t22,axiom,
sFlat4 = multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
introduced(definition) ).
cnf(t40,plain,
multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)) = sFlat4,
inference(orient,[status(thm)],[t22]) ).
cnf(t93,plain,
multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)) = sFlat4,
inference(rw,[status(thm)],[t40]) ).
cnf(t4080,plain,
multiply(least_upper_bound(identity,a),least_upper_bound(b,identity)) = sFlat4,
inference(step,[status(thm)],[t93,t89]) ).
cnf(t4081,plain,
multiply(sFlat2,least_upper_bound(b,identity)) = sFlat4,
inference(step,[status(thm)],[t4080,t110]) ).
cnf(t4082,plain,
multiply(sFlat2,least_upper_bound(identity,b)) = sFlat4,
inference(step,[status(thm)],[t4081,t89]) ).
cnf(t4083,plain,
multiply(sFlat2,sFlat3) = sFlat4,
inference(step,[status(thm)],[t4082,t114]) ).
cnf(t3164,plain,
multiply(sFlat2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t4083]) ).
cnf(t3,axiom,
least_upper_bound(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
least_upper_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t98,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(cp,[status(thm)],[t94,t25]) ).
cnf(t223,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t98]) ).
cnf(t115,plain,
least_upper_bound(identity,least_upper_bound(b,X1)) = least_upper_bound(sFlat3,X1),
inference(cp,[status(thm)],[t94,t114]) ).
cnf(t333,plain,
least_upper_bound(identity,least_upper_bound(b,X1)) = least_upper_bound(sFlat3,X1),
inference(orient,[status(thm)],[t115]) ).
cnf(t340,plain,
least_upper_bound(identity,least_upper_bound(b,X1)) = least_upper_bound(identity,least_upper_bound(sFlat3,X1)),
inference(cp,[status(thm)],[t223,t333]) ).
cnf(t3957,plain,
least_upper_bound(sFlat3,X1) = least_upper_bound(identity,least_upper_bound(sFlat3,X1)),
inference(step,[status(thm)],[t340,t333]) ).
cnf(t614,plain,
least_upper_bound(identity,least_upper_bound(sFlat3,X1)) = least_upper_bound(sFlat3,X1),
inference(orient,[status(thm)],[t3957]) ).
cnf(t9,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t7,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t116,plain,
identity = greatest_lower_bound(identity,sFlat3),
inference(cp,[status(thm)],[t28,t114]) ).
cnf(t6,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t117,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t3928,plain,
identity = greatest_lower_bound(sFlat3,identity),
inference(step,[status(thm)],[t116,t117]) ).
cnf(t139,plain,
greatest_lower_bound(sFlat3,identity) = identity,
inference(orient,[status(thm)],[t3928]) ).
cnf(t140,plain,
sFlat3 = least_upper_bound(sFlat3,identity),
inference(cp,[status(thm)],[t26,t139]) ).
cnf(t144,plain,
least_upper_bound(sFlat3,identity) = sFlat3,
inference(orient,[status(thm)],[t140]) ).
cnf(t145,plain,
least_upper_bound(sFlat3,least_upper_bound(identity,X1)) = least_upper_bound(sFlat3,X1),
inference(cp,[status(thm)],[t94,t144]) ).
cnf(t411,plain,
least_upper_bound(sFlat3,least_upper_bound(identity,X1)) = least_upper_bound(sFlat3,X1),
inference(orient,[status(thm)],[t145]) ).
cnf(t111,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(sFlat2,X1),
inference(cp,[status(thm)],[t94,t110]) ).
cnf(t299,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(sFlat2,X1),
inference(orient,[status(thm)],[t111]) ).
cnf(t304,plain,
least_upper_bound(sFlat2,X1) = least_upper_bound(identity,least_upper_bound(X1,a)),
inference(cp,[status(thm)],[t299,t89]) ).
cnf(t534,plain,
least_upper_bound(identity,least_upper_bound(X1,a)) = least_upper_bound(sFlat2,X1),
inference(orient,[status(thm)],[t304]) ).
cnf(t16,axiom,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t86,plain,
multiply(a,least_upper_bound(b,X1)) = least_upper_bound(sFlat0,multiply(a,X1)),
inference(cp,[status(thm)],[t31,t79]) ).
cnf(t1206,plain,
least_upper_bound(sFlat0,multiply(a,X1)) = multiply(a,least_upper_bound(b,X1)),
inference(orient,[status(thm)],[t86]) ).
cnf(t2,axiom,
inverse(inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t66,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t10]) ).
cnf(t0,axiom,
inverse(identity) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t131,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t132,plain,
inverse(multiply(X1,identity)) = multiply(identity,inverse(X1)),
inference(cp,[status(thm)],[t66,t131]) ).
cnf(t4,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t3929,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(step,[status(thm)],[t132,t24]) ).
cnf(t157,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(orient,[status(thm)],[t3929]) ).
cnf(t161,plain,
multiply(X1,identity) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t29,t157]) ).
cnf(t3930,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t161,t29]) ).
cnf(t162,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t3930]) ).
cnf(t1212,plain,
multiply(a,least_upper_bound(b,identity)) = least_upper_bound(sFlat0,a),
inference(cp,[status(thm)],[t1206,t162]) ).
cnf(t4001,plain,
multiply(a,least_upper_bound(identity,b)) = least_upper_bound(sFlat0,a),
inference(step,[status(thm)],[t1212,t89]) ).
cnf(t4002,plain,
multiply(a,sFlat3) = least_upper_bound(sFlat0,a),
inference(step,[status(thm)],[t4001,t114]) ).
cnf(t1239,plain,
least_upper_bound(sFlat0,a) = multiply(a,sFlat3),
inference(orient,[status(thm)],[t4002]) ).
cnf(t1242,plain,
least_upper_bound(sFlat2,sFlat0) = least_upper_bound(identity,multiply(a,sFlat3)),
inference(cp,[status(thm)],[t534,t1239]) ).
cnf(t4005,plain,
least_upper_bound(sFlat0,sFlat2) = least_upper_bound(identity,multiply(a,sFlat3)),
inference(step,[status(thm)],[t1242,t89]) ).
cnf(t1261,plain,
least_upper_bound(identity,multiply(a,sFlat3)) = least_upper_bound(sFlat0,sFlat2),
inference(orient,[status(thm)],[t4005]) ).
cnf(t1263,plain,
least_upper_bound(sFlat3,multiply(a,sFlat3)) = least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)),
inference(cp,[status(thm)],[t411,t1261]) ).
cnf(t17,axiom,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t17]) ).
cnf(t35,plain,
multiply(least_upper_bound(identity,X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t34,t24]) ).
cnf(t263,plain,
least_upper_bound(X1,multiply(X2,X1)) = multiply(least_upper_bound(identity,X2),X1),
inference(orient,[status(thm)],[t35]) ).
cnf(t4008,plain,
multiply(least_upper_bound(identity,a),sFlat3) = least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)),
inference(step,[status(thm)],[t1263,t263]) ).
cnf(t4009,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)),
inference(step,[status(thm)],[t4008,t110]) ).
cnf(t1271,plain,
least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t4009]) ).
cnf(t1273,plain,
least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)) = least_upper_bound(identity,multiply(sFlat2,sFlat3)),
inference(cp,[status(thm)],[t614,t1271]) ).
cnf(t4010,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(identity,multiply(sFlat2,sFlat3)),
inference(step,[status(thm)],[t1273,t1271]) ).
cnf(t1286,plain,
least_upper_bound(identity,multiply(sFlat2,sFlat3)) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t4010]) ).
cnf(t1288,plain,
least_upper_bound(sFlat1,multiply(sFlat2,sFlat3)) = least_upper_bound(sFlat0,multiply(sFlat2,sFlat3)),
inference(cp,[status(thm)],[t229,t1286]) ).
cnf(t1706,plain,
least_upper_bound(sFlat1,multiply(sFlat2,sFlat3)) = least_upper_bound(sFlat0,multiply(sFlat2,sFlat3)),
inference(orient,[status(thm)],[t1288]) ).
cnf(t4090,plain,
least_upper_bound(sFlat1,sFlat4) = least_upper_bound(sFlat0,multiply(sFlat2,sFlat3)),
inference(step,[status(thm)],[t1706,t3164]) ).
cnf(t4091,plain,
least_upper_bound(sFlat1,sFlat4) = least_upper_bound(sFlat0,sFlat4),
inference(step,[status(thm)],[t4090,t3164]) ).
cnf(t3196,plain,
least_upper_bound(sFlat1,sFlat4) = least_upper_bound(sFlat0,sFlat4),
inference(rw,[status(thm)],[t4091]) ).
cnf(t3235,plain,
least_upper_bound(sFlat1,sFlat4) = least_upper_bound(sFlat0,sFlat4),
inference(orient,[status(thm)],[t3196]) ).
cnf(t4097,plain,
least_upper_bound(identity,sFlat4) = multiply(sFlat2,sFlat3),
inference(step,[status(thm)],[t1286,t3164]) ).
cnf(t4098,plain,
least_upper_bound(identity,sFlat4) = sFlat4,
inference(step,[status(thm)],[t4097,t3164]) ).
cnf(t3200,plain,
least_upper_bound(identity,sFlat4) = sFlat4,
inference(rw,[status(thm)],[t4098]) ).
cnf(t4104,plain,
least_upper_bound(sFlat4,identity) = sFlat4,
inference(step,[status(thm)],[t3200,t89]) ).
cnf(t3217,plain,
least_upper_bound(sFlat4,identity) = sFlat4,
inference(orient,[status(thm)],[t4104]) ).
cnf(t3223,plain,
least_upper_bound(sFlat4,least_upper_bound(identity,X1)) = least_upper_bound(sFlat4,X1),
inference(cp,[status(thm)],[t94,t3217]) ).
cnf(t3470,plain,
least_upper_bound(sFlat4,least_upper_bound(identity,X1)) = least_upper_bound(sFlat4,X1),
inference(orient,[status(thm)],[t3223]) ).
cnf(t3479,plain,
least_upper_bound(sFlat4,least_upper_bound(b,X1)) = least_upper_bound(sFlat4,least_upper_bound(sFlat3,X1)),
inference(cp,[status(thm)],[t3470,t333]) ).
cnf(t120,plain,
X1 = least_upper_bound(X1,greatest_lower_bound(X2,X1)),
inference(cp,[status(thm)],[t26,t117]) ).
cnf(t195,plain,
least_upper_bound(X1,greatest_lower_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t120]) ).
cnf(t92,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,X1)),
inference(cp,[status(thm)],[t28,t89]) ).
cnf(t167,plain,
greatest_lower_bound(X1,least_upper_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t92]) ).
cnf(t336,plain,
least_upper_bound(sFlat3,greatest_lower_bound(b,X1)) = least_upper_bound(identity,b),
inference(cp,[status(thm)],[t333,t26]) ).
cnf(t3942,plain,
least_upper_bound(sFlat3,greatest_lower_bound(b,X1)) = sFlat3,
inference(step,[status(thm)],[t336,t114]) ).
cnf(t343,plain,
least_upper_bound(sFlat3,greatest_lower_bound(b,X1)) = sFlat3,
inference(orient,[status(thm)],[t3942]) ).
cnf(t345,plain,
greatest_lower_bound(b,X1) = greatest_lower_bound(greatest_lower_bound(b,X1),sFlat3),
inference(cp,[status(thm)],[t167,t343]) ).
cnf(t11,axiom,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t121,plain,
greatest_lower_bound(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t3958,plain,
greatest_lower_bound(b,X1) = greatest_lower_bound(b,greatest_lower_bound(X1,sFlat3)),
inference(step,[status(thm)],[t345,t121]) ).
cnf(t629,plain,
greatest_lower_bound(b,greatest_lower_bound(X1,sFlat3)) = greatest_lower_bound(b,X1),
inference(orient,[status(thm)],[t3958]) ).
cnf(t632,plain,
greatest_lower_bound(b,X1) = greatest_lower_bound(b,greatest_lower_bound(sFlat3,X1)),
inference(cp,[status(thm)],[t629,t117]) ).
cnf(t801,plain,
greatest_lower_bound(b,greatest_lower_bound(sFlat3,X1)) = greatest_lower_bound(b,X1),
inference(orient,[status(thm)],[t632]) ).
cnf(t804,plain,
greatest_lower_bound(b,least_upper_bound(sFlat3,X1)) = greatest_lower_bound(b,sFlat3),
inference(cp,[status(thm)],[t801,t28]) ).
cnf(t3985,plain,
greatest_lower_bound(b,least_upper_bound(sFlat3,X1)) = greatest_lower_bound(sFlat3,b),
inference(step,[status(thm)],[t804,t117]) ).
cnf(t173,plain,
b = greatest_lower_bound(b,sFlat3),
inference(cp,[status(thm)],[t167,t114]) ).
cnf(t3932,plain,
b = greatest_lower_bound(sFlat3,b),
inference(step,[status(thm)],[t173,t117]) ).
cnf(t180,plain,
greatest_lower_bound(sFlat3,b) = b,
inference(orient,[status(thm)],[t3932]) ).
cnf(t3986,plain,
greatest_lower_bound(b,least_upper_bound(sFlat3,X1)) = b,
inference(step,[status(thm)],[t3985,t180]) ).
cnf(t881,plain,
greatest_lower_bound(b,least_upper_bound(sFlat3,X1)) = b,
inference(orient,[status(thm)],[t3986]) ).
cnf(t1272,plain,
b = greatest_lower_bound(b,multiply(sFlat2,sFlat3)),
inference(cp,[status(thm)],[t881,t1271]) ).
cnf(t1280,plain,
greatest_lower_bound(b,multiply(sFlat2,sFlat3)) = b,
inference(orient,[status(thm)],[t1272]) ).
cnf(t1281,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(multiply(sFlat2,sFlat3),b),
inference(cp,[status(thm)],[t195,t1280]) ).
cnf(t4011,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(b,multiply(sFlat2,sFlat3)),
inference(step,[status(thm)],[t1281,t89]) ).
cnf(t1290,plain,
least_upper_bound(b,multiply(sFlat2,sFlat3)) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t4011]) ).
cnf(t4095,plain,
least_upper_bound(b,sFlat4) = multiply(sFlat2,sFlat3),
inference(step,[status(thm)],[t1290,t3164]) ).
cnf(t4096,plain,
least_upper_bound(b,sFlat4) = sFlat4,
inference(step,[status(thm)],[t4095,t3164]) ).
cnf(t3199,plain,
least_upper_bound(b,sFlat4) = sFlat4,
inference(rw,[status(thm)],[t4096]) ).
cnf(t4103,plain,
least_upper_bound(sFlat4,b) = sFlat4,
inference(step,[status(thm)],[t3199,t89]) ).
cnf(t3212,plain,
least_upper_bound(sFlat4,b) = sFlat4,
inference(orient,[status(thm)],[t4103]) ).
cnf(t3216,plain,
least_upper_bound(sFlat4,least_upper_bound(b,X1)) = least_upper_bound(sFlat4,X1),
inference(cp,[status(thm)],[t94,t3212]) ).
cnf(t3450,plain,
least_upper_bound(sFlat4,least_upper_bound(b,X1)) = least_upper_bound(sFlat4,X1),
inference(orient,[status(thm)],[t3216]) ).
cnf(t4124,plain,
least_upper_bound(sFlat4,X1) = least_upper_bound(sFlat4,least_upper_bound(sFlat3,X1)),
inference(step,[status(thm)],[t3479,t3450]) ).
cnf(t3770,plain,
least_upper_bound(sFlat4,least_upper_bound(sFlat3,X1)) = least_upper_bound(sFlat4,X1),
inference(orient,[status(thm)],[t4124]) ).
cnf(t4084,plain,
least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t1271,t3164]) ).
cnf(t3165,plain,
least_upper_bound(sFlat3,least_upper_bound(sFlat0,sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t4084]) ).
cnf(t3775,plain,
least_upper_bound(sFlat4,least_upper_bound(sFlat0,sFlat2)) = least_upper_bound(sFlat4,sFlat4),
inference(cp,[status(thm)],[t3770,t3165]) ).
cnf(t4125,plain,
least_upper_bound(sFlat4,least_upper_bound(sFlat0,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t3775,t25]) ).
cnf(t3792,plain,
least_upper_bound(sFlat4,least_upper_bound(sFlat0,sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t4125]) ).
cnf(t197,plain,
least_upper_bound(X1,X2) = least_upper_bound(least_upper_bound(X1,X2),X1),
inference(cp,[status(thm)],[t195,t28]) ).
cnf(t3948,plain,
least_upper_bound(X1,X2) = least_upper_bound(X1,least_upper_bound(X2,X1)),
inference(step,[status(thm)],[t197,t94]) ).
cnf(t471,plain,
least_upper_bound(X1,least_upper_bound(X2,X1)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t3948]) ).
cnf(t302,plain,
least_upper_bound(sFlat2,greatest_lower_bound(a,X1)) = least_upper_bound(identity,a),
inference(cp,[status(thm)],[t299,t26]) ).
cnf(t3940,plain,
least_upper_bound(sFlat2,greatest_lower_bound(a,X1)) = sFlat2,
inference(step,[status(thm)],[t302,t110]) ).
cnf(t309,plain,
least_upper_bound(sFlat2,greatest_lower_bound(a,X1)) = sFlat2,
inference(orient,[status(thm)],[t3940]) ).
cnf(t311,plain,
greatest_lower_bound(a,X1) = greatest_lower_bound(greatest_lower_bound(a,X1),sFlat2),
inference(cp,[status(thm)],[t167,t309]) ).
cnf(t3955,plain,
greatest_lower_bound(a,X1) = greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)),
inference(step,[status(thm)],[t311,t121]) ).
cnf(t586,plain,
greatest_lower_bound(a,greatest_lower_bound(X1,sFlat2)) = greatest_lower_bound(a,X1),
inference(orient,[status(thm)],[t3955]) ).
cnf(t589,plain,
greatest_lower_bound(a,X1) = greatest_lower_bound(a,greatest_lower_bound(sFlat2,X1)),
inference(cp,[status(thm)],[t586,t117]) ).
cnf(t773,plain,
greatest_lower_bound(a,greatest_lower_bound(sFlat2,X1)) = greatest_lower_bound(a,X1),
inference(orient,[status(thm)],[t589]) ).
cnf(t776,plain,
greatest_lower_bound(a,least_upper_bound(sFlat2,X1)) = greatest_lower_bound(a,sFlat2),
inference(cp,[status(thm)],[t773,t28]) ).
cnf(t3983,plain,
greatest_lower_bound(a,least_upper_bound(sFlat2,X1)) = greatest_lower_bound(sFlat2,a),
inference(step,[status(thm)],[t776,t117]) ).
cnf(t172,plain,
a = greatest_lower_bound(a,sFlat2),
inference(cp,[status(thm)],[t167,t110]) ).
cnf(t3931,plain,
a = greatest_lower_bound(sFlat2,a),
inference(step,[status(thm)],[t172,t117]) ).
cnf(t177,plain,
greatest_lower_bound(sFlat2,a) = a,
inference(orient,[status(thm)],[t3931]) ).
cnf(t3984,plain,
greatest_lower_bound(a,least_upper_bound(sFlat2,X1)) = a,
inference(step,[status(thm)],[t3983,t177]) ).
cnf(t864,plain,
greatest_lower_bound(a,least_upper_bound(sFlat2,X1)) = a,
inference(orient,[status(thm)],[t3984]) ).
cnf(t308,plain,
identity = greatest_lower_bound(identity,least_upper_bound(sFlat2,X1)),
inference(cp,[status(thm)],[t28,t299]) ).
cnf(t317,plain,
greatest_lower_bound(identity,least_upper_bound(sFlat2,X1)) = identity,
inference(orient,[status(thm)],[t308]) ).
cnf(t327,plain,
least_upper_bound(sFlat2,X1) = least_upper_bound(least_upper_bound(sFlat2,X1),identity),
inference(cp,[status(thm)],[t195,t317]) ).
cnf(t3956,plain,
least_upper_bound(sFlat2,X1) = least_upper_bound(sFlat2,least_upper_bound(X1,identity)),
inference(step,[status(thm)],[t327,t94]) ).
cnf(t592,plain,
least_upper_bound(sFlat2,least_upper_bound(X1,identity)) = least_upper_bound(sFlat2,X1),
inference(orient,[status(thm)],[t3956]) ).
cnf(t268,plain,
multiply(least_upper_bound(identity,a),b) = least_upper_bound(b,sFlat0),
inference(cp,[status(thm)],[t263,t79]) ).
cnf(t3938,plain,
multiply(sFlat2,b) = least_upper_bound(b,sFlat0),
inference(step,[status(thm)],[t268,t110]) ).
cnf(t3939,plain,
multiply(sFlat2,b) = least_upper_bound(sFlat0,b),
inference(step,[status(thm)],[t3938,t89]) ).
cnf(t276,plain,
least_upper_bound(sFlat0,b) = multiply(sFlat2,b),
inference(orient,[status(thm)],[t3939]) ).
cnf(t279,plain,
least_upper_bound(sFlat0,least_upper_bound(b,X1)) = least_upper_bound(multiply(sFlat2,b),X1),
inference(cp,[status(thm)],[t94,t276]) ).
cnf(t1453,plain,
least_upper_bound(multiply(sFlat2,b),X1) = least_upper_bound(sFlat0,least_upper_bound(b,X1)),
inference(orient,[status(thm)],[t279]) ).
cnf(t1471,plain,
least_upper_bound(sFlat2,multiply(sFlat2,b)) = least_upper_bound(sFlat2,least_upper_bound(sFlat0,least_upper_bound(b,identity))),
inference(cp,[status(thm)],[t592,t1453]) ).
cnf(t165,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t31,t162]) ).
cnf(t1360,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(identity,X2)),
inference(orient,[status(thm)],[t165]) ).
cnf(t4022,plain,
multiply(sFlat2,least_upper_bound(identity,b)) = least_upper_bound(sFlat2,least_upper_bound(sFlat0,least_upper_bound(b,identity))),
inference(step,[status(thm)],[t1471,t1360]) ).
cnf(t4023,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(sFlat2,least_upper_bound(sFlat0,least_upper_bound(b,identity))),
inference(step,[status(thm)],[t4022,t114]) ).
cnf(t235,plain,
least_upper_bound(sFlat1,X1) = least_upper_bound(sFlat0,least_upper_bound(X1,identity)),
inference(cp,[status(thm)],[t229,t89]) ).
cnf(t505,plain,
least_upper_bound(sFlat0,least_upper_bound(X1,identity)) = least_upper_bound(sFlat1,X1),
inference(orient,[status(thm)],[t235]) ).
cnf(t4024,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(sFlat2,least_upper_bound(sFlat1,b)),
inference(step,[status(thm)],[t4023,t505]) ).
cnf(t231,plain,
least_upper_bound(sFlat1,b) = least_upper_bound(sFlat0,sFlat3),
inference(cp,[status(thm)],[t229,t114]) ).
cnf(t244,plain,
least_upper_bound(sFlat1,b) = least_upper_bound(sFlat0,sFlat3),
inference(orient,[status(thm)],[t231]) ).
cnf(t4025,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(sFlat2,least_upper_bound(sFlat0,sFlat3)),
inference(step,[status(thm)],[t4024,t244]) ).
cnf(t1479,plain,
least_upper_bound(sFlat2,least_upper_bound(sFlat0,sFlat3)) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t4025]) ).
cnf(t1480,plain,
a = greatest_lower_bound(a,multiply(sFlat2,sFlat3)),
inference(cp,[status(thm)],[t864,t1479]) ).
cnf(t1486,plain,
greatest_lower_bound(a,multiply(sFlat2,sFlat3)) = a,
inference(orient,[status(thm)],[t1480]) ).
cnf(t1487,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(multiply(sFlat2,sFlat3),a),
inference(cp,[status(thm)],[t195,t1486]) ).
cnf(t4026,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(a,multiply(sFlat2,sFlat3)),
inference(step,[status(thm)],[t1487,t89]) ).
cnf(t1489,plain,
least_upper_bound(a,multiply(sFlat2,sFlat3)) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t4026]) ).
cnf(t4092,plain,
least_upper_bound(a,sFlat4) = multiply(sFlat2,sFlat3),
inference(step,[status(thm)],[t1489,t3164]) ).
cnf(t4093,plain,
least_upper_bound(a,sFlat4) = sFlat4,
inference(step,[status(thm)],[t4092,t3164]) ).
cnf(t3197,plain,
least_upper_bound(a,sFlat4) = sFlat4,
inference(rw,[status(thm)],[t4093]) ).
cnf(t4101,plain,
least_upper_bound(sFlat4,a) = sFlat4,
inference(step,[status(thm)],[t3197,t89]) ).
cnf(t3203,plain,
least_upper_bound(sFlat4,a) = sFlat4,
inference(orient,[status(thm)],[t4101]) ).
cnf(t3205,plain,
least_upper_bound(sFlat2,sFlat4) = least_upper_bound(identity,sFlat4),
inference(cp,[status(thm)],[t534,t3203]) ).
cnf(t4107,plain,
least_upper_bound(sFlat2,sFlat4) = least_upper_bound(sFlat4,identity),
inference(step,[status(thm)],[t3205,t89]) ).
cnf(t4108,plain,
least_upper_bound(sFlat2,sFlat4) = sFlat4,
inference(step,[status(thm)],[t4107,t3217]) ).
cnf(t3240,plain,
least_upper_bound(sFlat2,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t4108]) ).
cnf(t3245,plain,
least_upper_bound(sFlat2,least_upper_bound(sFlat4,X1)) = least_upper_bound(sFlat4,X1),
inference(cp,[status(thm)],[t94,t3240]) ).
cnf(t3505,plain,
least_upper_bound(sFlat2,least_upper_bound(sFlat4,X1)) = least_upper_bound(sFlat4,X1),
inference(orient,[status(thm)],[t3245]) ).
cnf(t3514,plain,
least_upper_bound(least_upper_bound(sFlat4,X1),sFlat2) = least_upper_bound(least_upper_bound(sFlat4,X1),least_upper_bound(sFlat4,X1)),
inference(cp,[status(thm)],[t471,t3505]) ).
cnf(t4133,plain,
least_upper_bound(sFlat4,least_upper_bound(X1,sFlat2)) = least_upper_bound(least_upper_bound(sFlat4,X1),least_upper_bound(sFlat4,X1)),
inference(step,[status(thm)],[t3514,t94]) ).
cnf(t4134,plain,
least_upper_bound(sFlat4,least_upper_bound(X1,sFlat2)) = least_upper_bound(sFlat4,least_upper_bound(X1,least_upper_bound(sFlat4,X1))),
inference(step,[status(thm)],[t4133,t94]) ).
cnf(t4135,plain,
least_upper_bound(sFlat4,least_upper_bound(X1,sFlat2)) = least_upper_bound(sFlat4,least_upper_bound(X1,sFlat4)),
inference(step,[status(thm)],[t4134,t471]) ).
cnf(t4136,plain,
least_upper_bound(sFlat4,least_upper_bound(X1,sFlat2)) = least_upper_bound(sFlat4,X1),
inference(step,[status(thm)],[t4135,t471]) ).
cnf(t3891,plain,
least_upper_bound(sFlat4,least_upper_bound(X1,sFlat2)) = least_upper_bound(sFlat4,X1),
inference(orient,[status(thm)],[t4136]) ).
cnf(t4137,plain,
least_upper_bound(sFlat4,sFlat0) = sFlat4,
inference(step,[status(thm)],[t3792,t3891]) ).
cnf(t3903,plain,
least_upper_bound(sFlat4,sFlat0) = sFlat4,
inference(rw,[status(thm)],[t4137]) ).
cnf(t4138,plain,
least_upper_bound(sFlat0,sFlat4) = sFlat4,
inference(step,[status(thm)],[t3903,t89]) ).
cnf(t3904,plain,
least_upper_bound(sFlat0,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t4138]) ).
cnf(t4141,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat4,
inference(step,[status(thm)],[t3235,t3904]) ).
cnf(t3907,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t4141]) ).
cnf(goal_0,negated_conjecture,
least_upper_bound(least_upper_bound(multiply(a,b),identity),multiply(least_upper_bound(a,identity),least_upper_bound(b,identity))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
least_upper_bound(multiply(a,b),least_upper_bound(identity,multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[goal_0,t94]) ).
cnf(g0_1,plain,
least_upper_bound(sFlat0,least_upper_bound(identity,multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_0,t79]) ).
cnf(g0_2,plain,
least_upper_bound(sFlat1,multiply(least_upper_bound(a,identity),least_upper_bound(b,identity))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_1,t229]) ).
cnf(g0_3,plain,
least_upper_bound(sFlat1,multiply(least_upper_bound(identity,a),least_upper_bound(b,identity))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_2,t89]) ).
cnf(g0_4,plain,
least_upper_bound(sFlat1,multiply(sFlat2,least_upper_bound(b,identity))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_3,t110]) ).
cnf(g0_5,plain,
least_upper_bound(sFlat1,multiply(sFlat2,least_upper_bound(identity,b))) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_4,t89]) ).
cnf(g0_6,plain,
least_upper_bound(sFlat1,multiply(sFlat2,sFlat3)) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_5,t114]) ).
cnf(g0_7,plain,
least_upper_bound(sFlat1,sFlat4) != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_6,t3164]) ).
cnf(g0_8,plain,
sFlat4 != multiply(least_upper_bound(a,identity),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_7,t3907]) ).
cnf(g0_9,plain,
sFlat4 != multiply(least_upper_bound(identity,a),least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_8,t89]) ).
cnf(g0_10,plain,
sFlat4 != multiply(sFlat2,least_upper_bound(b,identity)),
inference(rw,[status(thm)],[g0_9,t110]) ).
cnf(g0_11,plain,
sFlat4 != multiply(sFlat2,least_upper_bound(identity,b)),
inference(rw,[status(thm)],[g0_10,t89]) ).
cnf(g0_12,plain,
sFlat4 != multiply(sFlat2,sFlat3),
inference(rw,[status(thm)],[g0_11,t114]) ).
cnf(g0_13,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_12,t3164]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP185-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 14:08:11 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.59/1.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.59/1.57 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------