%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN102-1.007.007 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 09:37:03 AM UTC 2026
% Result : Unsatisfiable 30.89s 14.37s
% Output : CNFRefutation 30.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 33
% Syntax : Number of formulae : 181 ( 19 unt; 0 def)
% Number of atoms : 927 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 1546 ( 800 ~; 746 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 1 prp; 0-7 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 710 ( 0 sgn 175 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(n_s3_type11_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_0(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_1) ).
cnf(c_1,plain,
( ~ p_2(A,B,C,D,E,F,V6)
| ~ p_1(A,B,C,D,E,F,V6)
| p_0(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_1]) ).
fof(n_s3_goal_1,axiom,
( ~ q_0(a,a,a,a,a,a,a)
| ~ p_0(a,a,a,a,a,a,a) ),
file('theBenchmark.p',n_s3_goal_1) ).
cnf(c_2,plain,
( ~ q_0(a,a,a,a,a,a,a)
| ~ p_0(a,a,a,a,a,a,a) ),
inference(clausify,[status(thm)],[n_s3_goal_1]) ).
fof(n_s3_type12_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ q_1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_0(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_2) ).
cnf(c_4,plain,
( ~ p_2(A,B,C,D,E,F,V6)
| ~ q_1(A,B,C,D,E,F,V6)
| q_0(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_2]) ).
cnf(c_5,plain,
( ~ q_0(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ p_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(n_s3_type11_7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_4(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_3(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_7) ).
cnf(c_8,plain,
( ~ p_5(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| p_3(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_7]) ).
fof(n_s3_type11_5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_4(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_3(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_5) ).
cnf(c_9,plain,
( ~ p_4(A,B,C,D,E,F,V6)
| ~ p_3(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_5]) ).
fof(n_s3_type11_3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_3(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_3) ).
cnf(c_10,plain,
( ~ p_3(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_3]) ).
fof(n_s3_type12_7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_4(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_3(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_7) ).
cnf(c_15,plain,
( ~ q_5(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| q_3(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_7]) ).
fof(n_s3_type12_3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_3(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_2(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_1(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_3) ).
cnf(c_17,plain,
( ~ q_3(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_3]) ).
fof(n_s3_type11_11,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_11) ).
cnf(c_20,plain,
( ~ p_7(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_5(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_11]) ).
fof(n_s3_type11_9,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_4(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_9) ).
cnf(c_21,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| ~ p_5(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_9]) ).
cnf(c_28,plain,
( ~ p_4(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_5(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_8,c_9]) ).
cnf(c_29,plain,
( ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6)
| ~ p_5(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_8,c_10]) ).
fof(n_s3_type12_11,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_11) ).
cnf(c_37,plain,
( ~ q_7(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| q_5(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_11]) ).
cnf(c_41,plain,
( ~ q_5(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_17,c_15]) ).
fof(n_s3_type11_15,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_15) ).
cnf(c_44,plain,
( ~ p_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| p_7(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_15]) ).
fof(n_s3_type11_13,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_13) ).
cnf(c_45,plain,
( ~ p_8(A,B,C,D,E,F,V6)
| ~ p_7(A,B,C,D,E,F,V6)
| p_6(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_13]) ).
cnf(c_58,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_7(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_20,c_21]) ).
cnf(c_64,plain,
( ~ p_7(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_28,c_20]) ).
cnf(c_65,plain,
( ~ p_7(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_29,c_20]) ).
fof(n_s3_type12_15,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_15) ).
cnf(c_78,plain,
( ~ q_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| q_7(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_15]) ).
cnf(c_88,plain,
( ~ q_7(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_41,c_37]) ).
fof(n_s3_type11_19,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_19) ).
cnf(c_90,plain,
( ~ p_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| p_9(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_19]) ).
fof(n_s3_type11_17,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_17) ).
cnf(c_91,plain,
( ~ p_10(A,B,C,D,E,F,V6)
| ~ p_9(A,B,C,D,E,F,V6)
| p_8(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_17]) ).
cnf(c_114,plain,
( ~ p_8(A,B,C,D,E,F,V6)
| p_6(A,B,C,D,E,F,V6)
| ~ p_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_44,c_45]) ).
cnf(c_126,plain,
( ~ p_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_58,c_44]) ).
cnf(c_131,plain,
( ~ p_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_64,c_44]) ).
cnf(c_132,plain,
( ~ p_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_65,c_44]) ).
fof(n_s3_type12_19,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_19) ).
cnf(c_155,plain,
( ~ q_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| q_9(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_19]) ).
cnf(c_176,plain,
( ~ q_9(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_88,c_78]) ).
fof(n_s3_type11_23,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ p_12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_23) ).
cnf(c_178,plain,
( ~ p_13(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| p_11(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_23]) ).
fof(n_s3_type11_24,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ q_12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_24) ).
cnf(c_221,plain,
( ~ q_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| p_11(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_24]) ).
cnf(c_223,plain,
( ~ p_10(A,B,C,D,E,F,V6)
| p_8(A,B,C,D,E,F,V6)
| ~ p_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_90,c_91]) ).
cnf(c_245,plain,
( ~ p_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| p_6(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_114,c_90]) ).
cnf(c_256,plain,
( ~ p_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_126,c_90]) ).
cnf(c_261,plain,
( ~ p_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_131,c_90]) ).
cnf(c_262,plain,
( ~ p_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_132,c_90]) ).
fof(n_s3_type12_24,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ q_12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| q_11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type12_24) ).
cnf(c_264,plain,
( ~ p_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| q_11(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type12_24]) ).
fof(n_s3_type11_22,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ q_12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| ~ q_11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type11_22) ).
cnf(c_308,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ q_11(A,B,C,D,E,F,V6)
| p_10(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type11_22]) ).
cnf(c_348,plain,
( ~ q_11(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_176,c_155]) ).
fof(n_s3_type2_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ p_6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6)
| p_13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_s3_type2_1) ).
cnf(c_350,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| p_13(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_s3_type2_1]) ).
cnf(c_393,plain,
( ~ p_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| p_10(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_308,c_264]) ).
cnf(c_432,plain,
( ~ p_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_348,c_264]) ).
fof(n_t3_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ nq_7(VAR_6)
| ~ nq_6(VAR_5)
| ~ nq_5(VAR_4)
| ~ nq_4(VAR_3)
| ~ nq_3(VAR_2)
| ~ nq_2(VAR_1)
| ~ nq_1(VAR_0)
| p_13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_t3_2) ).
cnf(c_434,plain,
( ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A)
| p_13(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_t3_2]) ).
cnf(c_510,plain,
( ~ p_13(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_256,c_178]) ).
cnf(c_515,plain,
( ~ p_13(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_261,c_178]) ).
fof(n_t3_4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ nq_7(VAR_6)
| ~ nq_6(VAR_5)
| ~ nq_5(VAR_4)
| ~ nq_4(VAR_3)
| ~ nq_3(VAR_2)
| ~ nq_2(VAR_1)
| ~ nq_1(VAR_0)
| q_13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_t3_4) ).
cnf(c_518,plain,
( ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A)
| q_13(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_t3_4]) ).
cnf(c_562,plain,
( ~ q_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| p_8(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_223,c_221]) ).
cnf(c_583,plain,
( ~ q_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| p_6(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_245,c_221]) ).
cnf(c_600,plain,
( ~ q_13(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_262,c_221]) ).
fof(n_1,axiom,
nq_1(a),
file('theBenchmark.p',n_1) ).
cnf(c_686,plain,
nq_1(a),
inference(clausify,[status(thm)],[n_1]) ).
fof(n_t3_3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ nq_7(VAR_6)
| ~ nq_6(VAR_5)
| ~ nq_5(VAR_4)
| ~ nq_4(VAR_3)
| ~ nq_3(VAR_2)
| ~ nq_2(VAR_1)
| ~ nq_1(VAR_0)
| q_12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_t3_3) ).
cnf(c_687,plain,
( ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A)
| q_12(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_t3_3]) ).
fof(n_t3_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ nq_7(VAR_6)
| ~ nq_6(VAR_5)
| ~ nq_5(VAR_4)
| ~ nq_4(VAR_3)
| ~ nq_3(VAR_2)
| ~ nq_2(VAR_1)
| ~ nq_1(VAR_0)
| p_12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6) ),
file('theBenchmark.p',n_t3_1) ).
cnf(c_688,plain,
( ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A)
| p_12(A,B,C,D,E,F,V6) ),
inference(clausify,[status(thm)],[n_t3_1]) ).
cnf(c_730,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| p_8(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A) ),
inference(resolve,[status(thm)],[c_518,c_562]) ).
cnf(c_750,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| p_6(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A) ),
inference(resolve,[status(thm)],[c_518,c_583]) ).
cnf(c_766,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| p_1(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A) ),
inference(resolve,[status(thm)],[c_518,c_600]) ).
cnf(c_833,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ q_12(A,B,C,D,E,F,V6)
| p_10(A,B,C,D,E,F,V6)
| ~ nq_7(V6)
| ~ nq_6(F)
| ~ nq_5(E)
| ~ nq_4(D)
| ~ nq_3(C)
| ~ nq_2(B)
| ~ nq_1(A) ),
inference(resolve,[status(thm)],[c_434,c_393]) ).
cnf(c_933,plain,
( ~ nq_7(F)
| ~ nq_6(E)
| ~ nq_5(D)
| ~ nq_4(C)
| ~ nq_3(B)
| ~ nq_2(A)
| q_12(a,A,B,C,D,E,F) ),
inference(resolve,[status(thm)],[c_686,c_687]) ).
cnf(c_934,plain,
( ~ nq_7(F)
| ~ nq_6(E)
| ~ nq_5(D)
| ~ nq_4(C)
| ~ nq_3(B)
| ~ nq_2(A)
| p_12(a,A,B,C,D,E,F) ),
inference(resolve,[status(thm)],[c_686,c_688]) ).
cnf(c_972,plain,
( ~ q_12(a,A,B,C,D,E,F)
| ~ p_10(a,A,B,C,D,E,F)
| p_8(a,A,B,C,D,E,F)
| ~ p_10(a,A,B,C,D,E,F)
| ~ nq_7(F)
| ~ nq_6(E)
| ~ nq_5(D)
| ~ nq_4(C)
| ~ nq_3(B)
| ~ nq_2(A) ),
inference(resolve,[status(thm)],[c_686,c_730]) ).
cnf(c_990,plain,
( ~ q_12(a,A,B,C,D,E,F)
| ~ p_10(a,A,B,C,D,E,F)
| ~ p_8(a,A,B,C,D,E,F)
| p_6(a,A,B,C,D,E,F)
| ~ p_8(a,A,B,C,D,E,F)
| ~ nq_7(F)
| ~ nq_6(E)
| ~ nq_5(D)
| ~ nq_4(C)
| ~ nq_3(B)
| ~ nq_2(A) ),
inference(resolve,[status(thm)],[c_686,c_750]) ).
cnf(c_1004,plain,
( ~ q_12(a,A,B,C,D,E,F)
| ~ p_10(a,A,B,C,D,E,F)
| ~ p_8(a,A,B,C,D,E,F)
| ~ p_6(a,A,B,C,D,E,F)
| ~ p_2(a,A,B,C,D,E,F)
| p_1(a,A,B,C,D,E,F)
| ~ p_4(a,A,B,C,D,E,F)
| ~ nq_7(F)
| ~ nq_6(E)
| ~ nq_5(D)
| ~ nq_4(C)
| ~ nq_3(B)
| ~ nq_2(A) ),
inference(resolve,[status(thm)],[c_686,c_766]) ).
cnf(c_1190,plain,
( ~ q_12(a,A,B,C,D,E,F)
| ~ q_12(a,A,B,C,D,E,F)
| p_10(a,A,B,C,D,E,F)
| ~ nq_7(F)
| ~ nq_6(E)
| ~ nq_5(D)
| ~ nq_4(C)
| ~ nq_3(B)
| ~ nq_2(A) ),
inference(resolve,[status(thm)],[c_833,c_686]) ).
fof(n_3,axiom,
nq_2(a),
file('theBenchmark.p',n_3) ).
cnf(c_1303,plain,
nq_2(a),
inference(clausify,[status(thm)],[n_3]) ).
cnf(c_1464,plain,
( ~ q_12(a,a,A,B,C,D,E)
| ~ q_12(a,a,A,B,C,D,E)
| p_10(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(resolve,[status(thm)],[c_1303,c_1190]) ).
cnf(c_1465,plain,
( ~ q_12(a,a,A,B,C,D,E)
| p_10(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(copy,[status(thm)],[c_1464]) ).
cnf(c_1685,plain,
( ~ q_12(a,a,A,B,C,D,E)
| ~ p_10(a,a,A,B,C,D,E)
| ~ p_8(a,a,A,B,C,D,E)
| ~ p_6(a,a,A,B,C,D,E)
| ~ p_2(a,a,A,B,C,D,E)
| p_1(a,a,A,B,C,D,E)
| ~ p_4(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(resolve,[status(thm)],[c_1303,c_1004]) ).
cnf(c_1694,plain,
( ~ q_12(a,a,A,B,C,D,E)
| ~ p_10(a,a,A,B,C,D,E)
| ~ p_8(a,a,A,B,C,D,E)
| p_6(a,a,A,B,C,D,E)
| ~ p_8(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(resolve,[status(thm)],[c_1303,c_990]) ).
cnf(c_1695,plain,
( ~ q_12(a,a,A,B,C,D,E)
| ~ p_10(a,a,A,B,C,D,E)
| p_6(a,a,A,B,C,D,E)
| ~ p_8(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(copy,[status(thm)],[c_1694]) ).
cnf(c_1708,plain,
( ~ q_12(a,a,A,B,C,D,E)
| ~ p_10(a,a,A,B,C,D,E)
| p_8(a,a,A,B,C,D,E)
| ~ p_10(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(resolve,[status(thm)],[c_1303,c_972]) ).
cnf(c_1709,plain,
( ~ q_12(a,a,A,B,C,D,E)
| p_8(a,a,A,B,C,D,E)
| ~ p_10(a,a,A,B,C,D,E)
| ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A) ),
inference(copy,[status(thm)],[c_1708]) ).
cnf(c_1738,plain,
( ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A)
| p_12(a,a,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_1303,c_934]) ).
cnf(c_1739,plain,
( ~ nq_7(E)
| ~ nq_6(D)
| ~ nq_5(C)
| ~ nq_4(B)
| ~ nq_3(A)
| q_12(a,a,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_1303,c_933]) ).
cnf(c_2415,plain,
( ~ p_2(a,a,a,a,a,a,a)
| ~ p_1(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_4,c_5]) ).
cnf(c_2416,plain,
( ~ p_1(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_2415]) ).
fof(n_5,axiom,
nq_3(a),
file('theBenchmark.p',n_5) ).
cnf(c_2417,plain,
nq_3(a),
inference(clausify,[status(thm)],[n_5]) ).
fof(n_7,axiom,
nq_4(a),
file('theBenchmark.p',n_7) ).
cnf(c_2419,plain,
nq_4(a),
inference(clausify,[status(thm)],[n_7]) ).
fof(n_9,axiom,
nq_5(a),
file('theBenchmark.p',n_9) ).
cnf(c_2421,plain,
nq_5(a),
inference(clausify,[status(thm)],[n_9]) ).
fof(n_11,axiom,
nq_6(a),
file('theBenchmark.p',n_11) ).
cnf(c_2423,plain,
nq_6(a),
inference(clausify,[status(thm)],[n_11]) ).
fof(n_13,axiom,
nq_7(a),
file('theBenchmark.p',n_13) ).
cnf(c_2425,plain,
nq_7(a),
inference(clausify,[status(thm)],[n_13]) ).
cnf(c_2516,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_350,c_432]) ).
cnf(c_2517,plain,
( ~ q_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| ~ p_2(A,B,C,D,E,F,V6)
| q_1(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(copy,[status(thm)],[c_2516]) ).
cnf(c_2596,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_510,c_350]) ).
cnf(c_3247,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(copy,[status(thm)],[c_2596]) ).
cnf(c_2597,plain,
( ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| p_4(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6) ),
inference(copy,[status(thm)],[c_3247]) ).
cnf(c_2606,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_515,c_350]) ).
cnf(c_3248,plain,
( ~ p_6(A,B,C,D,E,F,V6)
| ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(copy,[status(thm)],[c_2606]) ).
cnf(c_2607,plain,
( ~ p_12(A,B,C,D,E,F,V6)
| ~ p_10(A,B,C,D,E,F,V6)
| ~ p_8(A,B,C,D,E,F,V6)
| ~ p_6(A,B,C,D,E,F,V6)
| p_2(A,B,C,D,E,F,V6)
| ~ p_4(A,B,C,D,E,F,V6) ),
inference(copy,[status(thm)],[c_3248]) ).
cnf(c_3249,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2416,c_1685]) ).
cnf(c_3250,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3249]) ).
cnf(c_3251,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2417,c_3250]) ).
cnf(c_3252,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2419,c_3251]) ).
cnf(c_3253,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2421,c_3252]) ).
cnf(c_3254,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2423,c_3253]) ).
cnf(c_2837,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2425,c_3254]) ).
cnf(c_3255,plain,
( ~ nq_7(D)
| ~ nq_6(C)
| ~ nq_5(B)
| ~ nq_4(A)
| q_12(a,a,a,A,B,C,D) ),
inference(resolve,[status(thm)],[c_1739,c_2417]) ).
cnf(c_3256,plain,
( ~ nq_7(C)
| ~ nq_6(B)
| ~ nq_5(A)
| q_12(a,a,a,a,A,B,C) ),
inference(resolve,[status(thm)],[c_3255,c_2419]) ).
cnf(c_3257,plain,
( ~ nq_7(B)
| ~ nq_6(A)
| q_12(a,a,a,a,a,A,B) ),
inference(resolve,[status(thm)],[c_3256,c_2421]) ).
cnf(c_3258,plain,
( ~ nq_7(A)
| q_12(a,a,a,a,a,a,A) ),
inference(resolve,[status(thm)],[c_3257,c_2423]) ).
cnf(c_2919,plain,
q_12(a,a,a,a,a,a,a),
inference(resolve,[status(thm)],[c_3258,c_2425]) ).
cnf(c_3259,plain,
( ~ nq_7(D)
| ~ nq_6(C)
| ~ nq_5(B)
| ~ nq_4(A)
| p_12(a,a,a,A,B,C,D) ),
inference(resolve,[status(thm)],[c_1738,c_2417]) ).
cnf(c_3260,plain,
( ~ nq_7(C)
| ~ nq_6(B)
| ~ nq_5(A)
| p_12(a,a,a,a,A,B,C) ),
inference(resolve,[status(thm)],[c_3259,c_2419]) ).
cnf(c_3261,plain,
( ~ nq_7(B)
| ~ nq_6(A)
| p_12(a,a,a,a,a,A,B) ),
inference(resolve,[status(thm)],[c_3260,c_2421]) ).
cnf(c_3262,plain,
( ~ nq_7(A)
| p_12(a,a,a,a,a,a,A) ),
inference(resolve,[status(thm)],[c_3261,c_2423]) ).
cnf(c_2935,plain,
p_12(a,a,a,a,a,a,a),
inference(resolve,[status(thm)],[c_3262,c_2425]) ).
cnf(c_2968,plain,
( ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ q_1(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2919,c_2837]) ).
cnf(c_3263,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2968,c_2517]) ).
cnf(c_3264,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3263]) ).
cnf(c_3265,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3264]) ).
cnf(c_3266,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3265]) ).
cnf(c_3267,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3266]) ).
cnf(c_3268,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3267]) ).
cnf(c_3197,plain,
( ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_2(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2919,c_3268]) ).
cnf(c_3269,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_3197,c_2607]) ).
cnf(c_3270,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3269]) ).
cnf(c_3271,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3270]) ).
cnf(c_3272,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3271]) ).
cnf(c_3273,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3272]) ).
cnf(c_3204,plain,
( ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_4(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2935,c_3273]) ).
cnf(c_3274,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_3204,c_2597]) ).
cnf(c_3275,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3274]) ).
cnf(c_3276,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3275]) ).
cnf(c_3277,plain,
( ~ p_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3276]) ).
cnf(c_3213,plain,
( ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ p_6(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2935,c_3277]) ).
cnf(c_3278,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_3213,c_1695]) ).
cnf(c_3279,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3278]) ).
cnf(c_3280,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3279]) ).
cnf(c_3281,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2417,c_3280]) ).
cnf(c_3282,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2419,c_3281]) ).
cnf(c_3283,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2421,c_3282]) ).
cnf(c_3284,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2423,c_3283]) ).
cnf(c_3285,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2425,c_3284]) ).
cnf(c_3225,plain,
( ~ p_10(a,a,a,a,a,a,a)
| ~ p_8(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2919,c_3285]) ).
cnf(c_3286,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_3225,c_1709]) ).
cnf(c_3287,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(copy,[status(thm)],[c_3286]) ).
cnf(c_3288,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2417,c_3287]) ).
cnf(c_3289,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2419,c_3288]) ).
cnf(c_3290,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2421,c_3289]) ).
cnf(c_3291,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2423,c_3290]) ).
cnf(c_3292,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ p_10(a,a,a,a,a,a,a) ),
inference(resolve,[status(thm)],[c_2425,c_3291]) ).
cnf(c_3241,plain,
~ p_10(a,a,a,a,a,a,a),
inference(resolve,[status(thm)],[c_2919,c_3292]) ).
cnf(c_3293,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a)
| ~ nq_3(a) ),
inference(resolve,[status(thm)],[c_3241,c_1465]) ).
cnf(c_3294,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a)
| ~ nq_4(a) ),
inference(resolve,[status(thm)],[c_2417,c_3293]) ).
cnf(c_3295,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a)
| ~ nq_5(a) ),
inference(resolve,[status(thm)],[c_2419,c_3294]) ).
cnf(c_3296,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a)
| ~ nq_6(a) ),
inference(resolve,[status(thm)],[c_2421,c_3295]) ).
cnf(c_3297,plain,
( ~ q_12(a,a,a,a,a,a,a)
| ~ nq_7(a) ),
inference(resolve,[status(thm)],[c_2423,c_3296]) ).
cnf(c_3298,plain,
~ q_12(a,a,a,a,a,a,a),
inference(resolve,[status(thm)],[c_2425,c_3297]) ).
cnf(c_3246,plain,
$false,
inference(resolve,[status(thm)],[c_2919,c_3298]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN102-1.007.007 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/10.40 % Computer : n004.cluster.edu
% 0.11/10.40 % Model : x86_64 x86_64
% 0.11/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.40 % Memory : 8046.5625MB
% 0.11/10.40 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Sat Sep 26 17:11:47 UTC 2026
% 0.11/10.40 % CPUTime :
% 0.11/10.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/10.41 % Process 2227709 was started by sandbox on n004,
% 0.11/10.41 % Sat Sep 26 17:11:47 2026
% 0.11/10.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/10.41
% 0.11/10.41 % From the command line: assign(max_seconds, 300).
% 30.89/14.37
% 30.89/14.37 % given #500 (I,wt=50): 2071 q_4(a,b,A,B,C,D,E) | -p_6(a,b,A,B,C,D,E) | -p_8(a,b,A,B,C,D,E) | -p_10(a,b,A,B,C,D,E) | -p_12(a,b,A,B,C,D,E) | -nq_3(A) | -nq_4(B) | -nq_5(C) | -nq_6(D) | -nq_7(E). [copy(2070),merge(c)].
% 30.89/14.37
% 30.89/14.37 % SZS status Unsatisfiable for theBenchmark
% 30.89/14.37
% 30.89/14.37 % Proof 1 at 3.87 (+ 0.06) seconds.
% 30.89/14.37 % Length of proof is 96.
% 30.89/14.37 % Level of proof is 16.
% 30.89/14.37 % Maximum clause weight is 66.000.
% 30.89/14.37 % Given clauses 800.
% 30.89/14.37
% 30.89/14.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------