%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP400-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Sun Sep 27 07:28:47 AM UTC 2026
% Result : Unsatisfiable 218.39s 28.20s
% Output : CNFRefutation 218.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 6
% Syntax : Number of formulae : 190 ( 167 unt; 0 def)
% Number of atoms : 213 ( 212 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 67 ( 44 ~; 23 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 491 ( 12 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(associativity_of_multiply,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_multiply) ).
cnf(c_1,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity_of_multiply]) ).
fof(right_cancellation,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 = VAR_2
| multiply(VAR_0,VAR_1) != multiply(VAR_2,VAR_1) ),
file('theBenchmark.p',right_cancellation) ).
cnf(c_2,plain,
( A = C
| multiply(A,B) != multiply(C,B) ),
inference(clausify,[status(thm)],[right_cancellation]) ).
fof(left_cancellation,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = VAR_2
| multiply(VAR_0,VAR_1) != multiply(VAR_0,VAR_2) ),
file('theBenchmark.p',left_cancellation) ).
cnf(c_3,plain,
( B = C
| multiply(A,B) != multiply(A,C) ),
inference(clausify,[status(thm)],[left_cancellation]) ).
fof(commutator,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,VAR_1) = multiply(VAR_1,multiply(VAR_0,commutator(VAR_0,VAR_1))),
file('theBenchmark.p',commutator) ).
cnf(c_4,plain,
multiply(A,B) = multiply(B,multiply(A,commutator(A,B))),
inference(clausify,[status(thm)],[commutator]) ).
cnf(c_5,plain,
multiply(A,multiply(B,commutator(B,A))) = multiply(B,A),
inference(copy,[status(thm)],[c_4]) ).
fof(associativity_of_commutator,axiom,
! [VAR_0,VAR_1,VAR_2] : commutator(commutator(VAR_0,VAR_1),VAR_2) = commutator(VAR_0,commutator(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_commutator) ).
cnf(c_6,plain,
commutator(commutator(A,B),C) = commutator(A,commutator(B,C)),
inference(clausify,[status(thm)],[associativity_of_commutator]) ).
fof(prove_commutator_distributes_over_product,axiom,
commutator(multiply(a,b),c) != multiply(commutator(a,c),commutator(b,c)),
file('theBenchmark.p',prove_commutator_distributes_over_product) ).
cnf(c_7,plain,
commutator(multiply(a,b),c) != multiply(commutator(a,c),commutator(b,c)),
inference(clausify,[status(thm)],[prove_commutator_distributes_over_product]) ).
cnf(c_8,plain,
( multiply(A,B) = D
| multiply(A,multiply(B,C)) != multiply(D,C) ),
inference(paramod,[status(thm)],[c_1,c_2]) ).
cnf(c_22287,plain,
( C = D
| multiply(A,multiply(B,C)) != multiply(multiply(A,B),D) ),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_9,plain,
( C = D
| multiply(A,multiply(B,C)) != multiply(A,multiply(B,D)) ),
inference(paramod,[status(thm)],[c_1,c_22287]) ).
cnf(c_10,plain,
multiply(A,commutator(A,A)) = A,
inference(resolve,[status(thm)],[c_3,c_5]) ).
cnf(c_22288,plain,
multiply(multiply(A,B),C) = multiply(B,multiply(multiply(A,commutator(A,B)),C)),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_22289,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(multiply(A,commutator(A,B)),C)),
inference(paramod,[status(thm)],[c_1,c_22288]) ).
cnf(c_22290,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(A,multiply(commutator(A,B),C))),
inference(paramod,[status(thm)],[c_1,c_22289]) ).
cnf(c_11,plain,
multiply(A,multiply(B,multiply(commutator(B,A),C))) = multiply(B,multiply(A,C)),
inference(copy,[status(thm)],[c_22290]) ).
cnf(c_22291,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(C,multiply(A,commutator(A,multiply(B,C))))),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_12,plain,
multiply(A,multiply(B,multiply(C,commutator(C,multiply(A,B))))) = multiply(C,multiply(A,B)),
inference(copy,[status(thm)],[c_22291]) ).
cnf(c_22292,plain,
multiply(A,multiply(B,multiply(C,commutator(multiply(B,C),A)))) = multiply(multiply(B,C),A),
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_13,plain,
multiply(A,multiply(B,multiply(C,commutator(multiply(B,C),A)))) = multiply(B,multiply(C,A)),
inference(paramod,[status(thm)],[c_1,c_22292]) ).
cnf(c_22293,plain,
( multiply(A,commutator(A,B)) = C
| multiply(A,B) != multiply(B,C) ),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_16,plain,
( multiply(C,commutator(C,A)) = B
| multiply(A,B) != multiply(C,A) ),
inference(copy,[status(thm)],[c_22293]) ).
cnf(c_17,plain,
multiply(A,multiply(commutator(B,C),commutator(B,commutator(C,A)))) = multiply(commutator(B,C),A),
inference(paramod,[status(thm)],[c_6,c_5]) ).
cnf(c_22294,plain,
multiply(commutator(multiply(a,b),c),A) != multiply(multiply(commutator(a,c),commutator(b,c)),A),
inference(resolve,[status(thm)],[c_2,c_7]) ).
cnf(c_19,plain,
multiply(commutator(multiply(a,b),c),A) != multiply(commutator(a,c),multiply(commutator(b,c),A)),
inference(paramod,[status(thm)],[c_1,c_22294]) ).
cnf(c_22295,plain,
multiply(A,commutator(multiply(a,b),c)) != multiply(commutator(a,c),multiply(commutator(b,c),multiply(A,commutator(A,commutator(multiply(a,b),c))))),
inference(paramod,[status(thm)],[c_5,c_19]) ).
cnf(c_27,plain,
multiply(commutator(a,c),multiply(commutator(b,c),multiply(A,commutator(A,commutator(multiply(a,b),c))))) != multiply(A,commutator(multiply(a,b),c)),
inference(copy,[status(thm)],[c_22295]) ).
cnf(c_22296,plain,
multiply(A,B) = multiply(A,multiply(commutator(A,A),B)),
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_37,plain,
multiply(A,multiply(commutator(A,A),B)) = multiply(A,B),
inference(copy,[status(thm)],[c_22296]) ).
cnf(c_22297,plain,
( commutator(A,A) = B
| A != multiply(A,B) ),
inference(paramod,[status(thm)],[c_10,c_3]) ).
cnf(c_41,plain,
( commutator(A,A) = B
| multiply(A,B) != A ),
inference(copy,[status(thm)],[c_22297]) ).
cnf(c_22298,plain,
( multiply(B,commutator(B,C)) = D
| multiply(A,multiply(B,C)) != multiply(A,multiply(C,D)) ),
inference(paramod,[status(thm)],[c_5,c_9]) ).
cnf(c_64,plain,
( multiply(D,commutator(D,B)) = C
| multiply(A,multiply(B,C)) != multiply(A,multiply(D,B)) ),
inference(copy,[status(thm)],[c_22298]) ).
cnf(c_86,plain,
multiply(commutator(A,A),B) = B,
inference(resolve,[status(thm)],[c_9,c_37]) ).
cnf(c_22299,plain,
( commutator(C,C) = B
| A != multiply(B,A) ),
inference(paramod,[status(thm)],[c_86,c_2]) ).
cnf(c_98,plain,
( commutator(C,C) = A
| multiply(A,B) != B ),
inference(copy,[status(thm)],[c_22299]) ).
cnf(c_22300,plain,
multiply(A,commutator(commutator(B,B),A)) = multiply(commutator(B,B),A),
inference(paramod,[status(thm)],[c_86,c_5]) ).
cnf(c_22301,plain,
multiply(A,commutator(B,commutator(B,A))) = multiply(commutator(B,B),A),
inference(paramod,[status(thm)],[c_6,c_22300]) ).
cnf(c_99,plain,
multiply(A,commutator(B,commutator(B,A))) = A,
inference(paramod,[status(thm)],[c_86,c_22301]) ).
cnf(c_101,plain,
multiply(commutator(A,commutator(B,commutator(A,B))),C) = C,
inference(paramod,[status(thm)],[c_6,c_86]) ).
cnf(c_22302,plain,
commutator(A,A) = commutator(B,commutator(B,A)),
inference(resolve,[status(thm)],[c_41,c_99]) ).
cnf(c_108,plain,
commutator(A,commutator(A,B)) = commutator(B,B),
inference(copy,[status(thm)],[c_22302]) ).
cnf(c_22303,plain,
commutator(A,A) = commutator(B,commutator(B,commutator(A,A))),
inference(paramod,[status(thm)],[c_99,c_86]) ).
cnf(c_121,plain,
commutator(A,commutator(A,commutator(B,B))) = commutator(B,B),
inference(copy,[status(thm)],[c_22303]) ).
cnf(c_128,plain,
multiply(commutator(A,commutator(A,B)),C) = C,
inference(paramod,[status(thm)],[c_108,c_86]) ).
cnf(c_22304,plain,
commutator(A,commutator(B,B)) = commutator(commutator(A,B),commutator(A,B)),
inference(paramod,[status(thm)],[c_108,c_108]) ).
cnf(c_22305,plain,
commutator(A,commutator(B,B)) = commutator(A,commutator(B,commutator(A,B))),
inference(paramod,[status(thm)],[c_6,c_22304]) ).
cnf(c_131,plain,
commutator(A,commutator(B,commutator(A,B))) = commutator(A,commutator(B,B)),
inference(copy,[status(thm)],[c_22305]) ).
cnf(c_135,plain,
multiply(commutator(A,commutator(B,B)),C) = C,
inference(paramod,[status(thm)],[c_131,c_101]) ).
cnf(c_147,plain,
( multiply(A,multiply(commutator(A,B),C)) = D
| multiply(A,multiply(B,C)) != multiply(B,D) ),
inference(paramod,[status(thm)],[c_11,c_3]) ).
cnf(c_22306,plain,
multiply(A,multiply(B,multiply(C,commutator(B,A)))) = multiply(B,multiply(A,multiply(C,commutator(C,commutator(B,A))))),
inference(paramod,[status(thm)],[c_5,c_11]) ).
cnf(c_148,plain,
multiply(A,multiply(B,multiply(C,commutator(C,commutator(A,B))))) = multiply(B,multiply(A,multiply(C,commutator(A,B)))),
inference(copy,[status(thm)],[c_22306]) ).
cnf(c_163,plain,
( multiply(commutator(A,B),C) = D
| multiply(A,multiply(B,C)) != multiply(B,multiply(A,D)) ),
inference(paramod,[status(thm)],[c_11,c_9]) ).
cnf(c_22307,plain,
multiply(commutator(A,B),multiply(A,multiply(commutator(B,B),C))) = multiply(A,multiply(commutator(A,B),C)),
inference(paramod,[status(thm)],[c_108,c_11]) ).
cnf(c_166,plain,
multiply(commutator(A,B),multiply(A,C)) = multiply(A,multiply(commutator(A,B),C)),
inference(paramod,[status(thm)],[c_86,c_22307]) ).
cnf(c_22308,plain,
commutator(commutator(A,commutator(B,B)),commutator(A,commutator(B,B))) = commutator(A,commutator(B,B)),
inference(resolve,[status(thm)],[c_41,c_135]) ).
cnf(c_22309,plain,
commutator(A,commutator(commutator(B,B),commutator(A,commutator(B,B)))) = commutator(A,commutator(B,B)),
inference(paramod,[status(thm)],[c_6,c_22308]) ).
cnf(c_196,plain,
commutator(A,commutator(B,commutator(B,commutator(A,commutator(B,B))))) = commutator(A,commutator(B,B)),
inference(paramod,[status(thm)],[c_6,c_22309]) ).
cnf(c_205,plain,
commutator(A,commutator(A,commutator(B,commutator(C,C)))) = commutator(B,commutator(C,C)),
inference(paramod,[status(thm)],[c_135,c_99]) ).
cnf(c_22310,plain,
commutator(A,commutator(A,commutator(B,B))) = commutator(A,commutator(B,B)),
inference(paramod,[status(thm)],[c_205,c_196]) ).
cnf(c_22311,plain,
commutator(B,B) = commutator(A,commutator(B,B)),
inference(paramod,[status(thm)],[c_121,c_22310]) ).
cnf(c_207,plain,
commutator(A,commutator(B,B)) = commutator(B,B),
inference(copy,[status(thm)],[c_22311]) ).
cnf(c_22312,plain,
commutator(commutator(A,A),B) = commutator(C,commutator(commutator(A,A),B)),
inference(paramod,[status(thm)],[c_207,c_6]) ).
cnf(c_22313,plain,
commutator(A,commutator(A,B)) = commutator(C,commutator(commutator(A,A),B)),
inference(paramod,[status(thm)],[c_6,c_22312]) ).
cnf(c_22314,plain,
commutator(A,commutator(A,B)) = commutator(C,commutator(A,commutator(A,B))),
inference(paramod,[status(thm)],[c_6,c_22313]) ).
cnf(c_219,plain,
commutator(A,commutator(B,commutator(B,C))) = commutator(B,commutator(B,C)),
inference(copy,[status(thm)],[c_22314]) ).
cnf(c_22315,plain,
commutator(A,A) = commutator(B,commutator(B,C)),
inference(resolve,[status(thm)],[c_98,c_128]) ).
cnf(c_221,plain,
commutator(A,commutator(A,B)) = commutator(C,C),
inference(copy,[status(thm)],[c_22315]) ).
cnf(c_222,plain,
commutator(A,A) = commutator(B,B),
inference(resolve,[status(thm)],[c_98,c_86]) ).
cnf(c_227,plain,
multiply(A,multiply(B,commutator(B,multiply(B,A)))) = multiply(B,A),
inference(resolve,[status(thm)],[c_3,c_12]) ).
cnf(c_22316,plain,
multiply(A,multiply(multiply(B,C),D)) = multiply(B,multiply(C,multiply(D,multiply(A,commutator(A,multiply(multiply(B,C),D)))))),
inference(paramod,[status(thm)],[c_12,c_1]) ).
cnf(c_22317,plain,
multiply(A,multiply(B,multiply(C,D))) = multiply(B,multiply(C,multiply(D,multiply(A,commutator(A,multiply(multiply(B,C),D)))))),
inference(paramod,[status(thm)],[c_1,c_22316]) ).
cnf(c_22318,plain,
multiply(A,multiply(B,multiply(C,D))) = multiply(B,multiply(C,multiply(D,multiply(A,commutator(A,multiply(B,multiply(C,D))))))),
inference(paramod,[status(thm)],[c_1,c_22317]) ).
cnf(c_228,plain,
multiply(A,multiply(B,multiply(C,multiply(D,commutator(D,multiply(A,multiply(B,C))))))) = multiply(D,multiply(A,multiply(B,C))),
inference(copy,[status(thm)],[c_22318]) ).
cnf(c_286,plain,
multiply(A,commutator(B,B)) = A,
inference(paramod,[status(thm)],[c_222,c_10]) ).
cnf(c_22319,plain,
( commutator(C,C) = B
| A != multiply(A,B) ),
inference(paramod,[status(thm)],[c_286,c_3]) ).
cnf(c_291,plain,
( commutator(C,C) = B
| multiply(A,B) != A ),
inference(copy,[status(thm)],[c_22319]) ).
cnf(c_22320,plain,
multiply(A,commutator(A,commutator(B,commutator(B,C)))) = A,
inference(paramod,[status(thm)],[c_221,c_99]) ).
cnf(c_299,plain,
multiply(A,commutator(B,commutator(B,C))) = A,
inference(paramod,[status(thm)],[c_219,c_22320]) ).
cnf(c_303,plain,
multiply(A,multiply(B,commutator(multiply(A,B),A))) = multiply(B,A),
inference(resolve,[status(thm)],[c_3,c_13]) ).
cnf(c_22321,plain,
multiply(A,commutator(multiply(a,b),c)) != multiply(commutator(a,c),multiply(commutator(b,c),multiply(A,commutator(A,commutator(multiply(a,b),c))))),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_22322,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(multiply(a,b),commutator(multiply(a,b),commutator(multiply(a,b),c)))))) != multiply(multiply(a,b),c),
inference(resolve,[status(thm)],[c_16,c_22321]) ).
cnf(c_22323,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(a,b)))) != multiply(multiply(a,b),c),
inference(paramod,[status(thm)],[c_299,c_22322]) ).
cnf(c_607,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(a,b)))) != multiply(a,multiply(b,c)),
inference(paramod,[status(thm)],[c_1,c_22323]) ).
cnf(c_22324,plain,
multiply(c,multiply(multiply(commutator(a,c),multiply(commutator(b,c),multiply(a,b))),A)) != multiply(multiply(a,multiply(b,c)),A),
inference(resolve,[status(thm)],[c_8,c_607]) ).
cnf(c_22325,plain,
multiply(c,multiply(commutator(a,c),multiply(multiply(commutator(b,c),multiply(a,b)),A))) != multiply(multiply(a,multiply(b,c)),A),
inference(paramod,[status(thm)],[c_1,c_22324]) ).
cnf(c_22326,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(multiply(a,b),A)))) != multiply(multiply(a,multiply(b,c)),A),
inference(paramod,[status(thm)],[c_1,c_22325]) ).
cnf(c_22327,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(a,multiply(b,A))))) != multiply(multiply(a,multiply(b,c)),A),
inference(paramod,[status(thm)],[c_1,c_22326]) ).
cnf(c_22328,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(a,multiply(b,A))))) != multiply(a,multiply(multiply(b,c),A)),
inference(paramod,[status(thm)],[c_1,c_22327]) ).
cnf(c_617,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(a,multiply(b,A))))) != multiply(a,multiply(b,multiply(c,A))),
inference(paramod,[status(thm)],[c_1,c_22328]) ).
cnf(c_22329,plain,
multiply(A,multiply(commutator(B,A),commutator(A,A))) = multiply(commutator(B,A),A),
inference(paramod,[status(thm)],[c_207,c_17]) ).
cnf(c_22330,plain,
multiply(A,commutator(B,A)) = multiply(commutator(B,A),A),
inference(paramod,[status(thm)],[c_286,c_22329]) ).
cnf(c_691,plain,
multiply(commutator(A,B),B) = multiply(B,commutator(A,B)),
inference(copy,[status(thm)],[c_22330]) ).
cnf(c_22331,plain,
multiply(c,multiply(commutator(a,c),multiply(commutator(b,c),multiply(b,a)))) != multiply(a,multiply(b,multiply(c,commutator(b,a)))),
inference(paramod,[status(thm)],[c_5,c_617]) ).
cnf(c_827,plain,
multiply(c,multiply(commutator(a,c),multiply(b,multiply(commutator(b,c),a)))) != multiply(a,multiply(b,multiply(c,commutator(b,a)))),
inference(paramod,[status(thm)],[c_166,c_22331]) ).
cnf(c_22332,plain,
multiply(multiply(A,commutator(B,A)),C) = multiply(commutator(B,A),multiply(A,C)),
inference(paramod,[status(thm)],[c_691,c_1]) ).
cnf(c_22333,plain,
multiply(A,multiply(commutator(B,A),C)) = multiply(commutator(B,A),multiply(A,C)),
inference(paramod,[status(thm)],[c_1,c_22332]) ).
cnf(c_1149,plain,
multiply(commutator(A,B),multiply(B,C)) = multiply(B,multiply(commutator(A,B),C)),
inference(copy,[status(thm)],[c_22333]) ).
cnf(c_22334,plain,
multiply(A,commutator(A,B)) = multiply(A,commutator(A,multiply(A,B))),
inference(resolve,[status(thm)],[c_16,c_227]) ).
cnf(c_2448,plain,
multiply(A,commutator(A,multiply(A,B))) = multiply(A,commutator(A,B)),
inference(copy,[status(thm)],[c_22334]) ).
cnf(c_22335,plain,
multiply(A,commutator(A,B)) = multiply(A,commutator(multiply(B,A),B)),
inference(resolve,[status(thm)],[c_16,c_303]) ).
cnf(c_2501,plain,
multiply(A,commutator(multiply(B,A),B)) = multiply(A,commutator(A,B)),
inference(copy,[status(thm)],[c_22335]) ).
cnf(c_22336,plain,
( multiply(C,commutator(C,commutator(D,D))) = B
| multiply(A,B) != multiply(A,multiply(C,commutator(D,D))) ),
inference(paramod,[status(thm)],[c_86,c_64]) ).
cnf(c_22337,plain,
( multiply(C,commutator(C,commutator(D,D))) = B
| multiply(A,B) != multiply(A,C) ),
inference(paramod,[status(thm)],[c_286,c_22336]) ).
cnf(c_22338,plain,
( multiply(C,commutator(D,D)) = B
| multiply(A,B) != multiply(A,C) ),
inference(paramod,[status(thm)],[c_207,c_22337]) ).
cnf(c_2566,plain,
( C = B
| multiply(A,B) != multiply(A,C) ),
inference(paramod,[status(thm)],[c_286,c_22338]) ).
cnf(c_22339,plain,
commutator(A,B) = commutator(A,multiply(A,B)),
inference(resolve,[status(thm)],[c_2566,c_2448]) ).
cnf(c_3304,plain,
commutator(A,multiply(A,B)) = commutator(A,B),
inference(copy,[status(thm)],[c_22339]) ).
cnf(c_3345,plain,
commutator(multiply(A,B),multiply(A,multiply(B,C))) = commutator(multiply(A,B),C),
inference(paramod,[status(thm)],[c_1,c_3304]) ).
cnf(c_22340,plain,
commutator(commutator(A,B),C) = commutator(A,commutator(multiply(A,B),C)),
inference(paramod,[status(thm)],[c_3304,c_6]) ).
cnf(c_22341,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(multiply(A,B),C)),
inference(paramod,[status(thm)],[c_6,c_22340]) ).
cnf(c_3347,plain,
commutator(A,commutator(multiply(A,B),C)) = commutator(A,commutator(B,C)),
inference(copy,[status(thm)],[c_22341]) ).
cnf(c_22342,plain,
commutator(A,multiply(B,multiply(A,C))) = commutator(A,multiply(B,multiply(commutator(B,A),C))),
inference(paramod,[status(thm)],[c_11,c_3304]) ).
cnf(c_3349,plain,
commutator(A,multiply(B,multiply(commutator(B,A),C))) = commutator(A,multiply(B,multiply(A,C))),
inference(copy,[status(thm)],[c_22342]) ).
cnf(c_22343,plain,
commutator(A,B) = commutator(multiply(B,A),B),
inference(resolve,[status(thm)],[c_2566,c_2501]) ).
cnf(c_3693,plain,
commutator(multiply(A,B),A) = commutator(B,A),
inference(copy,[status(thm)],[c_22343]) ).
cnf(c_22344,plain,
commutator(commutator(A,B),C) = commutator(multiply(B,A),commutator(B,C)),
inference(paramod,[status(thm)],[c_3693,c_6]) ).
cnf(c_22345,plain,
commutator(A,commutator(B,C)) = commutator(multiply(B,A),commutator(B,C)),
inference(paramod,[status(thm)],[c_6,c_22344]) ).
cnf(c_3949,plain,
commutator(multiply(A,B),commutator(A,C)) = commutator(B,commutator(A,C)),
inference(copy,[status(thm)],[c_22345]) ).
cnf(c_22346,plain,
commutator(A,commutator(multiply(A,B),C)) = commutator(A,commutator(B,multiply(multiply(A,B),C))),
inference(paramod,[status(thm)],[c_3304,c_3347]) ).
cnf(c_22347,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(B,multiply(multiply(A,B),C))),
inference(paramod,[status(thm)],[c_3347,c_22346]) ).
cnf(c_22348,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(B,multiply(A,multiply(B,C)))),
inference(paramod,[status(thm)],[c_1,c_22347]) ).
cnf(c_4700,plain,
commutator(A,commutator(B,multiply(A,multiply(B,C)))) = commutator(A,commutator(B,C)),
inference(copy,[status(thm)],[c_22348]) ).
cnf(c_4798,plain,
multiply(A,multiply(commutator(A,B),commutator(B,A))) = A,
inference(resolve,[status(thm)],[c_147,c_5]) ).
cnf(c_4918,plain,
commutator(A,A) = multiply(commutator(B,C),commutator(C,B)),
inference(resolve,[status(thm)],[c_291,c_4798]) ).
cnf(c_22349,plain,
multiply(commutator(A,A),B) = multiply(commutator(C,D),multiply(commutator(D,C),B)),
inference(paramod,[status(thm)],[c_4918,c_1]) ).
cnf(c_22350,plain,
B = multiply(commutator(C,D),multiply(commutator(D,C),B)),
inference(paramod,[status(thm)],[c_86,c_22349]) ).
cnf(c_5039,plain,
multiply(commutator(A,B),multiply(commutator(B,A),C)) = C,
inference(copy,[status(thm)],[c_22350]) ).
cnf(c_22351,plain,
multiply(B,multiply(C,A)) = multiply(A,multiply(B,multiply(C,commutator(multiply(B,C),A)))),
inference(copy,[status(thm)],[c_13]) ).
cnf(c_22352,plain,
multiply(commutator(A,B),B) = multiply(B,commutator(multiply(A,B),B)),
inference(resolve,[status(thm)],[c_163,c_22351]) ).
cnf(c_22353,plain,
multiply(B,commutator(A,B)) = multiply(B,commutator(multiply(A,B),B)),
inference(paramod,[status(thm)],[c_691,c_22352]) ).
cnf(c_8481,plain,
multiply(A,commutator(multiply(B,A),A)) = multiply(A,commutator(B,A)),
inference(copy,[status(thm)],[c_22353]) ).
cnf(c_22354,plain,
commutator(A,B) = commutator(multiply(A,B),B),
inference(resolve,[status(thm)],[c_2566,c_8481]) ).
cnf(c_9045,plain,
commutator(multiply(A,B),B) = commutator(A,B),
inference(copy,[status(thm)],[c_22354]) ).
cnf(c_22355,plain,
commutator(commutator(A,B),multiply(A,multiply(commutator(A,B),C))) = commutator(commutator(A,B),multiply(A,C)),
inference(paramod,[status(thm)],[c_166,c_3304]) ).
cnf(c_22356,plain,
commutator(A,commutator(B,multiply(A,multiply(commutator(A,B),C)))) = commutator(commutator(A,B),multiply(A,C)),
inference(paramod,[status(thm)],[c_6,c_22355]) ).
cnf(c_22357,plain,
commutator(A,commutator(B,multiply(A,multiply(B,C)))) = commutator(commutator(A,B),multiply(A,C)),
inference(paramod,[status(thm)],[c_3349,c_22356]) ).
cnf(c_22358,plain,
commutator(A,commutator(B,C)) = commutator(commutator(A,B),multiply(A,C)),
inference(paramod,[status(thm)],[c_4700,c_22357]) ).
cnf(c_22359,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(B,multiply(A,C))),
inference(paramod,[status(thm)],[c_6,c_22358]) ).
cnf(c_9212,plain,
commutator(A,commutator(B,multiply(A,C))) = commutator(A,commutator(B,C)),
inference(copy,[status(thm)],[c_22359]) ).
cnf(c_9396,plain,
commutator(multiply(A,multiply(B,C)),C) = commutator(multiply(A,B),C),
inference(paramod,[status(thm)],[c_1,c_9045]) ).
cnf(c_22360,plain,
commutator(commutator(A,B),C) = commutator(multiply(A,B),commutator(B,C)),
inference(paramod,[status(thm)],[c_9045,c_6]) ).
cnf(c_22361,plain,
commutator(A,commutator(B,C)) = commutator(multiply(A,B),commutator(B,C)),
inference(paramod,[status(thm)],[c_6,c_22360]) ).
cnf(c_9398,plain,
commutator(multiply(A,B),commutator(B,C)) = commutator(A,commutator(B,C)),
inference(copy,[status(thm)],[c_22361]) ).
cnf(c_9418,plain,
commutator(A,A) = multiply(commutator(B,C),commutator(C,multiply(B,C))),
inference(paramod,[status(thm)],[c_9045,c_4918]) ).
cnf(c_22362,plain,
commutator(A,commutator(B,multiply(A,C))) = commutator(A,commutator(multiply(B,multiply(A,C)),C)),
inference(paramod,[status(thm)],[c_9045,c_9212]) ).
cnf(c_22363,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(multiply(B,multiply(A,C)),C)),
inference(paramod,[status(thm)],[c_9212,c_22362]) ).
cnf(c_22364,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(multiply(B,A),C)),
inference(paramod,[status(thm)],[c_9396,c_22363]) ).
cnf(c_9676,plain,
commutator(A,commutator(multiply(B,A),C)) = commutator(A,commutator(B,C)),
inference(copy,[status(thm)],[c_22364]) ).
cnf(c_22365,plain,
commutator(commutator(multiply(A,B),C),D) = commutator(multiply(A,multiply(B,C)),commutator(C,D)),
inference(paramod,[status(thm)],[c_9396,c_6]) ).
cnf(c_22366,plain,
commutator(multiply(A,B),commutator(C,D)) = commutator(multiply(A,multiply(B,C)),commutator(C,D)),
inference(paramod,[status(thm)],[c_6,c_22365]) ).
cnf(c_10093,plain,
commutator(multiply(A,multiply(B,C)),commutator(C,D)) = commutator(multiply(A,B),commutator(C,D)),
inference(copy,[status(thm)],[c_22366]) ).
cnf(c_22367,plain,
commutator(multiply(A,multiply(B,C)),commutator(C,B)) = commutator(A,commutator(multiply(B,C),B)),
inference(paramod,[status(thm)],[c_3693,c_9398]) ).
cnf(c_22368,plain,
commutator(multiply(A,B),commutator(C,B)) = commutator(A,commutator(multiply(B,C),B)),
inference(paramod,[status(thm)],[c_10093,c_22367]) ).
cnf(c_10237,plain,
commutator(multiply(A,B),commutator(C,B)) = commutator(A,commutator(C,B)),
inference(paramod,[status(thm)],[c_3693,c_22368]) ).
cnf(c_22369,plain,
multiply(commutator(A,B),commutator(C,C)) = commutator(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_9418,c_5039]) ).
cnf(c_22370,plain,
commutator(A,B) = commutator(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_286,c_22369]) ).
cnf(c_10382,plain,
commutator(A,multiply(B,A)) = commutator(A,B),
inference(copy,[status(thm)],[c_22370]) ).
cnf(c_10848,plain,
commutator(A,multiply(B,multiply(C,A))) = commutator(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_1,c_10382]) ).
cnf(c_22371,plain,
commutator(A,commutator(multiply(A,B),C)) = commutator(A,commutator(B,multiply(C,multiply(A,B)))),
inference(paramod,[status(thm)],[c_10382,c_3347]) ).
cnf(c_22372,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(B,multiply(C,multiply(A,B)))),
inference(paramod,[status(thm)],[c_3347,c_22371]) ).
cnf(c_22373,plain,
commutator(A,commutator(B,C)) = commutator(A,commutator(B,multiply(C,A))),
inference(paramod,[status(thm)],[c_10848,c_22372]) ).
cnf(c_10859,plain,
commutator(A,commutator(B,multiply(C,A))) = commutator(A,commutator(B,C)),
inference(copy,[status(thm)],[c_22373]) ).
cnf(c_11560,plain,
commutator(A,multiply(B,multiply(C,multiply(D,A)))) = commutator(A,multiply(B,multiply(C,D))),
inference(paramod,[status(thm)],[c_1,c_10848]) ).
cnf(c_22374,plain,
commutator(A,commutator(multiply(A,B),multiply(C,D))) = commutator(A,commutator(B,multiply(C,multiply(D,multiply(A,B))))),
inference(paramod,[status(thm)],[c_10848,c_3347]) ).
cnf(c_22375,plain,
commutator(A,commutator(B,multiply(C,D))) = commutator(A,commutator(B,multiply(C,multiply(D,multiply(A,B))))),
inference(paramod,[status(thm)],[c_3347,c_22374]) ).
cnf(c_22376,plain,
commutator(A,commutator(B,multiply(C,D))) = commutator(A,commutator(B,multiply(C,multiply(D,A)))),
inference(paramod,[status(thm)],[c_11560,c_22375]) ).
cnf(c_11594,plain,
commutator(A,commutator(B,multiply(C,multiply(D,A)))) = commutator(A,commutator(B,multiply(C,D))),
inference(copy,[status(thm)],[c_22376]) ).
cnf(c_22377,plain,
multiply(A,multiply(B,multiply(C,commutator(commutator(B,C),multiply(A,multiply(C,B)))))) = multiply(commutator(B,C),multiply(A,multiply(C,B))),
inference(paramod,[status(thm)],[c_11,c_228]) ).
cnf(c_22378,plain,
multiply(A,multiply(B,multiply(C,commutator(B,commutator(C,multiply(A,multiply(C,B))))))) = multiply(commutator(B,C),multiply(A,multiply(C,B))),
inference(paramod,[status(thm)],[c_6,c_22377]) ).
cnf(c_22379,plain,
multiply(A,multiply(B,multiply(C,commutator(B,commutator(C,multiply(A,C)))))) = multiply(commutator(B,C),multiply(A,multiply(C,B))),
inference(paramod,[status(thm)],[c_11594,c_22378]) ).
cnf(c_11925,plain,
multiply(A,multiply(B,multiply(C,commutator(B,commutator(C,A))))) = multiply(commutator(B,C),multiply(A,multiply(C,B))),
inference(paramod,[status(thm)],[c_10382,c_22379]) ).
cnf(c_22380,plain,
multiply(commutator(A,B),multiply(C,multiply(B,D))) = multiply(B,multiply(commutator(A,B),multiply(C,multiply(commutator(C,B),D)))),
inference(paramod,[status(thm)],[c_11,c_1149]) ).
cnf(c_19595,plain,
multiply(A,multiply(commutator(B,A),multiply(C,multiply(commutator(C,A),D)))) = multiply(commutator(B,A),multiply(C,multiply(A,D))),
inference(copy,[status(thm)],[c_22380]) ).
cnf(c_22381,plain,
multiply(commutator(a,c),multiply(b,multiply(c,a))) != multiply(a,multiply(b,multiply(c,commutator(b,a)))),
inference(paramod,[status(thm)],[c_19595,c_827]) ).
cnf(c_19864,plain,
multiply(a,multiply(b,multiply(c,commutator(b,a)))) != multiply(commutator(a,c),multiply(b,multiply(c,a))),
inference(copy,[status(thm)],[c_22381]) ).
cnf(c_22382,plain,
commutator(multiply(A,B),commutator(multiply(C,A),B)) = commutator(multiply(A,B),commutator(multiply(C,A),C)),
inference(paramod,[status(thm)],[c_3345,c_10859]) ).
cnf(c_22383,plain,
commutator(A,commutator(multiply(C,A),B)) = commutator(multiply(A,B),commutator(multiply(C,A),C)),
inference(paramod,[status(thm)],[c_10237,c_22382]) ).
cnf(c_22384,plain,
commutator(A,commutator(C,B)) = commutator(multiply(A,B),commutator(multiply(C,A),C)),
inference(paramod,[status(thm)],[c_9676,c_22383]) ).
cnf(c_22385,plain,
commutator(A,commutator(C,B)) = commutator(multiply(A,B),commutator(A,C)),
inference(paramod,[status(thm)],[c_3693,c_22384]) ).
cnf(c_21624,plain,
commutator(A,commutator(B,C)) = commutator(C,commutator(A,B)),
inference(paramod,[status(thm)],[c_3949,c_22385]) ).
cnf(c_22386,plain,
multiply(A,multiply(B,multiply(C,commutator(B,commutator(C,A))))) = multiply(B,multiply(A,multiply(C,commutator(A,B)))),
inference(paramod,[status(thm)],[c_21624,c_148]) ).
cnf(c_22285,plain,
multiply(commutator(A,B),multiply(C,multiply(B,A))) = multiply(A,multiply(C,multiply(B,commutator(C,A)))),
inference(paramod,[status(thm)],[c_11925,c_22386]) ).
cnf(c_22387,plain,
multiply(commutator(a,c),multiply(b,multiply(c,a))) != multiply(a,multiply(b,multiply(c,commutator(b,a)))),
inference(copy,[status(thm)],[c_19864]) ).
cnf(c_22286,plain,
$false,
inference(resolve,[status(thm)],[c_22285,c_22387]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP400-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.45 % Computer : n019.cluster.edu
% 0.16/0.45 % Model : x86_64 x86_64
% 0.16/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.45 % Memory : 8046.5625MB
% 0.16/0.45 % OS : Linux 6.8.0-71-generic
% 0.16/0.45 % CPULimit : 300
% 0.16/0.45 % WCLimit : 300
% 0.16/0.45 % DateTime : Fri Sep 25 14:51:34 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.45 % Process 3027306 was started by sandbox on n019,
% 0.16/0.45 % Fri Sep 25 14:51:34 2026
% 0.16/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/0.46
% 0.16/0.46 % From the command line: assign(max_seconds, 300).
% 218.39/28.20
% 218.39/28.20 % given #500 (T,wt=14): 1097 multiply(A,B) != multiply(C,A) | multiply(B,commutator(A,B)) = C. [para(5(a,1),22(a,2)),rewrite([299(3)]),flip(a)].
% 218.39/28.20
% 218.39/28.20 % SZS status Unsatisfiable for theBenchmark
% 218.39/28.20
% 218.39/28.20 % Proof 1 at 24.83 (+ 2.78) seconds.
% 218.39/28.20 % Length of proof is 83.
% 218.39/28.20 % Level of proof is 21.
% 218.39/28.20 % Maximum clause weight is 25.000.
% 218.39/28.20 % Given clauses 716.
% 218.39/28.20
% 218.39/28.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------