%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP401-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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:05 PM UTC 2026
% Result : Unsatisfiable 52.65s 17.53s
% Output : Proof 52.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 10
% Syntax : Number of formulae : 203 ( 195 unt; 0 def)
% Number of atoms : 211 ( 210 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 25 ( 17 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-4 aty)
% Number of variables : 223 ( 2 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
sFlat0 = commutator(a,b),
introduced(definition) ).
cnf(t44,plain,
commutator(a,b) = sFlat0,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sFlat1 = multiply(commutator(a,b),c),
introduced(definition) ).
cnf(t32,plain,
multiply(commutator(a,b),c) = sFlat1,
inference(orient,[status(thm)],[t7]) ).
cnf(t80295,plain,
multiply(sFlat0,c) = sFlat1,
inference(step,[status(thm)],[t32,t44]) ).
cnf(t49,plain,
multiply(sFlat0,c) = sFlat1,
inference(rw,[status(thm)],[t80295]) ).
cnf(t56,plain,
multiply(sFlat0,c) = sFlat1,
inference(orient,[status(thm)],[t49]) ).
cnf(t8,axiom,
sFlat2 = multiply(c,commutator(a,b)),
introduced(definition) ).
cnf(t38,plain,
multiply(c,commutator(a,b)) = sFlat2,
inference(orient,[status(thm)],[t8]) ).
cnf(t80294,plain,
multiply(c,sFlat0) = sFlat2,
inference(step,[status(thm)],[t38,t44]) ).
cnf(t48,plain,
multiply(c,sFlat0) = sFlat2,
inference(rw,[status(thm)],[t80294]) ).
cnf(t50,plain,
multiply(c,sFlat0) = sFlat2,
inference(orient,[status(thm)],[t48]) ).
cnf(f1,axiom,
( A = C
| multiply(A,B) != multiply(C,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_cancellation) ).
fof(f1_nnf,plain,
! [A,B,C] :
( A = C
| multiply(A,B) != multiply(C,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] :
( A = C
| multiply(A,B) != multiply(C,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( X0 = X2
| multiply(X0,X1) != multiply(X2,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
ifeq(multiply(X1,X2),multiply(X3,X2),X1,X3) = X3,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t11,plain,
ifeq(multiply(X1,X2),multiply(X3,X2),X1,X3) = X3,
inference(orient,[status(thm)],[t2]) ).
cnf(f0,axiom,
multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_multiply) ).
fof(f0_nnf,plain,
! [X,Y,Z] : multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] : multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t4,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t17,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t4]) ).
cnf(t59,plain,
multiply(sFlat0,multiply(c,X1)) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t17,t56]) ).
cnf(t88,plain,
multiply(sFlat0,multiply(c,X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t59]) ).
cnf(t53,plain,
multiply(c,multiply(sFlat0,X1)) = multiply(sFlat2,X1),
inference(cp,[status(thm)],[t17,t50]) ).
cnf(t68,plain,
multiply(c,multiply(sFlat0,X1)) = multiply(sFlat2,X1),
inference(orient,[status(thm)],[t53]) ).
cnf(t92,plain,
multiply(sFlat1,multiply(sFlat0,X1)) = multiply(sFlat0,multiply(sFlat2,X1)),
inference(cp,[status(thm)],[t88,t68]) ).
cnf(t136,plain,
multiply(sFlat1,multiply(sFlat0,X1)) = multiply(sFlat0,multiply(sFlat2,X1)),
inference(orient,[status(thm)],[t92]) ).
cnf(t143,plain,
X1 = ifeq(multiply(sFlat0,multiply(sFlat2,X2)),multiply(X1,multiply(sFlat0,X2)),sFlat1,X1),
inference(cp,[status(thm)],[t11,t136]) ).
cnf(t79932,plain,
ifeq(multiply(sFlat0,multiply(sFlat2,X1)),multiply(X2,multiply(sFlat0,X1)),sFlat1,X2) = X2,
inference(orient,[status(thm)],[t143]) ).
cnf(f3,axiom,
multiply(A,B) = multiply(B,multiply(A,commutator(A,B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutator) ).
fof(f3_nnf,plain,
! [A,B] : multiply(A,B) = multiply(B,multiply(A,commutator(A,B))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : multiply(A,B) = multiply(B,multiply(A,commutator(A,B))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
multiply(X0,X1) = multiply(X1,multiply(X0,commutator(X0,X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t3,plain,
multiply(X1,multiply(X2,commutator(X2,X1))) = multiply(X2,X1),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t12,plain,
multiply(X1,multiply(X2,commutator(X2,X1))) = multiply(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(f4,axiom,
commutator(multiply(A,B),C) = multiply(commutator(A,C),commutator(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutator_distributes_over_product) ).
fof(f4_nnf,plain,
! [A,B,C] : commutator(multiply(A,B),C) = multiply(commutator(A,C),commutator(B,C)),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : commutator(multiply(A,B),C) = multiply(commutator(A,C),commutator(B,C)),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
commutator(multiply(X0,X1),X2) = multiply(commutator(X0,X2),commutator(X1,X2)),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t5,plain,
multiply(commutator(X1,X2),commutator(X3,X2)) = commutator(multiply(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t25,plain,
multiply(commutator(X1,X2),commutator(X3,X2)) = commutator(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t45,plain,
commutator(multiply(a,X1),b) = multiply(sFlat0,commutator(X1,b)),
inference(cp,[status(thm)],[t25,t44]) ).
cnf(t118,plain,
commutator(multiply(a,X1),b) = multiply(sFlat0,commutator(X1,b)),
inference(orient,[status(thm)],[t45]) ).
cnf(t121,plain,
multiply(multiply(a,X1),b) = multiply(b,multiply(multiply(a,X1),multiply(sFlat0,commutator(X1,b)))),
inference(cp,[status(thm)],[t12,t118]) ).
cnf(t82448,plain,
multiply(a,multiply(X1,b)) = multiply(b,multiply(multiply(a,X1),multiply(sFlat0,commutator(X1,b)))),
inference(step,[status(thm)],[t121,t17]) ).
cnf(t82449,plain,
multiply(a,multiply(X1,b)) = multiply(b,multiply(a,multiply(X1,multiply(sFlat0,commutator(X1,b))))),
inference(step,[status(thm)],[t82448,t17]) ).
cnf(t48503,plain,
multiply(b,multiply(a,multiply(X1,multiply(sFlat0,commutator(X1,b))))) = multiply(a,multiply(X1,b)),
inference(orient,[status(thm)],[t82449]) ).
cnf(t48505,plain,
multiply(a,multiply(sFlat1,b)) = multiply(b,multiply(a,multiply(sFlat0,multiply(sFlat2,commutator(sFlat1,b))))),
inference(cp,[status(thm)],[t48503,t136]) ).
cnf(t47,plain,
multiply(a,b) = multiply(b,multiply(a,sFlat0)),
inference(cp,[status(thm)],[t12,t44]) ).
cnf(t62,plain,
multiply(b,multiply(a,sFlat0)) = multiply(a,b),
inference(orient,[status(thm)],[t47]) ).
cnf(t65,plain,
multiply(b,multiply(multiply(a,sFlat0),X1)) = multiply(multiply(a,b),X1),
inference(cp,[status(thm)],[t17,t62]) ).
cnf(t80300,plain,
multiply(b,multiply(a,multiply(sFlat0,X1))) = multiply(multiply(a,b),X1),
inference(step,[status(thm)],[t65,t17]) ).
cnf(t80301,plain,
multiply(b,multiply(a,multiply(sFlat0,X1))) = multiply(a,multiply(b,X1)),
inference(step,[status(thm)],[t80300,t17]) ).
cnf(t222,plain,
multiply(b,multiply(a,multiply(sFlat0,X1))) = multiply(a,multiply(b,X1)),
inference(orient,[status(thm)],[t80301]) ).
cnf(t82450,plain,
multiply(a,multiply(sFlat1,b)) = multiply(a,multiply(b,multiply(sFlat2,commutator(sFlat1,b)))),
inference(step,[status(thm)],[t48505,t222]) ).
cnf(f2,axiom,
( B = C
| multiply(A,B) != multiply(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_cancellation) ).
fof(f2_nnf,plain,
! [A,B,C] :
( B = C
| multiply(A,B) != multiply(A,C) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B,C] :
( B = C
| multiply(A,B) != multiply(A,C) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( X1 = X2
| multiply(X0,X1) != multiply(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t1,plain,
ifeq(multiply(X1,X2),multiply(X1,X3),X2,X3) = X3,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t10,plain,
ifeq(multiply(X1,X2),multiply(X1,X3),X2,X3) = X3,
inference(orient,[status(thm)],[t1]) ).
cnf(t13,plain,
X1 = ifeq(multiply(X2,X3),multiply(X3,X1),multiply(X2,commutator(X2,X3)),X1),
inference(cp,[status(thm)],[t10,t12]) ).
cnf(t312,plain,
ifeq(multiply(X1,X2),multiply(X2,X3),multiply(X1,commutator(X1,X2)),X3) = X3,
inference(orient,[status(thm)],[t13]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t313,plain,
X1 = multiply(X1,commutator(X1,X1)),
inference(cp,[status(thm)],[t312,t9]) ).
cnf(t379,plain,
multiply(X1,commutator(X1,X1)) = X1,
inference(orient,[status(thm)],[t313]) ).
cnf(t381,plain,
X1 = ifeq(X2,multiply(X2,X1),commutator(X2,X2),X1),
inference(cp,[status(thm)],[t10,t379]) ).
cnf(t4161,plain,
ifeq(X1,multiply(X1,X2),commutator(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t381]) ).
cnf(t392,plain,
multiply(X1,multiply(commutator(X1,X1),X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t17,t379]) ).
cnf(t463,plain,
multiply(X1,multiply(commutator(X1,X1),X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t392]) ).
cnf(t468,plain,
multiply(X1,commutator(X2,X1)) = multiply(X1,commutator(multiply(X1,X2),X1)),
inference(cp,[status(thm)],[t463,t25]) ).
cnf(t627,plain,
multiply(X1,commutator(multiply(X1,X2),X1)) = multiply(X1,commutator(X2,X1)),
inference(orient,[status(thm)],[t468]) ).
cnf(t631,plain,
multiply(X1,commutator(commutator(X1,X1),X1)) = multiply(X1,commutator(X1,X1)),
inference(cp,[status(thm)],[t627,t379]) ).
cnf(t464,plain,
multiply(X1,commutator(commutator(X1,X1),X1)) = multiply(commutator(X1,X1),X1),
inference(cp,[status(thm)],[t463,t12]) ).
cnf(t599,plain,
multiply(X1,commutator(commutator(X1,X1),X1)) = multiply(commutator(X1,X1),X1),
inference(orient,[status(thm)],[t464]) ).
cnf(t80316,plain,
multiply(commutator(X1,X1),X1) = multiply(X1,commutator(X1,X1)),
inference(step,[status(thm)],[t631,t599]) ).
cnf(t80317,plain,
multiply(commutator(X1,X1),X1) = X1,
inference(step,[status(thm)],[t80316,t379]) ).
cnf(t705,plain,
multiply(commutator(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t80317]) ).
cnf(t716,plain,
X1 = ifeq(X2,multiply(X1,X2),commutator(X2,X2),X1),
inference(cp,[status(thm)],[t11,t705]) ).
cnf(t8205,plain,
ifeq(X1,multiply(X2,X1),commutator(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t716]) ).
cnf(t715,plain,
multiply(commutator(X1,X1),multiply(X1,X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t17,t705]) ).
cnf(t809,plain,
multiply(commutator(X1,X1),multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t715]) ).
cnf(t8295,plain,
commutator(X1,X1) = ifeq(multiply(X1,X2),multiply(X1,X2),commutator(multiply(X1,X2),multiply(X1,X2)),commutator(X1,X1)),
inference(cp,[status(thm)],[t8205,t809]) ).
cnf(t80959,plain,
commutator(X1,X1) = commutator(multiply(X1,X2),multiply(X1,X2)),
inference(step,[status(thm)],[t8295,t9]) ).
cnf(t9211,plain,
commutator(multiply(X1,X2),multiply(X1,X2)) = commutator(X1,X1),
inference(orient,[status(thm)],[t80959]) ).
cnf(t9212,plain,
commutator(X1,X1) = commutator(multiply(X2,X1),multiply(X1,multiply(X2,commutator(X2,X1)))),
inference(cp,[status(thm)],[t9211,t12]) ).
cnf(t80975,plain,
commutator(X1,X1) = commutator(multiply(X2,X1),multiply(X2,X1)),
inference(step,[status(thm)],[t9212,t12]) ).
cnf(t80976,plain,
commutator(X1,X1) = commutator(X2,X2),
inference(step,[status(thm)],[t80975,t9211]) ).
cnf(t9481,plain,
commutator(X1,X1) = commutator(X2,X2),
inference(orient,[status(thm)],[t80976]) ).
cnf(t9519,plain,
X1 = multiply(commutator(X2,X2),X1),
inference(cp,[status(thm)],[t705,t9481]) ).
cnf(t9851,plain,
multiply(commutator(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t9519]) ).
cnf(t9852,plain,
commutator(X1,X2) = commutator(multiply(X2,X1),X2),
inference(cp,[status(thm)],[t9851,t25]) ).
cnf(t10017,plain,
commutator(multiply(X1,X2),X1) = commutator(X2,X1),
inference(orient,[status(thm)],[t9852]) ).
cnf(t10061,plain,
commutator(multiply(a,sFlat0),b) = commutator(multiply(a,b),b),
inference(cp,[status(thm)],[t10017,t62]) ).
cnf(t81002,plain,
multiply(sFlat0,commutator(sFlat0,b)) = commutator(multiply(a,b),b),
inference(step,[status(thm)],[t10061,t118]) ).
cnf(t81003,plain,
multiply(sFlat0,commutator(sFlat0,b)) = multiply(sFlat0,commutator(b,b)),
inference(step,[status(thm)],[t81002,t118]) ).
cnf(t9523,plain,
X1 = multiply(X1,commutator(X2,X2)),
inference(cp,[status(thm)],[t379,t9481]) ).
cnf(t9940,plain,
multiply(X1,commutator(X2,X2)) = X1,
inference(orient,[status(thm)],[t9523]) ).
cnf(t81004,plain,
multiply(sFlat0,commutator(sFlat0,b)) = sFlat0,
inference(step,[status(thm)],[t81003,t9940]) ).
cnf(t10074,plain,
multiply(sFlat0,commutator(sFlat0,b)) = sFlat0,
inference(orient,[status(thm)],[t81004]) ).
cnf(t10079,plain,
commutator(sFlat0,b) = ifeq(sFlat0,sFlat0,commutator(sFlat0,sFlat0),commutator(sFlat0,b)),
inference(cp,[status(thm)],[t4161,t10074]) ).
cnf(t81005,plain,
commutator(sFlat0,b) = commutator(sFlat0,sFlat0),
inference(step,[status(thm)],[t10079,t9]) ).
cnf(t10110,plain,
commutator(sFlat0,b) = commutator(sFlat0,sFlat0),
inference(orient,[status(thm)],[t81005]) ).
cnf(t10112,plain,
commutator(multiply(X1,sFlat0),b) = multiply(commutator(X1,b),commutator(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t25,t10110]) ).
cnf(t81055,plain,
commutator(multiply(X1,sFlat0),b) = commutator(X1,b),
inference(step,[status(thm)],[t10112,t9940]) ).
cnf(t10635,plain,
commutator(multiply(X1,sFlat0),b) = commutator(X1,b),
inference(orient,[status(thm)],[t81055]) ).
cnf(t91,plain,
multiply(sFlat1,sFlat0) = multiply(sFlat0,sFlat2),
inference(cp,[status(thm)],[t88,t50]) ).
cnf(t99,plain,
multiply(sFlat1,sFlat0) = multiply(sFlat0,sFlat2),
inference(orient,[status(thm)],[t91]) ).
cnf(t10638,plain,
commutator(sFlat1,b) = commutator(multiply(sFlat0,sFlat2),b),
inference(cp,[status(thm)],[t10635,t99]) ).
cnf(t10111,plain,
commutator(multiply(sFlat0,X1),b) = multiply(commutator(sFlat0,sFlat0),commutator(X1,b)),
inference(cp,[status(thm)],[t25,t10110]) ).
cnf(t81054,plain,
commutator(multiply(sFlat0,X1),b) = commutator(X1,b),
inference(step,[status(thm)],[t10111,t9851]) ).
cnf(t10598,plain,
commutator(multiply(sFlat0,X1),b) = commutator(X1,b),
inference(orient,[status(thm)],[t81054]) ).
cnf(t81056,plain,
commutator(sFlat1,b) = commutator(sFlat2,b),
inference(step,[status(thm)],[t10638,t10598]) ).
cnf(t10653,plain,
commutator(sFlat2,b) = commutator(sFlat1,b),
inference(orient,[status(thm)],[t81056]) ).
cnf(t10656,plain,
multiply(sFlat2,b) = multiply(b,multiply(sFlat2,commutator(sFlat1,b))),
inference(cp,[status(thm)],[t12,t10653]) ).
cnf(t12139,plain,
multiply(b,multiply(sFlat2,commutator(sFlat1,b))) = multiply(sFlat2,b),
inference(orient,[status(thm)],[t10656]) ).
cnf(t82451,plain,
multiply(a,multiply(sFlat1,b)) = multiply(a,multiply(sFlat2,b)),
inference(step,[status(thm)],[t82450,t12139]) ).
cnf(t48707,plain,
multiply(a,multiply(sFlat2,b)) = multiply(a,multiply(sFlat1,b)),
inference(orient,[status(thm)],[t82451]) ).
cnf(t48716,plain,
multiply(a,multiply(multiply(sFlat2,b),X1)) = multiply(multiply(a,multiply(sFlat1,b)),X1),
inference(cp,[status(thm)],[t17,t48707]) ).
cnf(t82452,plain,
multiply(a,multiply(sFlat2,multiply(b,X1))) = multiply(multiply(a,multiply(sFlat1,b)),X1),
inference(step,[status(thm)],[t48716,t17]) ).
cnf(t82453,plain,
multiply(a,multiply(sFlat2,multiply(b,X1))) = multiply(a,multiply(multiply(sFlat1,b),X1)),
inference(step,[status(thm)],[t82452,t17]) ).
cnf(t82454,plain,
multiply(a,multiply(sFlat2,multiply(b,X1))) = multiply(a,multiply(sFlat1,multiply(b,X1))),
inference(step,[status(thm)],[t82453,t17]) ).
cnf(t48744,plain,
multiply(a,multiply(sFlat2,multiply(b,X1))) = multiply(a,multiply(sFlat1,multiply(b,X1))),
inference(orient,[status(thm)],[t82454]) ).
cnf(t24,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,multiply(X1,multiply(X2,commutator(multiply(X1,X2),X3)))),
inference(cp,[status(thm)],[t12,t17]) ).
cnf(t80949,plain,
multiply(X1,multiply(X2,X3)) = multiply(X3,multiply(X1,multiply(X2,commutator(multiply(X1,X2),X3)))),
inference(step,[status(thm)],[t24,t17]) ).
cnf(t8745,plain,
multiply(X1,multiply(X2,multiply(X3,commutator(multiply(X2,X3),X1)))) = multiply(X2,multiply(X3,X1)),
inference(orient,[status(thm)],[t80949]) ).
cnf(t48746,plain,
multiply(a,multiply(sFlat1,multiply(b,commutator(multiply(sFlat2,b),a)))) = multiply(sFlat2,multiply(b,a)),
inference(cp,[status(thm)],[t48744,t8745]) ).
cnf(t10071,plain,
commutator(multiply(X1,multiply(X2,X3)),X2) = multiply(commutator(X1,X2),commutator(X3,X2)),
inference(cp,[status(thm)],[t25,t10017]) ).
cnf(t81138,plain,
commutator(multiply(X1,multiply(X2,X3)),X2) = commutator(multiply(X1,X3),X2),
inference(step,[status(thm)],[t10071,t25]) ).
cnf(t12582,plain,
commutator(multiply(X1,multiply(X2,X3)),X2) = commutator(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t81138]) ).
cnf(t12598,plain,
commutator(multiply(b,sFlat0),a) = commutator(multiply(a,b),a),
inference(cp,[status(thm)],[t12582,t62]) ).
cnf(t663,plain,
multiply(b,commutator(multiply(a,sFlat0),b)) = multiply(b,commutator(multiply(a,b),b)),
inference(cp,[status(thm)],[t627,t62]) ).
cnf(t80325,plain,
multiply(b,multiply(sFlat0,commutator(sFlat0,b))) = multiply(b,commutator(multiply(a,b),b)),
inference(step,[status(thm)],[t663,t118]) ).
cnf(t80326,plain,
multiply(sFlat0,b) = multiply(b,commutator(multiply(a,b),b)),
inference(step,[status(thm)],[t80325,t12]) ).
cnf(t80327,plain,
multiply(sFlat0,b) = multiply(b,multiply(sFlat0,commutator(b,b))),
inference(step,[status(thm)],[t80326,t118]) ).
cnf(t798,plain,
multiply(b,multiply(sFlat0,commutator(b,b))) = multiply(sFlat0,b),
inference(orient,[status(thm)],[t80327]) ).
cnf(t9226,plain,
commutator(b,b) = commutator(multiply(sFlat0,b),multiply(b,multiply(sFlat0,commutator(b,b)))),
inference(cp,[status(thm)],[t9211,t798]) ).
cnf(t80967,plain,
commutator(b,b) = commutator(multiply(sFlat0,b),multiply(sFlat0,b)),
inference(step,[status(thm)],[t9226,t798]) ).
cnf(t80968,plain,
commutator(b,b) = commutator(sFlat0,sFlat0),
inference(step,[status(thm)],[t80967,t9211]) ).
cnf(t9303,plain,
commutator(b,b) = commutator(sFlat0,sFlat0),
inference(orient,[status(thm)],[t80968]) ).
cnf(t80971,plain,
multiply(b,multiply(sFlat0,commutator(sFlat0,sFlat0))) = multiply(sFlat0,b),
inference(step,[status(thm)],[t798,t9303]) ).
cnf(t80972,plain,
multiply(b,sFlat0) = multiply(sFlat0,b),
inference(step,[status(thm)],[t80971,t379]) ).
cnf(t9329,plain,
multiply(b,sFlat0) = multiply(sFlat0,b),
inference(rw,[status(thm)],[t80972]) ).
cnf(t9330,plain,
multiply(b,sFlat0) = multiply(sFlat0,b),
inference(orient,[status(thm)],[t9329]) ).
cnf(t81140,plain,
commutator(multiply(sFlat0,b),a) = commutator(multiply(a,b),a),
inference(step,[status(thm)],[t12598,t9330]) ).
cnf(t81141,plain,
commutator(multiply(sFlat0,b),a) = commutator(b,a),
inference(step,[status(thm)],[t81140,t10017]) ).
cnf(t12676,plain,
commutator(multiply(sFlat0,b),a) = commutator(b,a),
inference(orient,[status(thm)],[t81141]) ).
cnf(t12678,plain,
commutator(multiply(X1,multiply(sFlat0,b)),a) = multiply(commutator(X1,a),commutator(b,a)),
inference(cp,[status(thm)],[t25,t12676]) ).
cnf(t81296,plain,
commutator(multiply(X1,multiply(sFlat0,b)),a) = commutator(multiply(X1,b),a),
inference(step,[status(thm)],[t12678,t25]) ).
cnf(t17245,plain,
commutator(multiply(X1,multiply(sFlat0,b)),a) = commutator(multiply(X1,b),a),
inference(orient,[status(thm)],[t81296]) ).
cnf(t17247,plain,
commutator(multiply(c,b),a) = commutator(multiply(sFlat2,b),a),
inference(cp,[status(thm)],[t17245,t68]) ).
cnf(t12599,plain,
commutator(multiply(b,multiply(sFlat0,X1)),a) = commutator(multiply(a,multiply(b,X1)),a),
inference(cp,[status(thm)],[t12582,t222]) ).
cnf(t9337,plain,
multiply(b,multiply(sFlat0,X1)) = multiply(multiply(sFlat0,b),X1),
inference(cp,[status(thm)],[t17,t9330]) ).
cnf(t81060,plain,
multiply(b,multiply(sFlat0,X1)) = multiply(sFlat0,multiply(b,X1)),
inference(step,[status(thm)],[t9337,t17]) ).
cnf(t10680,plain,
multiply(b,multiply(sFlat0,X1)) = multiply(sFlat0,multiply(b,X1)),
inference(orient,[status(thm)],[t81060]) ).
cnf(t81288,plain,
commutator(multiply(sFlat0,multiply(b,X1)),a) = commutator(multiply(a,multiply(b,X1)),a),
inference(step,[status(thm)],[t12599,t10680]) ).
cnf(t81289,plain,
commutator(multiply(sFlat0,multiply(b,X1)),a) = commutator(multiply(b,X1),a),
inference(step,[status(thm)],[t81288,t10017]) ).
cnf(t17103,plain,
commutator(multiply(sFlat0,multiply(b,X1)),a) = commutator(multiply(b,X1),a),
inference(orient,[status(thm)],[t81289]) ).
cnf(t10605,plain,
commutator(c,b) = commutator(sFlat1,b),
inference(cp,[status(thm)],[t10598,t56]) ).
cnf(t10624,plain,
commutator(c,b) = commutator(sFlat1,b),
inference(orient,[status(thm)],[t10605]) ).
cnf(t10627,plain,
multiply(c,b) = multiply(b,multiply(c,commutator(sFlat1,b))),
inference(cp,[status(thm)],[t12,t10624]) ).
cnf(t12107,plain,
multiply(b,multiply(c,commutator(sFlat1,b))) = multiply(c,b),
inference(orient,[status(thm)],[t10627]) ).
cnf(t17112,plain,
commutator(multiply(b,multiply(c,commutator(sFlat1,b))),a) = commutator(multiply(sFlat0,multiply(c,b)),a),
inference(cp,[status(thm)],[t17103,t12107]) ).
cnf(t81290,plain,
commutator(multiply(c,b),a) = commutator(multiply(sFlat0,multiply(c,b)),a),
inference(step,[status(thm)],[t17112,t12107]) ).
cnf(t81291,plain,
commutator(multiply(c,b),a) = commutator(multiply(sFlat1,b),a),
inference(step,[status(thm)],[t81290,t88]) ).
cnf(t17142,plain,
commutator(multiply(c,b),a) = commutator(multiply(sFlat1,b),a),
inference(orient,[status(thm)],[t81291]) ).
cnf(t81297,plain,
commutator(multiply(sFlat1,b),a) = commutator(multiply(sFlat2,b),a),
inference(step,[status(thm)],[t17247,t17142]) ).
cnf(t17270,plain,
commutator(multiply(sFlat2,b),a) = commutator(multiply(sFlat1,b),a),
inference(orient,[status(thm)],[t81297]) ).
cnf(t82455,plain,
multiply(a,multiply(sFlat1,multiply(b,commutator(multiply(sFlat1,b),a)))) = multiply(sFlat2,multiply(b,a)),
inference(step,[status(thm)],[t48746,t17270]) ).
cnf(t82456,plain,
multiply(sFlat1,multiply(b,a)) = multiply(sFlat2,multiply(b,a)),
inference(step,[status(thm)],[t82455,t8745]) ).
cnf(t48808,plain,
multiply(sFlat2,multiply(b,a)) = multiply(sFlat1,multiply(b,a)),
inference(orient,[status(thm)],[t82456]) ).
cnf(t48834,plain,
multiply(sFlat2,multiply(multiply(b,a),X1)) = multiply(multiply(sFlat1,multiply(b,a)),X1),
inference(cp,[status(thm)],[t17,t48808]) ).
cnf(t82467,plain,
multiply(sFlat2,multiply(b,multiply(a,X1))) = multiply(multiply(sFlat1,multiply(b,a)),X1),
inference(step,[status(thm)],[t48834,t17]) ).
cnf(t82468,plain,
multiply(sFlat2,multiply(b,multiply(a,X1))) = multiply(sFlat1,multiply(multiply(b,a),X1)),
inference(step,[status(thm)],[t82467,t17]) ).
cnf(t82469,plain,
multiply(sFlat2,multiply(b,multiply(a,X1))) = multiply(sFlat1,multiply(b,multiply(a,X1))),
inference(step,[status(thm)],[t82468,t17]) ).
cnf(t49206,plain,
multiply(sFlat2,multiply(b,multiply(a,X1))) = multiply(sFlat1,multiply(b,multiply(a,X1))),
inference(orient,[status(thm)],[t82469]) ).
cnf(t18,plain,
multiply(X1,multiply(X2,multiply(X3,commutator(X3,multiply(X1,X2))))) = multiply(X3,multiply(X1,X2)),
inference(cp,[status(thm)],[t17,t12]) ).
cnf(t3744,plain,
multiply(X1,multiply(X2,multiply(X3,commutator(X3,multiply(X1,X2))))) = multiply(X3,multiply(X1,X2)),
inference(orient,[status(thm)],[t18]) ).
cnf(t49213,plain,
multiply(sFlat1,multiply(b,multiply(a,multiply(X1,commutator(X1,multiply(b,a)))))) = multiply(sFlat2,multiply(X1,multiply(b,a))),
inference(cp,[status(thm)],[t49206,t3744]) ).
cnf(t82483,plain,
multiply(sFlat1,multiply(X1,multiply(b,a))) = multiply(sFlat2,multiply(X1,multiply(b,a))),
inference(step,[status(thm)],[t49213,t3744]) ).
cnf(t49784,plain,
multiply(sFlat2,multiply(X1,multiply(b,a))) = multiply(sFlat1,multiply(X1,multiply(b,a))),
inference(orient,[status(thm)],[t82483]) ).
cnf(t80020,plain,
sFlat2 = ifeq(multiply(sFlat0,multiply(sFlat2,multiply(b,a))),multiply(sFlat1,multiply(sFlat0,multiply(b,a))),sFlat1,sFlat2),
inference(cp,[status(thm)],[t79932,t49784]) ).
cnf(t83224,plain,
sFlat2 = ifeq(multiply(sFlat0,multiply(sFlat1,multiply(b,a))),multiply(sFlat1,multiply(sFlat0,multiply(b,a))),sFlat1,sFlat2),
inference(step,[status(thm)],[t80020,t48808]) ).
cnf(t83225,plain,
sFlat2 = ifeq(multiply(sFlat0,multiply(sFlat1,multiply(b,a))),multiply(sFlat0,multiply(sFlat2,multiply(b,a))),sFlat1,sFlat2),
inference(step,[status(thm)],[t83224,t136]) ).
cnf(t83226,plain,
sFlat2 = ifeq(multiply(sFlat0,multiply(sFlat1,multiply(b,a))),multiply(sFlat0,multiply(sFlat1,multiply(b,a))),sFlat1,sFlat2),
inference(step,[status(thm)],[t83225,t48808]) ).
cnf(t83227,plain,
sFlat2 = sFlat1,
inference(step,[status(thm)],[t83226,t9]) ).
cnf(t80051,plain,
sFlat2 = sFlat1,
inference(orient,[status(thm)],[t83227]) ).
cnf(t83228,plain,
multiply(c,sFlat0) = sFlat1,
inference(step,[status(thm)],[t50,t80051]) ).
cnf(t80052,plain,
multiply(c,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t83228]) ).
cnf(f5,negated_conjecture,
multiply(commutator(a,b),c) != multiply(c,commutator(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_nilpotency) ).
fof(f5_nnf,plain,
multiply(commutator(a,b),c) != multiply(c,commutator(a,b)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
multiply(commutator(a,b),c) != multiply(c,commutator(a,b)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
multiply(commutator(a,b),c) != multiply(c,commutator(a,b)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(goal_0,negated_conjecture,
multiply(commutator(a,b),c) != multiply(c,commutator(a,b)),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(g0_0,plain,
multiply(sFlat0,c) != multiply(c,commutator(a,b)),
inference(rw,[status(thm)],[goal_0,t44]) ).
cnf(g0_1,plain,
sFlat1 != multiply(c,commutator(a,b)),
inference(rw,[status(thm)],[g0_0,t56]) ).
cnf(g0_2,plain,
sFlat1 != multiply(c,sFlat0),
inference(rw,[status(thm)],[g0_1,t44]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t80052]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP401-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/10.59 % Computer : n013.cluster.edu
% 0.11/10.59 % Model : x86_64 x86_64
% 0.11/10.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.59 % Memory : 8046.5625MB
% 0.11/10.59 % OS : Linux 6.8.0-71-generic
% 0.11/10.59 % CPULimit : 300
% 0.11/10.59 % WCLimit : 300
% 0.11/10.59 % DateTime : Wed Sep 23 14:40:07 UTC 2026
% 0.11/10.59 % CPUTime :
% 0.11/10.59 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 52.65/17.53 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 52.65/17.53 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------