%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP200-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:40 PM UTC 2026
% Result : Unsatisfiable 7.74s 1.85s
% Output : CNFRefutation 7.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 9
% Syntax : Number of clauses : 145 ( 145 unt; 0 nHn; 3 RR)
% Number of literals : 145 ( 144 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 311 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7,axiom,
right_division(multiply(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
right_division(multiply(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t5,axiom,
multiply(X1,left_division(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
multiply(X1,left_division(X1,X2)) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t16,plain,
X1 = right_division(X2,left_division(X1,X2)),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t53,plain,
right_division(X1,left_division(X2,X1)) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t4,axiom,
left_division(X1,multiply(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
left_division(X1,multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t6,axiom,
multiply(right_division(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
multiply(right_division(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t21,plain,
X1 = left_division(right_division(X2,X1),X2),
inference(cp,[status(thm)],[t19,t13]) ).
cnf(t54,plain,
left_division(right_division(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(t8,axiom,
multiply(multiply(X1,multiply(X2,X3)),X1) = multiply(multiply(X1,X2),multiply(X3,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
multiply(multiply(X1,multiply(X2,X3)),X1) = multiply(multiply(X1,X2),multiply(X3,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t32,plain,
multiply(multiply(X1,identity),multiply(X2,X1)) = multiply(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t27,t11]) ).
cnf(t0,axiom,
multiply(X1,identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t17409,plain,
multiply(X1,multiply(X2,X1)) = multiply(multiply(X1,X2),X1),
inference(step,[status(thm)],[t32,t10]) ).
cnf(t55,plain,
multiply(multiply(X1,X2),X1) = multiply(X1,multiply(X2,X1)),
inference(orient,[status(thm)],[t17409]) ).
cnf(t62,plain,
multiply(X1,X2) = right_division(multiply(X1,multiply(X2,X1)),X1),
inference(cp,[status(thm)],[t15,t55]) ).
cnf(t115,plain,
right_division(multiply(X1,multiply(X2,X1)),X1) = multiply(X1,X2),
inference(orient,[status(thm)],[t62]) ).
cnf(t121,plain,
multiply(X1,right_division(X2,X1)) = right_division(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t115,t13]) ).
cnf(t123,plain,
multiply(X1,right_division(X2,X1)) = right_division(multiply(X1,X2),X1),
inference(orient,[status(thm)],[t121]) ).
cnf(t130,plain,
X1 = right_division(right_division(multiply(X1,X2),X1),right_division(X2,X1)),
inference(cp,[status(thm)],[t15,t123]) ).
cnf(t167,plain,
right_division(right_division(multiply(X1,X2),X1),right_division(X2,X1)) = X1,
inference(orient,[status(thm)],[t130]) ).
cnf(t17410,plain,
multiply(X1,multiply(multiply(X2,X3),X1)) = multiply(multiply(X1,X2),multiply(X3,X1)),
inference(step,[status(thm)],[t27,t55]) ).
cnf(t63,plain,
multiply(X1,multiply(multiply(X2,X3),X1)) = multiply(multiply(X1,X2),multiply(X3,X1)),
inference(rw,[status(thm)],[t17410]) ).
cnf(t218,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = multiply(X1,multiply(multiply(X2,X3),X1)),
inference(orient,[status(thm)],[t63]) ).
cnf(t2,axiom,
multiply(X1,right_inverse(X1)) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
multiply(X1,right_inverse(X1)) = identity,
inference(orient,[status(thm)],[t2]) ).
cnf(t221,plain,
multiply(X1,multiply(multiply(right_inverse(X1),X2),X1)) = multiply(identity,multiply(X2,X1)),
inference(cp,[status(thm)],[t218,t23]) ).
cnf(t17422,plain,
multiply(X1,multiply(multiply(right_inverse(X1),X2),X1)) = multiply(X2,X1),
inference(step,[status(thm)],[t221,t11]) ).
cnf(t246,plain,
multiply(X1,multiply(multiply(right_inverse(X1),X2),X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t17422]) ).
cnf(t257,plain,
X1 = right_division(right_division(multiply(X2,X1),X1),right_division(multiply(multiply(right_inverse(X1),X2),X1),X1)),
inference(cp,[status(thm)],[t167,t246]) ).
cnf(t17423,plain,
X1 = right_division(X2,right_division(multiply(multiply(right_inverse(X1),X2),X1),X1)),
inference(step,[status(thm)],[t257,t15]) ).
cnf(t17424,plain,
X1 = right_division(X2,multiply(right_inverse(X1),X2)),
inference(step,[status(thm)],[t17423,t15]) ).
cnf(t265,plain,
right_division(X1,multiply(right_inverse(X2),X1)) = X2,
inference(orient,[status(thm)],[t17424]) ).
cnf(t273,plain,
multiply(right_inverse(X1),X2) = left_division(X1,X2),
inference(cp,[status(thm)],[t54,t265]) ).
cnf(t305,plain,
multiply(right_inverse(X1),X2) = left_division(X1,X2),
inference(orient,[status(thm)],[t273]) ).
cnf(t56,plain,
multiply(X1,multiply(right_inverse(X1),X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t55,t23]) ).
cnf(t17411,plain,
multiply(X1,multiply(right_inverse(X1),X1)) = X1,
inference(step,[status(thm)],[t56,t11]) ).
cnf(t64,plain,
multiply(X1,multiply(right_inverse(X1),X1)) = X1,
inference(orient,[status(thm)],[t17411]) ).
cnf(t67,plain,
multiply(right_inverse(X1),X1) = left_division(X1,X1),
inference(cp,[status(thm)],[t19,t64]) ).
cnf(t20,plain,
identity = left_division(X1,X1),
inference(cp,[status(thm)],[t19,t10]) ).
cnf(t48,plain,
left_division(X1,X1) = identity,
inference(orient,[status(thm)],[t20]) ).
cnf(t17412,plain,
multiply(right_inverse(X1),X1) = identity,
inference(step,[status(thm)],[t67,t48]) ).
cnf(t69,plain,
multiply(right_inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t17412]) ).
cnf(t71,plain,
X1 = left_division(right_inverse(X1),identity),
inference(cp,[status(thm)],[t19,t69]) ).
cnf(t25,plain,
right_inverse(X1) = left_division(X1,identity),
inference(cp,[status(thm)],[t19,t23]) ).
cnf(t49,plain,
left_division(X1,identity) = right_inverse(X1),
inference(orient,[status(thm)],[t25]) ).
cnf(t17418,plain,
X1 = right_inverse(right_inverse(X1)),
inference(step,[status(thm)],[t71,t49]) ).
cnf(t78,plain,
right_inverse(right_inverse(X1)) = X1,
inference(orient,[status(thm)],[t17418]) ).
cnf(t309,plain,
left_division(right_inverse(X1),X2) = multiply(X1,X2),
inference(cp,[status(thm)],[t305,t78]) ).
cnf(t324,plain,
left_division(right_inverse(X1),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t309]) ).
cnf(t328,plain,
right_inverse(X1) = right_division(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t53,t324]) ).
cnf(t384,plain,
right_division(X1,multiply(X2,X1)) = right_inverse(X2),
inference(orient,[status(thm)],[t328]) ).
cnf(t232,plain,
multiply(X1,multiply(multiply(X2,right_division(X3,X1)),X1)) = multiply(multiply(X1,X2),X3),
inference(cp,[status(thm)],[t218,t13]) ).
cnf(t57,plain,
multiply(X1,multiply(left_division(X1,X2),X1)) = multiply(X2,X1),
inference(cp,[status(thm)],[t55,t9]) ).
cnf(t79,plain,
multiply(X1,multiply(left_division(X1,X2),X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t82,plain,
multiply(left_division(X1,X2),X1) = left_division(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t19,t79]) ).
cnf(t84,plain,
left_division(X1,multiply(X2,X1)) = multiply(left_division(X1,X2),X1),
inference(orient,[status(thm)],[t82]) ).
cnf(t89,plain,
multiply(left_division(X1,right_division(X2,X1)),X1) = left_division(X1,X2),
inference(cp,[status(thm)],[t84,t13]) ).
cnf(t132,plain,
multiply(left_division(X1,right_division(X2,X1)),X1) = left_division(X1,X2),
inference(orient,[status(thm)],[t89]) ).
cnf(t139,plain,
left_division(X1,right_division(X2,X1)) = right_division(left_division(X1,X2),X1),
inference(cp,[status(thm)],[t15,t132]) ).
cnf(t140,plain,
left_division(X1,right_division(X2,X1)) = right_division(left_division(X1,X2),X1),
inference(orient,[status(thm)],[t139]) ).
cnf(t325,plain,
multiply(X1,right_division(X2,right_inverse(X1))) = right_division(left_division(right_inverse(X1),X2),right_inverse(X1)),
inference(cp,[status(thm)],[t324,t140]) ).
cnf(t17440,plain,
multiply(X1,right_division(X2,right_inverse(X1))) = right_division(multiply(X1,X2),right_inverse(X1)),
inference(step,[status(thm)],[t325,t324]) ).
cnf(t549,plain,
multiply(X1,right_division(X2,right_inverse(X1))) = right_division(multiply(X1,X2),right_inverse(X1)),
inference(orient,[status(thm)],[t17440]) ).
cnf(t552,plain,
right_division(multiply(X1,multiply(X2,right_inverse(X1))),right_inverse(X1)) = multiply(X1,X2),
inference(cp,[status(thm)],[t549,t15]) ).
cnf(t955,plain,
right_division(multiply(X1,multiply(X2,right_inverse(X1))),right_inverse(X1)) = multiply(X1,X2),
inference(orient,[status(thm)],[t552]) ).
cnf(t228,plain,
multiply(right_inverse(X1),multiply(multiply(X2,X1),right_inverse(X1))) = multiply(multiply(right_inverse(X1),X2),identity),
inference(cp,[status(thm)],[t218,t23]) ).
cnf(t17457,plain,
left_division(X1,multiply(multiply(X2,X1),right_inverse(X1))) = multiply(multiply(right_inverse(X1),X2),identity),
inference(step,[status(thm)],[t228,t305]) ).
cnf(t313,plain,
multiply(right_inverse(X1),multiply(X2,right_inverse(X1))) = multiply(left_division(X1,X2),right_inverse(X1)),
inference(cp,[status(thm)],[t55,t305]) ).
cnf(t17439,plain,
left_division(X1,multiply(X2,right_inverse(X1))) = multiply(left_division(X1,X2),right_inverse(X1)),
inference(step,[status(thm)],[t313,t305]) ).
cnf(t539,plain,
left_division(X1,multiply(X2,right_inverse(X1))) = multiply(left_division(X1,X2),right_inverse(X1)),
inference(orient,[status(thm)],[t17439]) ).
cnf(t17458,plain,
multiply(left_division(X1,multiply(X2,X1)),right_inverse(X1)) = multiply(multiply(right_inverse(X1),X2),identity),
inference(step,[status(thm)],[t17457,t539]) ).
cnf(t17459,plain,
multiply(multiply(left_division(X1,X2),X1),right_inverse(X1)) = multiply(multiply(right_inverse(X1),X2),identity),
inference(step,[status(thm)],[t17458,t84]) ).
cnf(t17460,plain,
multiply(multiply(left_division(X1,X2),X1),right_inverse(X1)) = multiply(right_inverse(X1),X2),
inference(step,[status(thm)],[t17459,t10]) ).
cnf(t17461,plain,
multiply(multiply(left_division(X1,X2),X1),right_inverse(X1)) = left_division(X1,X2),
inference(step,[status(thm)],[t17460,t305]) ).
cnf(t1095,plain,
multiply(multiply(left_division(X1,X2),X1),right_inverse(X1)) = left_division(X1,X2),
inference(orient,[status(thm)],[t17461]) ).
cnf(t1129,plain,
multiply(X1,multiply(left_division(X1,X2),X1)) = right_division(multiply(X1,left_division(X1,X2)),right_inverse(X1)),
inference(cp,[status(thm)],[t955,t1095]) ).
cnf(t17462,plain,
multiply(X2,X1) = right_division(multiply(X1,left_division(X1,X2)),right_inverse(X1)),
inference(step,[status(thm)],[t1129,t79]) ).
cnf(t17463,plain,
multiply(X2,X1) = right_division(X2,right_inverse(X1)),
inference(step,[status(thm)],[t17462,t9]) ).
cnf(t1130,plain,
right_division(X1,right_inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t17463]) ).
cnf(t315,plain,
right_inverse(X1) = right_division(left_division(X1,X2),X2),
inference(cp,[status(thm)],[t15,t305]) ).
cnf(t340,plain,
right_division(left_division(X1,X2),X2) = right_inverse(X1),
inference(orient,[status(thm)],[t315]) ).
cnf(t347,plain,
right_inverse(right_division(X1,X2)) = right_division(X2,X1),
inference(cp,[status(thm)],[t340,t54]) ).
cnf(t354,plain,
right_inverse(right_division(X1,X2)) = right_division(X2,X1),
inference(orient,[status(thm)],[t347]) ).
cnf(t1138,plain,
multiply(X1,right_division(X2,X3)) = right_division(X1,right_division(X3,X2)),
inference(cp,[status(thm)],[t1130,t354]) ).
cnf(t1379,plain,
multiply(X1,right_division(X2,X3)) = right_division(X1,right_division(X3,X2)),
inference(orient,[status(thm)],[t1138]) ).
cnf(t17756,plain,
multiply(X1,multiply(right_division(X2,right_division(X1,X3)),X1)) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t232,t1379]) ).
cnf(t1139,plain,
multiply(X1,right_inverse(X2)) = right_division(X1,X2),
inference(cp,[status(thm)],[t1130,t78]) ).
cnf(t1152,plain,
multiply(X1,right_inverse(X2)) = right_division(X1,X2),
inference(orient,[status(thm)],[t1139]) ).
cnf(t1145,plain,
right_division(right_inverse(X1),X2) = right_inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t354,t1130]) ).
cnf(t1177,plain,
right_inverse(multiply(X1,X2)) = right_division(right_inverse(X2),X1),
inference(orient,[status(thm)],[t1145]) ).
cnf(t1185,plain,
right_division(right_inverse(X1),right_inverse(X2)) = right_inverse(left_division(X2,X1)),
inference(cp,[status(thm)],[t1177,t305]) ).
cnf(t17477,plain,
multiply(right_inverse(X1),X2) = right_inverse(left_division(X2,X1)),
inference(step,[status(thm)],[t1185,t1130]) ).
cnf(t17478,plain,
left_division(X1,X2) = right_inverse(left_division(X2,X1)),
inference(step,[status(thm)],[t17477,t305]) ).
cnf(t1209,plain,
right_inverse(left_division(X1,X2)) = left_division(X2,X1),
inference(orient,[status(thm)],[t17478]) ).
cnf(t1219,plain,
right_division(X1,left_division(X2,X3)) = multiply(X1,left_division(X3,X2)),
inference(cp,[status(thm)],[t1152,t1209]) ).
cnf(t1470,plain,
multiply(X1,left_division(X2,X3)) = right_division(X1,left_division(X3,X2)),
inference(orient,[status(thm)],[t1219]) ).
cnf(t365,plain,
multiply(right_division(X1,X2),X3) = left_division(right_division(X2,X1),X3),
inference(cp,[status(thm)],[t324,t354]) ).
cnf(t407,plain,
left_division(right_division(X1,X2),X3) = multiply(right_division(X2,X1),X3),
inference(orient,[status(thm)],[t365]) ).
cnf(t1478,plain,
right_division(X1,left_division(X2,right_division(X3,Y3))) = multiply(X1,multiply(right_division(Y3,X3),X2)),
inference(cp,[status(thm)],[t1470,t407]) ).
cnf(t2021,plain,
multiply(X1,multiply(right_division(X2,X3),Y3)) = right_division(X1,left_division(Y3,right_division(X3,X2))),
inference(orient,[status(thm)],[t1478]) ).
cnf(t17757,plain,
right_division(X1,left_division(X1,right_division(right_division(X1,X3),X2))) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t17756,t2021]) ).
cnf(t7818,plain,
right_division(X1,left_division(X1,right_division(right_division(X1,X2),X3))) = multiply(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t17757]) ).
cnf(t411,plain,
multiply(right_division(X1,X2),multiply(right_division(X2,X1),X3)) = X3,
inference(cp,[status(thm)],[t407,t19]) ).
cnf(t725,plain,
multiply(right_division(X1,X2),multiply(right_division(X2,X1),X3)) = X3,
inference(orient,[status(thm)],[t411]) ).
cnf(t1169,plain,
right_inverse(X1) = multiply(right_division(X2,X3),right_division(right_division(X3,X2),X1)),
inference(cp,[status(thm)],[t725,t1152]) ).
cnf(t17518,plain,
right_inverse(X1) = right_division(right_division(X2,X3),right_division(X1,right_division(X3,X2))),
inference(step,[status(thm)],[t1169,t1379]) ).
cnf(t1886,plain,
right_division(right_division(X1,X2),right_division(X3,right_division(X2,X1))) = right_inverse(X3),
inference(orient,[status(thm)],[t17518]) ).
cnf(t7833,plain,
multiply(multiply(X1,right_division(X2,right_division(X3,X1))),X3) = right_division(X1,left_division(X1,right_inverse(X2))),
inference(cp,[status(thm)],[t7818,t1886]) ).
cnf(t17880,plain,
multiply(right_division(X1,right_division(right_division(X3,X1),X2)),X3) = right_division(X1,left_division(X1,right_inverse(X2))),
inference(step,[status(thm)],[t7833,t1379]) ).
cnf(t1159,plain,
right_division(right_inverse(X1),X2) = left_division(X1,right_inverse(X2)),
inference(cp,[status(thm)],[t1152,t305]) ).
cnf(t1238,plain,
left_division(X1,right_inverse(X2)) = right_division(right_inverse(X1),X2),
inference(orient,[status(thm)],[t1159]) ).
cnf(t17881,plain,
multiply(right_division(X1,right_division(right_division(X3,X1),X2)),X3) = right_division(X1,right_division(right_inverse(X1),X2)),
inference(step,[status(thm)],[t17880,t1238]) ).
cnf(t1192,plain,
multiply(X1,multiply(X2,X3)) = right_division(X1,right_division(right_inverse(X3),X2)),
inference(cp,[status(thm)],[t1130,t1177]) ).
cnf(t1590,plain,
right_division(X1,right_division(right_inverse(X2),X3)) = multiply(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t1192]) ).
cnf(t17882,plain,
multiply(right_division(X1,right_division(right_division(X3,X1),X2)),X3) = multiply(X1,multiply(X2,X1)),
inference(step,[status(thm)],[t17881,t1590]) ).
cnf(t15666,plain,
multiply(right_division(X1,right_division(right_division(X2,X1),X3)),X2) = multiply(X1,multiply(X3,X1)),
inference(orient,[status(thm)],[t17882]) ).
cnf(t15838,plain,
right_inverse(right_division(X1,right_division(right_division(X2,X1),X3))) = right_division(X2,multiply(X1,multiply(X3,X1))),
inference(cp,[status(thm)],[t384,t15666]) ).
cnf(t17883,plain,
right_division(right_division(right_division(X2,X1),X3),X1) = right_division(X2,multiply(X1,multiply(X3,X1))),
inference(step,[status(thm)],[t15838,t354]) ).
cnf(t15909,plain,
right_division(right_division(right_division(X1,X2),X3),X2) = right_division(X1,multiply(X2,multiply(X3,X2))),
inference(orient,[status(thm)],[t17883]) ).
cnf(t15918,plain,
right_division(X1,multiply(right_inverse(X2),multiply(X3,right_inverse(X2)))) = multiply(right_division(right_division(X1,right_inverse(X2)),X3),X2),
inference(cp,[status(thm)],[t15909,t1130]) ).
cnf(t17884,plain,
right_division(X1,left_division(X2,multiply(X3,right_inverse(X2)))) = multiply(right_division(right_division(X1,right_inverse(X2)),X3),X2),
inference(step,[status(thm)],[t15918,t305]) ).
cnf(t17885,plain,
right_division(X1,multiply(left_division(X2,X3),right_inverse(X2))) = multiply(right_division(right_division(X1,right_inverse(X2)),X3),X2),
inference(step,[status(thm)],[t17884,t539]) ).
cnf(t17886,plain,
right_division(X1,right_division(left_division(X2,X3),X2)) = multiply(right_division(right_division(X1,right_inverse(X2)),X3),X2),
inference(step,[status(thm)],[t17885,t1152]) ).
cnf(t17887,plain,
right_division(X1,right_division(left_division(X2,X3),X2)) = multiply(right_division(multiply(X1,X2),X3),X2),
inference(step,[status(thm)],[t17886,t1130]) ).
cnf(t16313,plain,
multiply(right_division(multiply(X1,X2),X3),X2) = right_division(X1,right_division(left_division(X2,X3),X2)),
inference(orient,[status(thm)],[t17887]) ).
cnf(t16348,plain,
right_division(X1,right_division(left_division(X2,right_inverse(X3)),X2)) = multiply(multiply(multiply(X1,X2),X3),X2),
inference(cp,[status(thm)],[t16313,t1130]) ).
cnf(t17898,plain,
right_division(X1,right_division(right_division(right_inverse(X2),X3),X2)) = multiply(multiply(multiply(X1,X2),X3),X2),
inference(step,[status(thm)],[t16348,t1238]) ).
cnf(t1186,plain,
right_division(right_inverse(X1),multiply(X1,X2)) = right_inverse(multiply(X1,multiply(X2,X1))),
inference(cp,[status(thm)],[t1177,t55]) ).
cnf(t17508,plain,
right_division(right_inverse(X1),multiply(X1,X2)) = right_division(right_inverse(multiply(X2,X1)),X1),
inference(step,[status(thm)],[t1186,t1177]) ).
cnf(t17509,plain,
right_division(right_inverse(X1),multiply(X1,X2)) = right_division(right_division(right_inverse(X1),X2),X1),
inference(step,[status(thm)],[t17508,t1177]) ).
cnf(t1671,plain,
right_division(right_division(right_inverse(X1),X2),X1) = right_division(right_inverse(X1),multiply(X1,X2)),
inference(orient,[status(thm)],[t17509]) ).
cnf(t17899,plain,
right_division(X1,right_division(right_inverse(X2),multiply(X2,X3))) = multiply(multiply(multiply(X1,X2),X3),X2),
inference(step,[status(thm)],[t17898,t1671]) ).
cnf(t17900,plain,
multiply(X1,multiply(multiply(X2,X3),X2)) = multiply(multiply(multiply(X1,X2),X3),X2),
inference(step,[status(thm)],[t17899,t1590]) ).
cnf(t17901,plain,
multiply(X1,multiply(X2,multiply(X3,X2))) = multiply(multiply(multiply(X1,X2),X3),X2),
inference(step,[status(thm)],[t17900,t55]) ).
cnf(t17248,plain,
multiply(multiply(multiply(X1,X2),X3),X2) = multiply(X1,multiply(X2,multiply(X3,X2))),
inference(orient,[status(thm)],[t17901]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(multiply(a,b),c),b) != multiply(a,multiply(b,multiply(c,b))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a,multiply(b,multiply(c,b))) != multiply(a,multiply(b,multiply(c,b))),
inference(rw,[status(thm)],[goal_0,t17248]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP200-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.03/0.36 % CPULimit : 300
% 0.03/0.36 % WCLimit : 300
% 0.03/0.36 % DateTime : Wed Sep 23 14:08:17 UTC 2026
% 0.03/0.37 % CPUTime :
% 0.03/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.74/1.85 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.74/1.85 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------