%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP061-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:26:54 AM UTC 2026
% Result : Unsatisfiable 28.77s 4.63s
% Output : CNFRefutation 28.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 2
% Syntax : Number of formulae : 153 ( 148 unt; 0 def)
% Number of atoms : 161 ( 160 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 812 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : inverse(multiply(VAR_0,multiply(VAR_1,multiply(multiply(inverse(VAR_1),VAR_2),inverse(multiply(VAR_3,multiply(VAR_0,VAR_2))))))) = VAR_3,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms,axiom,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('theBenchmark.p',prove_these_axioms) ).
cnf(c_2,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(clausify,[status(thm)],[prove_these_axioms]) ).
cnf(c_3,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ),
inference(copy,[status(thm)],[c_2]) ).
cnf(c_4,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F))))))) = V6,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_5,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),C),inverse(multiply(D,multiply(E,C))))),D)))) = E,
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_12,plain,
inverse(multiply(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))),multiply(multiply(E,multiply(F,multiply(multiply(inverse(F),V6),inverse(multiply(V7,multiply(E,V6)))))),multiply(multiply(V7,multiply(multiply(D,V8),inverse(multiply(V9,multiply(V10,V8))))),V9)))) = V10,
inference(paramod,[status(thm)],[c_4,c_4]) ).
cnf(c_13,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = C,
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_17,plain,
inverse(multiply(A,multiply(multiply(B,multiply(multiply(C,multiply(D,multiply(multiply(inverse(D),E),inverse(multiply(F,multiply(C,E)))))),multiply(multiply(F,V6),inverse(multiply(V7,multiply(B,V6)))))),multiply(multiply(V7,multiply(multiply(inverse(A),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)))) = V10,
inference(paramod,[status(thm)],[c_4,c_5]) ).
cnf(c_8421,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(C,D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = multiply(V6,multiply(V7,multiply(multiply(inverse(V7),V8),inverse(multiply(C,multiply(V6,V8)))))),
inference(paramod,[status(thm)],[c_4,c_5]) ).
cnf(c_19,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(D,V6),inverse(multiply(V7,multiply(V8,V6))))),V7)),V8)))),
inference(copy,[status(thm)],[c_8421]) ).
cnf(c_20,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),V6),inverse(multiply(V7,multiply(V8,V6))))),V7)))) = V8,
inference(paramod,[status(thm)],[c_5,c_5]) ).
cnf(c_521,plain,
inverse(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(C,D),inverse(multiply(E,multiply(F,D))))),E)),F))))) = C,
inference(paramod,[status(thm)],[c_19,c_1]) ).
cnf(c_536,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(inverse(D),multiply(A,C)))))) = D,
inference(paramod,[status(thm)],[c_19,c_13]) ).
cnf(c_672,plain,
inverse(multiply(A,multiply(B,multiply(C,inverse(multiply(D,multiply(A,multiply(E,multiply(multiply(inverse(E),F),inverse(multiply(inverse(C),multiply(inverse(B),F)))))))))))) = D,
inference(paramod,[status(thm)],[c_536,c_1]) ).
cnf(c_8422,plain,
inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,inverse(multiply(D,multiply(E,multiply(multiply(inverse(E),multiply(multiply(inverse(D),multiply(multiply(inverse(B),F),inverse(multiply(V6,multiply(V7,F))))),V6)),V7)))))))))) = C,
inference(paramod,[status(thm)],[c_19,c_672]) ).
cnf(c_1418,plain,
inverse(multiply(inverse(A),multiply(A,multiply(B,inverse(multiply(C,B)))))) = C,
inference(paramod,[status(thm)],[c_13,c_8422]) ).
cnf(c_8423,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(inverse(A),V6),inverse(multiply(V7,multiply(V8,V6))))),V7)),V8)))),
inference(paramod,[status(thm)],[c_1418,c_19]) ).
cnf(c_1544,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(C,inverse(multiply(D,C)))),D))) = A,
inference(paramod,[status(thm)],[c_13,c_8423]) ).
cnf(c_8424,plain,
inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,multiply(A,multiply(D,multiply(multiply(inverse(D),multiply(E,inverse(multiply(F,E)))),F))))))))) = C,
inference(paramod,[status(thm)],[c_1418,c_672]) ).
cnf(c_1578,plain,
inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(C,A)))))) = C,
inference(paramod,[status(thm)],[c_1544,c_8424]) ).
cnf(c_1582,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(C,inverse(multiply(D,C)))),D)))) = inverse(B),
inference(paramod,[status(thm)],[c_1418,c_1418]) ).
cnf(c_1706,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(multiply(C,D)))),C)))) = D,
inference(paramod,[status(thm)],[c_1578,c_1418]) ).
cnf(c_1710,plain,
inverse(multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,C)))),multiply(D,multiply(inverse(D),B)))) = C,
inference(paramod,[status(thm)],[c_1578,c_1578]) ).
cnf(c_8425,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),multiply(A,multiply(D,multiply(multiply(inverse(D),multiply(E,inverse(multiply(F,E)))),F)))))))) = C,
inference(paramod,[status(thm)],[c_1544,c_536]) ).
cnf(c_1781,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),A))))) = C,
inference(paramod,[status(thm)],[c_1544,c_8425]) ).
cnf(c_1811,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(C,multiply(D,inverse(multiply(E,D)))),E)),inverse(C)))) = A,
inference(paramod,[status(thm)],[c_1418,c_1544]) ).
cnf(c_1814,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(multiply(D,E)))),D)),E))) = A,
inference(paramod,[status(thm)],[c_1578,c_1544]) ).
cnf(c_1939,plain,
multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),multiply(D,multiply(inverse(D),C))) = A,
inference(paramod,[status(thm)],[c_1418,c_1781]) ).
cnf(c_1942,plain,
multiply(multiply(A,multiply(inverse(A),inverse(multiply(B,inverse(C))))),multiply(D,multiply(inverse(D),B))) = C,
inference(paramod,[status(thm)],[c_1578,c_1781]) ).
cnf(c_2460,plain,
multiply(multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))),D) = A,
inference(paramod,[status(thm)],[c_1781,c_1939]) ).
cnf(c_8426,plain,
inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(F,D))))),E)),F)))) = multiply(inverse(V6),multiply(V6,multiply(multiply(C,multiply(V7,inverse(multiply(V8,V7)))),V8))),
inference(paramod,[status(thm)],[c_1582,c_13]) ).
cnf(c_8427,plain,
C = multiply(inverse(V6),multiply(V6,multiply(multiply(C,multiply(V7,inverse(multiply(V8,V7)))),V8))),
inference(paramod,[status(thm)],[c_13,c_8426]) ).
cnf(c_2496,plain,
multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(C,inverse(multiply(D,C)))),D))) = B,
inference(copy,[status(thm)],[c_8427]) ).
cnf(c_8428,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),C)),D)))) = multiply(E,multiply(multiply(inverse(E),F),inverse(multiply(C,multiply(D,F))))),
inference(paramod,[status(thm)],[c_1,c_1706]) ).
cnf(c_2999,plain,
multiply(A,multiply(multiply(inverse(A),B),inverse(multiply(C,multiply(D,B))))) = inverse(multiply(inverse(E),multiply(E,multiply(multiply(F,multiply(inverse(F),C)),D)))),
inference(copy,[status(thm)],[c_8428]) ).
cnf(c_8429,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),C)),D)))) = multiply(multiply(E,multiply(F,multiply(multiply(inverse(F),V6),inverse(multiply(V7,multiply(E,V6)))))),multiply(multiply(V7,V8),inverse(multiply(C,multiply(D,V8))))),
inference(paramod,[status(thm)],[c_4,c_1706]) ).
cnf(c_3004,plain,
multiply(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))) = inverse(multiply(inverse(V7),multiply(V7,multiply(multiply(V8,multiply(inverse(V8),F)),V6)))),
inference(copy,[status(thm)],[c_8429]) ).
cnf(c_8430,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),C)),multiply(D,multiply(E,multiply(multiply(inverse(E),F),inverse(multiply(V6,multiply(D,F)))))))))) = multiply(multiply(V7,multiply(V8,multiply(multiply(inverse(V8),V9),inverse(multiply(V10,multiply(V7,V9)))))),multiply(multiply(V10,multiply(multiply(V6,V11),inverse(multiply(V12,multiply(C,V11))))),V12)),
inference(paramod,[status(thm)],[c_12,c_1706]) ).
cnf(c_3112,plain,
multiply(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(inverse(V8),multiply(V8,multiply(multiply(V9,multiply(inverse(V9),V7)),multiply(V10,multiply(V11,multiply(multiply(inverse(V11),V12),inverse(multiply(E,multiply(V10,V12)))))))))),
inference(copy,[status(thm)],[c_8430]) ).
cnf(c_8431,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),C)),D)))) = multiply(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),V7),inverse(multiply(V8,multiply(F,V7)))))),multiply(multiply(V8,V9),inverse(multiply(V10,multiply(E,V9)))))),multiply(multiply(V10,multiply(multiply(inverse(D),V11),inverse(multiply(V12,multiply(C,V11))))),V12)),
inference(paramod,[status(thm)],[c_17,c_1706]) ).
cnf(c_3150,plain,
multiply(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(multiply(V6,multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)) = inverse(multiply(inverse(V11),multiply(V11,multiply(multiply(V12,multiply(inverse(V12),V10)),V7)))),
inference(copy,[status(thm)],[c_8431]) ).
cnf(c_3607,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),multiply(V6,multiply(multiply(V7,multiply(V8,inverse(multiply(V9,V8)))),V9))),inverse(multiply(V10,V7)))),V10)))) = inverse(V6),
inference(paramod,[status(thm)],[c_2496,c_20]) ).
cnf(c_4138,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(D)))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(multiply(D,multiply(V6,inverse(multiply(multiply(inverse(inverse(V7)),inverse(multiply(inverse(multiply(A,C)),V7))),V6)))),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10)))),
inference(paramod,[status(thm)],[c_2460,c_19]) ).
cnf(c_8432,plain,
inverse(inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(C,inverse(multiply(D,multiply(E,F))))),D)),E))))) = multiply(C,multiply(V6,inverse(multiply(multiply(inverse(inverse(V7)),inverse(multiply(inverse(F),V7))),V6)))),
inference(paramod,[status(thm)],[c_2460,c_521]) ).
cnf(c_4148,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))) = inverse(inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(A,inverse(multiply(V6,multiply(V7,D))))),V6)),V7))))),
inference(copy,[status(thm)],[c_8432]) ).
cnf(c_8433,plain,
inverse(multiply(A,multiply(B,multiply(inverse(B),inverse(C))))) = multiply(C,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(A),E))),D)))),
inference(paramod,[status(thm)],[c_2460,c_1578]) ).
cnf(c_4187,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))) = inverse(multiply(D,multiply(E,multiply(inverse(E),inverse(A))))),
inference(copy,[status(thm)],[c_8433]) ).
cnf(c_4220,plain,
multiply(A,multiply(B,multiply(inverse(B),C))) = multiply(A,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(multiply(F,inverse(multiply(C,F)))),E))),D)))),
inference(paramod,[status(thm)],[c_2460,c_1939]) ).
cnf(c_4231,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),multiply(C,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(F),E))),D)))))))) = F,
inference(paramod,[status(thm)],[c_2460,c_1706]) ).
cnf(c_8434,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),V6),inverse(multiply(V7,V8)))),V7)))) = multiply(V8,multiply(V9,inverse(multiply(multiply(inverse(inverse(V10)),inverse(multiply(inverse(V6),V10))),V9)))),
inference(paramod,[status(thm)],[c_2460,c_20]) ).
cnf(c_4248,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(inverse(D),C))),B)))) = inverse(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),V7),inverse(multiply(V8,multiply(V9,V7))))),V8))),multiply(multiply(V9,multiply(multiply(inverse(E),D),inverse(multiply(V10,A)))),V10)))),
inference(copy,[status(thm)],[c_8434]) ).
cnf(c_4258,plain,
multiply(multiply(A,multiply(inverse(A),inverse(B))),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(inverse(F)),E))),D))))))) = F,
inference(paramod,[status(thm)],[c_2460,c_1942]) ).
cnf(c_8435,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D)),multiply(E,multiply(multiply(inverse(E),multiply(F,inverse(multiply(V6,F)))),V6))))) = A,
inference(paramod,[status(thm)],[c_1544,c_1814]) ).
cnf(c_4545,plain,
multiply(A,multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D)))) = A,
inference(paramod,[status(thm)],[c_1544,c_8435]) ).
cnf(c_4728,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_4545,c_1418]) ).
cnf(c_4757,plain,
multiply(A,multiply(B,inverse(multiply(multiply(multiply(C,multiply(inverse(C),inverse(D))),D),B)))) = A,
inference(paramod,[status(thm)],[c_4545,c_1939]) ).
cnf(c_4793,plain,
multiply(multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(E))))),multiply(F,inverse(F))) = E,
inference(paramod,[status(thm)],[c_4545,c_1942]) ).
cnf(c_8436,plain,
inverse(multiply(inverse(A),A)) = multiply(multiply(B,multiply(inverse(B),inverse(C))),C),
inference(paramod,[status(thm)],[c_4757,c_1]) ).
cnf(c_5359,plain,
multiply(multiply(A,multiply(inverse(A),inverse(B))),B) = inverse(multiply(inverse(C),C)),
inference(copy,[status(thm)],[c_8436]) ).
cnf(c_5525,plain,
multiply(multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(multiply(multiply(D,multiply(inverse(D),inverse(E))),E),C))),B)))),multiply(F,inverse(F))) = A,
inference(paramod,[status(thm)],[c_4757,c_1939]) ).
cnf(c_5529,plain,
multiply(inverse(A),multiply(A,multiply(B,multiply(multiply(C,multiply(inverse(C),inverse(D))),D)))) = B,
inference(paramod,[status(thm)],[c_4757,c_2496]) ).
cnf(c_5530,plain,
multiply(inverse(A),multiply(A,multiply(B,multiply(C,inverse(multiply(multiply(D,inverse(multiply(multiply(multiply(E,multiply(inverse(E),inverse(F))),F),D))),C)))))) = B,
inference(paramod,[status(thm)],[c_4757,c_2496]) ).
cnf(c_8437,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),multiply(multiply(D,multiply(inverse(D),inverse(E))),E)))) = inverse(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),multiply(multiply(inverse(multiply(A,C)),V7),inverse(multiply(V8,multiply(V9,V7))))),V8)),V9)))),
inference(paramod,[status(thm)],[c_5359,c_19]) ).
cnf(c_5734,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),multiply(multiply(D,multiply(inverse(D),inverse(E))),E)))) = multiply(A,C),
inference(paramod,[status(thm)],[c_13,c_8437]) ).
cnf(c_5858,plain,
multiply(inverse(A),multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(D,multiply(inverse(D),inverse(E))),E))),inverse(C)))) = B,
inference(paramod,[status(thm)],[c_5359,c_2496]) ).
cnf(c_8438,plain,
inverse(inverse(multiply(inverse(A),A))) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_5359,c_1710]) ).
cnf(c_5905,plain,
multiply(inverse(A),A) = inverse(inverse(multiply(inverse(B),B))),
inference(copy,[status(thm)],[c_8438]) ).
cnf(c_8439,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(multiply(inverse(C),C),multiply(D,inverse(multiply(E,D)))),E)),multiply(multiply(F,multiply(inverse(F),inverse(V6))),V6)))) = A,
inference(paramod,[status(thm)],[c_5359,c_1811]) ).
cnf(c_5923,plain,
multiply(A,multiply(multiply(multiply(inverse(B),B),multiply(C,inverse(multiply(D,C)))),D)) = A,
inference(paramod,[status(thm)],[c_5734,c_8439]) ).
cnf(c_5930,plain,
multiply(A,multiply(B,multiply(inverse(B),inverse(multiply(inverse(C),C))))) = A,
inference(paramod,[status(thm)],[c_5359,c_4545]) ).
cnf(c_8440,plain,
multiply(A,multiply(inverse(multiply(inverse(B),B)),multiply(multiply(multiply(inverse(C),C),multiply(D,inverse(multiply(E,D)))),E))) = A,
inference(paramod,[status(thm)],[c_5905,c_1544]) ).
cnf(c_6189,plain,
multiply(A,inverse(multiply(inverse(B),B))) = A,
inference(paramod,[status(thm)],[c_5923,c_8440]) ).
cnf(c_6222,plain,
multiply(inverse(A),multiply(A,multiply(inverse(inverse(multiply(inverse(B),B))),C))) = inverse(multiply(D,inverse(multiply(C,D)))),
inference(paramod,[status(thm)],[c_5905,c_2496]) ).
cnf(c_6342,plain,
multiply(inverse(A),A) = multiply(inverse(B),B),
inference(paramod,[status(thm)],[c_5905,c_5905]) ).
cnf(c_6350,plain,
multiply(A,multiply(B,inverse(B))) = A,
inference(paramod,[status(thm)],[c_6189,c_5930]) ).
cnf(c_6401,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(resolve,[status(thm)],[c_6342,c_3]) ).
cnf(c_6404,plain,
multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(multiply(multiply(D,multiply(inverse(D),inverse(E))),E),C))),B)))) = A,
inference(paramod,[status(thm)],[c_6350,c_5525]) ).
cnf(c_6405,plain,
multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,multiply(inverse(B),multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_6350,c_4793]) ).
cnf(c_6418,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(paramod,[status(thm)],[c_6404,c_5530]) ).
cnf(c_6424,plain,
multiply(inverse(inverse(multiply(inverse(A),A))),B) = inverse(multiply(C,inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_6418,c_6222]) ).
cnf(c_6434,plain,
multiply(multiply(A,multiply(B,multiply(multiply(C,multiply(inverse(C),inverse(D))),D))),inverse(B)) = A,
inference(paramod,[status(thm)],[c_6418,c_5858]) ).
cnf(c_6444,plain,
multiply(A,multiply(multiply(B,multiply(inverse(B),inverse(C))),C)) = A,
inference(paramod,[status(thm)],[c_6418,c_5529]) ).
cnf(c_8441,plain,
inverse(multiply(inverse(A),multiply(A,multiply(multiply(B,inverse(B)),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_6444,c_4728]) ).
cnf(c_6478,plain,
inverse(multiply(multiply(A,inverse(A)),inverse(B))) = B,
inference(paramod,[status(thm)],[c_6418,c_8441]) ).
cnf(c_6495,plain,
inverse(multiply(multiply(A,multiply(inverse(A),inverse(B))),multiply(B,multiply(C,inverse(multiply(multiply(inverse(inverse(D)),inverse(multiply(inverse(E),D))),C)))))) = E,
inference(paramod,[status(thm)],[c_6418,c_4231]) ).
cnf(c_6549,plain,
multiply(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),D),inverse(multiply(E,multiply(B,D)))))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(multiply(V6,multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)) = inverse(multiply(multiply(V11,multiply(inverse(V11),V10)),V7)),
inference(paramod,[status(thm)],[c_6418,c_3150]) ).
cnf(c_6575,plain,
multiply(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(multiply(V8,multiply(inverse(V8),V7)),multiply(V9,multiply(V10,multiply(multiply(inverse(V10),V11),inverse(multiply(E,multiply(V9,V11)))))))),
inference(paramod,[status(thm)],[c_6418,c_3112]) ).
cnf(c_6646,plain,
multiply(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C)))))),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))) = inverse(multiply(multiply(V7,multiply(inverse(V7),F)),V6)),
inference(paramod,[status(thm)],[c_6418,c_3004]) ).
cnf(c_6649,plain,
multiply(A,multiply(multiply(inverse(A),B),inverse(multiply(C,multiply(D,B))))) = inverse(multiply(multiply(E,multiply(inverse(E),C)),D)),
inference(paramod,[status(thm)],[c_6418,c_2999]) ).
cnf(c_6685,plain,
multiply(multiply(A,multiply(B,inverse(multiply(C,B)))),C) = A,
inference(paramod,[status(thm)],[c_6418,c_2496]) ).
cnf(c_6766,plain,
inverse(multiply(A,inverse(multiply(B,A)))) = B,
inference(paramod,[status(thm)],[c_6418,c_1418]) ).
cnf(c_6768,plain,
multiply(multiply(A,B),inverse(B)) = A,
inference(paramod,[status(thm)],[c_6444,c_6434]) ).
cnf(c_8442,plain,
multiply(A,multiply(inverse(A),inverse(multiply(multiply(B,inverse(B)),inverse(E))))) = E,
inference(paramod,[status(thm)],[c_6444,c_6405]) ).
cnf(c_6770,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_6478,c_8442]) ).
cnf(c_8443,plain,
multiply(A,C) = multiply(A,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(multiply(F,inverse(multiply(C,F)))),E))),D)))),
inference(paramod,[status(thm)],[c_6770,c_4220]) ).
cnf(c_8444,plain,
multiply(A,C) = multiply(A,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(C,E))),D)))),
inference(paramod,[status(thm)],[c_6766,c_8443]) ).
cnf(c_6947,plain,
multiply(A,multiply(B,inverse(multiply(multiply(inverse(inverse(C)),inverse(multiply(D,C))),B)))) = multiply(A,D),
inference(copy,[status(thm)],[c_8444]) ).
cnf(c_8445,plain,
inverse(multiply(inverse(B),multiply(B,multiply(C,inverse(multiply(multiply(inverse(inverse(D)),inverse(multiply(inverse(E),D))),C)))))) = E,
inference(paramod,[status(thm)],[c_6770,c_6495]) ).
cnf(c_8446,plain,
inverse(multiply(inverse(B),multiply(B,inverse(E)))) = E,
inference(paramod,[status(thm)],[c_6947,c_8445]) ).
cnf(c_6952,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_6418,c_8446]) ).
cnf(c_8447,plain,
multiply(inverse(B),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(inverse(inverse(E)),inverse(multiply(inverse(inverse(F)),E))),D))))))) = F,
inference(paramod,[status(thm)],[c_6770,c_4258]) ).
cnf(c_8448,plain,
multiply(inverse(B),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(E,inverse(multiply(inverse(inverse(F)),E))),D))))))) = F,
inference(paramod,[status(thm)],[c_6952,c_8447]) ).
cnf(c_8449,plain,
multiply(inverse(B),multiply(C,multiply(inverse(C),multiply(B,multiply(D,inverse(multiply(multiply(E,inverse(multiply(F,E))),D))))))) = F,
inference(paramod,[status(thm)],[c_6952,c_8448]) ).
cnf(c_8450,plain,
multiply(inverse(B),multiply(B,multiply(D,inverse(multiply(multiply(E,inverse(multiply(F,E))),D))))) = F,
inference(paramod,[status(thm)],[c_6770,c_8449]) ).
cnf(c_6966,plain,
multiply(A,inverse(multiply(multiply(B,inverse(multiply(C,B))),A))) = C,
inference(paramod,[status(thm)],[c_6418,c_8450]) ).
cnf(c_8451,plain,
multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(inverse(D),C))),B)))) = inverse(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),V7),inverse(multiply(V8,multiply(V9,V7))))),V8))),multiply(multiply(V9,multiply(multiply(inverse(E),D),inverse(multiply(V10,A)))),V10)))),
inference(paramod,[status(thm)],[c_6952,c_4248]) ).
cnf(c_8452,plain,
multiply(A,inverse(D)) = inverse(multiply(E,multiply(multiply(F,multiply(V6,multiply(multiply(inverse(V6),multiply(multiply(inverse(F),V7),inverse(multiply(V8,multiply(V9,V7))))),V8))),multiply(multiply(V9,multiply(multiply(inverse(E),D),inverse(multiply(V10,A)))),V10)))),
inference(paramod,[status(thm)],[c_6966,c_8451]) ).
cnf(c_6969,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),V6),inverse(multiply(V7,V8)))),V7)))) = multiply(V8,inverse(V6)),
inference(copy,[status(thm)],[c_8452]) ).
cnf(c_8453,plain,
multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(inverse(D),C))),B)))) = inverse(multiply(D,multiply(E,multiply(inverse(E),inverse(A))))),
inference(paramod,[status(thm)],[c_6952,c_4187]) ).
cnf(c_8454,plain,
multiply(A,inverse(D)) = inverse(multiply(D,multiply(E,multiply(inverse(E),inverse(A))))),
inference(paramod,[status(thm)],[c_6966,c_8453]) ).
cnf(c_8455,plain,
multiply(A,inverse(D)) = inverse(multiply(D,inverse(A))),
inference(paramod,[status(thm)],[c_6770,c_8454]) ).
cnf(c_6998,plain,
inverse(multiply(A,inverse(B))) = multiply(B,inverse(A)),
inference(copy,[status(thm)],[c_8455]) ).
cnf(c_8456,plain,
multiply(A,multiply(B,inverse(multiply(multiply(C,inverse(multiply(inverse(D),C))),B)))) = inverse(inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(A,inverse(multiply(V6,multiply(V7,D))))),V6)),V7))))),
inference(paramod,[status(thm)],[c_6952,c_4148]) ).
cnf(c_8457,plain,
multiply(A,inverse(D)) = inverse(inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(A,inverse(multiply(V6,multiply(V7,D))))),V6)),V7))))),
inference(paramod,[status(thm)],[c_6966,c_8456]) ).
cnf(c_8458,plain,
multiply(A,inverse(D)) = multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(A,inverse(multiply(V6,multiply(V7,D))))),V6)),V7))),
inference(paramod,[status(thm)],[c_6952,c_8457]) ).
cnf(c_7017,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),multiply(multiply(inverse(A),multiply(C,inverse(multiply(D,multiply(E,F))))),D)),E))) = multiply(C,inverse(F)),
inference(copy,[status(thm)],[c_8458]) ).
cnf(c_8459,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(D)))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(multiply(D,multiply(V6,inverse(multiply(multiply(V7,inverse(multiply(inverse(multiply(A,C)),V7))),V6)))),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10)))),
inference(paramod,[status(thm)],[c_6952,c_4138]) ).
cnf(c_8460,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(D)))) = inverse(multiply(E,multiply(F,multiply(multiply(inverse(F),multiply(multiply(inverse(E),multiply(multiply(multiply(D,inverse(multiply(A,C))),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)),V10)))),
inference(paramod,[status(thm)],[c_6966,c_8459]) ).
cnf(c_8461,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(D)))) = inverse(multiply(multiply(multiply(D,inverse(multiply(A,C))),V8),inverse(V8))),
inference(paramod,[status(thm)],[c_7017,c_8460]) ).
cnf(c_8462,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(D)))) = inverse(multiply(D,inverse(multiply(A,C)))),
inference(paramod,[status(thm)],[c_6768,c_8461]) ).
cnf(c_7021,plain,
multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(D)))) = multiply(multiply(A,C),inverse(D)),
inference(paramod,[status(thm)],[c_6998,c_8462]) ).
cnf(c_8463,plain,
inverse(multiply(A,multiply(multiply(B,multiply(C,multiply(multiply(inverse(C),multiply(multiply(inverse(B),D),inverse(multiply(E,multiply(F,D))))),E))),multiply(multiply(F,multiply(multiply(inverse(A),multiply(V6,V7)),inverse(multiply(V10,V7)))),V10)))) = inverse(V6),
inference(paramod,[status(thm)],[c_6685,c_3607]) ).
cnf(c_7280,plain,
multiply(A,inverse(multiply(B,A))) = inverse(B),
inference(paramod,[status(thm)],[c_6969,c_8463]) ).
cnf(c_8464,plain,
multiply(multiply(inverse(A),A),B) = inverse(multiply(C,inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_6952,c_6424]) ).
cnf(c_8465,plain,
multiply(multiply(inverse(A),A),B) = inverse(inverse(B)),
inference(paramod,[status(thm)],[c_7280,c_8464]) ).
cnf(c_7346,plain,
multiply(multiply(inverse(A),A),B) = B,
inference(paramod,[status(thm)],[c_6952,c_8465]) ).
cnf(c_7349,plain,
multiply(A,multiply(multiply(inverse(A),B),inverse(multiply(C,multiply(D,B))))) = inverse(multiply(C,D)),
inference(paramod,[status(thm)],[c_6770,c_6649]) ).
cnf(c_8466,plain,
multiply(multiply(A,inverse(multiply(D,A))),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))) = inverse(multiply(multiply(V7,multiply(inverse(V7),F)),V6)),
inference(paramod,[status(thm)],[c_7349,c_6646]) ).
cnf(c_8467,plain,
multiply(inverse(D),multiply(multiply(D,E),inverse(multiply(F,multiply(V6,E))))) = inverse(multiply(multiply(V7,multiply(inverse(V7),F)),V6)),
inference(paramod,[status(thm)],[c_7280,c_8466]) ).
cnf(c_7351,plain,
multiply(inverse(A),multiply(multiply(A,B),inverse(multiply(C,multiply(D,B))))) = inverse(multiply(C,D)),
inference(paramod,[status(thm)],[c_6770,c_8467]) ).
cnf(c_8468,plain,
multiply(multiply(A,inverse(multiply(D,A))),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(multiply(V8,multiply(inverse(V8),V7)),multiply(V9,multiply(V10,multiply(multiply(inverse(V10),V11),inverse(multiply(E,multiply(V9,V11)))))))),
inference(paramod,[status(thm)],[c_7349,c_6575]) ).
cnf(c_8469,plain,
multiply(inverse(D),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(multiply(V8,multiply(inverse(V8),V7)),multiply(V9,multiply(V10,multiply(multiply(inverse(V10),V11),inverse(multiply(E,multiply(V9,V11)))))))),
inference(paramod,[status(thm)],[c_7280,c_8468]) ).
cnf(c_8470,plain,
multiply(inverse(D),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(V7,multiply(V9,multiply(V10,multiply(multiply(inverse(V10),V11),inverse(multiply(E,multiply(V9,V11)))))))),
inference(paramod,[status(thm)],[c_6770,c_8469]) ).
cnf(c_8471,plain,
multiply(inverse(D),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(V7,multiply(V9,inverse(multiply(E,V9))))),
inference(paramod,[status(thm)],[c_7349,c_8470]) ).
cnf(c_8472,plain,
multiply(inverse(D),multiply(multiply(D,multiply(multiply(E,F),inverse(multiply(V6,multiply(V7,F))))),V6)) = inverse(multiply(V7,inverse(E))),
inference(paramod,[status(thm)],[c_7280,c_8471]) ).
cnf(c_7381,plain,
multiply(inverse(A),multiply(multiply(A,multiply(multiply(B,C),inverse(multiply(D,multiply(E,C))))),D)) = multiply(B,inverse(E)),
inference(paramod,[status(thm)],[c_6998,c_8472]) ).
cnf(c_8473,plain,
multiply(multiply(A,multiply(multiply(B,inverse(multiply(E,B))),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(multiply(V6,multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)) = inverse(multiply(multiply(V11,multiply(inverse(V11),V10)),V7)),
inference(paramod,[status(thm)],[c_7349,c_6549]) ).
cnf(c_8474,plain,
multiply(multiply(A,multiply(inverse(E),multiply(multiply(E,F),inverse(multiply(V6,multiply(A,F)))))),multiply(multiply(V6,multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)) = inverse(multiply(multiply(V11,multiply(inverse(V11),V10)),V7)),
inference(paramod,[status(thm)],[c_7280,c_8473]) ).
cnf(c_8475,plain,
multiply(multiply(A,inverse(multiply(V6,A))),multiply(multiply(V6,multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)) = inverse(multiply(multiply(V11,multiply(inverse(V11),V10)),V7)),
inference(paramod,[status(thm)],[c_7351,c_8474]) ).
cnf(c_8476,plain,
multiply(inverse(V6),multiply(multiply(V6,multiply(multiply(inverse(V7),V8),inverse(multiply(V9,multiply(V10,V8))))),V9)) = inverse(multiply(multiply(V11,multiply(inverse(V11),V10)),V7)),
inference(paramod,[status(thm)],[c_7280,c_8475]) ).
cnf(c_8477,plain,
multiply(inverse(V7),inverse(V10)) = inverse(multiply(multiply(V11,multiply(inverse(V11),V10)),V7)),
inference(paramod,[status(thm)],[c_7381,c_8476]) ).
cnf(c_8478,plain,
multiply(inverse(V7),inverse(V10)) = inverse(multiply(V10,V7)),
inference(paramod,[status(thm)],[c_6770,c_8477]) ).
cnf(c_7387,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_8478]) ).
cnf(c_8479,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(paramod,[status(thm)],[c_7346,c_6401]) ).
cnf(c_8028,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(copy,[status(thm)],[c_8479]) ).
cnf(c_8480,plain,
multiply(A,B) = multiply(multiply(A,C),inverse(multiply(inverse(B),C))),
inference(paramod,[status(thm)],[c_6350,c_7021]) ).
cnf(c_8481,plain,
multiply(A,B) = multiply(multiply(A,C),multiply(inverse(C),inverse(inverse(B)))),
inference(paramod,[status(thm)],[c_7387,c_8480]) ).
cnf(c_8482,plain,
multiply(A,B) = multiply(multiply(A,C),multiply(inverse(C),B)),
inference(paramod,[status(thm)],[c_6952,c_8481]) ).
cnf(c_8116,plain,
multiply(multiply(A,B),multiply(inverse(B),C)) = multiply(A,C),
inference(copy,[status(thm)],[c_8482]) ).
cnf(c_8419,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_6418,c_8116]) ).
cnf(c_8420,plain,
$false,
inference(resolve,[status(thm)],[c_8419,c_8028]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP061-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.42 % Computer : n014.cluster.edu
% 0.18/0.42 % Model : x86_64 x86_64
% 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42 % Memory : 8046.5625MB
% 0.18/0.42 % OS : Linux 6.8.0-71-generic
% 0.18/0.42 % CPULimit : 300
% 0.18/0.42 % WCLimit : 300
% 0.18/0.42 % DateTime : Fri Sep 25 14:20:17 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.43 % Process 411381 was started by sandbox on n014,
% 0.18/0.43 % Fri Sep 25 14:20:17 2026
% 0.18/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.44
% 0.18/0.44 % From the command line: assign(max_seconds, 300).
% 28.77/4.63
% 28.77/4.63 % Assigning unary symbol inverse kb_weight 0 and highest precedence (10).
% 28.77/4.63
% 28.77/4.63 % SZS status Unsatisfiable for theBenchmark
% 28.77/4.63
% 28.77/4.63 % Proof 1 at 3.70 (+ 0.36) seconds.
% 28.77/4.63 % Length of proof is 89.
% 28.77/4.63 % Level of proof is 30.
% 28.77/4.63 % Maximum clause weight is 59.000.
% 28.77/4.63 % Given clauses 64.
% 28.77/4.63
% 28.77/4.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------