%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP167-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 : n014.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:29 PM UTC 2026
% Result : Unsatisfiable 9.69s 2.04s
% Output : CNFRefutation 9.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 18
% Syntax : Number of clauses : 196 ( 196 unt; 0 nHn; 5 RR)
% Number of literals : 196 ( 195 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 285 ( 32 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t15,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t15]) ).
cnf(t7,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t7]) ).
cnf(t53,plain,
multiply(inverse(X1),multiply(X1,X2)) = multiply(identity,X2),
inference(cp,[status(thm)],[t28,t43]) ).
cnf(t4,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t3647,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(step,[status(thm)],[t53,t22]) ).
cnf(t377,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t3647]) ).
cnf(t12,axiom,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t12]) ).
cnf(t2,axiom,
inverse(inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t57,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t54,t27]) ).
cnf(t478,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t20,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(t29,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t20]) ).
cnf(t0,axiom,
inverse(identity) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t139,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t0]) ).
cnf(t140,plain,
inverse(multiply(X1,identity)) = multiply(identity,inverse(X1)),
inference(cp,[status(thm)],[t54,t139]) ).
cnf(t3627,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(step,[status(thm)],[t140,t22]) ).
cnf(t183,plain,
inverse(multiply(X1,identity)) = inverse(X1),
inference(orient,[status(thm)],[t3627]) ).
cnf(t187,plain,
multiply(X1,identity) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t27,t183]) ).
cnf(t3628,plain,
multiply(X1,identity) = X1,
inference(step,[status(thm)],[t187,t27]) ).
cnf(t188,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t3628]) ).
cnf(t191,plain,
multiply(X1,least_upper_bound(identity,X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t29,t188]) ).
cnf(t6,axiom,
least_upper_bound(X1,identity) = positive_part(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t92,plain,
least_upper_bound(X1,identity) = positive_part(X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t10,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t67,plain,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t95,plain,
positive_part(X1) = least_upper_bound(identity,X1),
inference(cp,[status(thm)],[t92,t67]) ).
cnf(t144,plain,
least_upper_bound(identity,X1) = positive_part(X1),
inference(orient,[status(thm)],[t95]) ).
cnf(t3656,plain,
multiply(X1,positive_part(X2)) = least_upper_bound(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t191,t144]) ).
cnf(t591,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,positive_part(X2)),
inference(orient,[status(thm)],[t3656]) ).
cnf(t44,plain,
identity = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t43,t27]) ).
cnf(t158,plain,
multiply(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t44]) ).
cnf(t597,plain,
multiply(X1,positive_part(inverse(X1))) = least_upper_bound(X1,identity),
inference(cp,[status(thm)],[t591,t158]) ).
cnf(t3657,plain,
multiply(X1,positive_part(inverse(X1))) = positive_part(X1),
inference(step,[status(thm)],[t597,t92]) ).
cnf(t624,plain,
multiply(X1,positive_part(inverse(X1))) = positive_part(X1),
inference(orient,[status(thm)],[t3657]) ).
cnf(t640,plain,
multiply(inverse(positive_part(inverse(inverse(X1)))),X1) = inverse(positive_part(inverse(X1))),
inference(cp,[status(thm)],[t478,t624]) ).
cnf(t3667,plain,
multiply(inverse(positive_part(X1)),X1) = inverse(positive_part(inverse(X1))),
inference(step,[status(thm)],[t640,t27]) ).
cnf(t783,plain,
multiply(inverse(positive_part(X1)),X1) = inverse(positive_part(inverse(X1))),
inference(orient,[status(thm)],[t3667]) ).
cnf(t792,plain,
X1 = multiply(inverse(inverse(positive_part(X1))),inverse(positive_part(inverse(X1)))),
inference(cp,[status(thm)],[t377,t783]) ).
cnf(t3691,plain,
X1 = inverse(multiply(positive_part(inverse(X1)),inverse(positive_part(X1)))),
inference(step,[status(thm)],[t792,t54]) ).
cnf(t56,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t54,t27]) ).
cnf(t469,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t56]) ).
cnf(t3692,plain,
X1 = multiply(positive_part(X1),inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t3691,t469]) ).
cnf(t1588,plain,
multiply(positive_part(X1),inverse(positive_part(inverse(X1)))) = X1,
inference(orient,[status(thm)],[t3692]) ).
cnf(t479,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(cp,[status(thm)],[t478,t377]) ).
cnf(t894,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t479]) ).
cnf(t17,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(t31,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,greatest_lower_bound(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t165,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = greatest_lower_bound(multiply(X1,X2),identity),
inference(cp,[status(thm)],[t31,t158]) ).
cnf(t5,axiom,
greatest_lower_bound(X1,identity) = negative_part(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t131,plain,
greatest_lower_bound(X1,identity) = negative_part(X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t3740,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = negative_part(multiply(X1,X2)),
inference(step,[status(thm)],[t165,t131]) ).
cnf(t2284,plain,
multiply(X1,greatest_lower_bound(X2,inverse(X1))) = negative_part(multiply(X1,X2)),
inference(orient,[status(thm)],[t3740]) ).
cnf(t19,axiom,
least_upper_bound(greatest_lower_bound(X1,X2),greatest_lower_bound(X1,X3)) = greatest_lower_bound(X1,least_upper_bound(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t100,plain,
least_upper_bound(greatest_lower_bound(X1,X2),greatest_lower_bound(X1,X3)) = greatest_lower_bound(X1,least_upper_bound(X2,X3)),
inference(orient,[status(thm)],[t19]) ).
cnf(t138,plain,
greatest_lower_bound(X1,least_upper_bound(X2,identity)) = least_upper_bound(greatest_lower_bound(X1,X2),negative_part(X1)),
inference(cp,[status(thm)],[t100,t131]) ).
cnf(t3711,plain,
greatest_lower_bound(X1,positive_part(X2)) = least_upper_bound(greatest_lower_bound(X1,X2),negative_part(X1)),
inference(step,[status(thm)],[t138,t92]) ).
cnf(t3712,plain,
greatest_lower_bound(X1,positive_part(X2)) = least_upper_bound(negative_part(X1),greatest_lower_bound(X1,X2)),
inference(step,[status(thm)],[t3711,t67]) ).
cnf(t1783,plain,
least_upper_bound(negative_part(X1),greatest_lower_bound(X1,X2)) = greatest_lower_bound(X1,positive_part(X2)),
inference(orient,[status(thm)],[t3712]) ).
cnf(t8,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t114,plain,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t1817,plain,
greatest_lower_bound(X1,positive_part(X2)) = least_upper_bound(negative_part(X1),greatest_lower_bound(X2,X1)),
inference(cp,[status(thm)],[t1783,t114]) ).
cnf(t2885,plain,
least_upper_bound(negative_part(X1),greatest_lower_bound(X2,X1)) = greatest_lower_bound(X1,positive_part(X2)),
inference(orient,[status(thm)],[t1817]) ).
cnf(t18,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(t38,plain,
greatest_lower_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(greatest_lower_bound(X1,X3),X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t39,plain,
multiply(greatest_lower_bound(identity,X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t38,t22]) ).
cnf(t134,plain,
negative_part(X1) = greatest_lower_bound(identity,X1),
inference(cp,[status(thm)],[t131,t114]) ).
cnf(t150,plain,
greatest_lower_bound(identity,X1) = negative_part(X1),
inference(orient,[status(thm)],[t134]) ).
cnf(t3669,plain,
multiply(negative_part(X1),X2) = greatest_lower_bound(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t39,t150]) ).
cnf(t927,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(negative_part(X2),X1),
inference(orient,[status(thm)],[t3669]) ).
cnf(t189,plain,
multiply(X1,greatest_lower_bound(identity,X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t31,t188]) ).
cnf(t3653,plain,
multiply(X1,negative_part(X2)) = greatest_lower_bound(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t189,t150]) ).
cnf(t528,plain,
greatest_lower_bound(X1,multiply(X1,X2)) = multiply(X1,negative_part(X2)),
inference(orient,[status(thm)],[t3653]) ).
cnf(t533,plain,
multiply(X1,negative_part(inverse(X1))) = greatest_lower_bound(X1,identity),
inference(cp,[status(thm)],[t528,t158]) ).
cnf(t3654,plain,
multiply(X1,negative_part(inverse(X1))) = negative_part(X1),
inference(step,[status(thm)],[t533,t131]) ).
cnf(t546,plain,
multiply(X1,negative_part(inverse(X1))) = negative_part(X1),
inference(orient,[status(thm)],[t3654]) ).
cnf(t562,plain,
multiply(inverse(negative_part(inverse(inverse(X1)))),X1) = inverse(negative_part(inverse(X1))),
inference(cp,[status(thm)],[t478,t546]) ).
cnf(t3666,plain,
multiply(inverse(negative_part(X1)),X1) = inverse(negative_part(inverse(X1))),
inference(step,[status(thm)],[t562,t27]) ).
cnf(t762,plain,
multiply(inverse(negative_part(X1)),X1) = inverse(negative_part(inverse(X1))),
inference(orient,[status(thm)],[t3666]) ).
cnf(t940,plain,
multiply(negative_part(inverse(negative_part(X1))),X1) = greatest_lower_bound(X1,inverse(negative_part(inverse(X1)))),
inference(cp,[status(thm)],[t927,t762]) ).
cnf(t9,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)],[t9]) ).
cnf(t151,plain,
negative_part(least_upper_bound(identity,X1)) = identity,
inference(cp,[status(thm)],[t150,t26]) ).
cnf(t3623,plain,
negative_part(positive_part(X1)) = identity,
inference(step,[status(thm)],[t151,t144]) ).
cnf(t156,plain,
negative_part(positive_part(X1)) = identity,
inference(orient,[status(thm)],[t3623]) ).
cnf(t21,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(t32,plain,
least_upper_bound(multiply(X1,X2),multiply(X3,X2)) = multiply(least_upper_bound(X1,X3),X2),
inference(orient,[status(thm)],[t21]) ).
cnf(t33,plain,
multiply(least_upper_bound(identity,X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t32,t22]) ).
cnf(t3639,plain,
multiply(positive_part(X1),X2) = least_upper_bound(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t33,t144]) ).
cnf(t298,plain,
least_upper_bound(X1,multiply(X2,X1)) = multiply(positive_part(X2),X1),
inference(orient,[status(thm)],[t3639]) ).
cnf(t302,plain,
multiply(positive_part(X1),inverse(X1)) = least_upper_bound(inverse(X1),identity),
inference(cp,[status(thm)],[t298,t158]) ).
cnf(t3643,plain,
multiply(positive_part(X1),inverse(X1)) = positive_part(inverse(X1)),
inference(step,[status(thm)],[t302,t92]) ).
cnf(t343,plain,
multiply(positive_part(X1),inverse(X1)) = positive_part(inverse(X1)),
inference(orient,[status(thm)],[t3643]) ).
cnf(t11,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t152,plain,
identity = least_upper_bound(identity,negative_part(X1)),
inference(cp,[status(thm)],[t24,t150]) ).
cnf(t3624,plain,
identity = positive_part(negative_part(X1)),
inference(step,[status(thm)],[t152,t144]) ).
cnf(t157,plain,
positive_part(negative_part(X1)) = identity,
inference(orient,[status(thm)],[t3624]) ).
cnf(t347,plain,
positive_part(inverse(negative_part(X1))) = multiply(identity,inverse(negative_part(X1))),
inference(cp,[status(thm)],[t343,t157]) ).
cnf(t3645,plain,
positive_part(inverse(negative_part(X1))) = inverse(negative_part(X1)),
inference(step,[status(thm)],[t347,t22]) ).
cnf(t361,plain,
positive_part(inverse(negative_part(X1))) = inverse(negative_part(X1)),
inference(orient,[status(thm)],[t3645]) ).
cnf(t366,plain,
identity = negative_part(inverse(negative_part(X1))),
inference(cp,[status(thm)],[t156,t361]) ).
cnf(t368,plain,
negative_part(inverse(negative_part(X1))) = identity,
inference(orient,[status(thm)],[t366]) ).
cnf(t3672,plain,
multiply(identity,X1) = greatest_lower_bound(X1,inverse(negative_part(inverse(X1)))),
inference(step,[status(thm)],[t940,t368]) ).
cnf(t3673,plain,
X1 = greatest_lower_bound(X1,inverse(negative_part(inverse(X1)))),
inference(step,[status(thm)],[t3672,t22]) ).
cnf(t1080,plain,
greatest_lower_bound(X1,inverse(negative_part(inverse(X1)))) = X1,
inference(orient,[status(thm)],[t3673]) ).
cnf(t2916,plain,
greatest_lower_bound(inverse(negative_part(inverse(X1))),positive_part(X1)) = least_upper_bound(negative_part(inverse(negative_part(inverse(X1)))),X1),
inference(cp,[status(thm)],[t2885,t1080]) ).
cnf(t3795,plain,
greatest_lower_bound(positive_part(X1),inverse(negative_part(inverse(X1)))) = least_upper_bound(negative_part(inverse(negative_part(inverse(X1)))),X1),
inference(step,[status(thm)],[t2916,t114]) ).
cnf(t3796,plain,
greatest_lower_bound(positive_part(X1),inverse(negative_part(inverse(X1)))) = least_upper_bound(X1,negative_part(inverse(negative_part(inverse(X1))))),
inference(step,[status(thm)],[t3795,t67]) ).
cnf(t3797,plain,
greatest_lower_bound(positive_part(X1),inverse(negative_part(inverse(X1)))) = least_upper_bound(X1,identity),
inference(step,[status(thm)],[t3796,t368]) ).
cnf(t3798,plain,
greatest_lower_bound(positive_part(X1),inverse(negative_part(inverse(X1)))) = positive_part(X1),
inference(step,[status(thm)],[t3797,t92]) ).
cnf(t3412,plain,
greatest_lower_bound(positive_part(X1),inverse(negative_part(inverse(X1)))) = positive_part(X1),
inference(orient,[status(thm)],[t3798]) ).
cnf(t3425,plain,
negative_part(multiply(negative_part(inverse(X1)),positive_part(X1))) = multiply(negative_part(inverse(X1)),positive_part(X1)),
inference(cp,[status(thm)],[t2284,t3412]) ).
cnf(t70,plain,
X1 = greatest_lower_bound(X1,least_upper_bound(X2,X1)),
inference(cp,[status(thm)],[t26,t67]) ).
cnf(t193,plain,
greatest_lower_bound(X1,least_upper_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t70]) ).
cnf(t303,plain,
multiply(positive_part(inverse(X1)),X1) = least_upper_bound(X1,identity),
inference(cp,[status(thm)],[t298,t43]) ).
cnf(t3640,plain,
multiply(positive_part(inverse(X1)),X1) = positive_part(X1),
inference(step,[status(thm)],[t303,t92]) ).
cnf(t311,plain,
multiply(positive_part(inverse(X1)),X1) = positive_part(X1),
inference(orient,[status(thm)],[t3640]) ).
cnf(t470,plain,
multiply(X1,inverse(positive_part(inverse(inverse(X1))))) = inverse(positive_part(inverse(X1))),
inference(cp,[status(thm)],[t469,t311]) ).
cnf(t3659,plain,
multiply(X1,inverse(positive_part(X1))) = inverse(positive_part(inverse(X1))),
inference(step,[status(thm)],[t470,t27]) ).
cnf(t659,plain,
multiply(X1,inverse(positive_part(X1))) = inverse(positive_part(inverse(X1))),
inference(orient,[status(thm)],[t3659]) ).
cnf(t665,plain,
multiply(X1,positive_part(inverse(positive_part(X1)))) = least_upper_bound(X1,inverse(positive_part(inverse(X1)))),
inference(cp,[status(thm)],[t591,t659]) ).
cnf(t135,plain,
X1 = least_upper_bound(X1,negative_part(X1)),
inference(cp,[status(thm)],[t24,t131]) ).
cnf(t176,plain,
least_upper_bound(X1,negative_part(X1)) = X1,
inference(orient,[status(thm)],[t135]) ).
cnf(t178,plain,
positive_part(X1) = least_upper_bound(positive_part(X1),identity),
inference(cp,[status(thm)],[t176,t156]) ).
cnf(t3626,plain,
positive_part(X1) = positive_part(positive_part(X1)),
inference(step,[status(thm)],[t178,t92]) ).
cnf(t182,plain,
positive_part(positive_part(X1)) = positive_part(X1),
inference(orient,[status(thm)],[t3626]) ).
cnf(t346,plain,
positive_part(inverse(positive_part(X1))) = multiply(positive_part(X1),inverse(positive_part(X1))),
inference(cp,[status(thm)],[t343,t182]) ).
cnf(t3644,plain,
positive_part(inverse(positive_part(X1))) = identity,
inference(step,[status(thm)],[t346,t158]) ).
cnf(t357,plain,
positive_part(inverse(positive_part(X1))) = identity,
inference(orient,[status(thm)],[t3644]) ).
cnf(t3660,plain,
multiply(X1,identity) = least_upper_bound(X1,inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t665,t357]) ).
cnf(t3661,plain,
X1 = least_upper_bound(X1,inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t3660,t188]) ).
cnf(t677,plain,
least_upper_bound(X1,inverse(positive_part(inverse(X1)))) = X1,
inference(orient,[status(thm)],[t3661]) ).
cnf(t681,plain,
inverse(X1) = least_upper_bound(inverse(X1),inverse(positive_part(X1))),
inference(cp,[status(thm)],[t677,t27]) ).
cnf(t913,plain,
least_upper_bound(inverse(X1),inverse(positive_part(X1))) = inverse(X1),
inference(orient,[status(thm)],[t681]) ).
cnf(t922,plain,
inverse(positive_part(X1)) = greatest_lower_bound(inverse(positive_part(X1)),inverse(X1)),
inference(cp,[status(thm)],[t193,t913]) ).
cnf(t3681,plain,
inverse(positive_part(X1)) = greatest_lower_bound(inverse(X1),inverse(positive_part(X1))),
inference(step,[status(thm)],[t922,t114]) ).
cnf(t1252,plain,
greatest_lower_bound(inverse(X1),inverse(positive_part(X1))) = inverse(positive_part(X1)),
inference(orient,[status(thm)],[t3681]) ).
cnf(t34,plain,
multiply(least_upper_bound(multiply(X1,X2),X3),Y3) = least_upper_bound(multiply(X1,multiply(X2,Y3)),multiply(X3,Y3)),
inference(cp,[status(thm)],[t32,t28]) ).
cnf(t975,plain,
least_upper_bound(multiply(X1,multiply(X2,X3)),multiply(Y3,X3)) = multiply(least_upper_bound(multiply(X1,X2),Y3),X3),
inference(orient,[status(thm)],[t34]) ).
cnf(t984,plain,
multiply(least_upper_bound(multiply(inverse(multiply(X1,X2)),X1),X3),X2) = least_upper_bound(identity,multiply(X3,X2)),
inference(cp,[status(thm)],[t975,t43]) ).
cnf(t3759,plain,
multiply(least_upper_bound(inverse(X2),X3),X2) = least_upper_bound(identity,multiply(X3,X2)),
inference(step,[status(thm)],[t984,t894]) ).
cnf(t3760,plain,
multiply(least_upper_bound(inverse(X2),X3),X2) = positive_part(multiply(X3,X2)),
inference(step,[status(thm)],[t3759,t144]) ).
cnf(t2471,plain,
multiply(least_upper_bound(inverse(X1),X2),X1) = positive_part(multiply(X2,X1)),
inference(orient,[status(thm)],[t3760]) ).
cnf(t118,plain,
X1 = least_upper_bound(X1,greatest_lower_bound(X2,X1)),
inference(cp,[status(thm)],[t24,t114]) ).
cnf(t207,plain,
least_upper_bound(X1,greatest_lower_bound(X2,X1)) = X1,
inference(orient,[status(thm)],[t118]) ).
cnf(t2484,plain,
positive_part(multiply(greatest_lower_bound(X1,inverse(X2)),X2)) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t2471,t207]) ).
cnf(t3762,plain,
positive_part(multiply(greatest_lower_bound(X1,inverse(X2)),X2)) = identity,
inference(step,[status(thm)],[t2484,t43]) ).
cnf(t2536,plain,
positive_part(multiply(greatest_lower_bound(X1,inverse(X2)),X2)) = identity,
inference(orient,[status(thm)],[t3762]) ).
cnf(t2541,plain,
identity = positive_part(multiply(greatest_lower_bound(X1,X2),inverse(X2))),
inference(cp,[status(thm)],[t2536,t27]) ).
cnf(t2586,plain,
positive_part(multiply(greatest_lower_bound(X1,X2),inverse(X2))) = identity,
inference(orient,[status(thm)],[t2541]) ).
cnf(t2598,plain,
identity = positive_part(multiply(X1,inverse(least_upper_bound(X2,X1)))),
inference(cp,[status(thm)],[t2586,t193]) ).
cnf(t2679,plain,
positive_part(multiply(X1,inverse(least_upper_bound(X2,X1)))) = identity,
inference(orient,[status(thm)],[t2598]) ).
cnf(t2706,plain,
inverse(positive_part(multiply(X1,inverse(least_upper_bound(X2,X1))))) = greatest_lower_bound(inverse(multiply(X1,inverse(least_upper_bound(X2,X1)))),inverse(identity)),
inference(cp,[status(thm)],[t1252,t2679]) ).
cnf(t3781,plain,
inverse(identity) = greatest_lower_bound(inverse(multiply(X1,inverse(least_upper_bound(X2,X1)))),inverse(identity)),
inference(step,[status(thm)],[t2706,t2679]) ).
cnf(t3782,plain,
identity = greatest_lower_bound(inverse(multiply(X1,inverse(least_upper_bound(X2,X1)))),inverse(identity)),
inference(step,[status(thm)],[t3781,t139]) ).
cnf(t3783,plain,
identity = greatest_lower_bound(inverse(identity),inverse(multiply(X1,inverse(least_upper_bound(X2,X1))))),
inference(step,[status(thm)],[t3782,t114]) ).
cnf(t3784,plain,
identity = greatest_lower_bound(identity,inverse(multiply(X1,inverse(least_upper_bound(X2,X1))))),
inference(step,[status(thm)],[t3783,t139]) ).
cnf(t3785,plain,
identity = negative_part(inverse(multiply(X1,inverse(least_upper_bound(X2,X1))))),
inference(step,[status(thm)],[t3784,t150]) ).
cnf(t3786,plain,
identity = negative_part(multiply(least_upper_bound(X2,X1),inverse(X1))),
inference(step,[status(thm)],[t3785,t469]) ).
cnf(t2784,plain,
negative_part(multiply(least_upper_bound(X1,X2),inverse(X2))) = identity,
inference(orient,[status(thm)],[t3786]) ).
cnf(t666,plain,
multiply(X1,negative_part(inverse(positive_part(X1)))) = greatest_lower_bound(X1,inverse(positive_part(inverse(X1)))),
inference(cp,[status(thm)],[t528,t659]) ).
cnf(t99,plain,
X1 = greatest_lower_bound(X1,positive_part(X1)),
inference(cp,[status(thm)],[t26,t92]) ).
cnf(t169,plain,
greatest_lower_bound(X1,positive_part(X1)) = X1,
inference(orient,[status(thm)],[t99]) ).
cnf(t360,plain,
inverse(positive_part(X1)) = greatest_lower_bound(inverse(positive_part(X1)),identity),
inference(cp,[status(thm)],[t169,t357]) ).
cnf(t3646,plain,
inverse(positive_part(X1)) = negative_part(inverse(positive_part(X1))),
inference(step,[status(thm)],[t360,t131]) ).
cnf(t371,plain,
negative_part(inverse(positive_part(X1))) = inverse(positive_part(X1)),
inference(orient,[status(thm)],[t3646]) ).
cnf(t3749,plain,
multiply(X1,inverse(positive_part(X1))) = greatest_lower_bound(X1,inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t666,t371]) ).
cnf(t3750,plain,
inverse(positive_part(inverse(X1))) = greatest_lower_bound(X1,inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t3749,t659]) ).
cnf(t2411,plain,
greatest_lower_bound(X1,inverse(positive_part(inverse(X1)))) = inverse(positive_part(inverse(X1))),
inference(orient,[status(thm)],[t3750]) ).
cnf(t2415,plain,
greatest_lower_bound(X1,positive_part(inverse(positive_part(inverse(X1))))) = least_upper_bound(negative_part(X1),inverse(positive_part(inverse(X1)))),
inference(cp,[status(thm)],[t1783,t2411]) ).
cnf(t3791,plain,
greatest_lower_bound(X1,identity) = least_upper_bound(negative_part(X1),inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t2415,t357]) ).
cnf(t3792,plain,
negative_part(X1) = least_upper_bound(negative_part(X1),inverse(positive_part(inverse(X1)))),
inference(step,[status(thm)],[t3791,t131]) ).
cnf(t3277,plain,
least_upper_bound(negative_part(X1),inverse(positive_part(inverse(X1)))) = negative_part(X1),
inference(orient,[status(thm)],[t3792]) ).
cnf(t3289,plain,
identity = negative_part(multiply(negative_part(X1),inverse(inverse(positive_part(inverse(X1)))))),
inference(cp,[status(thm)],[t2784,t3277]) ).
cnf(t3793,plain,
identity = negative_part(multiply(negative_part(X1),positive_part(inverse(X1)))),
inference(step,[status(thm)],[t3289,t27]) ).
cnf(t3296,plain,
negative_part(multiply(negative_part(X1),positive_part(inverse(X1)))) = identity,
inference(orient,[status(thm)],[t3793]) ).
cnf(t3302,plain,
identity = negative_part(multiply(negative_part(inverse(X1)),positive_part(X1))),
inference(cp,[status(thm)],[t3296,t27]) ).
cnf(t3352,plain,
negative_part(multiply(negative_part(inverse(X1)),positive_part(X1))) = identity,
inference(orient,[status(thm)],[t3302]) ).
cnf(t3799,plain,
identity = multiply(negative_part(inverse(X1)),positive_part(X1)),
inference(step,[status(thm)],[t3425,t3352]) ).
cnf(t3432,plain,
multiply(negative_part(inverse(X1)),positive_part(X1)) = identity,
inference(orient,[status(thm)],[t3799]) ).
cnf(t3456,plain,
inverse(positive_part(X1)) = multiply(inverse(identity),negative_part(inverse(X1))),
inference(cp,[status(thm)],[t894,t3432]) ).
cnf(t3800,plain,
inverse(positive_part(X1)) = multiply(identity,negative_part(inverse(X1))),
inference(step,[status(thm)],[t3456,t139]) ).
cnf(t3801,plain,
inverse(positive_part(X1)) = negative_part(inverse(X1)),
inference(step,[status(thm)],[t3800,t22]) ).
cnf(t3458,plain,
inverse(positive_part(X1)) = negative_part(inverse(X1)),
inference(orient,[status(thm)],[t3801]) ).
cnf(t3805,plain,
multiply(positive_part(X1),negative_part(inverse(inverse(X1)))) = X1,
inference(step,[status(thm)],[t1588,t3458]) ).
cnf(t3806,plain,
multiply(positive_part(X1),negative_part(X1)) = X1,
inference(step,[status(thm)],[t3805,t27]) ).
cnf(t3495,plain,
multiply(positive_part(X1),negative_part(X1)) = X1,
inference(rw,[status(thm)],[t3806]) ).
cnf(t3572,plain,
multiply(positive_part(X1),negative_part(X1)) = X1,
inference(orient,[status(thm)],[t3495]) ).
cnf(goal_0,negated_conjecture,
multiply(positive_part(a),negative_part(a)) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
a != a,
inference(rw,[status(thm)],[goal_0,t3572]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP167-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n014.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Wed Sep 23 13:55:19 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.69/2.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.69/2.04 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------