%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP583-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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:27:35 PM UTC 2026
% Result : Unsatisfiable 6.15s 1.22s
% Output : CNFRefutation 6.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 5
% Syntax : Number of clauses : 186 ( 186 unt; 0 nHn; 21 RR)
% Number of literals : 186 ( 185 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 277 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
double_divide(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1)))),double_divide(identity,identity)) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
double_divide(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1)))),double_divide(identity,identity)) = X3,
inference(orient,[status(thm)],[t3]) ).
cnf(t0,axiom,
double_divide(X1,identity) = inverse(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
double_divide(X1,identity) = inverse(X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t968,plain,
double_divide(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1)))),inverse(identity)) = X3,
inference(step,[status(thm)],[t4,t7]) ).
cnf(t8,plain,
double_divide(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1)))),inverse(identity)) = X3,
inference(rw,[status(thm)],[t968]) ).
cnf(t69,plain,
double_divide(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1)))),inverse(identity)) = X3,
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
double_divide(X1,inverse(X1)) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
double_divide(X1,inverse(X1)) = identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t73,plain,
X1 = double_divide(double_divide(inverse(X2),double_divide(double_divide(identity,X2),double_divide(X1,identity))),inverse(identity)),
inference(cp,[status(thm)],[t69,t9]) ).
cnf(t970,plain,
X1 = double_divide(double_divide(inverse(X2),double_divide(double_divide(identity,X2),inverse(X1))),inverse(identity)),
inference(step,[status(thm)],[t73,t7]) ).
cnf(t84,plain,
double_divide(double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X2))),inverse(identity)) = X2,
inference(orient,[status(thm)],[t970]) ).
cnf(t91,plain,
X1 = double_divide(double_divide(inverse(inverse(identity)),double_divide(identity,inverse(X1))),inverse(identity)),
inference(cp,[status(thm)],[t84,t9]) ).
cnf(t2,axiom,
double_divide(double_divide(X1,X2),identity) = multiply(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t969,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(step,[status(thm)],[t2,t7]) ).
cnf(t10,plain,
inverse(double_divide(X1,X2)) = multiply(X2,X1),
inference(orient,[status(thm)],[t969]) ).
cnf(t11,plain,
multiply(identity,X1) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t10,t7]) ).
cnf(t14,plain,
inverse(inverse(X1)) = multiply(identity,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t974,plain,
X1 = double_divide(double_divide(multiply(identity,identity),double_divide(identity,inverse(X1))),inverse(identity)),
inference(step,[status(thm)],[t91,t14]) ).
cnf(t125,plain,
double_divide(double_divide(multiply(identity,identity),double_divide(identity,inverse(X1))),inverse(identity)) = X1,
inference(orient,[status(thm)],[t974]) ).
cnf(t127,plain,
double_divide(X1,X2) = double_divide(double_divide(multiply(identity,identity),double_divide(identity,multiply(X2,X1))),inverse(identity)),
inference(cp,[status(thm)],[t125,t10]) ).
cnf(t168,plain,
double_divide(double_divide(multiply(identity,identity),double_divide(identity,multiply(X1,X2))),inverse(identity)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t127]) ).
cnf(t70,plain,
X1 = double_divide(double_divide(X2,double_divide(inverse(identity),double_divide(X1,double_divide(identity,X2)))),inverse(identity)),
inference(cp,[status(thm)],[t69,t7]) ).
cnf(t176,plain,
double_divide(double_divide(X1,double_divide(inverse(identity),double_divide(X2,double_divide(identity,X1)))),inverse(identity)) = X2,
inference(orient,[status(thm)],[t70]) ).
cnf(t177,plain,
X1 = double_divide(double_divide(identity,double_divide(inverse(identity),double_divide(X1,inverse(identity)))),inverse(identity)),
inference(cp,[status(thm)],[t176,t7]) ).
cnf(t185,plain,
double_divide(double_divide(identity,double_divide(inverse(identity),double_divide(X1,inverse(identity)))),inverse(identity)) = X1,
inference(orient,[status(thm)],[t177]) ).
cnf(t186,plain,
identity = double_divide(double_divide(identity,double_divide(inverse(identity),identity)),inverse(identity)),
inference(cp,[status(thm)],[t185,t9]) ).
cnf(t977,plain,
identity = double_divide(double_divide(identity,inverse(inverse(identity))),inverse(identity)),
inference(step,[status(thm)],[t186,t7]) ).
cnf(t978,plain,
identity = double_divide(double_divide(identity,multiply(identity,identity)),inverse(identity)),
inference(step,[status(thm)],[t977,t14]) ).
cnf(t204,plain,
double_divide(double_divide(identity,multiply(identity,identity)),inverse(identity)) = identity,
inference(orient,[status(thm)],[t978]) ).
cnf(t210,plain,
identity = double_divide(double_divide(inverse(multiply(identity,identity)),identity),inverse(identity)),
inference(cp,[status(thm)],[t84,t204]) ).
cnf(t979,plain,
identity = double_divide(inverse(inverse(multiply(identity,identity))),inverse(identity)),
inference(step,[status(thm)],[t210,t7]) ).
cnf(t980,plain,
identity = double_divide(multiply(identity,multiply(identity,identity)),inverse(identity)),
inference(step,[status(thm)],[t979,t14]) ).
cnf(t89,plain,
double_divide(identity,X1) = double_divide(double_divide(inverse(X1),identity),inverse(identity)),
inference(cp,[status(thm)],[t84,t9]) ).
cnf(t971,plain,
double_divide(identity,X1) = double_divide(inverse(inverse(X1)),inverse(identity)),
inference(step,[status(thm)],[t89,t7]) ).
cnf(t972,plain,
double_divide(identity,X1) = double_divide(multiply(identity,X1),inverse(identity)),
inference(step,[status(thm)],[t971,t14]) ).
cnf(t100,plain,
double_divide(multiply(identity,X1),inverse(identity)) = double_divide(identity,X1),
inference(orient,[status(thm)],[t972]) ).
cnf(t981,plain,
identity = double_divide(identity,multiply(identity,identity)),
inference(step,[status(thm)],[t980,t100]) ).
cnf(t213,plain,
double_divide(identity,multiply(identity,identity)) = identity,
inference(orient,[status(thm)],[t981]) ).
cnf(t219,plain,
double_divide(identity,identity) = double_divide(double_divide(multiply(identity,identity),identity),inverse(identity)),
inference(cp,[status(thm)],[t168,t213]) ).
cnf(t982,plain,
inverse(identity) = double_divide(double_divide(multiply(identity,identity),identity),inverse(identity)),
inference(step,[status(thm)],[t219,t7]) ).
cnf(t983,plain,
inverse(identity) = double_divide(inverse(multiply(identity,identity)),inverse(identity)),
inference(step,[status(thm)],[t982,t7]) ).
cnf(t17,plain,
multiply(identity,inverse(X1)) = inverse(multiply(identity,X1)),
inference(cp,[status(thm)],[t14,t14]) ).
cnf(t21,plain,
inverse(multiply(identity,X1)) = multiply(identity,inverse(X1)),
inference(orient,[status(thm)],[t17]) ).
cnf(t984,plain,
inverse(identity) = double_divide(multiply(identity,inverse(identity)),inverse(identity)),
inference(step,[status(thm)],[t983,t21]) ).
cnf(t985,plain,
inverse(identity) = double_divide(identity,inverse(identity)),
inference(step,[status(thm)],[t984,t100]) ).
cnf(t986,plain,
inverse(identity) = identity,
inference(step,[status(thm)],[t985,t9]) ).
cnf(t225,plain,
inverse(identity) = identity,
inference(orient,[status(thm)],[t986]) ).
cnf(t1040,plain,
double_divide(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1)))),identity) = X3,
inference(step,[status(thm)],[t69,t225]) ).
cnf(t1041,plain,
inverse(double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))) = X3,
inference(step,[status(thm)],[t1040,t7]) ).
cnf(t1042,plain,
multiply(double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))),X1) = X3,
inference(step,[status(thm)],[t1041,t10]) ).
cnf(t261,plain,
multiply(double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))),X1) = X3,
inference(rw,[status(thm)],[t1042]) ).
cnf(t1000,plain,
double_divide(multiply(identity,X1),identity) = double_divide(identity,X1),
inference(step,[status(thm)],[t100,t225]) ).
cnf(t1001,plain,
inverse(multiply(identity,X1)) = double_divide(identity,X1),
inference(step,[status(thm)],[t1000,t7]) ).
cnf(t1002,plain,
multiply(identity,inverse(X1)) = double_divide(identity,X1),
inference(step,[status(thm)],[t1001,t21]) ).
cnf(t248,plain,
multiply(identity,inverse(X1)) = double_divide(identity,X1),
inference(rw,[status(thm)],[t1002]) ).
cnf(t265,plain,
multiply(identity,inverse(X1)) = double_divide(identity,X1),
inference(orient,[status(thm)],[t248]) ).
cnf(t1049,plain,
double_divide(double_divide(X1,double_divide(identity,double_divide(X2,double_divide(identity,X1)))),inverse(identity)) = X2,
inference(step,[status(thm)],[t176,t225]) ).
cnf(t1050,plain,
double_divide(double_divide(X1,double_divide(identity,double_divide(X2,double_divide(identity,X1)))),identity) = X2,
inference(step,[status(thm)],[t1049,t225]) ).
cnf(t1051,plain,
inverse(double_divide(X1,double_divide(identity,double_divide(X2,double_divide(identity,X1))))) = X2,
inference(step,[status(thm)],[t1050,t7]) ).
cnf(t1052,plain,
multiply(double_divide(identity,double_divide(X2,double_divide(identity,X1))),X1) = X2,
inference(step,[status(thm)],[t1051,t10]) ).
cnf(t263,plain,
multiply(double_divide(identity,double_divide(X2,double_divide(identity,X1))),X1) = X2,
inference(rw,[status(thm)],[t1052]) ).
cnf(t15,plain,
multiply(identity,double_divide(X1,X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t14,t10]) ).
cnf(t29,plain,
multiply(identity,double_divide(X1,X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t15]) ).
cnf(t101,plain,
double_divide(identity,double_divide(X1,X2)) = double_divide(inverse(multiply(X2,X1)),inverse(identity)),
inference(cp,[status(thm)],[t100,t29]) ).
cnf(t109,plain,
double_divide(inverse(multiply(X1,X2)),inverse(identity)) = double_divide(identity,double_divide(X2,X1)),
inference(orient,[status(thm)],[t101]) ).
cnf(t1004,plain,
double_divide(inverse(multiply(X1,X2)),identity) = double_divide(identity,double_divide(X2,X1)),
inference(step,[status(thm)],[t109,t225]) ).
cnf(t1005,plain,
inverse(inverse(multiply(X1,X2))) = double_divide(identity,double_divide(X2,X1)),
inference(step,[status(thm)],[t1004,t7]) ).
cnf(t1006,plain,
multiply(identity,multiply(X1,X2)) = double_divide(identity,double_divide(X2,X1)),
inference(step,[status(thm)],[t1005,t14]) ).
cnf(t250,plain,
multiply(identity,multiply(X1,X2)) = double_divide(identity,double_divide(X2,X1)),
inference(rw,[status(thm)],[t1006]) ).
cnf(t311,plain,
double_divide(identity,double_divide(X1,X2)) = multiply(identity,multiply(X2,X1)),
inference(orient,[status(thm)],[t250]) ).
cnf(t1096,plain,
multiply(multiply(identity,multiply(double_divide(identity,X1),X2)),X1) = X2,
inference(step,[status(thm)],[t263,t311]) ).
cnf(t450,plain,
multiply(multiply(identity,multiply(double_divide(identity,X1),X2)),X1) = X2,
inference(orient,[status(thm)],[t1096]) ).
cnf(t1037,plain,
double_divide(double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X2))),identity) = X2,
inference(step,[status(thm)],[t84,t225]) ).
cnf(t1038,plain,
inverse(double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X2)))) = X2,
inference(step,[status(thm)],[t1037,t7]) ).
cnf(t1039,plain,
multiply(double_divide(double_divide(identity,X1),inverse(X2)),inverse(X1)) = X2,
inference(step,[status(thm)],[t1038,t10]) ).
cnf(t260,plain,
multiply(double_divide(double_divide(identity,X1),inverse(X2)),inverse(X1)) = X2,
inference(rw,[status(thm)],[t1039]) ).
cnf(t365,plain,
multiply(double_divide(double_divide(identity,X1),inverse(X2)),inverse(X1)) = X2,
inference(orient,[status(thm)],[t260]) ).
cnf(t369,plain,
identity = multiply(double_divide(double_divide(identity,X1),identity),inverse(X1)),
inference(cp,[status(thm)],[t365,t225]) ).
cnf(t1081,plain,
identity = multiply(inverse(double_divide(identity,X1)),inverse(X1)),
inference(step,[status(thm)],[t369,t7]) ).
cnf(t1082,plain,
identity = multiply(multiply(X1,identity),inverse(X1)),
inference(step,[status(thm)],[t1081,t10]) ).
cnf(t381,plain,
multiply(multiply(X1,identity),inverse(X1)) = identity,
inference(orient,[status(thm)],[t1082]) ).
cnf(t90,plain,
X1 = double_divide(double_divide(inverse(identity),double_divide(inverse(identity),inverse(X1))),inverse(identity)),
inference(cp,[status(thm)],[t84,t7]) ).
cnf(t116,plain,
double_divide(double_divide(inverse(identity),double_divide(inverse(identity),inverse(X1))),inverse(identity)) = X1,
inference(orient,[status(thm)],[t90]) ).
cnf(t1032,plain,
double_divide(double_divide(identity,double_divide(inverse(identity),inverse(X1))),inverse(identity)) = X1,
inference(step,[status(thm)],[t116,t225]) ).
cnf(t1033,plain,
double_divide(double_divide(identity,double_divide(identity,inverse(X1))),inverse(identity)) = X1,
inference(step,[status(thm)],[t1032,t225]) ).
cnf(t1034,plain,
double_divide(double_divide(identity,double_divide(identity,inverse(X1))),identity) = X1,
inference(step,[status(thm)],[t1033,t225]) ).
cnf(t1035,plain,
inverse(double_divide(identity,double_divide(identity,inverse(X1)))) = X1,
inference(step,[status(thm)],[t1034,t7]) ).
cnf(t1036,plain,
multiply(double_divide(identity,inverse(X1)),identity) = X1,
inference(step,[status(thm)],[t1035,t10]) ).
cnf(t259,plain,
multiply(double_divide(identity,inverse(X1)),identity) = X1,
inference(rw,[status(thm)],[t1036]) ).
cnf(t1053,plain,
inverse(multiply(identity,X1)) = double_divide(identity,X1),
inference(step,[status(thm)],[t21,t265]) ).
cnf(t266,plain,
inverse(multiply(identity,X1)) = double_divide(identity,X1),
inference(orient,[status(thm)],[t1053]) ).
cnf(t275,plain,
double_divide(identity,inverse(X1)) = inverse(double_divide(identity,X1)),
inference(cp,[status(thm)],[t266,t265]) ).
cnf(t1063,plain,
double_divide(identity,inverse(X1)) = multiply(X1,identity),
inference(step,[status(thm)],[t275,t10]) ).
cnf(t282,plain,
double_divide(identity,inverse(X1)) = multiply(X1,identity),
inference(orient,[status(thm)],[t1063]) ).
cnf(t1064,plain,
multiply(multiply(X1,identity),identity) = X1,
inference(step,[status(thm)],[t259,t282]) ).
cnf(t302,plain,
multiply(multiply(X1,identity),identity) = X1,
inference(orient,[status(thm)],[t1064]) ).
cnf(t383,plain,
identity = multiply(X1,inverse(multiply(X1,identity))),
inference(cp,[status(thm)],[t381,t302]) ).
cnf(t289,plain,
multiply(inverse(X1),identity) = inverse(multiply(X1,identity)),
inference(cp,[status(thm)],[t10,t282]) ).
cnf(t290,plain,
inverse(multiply(X1,identity)) = multiply(inverse(X1),identity),
inference(orient,[status(thm)],[t289]) ).
cnf(t1083,plain,
identity = multiply(X1,multiply(inverse(X1),identity)),
inference(step,[status(thm)],[t383,t290]) ).
cnf(t389,plain,
multiply(X1,multiply(inverse(X1),identity)) = identity,
inference(orient,[status(thm)],[t1083]) ).
cnf(t392,plain,
identity = multiply(inverse(X1),multiply(multiply(identity,X1),identity)),
inference(cp,[status(thm)],[t389,t14]) ).
cnf(t283,plain,
multiply(multiply(identity,X1),identity) = double_divide(identity,double_divide(identity,X1)),
inference(cp,[status(thm)],[t282,t266]) ).
cnf(t1067,plain,
multiply(multiply(identity,X1),identity) = multiply(identity,multiply(X1,identity)),
inference(step,[status(thm)],[t283,t311]) ).
cnf(t318,plain,
multiply(multiply(identity,X1),identity) = multiply(identity,multiply(X1,identity)),
inference(orient,[status(thm)],[t1067]) ).
cnf(t1088,plain,
identity = multiply(inverse(X1),multiply(identity,multiply(X1,identity))),
inference(step,[status(thm)],[t392,t318]) ).
cnf(t421,plain,
multiply(inverse(X1),multiply(identity,multiply(X1,identity))) = identity,
inference(orient,[status(thm)],[t1088]) ).
cnf(t422,plain,
identity = multiply(double_divide(identity,X1),multiply(identity,multiply(multiply(identity,X1),identity))),
inference(cp,[status(thm)],[t421,t266]) ).
cnf(t1089,plain,
identity = multiply(double_divide(identity,X1),multiply(identity,multiply(identity,multiply(X1,identity)))),
inference(step,[status(thm)],[t422,t318]) ).
cnf(t105,plain,
multiply(inverse(identity),multiply(identity,X1)) = inverse(double_divide(identity,X1)),
inference(cp,[status(thm)],[t10,t100]) ).
cnf(t973,plain,
multiply(inverse(identity),multiply(identity,X1)) = multiply(X1,identity),
inference(step,[status(thm)],[t105,t10]) ).
cnf(t107,plain,
multiply(inverse(identity),multiply(identity,X1)) = multiply(X1,identity),
inference(orient,[status(thm)],[t973]) ).
cnf(t999,plain,
multiply(identity,multiply(identity,X1)) = multiply(X1,identity),
inference(step,[status(thm)],[t107,t225]) ).
cnf(t247,plain,
multiply(identity,multiply(identity,X1)) = multiply(X1,identity),
inference(rw,[status(thm)],[t999]) ).
cnf(t298,plain,
multiply(identity,multiply(identity,X1)) = multiply(X1,identity),
inference(orient,[status(thm)],[t247]) ).
cnf(t1090,plain,
identity = multiply(double_divide(identity,X1),multiply(multiply(X1,identity),identity)),
inference(step,[status(thm)],[t1089,t298]) ).
cnf(t1091,plain,
identity = multiply(double_divide(identity,X1),X1),
inference(step,[status(thm)],[t1090,t302]) ).
cnf(t428,plain,
multiply(double_divide(identity,X1),X1) = identity,
inference(orient,[status(thm)],[t1091]) ).
cnf(t451,plain,
X1 = multiply(multiply(identity,identity),X1),
inference(cp,[status(thm)],[t450,t428]) ).
cnf(t12,plain,
multiply(inverse(X1),X1) = inverse(identity),
inference(cp,[status(thm)],[t10,t9]) ).
cnf(t18,plain,
multiply(inverse(X1),X1) = inverse(identity),
inference(orient,[status(thm)],[t12]) ).
cnf(t987,plain,
multiply(inverse(X1),X1) = identity,
inference(step,[status(thm)],[t18,t225]) ).
cnf(t226,plain,
multiply(inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t987]) ).
cnf(t239,plain,
identity = multiply(identity,identity),
inference(cp,[status(thm)],[t226,t225]) ).
cnf(t264,plain,
multiply(identity,identity) = identity,
inference(orient,[status(thm)],[t239]) ).
cnf(t1097,plain,
X1 = multiply(identity,X1),
inference(step,[status(thm)],[t451,t264]) ).
cnf(t459,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t1097]) ).
cnf(t1104,plain,
inverse(X1) = double_divide(identity,X1),
inference(step,[status(thm)],[t265,t459]) ).
cnf(t468,plain,
inverse(X1) = double_divide(identity,X1),
inference(rw,[status(thm)],[t1104]) ).
cnf(t494,plain,
double_divide(identity,X1) = inverse(X1),
inference(orient,[status(thm)],[t468]) ).
cnf(t1141,plain,
multiply(double_divide(inverse(X2),double_divide(X3,double_divide(X2,X1))),X1) = X3,
inference(step,[status(thm)],[t261,t494]) ).
cnf(t1116,plain,
multiply(multiply(double_divide(identity,X1),X2),X1) = X2,
inference(step,[status(thm)],[t450,t459]) ).
cnf(t480,plain,
multiply(multiply(double_divide(identity,X1),X2),X1) = X2,
inference(rw,[status(thm)],[t1116]) ).
cnf(t1131,plain,
multiply(multiply(inverse(X1),X2),X1) = X2,
inference(step,[status(thm)],[t480,t494]) ).
cnf(t507,plain,
multiply(multiply(inverse(X1),X2),X1) = X2,
inference(orient,[status(thm)],[t1131]) ).
cnf(t1098,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t14,t459]) ).
cnf(t460,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t1098]) ).
cnf(t510,plain,
X1 = multiply(multiply(X2,X1),inverse(X2)),
inference(cp,[status(thm)],[t507,t460]) ).
cnf(t514,plain,
multiply(multiply(X1,X2),inverse(X1)) = X2,
inference(orient,[status(thm)],[t510]) ).
cnf(t518,plain,
inverse(X1) = multiply(X2,inverse(multiply(X1,X2))),
inference(cp,[status(thm)],[t514,t514]) ).
cnf(t1106,plain,
double_divide(X1,X2) = inverse(multiply(X2,X1)),
inference(step,[status(thm)],[t29,t459]) ).
cnf(t470,plain,
double_divide(X1,X2) = inverse(multiply(X2,X1)),
inference(rw,[status(thm)],[t1106]) ).
cnf(t504,plain,
inverse(multiply(X1,X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t470]) ).
cnf(t1132,plain,
inverse(X1) = multiply(X2,double_divide(X2,X1)),
inference(step,[status(thm)],[t518,t504]) ).
cnf(t522,plain,
multiply(X1,double_divide(X1,X2)) = inverse(X2),
inference(orient,[status(thm)],[t1132]) ).
cnf(t527,plain,
double_divide(inverse(X1),X2) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t507,t522]) ).
cnf(t535,plain,
double_divide(inverse(X1),X2) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t527]) ).
cnf(t1142,plain,
multiply(multiply(inverse(double_divide(X3,double_divide(X2,X1))),X2),X1) = X3,
inference(step,[status(thm)],[t1141,t535]) ).
cnf(t1143,plain,
multiply(multiply(multiply(double_divide(X2,X1),X3),X2),X1) = X3,
inference(step,[status(thm)],[t1142,t10]) ).
cnf(t657,plain,
multiply(multiply(multiply(double_divide(X1,X2),X3),X1),X2) = X3,
inference(orient,[status(thm)],[t1143]) ).
cnf(t717,plain,
multiply(multiply(multiply(double_divide(X1,X2),X3),X1),X2) = X3,
inference(rw,[status(thm)],[t657]) ).
cnf(t1128,plain,
multiply(double_divide(inverse(X1),inverse(X2)),inverse(X1)) = X2,
inference(step,[status(thm)],[t365,t494]) ).
cnf(t498,plain,
multiply(double_divide(inverse(X1),inverse(X2)),inverse(X1)) = X2,
inference(rw,[status(thm)],[t1128]) ).
cnf(t544,plain,
multiply(X1,inverse(X2)) = inverse(multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t10,t535]) ).
cnf(t1134,plain,
multiply(X1,inverse(X2)) = double_divide(X2,inverse(X1)),
inference(step,[status(thm)],[t544,t504]) ).
cnf(t545,plain,
double_divide(X1,inverse(X2)) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t1134]) ).
cnf(t548,plain,
multiply(double_divide(X1,X2),inverse(X3)) = double_divide(X3,multiply(X2,X1)),
inference(cp,[status(thm)],[t545,t10]) ).
cnf(t603,plain,
multiply(double_divide(X1,X2),inverse(X3)) = double_divide(X3,multiply(X2,X1)),
inference(orient,[status(thm)],[t548]) ).
cnf(t1139,plain,
double_divide(X1,multiply(inverse(X2),inverse(X1))) = X2,
inference(step,[status(thm)],[t498,t603]) ).
cnf(t523,plain,
double_divide(X1,X2) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t514,t522]) ).
cnf(t556,plain,
multiply(inverse(X1),inverse(X2)) = double_divide(X2,X1),
inference(orient,[status(thm)],[t523]) ).
cnf(t1140,plain,
double_divide(X1,double_divide(X1,X2)) = X2,
inference(step,[status(thm)],[t1139,t556]) ).
cnf(t606,plain,
double_divide(X1,double_divide(X1,X2)) = X2,
inference(orient,[status(thm)],[t1140]) ).
cnf(t621,plain,
inverse(double_divide(X1,X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t522,t606]) ).
cnf(t1144,plain,
multiply(X2,X1) = multiply(X1,X2),
inference(step,[status(thm)],[t621,t10]) ).
cnf(t699,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t1144]) ).
cnf(t1147,plain,
multiply(X2,multiply(multiply(double_divide(X1,X2),X3),X1)) = X3,
inference(step,[status(thm)],[t717,t699]) ).
cnf(t1148,plain,
multiply(X2,multiply(X1,multiply(double_divide(X1,X2),X3))) = X3,
inference(step,[status(thm)],[t1147,t699]) ).
cnf(t903,plain,
multiply(X1,multiply(X2,multiply(double_divide(X2,X1),X3))) = X3,
inference(orient,[status(thm)],[t1148]) ).
cnf(t524,plain,
double_divide(double_divide(X1,X2),X1) = inverse(inverse(X2)),
inference(cp,[status(thm)],[t504,t522]) ).
cnf(t1133,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(step,[status(thm)],[t524,t460]) ).
cnf(t528,plain,
double_divide(double_divide(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t1133]) ).
cnf(t530,plain,
inverse(X1) = multiply(double_divide(X1,X2),X2),
inference(cp,[status(thm)],[t522,t528]) ).
cnf(t554,plain,
multiply(double_divide(X1,X2),X2) = inverse(X1),
inference(orient,[status(thm)],[t530]) ).
cnf(t618,plain,
inverse(X1) = multiply(X2,double_divide(X1,X2)),
inference(cp,[status(thm)],[t554,t606]) ).
cnf(t642,plain,
multiply(X1,double_divide(X2,X1)) = inverse(X2),
inference(orient,[status(thm)],[t618]) ).
cnf(t646,plain,
inverse(inverse(X1)) = multiply(X2,multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t642,t535]) ).
cnf(t1145,plain,
X1 = multiply(X2,multiply(inverse(X2),X1)),
inference(step,[status(thm)],[t646,t460]) ).
cnf(t718,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t1145]) ).
cnf(t910,plain,
multiply(inverse(double_divide(X1,X2)),X3) = multiply(X2,multiply(X1,X3)),
inference(cp,[status(thm)],[t903,t718]) ).
cnf(t1149,plain,
multiply(multiply(X2,X1),X3) = multiply(X2,multiply(X1,X3)),
inference(step,[status(thm)],[t910,t10]) ).
cnf(t940,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t1149]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t940]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP583-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 15:08:12 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.15/1.22 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.15/1.22 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------