%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP351-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:28:41 AM UTC 2026
% Result : Unsatisfiable 88.84s 12.71s
% Output : CNFRefutation 88.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 22
% Syntax : Number of formulae : 224 ( 35 unt; 0 def)
% Number of atoms : 542 ( 541 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 459 ( 141 ~; 318 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 83 ( 0 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_identity,axiom,
! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_identity) ).
cnf(c_1,plain,
multiply(identity,A) = A,
inference(clausify,[status(thm)],[left_identity]) ).
fof(left_inverse,axiom,
! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
file('theBenchmark.p',left_inverse) ).
cnf(c_2,plain,
multiply(inverse(A),A) = identity,
inference(clausify,[status(thm)],[left_inverse]) ).
fof(associativity,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) ).
cnf(c_3,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(clausify,[status(thm)],[associativity]) ).
fof(prove_this_2,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c6,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_2) ).
cnf(c_5,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_2]) ).
fof(prove_this_3,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c6,sk_c5) = sk_c7 ),
file('theBenchmark.p',prove_this_3) ).
cnf(c_6,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_3]) ).
fof(prove_this_6,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_6) ).
cnf(c_9,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_6]) ).
fof(prove_this_7,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_7) ).
cnf(c_10,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_7]) ).
fof(prove_this_8,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_8) ).
cnf(c_11,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_8]) ).
fof(prove_this_9,axiom,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('theBenchmark.p',prove_this_9) ).
cnf(c_12,plain,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_9]) ).
fof(prove_this_11,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_11) ).
cnf(c_14,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_11]) ).
fof(prove_this_12,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_12) ).
cnf(c_15,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_12]) ).
fof(prove_this_13,axiom,
( inverse(sk_c3) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_13) ).
cnf(c_16,plain,
( inverse(sk_c3) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_13]) ).
fof(prove_this_14,axiom,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('theBenchmark.p',prove_this_14) ).
cnf(c_17,plain,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c7 ),
inference(clausify,[status(thm)],[prove_this_14]) ).
fof(prove_this_16,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_16) ).
cnf(c_19,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_16]) ).
fof(prove_this_17,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_17) ).
cnf(c_20,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_17]) ).
fof(prove_this_18,axiom,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_18) ).
cnf(c_21,plain,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_18]) ).
fof(prove_this_20,axiom,
( multiply(sk_c4,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
file('theBenchmark.p',prove_this_20) ).
cnf(c_23,plain,
( multiply(sk_c4,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(clausify,[status(thm)],[prove_this_20]) ).
fof(prove_this_21,axiom,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_21) ).
cnf(c_24,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_21]) ).
fof(prove_this_22,axiom,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_22) ).
cnf(c_25,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_22]) ).
fof(prove_this_23,axiom,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_23) ).
cnf(c_26,plain,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_23]) ).
fof(prove_this_25,axiom,
( multiply(sk_c4,sk_c6) = sk_c5
| inverse(sk_c2) = sk_c6 ),
file('theBenchmark.p',prove_this_25) ).
cnf(c_28,plain,
( multiply(sk_c4,sk_c6) = sk_c5
| inverse(sk_c2) = sk_c6 ),
inference(clausify,[status(thm)],[prove_this_25]) ).
fof(prove_this_26,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( multiply(VAR_3,sk_c6) != sk_c5
| inverse(VAR_3) != sk_c5
| inverse(VAR_2) != sk_c6
| multiply(VAR_2,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(VAR_1) != sk_c6
| multiply(VAR_1,sk_c6) != sk_c5
| inverse(VAR_0) != sk_c7
| multiply(VAR_0,sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
file('theBenchmark.p',prove_this_26) ).
cnf(c_29,plain,
( multiply(D,sk_c6) != sk_c5
| inverse(D) != sk_c5
| inverse(C) != sk_c6
| multiply(C,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
inference(clausify,[status(thm)],[prove_this_26]) ).
cnf(c_20244,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_20245,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_20244]) ).
cnf(c_33,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_20245]) ).
cnf(c_20246,plain,
( multiply(sk_c7,A) = multiply(sk_c3,multiply(sk_c6,A))
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_36,plain,
( multiply(sk_c3,multiply(sk_c6,A)) = multiply(sk_c7,A)
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(copy,[status(thm)],[c_20246]) ).
cnf(c_20247,plain,
( multiply(multiply(A,sk_c3),sk_c6) = multiply(A,sk_c7)
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_37,plain,
( multiply(A,multiply(sk_c3,sk_c6)) = multiply(A,sk_c7)
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_20247]) ).
cnf(c_46,plain,
( multiply(sk_c6,sk_c3) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_47,plain,
( multiply(sk_c5,sk_c4) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_51,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_52,plain,
( multiply(sk_c6,sk_c3) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_53,plain,
( multiply(sk_c5,sk_c4) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_64,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c3,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_25,c_2]) ).
cnf(c_237,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_33]) ).
cnf(c_264,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_33,c_33]) ).
cnf(c_265,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_264,c_237]) ).
cnf(c_266,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_265,c_2]) ).
cnf(c_398,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_264,c_2]) ).
cnf(c_20248,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_264,c_265]) ).
cnf(c_20249,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_265,c_20248]) ).
cnf(c_416,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_20249]) ).
cnf(c_20250,plain,
( multiply(C,sk_c6) != sk_c5
| inverse(C) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| multiply(inverse(sk_c6),sk_c6) != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
inference(resolve,[status(thm)],[c_416,c_29]) ).
cnf(c_435,plain,
( multiply(C,sk_c6) != sk_c5
| inverse(C) != sk_c5
| inverse(B) != sk_c6
| multiply(B,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| inverse(A) != sk_c7
| multiply(A,sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_20250]) ).
cnf(c_20251,plain,
identity = multiply(A,multiply(B,inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_398,c_3]) ).
cnf(c_506,plain,
multiply(A,multiply(B,inverse(multiply(A,B)))) = identity,
inference(copy,[status(thm)],[c_20251]) ).
cnf(c_507,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_6,c_398]) ).
cnf(c_509,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_11,c_398]) ).
cnf(c_511,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_14,c_398]) ).
cnf(c_513,plain,
( multiply(sk_c3,sk_c6) = identity
| inverse(sk_c1) = sk_c7 ),
inference(paramod,[status(thm)],[c_16,c_398]) ).
cnf(c_516,plain,
( multiply(sk_c3,sk_c6) = identity
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_21,c_398]) ).
cnf(c_518,plain,
( multiply(sk_c2,sk_c6) = identity
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_24,c_398]) ).
cnf(c_520,plain,
( multiply(sk_c3,sk_c6) = identity
| inverse(sk_c2) = sk_c6 ),
inference(paramod,[status(thm)],[c_26,c_398]) ).
cnf(c_522,plain,
( multiply(sk_c2,sk_c6) = identity
| multiply(sk_c4,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_28,c_398]) ).
cnf(c_523,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c6,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_52,c_398]) ).
cnf(c_524,plain,
( multiply(sk_c1,sk_c7) = identity
| multiply(sk_c5,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_53,c_398]) ).
cnf(c_724,plain,
( multiply(inverse(multiply(sk_c3,sk_c6)),sk_c7) = identity
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_37,c_2]) ).
cnf(c_1629,plain,
( multiply(sk_c7,sk_c1) = identity
| multiply(sk_c3,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_513,c_2]) ).
cnf(c_1716,plain,
( multiply(sk_c6,sk_c2) = identity
| multiply(sk_c3,sk_c6) = identity ),
inference(paramod,[status(thm)],[c_520,c_2]) ).
cnf(c_20252,plain,
multiply(inverse(A),identity) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_506,c_33]) ).
cnf(c_20253,plain,
inverse(A) = multiply(B,inverse(multiply(A,B))),
inference(paramod,[status(thm)],[c_265,c_20252]) ).
cnf(c_4965,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(copy,[status(thm)],[c_20253]) ).
cnf(c_20254,plain,
( identity = multiply(sk_c7,inverse(multiply(sk_c3,sk_c6)))
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_506,c_36]) ).
cnf(c_4968,plain,
( multiply(sk_c7,inverse(multiply(sk_c3,sk_c6))) = identity
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(copy,[status(thm)],[c_20254]) ).
cnf(c_20255,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_4965,c_33]) ).
cnf(c_5000,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_20255]) ).
cnf(c_5020,plain,
( multiply(sk_c7,multiply(inverse(sk_c6),inverse(sk_c3))) = identity
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_5000,c_4968]) ).
cnf(c_20256,plain,
( multiply(multiply(inverse(sk_c6),inverse(sk_c3)),sk_c7) = identity
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_5000,c_724]) ).
cnf(c_5028,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c3),sk_c7)) = identity
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_20256]) ).
cnf(c_20257,plain,
( identity = sk_c7
| multiply(sk_c6,sk_c5) = sk_c7
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(paramod,[status(thm)],[c_507,c_5]) ).
cnf(c_5031,plain,
( identity = sk_c7
| multiply(sk_c6,sk_c5) = sk_c7 ),
inference(copy,[status(thm)],[c_20257]) ).
cnf(c_5035,plain,
( multiply(inverse(sk_c6),sk_c7) = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5031,c_33]) ).
cnf(c_20258,plain,
( multiply(multiply(A,inverse(sk_c6)),sk_c7) = multiply(A,sk_c5)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_5035,c_3]) ).
cnf(c_5567,plain,
( multiply(A,multiply(inverse(sk_c6),sk_c7)) = multiply(A,sk_c5)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_3,c_20258]) ).
cnf(c_20259,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(paramod,[status(thm)],[c_509,c_10]) ).
cnf(c_5593,plain,
( identity = sk_c7
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(copy,[status(thm)],[c_20259]) ).
cnf(c_20260,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_511,c_9]) ).
cnf(c_5753,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_20260]) ).
cnf(c_5758,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_5753,c_33]) ).
cnf(c_20261,plain,
( identity = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(paramod,[status(thm)],[c_516,c_20]) ).
cnf(c_6072,plain,
( identity = sk_c7
| multiply(sk_c2,sk_c6) = sk_c5 ),
inference(copy,[status(thm)],[c_20261]) ).
cnf(c_20262,plain,
( multiply(sk_c6,sk_c7) = sk_c5
| identity = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(paramod,[status(thm)],[c_518,c_19]) ).
cnf(c_6290,plain,
( identity = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(copy,[status(thm)],[c_20262]) ).
cnf(c_6627,plain,
( multiply(inverse(sk_c6),sk_c5) = sk_c7
| identity = sk_c5 ),
inference(paramod,[status(thm)],[c_6290,c_33]) ).
cnf(c_20263,plain,
( multiply(B,sk_c6) != sk_c5
| inverse(B) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| multiply(inverse(sk_c7),sk_c7) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
inference(resolve,[status(thm)],[c_435,c_416]) ).
cnf(c_6765,plain,
( multiply(B,sk_c6) != sk_c5
| inverse(B) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_20263]) ).
cnf(c_6950,plain,
( multiply(inverse(sk_c5),sk_c6) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7 ),
inference(resolve,[status(thm)],[c_6765,c_416]) ).
cnf(c_20264,plain,
( multiply(sk_c6,sk_c3) = identity
| identity = sk_c6
| multiply(sk_c6,sk_c3) = identity ),
inference(paramod,[status(thm)],[c_523,c_46]) ).
cnf(c_7064,plain,
( identity = sk_c6
| multiply(sk_c6,sk_c3) = identity ),
inference(copy,[status(thm)],[c_20264]) ).
cnf(c_20265,plain,
( multiply(inverse(sk_c6),identity) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7064,c_33]) ).
cnf(c_7067,plain,
( inverse(sk_c6) = sk_c3
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_265,c_20265]) ).
cnf(c_7072,plain,
( multiply(sk_c3,sk_c6) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7067,c_2]) ).
cnf(c_20266,plain,
( multiply(sk_c3,sk_c5) = sk_c7
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7067,c_5758]) ).
cnf(c_7137,plain,
( multiply(sk_c3,sk_c5) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20266]) ).
cnf(c_7333,plain,
( multiply(inverse(sk_c3),sk_c7) = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7137,c_33]) ).
cnf(c_20267,plain,
( multiply(sk_c5,sk_c4) = identity
| identity = sk_c6
| multiply(sk_c5,sk_c4) = identity ),
inference(paramod,[status(thm)],[c_524,c_47]) ).
cnf(c_7353,plain,
( identity = sk_c6
| multiply(sk_c5,sk_c4) = identity ),
inference(copy,[status(thm)],[c_20267]) ).
cnf(c_20268,plain,
( multiply(inverse(sk_c5),identity) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7353,c_33]) ).
cnf(c_7743,plain,
( inverse(sk_c5) = sk_c4
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_265,c_20268]) ).
cnf(c_20269,plain,
( multiply(sk_c7,sk_c1) = identity
| identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(paramod,[status(thm)],[c_1629,c_51]) ).
cnf(c_9275,plain,
( identity = sk_c7
| multiply(sk_c7,sk_c1) = identity ),
inference(copy,[status(thm)],[c_20269]) ).
cnf(c_20270,plain,
( multiply(inverse(sk_c7),identity) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9275,c_33]) ).
cnf(c_9278,plain,
( inverse(sk_c7) = sk_c1
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_265,c_20270]) ).
cnf(c_9391,plain,
( multiply(sk_c1,sk_c7) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9278,c_2]) ).
cnf(c_20271,plain,
( identity = sk_c7
| identity = sk_c6
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_9391,c_5593]) ).
cnf(c_9481,plain,
( identity = sk_c6
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_20271]) ).
cnf(c_9483,plain,
( multiply(A,sk_c7) = A
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9481,c_265]) ).
cnf(c_20272,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9481,c_7072]) ).
cnf(c_9493,plain,
( multiply(sk_c3,sk_c6) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20272]) ).
cnf(c_20273,plain,
( identity = sk_c6
| sk_c6 = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9483,c_5753]) ).
cnf(c_20274,plain,
( identity = sk_c6
| sk_c5 = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20273]) ).
cnf(c_9721,plain,
( sk_c5 = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20274]) ).
cnf(c_20275,plain,
( inverse(sk_c3) = sk_c5
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9483,c_7333]) ).
cnf(c_9726,plain,
( inverse(sk_c3) = sk_c5
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20275]) ).
cnf(c_9742,plain,
( inverse(sk_c6) = identity
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_9721,c_266]) ).
cnf(c_20276,plain,
( multiply(identity,sk_c5) = sk_c7
| identity = sk_c5
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_9742,c_6627]) ).
cnf(c_20277,plain,
( sk_c5 = sk_c7
| identity = sk_c5
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_1,c_20276]) ).
cnf(c_9885,plain,
( sk_c7 = sk_c5
| identity = sk_c5
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_20277]) ).
cnf(c_10218,plain,
( multiply(inverse(sk_c3),sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9493,c_33]) ).
cnf(c_20278,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6
| sk_c7 = sk_c5
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_9885,c_9721]) ).
cnf(c_20279,plain,
( sk_c5 = sk_c6
| sk_c7 = sk_c5
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_20278]) ).
cnf(c_10714,plain,
( sk_c7 = sk_c5
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_20279]) ).
cnf(c_20280,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_9726,c_10218]) ).
cnf(c_10976,plain,
( multiply(sk_c5,sk_c7) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20280]) ).
cnf(c_10979,plain,
( multiply(inverse(sk_c5),sk_c6) = sk_c7
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_10976,c_33]) ).
cnf(c_20281,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_7743,c_10979]) ).
cnf(c_11211,plain,
( multiply(sk_c4,sk_c6) = sk_c7
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20281]) ).
cnf(c_11231,plain,
( multiply(inverse(sk_c4),sk_c7) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_11211,c_33]) ).
cnf(c_20282,plain,
( sk_c6 = inverse(sk_c4)
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_11231,c_9483]) ).
cnf(c_20283,plain,
( inverse(sk_c4) = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20282]) ).
cnf(c_12084,plain,
( inverse(sk_c4) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20283]) ).
cnf(c_12162,plain,
( multiply(sk_c4,sk_c6) = identity
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_12084,c_398]) ).
cnf(c_12792,plain,
( identity = sk_c5
| multiply(sk_c2,sk_c6) = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_12162,c_23]) ).
cnf(c_12799,plain,
( multiply(sk_c2,sk_c6) = identity
| identity = sk_c5
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_12162,c_522]) ).
cnf(c_20284,plain,
( multiply(sk_c6,sk_c2) = identity
| identity = sk_c7
| multiply(sk_c6,sk_c2) = identity ),
inference(paramod,[status(thm)],[c_1716,c_64]) ).
cnf(c_13031,plain,
( identity = sk_c7
| multiply(sk_c6,sk_c2) = identity ),
inference(copy,[status(thm)],[c_20284]) ).
cnf(c_20285,plain,
( multiply(inverse(sk_c6),identity) = sk_c2
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_13031,c_33]) ).
cnf(c_13034,plain,
( inverse(sk_c6) = sk_c2
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_265,c_20285]) ).
cnf(c_13043,plain,
( multiply(sk_c2,sk_c6) = identity
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_13034,c_2]) ).
cnf(c_20286,plain,
( identity = sk_c7
| identity = sk_c5
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_13043,c_6072]) ).
cnf(c_13394,plain,
( identity = sk_c5
| identity = sk_c7 ),
inference(copy,[status(thm)],[c_20286]) ).
cnf(c_20287,plain,
( identity = sk_c5
| identity = sk_c5
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_10714,c_13394]) ).
cnf(c_13416,plain,
( identity = sk_c5
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_20287]) ).
cnf(c_20288,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(paramod,[status(thm)],[c_13416,c_9721]) ).
cnf(c_20289,plain,
( sk_c5 = sk_c6
| sk_c5 = sk_c6 ),
inference(copy,[status(thm)],[c_20288]) ).
cnf(c_13437,plain,
sk_c5 = sk_c6,
inference(copy,[status(thm)],[c_20289]) ).
cnf(c_20290,plain,
( multiply(sk_c2,sk_c6) = identity
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13437,c_12799]) ).
cnf(c_13651,plain,
( multiply(sk_c2,sk_c6) = identity
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20290]) ).
cnf(c_20291,plain,
( identity = sk_c5
| multiply(sk_c2,sk_c6) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13437,c_12792]) ).
cnf(c_20292,plain,
( identity = sk_c6
| multiply(sk_c2,sk_c6) = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13437,c_20291]) ).
cnf(c_13658,plain,
( multiply(sk_c2,sk_c6) = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20292]) ).
cnf(c_20293,plain,
( multiply(inverse(sk_c5),sk_c6) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c5
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_6950]) ).
cnf(c_20294,plain,
( multiply(inverse(sk_c5),sk_c6) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5
| identity != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_20293]) ).
cnf(c_20295,plain,
( multiply(inverse(sk_c5),sk_c6) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_20294]) ).
cnf(c_20296,plain,
( multiply(inverse(sk_c6),sk_c6) != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_20295]) ).
cnf(c_20297,plain,
( identity != sk_c5
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_2,c_20296]) ).
cnf(c_20298,plain,
( identity != sk_c6
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_20297]) ).
cnf(c_20299,plain,
( identity != sk_c6
| inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(copy,[status(thm)],[c_20298]) ).
cnf(c_15537,plain,
( inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| identity != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(copy,[status(thm)],[c_20299]) ).
cnf(c_16048,plain,
( multiply(A,multiply(inverse(sk_c6),sk_c7)) = multiply(A,sk_c6)
| identity = sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_5567]) ).
cnf(c_16218,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c3),sk_c7)) = identity
| multiply(sk_c6,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_5028]) ).
cnf(c_16225,plain,
( multiply(sk_c7,multiply(inverse(sk_c6),inverse(sk_c3))) = identity
| multiply(sk_c6,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_13437,c_5020]) ).
cnf(c_20300,plain,
( sk_c6 = identity
| identity = sk_c6
| identity = sk_c6 ),
inference(paramod,[status(thm)],[c_13658,c_13651]) ).
cnf(c_20301,plain,
( identity = sk_c6
| identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20300]) ).
cnf(c_20302,plain,
( identity = sk_c6
| identity = sk_c6 ),
inference(copy,[status(thm)],[c_20301]) ).
cnf(c_19427,plain,
identity = sk_c6,
inference(copy,[status(thm)],[c_20302]) ).
cnf(c_20002,plain,
( multiply(sk_c7,multiply(inverse(sk_c6),inverse(sk_c3))) = sk_c6
| multiply(sk_c6,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_19427,c_16225]) ).
cnf(c_20009,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c3),sk_c7)) = sk_c6
| multiply(sk_c6,sk_c6) = sk_c7 ),
inference(paramod,[status(thm)],[c_19427,c_16218]) ).
cnf(c_20303,plain,
( multiply(A,multiply(inverse(sk_c6),sk_c7)) = multiply(A,sk_c6)
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_19427,c_16048]) ).
cnf(c_20020,plain,
( multiply(A,multiply(inverse(sk_c6),sk_c7)) = multiply(A,sk_c6)
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_20303]) ).
cnf(c_20304,plain,
( inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| sk_c6 != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(paramod,[status(thm)],[c_19427,c_15537]) ).
cnf(c_20039,plain,
( inverse(A) != sk_c6
| multiply(A,sk_c6) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(copy,[status(thm)],[c_20304]) ).
cnf(c_20305,plain,
inverse(sk_c6) = identity,
inference(paramod,[status(thm)],[c_19427,c_266]) ).
cnf(c_20186,plain,
inverse(sk_c6) = sk_c6,
inference(paramod,[status(thm)],[c_19427,c_20305]) ).
cnf(c_20187,plain,
multiply(A,sk_c6) = A,
inference(paramod,[status(thm)],[c_19427,c_265]) ).
cnf(c_20192,plain,
multiply(sk_c6,A) = A,
inference(paramod,[status(thm)],[c_19427,c_1]) ).
cnf(c_20306,plain,
( inverse(sk_c6) != sk_c6
| multiply(sk_c6,sk_c7) != sk_c6
| multiply(sk_c6,sk_c6) != sk_c7 ),
inference(factor,[status(thm)],[c_20039]) ).
cnf(c_20307,plain,
( inverse(sk_c6) != sk_c6
| multiply(sk_c6,sk_c7) != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_20187,c_20306]) ).
cnf(c_20308,plain,
( inverse(sk_c6) != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_20192,c_20307]) ).
cnf(c_20309,plain,
( sk_c6 != sk_c6
| sk_c7 != sk_c6
| sk_c6 != sk_c7 ),
inference(paramod,[status(thm)],[c_20186,c_20308]) ).
cnf(c_20310,plain,
( sk_c6 != sk_c6
| sk_c7 != sk_c6
| sk_c7 != sk_c6 ),
inference(copy,[status(thm)],[c_20309]) ).
cnf(c_20311,plain,
( sk_c7 != sk_c6
| sk_c7 != sk_c6 ),
inference(copy,[status(thm)],[c_20310]) ).
cnf(c_20230,plain,
sk_c7 != sk_c6,
inference(copy,[status(thm)],[c_20311]) ).
cnf(c_20312,plain,
( multiply(A,multiply(sk_c6,sk_c7)) = multiply(A,sk_c6)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_20186,c_20020]) ).
cnf(c_20313,plain,
( multiply(A,sk_c7) = multiply(A,sk_c6)
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_20192,c_20312]) ).
cnf(c_20314,plain,
( multiply(A,sk_c7) = A
| sk_c7 = sk_c6 ),
inference(paramod,[status(thm)],[c_20187,c_20313]) ).
cnf(c_20238,plain,
multiply(A,sk_c7) = A,
inference(resolve,[status(thm)],[c_20230,c_20314]) ).
cnf(c_20315,plain,
( multiply(inverse(sk_c6),multiply(inverse(sk_c3),sk_c7)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20187,c_20009]) ).
cnf(c_20316,plain,
( multiply(sk_c6,multiply(inverse(sk_c3),sk_c7)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20186,c_20315]) ).
cnf(c_20317,plain,
( multiply(sk_c6,inverse(sk_c3)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20238,c_20316]) ).
cnf(c_20318,plain,
( inverse(sk_c3) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20192,c_20317]) ).
cnf(c_20319,plain,
( inverse(sk_c3) = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_20318]) ).
cnf(c_20240,plain,
inverse(sk_c3) = sk_c6,
inference(resolve,[status(thm)],[c_20230,c_20319]) ).
cnf(c_20320,plain,
( multiply(sk_c7,multiply(inverse(sk_c6),inverse(sk_c3))) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20187,c_20002]) ).
cnf(c_20321,plain,
( multiply(sk_c7,multiply(sk_c6,inverse(sk_c3))) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20186,c_20320]) ).
cnf(c_20322,plain,
( multiply(sk_c7,multiply(sk_c6,sk_c6)) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20240,c_20321]) ).
cnf(c_20323,plain,
( multiply(sk_c7,sk_c6) = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20187,c_20322]) ).
cnf(c_20324,plain,
( sk_c7 = sk_c6
| sk_c6 = sk_c7 ),
inference(paramod,[status(thm)],[c_20187,c_20323]) ).
cnf(c_20325,plain,
( sk_c7 = sk_c6
| sk_c7 = sk_c6 ),
inference(copy,[status(thm)],[c_20324]) ).
cnf(c_20326,plain,
sk_c7 = sk_c6,
inference(copy,[status(thm)],[c_20325]) ).
cnf(c_20243,plain,
$false,
inference(resolve,[status(thm)],[c_20230,c_20326]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP351-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n020.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 14:48:34 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 3176315 was started by sandbox2 on n020,
% 0.17/0.44 % Fri Sep 25 14:48:34 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 88.84/12.71
% 88.84/12.71 % given #500 (T,wt=7): 18833 sk_c3 = sk_c2 | inverse(sk_c6) = sk_c6. [para(18749(a,1),18756(b,2)),merge(b)].
% 88.84/12.71
% 88.84/12.71 % SZS status Unsatisfiable for theBenchmark
% 88.84/12.71
% 88.84/12.71 % Proof 1 at 10.66 (+ 1.46) seconds.
% 88.84/12.71 % Length of proof is 119.
% 88.84/12.71 % Level of proof is 25.
% 88.84/12.71 % Maximum clause weight is 46.000.
% 88.84/12.71 % Given clauses 533.
% 88.84/12.71
% 88.84/12.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------