%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP506-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:30:04 AM UTC 2026
% Result : Unsatisfiable 39.62s 10.68s
% Output : CNFRefutation 39.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 2
% Syntax : Number of formulae : 138 ( 138 unt; 0 def)
% Number of atoms : 138 ( 137 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 1 avg)
% Maximal term depth : 23 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 739 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(single_axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(VAR_0,VAR_1)),multiply(VAR_1,VAR_0))),multiply(inverse(multiply(VAR_2,VAR_3)),multiply(VAR_2,inverse(multiply(multiply(VAR_4,inverse(VAR_5)),inverse(VAR_3))))))),VAR_5) = VAR_4,
file('theBenchmark.p',single_axiom) ).
cnf(c_1,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(F)),inverse(D))))))),F) = E,
inference(clausify,[status(thm)],[single_axiom]) ).
fof(prove_these_axioms_2,axiom,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('theBenchmark.p',prove_these_axioms_2) ).
cnf(c_2,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(clausify,[status(thm)],[prove_these_axioms_2]) ).
cnf(c_14125,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F) = inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(V9))))))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_6,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9))))))),F),
inference(copy,[status(thm)],[c_14125]) ).
cnf(c_8,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F),inverse(F)) = E,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_9,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,inverse(F)),inverse(inverse(F))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_14126,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(E))))),D) = inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(multiply(V7,V8)),multiply(V7,inverse(multiply(E,inverse(V8))))))),
inference(paramod,[status(thm)],[c_8,c_1]) ).
cnf(c_14,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(multiply(V7,inverse(V8))),multiply(V7,inverse(E))))),V8),
inference(copy,[status(thm)],[c_14126]) ).
cnf(c_14127,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(E))))),F),inverse(F)) = inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(E,inverse(inverse(D))),inverse(V9))))))),
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_19,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,F)),multiply(V8,inverse(E))))),V9),inverse(V9)),
inference(copy,[status(thm)],[c_14127]) ).
cnf(c_14128,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,inverse(C)),inverse(inverse(C))),
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_33,plain,
multiply(multiply(A,inverse(B)),inverse(inverse(B))) = multiply(multiply(A,C),inverse(C)),
inference(copy,[status(thm)],[c_14128]) ).
cnf(c_14129,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(multiply(multiply(F,inverse(V10)),inverse(inverse(V10))),inverse(V9))))))))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_9,c_9]) ).
cnf(c_35,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_9,c_14129]) ).
cnf(c_39,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(multiply(multiply(E,F),inverse(F))))))),D) = E,
inference(paramod,[status(thm)],[c_33,c_1]) ).
cnf(c_60,plain,
multiply(multiply(A,B),inverse(B)) = multiply(multiply(A,C),inverse(C)),
inference(paramod,[status(thm)],[c_33,c_33]) ).
cnf(c_70,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,F),inverse(F))))))),V6),inverse(V6)) = multiply(E,D),
inference(paramod,[status(thm)],[c_60,c_8]) ).
cnf(c_74,plain,
multiply(multiply(multiply(A,B),inverse(B)),inverse(inverse(C))) = multiply(multiply(multiply(A,C),D),inverse(D)),
inference(paramod,[status(thm)],[c_60,c_60]) ).
cnf(c_94,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(inverse(V6)))))))),V7),inverse(V7)) = multiply(multiply(E,V6),D),
inference(paramod,[status(thm)],[c_74,c_8]) ).
cnf(c_121,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(C,D),inverse(D))),multiply(multiply(C,E),inverse(multiply(multiply(F,V6),inverse(V6))))))),E) = F,
inference(paramod,[status(thm)],[c_60,c_39]) ).
cnf(c_14130,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(multiply(E,F)),multiply(E,inverse(multiply(V6,inverse(F))))))),V7),inverse(V7))),V6))),multiply(multiply(V8,V9),inverse(V9))) = V8,
inference(paramod,[status(thm)],[c_8,c_121]) ).
cnf(c_378,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),multiply(multiply(D,E),inverse(E))) = D,
inference(paramod,[status(thm)],[c_8,c_14130]) ).
cnf(c_14131,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(C))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F))),C),V6),inverse(V6)),
inference(paramod,[status(thm)],[c_378,c_74]) ).
cnf(c_414,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(inverse(D))),
inference(copy,[status(thm)],[c_14131]) ).
cnf(c_461,plain,
multiply(A,inverse(multiply(multiply(A,B),inverse(B)))) = multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),
inference(paramod,[status(thm)],[c_378,c_70]) ).
cnf(c_486,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(E,inverse(multiply(multiply(E,F),inverse(F))))))),D) = C,
inference(paramod,[status(thm)],[c_461,c_1]) ).
cnf(c_14132,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(multiply(E,F)),multiply(E,inverse(multiply(V6,inverse(F))))))),V7),inverse(V7))))) = V6,
inference(paramod,[status(thm)],[c_461,c_8]) ).
cnf(c_500,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(C))) = C,
inference(paramod,[status(thm)],[c_8,c_14132]) ).
cnf(c_546,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = D,
inference(paramod,[status(thm)],[c_500,c_414]) ).
cnf(c_14133,plain,
multiply(A,inverse(inverse(inverse(A)))) = multiply(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D),inverse(D)),
inference(paramod,[status(thm)],[c_500,c_60]) ).
cnf(c_561,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C),inverse(C)) = multiply(D,inverse(inverse(inverse(D)))),
inference(copy,[status(thm)],[c_14133]) ).
cnf(c_597,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),multiply(multiply(D,inverse(multiply(multiply(D,E),inverse(E)))),inverse(multiply(multiply(F,V6),inverse(V6))))))),V7),inverse(V7)) = multiply(F,inverse(inverse(C))),
inference(paramod,[status(thm)],[c_500,c_70]) ).
cnf(c_614,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(multiply(C,inverse(inverse(inverse(C)))))) = multiply(D,inverse(multiply(multiply(D,E),inverse(E)))),
inference(paramod,[status(thm)],[c_500,c_461]) ).
cnf(c_615,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(multiply(C,inverse(inverse(inverse(C)))))),inverse(inverse(D))) = D,
inference(paramod,[status(thm)],[c_500,c_500]) ).
cnf(c_696,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(inverse(V6),V6))),D),
inference(paramod,[status(thm)],[c_546,c_378]) ).
cnf(c_14134,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E)))))),F),inverse(F)) = multiply(V6,inverse(inverse(inverse(V6)))),
inference(paramod,[status(thm)],[c_378,c_561]) ).
cnf(c_799,plain,
inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))) = multiply(C,inverse(inverse(inverse(C)))),
inference(paramod,[status(thm)],[c_546,c_14134]) ).
cnf(c_14135,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C),inverse(C)) = inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))),
inference(paramod,[status(thm)],[c_561,c_500]) ).
cnf(c_804,plain,
inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))) = multiply(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),E),inverse(E)),
inference(copy,[status(thm)],[c_14135]) ).
cnf(c_843,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),inverse(inverse(inverse(inverse(C))))) = multiply(multiply(C,D),inverse(D)),
inference(paramod,[status(thm)],[c_799,c_60]) ).
cnf(c_14136,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(inverse(inverse(inverse(inverse(E))))))))))),V6),inverse(V6)) = multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),D),
inference(paramod,[status(thm)],[c_843,c_70]) ).
cnf(c_14137,plain,
multiply(multiply(E,inverse(inverse(inverse(E)))),D) = multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),D),
inference(paramod,[status(thm)],[c_94,c_14136]) ).
cnf(c_1313,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),C) = multiply(multiply(D,inverse(inverse(inverse(D)))),C),
inference(copy,[status(thm)],[c_14137]) ).
cnf(c_1401,plain,
multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),F),inverse(multiply(E,inverse(inverse(F)))))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
inference(paramod,[status(thm)],[c_8,c_1313]) ).
cnf(c_1469,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),C) = multiply(inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))),C),
inference(paramod,[status(thm)],[c_500,c_1313]) ).
cnf(c_14138,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(multiply(V7,V8)),multiply(V7,inverse(multiply(E,inverse(V8))))))),V9),inverse(V9)))))),inverse(D)))))))),V10) = multiply(inverse(multiply(V11,inverse(multiply(multiply(V11,V12),inverse(V12))))),V10),
inference(paramod,[status(thm)],[c_6,c_1469]) ).
cnf(c_1513,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(inverse(E)))),inverse(D)))))))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
inference(paramod,[status(thm)],[c_8,c_14138]) ).
cnf(c_2044,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),multiply(C,inverse(E))))),D),F),inverse(F)) = E,
inference(paramod,[status(thm)],[c_14,c_8]) ).
cnf(c_2179,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))))),multiply(E,inverse(multiply(multiply(E,F),inverse(F))))))),inverse(inverse(V6))) = V6,
inference(paramod,[status(thm)],[c_799,c_486]) ).
cnf(c_14139,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D))))),multiply(multiply(E,inverse(multiply(multiply(E,F),inverse(F)))),inverse(multiply(multiply(V6,V7),inverse(V7))))))),V8),inverse(V8)) = multiply(V6,inverse(multiply(V9,inverse(inverse(inverse(V9)))))),
inference(paramod,[status(thm)],[c_614,c_70]) ).
cnf(c_3404,plain,
multiply(A,inverse(inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C))))))) = multiply(A,inverse(multiply(D,inverse(inverse(inverse(D)))))),
inference(paramod,[status(thm)],[c_597,c_14139]) ).
cnf(c_3524,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))))),inverse(D))))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
inference(paramod,[status(thm)],[c_3404,c_1]) ).
cnf(c_14140,plain,
multiply(A,inverse(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(multiply(F,inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(F,inverse(V9))))))),V10),inverse(V10)))))),inverse(E)))))))))) = multiply(A,inverse(multiply(V11,inverse(inverse(inverse(V11)))))),
inference(paramod,[status(thm)],[c_6,c_3404]) ).
cnf(c_3533,plain,
multiply(A,inverse(inverse(inverse(multiply(inverse(multiply(inverse(multiply(B,C)),multiply(C,B))),multiply(inverse(multiply(D,E)),multiply(D,inverse(multiply(multiply(F,inverse(inverse(inverse(F)))),inverse(E)))))))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
inference(paramod,[status(thm)],[c_8,c_14140]) ).
cnf(c_3538,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),inverse(multiply(F,inverse(inverse(inverse(F)))))),inverse(inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))))) = E,
inference(paramod,[status(thm)],[c_3404,c_8]) ).
cnf(c_3539,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
inference(paramod,[status(thm)],[c_3404,c_8]) ).
cnf(c_3590,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,multiply(F,inverse(inverse(inverse(F))))),inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_3404,c_35]) ).
cnf(c_3691,plain,
multiply(A,inverse(inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C))))))) = multiply(A,inverse(inverse(multiply(D,inverse(multiply(multiply(D,E),inverse(E))))))),
inference(paramod,[status(thm)],[c_500,c_3404]) ).
cnf(c_14141,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),inverse(multiply(D,inverse(inverse(inverse(D)))))),E),inverse(E)) = inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),
inference(paramod,[status(thm)],[c_3404,c_546]) ).
cnf(c_14142,plain,
inverse(multiply(D,inverse(inverse(inverse(D))))) = inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),
inference(paramod,[status(thm)],[c_546,c_14141]) ).
cnf(c_3695,plain,
inverse(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))))) = inverse(multiply(C,inverse(inverse(inverse(C))))),
inference(copy,[status(thm)],[c_14142]) ).
cnf(c_3939,plain,
inverse(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))))) = inverse(inverse(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))))),
inference(paramod,[status(thm)],[c_500,c_3695]) ).
cnf(c_4223,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_3939,c_35]) ).
cnf(c_4350,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6))))))),inverse(inverse(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))))))),inverse(D))))))) = E,
inference(paramod,[status(thm)],[c_3691,c_35]) ).
cnf(c_14143,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(E,F)),multiply(F,E))),multiply(inverse(V6),V6))),inverse(V7)),inverse(D))))))),V7) = inverse(multiply(inverse(multiply(inverse(multiply(V8,V9)),multiply(V9,V8))),multiply(inverse(V10),V10))),
inference(paramod,[status(thm)],[c_696,c_1]) ).
cnf(c_8143,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))) = inverse(multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F))),
inference(paramod,[status(thm)],[c_1,c_14143]) ).
cnf(c_14144,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E))))) = multiply(inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F))),multiply(inverse(V7),V7)),
inference(paramod,[status(thm)],[c_8143,c_500]) ).
cnf(c_8389,plain,
multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C)) = multiply(inverse(multiply(inverse(multiply(D,E)),multiply(E,D))),multiply(inverse(F),F)),
inference(paramod,[status(thm)],[c_500,c_14144]) ).
cnf(c_8597,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E)))),F),V6),inverse(V6)) = F,
inference(paramod,[status(thm)],[c_8389,c_546]) ).
cnf(c_9174,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),inverse(E))),F))),E),V6),inverse(V6)) = inverse(F),
inference(paramod,[status(thm)],[c_500,c_2044]) ).
cnf(c_9202,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,inverse(D))),inverse(multiply(E,inverse(multiply(multiply(E,F),inverse(F)))))))),D),V6),inverse(V6)) = inverse(inverse(C)),
inference(paramod,[status(thm)],[c_799,c_2044]) ).
cnf(c_14145,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(multiply(multiply(C,inverse(multiply(multiply(C,D),inverse(D)))),E),inverse(F))),inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))))),F),V8),inverse(V8)) = E,
inference(paramod,[status(thm)],[c_804,c_2044]) ).
cnf(c_9223,plain,
inverse(inverse(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),C))) = C,
inference(paramod,[status(thm)],[c_9202,c_14145]) ).
cnf(c_9486,plain,
multiply(multiply(A,inverse(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),D))),D) = multiply(multiply(A,E),inverse(E)),
inference(paramod,[status(thm)],[c_9223,c_60]) ).
cnf(c_14146,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(E,F),inverse(F)),inverse(D))))))),V6) = multiply(E,inverse(multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(V6)))),
inference(paramod,[status(thm)],[c_9486,c_1]) ).
cnf(c_14147,plain,
multiply(E,V6) = multiply(E,inverse(multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(V6)))),
inference(paramod,[status(thm)],[c_35,c_14146]) ).
cnf(c_10159,plain,
multiply(A,inverse(multiply(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))),inverse(D)))) = multiply(A,D),
inference(copy,[status(thm)],[c_14147]) ).
cnf(c_14148,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(C),C))),D),E),inverse(E)) = inverse(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(D))),
inference(paramod,[status(thm)],[c_10159,c_546]) ).
cnf(c_14149,plain,
D = inverse(multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(D))),
inference(paramod,[status(thm)],[c_546,c_14148]) ).
cnf(c_10700,plain,
inverse(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(C))) = C,
inference(copy,[status(thm)],[c_14149]) ).
cnf(c_10870,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(C,D))),C),E),inverse(E)) = inverse(D),
inference(paramod,[status(thm)],[c_10700,c_9174]) ).
cnf(c_14150,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(inverse(multiply(C,D)),multiply(D,C))),multiply(inverse(E),E)))),inverse(multiply(inverse(multiply(F,V6)),multiply(V6,F)))),V7),inverse(V7)) = inverse(multiply(inverse(V8),V8)),
inference(paramod,[status(thm)],[c_8389,c_10870]) ).
cnf(c_11897,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(B,A))) = inverse(multiply(inverse(C),C)),
inference(paramod,[status(thm)],[c_8597,c_14150]) ).
cnf(c_11980,plain,
multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(inverse(multiply(E,F)),multiply(F,E))))))),V6),inverse(V6)) = inverse(inverse(D)),
inference(paramod,[status(thm)],[c_11897,c_8]) ).
cnf(c_12118,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),C),D),inverse(D)) = C,
inference(paramod,[status(thm)],[c_11897,c_546]) ).
cnf(c_12440,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(multiply(multiply(inverse(multiply(C,D)),multiply(D,C)),inverse(inverse(inverse(multiply(inverse(E),E))))))),inverse(inverse(F))) = F,
inference(paramod,[status(thm)],[c_11897,c_615]) ).
cnf(c_14151,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(inverse(E),E),inverse(inverse(F))),inverse(D))))))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,F)),multiply(V8,inverse(multiply(inverse(multiply(V9,V10)),multiply(V10,V9))))))),V11),inverse(V11)),
inference(paramod,[status(thm)],[c_11897,c_19]) ).
cnf(c_12490,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(multiply(inverse(E),E),inverse(inverse(F))),inverse(D))))))) = inverse(inverse(F)),
inference(paramod,[status(thm)],[c_11980,c_14151]) ).
cnf(c_14152,plain,
multiply(multiply(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),inverse(multiply(C,D))),E),inverse(E)) = inverse(multiply(D,C)),
inference(paramod,[status(thm)],[c_11897,c_10870]) ).
cnf(c_12628,plain,
inverse(multiply(A,B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_12118,c_14152]) ).
cnf(c_14153,plain,
multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(C,D)))) = multiply(D,C),
inference(paramod,[status(thm)],[c_12628,c_500]) ).
cnf(c_12800,plain,
multiply(A,B) = multiply(B,A),
inference(paramod,[status(thm)],[c_500,c_14153]) ).
cnf(c_13162,plain,
inverse(multiply(inverse(A),multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))) = A,
inference(paramod,[status(thm)],[c_12628,c_10700]) ).
cnf(c_13347,plain,
multiply(multiply(b2,inverse(b2)),a2) != a2,
inference(paramod,[status(thm)],[c_12800,c_2]) ).
cnf(c_13361,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(inverse(F))),inverse(D))))))) = multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9)))))))),
inference(paramod,[status(thm)],[c_12800,c_6]) ).
cnf(c_13435,plain,
multiply(inverse(inverse(A)),multiply(B,inverse(multiply(multiply(B,C),inverse(C))))) = A,
inference(paramod,[status(thm)],[c_12800,c_500]) ).
cnf(c_14154,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(C,inverse(multiply(multiply(C,D),inverse(D)))))),inverse(inverse(V6))) = V6,
inference(paramod,[status(thm)],[c_13435,c_2179]) ).
cnf(c_13700,plain,
multiply(multiply(inverse(multiply(A,B)),multiply(B,A)),inverse(inverse(C))) = C,
inference(paramod,[status(thm)],[c_13162,c_14154]) ).
cnf(c_14155,plain,
multiply(multiply(multiply(A,inverse(multiply(multiply(A,B),inverse(B)))),inverse(inverse(multiply(inverse(E),E)))),inverse(inverse(F))) = F,
inference(paramod,[status(thm)],[c_13700,c_12440]) ).
cnf(c_13707,plain,
multiply(multiply(inverse(A),A),inverse(inverse(B))) = B,
inference(paramod,[status(thm)],[c_500,c_14155]) ).
cnf(c_13727,plain,
inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))) = inverse(inverse(E)),
inference(paramod,[status(thm)],[c_13707,c_12490]) ).
cnf(c_14156,plain,
inverse(inverse(multiply(E,inverse(inverse(F))))) = multiply(F,inverse(multiply(inverse(multiply(inverse(multiply(V6,V7)),multiply(V7,V6))),multiply(inverse(multiply(V8,V9)),multiply(V8,inverse(multiply(E,inverse(V9)))))))),
inference(paramod,[status(thm)],[c_13727,c_13361]) ).
cnf(c_13784,plain,
inverse(inverse(multiply(A,inverse(inverse(B))))) = multiply(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_13727,c_14156]) ).
cnf(c_14157,plain,
inverse(inverse(multiply(multiply(E,inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6))))))),inverse(inverse(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))))))))) = E,
inference(paramod,[status(thm)],[c_13727,c_4350]) ).
cnf(c_14158,plain,
multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),inverse(inverse(multiply(E,inverse(inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))))))) = E,
inference(paramod,[status(thm)],[c_13784,c_14157]) ).
cnf(c_14159,plain,
multiply(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))),multiply(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))),inverse(inverse(E)))) = E,
inference(paramod,[status(thm)],[c_13784,c_14158]) ).
cnf(c_14057,plain,
multiply(inverse(multiply(A,inverse(multiply(multiply(A,B),inverse(B))))),C) = C,
inference(paramod,[status(thm)],[c_500,c_14159]) ).
cnf(c_14160,plain,
inverse(inverse(multiply(multiply(E,inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(inverse(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8))))))))) = E,
inference(paramod,[status(thm)],[c_13727,c_4223]) ).
cnf(c_14161,plain,
multiply(multiply(V7,inverse(multiply(multiply(V7,V8),inverse(V8)))),inverse(inverse(multiply(E,inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6))))))))) = E,
inference(paramod,[status(thm)],[c_13784,c_14160]) ).
cnf(c_14063,plain,
multiply(A,inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))) = A,
inference(paramod,[status(thm)],[c_500,c_14161]) ).
cnf(c_14162,plain,
inverse(inverse(multiply(multiply(E,multiply(F,inverse(inverse(inverse(F))))),inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))))))) = E,
inference(paramod,[status(thm)],[c_13727,c_3590]) ).
cnf(c_14163,plain,
multiply(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))),inverse(inverse(multiply(E,multiply(F,inverse(inverse(inverse(F)))))))) = E,
inference(paramod,[status(thm)],[c_13784,c_14162]) ).
cnf(c_14076,plain,
multiply(A,multiply(B,inverse(inverse(inverse(B))))) = A,
inference(paramod,[status(thm)],[c_500,c_14163]) ).
cnf(c_14164,plain,
multiply(multiply(inverse(inverse(E)),inverse(multiply(F,inverse(multiply(multiply(F,V6),inverse(V6)))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
inference(paramod,[status(thm)],[c_13727,c_3539]) ).
cnf(c_14081,plain,
multiply(inverse(inverse(A)),inverse(multiply(B,inverse(inverse(inverse(B)))))) = A,
inference(paramod,[status(thm)],[c_14063,c_14164]) ).
cnf(c_14165,plain,
multiply(multiply(inverse(inverse(E)),inverse(multiply(F,inverse(inverse(inverse(F)))))),inverse(inverse(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7)))))))) = E,
inference(paramod,[status(thm)],[c_13727,c_3538]) ).
cnf(c_14082,plain,
multiply(A,inverse(inverse(inverse(multiply(B,inverse(multiply(multiply(B,C),inverse(C)))))))) = A,
inference(paramod,[status(thm)],[c_14081,c_14165]) ).
cnf(c_14166,plain,
multiply(A,inverse(inverse(inverse(inverse(multiply(F,inverse(inverse(inverse(F))))))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
inference(paramod,[status(thm)],[c_13727,c_3533]) ).
cnf(c_14167,plain,
multiply(A,inverse(inverse(multiply(inverse(F),inverse(inverse(F)))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
inference(paramod,[status(thm)],[c_13784,c_14166]) ).
cnf(c_14168,plain,
multiply(A,multiply(F,inverse(inverse(inverse(F))))) = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
inference(paramod,[status(thm)],[c_13784,c_14167]) ).
cnf(c_14169,plain,
A = multiply(A,inverse(multiply(V6,inverse(inverse(inverse(V6)))))),
inference(paramod,[status(thm)],[c_14076,c_14168]) ).
cnf(c_14083,plain,
multiply(A,inverse(multiply(B,inverse(inverse(inverse(B)))))) = A,
inference(copy,[status(thm)],[c_14169]) ).
cnf(c_14170,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(E,inverse(D))))))),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
inference(paramod,[status(thm)],[c_14082,c_3524]) ).
cnf(c_14171,plain,
multiply(inverse(inverse(E)),inverse(multiply(V7,inverse(inverse(inverse(V7)))))) = E,
inference(paramod,[status(thm)],[c_13727,c_14170]) ).
cnf(c_14085,plain,
inverse(inverse(A)) = A,
inference(paramod,[status(thm)],[c_14083,c_14171]) ).
cnf(c_14172,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(A,B)),multiply(B,A))),multiply(inverse(multiply(C,D)),multiply(C,inverse(multiply(multiply(E,inverse(E)),inverse(D)))))))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
inference(paramod,[status(thm)],[c_14085,c_1513]) ).
cnf(c_14173,plain,
multiply(inverse(inverse(inverse(multiply(E,inverse(E))))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
inference(paramod,[status(thm)],[c_13727,c_14172]) ).
cnf(c_14174,plain,
multiply(inverse(multiply(E,inverse(E))),F) = multiply(inverse(multiply(V6,inverse(multiply(multiply(V6,V7),inverse(V7))))),F),
inference(paramod,[status(thm)],[c_14085,c_14173]) ).
cnf(c_14122,plain,
multiply(inverse(multiply(A,inverse(A))),B) = B,
inference(paramod,[status(thm)],[c_14057,c_14174]) ).
cnf(c_14175,plain,
multiply(inverse(multiply(multiply(inverse(inverse(E)),F),inverse(multiply(E,inverse(inverse(F)))))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
inference(paramod,[status(thm)],[c_13727,c_1401]) ).
cnf(c_14176,plain,
multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,inverse(inverse(F)))))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
inference(paramod,[status(thm)],[c_14085,c_14175]) ).
cnf(c_14177,plain,
multiply(inverse(multiply(multiply(E,F),inverse(multiply(E,F)))),V6) = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
inference(paramod,[status(thm)],[c_14085,c_14176]) ).
cnf(c_14178,plain,
V6 = multiply(multiply(V7,inverse(inverse(inverse(V7)))),V6),
inference(paramod,[status(thm)],[c_14122,c_14177]) ).
cnf(c_14179,plain,
V6 = multiply(multiply(V7,inverse(V7)),V6),
inference(paramod,[status(thm)],[c_14085,c_14178]) ).
cnf(c_14123,plain,
multiply(multiply(A,inverse(A)),B) = B,
inference(copy,[status(thm)],[c_14179]) ).
cnf(c_14124,plain,
$false,
inference(resolve,[status(thm)],[c_14123,c_13347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP506-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.58 % Computer : n008.cluster.edu
% 0.09/5.58 % Model : x86_64 x86_64
% 0.09/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.58 % Memory : 8046.5625MB
% 0.09/5.58 % OS : Linux 6.8.0-71-generic
% 0.09/5.58 % CPULimit : 300
% 0.09/5.58 % WCLimit : 300
% 0.09/5.58 % DateTime : Fri Sep 25 14:57:45 UTC 2026
% 0.09/5.58 % CPUTime :
% 0.09/5.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.58 % Process 1340685 was started by sandbox on n008,
% 0.09/5.58 % Fri Sep 25 14:57:45 2026
% 0.09/5.58 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/5.58
% 0.09/5.58 % From the command line: assign(max_seconds, 300).
% 39.62/10.68
% 39.62/10.68 % SZS status Unsatisfiable for theBenchmark
% 39.62/10.68
% 39.62/10.68 % Proof 1 at 4.36 (+ 0.57) seconds.
% 39.62/10.68 % Length of proof is 81.
% 39.62/10.68 % Level of proof is 32.
% 39.62/10.68 % Maximum clause weight is 100.000.
% 39.62/10.68 % Given clauses 109.
% 39.62/10.68
% 39.62/10.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------