%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP413-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 : n012.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:26:16 PM UTC 2026
% Result : Unsatisfiable 14.84s 2.25s
% Output : CNFRefutation 14.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 4
% Syntax : Number of clauses : 171 ( 171 unt; 0 nHn; 27 RR)
% Number of literals : 171 ( 170 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 226 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2))) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2))) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t1,axiom,
sFlat0 = inverse(b2),
introduced(definition) ).
cnf(t11,plain,
inverse(b2) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t12,plain,
X1 = multiply(X2,inverse(multiply(multiply(multiply(sFlat0,b2),inverse(multiply(inverse(multiply(X2,inverse(b2))),X1))),b2))),
inference(cp,[status(thm)],[t4,t11]) ).
cnf(t2,axiom,
sFlat1 = multiply(inverse(b2),b2),
introduced(definition) ).
cnf(t8,plain,
multiply(inverse(b2),b2) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t1994,plain,
multiply(sFlat0,b2) = sFlat1,
inference(step,[status(thm)],[t8,t11]) ).
cnf(t14,plain,
multiply(sFlat0,b2) = sFlat1,
inference(rw,[status(thm)],[t1994]) ).
cnf(t16,plain,
multiply(sFlat0,b2) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t1995,plain,
X1 = multiply(X2,inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,inverse(b2))),X1))),b2))),
inference(step,[status(thm)],[t12,t16]) ).
cnf(t1996,plain,
X1 = multiply(X2,inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),X1))),b2))),
inference(step,[status(thm)],[t1995,t11]) ).
cnf(t17,plain,
multiply(X1,inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2))) = X2,
inference(orient,[status(thm)],[t1996]) ).
cnf(t19,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),sFlat0)),X2))),b2)) = multiply(X1,inverse(multiply(multiply(sFlat1,inverse(X2)),b2))),
inference(cp,[status(thm)],[t17,t17]) ).
cnf(t22,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),sFlat0)),X2))),b2)) = multiply(X1,inverse(multiply(multiply(sFlat1,inverse(X2)),b2))),
inference(orient,[status(thm)],[t19]) ).
cnf(t24,plain,
X1 = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(sFlat1,inverse(X1)),b2)))),
inference(cp,[status(thm)],[t17,t22]) ).
cnf(t27,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,inverse(X2)),b2)))) = X2,
inference(orient,[status(thm)],[t24]) ).
cnf(t30,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(X1,b2)))),
inference(cp,[status(thm)],[t27,t17]) ).
cnf(t42,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(X1,b2)))),
inference(orient,[status(thm)],[t30]) ).
cnf(t46,plain,
multiply(inverse(multiply(sFlat1,sFlat0)),X1) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(X1,b2))))))),
inference(cp,[status(thm)],[t27,t42]) ).
cnf(t71,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(X3,b2))))))) = multiply(inverse(multiply(sFlat1,sFlat0)),X3),
inference(orient,[status(thm)],[t46]) ).
cnf(t31,plain,
b2 = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,sFlat0),b2)))),
inference(cp,[status(thm)],[t27,t11]) ).
cnf(t33,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,sFlat0),b2)))) = b2,
inference(orient,[status(thm)],[t31]) ).
cnf(t73,plain,
multiply(inverse(multiply(sFlat1,sFlat0)),multiply(sFlat1,sFlat0)) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(b2))),
inference(cp,[status(thm)],[t71,t33]) ).
cnf(t1998,plain,
multiply(inverse(multiply(sFlat1,sFlat0)),multiply(sFlat1,sFlat0)) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)),
inference(step,[status(thm)],[t73,t11]) ).
cnf(t82,plain,
multiply(inverse(multiply(sFlat1,sFlat0)),multiply(sFlat1,sFlat0)) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)),
inference(orient,[status(thm)],[t1998]) ).
cnf(t85,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,sFlat0),b2)))) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)))),b2),
inference(cp,[status(thm)],[t42,t82]) ).
cnf(t1999,plain,
b2 = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)))),b2),
inference(step,[status(thm)],[t85,t33]) ).
cnf(t92,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2) = b2,
inference(orient,[status(thm)],[t1999]) ).
cnf(t28,plain,
multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),sFlat0)),X2) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,multiply(X1,inverse(multiply(multiply(sFlat1,inverse(X2)),b2))))),
inference(cp,[status(thm)],[t27,t22]) ).
cnf(t34,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,multiply(X2,inverse(multiply(multiply(sFlat1,inverse(X3)),b2))))) = multiply(inverse(multiply(inverse(multiply(X2,sFlat0)),sFlat0)),X3),
inference(orient,[status(thm)],[t28]) ).
cnf(t35,plain,
multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),sFlat0)),multiply(inverse(multiply(X1,sFlat0)),X2)) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)),
inference(cp,[status(thm)],[t34,t17]) ).
cnf(t181,plain,
multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),sFlat0)),multiply(inverse(multiply(X1,sFlat0)),X2)) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)),
inference(orient,[status(thm)],[t35]) ).
cnf(t196,plain,
multiply(X1,inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2))) = inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)))),b2)),
inference(cp,[status(thm)],[t22,t181]) ).
cnf(t2001,plain,
X2 = inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)))),b2)),
inference(step,[status(thm)],[t196,t17]) ).
cnf(t220,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)))),b2)) = X2,
inference(orient,[status(thm)],[t2001]) ).
cnf(t230,plain,
b2 = inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1))),b2)),
inference(cp,[status(thm)],[t220,t16]) ).
cnf(t246,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1))),b2)) = b2,
inference(orient,[status(thm)],[t230]) ).
cnf(t247,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,b2)),
inference(cp,[status(thm)],[t27,t246]) ).
cnf(t258,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,b2)) = multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1),
inference(orient,[status(thm)],[t247]) ).
cnf(t72,plain,
multiply(inverse(multiply(sFlat1,sFlat0)),multiply(sFlat1,inverse(X1))) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t71,t27]) ).
cnf(t101,plain,
multiply(inverse(multiply(sFlat1,sFlat0)),multiply(sFlat1,inverse(X1))) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t72]) ).
cnf(t107,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,inverse(X2)),b2)))) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(X2))))),b2),
inference(cp,[status(thm)],[t42,t101]) ).
cnf(t2000,plain,
X2 = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(X2))))),b2),
inference(step,[status(thm)],[t107,t27]) ).
cnf(t117,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(X2))))),b2) = X2,
inference(orient,[status(thm)],[t2000]) ).
cnf(t261,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1) = multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(X2))))),sFlat0)),X2),
inference(cp,[status(thm)],[t258,t117]) ).
cnf(t340,plain,
multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(X2))))),sFlat0)),X2) = multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1),
inference(orient,[status(thm)],[t261]) ).
cnf(t372,plain,
b2 = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(sFlat0))))),sFlat0)),sFlat0)))),b2),
inference(cp,[status(thm)],[t92,t340]) ).
cnf(t2003,plain,
b2 = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)))),b2),
inference(step,[status(thm)],[t372,t340]) ).
cnf(t402,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)))),b2) = b2,
inference(orient,[status(thm)],[t2003]) ).
cnf(t404,plain,
multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(b2))),
inference(cp,[status(thm)],[t27,t402]) ).
cnf(t2004,plain,
multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)),
inference(step,[status(thm)],[t404,t11]) ).
cnf(t412,plain,
multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)),
inference(orient,[status(thm)],[t2004]) ).
cnf(t119,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),X3))),b2),
inference(cp,[status(thm)],[t117,t4]) ).
cnf(t138,plain,
multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),X3))),b2),
inference(orient,[status(thm)],[t119]) ).
cnf(t418,plain,
multiply(inverse(multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)),multiply(inverse(multiply(sFlat0,sFlat0)),sFlat1)) = multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),multiply(multiply(multiply(inverse(sFlat0),sFlat0),inverse(multiply(inverse(multiply(X1,inverse(sFlat0))),X2))),sFlat0)),
inference(cp,[status(thm)],[t412,t138]) ).
cnf(t2006,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),multiply(multiply(multiply(inverse(sFlat0),sFlat0),inverse(multiply(inverse(multiply(X1,inverse(sFlat0))),X2))),sFlat0)),
inference(step,[status(thm)],[t418,t412]) ).
cnf(t2007,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),
inference(step,[status(thm)],[t2006,t138]) ).
cnf(t1003,plain,
multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)) = multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)),
inference(orient,[status(thm)],[t2007]) ).
cnf(t221,plain,
X1 = inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(sFlat1,X1),b2))))),
inference(cp,[status(thm)],[t220,t42]) ).
cnf(t294,plain,
inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,X2),b2))))) = X2,
inference(orient,[status(thm)],[t221]) ).
cnf(t1011,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(multiply(multiply(sFlat1,X1),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(sFlat1,X1),b2)))))),b2)),
inference(cp,[status(thm)],[t1003,t294]) ).
cnf(t48,plain,
X1 = multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(X1,b2)))))),
inference(cp,[status(thm)],[t17,t42]) ).
cnf(t59,plain,
multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(X2,b2)))))) = X2,
inference(orient,[status(thm)],[t48]) ).
cnf(t60,plain,
sFlat0 = multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(sFlat1))))),
inference(cp,[status(thm)],[t59,t16]) ).
cnf(t65,plain,
multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(sFlat1))))) = sFlat0,
inference(orient,[status(thm)],[t60]) ).
cnf(t1009,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(multiply(sFlat0,b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(sFlat1))))),b2)),
inference(cp,[status(thm)],[t1003,t65]) ).
cnf(t2008,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(sFlat1),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(sFlat1))))),b2)),
inference(step,[status(thm)],[t1009,t16]) ).
cnf(t236,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)))),b2) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(multiply(sFlat1,X2),b2)))),
inference(cp,[status(thm)],[t27,t220]) ).
cnf(t552,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)))),b2) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,inverse(multiply(multiply(sFlat1,X2),b2)))),
inference(orient,[status(thm)],[t236]) ).
cnf(t2009,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(sFlat1),multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,inverse(multiply(multiply(sFlat1,inverse(sFlat1)),b2))))),
inference(step,[status(thm)],[t2008,t552]) ).
cnf(t2010,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(sFlat1),sFlat1),
inference(step,[status(thm)],[t2009,t27]) ).
cnf(t1083,plain,
multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)) = multiply(inverse(sFlat1),sFlat1),
inference(orient,[status(thm)],[t2010]) ).
cnf(t2036,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(inverse(multiply(multiply(sFlat1,X1),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(sFlat1,X1),b2)))))),b2)),
inference(step,[status(thm)],[t1011,t1083]) ).
cnf(t2011,plain,
multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)) = multiply(inverse(sFlat1),sFlat1),
inference(step,[status(thm)],[t1003,t1083]) ).
cnf(t1084,plain,
multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2)) = multiply(inverse(sFlat1),sFlat1),
inference(orient,[status(thm)],[t2011]) ).
cnf(t199,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)),
inference(cp,[status(thm)],[t181,t181]) ).
cnf(t310,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)) = multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)),
inference(orient,[status(thm)],[t199]) ).
cnf(t1086,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)),
inference(cp,[status(thm)],[t1083,t310]) ).
cnf(t1119,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)) = multiply(inverse(sFlat1),sFlat1),
inference(orient,[status(thm)],[t1086]) ).
cnf(t1123,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),sFlat1))),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2)),
inference(cp,[status(thm)],[t1084,t1119]) ).
cnf(t1098,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,sFlat0),b2)))) = multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),sFlat1))),b2),
inference(cp,[status(thm)],[t552,t1083]) ).
cnf(t2013,plain,
b2 = multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),sFlat1))),b2),
inference(step,[status(thm)],[t1098,t33]) ).
cnf(t1100,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),sFlat1))),b2) = b2,
inference(orient,[status(thm)],[t2013]) ).
cnf(t2017,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(inverse(b2),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2)),
inference(step,[status(thm)],[t1123,t1100]) ).
cnf(t2018,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(sFlat0,multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),b2)),
inference(step,[status(thm)],[t2017,t11]) ).
cnf(t2019,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(sFlat0,multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,inverse(multiply(multiply(sFlat1,sFlat0),b2))))),
inference(step,[status(thm)],[t2018,t552]) ).
cnf(t2020,plain,
multiply(inverse(sFlat1),sFlat1) = multiply(sFlat0,b2),
inference(step,[status(thm)],[t2019,t33]) ).
cnf(t2021,plain,
multiply(inverse(sFlat1),sFlat1) = sFlat1,
inference(step,[status(thm)],[t2020,t16]) ).
cnf(t1134,plain,
multiply(inverse(sFlat1),sFlat1) = sFlat1,
inference(orient,[status(thm)],[t2021]) ).
cnf(t2037,plain,
sFlat1 = multiply(inverse(multiply(multiply(sFlat1,X1),b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(multiply(sFlat1,X1),b2)))))),b2)),
inference(step,[status(thm)],[t2036,t1134]) ).
cnf(t2038,plain,
sFlat1 = multiply(inverse(multiply(multiply(sFlat1,X1),b2)),multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,inverse(multiply(multiply(sFlat1,inverse(multiply(multiply(sFlat1,X1),b2))),b2))))),
inference(step,[status(thm)],[t2037,t552]) ).
cnf(t2039,plain,
sFlat1 = multiply(inverse(multiply(multiply(sFlat1,X1),b2)),multiply(multiply(sFlat1,X1),b2)),
inference(step,[status(thm)],[t2038,t27]) ).
cnf(t1259,plain,
multiply(inverse(multiply(multiply(sFlat1,X1),b2)),multiply(multiply(sFlat1,X1),b2)) = sFlat1,
inference(orient,[status(thm)],[t2039]) ).
cnf(t1264,plain,
sFlat1 = multiply(inverse(multiply(X1,b2)),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(multiply(X1,b2)))))),b2)),
inference(cp,[status(thm)],[t1259,t59]) ).
cnf(t2041,plain,
sFlat1 = multiply(inverse(multiply(X1,b2)),multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,inverse(multiply(multiply(sFlat1,inverse(multiply(X1,b2))),b2))))),
inference(step,[status(thm)],[t1264,t552]) ).
cnf(t2042,plain,
sFlat1 = multiply(inverse(multiply(X1,b2)),multiply(X1,b2)),
inference(step,[status(thm)],[t2041,t27]) ).
cnf(t1286,plain,
multiply(inverse(multiply(X1,b2)),multiply(X1,b2)) = sFlat1,
inference(orient,[status(thm)],[t2042]) ).
cnf(t1291,plain,
sFlat1 = multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(multiply(multiply(sFlat1,X2),b2))))),multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)))),b2)),
inference(cp,[status(thm)],[t1286,t552]) ).
cnf(t2045,plain,
sFlat1 = multiply(X2,multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,X2)))),b2)),
inference(step,[status(thm)],[t1291,t294]) ).
cnf(t2046,plain,
sFlat1 = multiply(X2,multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,inverse(multiply(multiply(sFlat1,X2),b2))))),
inference(step,[status(thm)],[t2045,t552]) ).
cnf(t1334,plain,
multiply(X1,multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,inverse(multiply(multiply(sFlat1,X1),b2))))) = sFlat1,
inference(orient,[status(thm)],[t2046]) ).
cnf(t1337,plain,
sFlat1 = multiply(inverse(X1),X1),
inference(cp,[status(thm)],[t1334,t27]) ).
cnf(t1360,plain,
multiply(inverse(X1),X1) = sFlat1,
inference(orient,[status(thm)],[t1337]) ).
cnf(t1443,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)) = multiply(inverse(sFlat1),multiply(inverse(sFlat0),X2)),
inference(cp,[status(thm)],[t310,t1360]) ).
cnf(t1490,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,X2)) = multiply(inverse(sFlat1),multiply(inverse(sFlat0),X2)),
inference(orient,[status(thm)],[t1443]) ).
cnf(t2071,plain,
multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(X2,b2)))))) = X2,
inference(step,[status(thm)],[t59,t1490]) ).
cnf(t1518,plain,
multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(X2,b2)))))) = X2,
inference(rw,[status(thm)],[t2071]) ).
cnf(t1576,plain,
multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(X1,b2)))))) = X1,
inference(orient,[status(thm)],[t1518]) ).
cnf(t1501,plain,
multiply(X1,inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X2))),b2))) = inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),X2)))),b2)),
inference(cp,[status(thm)],[t22,t1490]) ).
cnf(t2092,plain,
X2 = inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),X2)))),b2)),
inference(step,[status(thm)],[t1501,t17]) ).
cnf(t1556,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),X1)))),b2)) = X1,
inference(orient,[status(thm)],[t2092]) ).
cnf(t2047,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),X3))),b2),
inference(step,[status(thm)],[t138,t1360]) ).
cnf(t1460,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X2,sFlat0)),X3))),b2),
inference(rw,[status(thm)],[t2047]) ).
cnf(t1636,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2) = multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),X3))),b2),
inference(orient,[status(thm)],[t1460]) ).
cnf(t1637,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,inverse(X2))))),b2) = multiply(multiply(sFlat1,inverse(sFlat1)),X2),
inference(cp,[status(thm)],[t1636,t1360]) ).
cnf(t2100,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(X2))))),b2) = multiply(multiply(sFlat1,inverse(sFlat1)),X2),
inference(step,[status(thm)],[t1637,t1490]) ).
cnf(t1658,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(X1))))),b2) = multiply(multiply(sFlat1,inverse(sFlat1)),X1),
inference(orient,[status(thm)],[t2100]) ).
cnf(t1678,plain,
inverse(X1) = inverse(multiply(multiply(sFlat1,inverse(sFlat1)),X1)),
inference(cp,[status(thm)],[t1556,t1658]) ).
cnf(t1699,plain,
inverse(multiply(multiply(sFlat1,inverse(sFlat1)),X1)) = inverse(X1),
inference(orient,[status(thm)],[t1678]) ).
cnf(t2065,plain,
multiply(X1,multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))))) = sFlat1,
inference(step,[status(thm)],[t1334,t1490]) ).
cnf(t1513,plain,
multiply(X1,multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))))) = sFlat1,
inference(rw,[status(thm)],[t2065]) ).
cnf(t1585,plain,
multiply(X1,multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))))) = sFlat1,
inference(orient,[status(thm)],[t1513]) ).
cnf(t1701,plain,
inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,multiply(sFlat1,inverse(sFlat1))),b2))))) = inverse(sFlat1),
inference(cp,[status(thm)],[t1699,t1585]) ).
cnf(t2068,plain,
inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X2),b2))))) = X2,
inference(step,[status(thm)],[t294,t1490]) ).
cnf(t1516,plain,
inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X2),b2))))) = X2,
inference(rw,[status(thm)],[t2068]) ).
cnf(t1571,plain,
inverse(multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))))) = X1,
inference(orient,[status(thm)],[t1516]) ).
cnf(t2110,plain,
multiply(sFlat1,inverse(sFlat1)) = inverse(sFlat1),
inference(step,[status(thm)],[t1701,t1571]) ).
cnf(t1714,plain,
multiply(sFlat1,inverse(sFlat1)) = inverse(sFlat1),
inference(orient,[status(thm)],[t2110]) ).
cnf(t2115,plain,
inverse(multiply(inverse(sFlat1),X1)) = inverse(X1),
inference(step,[status(thm)],[t1699,t1714]) ).
cnf(t1725,plain,
inverse(multiply(inverse(sFlat1),X1)) = inverse(X1),
inference(rw,[status(thm)],[t2115]) ).
cnf(t1736,plain,
inverse(multiply(inverse(sFlat1),X1)) = inverse(X1),
inference(orient,[status(thm)],[t1725]) ).
cnf(t2120,plain,
multiply(sFlat1,inverse(multiply(inverse(sFlat0),inverse(multiply(X1,b2))))) = X1,
inference(step,[status(thm)],[t1576,t1736]) ).
cnf(t1755,plain,
multiply(sFlat1,inverse(multiply(inverse(sFlat0),inverse(multiply(X1,b2))))) = X1,
inference(rw,[status(thm)],[t2120]) ).
cnf(t1799,plain,
multiply(sFlat1,inverse(multiply(inverse(sFlat0),inverse(multiply(X1,b2))))) = X1,
inference(orient,[status(thm)],[t1755]) ).
cnf(t1721,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(multiply(sFlat1,inverse(multiply(inverse(inverse(sFlat1)),X1))),sFlat1),
inference(cp,[status(thm)],[t1636,t1714]) ).
cnf(t2055,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(X1,b2)))),
inference(step,[status(thm)],[t42,t1490]) ).
cnf(t1504,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(X1,b2)))),
inference(rw,[status(thm)],[t2055]) ).
cnf(t1620,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(X1,b2)))),
inference(orient,[status(thm)],[t1504]) ).
cnf(t2064,plain,
multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X2)),b2)))) = X2,
inference(step,[status(thm)],[t27,t1490]) ).
cnf(t1512,plain,
multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X2)),b2)))) = X2,
inference(rw,[status(thm)],[t2064]) ).
cnf(t1563,plain,
multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X1)),b2)))) = X1,
inference(orient,[status(thm)],[t1512]) ).
cnf(t1745,plain,
multiply(inverse(sFlat1),X1) = multiply(inverse(sFlat1),multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X1)),b2)))),
inference(cp,[status(thm)],[t1563,t1736]) ).
cnf(t2125,plain,
multiply(inverse(sFlat1),X1) = X1,
inference(step,[status(thm)],[t1745,t1563]) ).
cnf(t1760,plain,
multiply(inverse(sFlat1),X1) = X1,
inference(orient,[status(thm)],[t2125]) ).
cnf(t2130,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(sFlat0),inverse(multiply(X1,b2))),
inference(step,[status(thm)],[t1620,t1760]) ).
cnf(t1765,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(sFlat1,sFlat0)),X1))),b2) = multiply(inverse(sFlat0),inverse(multiply(X1,b2))),
inference(orient,[status(thm)],[t2130]) ).
cnf(t2151,plain,
multiply(inverse(sFlat0),inverse(multiply(X1,b2))) = multiply(multiply(sFlat1,inverse(multiply(inverse(inverse(sFlat1)),X1))),sFlat1),
inference(step,[status(thm)],[t1721,t1765]) ).
cnf(t1768,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(multiply(inverse(sFlat1),sFlat0)),X1))),b2) = multiply(multiply(sFlat1,inverse(multiply(inverse(inverse(X2)),X1))),X2),
inference(cp,[status(thm)],[t1636,t1760]) ).
cnf(t2147,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat0),X1))),b2) = multiply(multiply(sFlat1,inverse(multiply(inverse(inverse(X2)),X1))),X2),
inference(step,[status(thm)],[t1768,t1736]) ).
cnf(t1408,plain,
X1 = multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),X1))),b2))),
inference(cp,[status(thm)],[t17,t1360]) ).
cnf(t1550,plain,
multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat1),X1))),b2))) = X1,
inference(orient,[status(thm)],[t1408]) ).
cnf(t2124,plain,
multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X1)),b2))) = X1,
inference(step,[status(thm)],[t1550,t1736]) ).
cnf(t1759,plain,
multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X1)),b2))) = X1,
inference(rw,[status(thm)],[t2124]) ).
cnf(t1819,plain,
multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,inverse(X1)),b2))) = X1,
inference(orient,[status(thm)],[t1759]) ).
cnf(t2123,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat0),X1))),b2)) = X1,
inference(step,[status(thm)],[t1556,t1736]) ).
cnf(t1758,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat0),X1))),b2)) = X1,
inference(rw,[status(thm)],[t2123]) ).
cnf(t1813,plain,
inverse(multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat0),X1))),b2)) = X1,
inference(orient,[status(thm)],[t1758]) ).
cnf(t1823,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat0),X1))),b2) = multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))),
inference(cp,[status(thm)],[t1819,t1813]) ).
cnf(t1882,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(sFlat0),X1))),b2) = multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))),
inference(orient,[status(thm)],[t1823]) ).
cnf(t2148,plain,
multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))) = multiply(multiply(sFlat1,inverse(multiply(inverse(inverse(X2)),X1))),X2),
inference(step,[status(thm)],[t2147,t1882]) ).
cnf(t1889,plain,
multiply(multiply(sFlat1,inverse(multiply(inverse(inverse(X1)),X2))),X1) = multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X2),b2))),
inference(orient,[status(thm)],[t2148]) ).
cnf(t2152,plain,
multiply(inverse(sFlat0),inverse(multiply(X1,b2))) = multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))),
inference(step,[status(thm)],[t2151,t1889]) ).
cnf(t1943,plain,
multiply(inverse(sFlat0),inverse(multiply(multiply(sFlat1,X1),b2))) = multiply(inverse(sFlat0),inverse(multiply(X1,b2))),
inference(orient,[status(thm)],[t2152]) ).
cnf(t1959,plain,
multiply(sFlat1,X1) = multiply(sFlat1,inverse(multiply(inverse(sFlat0),inverse(multiply(X1,b2))))),
inference(cp,[status(thm)],[t1799,t1943]) ).
cnf(t2163,plain,
multiply(sFlat1,X1) = X1,
inference(step,[status(thm)],[t1959,t1799]) ).
cnf(t1969,plain,
multiply(sFlat1,X1) = X1,
inference(orient,[status(thm)],[t2163]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(sFlat1,a2) != a2,
inference(rw,[status(thm)],[goal_0,t1360]) ).
cnf(g0_1,plain,
a2 != a2,
inference(rw,[status(thm)],[g0_0,t1969]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP413-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Wed Sep 23 14:41:21 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.84/2.25 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.84/2.25 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------