%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP130-3.003 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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:28:03 AM UTC 2026
% Result : Unsatisfiable 0.19s 0.54s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 27
% Syntax : Number of formulae : 173 ( 40 unt; 0 def)
% Number of atoms : 513 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 535 ( 195 ~; 340 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 123 ( 0 sgn 35 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2),
file('theBenchmark.p',e_1_is_not_e_2) ).
cnf(c_1,plain,
~ equalish(e_1,e_2),
inference(clausify,[status(thm)],[e_1_is_not_e_2]) ).
fof(cycle7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_2,VAR_3)
| ~ next(VAR_0,VAR_3)
| ~ greater(VAR_1,e_0)
| ~ product(VAR_0,e_1,VAR_2)
| ~ cycle(VAR_0,VAR_1) ),
file('theBenchmark.p',cycle7) ).
cnf(c_2,plain,
( equalish(C,D)
| ~ next(A,D)
| ~ greater(B,e_0)
| ~ product(A,e_1,C)
| ~ cycle(A,B) ),
inference(clausify,[status(thm)],[cycle7]) ).
fof(cycle4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( equalish(VAR_1,VAR_4)
| ~ next(VAR_3,VAR_4)
| ~ greater(VAR_1,e_0)
| ~ next(VAR_0,VAR_2)
| ~ cycle(VAR_2,VAR_3)
| ~ cycle(VAR_0,VAR_1) ),
file('theBenchmark.p',cycle4) ).
cnf(c_3,plain,
( equalish(B,E)
| ~ next(D,E)
| ~ greater(B,e_0)
| ~ next(A,C)
| ~ cycle(C,D)
| ~ cycle(A,B) ),
inference(clausify,[status(thm)],[cycle4]) ).
fof(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3),
file('theBenchmark.p',e_1_is_not_e_3) ).
cnf(c_5,plain,
~ equalish(e_1,e_3),
inference(clausify,[status(thm)],[e_1_is_not_e_3]) ).
fof(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1),
file('theBenchmark.p',e_2_is_not_e_1) ).
cnf(c_6,plain,
~ equalish(e_2,e_1),
inference(clausify,[status(thm)],[e_2_is_not_e_1]) ).
fof(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3),
file('theBenchmark.p',e_2_is_not_e_3) ).
cnf(c_7,plain,
~ equalish(e_2,e_3),
inference(clausify,[status(thm)],[e_2_is_not_e_3]) ).
fof(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1),
file('theBenchmark.p',e_3_is_not_e_1) ).
cnf(c_8,plain,
~ equalish(e_3,e_1),
inference(clausify,[status(thm)],[e_3_is_not_e_1]) ).
fof(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2),
file('theBenchmark.p',e_3_is_not_e_2) ).
cnf(c_9,plain,
~ equalish(e_3,e_2),
inference(clausify,[status(thm)],[e_3_is_not_e_2]) ).
fof(product_total_function2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_2,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_total_function2) ).
cnf(c_10,plain,
( equalish(C,D)
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_total_function2]) ).
fof(product_right_cancellation,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_1,VAR_3)
| ~ product(VAR_0,VAR_3,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_right_cancellation) ).
cnf(c_11,plain,
( equalish(B,D)
| ~ product(A,D,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_right_cancellation]) ).
fof(product_left_cancellation,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equalish(VAR_0,VAR_3)
| ~ product(VAR_3,VAR_1,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_left_cancellation) ).
cnf(c_12,plain,
( equalish(A,D)
| ~ product(D,B,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_left_cancellation]) ).
cnf(c_15,plain,
( ~ product(e_2,A,B)
| ~ product(e_3,A,B) ),
inference(resolve,[status(thm)],[c_12,c_9]) ).
cnf(c_16,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_2,B) ),
inference(resolve,[status(thm)],[c_11,c_6]) ).
cnf(c_17,plain,
( ~ product(A,e_1,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_11,c_8]) ).
cnf(c_18,plain,
( ~ product(A,e_2,B)
| ~ product(A,e_3,B) ),
inference(resolve,[status(thm)],[c_11,c_9]) ).
cnf(c_21,plain,
( ~ product(A,B,e_2)
| ~ product(A,B,e_3) ),
inference(resolve,[status(thm)],[c_10,c_9]) ).
cnf(c_28,plain,
( ~ next(A,e_3)
| ~ greater(B,e_0)
| ~ product(A,e_1,e_2)
| ~ cycle(A,B) ),
inference(resolve,[status(thm)],[c_7,c_2]) ).
cnf(c_29,plain,
( ~ next(C,e_1)
| ~ greater(e_2,e_0)
| ~ next(A,B)
| ~ cycle(B,C)
| ~ cycle(A,e_2) ),
inference(resolve,[status(thm)],[c_6,c_3]) ).
cnf(c_33,plain,
( ~ next(A,e_3)
| ~ greater(B,e_0)
| ~ product(A,e_1,e_1)
| ~ cycle(A,B) ),
inference(resolve,[status(thm)],[c_5,c_2]) ).
cnf(c_35,plain,
( ~ next(C,e_2)
| ~ greater(e_1,e_0)
| ~ next(A,B)
| ~ cycle(B,C)
| ~ cycle(A,e_1) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
fof(qg3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( product(VAR_3,VAR_1,VAR_0)
| ~ product(VAR_0,VAR_2,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',qg3) ).
cnf(c_37,plain,
( product(D,B,A)
| ~ product(A,C,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[qg3]) ).
fof(product_total_function1,axiom,
! [VAR_0,VAR_1] :
( product(VAR_0,VAR_1,e_3)
| product(VAR_0,VAR_1,e_2)
| product(VAR_0,VAR_1,e_1)
| ~ group_element(VAR_1)
| ~ group_element(VAR_0) ),
file('theBenchmark.p',product_total_function1) ).
cnf(c_38,plain,
( product(A,B,e_3)
| product(A,B,e_2)
| product(A,B,e_1)
| ~ group_element(B)
| ~ group_element(A) ),
inference(clausify,[status(thm)],[product_total_function1]) ).
fof(element_3,axiom,
group_element(e_3),
file('theBenchmark.p',element_3) ).
cnf(c_39,plain,
group_element(e_3),
inference(clausify,[status(thm)],[element_3]) ).
fof(element_2,axiom,
group_element(e_2),
file('theBenchmark.p',element_2) ).
cnf(c_40,plain,
group_element(e_2),
inference(clausify,[status(thm)],[element_2]) ).
fof(element_1,axiom,
group_element(e_1),
file('theBenchmark.p',element_1) ).
cnf(c_41,plain,
group_element(e_1),
inference(clausify,[status(thm)],[element_1]) ).
fof(cycle6,axiom,
! [VAR_0,VAR_1] :
( ~ greater(VAR_1,VAR_0)
| ~ product(VAR_0,e_1,VAR_1)
| ~ cycle(VAR_0,e_0) ),
file('theBenchmark.p',cycle6) ).
cnf(c_42,plain,
( ~ greater(B,A)
| ~ product(A,e_1,B)
| ~ cycle(A,e_0) ),
inference(clausify,[status(thm)],[cycle6]) ).
fof(cycle5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ greater(VAR_1,VAR_4)
| ~ greater(VAR_2,VAR_0)
| ~ next(VAR_2,VAR_3)
| ~ cycle(VAR_3,VAR_4)
| ~ cycle(VAR_2,e_0)
| ~ cycle(VAR_0,VAR_1) ),
file('theBenchmark.p',cycle5) ).
cnf(c_43,plain,
( ~ greater(B,E)
| ~ greater(C,A)
| ~ next(C,D)
| ~ cycle(D,E)
| ~ cycle(C,e_0)
| ~ cycle(A,B) ),
inference(clausify,[status(thm)],[cycle5]) ).
fof(cycle3,axiom,
cycle(e_3,e_0),
file('theBenchmark.p',cycle3) ).
cnf(c_44,plain,
cycle(e_3,e_0),
inference(clausify,[status(thm)],[cycle3]) ).
fof(cycle2,axiom,
! [VAR_0] :
( cycle(VAR_0,e_2)
| cycle(VAR_0,e_1)
| cycle(VAR_0,e_0)
| ~ group_element(VAR_0) ),
file('theBenchmark.p',cycle2) ).
cnf(c_45,plain,
( cycle(A,e_2)
| cycle(A,e_1)
| cycle(A,e_0)
| ~ group_element(A) ),
inference(clausify,[status(thm)],[cycle2]) ).
fof(e_3_greater_e_2,axiom,
greater(e_3,e_2),
file('theBenchmark.p',e_3_greater_e_2) ).
cnf(c_46,plain,
greater(e_3,e_2),
inference(clausify,[status(thm)],[e_3_greater_e_2]) ).
fof(e_2_greater_e_1,axiom,
greater(e_2,e_1),
file('theBenchmark.p',e_2_greater_e_1) ).
cnf(c_48,plain,
greater(e_2,e_1),
inference(clausify,[status(thm)],[e_2_greater_e_1]) ).
fof(e_2_greater_e_0,axiom,
greater(e_2,e_0),
file('theBenchmark.p',e_2_greater_e_0) ).
cnf(c_50,plain,
greater(e_2,e_0),
inference(clausify,[status(thm)],[e_2_greater_e_0]) ).
fof(e_1_greater_e_0,axiom,
greater(e_1,e_0),
file('theBenchmark.p',e_1_greater_e_0) ).
cnf(c_51,plain,
greater(e_1,e_0),
inference(clausify,[status(thm)],[e_1_greater_e_0]) ).
fof(e_2_then_e_3,axiom,
next(e_2,e_3),
file('theBenchmark.p',e_2_then_e_3) ).
cnf(c_52,plain,
next(e_2,e_3),
inference(clausify,[status(thm)],[e_2_then_e_3]) ).
fof(e_1_then_e_2,axiom,
next(e_1,e_2),
file('theBenchmark.p',e_1_then_e_2) ).
cnf(c_53,plain,
next(e_1,e_2),
inference(clausify,[status(thm)],[e_1_then_e_2]) ).
fof(e_0_then_e_1,axiom,
next(e_0,e_1),
file('theBenchmark.p',e_0_then_e_1) ).
cnf(c_54,plain,
next(e_0,e_1),
inference(clausify,[status(thm)],[e_0_then_e_1]) ).
cnf(c_695,plain,
( ~ greater(e_1,e_0)
| ~ next(A,e_2)
| ~ cycle(e_2,A)
| ~ cycle(A,e_1) ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_65,plain,
( ~ next(A,e_2)
| ~ cycle(e_2,A)
| ~ cycle(A,e_1) ),
inference(resolve,[status(thm)],[c_51,c_695]) ).
cnf(c_66,plain,
( product(B,B,A)
| ~ product(A,B,B) ),
inference(factor,[status(thm)],[c_37]) ).
cnf(c_67,plain,
( product(A,A,e_3)
| product(A,A,e_2)
| product(A,A,e_1)
| ~ group_element(A) ),
inference(factor,[status(thm)],[c_38]) ).
cnf(c_74,plain,
( ~ next(C,e_1)
| ~ next(A,B)
| ~ cycle(B,C)
| ~ cycle(A,e_2) ),
inference(resolve,[status(thm)],[c_50,c_29]) ).
cnf(c_83,plain,
( product(A,e_3,e_3)
| product(A,e_3,e_2)
| product(A,e_3,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_39,c_38]) ).
cnf(c_84,plain,
( product(e_3,A,e_3)
| product(e_3,A,e_2)
| product(e_3,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_39,c_38]) ).
cnf(c_86,plain,
( product(e_2,A,e_3)
| product(e_2,A,e_2)
| product(e_2,A,e_1)
| ~ group_element(A) ),
inference(resolve,[status(thm)],[c_40,c_38]) ).
cnf(c_89,plain,
( cycle(e_1,e_2)
| cycle(e_1,e_1)
| cycle(e_1,e_0) ),
inference(resolve,[status(thm)],[c_45,c_41]) ).
cnf(c_90,plain,
( cycle(e_2,e_2)
| cycle(e_2,e_1)
| cycle(e_2,e_0) ),
inference(resolve,[status(thm)],[c_45,c_40]) ).
cnf(c_91,plain,
( ~ greater(B,C)
| ~ greater(e_2,A)
| ~ cycle(e_3,C)
| ~ cycle(e_2,e_0)
| ~ cycle(A,B) ),
inference(resolve,[status(thm)],[c_52,c_43]) ).
cnf(c_109,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_65,c_53]) ).
cnf(c_111,plain,
( product(e_2,e_2,e_3)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_67,c_40]) ).
cnf(c_696,plain,
( ~ next(e_0,e_1)
| ~ next(A,e_3)
| ~ cycle(A,e_2) ),
inference(resolve,[status(thm)],[c_74,c_44]) ).
cnf(c_697,plain,
( ~ next(e_0,e_1)
| ~ cycle(e_2,e_2) ),
inference(resolve,[status(thm)],[c_696,c_52]) ).
cnf(c_125,plain,
~ cycle(e_2,e_2),
inference(resolve,[status(thm)],[c_697,c_54]) ).
cnf(c_126,plain,
( cycle(e_2,e_1)
| cycle(e_2,e_0) ),
inference(resolve,[status(thm)],[c_125,c_90]) ).
cnf(c_139,plain,
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_83,c_40]) ).
cnf(c_140,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolve,[status(thm)],[c_84,c_41]) ).
cnf(c_150,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_86,c_41]) ).
cnf(c_153,plain,
( product(A,e_2,e_2)
| ~ product(e_2,e_3,A)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_111,c_37]) ).
cnf(c_156,plain,
( ~ product(e_2,e_3,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(factor,[status(thm)],[c_153]) ).
cnf(c_168,plain,
( ~ product(e_2,e_2,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_139,c_18]) ).
cnf(c_169,plain,
( ~ product(e_2,e_1,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_139,c_17]) ).
cnf(c_174,plain,
( ~ greater(B,e_0)
| ~ greater(e_2,A)
| ~ cycle(e_2,e_0)
| ~ cycle(A,B) ),
inference(resolve,[status(thm)],[c_91,c_44]) ).
cnf(c_184,plain,
( ~ product(e_2,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolve,[status(thm)],[c_140,c_15]) ).
cnf(c_698,plain,
( ~ greater(e_3,e_2)
| ~ cycle(e_2,e_0)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_150,c_42]) ).
cnf(c_202,plain,
( ~ cycle(e_2,e_0)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_46,c_698]) ).
cnf(c_203,plain,
( product(e_3,A,e_2)
| ~ product(e_2,A,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_150,c_37]) ).
cnf(c_204,plain,
( product(A,e_1,e_2)
| ~ product(e_2,e_3,A)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_150,c_37]) ).
cnf(c_208,plain,
( ~ product(e_2,e_3,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(factor,[status(thm)],[c_204]) ).
cnf(c_218,plain,
( cycle(e_2,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_202,c_126]) ).
cnf(c_256,plain,
( cycle(e_2,e_1)
| ~ greater(B,e_0)
| ~ greater(e_2,A)
| ~ cycle(A,B) ),
inference(resolve,[status(thm)],[c_174,c_126]) ).
cnf(c_259,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_168,c_111]) ).
cnf(c_260,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_169,c_150]) ).
cnf(c_262,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolve,[status(thm)],[c_184,c_150]) ).
cnf(c_699,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_259,c_156]) ).
cnf(c_700,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_3,e_1) ),
inference(copy,[status(thm)],[c_699]) ).
cnf(c_317,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_3,e_1) ),
inference(copy,[status(thm)],[c_700]) ).
cnf(c_701,plain,
( product(e_1,e_2,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_317,c_153]) ).
cnf(c_702,plain,
( product(e_1,e_2,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(copy,[status(thm)],[c_701]) ).
cnf(c_320,plain,
( product(e_1,e_2,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(copy,[status(thm)],[c_702]) ).
cnf(c_326,plain,
( ~ product(e_2,e_1,e_2)
| product(e_1,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_320,c_16]) ).
cnf(c_703,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_3,e_1) ),
inference(resolve,[status(thm)],[c_260,c_208]) ).
cnf(c_704,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_3,e_1) ),
inference(copy,[status(thm)],[c_703]) ).
cnf(c_334,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_3,e_1) ),
inference(copy,[status(thm)],[c_704]) ).
cnf(c_340,plain,
( cycle(e_2,e_1)
| product(e_2,e_1,e_1)
| product(e_1,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolve,[status(thm)],[c_326,c_218]) ).
cnf(c_705,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_334,c_204]) ).
cnf(c_706,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_705]) ).
cnf(c_342,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_706]) ).
cnf(c_707,plain,
( product(e_3,e_3,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_334,c_203]) ).
cnf(c_708,plain,
( product(e_3,e_3,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_707]) ).
cnf(c_343,plain,
( product(e_3,e_3,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_708]) ).
cnf(c_352,plain,
( product(A,e_1,e_2)
| ~ product(e_2,e_2,A)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_342,c_37]) ).
cnf(c_709,plain,
( ~ next(e_2,e_3)
| ~ greater(A,e_0)
| ~ cycle(e_2,A)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_342,c_28]) ).
cnf(c_354,plain,
( ~ greater(A,e_0)
| ~ cycle(e_2,A)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_52,c_709]) ).
cnf(c_355,plain,
( ~ product(e_2,e_2,e_1)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(factor,[status(thm)],[c_352]) ).
cnf(c_362,plain,
( ~ product(e_3,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_343,c_17]) ).
cnf(c_710,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_3,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_362,c_262]) ).
cnf(c_711,plain,
( product(e_2,e_1,e_2)
| product(e_3,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_710]) ).
cnf(c_385,plain,
( product(e_3,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(copy,[status(thm)],[c_711]) ).
cnf(c_400,plain,
( product(e_1,e_1,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_385,c_66]) ).
cnf(c_712,plain,
( ~ next(e_2,e_3)
| ~ greater(A,e_0)
| ~ cycle(e_2,A)
| product(e_1,e_1,e_3)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_400,c_28]) ).
cnf(c_413,plain,
( ~ greater(A,e_0)
| ~ cycle(e_2,A)
| product(e_1,e_1,e_3)
| product(e_2,e_1,e_1) ),
inference(resolve,[status(thm)],[c_52,c_712]) ).
cnf(c_713,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_1)
| cycle(e_2,e_1)
| product(e_2,e_1,e_1)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_340,c_355]) ).
cnf(c_440,plain,
( product(e_1,e_1,e_2)
| cycle(e_2,e_1)
| product(e_2,e_1,e_1)
| product(e_1,e_2,e_2) ),
inference(copy,[status(thm)],[c_713]) ).
cnf(c_714,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_2)
| cycle(e_2,e_1)
| product(e_1,e_2,e_2) ),
inference(resolve,[status(thm)],[c_440,c_66]) ).
cnf(c_457,plain,
( product(e_1,e_1,e_2)
| cycle(e_2,e_1)
| product(e_1,e_2,e_2) ),
inference(copy,[status(thm)],[c_714]) ).
cnf(c_458,plain,
( product(e_2,e_2,e_1)
| product(e_1,e_1,e_2)
| cycle(e_2,e_1) ),
inference(resolve,[status(thm)],[c_457,c_66]) ).
cnf(c_715,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_1)
| product(e_1,e_1,e_2)
| cycle(e_2,e_1) ),
inference(resolve,[status(thm)],[c_458,c_355]) ).
cnf(c_462,plain,
( product(e_2,e_1,e_1)
| product(e_1,e_1,e_2)
| cycle(e_2,e_1) ),
inference(copy,[status(thm)],[c_715]) ).
cnf(c_716,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_2)
| cycle(e_2,e_1) ),
inference(resolve,[status(thm)],[c_462,c_66]) ).
cnf(c_466,plain,
( product(e_1,e_1,e_2)
| cycle(e_2,e_1) ),
inference(copy,[status(thm)],[c_716]) ).
cnf(c_717,plain,
( ~ greater(e_2,e_1)
| ~ cycle(e_1,e_0)
| cycle(e_2,e_1) ),
inference(resolve,[status(thm)],[c_466,c_42]) ).
cnf(c_477,plain,
( ~ cycle(e_1,e_0)
| cycle(e_2,e_1) ),
inference(resolve,[status(thm)],[c_48,c_717]) ).
cnf(c_483,plain,
( cycle(e_1,e_2)
| cycle(e_1,e_1)
| cycle(e_2,e_1) ),
inference(resolve,[status(thm)],[c_477,c_89]) ).
cnf(c_718,plain,
( ~ greater(e_1,e_0)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_1)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_483,c_354]) ).
cnf(c_491,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_1)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_51,c_718]) ).
cnf(c_719,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_2)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_491,c_66]) ).
cnf(c_528,plain,
( product(e_1,e_1,e_2)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(copy,[status(thm)],[c_719]) ).
cnf(c_720,plain,
( ~ greater(e_2,e_1)
| ~ cycle(e_1,e_0)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_528,c_42]) ).
cnf(c_531,plain,
( ~ cycle(e_1,e_0)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_48,c_720]) ).
cnf(c_721,plain,
( cycle(e_1,e_2)
| cycle(e_1,e_1)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_531,c_89]) ).
cnf(c_722,plain,
( cycle(e_1,e_2)
| cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(copy,[status(thm)],[c_721]) ).
cnf(c_535,plain,
( cycle(e_1,e_2)
| cycle(e_1,e_1) ),
inference(copy,[status(thm)],[c_722]) ).
cnf(c_723,plain,
( cycle(e_2,e_1)
| ~ greater(e_2,e_0)
| ~ greater(e_2,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_535,c_256]) ).
cnf(c_724,plain,
( cycle(e_2,e_1)
| ~ greater(e_2,e_0)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_48,c_723]) ).
cnf(c_539,plain,
( cycle(e_2,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_50,c_724]) ).
cnf(c_725,plain,
( ~ greater(e_1,e_0)
| product(e_1,e_1,e_3)
| product(e_2,e_1,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_539,c_413]) ).
cnf(c_548,plain,
( product(e_1,e_1,e_3)
| product(e_2,e_1,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_51,c_725]) ).
cnf(c_726,plain,
( ~ greater(e_1,e_0)
| product(e_1,e_1,e_2)
| product(e_2,e_1,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_539,c_354]) ).
cnf(c_549,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_51,c_726]) ).
cnf(c_727,plain,
( ~ next(e_2,e_3)
| ~ greater(A,e_0)
| ~ cycle(e_2,A)
| product(e_1,e_1,e_3)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_548,c_33]) ).
cnf(c_587,plain,
( ~ greater(A,e_0)
| ~ cycle(e_2,A)
| product(e_1,e_1,e_3)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_52,c_727]) ).
cnf(c_728,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_549,c_66]) ).
cnf(c_590,plain,
( product(e_1,e_1,e_2)
| cycle(e_1,e_1) ),
inference(copy,[status(thm)],[c_728]) ).
cnf(c_729,plain,
( cycle(e_1,e_1)
| ~ greater(e_1,e_0)
| product(e_1,e_1,e_3)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_587,c_539]) ).
cnf(c_730,plain,
( ~ greater(e_1,e_0)
| product(e_1,e_1,e_3)
| cycle(e_1,e_1) ),
inference(copy,[status(thm)],[c_729]) ).
cnf(c_627,plain,
( product(e_1,e_1,e_3)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_51,c_730]) ).
cnf(c_635,plain,
( ~ product(e_1,e_1,e_2)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_627,c_21]) ).
cnf(c_731,plain,
( cycle(e_1,e_1)
| cycle(e_1,e_1) ),
inference(resolve,[status(thm)],[c_635,c_590]) ).
cnf(c_637,plain,
cycle(e_1,e_1),
inference(copy,[status(thm)],[c_731]) ).
cnf(c_642,plain,
~ cycle(e_2,e_1),
inference(resolve,[status(thm)],[c_637,c_109]) ).
cnf(c_666,plain,
cycle(e_2,e_0),
inference(resolve,[status(thm)],[c_642,c_126]) ).
cnf(c_732,plain,
( ~ greater(e_1,C)
| ~ greater(A,e_1)
| ~ next(A,B)
| ~ cycle(B,C)
| ~ cycle(A,e_0) ),
inference(resolve,[status(thm)],[c_43,c_637]) ).
cnf(c_733,plain,
( ~ greater(e_1,e_0)
| ~ greater(A,e_1)
| ~ next(A,e_3)
| ~ cycle(A,e_0) ),
inference(resolve,[status(thm)],[c_732,c_44]) ).
cnf(c_734,plain,
( ~ greater(e_1,e_0)
| ~ greater(e_2,e_1)
| ~ cycle(e_2,e_0) ),
inference(resolve,[status(thm)],[c_733,c_52]) ).
cnf(c_735,plain,
( ~ greater(e_1,e_0)
| ~ cycle(e_2,e_0) ),
inference(resolve,[status(thm)],[c_734,c_48]) ).
cnf(c_736,plain,
~ cycle(e_2,e_0),
inference(resolve,[status(thm)],[c_735,c_51]) ).
cnf(c_694,plain,
$false,
inference(resolve,[status(thm)],[c_666,c_736]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP130-3.003 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n008.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Fri Sep 25 14:29:54 UTC 2026
% 0.19/0.43 % CPUTime :
% 0.19/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.44 % Process 1266400 was started by sandbox2 on n008,
% 0.19/0.44 % Fri Sep 25 14:29:54 2026
% 0.19/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/0.44
% 0.19/0.44 % From the command line: assign(max_seconds, 300).
% 0.19/0.54
% 0.19/0.54 % SZS status Unsatisfiable for theBenchmark
% 0.19/0.54
% 0.19/0.54 % Proof 1 at 0.05 (+ 0.02) seconds.
% 0.19/0.54 % Length of proof is 104.
% 0.19/0.54 % Level of proof is 28.
% 0.19/0.54 % Maximum clause weight is 23.000.
% 0.19/0.54 % Given clauses 363.
% 0.19/0.54
% 0.19/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------