%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MSC015-1.010 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 08:04:28 AM UTC 2026
% Result : Unsatisfiable 0.15s 5.48s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 559
% Number of leaves : 12
% Syntax : Number of formulae : 1048 (1028 unt; 0 def)
% Number of atoms : 1068 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 599 ( 579 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-10 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 90 ( 0 sgn 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(init,axiom,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0),
file('theBenchmark.p',init) ).
cnf(c_1,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0),
inference(clausify,[status(thm)],[init]) ).
fof(rule1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] :
( p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8,s1)
| ~ p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8,s0) ),
file('theBenchmark.p',rule1) ).
cnf(c_2,plain,
( p(A,B,C,D,E,F,V6,V7,V8,s1)
| ~ p(A,B,C,D,E,F,V6,V7,V8,s0) ),
inference(clausify,[status(thm)],[rule1]) ).
fof(rule2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,s1,s0)
| ~ p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,s0,s1) ),
file('theBenchmark.p',rule2) ).
cnf(c_3,plain,
( p(A,B,C,D,E,F,V6,V7,s1,s0)
| ~ p(A,B,C,D,E,F,V6,V7,s0,s1) ),
inference(clausify,[status(thm)],[rule2]) ).
fof(rule3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,s1,s0,s0)
| ~ p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,s0,s1,s1) ),
file('theBenchmark.p',rule3) ).
cnf(c_4,plain,
( p(A,B,C,D,E,F,V6,s1,s0,s0)
| ~ p(A,B,C,D,E,F,V6,s0,s1,s1) ),
inference(clausify,[status(thm)],[rule3]) ).
fof(rule4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,s1,s0,s0,s0)
| ~ p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,s0,s1,s1,s1) ),
file('theBenchmark.p',rule4) ).
cnf(c_5,plain,
( p(A,B,C,D,E,F,s1,s0,s0,s0)
| ~ p(A,B,C,D,E,F,s0,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule4]) ).
fof(rule5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,s1,s0,s0,s0,s0)
| ~ p(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,s0,s1,s1,s1,s1) ),
file('theBenchmark.p',rule5) ).
cnf(c_6,plain,
( p(A,B,C,D,E,s1,s0,s0,s0,s0)
| ~ p(A,B,C,D,E,s0,s1,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule5]) ).
fof(rule6,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p(VAR_0,VAR_1,VAR_2,VAR_3,s1,s0,s0,s0,s0,s0)
| ~ p(VAR_0,VAR_1,VAR_2,VAR_3,s0,s1,s1,s1,s1,s1) ),
file('theBenchmark.p',rule6) ).
cnf(c_7,plain,
( p(A,B,C,D,s1,s0,s0,s0,s0,s0)
| ~ p(A,B,C,D,s0,s1,s1,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule6]) ).
fof(rule7,axiom,
! [VAR_0,VAR_1,VAR_2] :
( p(VAR_0,VAR_1,VAR_2,s1,s0,s0,s0,s0,s0,s0)
| ~ p(VAR_0,VAR_1,VAR_2,s0,s1,s1,s1,s1,s1,s1) ),
file('theBenchmark.p',rule7) ).
cnf(c_8,plain,
( p(A,B,C,s1,s0,s0,s0,s0,s0,s0)
| ~ p(A,B,C,s0,s1,s1,s1,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule7]) ).
fof(rule8,axiom,
! [VAR_0,VAR_1] :
( p(VAR_0,VAR_1,s1,s0,s0,s0,s0,s0,s0,s0)
| ~ p(VAR_0,VAR_1,s0,s1,s1,s1,s1,s1,s1,s1) ),
file('theBenchmark.p',rule8) ).
cnf(c_9,plain,
( p(A,B,s1,s0,s0,s0,s0,s0,s0,s0)
| ~ p(A,B,s0,s1,s1,s1,s1,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule8]) ).
fof(rule9,axiom,
! [VAR_0] :
( p(VAR_0,s1,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(VAR_0,s0,s1,s1,s1,s1,s1,s1,s1,s1) ),
file('theBenchmark.p',rule9) ).
cnf(c_10,plain,
( p(A,s1,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(A,s0,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule9]) ).
fof(rule10,axiom,
( p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) ),
file('theBenchmark.p',rule10) ).
cnf(c_11,plain,
( p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(clausify,[status(thm)],[rule10]) ).
fof(goal,axiom,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1),
file('theBenchmark.p',goal) ).
cnf(c_12,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_13,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_1]) ).
cnf(c_14,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_12,c_2]) ).
cnf(c_15,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_13]) ).
cnf(c_16,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_14,c_3]) ).
cnf(c_17,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_16,c_2]) ).
cnf(c_18,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_17,c_4]) ).
cnf(c_19,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_18,c_2]) ).
cnf(c_20,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_15]) ).
cnf(c_21,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_20]) ).
cnf(c_22,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_21]) ).
cnf(c_23,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_22]) ).
cnf(c_24,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_19,c_3]) ).
cnf(c_25,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_23]) ).
cnf(c_26,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_24,c_2]) ).
cnf(c_27,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_26,c_5]) ).
cnf(c_28,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_27,c_2]) ).
cnf(c_29,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_28,c_3]) ).
cnf(c_30,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_29,c_2]) ).
cnf(c_31,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_25]) ).
cnf(c_32,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_31]) ).
cnf(c_33,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_32]) ).
cnf(c_34,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_33]) ).
cnf(c_35,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_30,c_4]) ).
cnf(c_36,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_34]) ).
cnf(c_37,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_35,c_2]) ).
cnf(c_38,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_37,c_3]) ).
cnf(c_39,plain,
~ p(s1,s1,s1,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_38,c_2]) ).
cnf(c_40,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_39,c_6]) ).
cnf(c_41,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_40,c_2]) ).
cnf(c_42,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_36]) ).
cnf(c_43,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_42]) ).
cnf(c_44,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_43]) ).
cnf(c_45,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_44]) ).
cnf(c_46,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_41,c_3]) ).
cnf(c_47,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_45]) ).
cnf(c_48,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_46,c_2]) ).
cnf(c_49,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_48,c_4]) ).
cnf(c_50,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_49,c_2]) ).
cnf(c_51,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_50,c_3]) ).
cnf(c_52,plain,
~ p(s1,s1,s1,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_51,c_2]) ).
cnf(c_53,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_47]) ).
cnf(c_54,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_53]) ).
cnf(c_55,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_54]) ).
cnf(c_56,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_55]) ).
cnf(c_57,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_52,c_5]) ).
cnf(c_58,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_56]) ).
cnf(c_59,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_57,c_2]) ).
cnf(c_60,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_59,c_3]) ).
cnf(c_61,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_60,c_2]) ).
cnf(c_62,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_61,c_4]) ).
cnf(c_63,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_62,c_2]) ).
cnf(c_64,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_58]) ).
cnf(c_65,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_64]) ).
cnf(c_66,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_65]) ).
cnf(c_67,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_66]) ).
cnf(c_68,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_63,c_3]) ).
cnf(c_69,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_67]) ).
cnf(c_70,plain,
~ p(s1,s1,s1,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_68,c_2]) ).
cnf(c_71,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_70,c_7]) ).
cnf(c_72,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_71,c_2]) ).
cnf(c_73,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_72,c_3]) ).
cnf(c_74,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_73,c_2]) ).
cnf(c_75,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_69]) ).
cnf(c_76,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_75]) ).
cnf(c_77,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_76]) ).
cnf(c_78,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_77]) ).
cnf(c_79,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_74,c_4]) ).
cnf(c_80,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_78]) ).
cnf(c_81,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_79,c_2]) ).
cnf(c_82,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_81,c_3]) ).
cnf(c_83,plain,
~ p(s1,s1,s1,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_82,c_2]) ).
cnf(c_84,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_83,c_5]) ).
cnf(c_85,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_84,c_2]) ).
cnf(c_86,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_80]) ).
cnf(c_87,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_86]) ).
cnf(c_88,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_87]) ).
cnf(c_89,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_88]) ).
cnf(c_90,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_85,c_3]) ).
cnf(c_91,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_89]) ).
cnf(c_92,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_90,c_2]) ).
cnf(c_93,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_92,c_4]) ).
cnf(c_94,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_93,c_2]) ).
cnf(c_95,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_94,c_3]) ).
cnf(c_96,plain,
~ p(s1,s1,s1,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_95,c_2]) ).
cnf(c_97,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_91]) ).
cnf(c_98,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_97]) ).
cnf(c_99,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_98]) ).
cnf(c_100,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_99]) ).
cnf(c_101,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_96,c_6]) ).
cnf(c_102,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_100]) ).
cnf(c_103,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_101,c_2]) ).
cnf(c_104,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_103,c_3]) ).
cnf(c_105,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_104,c_2]) ).
cnf(c_106,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_105,c_4]) ).
cnf(c_107,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_106,c_2]) ).
cnf(c_108,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_102]) ).
cnf(c_109,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_108]) ).
cnf(c_110,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_109]) ).
cnf(c_111,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_110]) ).
cnf(c_112,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_107,c_3]) ).
cnf(c_113,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_111]) ).
cnf(c_114,plain,
~ p(s1,s1,s1,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_112,c_2]) ).
cnf(c_115,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_114,c_5]) ).
cnf(c_116,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_115,c_2]) ).
cnf(c_117,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_116,c_3]) ).
cnf(c_118,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_117,c_2]) ).
cnf(c_119,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_113]) ).
cnf(c_120,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_119]) ).
cnf(c_121,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_120]) ).
cnf(c_122,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_121]) ).
cnf(c_123,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_118,c_4]) ).
cnf(c_124,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_122]) ).
cnf(c_125,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_123,c_2]) ).
cnf(c_126,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_125,c_3]) ).
cnf(c_127,plain,
~ p(s1,s1,s1,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_126,c_2]) ).
cnf(c_128,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_127,c_8]) ).
cnf(c_129,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_128,c_2]) ).
cnf(c_130,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_124]) ).
cnf(c_131,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_130]) ).
cnf(c_132,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_131]) ).
cnf(c_133,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_132]) ).
cnf(c_134,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_129,c_3]) ).
cnf(c_135,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_133]) ).
cnf(c_136,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_134,c_2]) ).
cnf(c_137,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_136,c_4]) ).
cnf(c_138,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_137,c_2]) ).
cnf(c_139,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_138,c_3]) ).
cnf(c_140,plain,
~ p(s1,s1,s1,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_139,c_2]) ).
cnf(c_141,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_135]) ).
cnf(c_142,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_141]) ).
cnf(c_143,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_142]) ).
cnf(c_144,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_143]) ).
cnf(c_145,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_140,c_5]) ).
cnf(c_146,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_144]) ).
cnf(c_147,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_145,c_2]) ).
cnf(c_148,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_147,c_3]) ).
cnf(c_149,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_148,c_2]) ).
cnf(c_150,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_149,c_4]) ).
cnf(c_151,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_150,c_2]) ).
cnf(c_152,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_146]) ).
cnf(c_153,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_8,c_152]) ).
cnf(c_154,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_153]) ).
cnf(c_155,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_154]) ).
cnf(c_156,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_151,c_3]) ).
cnf(c_157,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_155]) ).
cnf(c_158,plain,
~ p(s1,s1,s1,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_156,c_2]) ).
cnf(c_159,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_158,c_6]) ).
cnf(c_160,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_159,c_2]) ).
cnf(c_161,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_160,c_3]) ).
cnf(c_162,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_161,c_2]) ).
cnf(c_163,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_157]) ).
cnf(c_164,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_163]) ).
cnf(c_165,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_164]) ).
cnf(c_166,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_165]) ).
cnf(c_167,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_162,c_4]) ).
cnf(c_168,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_166]) ).
cnf(c_169,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_167,c_2]) ).
cnf(c_170,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_169,c_3]) ).
cnf(c_171,plain,
~ p(s1,s1,s1,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_170,c_2]) ).
cnf(c_172,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_171,c_5]) ).
cnf(c_173,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_172,c_2]) ).
cnf(c_174,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_168]) ).
cnf(c_175,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_174]) ).
cnf(c_176,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_175]) ).
cnf(c_177,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_176]) ).
cnf(c_178,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_173,c_3]) ).
cnf(c_179,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_177]) ).
cnf(c_180,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_178,c_2]) ).
cnf(c_181,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_180,c_4]) ).
cnf(c_182,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_181,c_2]) ).
cnf(c_183,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_182,c_3]) ).
cnf(c_184,plain,
~ p(s1,s1,s1,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_183,c_2]) ).
cnf(c_185,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_179]) ).
cnf(c_186,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_185]) ).
cnf(c_187,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_186]) ).
cnf(c_188,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_187]) ).
cnf(c_189,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_184,c_7]) ).
cnf(c_190,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_188]) ).
cnf(c_191,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_189,c_2]) ).
cnf(c_192,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_191,c_3]) ).
cnf(c_193,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_192,c_2]) ).
cnf(c_194,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_193,c_4]) ).
cnf(c_195,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_194,c_2]) ).
cnf(c_196,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_190]) ).
cnf(c_197,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_196]) ).
cnf(c_198,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_197]) ).
cnf(c_199,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_198]) ).
cnf(c_200,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_195,c_3]) ).
cnf(c_201,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_199]) ).
cnf(c_202,plain,
~ p(s1,s1,s1,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_200,c_2]) ).
cnf(c_203,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_202,c_5]) ).
cnf(c_204,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_203,c_2]) ).
cnf(c_205,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_204,c_3]) ).
cnf(c_206,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_205,c_2]) ).
cnf(c_207,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_201]) ).
cnf(c_208,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_207]) ).
cnf(c_209,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_208]) ).
cnf(c_210,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_209]) ).
cnf(c_211,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_206,c_4]) ).
cnf(c_212,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_210]) ).
cnf(c_213,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_211,c_2]) ).
cnf(c_214,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_213,c_3]) ).
cnf(c_215,plain,
~ p(s1,s1,s1,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_214,c_2]) ).
cnf(c_216,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_215,c_6]) ).
cnf(c_217,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_216,c_2]) ).
cnf(c_218,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_212]) ).
cnf(c_219,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_218]) ).
cnf(c_220,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_219]) ).
cnf(c_221,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_220]) ).
cnf(c_222,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_217,c_3]) ).
cnf(c_223,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_221]) ).
cnf(c_224,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_222,c_2]) ).
cnf(c_225,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_224,c_4]) ).
cnf(c_226,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_225,c_2]) ).
cnf(c_227,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_226,c_3]) ).
cnf(c_228,plain,
~ p(s1,s1,s1,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_227,c_2]) ).
cnf(c_229,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_223]) ).
cnf(c_230,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_229]) ).
cnf(c_231,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_230]) ).
cnf(c_232,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_231]) ).
cnf(c_233,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_228,c_5]) ).
cnf(c_234,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_232]) ).
cnf(c_235,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_233,c_2]) ).
cnf(c_236,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_235,c_3]) ).
cnf(c_237,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_236,c_2]) ).
cnf(c_238,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_237,c_4]) ).
cnf(c_239,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_238,c_2]) ).
cnf(c_240,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_234]) ).
cnf(c_241,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_240]) ).
cnf(c_242,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_241]) ).
cnf(c_243,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_242]) ).
cnf(c_244,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_239,c_3]) ).
cnf(c_245,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_243]) ).
cnf(c_246,plain,
~ p(s1,s1,s1,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_244,c_2]) ).
cnf(c_247,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_246,c_9]) ).
cnf(c_248,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_247,c_2]) ).
cnf(c_249,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_248,c_3]) ).
cnf(c_250,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_249,c_2]) ).
cnf(c_251,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_245]) ).
cnf(c_252,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_251]) ).
cnf(c_253,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_252]) ).
cnf(c_254,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_253]) ).
cnf(c_255,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_250,c_4]) ).
cnf(c_256,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_254]) ).
cnf(c_257,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_255,c_2]) ).
cnf(c_258,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_257,c_3]) ).
cnf(c_259,plain,
~ p(s1,s1,s0,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_258,c_2]) ).
cnf(c_260,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_259,c_5]) ).
cnf(c_261,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_260,c_2]) ).
cnf(c_262,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_256]) ).
cnf(c_263,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_262]) ).
cnf(c_264,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_263]) ).
cnf(c_265,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_264]) ).
cnf(c_266,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_261,c_3]) ).
cnf(c_267,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_265]) ).
cnf(c_268,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_266,c_2]) ).
cnf(c_269,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_268,c_4]) ).
cnf(c_270,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_269,c_2]) ).
cnf(c_271,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_270,c_3]) ).
cnf(c_272,plain,
~ p(s1,s1,s0,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_271,c_2]) ).
cnf(c_273,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_267]) ).
cnf(c_274,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_273]) ).
cnf(c_275,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_274]) ).
cnf(c_276,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_275]) ).
cnf(c_277,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_272,c_6]) ).
cnf(c_278,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_276]) ).
cnf(c_279,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_277,c_2]) ).
cnf(c_280,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_279,c_3]) ).
cnf(c_281,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_280,c_2]) ).
cnf(c_282,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_281,c_4]) ).
cnf(c_283,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_282,c_2]) ).
cnf(c_284,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_278]) ).
cnf(c_285,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_284]) ).
cnf(c_286,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_285]) ).
cnf(c_287,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_286]) ).
cnf(c_288,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_283,c_3]) ).
cnf(c_289,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_287]) ).
cnf(c_290,plain,
~ p(s1,s1,s0,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_288,c_2]) ).
cnf(c_291,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_290,c_5]) ).
cnf(c_292,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_291,c_2]) ).
cnf(c_293,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_292,c_3]) ).
cnf(c_294,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_293,c_2]) ).
cnf(c_295,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_9,c_289]) ).
cnf(c_296,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_295]) ).
cnf(c_297,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_296]) ).
cnf(c_298,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_297]) ).
cnf(c_299,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_294,c_4]) ).
cnf(c_300,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_298]) ).
cnf(c_301,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_299,c_2]) ).
cnf(c_302,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_301,c_3]) ).
cnf(c_303,plain,
~ p(s1,s1,s0,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_302,c_2]) ).
cnf(c_304,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_303,c_7]) ).
cnf(c_305,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_304,c_2]) ).
cnf(c_306,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_300]) ).
cnf(c_307,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_306]) ).
cnf(c_308,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_307]) ).
cnf(c_309,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_308]) ).
cnf(c_310,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_305,c_3]) ).
cnf(c_311,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_309]) ).
cnf(c_312,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_310,c_2]) ).
cnf(c_313,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_312,c_4]) ).
cnf(c_314,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_313,c_2]) ).
cnf(c_315,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_314,c_3]) ).
cnf(c_316,plain,
~ p(s1,s1,s0,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_315,c_2]) ).
cnf(c_317,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_311]) ).
cnf(c_318,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_317]) ).
cnf(c_319,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_318]) ).
cnf(c_320,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_319]) ).
cnf(c_321,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_316,c_5]) ).
cnf(c_322,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_320]) ).
cnf(c_323,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_321,c_2]) ).
cnf(c_324,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_323,c_3]) ).
cnf(c_325,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_324,c_2]) ).
cnf(c_326,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_325,c_4]) ).
cnf(c_327,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_326,c_2]) ).
cnf(c_328,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_322]) ).
cnf(c_329,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_328]) ).
cnf(c_330,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_329]) ).
cnf(c_331,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_330]) ).
cnf(c_332,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_327,c_3]) ).
cnf(c_333,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_331]) ).
cnf(c_334,plain,
~ p(s1,s1,s0,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_332,c_2]) ).
cnf(c_335,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_334,c_6]) ).
cnf(c_336,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_335,c_2]) ).
cnf(c_337,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_336,c_3]) ).
cnf(c_338,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_337,c_2]) ).
cnf(c_339,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_333]) ).
cnf(c_340,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_339]) ).
cnf(c_341,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_340]) ).
cnf(c_342,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_341]) ).
cnf(c_343,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_338,c_4]) ).
cnf(c_344,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_342]) ).
cnf(c_345,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_343,c_2]) ).
cnf(c_346,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_345,c_3]) ).
cnf(c_347,plain,
~ p(s1,s1,s0,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_346,c_2]) ).
cnf(c_348,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_347,c_5]) ).
cnf(c_349,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_348,c_2]) ).
cnf(c_350,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_344]) ).
cnf(c_351,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_350]) ).
cnf(c_352,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_351]) ).
cnf(c_353,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_352]) ).
cnf(c_354,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_349,c_3]) ).
cnf(c_355,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_353]) ).
cnf(c_356,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_354,c_2]) ).
cnf(c_357,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_356,c_4]) ).
cnf(c_358,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_357,c_2]) ).
cnf(c_359,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_358,c_3]) ).
cnf(c_360,plain,
~ p(s1,s1,s0,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_359,c_2]) ).
cnf(c_361,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_355]) ).
cnf(c_362,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_361]) ).
cnf(c_363,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_362]) ).
cnf(c_364,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_363]) ).
cnf(c_365,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_360,c_8]) ).
cnf(c_366,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_364]) ).
cnf(c_367,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_365,c_2]) ).
cnf(c_368,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_367,c_3]) ).
cnf(c_369,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_368,c_2]) ).
cnf(c_370,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_369,c_4]) ).
cnf(c_371,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_370,c_2]) ).
cnf(c_372,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_366]) ).
cnf(c_373,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_372]) ).
cnf(c_374,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_373]) ).
cnf(c_375,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_374]) ).
cnf(c_376,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_371,c_3]) ).
cnf(c_377,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_375]) ).
cnf(c_378,plain,
~ p(s1,s1,s0,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_376,c_2]) ).
cnf(c_379,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_378,c_5]) ).
cnf(c_380,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_379,c_2]) ).
cnf(c_381,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_380,c_3]) ).
cnf(c_382,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_381,c_2]) ).
cnf(c_383,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_377]) ).
cnf(c_384,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_383]) ).
cnf(c_385,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_384]) ).
cnf(c_386,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_385]) ).
cnf(c_387,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_382,c_4]) ).
cnf(c_388,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_386]) ).
cnf(c_389,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_387,c_2]) ).
cnf(c_390,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_389,c_3]) ).
cnf(c_391,plain,
~ p(s1,s1,s0,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_390,c_2]) ).
cnf(c_392,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_391,c_6]) ).
cnf(c_393,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_392,c_2]) ).
cnf(c_394,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_388]) ).
cnf(c_395,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_394]) ).
cnf(c_396,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_395]) ).
cnf(c_397,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_396]) ).
cnf(c_398,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_393,c_3]) ).
cnf(c_399,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_397]) ).
cnf(c_400,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_398,c_2]) ).
cnf(c_401,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_400,c_4]) ).
cnf(c_402,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_401,c_2]) ).
cnf(c_403,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_402,c_3]) ).
cnf(c_404,plain,
~ p(s1,s1,s0,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_403,c_2]) ).
cnf(c_405,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_399]) ).
cnf(c_406,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_405]) ).
cnf(c_407,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_406]) ).
cnf(c_408,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_407]) ).
cnf(c_409,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_404,c_5]) ).
cnf(c_410,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_408]) ).
cnf(c_411,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_409,c_2]) ).
cnf(c_412,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_411,c_3]) ).
cnf(c_413,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_412,c_2]) ).
cnf(c_414,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_413,c_4]) ).
cnf(c_415,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_414,c_2]) ).
cnf(c_416,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_410]) ).
cnf(c_417,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_416]) ).
cnf(c_418,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_417]) ).
cnf(c_419,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_418]) ).
cnf(c_420,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_415,c_3]) ).
cnf(c_421,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_419]) ).
cnf(c_422,plain,
~ p(s1,s1,s0,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_420,c_2]) ).
cnf(c_423,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_422,c_7]) ).
cnf(c_424,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_423,c_2]) ).
cnf(c_425,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_424,c_3]) ).
cnf(c_426,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_425,c_2]) ).
cnf(c_427,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_421]) ).
cnf(c_428,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_427]) ).
cnf(c_429,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_428]) ).
cnf(c_430,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_429]) ).
cnf(c_431,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_426,c_4]) ).
cnf(c_432,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_8,c_430]) ).
cnf(c_433,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_431,c_2]) ).
cnf(c_434,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_433,c_3]) ).
cnf(c_435,plain,
~ p(s1,s1,s0,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_434,c_2]) ).
cnf(c_436,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_435,c_5]) ).
cnf(c_437,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_436,c_2]) ).
cnf(c_438,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_432]) ).
cnf(c_439,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_438]) ).
cnf(c_440,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_439]) ).
cnf(c_441,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_440]) ).
cnf(c_442,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_437,c_3]) ).
cnf(c_443,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_441]) ).
cnf(c_444,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_442,c_2]) ).
cnf(c_445,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_444,c_4]) ).
cnf(c_446,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_445,c_2]) ).
cnf(c_447,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_446,c_3]) ).
cnf(c_448,plain,
~ p(s1,s1,s0,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_447,c_2]) ).
cnf(c_449,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_443]) ).
cnf(c_450,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_449]) ).
cnf(c_451,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_450]) ).
cnf(c_452,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_451]) ).
cnf(c_453,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_448,c_6]) ).
cnf(c_454,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_452]) ).
cnf(c_455,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_453,c_2]) ).
cnf(c_456,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_455,c_3]) ).
cnf(c_457,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_456,c_2]) ).
cnf(c_458,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_457,c_4]) ).
cnf(c_459,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_458,c_2]) ).
cnf(c_460,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_454]) ).
cnf(c_461,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_460]) ).
cnf(c_462,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_461]) ).
cnf(c_463,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_462]) ).
cnf(c_464,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_459,c_3]) ).
cnf(c_465,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_463]) ).
cnf(c_466,plain,
~ p(s1,s1,s0,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_464,c_2]) ).
cnf(c_467,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_466,c_5]) ).
cnf(c_468,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_467,c_2]) ).
cnf(c_469,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_468,c_3]) ).
cnf(c_470,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_469,c_2]) ).
cnf(c_471,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_465]) ).
cnf(c_472,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_471]) ).
cnf(c_473,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_472]) ).
cnf(c_474,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_473]) ).
cnf(c_475,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_470,c_4]) ).
cnf(c_476,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_474]) ).
cnf(c_477,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_475,c_2]) ).
cnf(c_478,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_477,c_3]) ).
cnf(c_479,plain,
~ p(s1,s1,s0,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_478,c_2]) ).
cnf(c_480,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_479,c_10]) ).
cnf(c_481,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_480,c_2]) ).
cnf(c_482,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_476]) ).
cnf(c_483,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_482]) ).
cnf(c_484,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_483]) ).
cnf(c_485,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_484]) ).
cnf(c_486,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_481,c_3]) ).
cnf(c_487,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_485]) ).
cnf(c_488,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_486,c_2]) ).
cnf(c_489,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_488,c_4]) ).
cnf(c_490,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_489,c_2]) ).
cnf(c_491,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_490,c_3]) ).
cnf(c_492,plain,
~ p(s1,s0,s1,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_491,c_2]) ).
cnf(c_493,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_487]) ).
cnf(c_494,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_493]) ).
cnf(c_495,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_494]) ).
cnf(c_496,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_495]) ).
cnf(c_497,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_492,c_5]) ).
cnf(c_498,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_496]) ).
cnf(c_499,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_497,c_2]) ).
cnf(c_500,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_499,c_3]) ).
cnf(c_501,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_500,c_2]) ).
cnf(c_502,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_501,c_4]) ).
cnf(c_503,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_502,c_2]) ).
cnf(c_504,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_498]) ).
cnf(c_505,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_504]) ).
cnf(c_506,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_505]) ).
cnf(c_507,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_506]) ).
cnf(c_508,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_503,c_3]) ).
cnf(c_509,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_507]) ).
cnf(c_510,plain,
~ p(s1,s0,s1,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_508,c_2]) ).
cnf(c_511,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_510,c_6]) ).
cnf(c_512,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_511,c_2]) ).
cnf(c_513,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_512,c_3]) ).
cnf(c_514,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_513,c_2]) ).
cnf(c_515,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_509]) ).
cnf(c_516,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_515]) ).
cnf(c_517,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_516]) ).
cnf(c_518,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_517]) ).
cnf(c_519,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_514,c_4]) ).
cnf(c_520,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_518]) ).
cnf(c_521,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_519,c_2]) ).
cnf(c_522,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_521,c_3]) ).
cnf(c_523,plain,
~ p(s1,s0,s1,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_522,c_2]) ).
cnf(c_524,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_523,c_5]) ).
cnf(c_525,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_524,c_2]) ).
cnf(c_526,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_520]) ).
cnf(c_527,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_526]) ).
cnf(c_528,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_527]) ).
cnf(c_529,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_528]) ).
cnf(c_530,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_525,c_3]) ).
cnf(c_531,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_529]) ).
cnf(c_532,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_530,c_2]) ).
cnf(c_533,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_532,c_4]) ).
cnf(c_534,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_533,c_2]) ).
cnf(c_535,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_534,c_3]) ).
cnf(c_536,plain,
~ p(s1,s0,s1,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_535,c_2]) ).
cnf(c_537,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_531]) ).
cnf(c_538,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_537]) ).
cnf(c_539,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_538]) ).
cnf(c_540,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_539]) ).
cnf(c_541,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_536,c_7]) ).
cnf(c_542,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_540]) ).
cnf(c_543,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_541,c_2]) ).
cnf(c_544,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_543,c_3]) ).
cnf(c_545,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_544,c_2]) ).
cnf(c_546,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_545,c_4]) ).
cnf(c_547,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_546,c_2]) ).
cnf(c_548,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_542]) ).
cnf(c_549,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_548]) ).
cnf(c_550,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_549]) ).
cnf(c_551,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_550]) ).
cnf(c_552,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_547,c_3]) ).
cnf(c_553,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_551]) ).
cnf(c_554,plain,
~ p(s1,s0,s1,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_552,c_2]) ).
cnf(c_555,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_554,c_5]) ).
cnf(c_556,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_555,c_2]) ).
cnf(c_557,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_556,c_3]) ).
cnf(c_558,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_557,c_2]) ).
cnf(c_559,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_553]) ).
cnf(c_560,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_559]) ).
cnf(c_561,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_560]) ).
cnf(c_562,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_561]) ).
cnf(c_563,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_558,c_4]) ).
cnf(c_564,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_562]) ).
cnf(c_565,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_563,c_2]) ).
cnf(c_566,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_565,c_3]) ).
cnf(c_567,plain,
~ p(s1,s0,s1,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_566,c_2]) ).
cnf(c_568,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_567,c_6]) ).
cnf(c_569,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_568,c_2]) ).
cnf(c_570,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_564]) ).
cnf(c_571,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_570]) ).
cnf(c_572,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_571]) ).
cnf(c_573,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_10,c_572]) ).
cnf(c_574,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_569,c_3]) ).
cnf(c_575,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_573]) ).
cnf(c_576,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_574,c_2]) ).
cnf(c_577,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_576,c_4]) ).
cnf(c_578,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_577,c_2]) ).
cnf(c_579,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_578,c_3]) ).
cnf(c_580,plain,
~ p(s1,s0,s1,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_579,c_2]) ).
cnf(c_581,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_575]) ).
cnf(c_582,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_581]) ).
cnf(c_583,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_582]) ).
cnf(c_584,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_583]) ).
cnf(c_585,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_580,c_5]) ).
cnf(c_586,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_584]) ).
cnf(c_587,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_585,c_2]) ).
cnf(c_588,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_587,c_3]) ).
cnf(c_589,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_588,c_2]) ).
cnf(c_590,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_589,c_4]) ).
cnf(c_591,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_590,c_2]) ).
cnf(c_592,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_586]) ).
cnf(c_593,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_592]) ).
cnf(c_594,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_593]) ).
cnf(c_595,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_594]) ).
cnf(c_596,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_591,c_3]) ).
cnf(c_597,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_595]) ).
cnf(c_598,plain,
~ p(s1,s0,s1,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_596,c_2]) ).
cnf(c_599,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_598,c_8]) ).
cnf(c_600,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_599,c_2]) ).
cnf(c_601,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_600,c_3]) ).
cnf(c_602,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_601,c_2]) ).
cnf(c_603,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_597]) ).
cnf(c_604,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_603]) ).
cnf(c_605,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_604]) ).
cnf(c_606,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_605]) ).
cnf(c_607,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_602,c_4]) ).
cnf(c_608,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_606]) ).
cnf(c_609,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_607,c_2]) ).
cnf(c_610,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_609,c_3]) ).
cnf(c_611,plain,
~ p(s1,s0,s1,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_610,c_2]) ).
cnf(c_612,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_611,c_5]) ).
cnf(c_613,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_612,c_2]) ).
cnf(c_614,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_608]) ).
cnf(c_615,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_614]) ).
cnf(c_616,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_615]) ).
cnf(c_617,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_616]) ).
cnf(c_618,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_613,c_3]) ).
cnf(c_619,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_617]) ).
cnf(c_620,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_618,c_2]) ).
cnf(c_621,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_620,c_4]) ).
cnf(c_622,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_621,c_2]) ).
cnf(c_623,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_622,c_3]) ).
cnf(c_624,plain,
~ p(s1,s0,s1,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_623,c_2]) ).
cnf(c_625,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_619]) ).
cnf(c_626,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_625]) ).
cnf(c_627,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_626]) ).
cnf(c_628,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_627]) ).
cnf(c_629,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_624,c_6]) ).
cnf(c_630,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_628]) ).
cnf(c_631,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_629,c_2]) ).
cnf(c_632,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_631,c_3]) ).
cnf(c_633,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_632,c_2]) ).
cnf(c_634,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_633,c_4]) ).
cnf(c_635,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_634,c_2]) ).
cnf(c_636,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_630]) ).
cnf(c_637,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_636]) ).
cnf(c_638,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_637]) ).
cnf(c_639,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_638]) ).
cnf(c_640,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_635,c_3]) ).
cnf(c_641,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_639]) ).
cnf(c_642,plain,
~ p(s1,s0,s1,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_640,c_2]) ).
cnf(c_643,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_642,c_5]) ).
cnf(c_644,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_643,c_2]) ).
cnf(c_645,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_644,c_3]) ).
cnf(c_646,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_645,c_2]) ).
cnf(c_647,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_641]) ).
cnf(c_648,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_647]) ).
cnf(c_649,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_648]) ).
cnf(c_650,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_649]) ).
cnf(c_651,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_646,c_4]) ).
cnf(c_652,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_650]) ).
cnf(c_653,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_651,c_2]) ).
cnf(c_654,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_653,c_3]) ).
cnf(c_655,plain,
~ p(s1,s0,s1,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_654,c_2]) ).
cnf(c_656,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_655,c_7]) ).
cnf(c_657,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_656,c_2]) ).
cnf(c_658,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_652]) ).
cnf(c_659,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_658]) ).
cnf(c_660,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_659]) ).
cnf(c_661,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_660]) ).
cnf(c_662,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_657,c_3]) ).
cnf(c_663,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_661]) ).
cnf(c_664,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_662,c_2]) ).
cnf(c_665,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_664,c_4]) ).
cnf(c_666,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_665,c_2]) ).
cnf(c_667,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_666,c_3]) ).
cnf(c_668,plain,
~ p(s1,s0,s1,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_667,c_2]) ).
cnf(c_669,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_663]) ).
cnf(c_670,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_669]) ).
cnf(c_671,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_670]) ).
cnf(c_672,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_671]) ).
cnf(c_673,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_668,c_5]) ).
cnf(c_674,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_672]) ).
cnf(c_675,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_673,c_2]) ).
cnf(c_676,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_675,c_3]) ).
cnf(c_677,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_676,c_2]) ).
cnf(c_678,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_677,c_4]) ).
cnf(c_679,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_678,c_2]) ).
cnf(c_680,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_674]) ).
cnf(c_681,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_680]) ).
cnf(c_682,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_681]) ).
cnf(c_683,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_682]) ).
cnf(c_684,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_679,c_3]) ).
cnf(c_685,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_683]) ).
cnf(c_686,plain,
~ p(s1,s0,s1,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_684,c_2]) ).
cnf(c_687,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_686,c_6]) ).
cnf(c_688,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_687,c_2]) ).
cnf(c_689,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_688,c_3]) ).
cnf(c_690,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_689,c_2]) ).
cnf(c_691,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_685]) ).
cnf(c_692,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_691]) ).
cnf(c_693,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_692]) ).
cnf(c_694,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_693]) ).
cnf(c_695,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_690,c_4]) ).
cnf(c_696,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_694]) ).
cnf(c_697,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_695,c_2]) ).
cnf(c_698,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_697,c_3]) ).
cnf(c_699,plain,
~ p(s1,s0,s1,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_698,c_2]) ).
cnf(c_700,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_699,c_5]) ).
cnf(c_701,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_700,c_2]) ).
cnf(c_702,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_696]) ).
cnf(c_703,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_702]) ).
cnf(c_704,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_703]) ).
cnf(c_705,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_704]) ).
cnf(c_706,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_701,c_3]) ).
cnf(c_707,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_705]) ).
cnf(c_708,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_706,c_2]) ).
cnf(c_709,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_708,c_4]) ).
cnf(c_710,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_709,c_2]) ).
cnf(c_711,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_710,c_3]) ).
cnf(c_712,plain,
~ p(s1,s0,s1,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_711,c_2]) ).
cnf(c_713,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_707]) ).
cnf(c_714,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_713]) ).
cnf(c_715,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_8,c_714]) ).
cnf(c_716,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_715]) ).
cnf(c_717,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_712,c_9]) ).
cnf(c_718,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_716]) ).
cnf(c_719,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_717,c_2]) ).
cnf(c_720,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_719,c_3]) ).
cnf(c_721,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_720,c_2]) ).
cnf(c_722,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_721,c_4]) ).
cnf(c_723,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_722,c_2]) ).
cnf(c_724,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_718]) ).
cnf(c_725,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_724]) ).
cnf(c_726,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_725]) ).
cnf(c_727,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_726]) ).
cnf(c_728,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_723,c_3]) ).
cnf(c_729,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_727]) ).
cnf(c_730,plain,
~ p(s1,s0,s0,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_728,c_2]) ).
cnf(c_731,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_730,c_5]) ).
cnf(c_732,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_731,c_2]) ).
cnf(c_733,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_732,c_3]) ).
cnf(c_734,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_733,c_2]) ).
cnf(c_735,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_729]) ).
cnf(c_736,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_735]) ).
cnf(c_737,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_736]) ).
cnf(c_738,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_737]) ).
cnf(c_739,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_734,c_4]) ).
cnf(c_740,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_738]) ).
cnf(c_741,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_739,c_2]) ).
cnf(c_742,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_741,c_3]) ).
cnf(c_743,plain,
~ p(s1,s0,s0,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_742,c_2]) ).
cnf(c_744,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_743,c_6]) ).
cnf(c_745,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_744,c_2]) ).
cnf(c_746,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_740]) ).
cnf(c_747,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_746]) ).
cnf(c_748,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_747]) ).
cnf(c_749,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_748]) ).
cnf(c_750,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_745,c_3]) ).
cnf(c_751,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_749]) ).
cnf(c_752,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_750,c_2]) ).
cnf(c_753,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_752,c_4]) ).
cnf(c_754,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_753,c_2]) ).
cnf(c_755,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_754,c_3]) ).
cnf(c_756,plain,
~ p(s1,s0,s0,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_755,c_2]) ).
cnf(c_757,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_751]) ).
cnf(c_758,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_757]) ).
cnf(c_759,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_758]) ).
cnf(c_760,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_759]) ).
cnf(c_761,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_756,c_5]) ).
cnf(c_762,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_760]) ).
cnf(c_763,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_761,c_2]) ).
cnf(c_764,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_763,c_3]) ).
cnf(c_765,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_764,c_2]) ).
cnf(c_766,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_765,c_4]) ).
cnf(c_767,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_766,c_2]) ).
cnf(c_768,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_762]) ).
cnf(c_769,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_768]) ).
cnf(c_770,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_769]) ).
cnf(c_771,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_770]) ).
cnf(c_772,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_767,c_3]) ).
cnf(c_773,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_771]) ).
cnf(c_774,plain,
~ p(s1,s0,s0,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_772,c_2]) ).
cnf(c_775,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_774,c_7]) ).
cnf(c_776,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_775,c_2]) ).
cnf(c_777,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_776,c_3]) ).
cnf(c_778,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_777,c_2]) ).
cnf(c_779,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_773]) ).
cnf(c_780,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_779]) ).
cnf(c_781,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_780]) ).
cnf(c_782,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_781]) ).
cnf(c_783,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_778,c_4]) ).
cnf(c_784,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_782]) ).
cnf(c_785,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_783,c_2]) ).
cnf(c_786,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_785,c_3]) ).
cnf(c_787,plain,
~ p(s1,s0,s0,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_786,c_2]) ).
cnf(c_788,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_787,c_5]) ).
cnf(c_789,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_788,c_2]) ).
cnf(c_790,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_784]) ).
cnf(c_791,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_790]) ).
cnf(c_792,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_791]) ).
cnf(c_793,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_792]) ).
cnf(c_794,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_789,c_3]) ).
cnf(c_795,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_793]) ).
cnf(c_796,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_794,c_2]) ).
cnf(c_797,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_796,c_4]) ).
cnf(c_798,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_797,c_2]) ).
cnf(c_799,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_798,c_3]) ).
cnf(c_800,plain,
~ p(s1,s0,s0,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_799,c_2]) ).
cnf(c_801,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_795]) ).
cnf(c_802,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_801]) ).
cnf(c_803,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_802]) ).
cnf(c_804,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_803]) ).
cnf(c_805,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_800,c_6]) ).
cnf(c_806,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_804]) ).
cnf(c_807,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_805,c_2]) ).
cnf(c_808,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_807,c_3]) ).
cnf(c_809,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_808,c_2]) ).
cnf(c_810,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_809,c_4]) ).
cnf(c_811,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_810,c_2]) ).
cnf(c_812,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_806]) ).
cnf(c_813,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_812]) ).
cnf(c_814,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_813]) ).
cnf(c_815,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_814]) ).
cnf(c_816,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_811,c_3]) ).
cnf(c_817,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_815]) ).
cnf(c_818,plain,
~ p(s1,s0,s0,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_816,c_2]) ).
cnf(c_819,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_818,c_5]) ).
cnf(c_820,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_819,c_2]) ).
cnf(c_821,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_820,c_3]) ).
cnf(c_822,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_821,c_2]) ).
cnf(c_823,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_817]) ).
cnf(c_824,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_823]) ).
cnf(c_825,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_824]) ).
cnf(c_826,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_825]) ).
cnf(c_827,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_822,c_4]) ).
cnf(c_828,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_826]) ).
cnf(c_829,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_827,c_2]) ).
cnf(c_830,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_829,c_3]) ).
cnf(c_831,plain,
~ p(s1,s0,s0,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_830,c_2]) ).
cnf(c_832,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_831,c_8]) ).
cnf(c_833,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_832,c_2]) ).
cnf(c_834,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_828]) ).
cnf(c_835,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_834]) ).
cnf(c_836,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_835]) ).
cnf(c_837,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_836]) ).
cnf(c_838,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_833,c_3]) ).
cnf(c_839,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_837]) ).
cnf(c_840,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_838,c_2]) ).
cnf(c_841,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_840,c_4]) ).
cnf(c_842,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_841,c_2]) ).
cnf(c_843,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_842,c_3]) ).
cnf(c_844,plain,
~ p(s1,s0,s0,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_843,c_2]) ).
cnf(c_845,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_839]) ).
cnf(c_846,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_845]) ).
cnf(c_847,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_846]) ).
cnf(c_848,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_847]) ).
cnf(c_849,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_844,c_5]) ).
cnf(c_850,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_848]) ).
cnf(c_851,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_849,c_2]) ).
cnf(c_852,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_851,c_3]) ).
cnf(c_853,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_852,c_2]) ).
cnf(c_854,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_853,c_4]) ).
cnf(c_855,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_854,c_2]) ).
cnf(c_856,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_850]) ).
cnf(c_857,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_9,c_856]) ).
cnf(c_858,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_857]) ).
cnf(c_859,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_858]) ).
cnf(c_860,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_855,c_3]) ).
cnf(c_861,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_859]) ).
cnf(c_862,plain,
~ p(s1,s0,s0,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_860,c_2]) ).
cnf(c_863,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_862,c_6]) ).
cnf(c_864,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_863,c_2]) ).
cnf(c_865,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_864,c_3]) ).
cnf(c_866,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_865,c_2]) ).
cnf(c_867,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_861]) ).
cnf(c_868,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_867]) ).
cnf(c_869,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_868]) ).
cnf(c_870,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_869]) ).
cnf(c_871,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_866,c_4]) ).
cnf(c_872,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_870]) ).
cnf(c_873,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_871,c_2]) ).
cnf(c_874,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_873,c_3]) ).
cnf(c_875,plain,
~ p(s1,s0,s0,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_874,c_2]) ).
cnf(c_876,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_875,c_5]) ).
cnf(c_877,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_876,c_2]) ).
cnf(c_878,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_872]) ).
cnf(c_879,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_878]) ).
cnf(c_880,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_879]) ).
cnf(c_881,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_880]) ).
cnf(c_882,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_877,c_3]) ).
cnf(c_883,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_881]) ).
cnf(c_884,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_882,c_2]) ).
cnf(c_885,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_884,c_4]) ).
cnf(c_886,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_885,c_2]) ).
cnf(c_887,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_886,c_3]) ).
cnf(c_888,plain,
~ p(s1,s0,s0,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_887,c_2]) ).
cnf(c_889,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_883]) ).
cnf(c_890,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_889]) ).
cnf(c_891,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_890]) ).
cnf(c_892,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_891]) ).
cnf(c_893,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_888,c_7]) ).
cnf(c_894,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_892]) ).
cnf(c_895,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_893,c_2]) ).
cnf(c_896,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_895,c_3]) ).
cnf(c_897,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_896,c_2]) ).
cnf(c_898,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_897,c_4]) ).
cnf(c_899,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_898,c_2]) ).
cnf(c_900,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_894]) ).
cnf(c_901,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_900]) ).
cnf(c_902,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_901]) ).
cnf(c_903,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_902]) ).
cnf(c_904,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_899,c_3]) ).
cnf(c_905,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_903]) ).
cnf(c_906,plain,
~ p(s1,s0,s0,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_904,c_2]) ).
cnf(c_907,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_906,c_5]) ).
cnf(c_908,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_907,c_2]) ).
cnf(c_909,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_908,c_3]) ).
cnf(c_910,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_909,c_2]) ).
cnf(c_911,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_905]) ).
cnf(c_912,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_911]) ).
cnf(c_913,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_912]) ).
cnf(c_914,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_913]) ).
cnf(c_915,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_910,c_4]) ).
cnf(c_916,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_914]) ).
cnf(c_917,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_915,c_2]) ).
cnf(c_918,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_917,c_3]) ).
cnf(c_919,plain,
~ p(s1,s0,s0,s0,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_918,c_2]) ).
cnf(c_920,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_919,c_6]) ).
cnf(c_921,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_920,c_2]) ).
cnf(c_922,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_916]) ).
cnf(c_923,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_922]) ).
cnf(c_924,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_923]) ).
cnf(c_925,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_7,c_924]) ).
cnf(c_926,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_921,c_3]) ).
cnf(c_927,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_925]) ).
cnf(c_928,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_926,c_2]) ).
cnf(c_929,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_928,c_4]) ).
cnf(c_930,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_929,c_2]) ).
cnf(c_931,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_930,c_3]) ).
cnf(c_932,plain,
~ p(s1,s0,s0,s0,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_931,c_2]) ).
cnf(c_933,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_927]) ).
cnf(c_934,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_933]) ).
cnf(c_935,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_934]) ).
cnf(c_936,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_935]) ).
cnf(c_937,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_932,c_5]) ).
cnf(c_938,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_936]) ).
cnf(c_939,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_937,c_2]) ).
cnf(c_940,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_939,c_3]) ).
cnf(c_941,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_940,c_2]) ).
cnf(c_942,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_941,c_4]) ).
cnf(c_943,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_942,c_2]) ).
cnf(c_944,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_938]) ).
cnf(c_945,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_944]) ).
cnf(c_946,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_945]) ).
cnf(c_947,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_946]) ).
cnf(c_948,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_943,c_3]) ).
cnf(c_949,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_947]) ).
cnf(c_950,plain,
~ p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_948,c_2]) ).
cnf(c_951,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_950,c_11]) ).
cnf(c_952,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_951,c_2]) ).
cnf(c_953,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_952,c_3]) ).
cnf(c_954,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_953,c_2]) ).
cnf(c_955,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_949]) ).
cnf(c_956,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_955]) ).
cnf(c_957,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_956]) ).
cnf(c_958,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_957]) ).
cnf(c_959,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_954,c_4]) ).
cnf(c_960,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_958]) ).
cnf(c_961,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_959,c_2]) ).
cnf(c_962,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_961,c_3]) ).
cnf(c_963,plain,
~ p(s0,s1,s1,s1,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_962,c_2]) ).
cnf(c_964,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_963,c_5]) ).
cnf(c_965,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_964,c_2]) ).
cnf(c_966,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_960]) ).
cnf(c_967,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_966]) ).
cnf(c_968,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_967]) ).
cnf(c_969,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_968]) ).
cnf(c_970,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_965,c_3]) ).
cnf(c_971,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_969]) ).
cnf(c_972,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_970,c_2]) ).
cnf(c_973,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_972,c_4]) ).
cnf(c_974,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_973,c_2]) ).
cnf(c_975,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_974,c_3]) ).
cnf(c_976,plain,
~ p(s0,s1,s1,s1,s1,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_975,c_2]) ).
cnf(c_977,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_971]) ).
cnf(c_978,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_977]) ).
cnf(c_979,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_978]) ).
cnf(c_980,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_979]) ).
cnf(c_981,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_976,c_6]) ).
cnf(c_982,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_980]) ).
cnf(c_983,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_981,c_2]) ).
cnf(c_984,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_983,c_3]) ).
cnf(c_985,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_984,c_2]) ).
cnf(c_986,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_985,c_4]) ).
cnf(c_987,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_986,c_2]) ).
cnf(c_988,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_982]) ).
cnf(c_989,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_988]) ).
cnf(c_990,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_989]) ).
cnf(c_991,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_990]) ).
cnf(c_992,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_987,c_3]) ).
cnf(c_993,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_991]) ).
cnf(c_994,plain,
~ p(s0,s1,s1,s1,s1,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_992,c_2]) ).
cnf(c_995,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_994,c_5]) ).
cnf(c_996,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_995,c_2]) ).
cnf(c_997,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_996,c_3]) ).
cnf(c_998,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_997,c_2]) ).
cnf(c_999,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_8,c_993]) ).
cnf(c_1000,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_999]) ).
cnf(c_1001,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_1000]) ).
cnf(c_1002,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_1001]) ).
cnf(c_1003,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_998,c_4]) ).
cnf(c_1004,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_1002]) ).
cnf(c_1005,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_1003,c_2]) ).
cnf(c_1006,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_1005,c_3]) ).
cnf(c_1007,plain,
~ p(s0,s1,s1,s1,s1,s0,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_1006,c_2]) ).
cnf(c_1008,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_1007,c_7]) ).
cnf(c_1009,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_1008,c_2]) ).
cnf(c_1010,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_1004]) ).
cnf(c_1011,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_1010]) ).
cnf(c_1012,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_1011]) ).
cnf(c_1013,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_5,c_1012]) ).
cnf(c_1014,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_1009,c_3]) ).
cnf(c_1015,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_1013]) ).
cnf(c_1016,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_1014,c_2]) ).
cnf(c_1017,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_1016,c_4]) ).
cnf(c_1018,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_1017,c_2]) ).
cnf(c_1019,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s0,s0,s1),
inference(resolve,[status(thm)],[c_1018,c_3]) ).
cnf(c_1020,plain,
~ p(s0,s1,s1,s1,s0,s1,s1,s0,s0,s0),
inference(resolve,[status(thm)],[c_1019,c_2]) ).
cnf(c_1021,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_1015]) ).
cnf(c_1022,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s1,s1),
inference(resolve,[status(thm)],[c_2,c_1021]) ).
cnf(c_1023,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s0,s0),
inference(resolve,[status(thm)],[c_4,c_1022]) ).
cnf(c_1024,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s0,s1),
inference(resolve,[status(thm)],[c_2,c_1023]) ).
cnf(c_1025,plain,
~ p(s0,s1,s1,s1,s0,s1,s0,s1,s1,s1),
inference(resolve,[status(thm)],[c_1020,c_5]) ).
cnf(c_1026,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s1,s0),
inference(resolve,[status(thm)],[c_3,c_1024]) ).
cnf(c_1027,plain,
~ p(s0,s1,s1,s1,s0,s1,s0,s1,s1,s0),
inference(resolve,[status(thm)],[c_1025,c_2]) ).
cnf(c_1028,plain,
~ p(s0,s1,s1,s1,s0,s1,s0,s1,s0,s1),
inference(resolve,[status(thm)],[c_1027,c_3]) ).
cnf(c_1029,plain,
~ p(s0,s1,s1,s1,s0,s1,s0,s1,s0,s0),
inference(resolve,[status(thm)],[c_1028,c_2]) ).
cnf(c_1030,plain,
~ p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s1),
inference(resolve,[status(thm)],[c_1029,c_4]) ).
cnf(c_1031,plain,
~ p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_1030,c_2]) ).
cnf(c_1032,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s1,s1),
inference(resolve,[status(thm)],[c_2,c_1026]) ).
cnf(c_1033,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s0,s0),
inference(resolve,[status(thm)],[c_6,c_1032]) ).
cnf(c_1034,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s0,s1),
inference(resolve,[status(thm)],[c_2,c_1033]) ).
cnf(c_1036,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s0),
inference(resolve,[status(thm)],[c_3,c_1034]) ).
cnf(c_1035,plain,
$false,
inference(resolve,[status(thm)],[c_1031,c_1036]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MSC015-1.010 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.36 % Computer : n004.cluster.edu
% 0.11/5.36 % Model : x86_64 x86_64
% 0.11/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.36 % Memory : 8046.5625MB
% 0.11/5.36 % OS : Linux 6.8.0-71-generic
% 0.11/5.36 % CPULimit : 300
% 0.11/5.36 % WCLimit : 300
% 0.11/5.36 % DateTime : Sat Sep 26 00:16:13 UTC 2026
% 0.11/5.36 % CPUTime :
% 0.11/5.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.36 % Process 320184 was started by sandbox2 on n004,
% 0.11/5.36 % Sat Sep 26 00:16:13 2026
% 0.11/5.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/5.37
% 0.11/5.37 % From the command line: assign(max_seconds, 300).
% 0.15/5.48
% 0.15/5.48 % given #500 (F,wt=16): 501 -p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s0). [resolve(500,a,2,b)].
% 0.15/5.48
% 0.15/5.48 % given #1000 (T,wt=16): 1001 p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s0). [ur(3,a,1000,a)].
% 0.15/5.48
% 0.15/5.48 % SZS status Unsatisfiable for theBenchmark
% 0.15/5.48
% 0.15/5.48 % Proof 1 at 0.06 (+ 0.02) seconds.
% 0.15/5.48 % Length of proof is 1035.
% 0.15/5.48 % Level of proof is 558.
% 0.15/5.48 % Maximum clause weight is 27.000.
% 0.15/5.48 % Given clauses 1033.
% 0.15/5.48
% 0.15/5.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------