%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP177-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:25:33 PM UTC 2026
% Result : Unsatisfiable 107.41s 16.41s
% Output : CNFRefutation 107.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 24
% Syntax : Number of clauses : 276 ( 276 unt; 0 nHn; 134 RR)
% Number of literals : 276 ( 275 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 : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 230 ( 31 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t18,axiom,
sFlat0 = multiply(b,c),
introduced(definition) ).
cnf(t54,plain,
multiply(b,c) = sFlat0,
inference(orient,[status(thm)],[t18]) ).
cnf(t7,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t74,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t19,axiom,
sFlat1 = greatest_lower_bound(a,multiply(b,c)),
introduced(definition) ).
cnf(t35817,plain,
sFlat1 = greatest_lower_bound(a,sFlat0),
inference(step,[status(thm)],[t19,t54]) ).
cnf(t35818,plain,
sFlat1 = greatest_lower_bound(sFlat0,a),
inference(step,[status(thm)],[t35817,t74]) ).
cnf(t86,plain,
greatest_lower_bound(sFlat0,a) = sFlat1,
inference(orient,[status(thm)],[t35818]) ).
cnf(t20,axiom,
sFlat2 = greatest_lower_bound(a,b),
introduced(definition) ).
cnf(t35819,plain,
sFlat2 = greatest_lower_bound(b,a),
inference(step,[status(thm)],[t20,t74]) ).
cnf(t89,plain,
greatest_lower_bound(b,a) = sFlat2,
inference(orient,[status(thm)],[t35819]) ).
cnf(t21,axiom,
sFlat3 = greatest_lower_bound(a,c),
introduced(definition) ).
cnf(t35820,plain,
sFlat3 = greatest_lower_bound(c,a),
inference(step,[status(thm)],[t21,t74]) ).
cnf(t92,plain,
greatest_lower_bound(c,a) = sFlat3,
inference(orient,[status(thm)],[t35820]) ).
cnf(t8,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
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(t96,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(t9,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t95,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t99,plain,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(X3,least_upper_bound(X1,X2)),
inference(cp,[status(thm)],[t96,t95]) ).
cnf(t254,plain,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(X3,least_upper_bound(X1,X2)),
inference(orient,[status(thm)],[t99]) ).
cnf(t261,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,least_upper_bound(X3,X1))),
inference(cp,[status(thm)],[t26,t254]) ).
cnf(t1424,plain,
greatest_lower_bound(X1,least_upper_bound(X2,least_upper_bound(X3,X1))) = X1,
inference(orient,[status(thm)],[t261]) ).
cnf(t1,axiom,
least_upper_bound(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
least_upper_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t100,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(cp,[status(thm)],[t96,t27]) ).
cnf(t144,plain,
least_upper_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t100]) ).
cnf(t1426,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,X1)),
inference(cp,[status(thm)],[t1424,t144]) ).
cnf(t1522,plain,
greatest_lower_bound(X1,least_upper_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t1426]) ).
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(t32,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t22,axiom,
sFlat4 = multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
introduced(definition) ).
cnf(t39,plain,
multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)) = sFlat4,
inference(orient,[status(thm)],[t22]) ).
cnf(t42,plain,
multiply(greatest_lower_bound(a,b),least_upper_bound(greatest_lower_bound(a,c),X1)) = least_upper_bound(sFlat4,multiply(greatest_lower_bound(a,b),X1)),
inference(cp,[status(thm)],[t32,t39]) ).
cnf(t35957,plain,
multiply(greatest_lower_bound(b,a),least_upper_bound(greatest_lower_bound(a,c),X1)) = least_upper_bound(sFlat4,multiply(greatest_lower_bound(a,b),X1)),
inference(step,[status(thm)],[t42,t74]) ).
cnf(t35958,plain,
multiply(sFlat2,least_upper_bound(greatest_lower_bound(a,c),X1)) = least_upper_bound(sFlat4,multiply(greatest_lower_bound(a,b),X1)),
inference(step,[status(thm)],[t35957,t89]) ).
cnf(t35959,plain,
multiply(sFlat2,least_upper_bound(greatest_lower_bound(c,a),X1)) = least_upper_bound(sFlat4,multiply(greatest_lower_bound(a,b),X1)),
inference(step,[status(thm)],[t35958,t74]) ).
cnf(t35960,plain,
multiply(sFlat2,least_upper_bound(sFlat3,X1)) = least_upper_bound(sFlat4,multiply(greatest_lower_bound(a,b),X1)),
inference(step,[status(thm)],[t35959,t92]) ).
cnf(t35961,plain,
multiply(sFlat2,least_upper_bound(sFlat3,X1)) = least_upper_bound(sFlat4,multiply(greatest_lower_bound(b,a),X1)),
inference(step,[status(thm)],[t35960,t74]) ).
cnf(t35962,plain,
multiply(sFlat2,least_upper_bound(sFlat3,X1)) = least_upper_bound(sFlat4,multiply(sFlat2,X1)),
inference(step,[status(thm)],[t35961,t89]) ).
cnf(t1718,plain,
least_upper_bound(sFlat4,multiply(sFlat2,X1)) = multiply(sFlat2,least_upper_bound(sFlat3,X1)),
inference(orient,[status(thm)],[t35962]) ).
cnf(t13,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t6,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t64,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t6]) ).
cnf(t73,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t29,t64]) ).
cnf(t5,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t35843,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t73,t24]) ).
cnf(t275,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t35843]) ).
cnf(t276,plain,
X1 = multiply(inverse(inverse(X1)),identity),
inference(cp,[status(thm)],[t275,t64]) ).
cnf(t310,plain,
multiply(inverse(inverse(X1)),identity) = X1,
inference(orient,[status(thm)],[t276]) ).
cnf(t281,plain,
multiply(X1,X2) = multiply(inverse(inverse(X1)),X2),
inference(cp,[status(thm)],[t275,t275]) ).
cnf(t340,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t281]) ).
cnf(t35844,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t310,t340]) ).
cnf(t349,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[t35844]) ).
cnf(t350,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t349]) ).
cnf(t1720,plain,
multiply(sFlat2,least_upper_bound(sFlat3,identity)) = least_upper_bound(sFlat4,sFlat2),
inference(cp,[status(thm)],[t1718,t350]) ).
cnf(t10,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t10]) ).
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(t76,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(t4,axiom,
least_upper_bound(identity,c) = c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t115,plain,
least_upper_bound(identity,c) = c,
inference(orient,[status(thm)],[t4]) ).
cnf(t116,plain,
identity = greatest_lower_bound(identity,c),
inference(cp,[status(thm)],[t26,t115]) ).
cnf(t132,plain,
greatest_lower_bound(identity,c) = identity,
inference(orient,[status(thm)],[t116]) ).
cnf(t133,plain,
greatest_lower_bound(identity,greatest_lower_bound(c,X1)) = greatest_lower_bound(identity,X1),
inference(cp,[status(thm)],[t76,t132]) ).
cnf(t438,plain,
greatest_lower_bound(identity,greatest_lower_bound(c,X1)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t133]) ).
cnf(t439,plain,
greatest_lower_bound(identity,a) = greatest_lower_bound(identity,sFlat3),
inference(cp,[status(thm)],[t438,t92]) ).
cnf(t2,axiom,
least_upper_bound(identity,a) = a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t109,plain,
least_upper_bound(identity,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t110,plain,
identity = greatest_lower_bound(identity,a),
inference(cp,[status(thm)],[t26,t109]) ).
cnf(t128,plain,
greatest_lower_bound(identity,a) = identity,
inference(orient,[status(thm)],[t110]) ).
cnf(t35849,plain,
identity = greatest_lower_bound(identity,sFlat3),
inference(step,[status(thm)],[t439,t128]) ).
cnf(t35850,plain,
identity = greatest_lower_bound(sFlat3,identity),
inference(step,[status(thm)],[t35849,t74]) ).
cnf(t442,plain,
greatest_lower_bound(sFlat3,identity) = identity,
inference(orient,[status(thm)],[t35850]) ).
cnf(t443,plain,
sFlat3 = least_upper_bound(sFlat3,identity),
inference(cp,[status(thm)],[t28,t442]) ).
cnf(t444,plain,
least_upper_bound(sFlat3,identity) = sFlat3,
inference(orient,[status(thm)],[t443]) ).
cnf(t35963,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(sFlat4,sFlat2),
inference(step,[status(thm)],[t1720,t444]) ).
cnf(t35964,plain,
multiply(sFlat2,sFlat3) = least_upper_bound(sFlat2,sFlat4),
inference(step,[status(thm)],[t35963,t95]) ).
cnf(t1726,plain,
least_upper_bound(sFlat2,sFlat4) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t35964]) ).
cnf(t1727,plain,
sFlat4 = greatest_lower_bound(sFlat4,multiply(sFlat2,sFlat3)),
inference(cp,[status(thm)],[t1522,t1726]) ).
cnf(t15,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t40,plain,
multiply(greatest_lower_bound(greatest_lower_bound(a,b),X1),greatest_lower_bound(a,c)) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(a,c))),
inference(cp,[status(thm)],[t33,t39]) ).
cnf(t35925,plain,
multiply(greatest_lower_bound(a,greatest_lower_bound(b,X1)),greatest_lower_bound(a,c)) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t40,t76]) ).
cnf(t84,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(greatest_lower_bound(X2,X1),X3),
inference(cp,[status(thm)],[t76,t74]) ).
cnf(t35841,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X2,greatest_lower_bound(X1,X3)),
inference(step,[status(thm)],[t84,t76]) ).
cnf(t250,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X2,greatest_lower_bound(X1,X3)),
inference(orient,[status(thm)],[t35841]) ).
cnf(t35926,plain,
multiply(greatest_lower_bound(b,greatest_lower_bound(a,X1)),greatest_lower_bound(a,c)) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35925,t250]) ).
cnf(t90,plain,
greatest_lower_bound(b,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat2,X1),
inference(cp,[status(thm)],[t76,t89]) ).
cnf(t168,plain,
greatest_lower_bound(b,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat2,X1),
inference(orient,[status(thm)],[t90]) ).
cnf(t35927,plain,
multiply(greatest_lower_bound(sFlat2,X1),greatest_lower_bound(a,c)) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35926,t168]) ).
cnf(t35928,plain,
multiply(greatest_lower_bound(sFlat2,X1),greatest_lower_bound(c,a)) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35927,t74]) ).
cnf(t35929,plain,
multiply(greatest_lower_bound(sFlat2,X1),sFlat3) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35928,t92]) ).
cnf(t35930,plain,
multiply(greatest_lower_bound(sFlat2,X1),sFlat3) = greatest_lower_bound(sFlat4,multiply(X1,greatest_lower_bound(c,a))),
inference(step,[status(thm)],[t35929,t74]) ).
cnf(t35931,plain,
multiply(greatest_lower_bound(sFlat2,X1),sFlat3) = greatest_lower_bound(sFlat4,multiply(X1,sFlat3)),
inference(step,[status(thm)],[t35930,t92]) ).
cnf(t1348,plain,
greatest_lower_bound(sFlat4,multiply(X1,sFlat3)) = multiply(greatest_lower_bound(sFlat2,X1),sFlat3),
inference(orient,[status(thm)],[t35931]) ).
cnf(t35965,plain,
sFlat4 = multiply(greatest_lower_bound(sFlat2,sFlat2),sFlat3),
inference(step,[status(thm)],[t1727,t1348]) ).
cnf(t0,axiom,
greatest_lower_bound(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
greatest_lower_bound(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t35966,plain,
sFlat4 = multiply(sFlat2,sFlat3),
inference(step,[status(thm)],[t35965,t25]) ).
cnf(t1729,plain,
multiply(sFlat2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t35966]) ).
cnf(t23,axiom,
sFlat5 = least_upper_bound(greatest_lower_bound(a,multiply(b,c)),multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))),
introduced(definition) ).
cnf(t35821,plain,
sFlat5 = least_upper_bound(greatest_lower_bound(a,sFlat0),multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t23,t54]) ).
cnf(t35822,plain,
sFlat5 = least_upper_bound(greatest_lower_bound(sFlat0,a),multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35821,t74]) ).
cnf(t35823,plain,
sFlat5 = least_upper_bound(sFlat1,multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35822,t86]) ).
cnf(t35824,plain,
sFlat5 = least_upper_bound(sFlat1,multiply(greatest_lower_bound(b,a),greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35823,t74]) ).
cnf(t35825,plain,
sFlat5 = least_upper_bound(sFlat1,multiply(sFlat2,greatest_lower_bound(a,c))),
inference(step,[status(thm)],[t35824,t89]) ).
cnf(t35826,plain,
sFlat5 = least_upper_bound(sFlat1,multiply(sFlat2,greatest_lower_bound(c,a))),
inference(step,[status(thm)],[t35825,t74]) ).
cnf(t35827,plain,
sFlat5 = least_upper_bound(sFlat1,multiply(sFlat2,sFlat3)),
inference(step,[status(thm)],[t35826,t92]) ).
cnf(t106,plain,
least_upper_bound(sFlat1,multiply(sFlat2,sFlat3)) = sFlat5,
inference(orient,[status(thm)],[t35827]) ).
cnf(t35971,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat5,
inference(step,[status(thm)],[t106,t1729]) ).
cnf(t1745,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t35971]) ).
cnf(t1746,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t1745]) ).
cnf(t79,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X3,greatest_lower_bound(X1,X2)),
inference(cp,[status(thm)],[t76,t74]) ).
cnf(t242,plain,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(X3,greatest_lower_bound(X1,X2)),
inference(orient,[status(thm)],[t79]) ).
cnf(t249,plain,
X1 = least_upper_bound(X1,greatest_lower_bound(X2,greatest_lower_bound(X3,X1))),
inference(cp,[status(thm)],[t28,t242]) ).
cnf(t1232,plain,
least_upper_bound(X1,greatest_lower_bound(X2,greatest_lower_bound(X3,X1))) = X1,
inference(orient,[status(thm)],[t249]) ).
cnf(t80,plain,
greatest_lower_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,X2),
inference(cp,[status(thm)],[t76,t25]) ).
cnf(t138,plain,
greatest_lower_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t80]) ).
cnf(t1234,plain,
X1 = least_upper_bound(X1,greatest_lower_bound(X2,X1)),
inference(cp,[status(thm)],[t1232,t138]) ).
cnf(t1312,plain,
least_upper_bound(X1,greatest_lower_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t1234]) ).
cnf(t87,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(cp,[status(thm)],[t76,t86]) ).
cnf(t159,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t87]) ).
cnf(t161,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat0,greatest_lower_bound(a,X1)),
inference(cp,[status(thm)],[t159,t138]) ).
cnf(t35851,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(step,[status(thm)],[t161,t159]) ).
cnf(t445,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t35851]) ).
cnf(t14,axiom,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t290,plain,
multiply(inverse(X1),greatest_lower_bound(X2,multiply(X1,X3))) = greatest_lower_bound(multiply(inverse(X1),X2),X3),
inference(cp,[status(thm)],[t30,t275]) ).
cnf(t27885,plain,
multiply(inverse(X1),greatest_lower_bound(X2,multiply(X1,X3))) = greatest_lower_bound(multiply(inverse(X1),X2),X3),
inference(orient,[status(thm)],[t290]) ).
cnf(t93,plain,
greatest_lower_bound(c,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat3,X1),
inference(cp,[status(thm)],[t76,t92]) ).
cnf(t177,plain,
greatest_lower_bound(c,greatest_lower_bound(a,X1)) = greatest_lower_bound(sFlat3,X1),
inference(orient,[status(thm)],[t93]) ).
cnf(t34,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t33,t24]) ).
cnf(t207,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(identity,X2),X1),
inference(orient,[status(thm)],[t34]) ).
cnf(t216,plain,
greatest_lower_bound(sFlat3,multiply(X1,a)) = greatest_lower_bound(c,multiply(greatest_lower_bound(identity,X1),a)),
inference(cp,[status(thm)],[t177,t207]) ).
cnf(t10072,plain,
greatest_lower_bound(c,multiply(greatest_lower_bound(identity,X1),a)) = greatest_lower_bound(sFlat3,multiply(X1,a)),
inference(orient,[status(thm)],[t216]) ).
cnf(t71,plain,
multiply(inverse(X1),greatest_lower_bound(X1,X2)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t30,t64]) ).
cnf(t1026,plain,
multiply(inverse(X1),greatest_lower_bound(X1,X2)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t71]) ).
cnf(t1039,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = multiply(greatest_lower_bound(identity,inverse(X1)),identity),
inference(cp,[status(thm)],[t1026,t207]) ).
cnf(t35977,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(step,[status(thm)],[t1039,t350]) ).
cnf(t1794,plain,
multiply(inverse(X1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(identity,inverse(X1)),
inference(orient,[status(thm)],[t35977]) ).
cnf(t3,axiom,
least_upper_bound(identity,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t112,plain,
least_upper_bound(identity,b) = b,
inference(orient,[status(thm)],[t3]) ).
cnf(t113,plain,
identity = greatest_lower_bound(identity,b),
inference(cp,[status(thm)],[t26,t112]) ).
cnf(t130,plain,
greatest_lower_bound(identity,b) = identity,
inference(orient,[status(thm)],[t113]) ).
cnf(t131,plain,
greatest_lower_bound(identity,greatest_lower_bound(b,X1)) = greatest_lower_bound(identity,X1),
inference(cp,[status(thm)],[t76,t130]) ).
cnf(t431,plain,
greatest_lower_bound(identity,greatest_lower_bound(b,X1)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t131]) ).
cnf(t432,plain,
greatest_lower_bound(identity,a) = greatest_lower_bound(identity,sFlat2),
inference(cp,[status(thm)],[t431,t89]) ).
cnf(t35847,plain,
identity = greatest_lower_bound(identity,sFlat2),
inference(step,[status(thm)],[t432,t128]) ).
cnf(t35848,plain,
identity = greatest_lower_bound(sFlat2,identity),
inference(step,[status(thm)],[t35847,t74]) ).
cnf(t435,plain,
greatest_lower_bound(sFlat2,identity) = identity,
inference(orient,[status(thm)],[t35848]) ).
cnf(t1797,plain,
greatest_lower_bound(identity,inverse(sFlat2)) = multiply(inverse(sFlat2),identity),
inference(cp,[status(thm)],[t1794,t435]) ).
cnf(t35979,plain,
greatest_lower_bound(identity,inverse(sFlat2)) = inverse(sFlat2),
inference(step,[status(thm)],[t1797,t350]) ).
cnf(t1826,plain,
greatest_lower_bound(identity,inverse(sFlat2)) = inverse(sFlat2),
inference(orient,[status(thm)],[t35979]) ).
cnf(t10161,plain,
greatest_lower_bound(sFlat3,multiply(inverse(sFlat2),a)) = greatest_lower_bound(c,multiply(inverse(sFlat2),a)),
inference(cp,[status(thm)],[t10072,t1826]) ).
cnf(t35656,plain,
greatest_lower_bound(c,multiply(inverse(sFlat2),a)) = greatest_lower_bound(sFlat3,multiply(inverse(sFlat2),a)),
inference(orient,[status(thm)],[t10161]) ).
cnf(t35660,plain,
greatest_lower_bound(multiply(inverse(inverse(sFlat2)),c),a) = multiply(inverse(inverse(sFlat2)),greatest_lower_bound(sFlat3,multiply(inverse(sFlat2),a))),
inference(cp,[status(thm)],[t27885,t35656]) ).
cnf(t35667,plain,
greatest_lower_bound(a,multiply(sFlat2,c)) = greatest_lower_bound(sFlat4,a),
inference(orient,[status(thm)],[t35660]) ).
cnf(t35673,plain,
greatest_lower_bound(sFlat1,multiply(sFlat2,c)) = greatest_lower_bound(sFlat1,greatest_lower_bound(sFlat4,a)),
inference(cp,[status(thm)],[t445,t35667]) ).
cnf(t85,plain,
greatest_lower_bound(X1,X2) = least_upper_bound(greatest_lower_bound(X1,X2),greatest_lower_bound(X1,greatest_lower_bound(X2,X3))),
inference(cp,[status(thm)],[t28,t76]) ).
cnf(t7278,plain,
least_upper_bound(greatest_lower_bound(X1,X2),greatest_lower_bound(X1,greatest_lower_bound(X2,X3))) = greatest_lower_bound(X1,X2),
inference(orient,[status(thm)],[t85]) ).
cnf(t163,plain,
greatest_lower_bound(sFlat1,X1) = greatest_lower_bound(sFlat0,greatest_lower_bound(X1,a)),
inference(cp,[status(thm)],[t159,t74]) ).
cnf(t447,plain,
greatest_lower_bound(sFlat0,greatest_lower_bound(X1,a)) = greatest_lower_bound(sFlat1,X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t7281,plain,
greatest_lower_bound(sFlat0,X1) = least_upper_bound(greatest_lower_bound(sFlat0,X1),greatest_lower_bound(sFlat1,X1)),
inference(cp,[status(thm)],[t7278,t447]) ).
cnf(t8963,plain,
least_upper_bound(greatest_lower_bound(sFlat0,X1),greatest_lower_bound(sFlat1,X1)) = greatest_lower_bound(sFlat0,X1),
inference(orient,[status(thm)],[t7281]) ).
cnf(t162,plain,
greatest_lower_bound(sFlat1,least_upper_bound(a,X1)) = greatest_lower_bound(sFlat0,a),
inference(cp,[status(thm)],[t159,t26]) ).
cnf(t35835,plain,
greatest_lower_bound(sFlat1,least_upper_bound(a,X1)) = sFlat1,
inference(step,[status(thm)],[t162,t86]) ).
cnf(t195,plain,
greatest_lower_bound(sFlat1,least_upper_bound(a,X1)) = sFlat1,
inference(orient,[status(thm)],[t35835]) ).
cnf(t354,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t32,t350]) ).
cnf(t730,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(identity,X2)),
inference(orient,[status(thm)],[t354]) ).
cnf(t759,plain,
sFlat1 = greatest_lower_bound(sFlat1,multiply(a,least_upper_bound(identity,X1))),
inference(cp,[status(thm)],[t195,t730]) ).
cnf(t12941,plain,
greatest_lower_bound(sFlat1,multiply(a,least_upper_bound(identity,X1))) = sFlat1,
inference(orient,[status(thm)],[t759]) ).
cnf(t13001,plain,
sFlat1 = greatest_lower_bound(sFlat1,multiply(a,c)),
inference(cp,[status(thm)],[t12941,t115]) ).
cnf(t13017,plain,
greatest_lower_bound(sFlat1,multiply(a,c)) = sFlat1,
inference(orient,[status(thm)],[t13001]) ).
cnf(t13018,plain,
greatest_lower_bound(sFlat0,multiply(a,c)) = least_upper_bound(greatest_lower_bound(sFlat0,multiply(a,c)),sFlat1),
inference(cp,[status(thm)],[t8963,t13017]) ).
cnf(t57,plain,
multiply(greatest_lower_bound(b,X1),c) = greatest_lower_bound(sFlat0,multiply(X1,c)),
inference(cp,[status(thm)],[t33,t54]) ).
cnf(t405,plain,
greatest_lower_bound(sFlat0,multiply(X1,c)) = multiply(greatest_lower_bound(b,X1),c),
inference(orient,[status(thm)],[t57]) ).
cnf(t36399,plain,
multiply(greatest_lower_bound(b,a),c) = least_upper_bound(greatest_lower_bound(sFlat0,multiply(a,c)),sFlat1),
inference(step,[status(thm)],[t13018,t405]) ).
cnf(t36400,plain,
multiply(sFlat2,c) = least_upper_bound(greatest_lower_bound(sFlat0,multiply(a,c)),sFlat1),
inference(step,[status(thm)],[t36399,t89]) ).
cnf(t36401,plain,
multiply(sFlat2,c) = least_upper_bound(sFlat1,greatest_lower_bound(sFlat0,multiply(a,c))),
inference(step,[status(thm)],[t36400,t95]) ).
cnf(t36402,plain,
multiply(sFlat2,c) = least_upper_bound(sFlat1,multiply(greatest_lower_bound(b,a),c)),
inference(step,[status(thm)],[t36401,t405]) ).
cnf(t36403,plain,
multiply(sFlat2,c) = least_upper_bound(sFlat1,multiply(sFlat2,c)),
inference(step,[status(thm)],[t36402,t89]) ).
cnf(t13031,plain,
least_upper_bound(sFlat1,multiply(sFlat2,c)) = multiply(sFlat2,c),
inference(orient,[status(thm)],[t36403]) ).
cnf(t13032,plain,
sFlat1 = greatest_lower_bound(sFlat1,multiply(sFlat2,c)),
inference(cp,[status(thm)],[t26,t13031]) ).
cnf(t13053,plain,
greatest_lower_bound(sFlat1,multiply(sFlat2,c)) = sFlat1,
inference(orient,[status(thm)],[t13032]) ).
cnf(t36943,plain,
sFlat1 = greatest_lower_bound(sFlat1,greatest_lower_bound(sFlat4,a)),
inference(step,[status(thm)],[t35673,t13053]) ).
cnf(t105,plain,
least_upper_bound(X1,X2) = greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(X1,least_upper_bound(X2,X3))),
inference(cp,[status(thm)],[t26,t96]) ).
cnf(t11174,plain,
greatest_lower_bound(least_upper_bound(X1,X2),least_upper_bound(X1,least_upper_bound(X2,X3))) = least_upper_bound(X1,X2),
inference(orient,[status(thm)],[t105]) ).
cnf(t111,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(a,X1),
inference(cp,[status(thm)],[t96,t109]) ).
cnf(t186,plain,
least_upper_bound(identity,least_upper_bound(a,X1)) = least_upper_bound(a,X1),
inference(orient,[status(thm)],[t111]) ).
cnf(t187,plain,
least_upper_bound(a,X1) = least_upper_bound(identity,least_upper_bound(X1,a)),
inference(cp,[status(thm)],[t186,t95]) ).
cnf(t511,plain,
least_upper_bound(identity,least_upper_bound(X1,a)) = least_upper_bound(a,X1),
inference(orient,[status(thm)],[t187]) ).
cnf(t11186,plain,
least_upper_bound(identity,X1) = greatest_lower_bound(least_upper_bound(identity,X1),least_upper_bound(a,X1)),
inference(cp,[status(thm)],[t11174,t511]) ).
cnf(t11430,plain,
greatest_lower_bound(least_upper_bound(identity,X1),least_upper_bound(a,X1)) = least_upper_bound(identity,X1),
inference(orient,[status(thm)],[t11186]) ).
cnf(t450,plain,
greatest_lower_bound(sFlat1,identity) = greatest_lower_bound(sFlat0,identity),
inference(cp,[status(thm)],[t447,t128]) ).
cnf(t457,plain,
greatest_lower_bound(sFlat1,identity) = greatest_lower_bound(sFlat0,identity),
inference(orient,[status(thm)],[t450]) ).
cnf(t117,plain,
least_upper_bound(identity,least_upper_bound(c,X1)) = least_upper_bound(c,X1),
inference(cp,[status(thm)],[t96,t115]) ).
cnf(t192,plain,
least_upper_bound(identity,least_upper_bound(c,X1)) = least_upper_bound(c,X1),
inference(orient,[status(thm)],[t117]) ).
cnf(t194,plain,
identity = greatest_lower_bound(identity,least_upper_bound(c,X1)),
inference(cp,[status(thm)],[t26,t192]) ).
cnf(t239,plain,
greatest_lower_bound(identity,least_upper_bound(c,X1)) = identity,
inference(orient,[status(thm)],[t194]) ).
cnf(t240,plain,
identity = greatest_lower_bound(identity,least_upper_bound(X1,c)),
inference(cp,[status(thm)],[t239,t95]) ).
cnf(t532,plain,
greatest_lower_bound(identity,least_upper_bound(X1,c)) = identity,
inference(orient,[status(thm)],[t240]) ).
cnf(t211,plain,
multiply(greatest_lower_bound(identity,b),c) = greatest_lower_bound(c,sFlat0),
inference(cp,[status(thm)],[t207,t54]) ).
cnf(t35837,plain,
multiply(identity,c) = greatest_lower_bound(c,sFlat0),
inference(step,[status(thm)],[t211,t130]) ).
cnf(t35838,plain,
c = greatest_lower_bound(c,sFlat0),
inference(step,[status(thm)],[t35837,t24]) ).
cnf(t35839,plain,
c = greatest_lower_bound(sFlat0,c),
inference(step,[status(thm)],[t35838,t74]) ).
cnf(t221,plain,
greatest_lower_bound(sFlat0,c) = c,
inference(orient,[status(thm)],[t35839]) ).
cnf(t223,plain,
sFlat0 = least_upper_bound(sFlat0,c),
inference(cp,[status(thm)],[t28,t221]) ).
cnf(t224,plain,
least_upper_bound(sFlat0,c) = sFlat0,
inference(orient,[status(thm)],[t223]) ).
cnf(t533,plain,
identity = greatest_lower_bound(identity,sFlat0),
inference(cp,[status(thm)],[t532,t224]) ).
cnf(t35865,plain,
identity = greatest_lower_bound(sFlat0,identity),
inference(step,[status(thm)],[t533,t74]) ).
cnf(t535,plain,
greatest_lower_bound(sFlat0,identity) = identity,
inference(orient,[status(thm)],[t35865]) ).
cnf(t35866,plain,
greatest_lower_bound(sFlat1,identity) = identity,
inference(step,[status(thm)],[t457,t535]) ).
cnf(t536,plain,
greatest_lower_bound(sFlat1,identity) = identity,
inference(orient,[status(thm)],[t35866]) ).
cnf(t7355,plain,
greatest_lower_bound(X1,sFlat1) = least_upper_bound(greatest_lower_bound(X1,sFlat1),greatest_lower_bound(X1,identity)),
inference(cp,[status(thm)],[t7278,t536]) ).
cnf(t33368,plain,
least_upper_bound(greatest_lower_bound(X1,sFlat1),greatest_lower_bound(X1,identity)) = greatest_lower_bound(X1,sFlat1),
inference(orient,[status(thm)],[t7355]) ).
cnf(t72,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(multiply(inverse(X1),X2),identity),
inference(cp,[status(thm)],[t30,t64]) ).
cnf(t35917,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t72,t74]) ).
cnf(t1049,plain,
multiply(inverse(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(identity,multiply(inverse(X1),X2)),
inference(orient,[status(thm)],[t35917]) ).
cnf(t440,plain,
greatest_lower_bound(identity,greatest_lower_bound(a,X1)) = greatest_lower_bound(identity,greatest_lower_bound(sFlat3,X1)),
inference(cp,[status(thm)],[t438,t177]) ).
cnf(t129,plain,
greatest_lower_bound(identity,greatest_lower_bound(a,X1)) = greatest_lower_bound(identity,X1),
inference(cp,[status(thm)],[t76,t128]) ).
cnf(t429,plain,
greatest_lower_bound(identity,greatest_lower_bound(a,X1)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t129]) ).
cnf(t35877,plain,
greatest_lower_bound(identity,X1) = greatest_lower_bound(identity,greatest_lower_bound(sFlat3,X1)),
inference(step,[status(thm)],[t440,t429]) ).
cnf(t35878,plain,
greatest_lower_bound(identity,X1) = greatest_lower_bound(sFlat3,greatest_lower_bound(identity,X1)),
inference(step,[status(thm)],[t35877,t250]) ).
cnf(t591,plain,
greatest_lower_bound(sFlat3,greatest_lower_bound(identity,X1)) = greatest_lower_bound(identity,X1),
inference(orient,[status(thm)],[t35878]) ).
cnf(t1833,plain,
greatest_lower_bound(identity,inverse(sFlat2)) = greatest_lower_bound(sFlat3,inverse(sFlat2)),
inference(cp,[status(thm)],[t591,t1826]) ).
cnf(t35982,plain,
inverse(sFlat2) = greatest_lower_bound(sFlat3,inverse(sFlat2)),
inference(step,[status(thm)],[t1833,t1826]) ).
cnf(t1861,plain,
greatest_lower_bound(sFlat3,inverse(sFlat2)) = inverse(sFlat2),
inference(orient,[status(thm)],[t35982]) ).
cnf(t1869,plain,
greatest_lower_bound(identity,multiply(inverse(inverse(sFlat2)),sFlat3)) = multiply(inverse(inverse(sFlat2)),inverse(sFlat2)),
inference(cp,[status(thm)],[t1049,t1861]) ).
cnf(t35983,plain,
greatest_lower_bound(identity,multiply(sFlat2,sFlat3)) = multiply(inverse(inverse(sFlat2)),inverse(sFlat2)),
inference(step,[status(thm)],[t1869,t340]) ).
cnf(t35984,plain,
greatest_lower_bound(identity,sFlat4) = multiply(inverse(inverse(sFlat2)),inverse(sFlat2)),
inference(step,[status(thm)],[t35983,t1729]) ).
cnf(t35985,plain,
greatest_lower_bound(sFlat4,identity) = multiply(inverse(inverse(sFlat2)),inverse(sFlat2)),
inference(step,[status(thm)],[t35984,t74]) ).
cnf(t35986,plain,
greatest_lower_bound(sFlat4,identity) = multiply(sFlat2,inverse(sFlat2)),
inference(step,[status(thm)],[t35985,t340]) ).
cnf(t341,plain,
multiply(X1,inverse(X1)) = identity,
inference(cp,[status(thm)],[t340,t64]) ).
cnf(t362,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t341]) ).
cnf(t35987,plain,
greatest_lower_bound(sFlat4,identity) = identity,
inference(step,[status(thm)],[t35986,t362]) ).
cnf(t1870,plain,
greatest_lower_bound(sFlat4,identity) = identity,
inference(orient,[status(thm)],[t35987]) ).
cnf(t33372,plain,
greatest_lower_bound(sFlat4,sFlat1) = least_upper_bound(greatest_lower_bound(sFlat4,sFlat1),identity),
inference(cp,[status(thm)],[t33368,t1870]) ).
cnf(t36903,plain,
greatest_lower_bound(sFlat1,sFlat4) = least_upper_bound(greatest_lower_bound(sFlat4,sFlat1),identity),
inference(step,[status(thm)],[t33372,t74]) ).
cnf(t36904,plain,
greatest_lower_bound(sFlat1,sFlat4) = least_upper_bound(identity,greatest_lower_bound(sFlat4,sFlat1)),
inference(step,[status(thm)],[t36903,t95]) ).
cnf(t36905,plain,
greatest_lower_bound(sFlat1,sFlat4) = least_upper_bound(identity,greatest_lower_bound(sFlat1,sFlat4)),
inference(step,[status(thm)],[t36904,t74]) ).
cnf(t33384,plain,
least_upper_bound(identity,greatest_lower_bound(sFlat1,sFlat4)) = greatest_lower_bound(sFlat1,sFlat4),
inference(orient,[status(thm)],[t36905]) ).
cnf(t33386,plain,
least_upper_bound(identity,greatest_lower_bound(sFlat1,sFlat4)) = greatest_lower_bound(greatest_lower_bound(sFlat1,sFlat4),least_upper_bound(a,greatest_lower_bound(sFlat1,sFlat4))),
inference(cp,[status(thm)],[t11430,t33384]) ).
cnf(t36906,plain,
greatest_lower_bound(sFlat1,sFlat4) = greatest_lower_bound(greatest_lower_bound(sFlat1,sFlat4),least_upper_bound(a,greatest_lower_bound(sFlat1,sFlat4))),
inference(step,[status(thm)],[t33386,t33384]) ).
cnf(t36907,plain,
greatest_lower_bound(sFlat1,sFlat4) = greatest_lower_bound(sFlat1,greatest_lower_bound(sFlat4,least_upper_bound(a,greatest_lower_bound(sFlat1,sFlat4)))),
inference(step,[status(thm)],[t36906,t76]) ).
cnf(t1238,plain,
a = least_upper_bound(a,greatest_lower_bound(sFlat1,X1)),
inference(cp,[status(thm)],[t1232,t447]) ).
cnf(t1382,plain,
least_upper_bound(a,greatest_lower_bound(sFlat1,X1)) = a,
inference(orient,[status(thm)],[t1238]) ).
cnf(t36908,plain,
greatest_lower_bound(sFlat1,sFlat4) = greatest_lower_bound(sFlat1,greatest_lower_bound(sFlat4,a)),
inference(step,[status(thm)],[t36907,t1382]) ).
cnf(t33435,plain,
greatest_lower_bound(sFlat1,greatest_lower_bound(sFlat4,a)) = greatest_lower_bound(sFlat1,sFlat4),
inference(orient,[status(thm)],[t36908]) ).
cnf(t36944,plain,
sFlat1 = greatest_lower_bound(sFlat1,sFlat4),
inference(step,[status(thm)],[t36943,t33435]) ).
cnf(t35684,plain,
greatest_lower_bound(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t36944]) ).
cnf(t35691,plain,
sFlat4 = least_upper_bound(sFlat4,sFlat1),
inference(cp,[status(thm)],[t1312,t35684]) ).
cnf(t36951,plain,
sFlat4 = least_upper_bound(sFlat1,sFlat4),
inference(step,[status(thm)],[t35691,t95]) ).
cnf(t36952,plain,
sFlat4 = sFlat5,
inference(step,[status(thm)],[t36951,t1746]) ).
cnf(t35697,plain,
sFlat5 = sFlat4,
inference(orient,[status(thm)],[t36952]) ).
cnf(t36953,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat4,
inference(step,[status(thm)],[t1746,t35697]) ).
cnf(t35698,plain,
least_upper_bound(sFlat1,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t36953]) ).
cnf(goal_0,negated_conjecture,
least_upper_bound(greatest_lower_bound(a,multiply(b,c)),multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
least_upper_bound(greatest_lower_bound(a,sFlat0),multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[goal_0,t54]) ).
cnf(g0_1,plain,
least_upper_bound(greatest_lower_bound(sFlat0,a),multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_0,t74]) ).
cnf(g0_2,plain,
least_upper_bound(sFlat1,multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_1,t86]) ).
cnf(g0_3,plain,
least_upper_bound(sFlat1,multiply(greatest_lower_bound(b,a),greatest_lower_bound(a,c))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_2,t74]) ).
cnf(g0_4,plain,
least_upper_bound(sFlat1,multiply(sFlat2,greatest_lower_bound(a,c))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_3,t89]) ).
cnf(g0_5,plain,
least_upper_bound(sFlat1,multiply(sFlat2,greatest_lower_bound(c,a))) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_4,t74]) ).
cnf(g0_6,plain,
least_upper_bound(sFlat1,multiply(sFlat2,sFlat3)) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_5,t92]) ).
cnf(g0_7,plain,
least_upper_bound(sFlat1,sFlat4) != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_6,t1729]) ).
cnf(g0_8,plain,
sFlat4 != multiply(greatest_lower_bound(a,b),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_7,t35698]) ).
cnf(g0_9,plain,
sFlat4 != multiply(greatest_lower_bound(b,a),greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_8,t74]) ).
cnf(g0_10,plain,
sFlat4 != multiply(sFlat2,greatest_lower_bound(a,c)),
inference(rw,[status(thm)],[g0_9,t89]) ).
cnf(g0_11,plain,
sFlat4 != multiply(sFlat2,greatest_lower_bound(c,a)),
inference(rw,[status(thm)],[g0_10,t74]) ).
cnf(g0_12,plain,
sFlat4 != multiply(sFlat2,sFlat3),
inference(rw,[status(thm)],[g0_11,t92]) ).
cnf(g0_13,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_12,t1729]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP177-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.34 % Computer : n005.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Wed Sep 23 13:58:47 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 107.41/16.41 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 107.41/16.41 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------