%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MSC015-1.010 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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 : Fri Sep 25 02:13:36 PM UTC 2026
% Result : Unsatisfiable 40.98s 5.64s
% Output : Proof 40.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 1030
% Number of leaves : 12
% Syntax : Number of formulae : 1085 (1045 unt; 0 def)
% Number of atoms : 1125 (1037 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 86 ( 46 ~; 40 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 1 avg)
% Maximal term depth : 11 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-10 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-4 aty)
% Number of variables : 225 ( 0 sgn 90 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f1,axiom,
( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s1)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule1) ).
fof(f1_nnf,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s1)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s0) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s1)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s0) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s1)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
ifeq(p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s0),true,p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s1),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(f0,axiom,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',init) ).
fof(f0_nnf,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(hi0,axiom,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h0,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,hi0]) ).
cnf(f2,axiom,
( p(X0,X1,X2,X3,X4,X5,X6,X7,s1,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,s0,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule2) ).
fof(f2_nnf,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( p(X0,X1,X2,X3,X4,X5,X6,X7,s1,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,s0,s1) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( p(X0,X1,X2,X3,X4,X5,X6,X7,s1,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,s0,s1) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( p(X0,X1,X2,X3,X4,X5,X6,X7,s1,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,X7,s0,s1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi2,axiom,
ifeq(p(X0,X1,X2,X3,X4,X5,X6,X7,s0,s1),true,p(X0,X1,X2,X3,X4,X5,X6,X7,s1,s0),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(h1,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h0]) ).
cnf(h2,plain,
p(s0,s0,s0,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1]) ).
cnf(f3,axiom,
( p(X0,X1,X2,X3,X4,X5,X6,s1,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,s0,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule3) ).
fof(f3_nnf,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( p(X0,X1,X2,X3,X4,X5,X6,s1,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,s0,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( p(X0,X1,X2,X3,X4,X5,X6,s1,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,s0,s1,s1) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( p(X0,X1,X2,X3,X4,X5,X6,s1,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,X6,s0,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,axiom,
ifeq(p(X0,X1,X2,X3,X4,X5,X6,s0,s1,s1),true,p(X0,X1,X2,X3,X4,X5,X6,s1,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h3,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h2]) ).
cnf(h4,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h3]) ).
cnf(h5,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h4]) ).
cnf(h6,plain,
p(s0,s0,s0,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h5]) ).
cnf(f4,axiom,
( p(X0,X1,X2,X3,X4,X5,s1,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,s0,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule4) ).
fof(f4_nnf,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X0,X1,X2,X3,X4,X5,s1,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,s0,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X0,X1,X2,X3,X4,X5,s1,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,s0,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( p(X0,X1,X2,X3,X4,X5,s1,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,X5,s0,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
ifeq(p(X0,X1,X2,X3,X4,X5,s0,s1,s1,s1),true,p(X0,X1,X2,X3,X4,X5,s1,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h7,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h6]) ).
cnf(h8,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h7]) ).
cnf(h9,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h8]) ).
cnf(h10,plain,
p(s0,s0,s0,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h9]) ).
cnf(h11,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h10]) ).
cnf(h12,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h11]) ).
cnf(h13,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h12]) ).
cnf(h14,plain,
p(s0,s0,s0,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h13]) ).
cnf(f5,axiom,
( p(X0,X1,X2,X3,X4,s1,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,s0,s1,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule5) ).
fof(f5_nnf,plain,
! [X0,X1,X2,X3,X4] :
( p(X0,X1,X2,X3,X4,s1,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,s0,s1,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0,X1,X2,X3,X4] :
( p(X0,X1,X2,X3,X4,s1,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,s0,s1,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( p(X0,X1,X2,X3,X4,s1,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,X4,s0,s1,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
ifeq(p(X0,X1,X2,X3,X4,s0,s1,s1,s1,s1),true,p(X0,X1,X2,X3,X4,s1,s0,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h15,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h14]) ).
cnf(h16,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h15]) ).
cnf(h17,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h16]) ).
cnf(h18,plain,
p(s0,s0,s0,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h17]) ).
cnf(h19,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h18]) ).
cnf(h20,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h19]) ).
cnf(h21,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h20]) ).
cnf(h22,plain,
p(s0,s0,s0,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h21]) ).
cnf(h23,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h22]) ).
cnf(h24,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h23]) ).
cnf(h25,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h24]) ).
cnf(h26,plain,
p(s0,s0,s0,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h25]) ).
cnf(h27,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h26]) ).
cnf(h28,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h27]) ).
cnf(h29,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h28]) ).
cnf(h30,plain,
p(s0,s0,s0,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h29]) ).
cnf(f6,axiom,
( p(X0,X1,X2,X3,s1,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,s0,s1,s1,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule6) ).
fof(f6_nnf,plain,
! [X0,X1,X2,X3] :
( p(X0,X1,X2,X3,s1,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,s0,s1,s1,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2,X3] :
( p(X0,X1,X2,X3,s1,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,s0,s1,s1,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( p(X0,X1,X2,X3,s1,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,X3,s0,s1,s1,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,axiom,
ifeq(p(X0,X1,X2,X3,s0,s1,s1,s1,s1,s1),true,p(X0,X1,X2,X3,s1,s0,s0,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(h31,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h30]) ).
cnf(h32,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h31]) ).
cnf(h33,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h32]) ).
cnf(h34,plain,
p(s0,s0,s0,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h33]) ).
cnf(h35,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h34]) ).
cnf(h36,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h35]) ).
cnf(h37,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h36]) ).
cnf(h38,plain,
p(s0,s0,s0,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h37]) ).
cnf(h39,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h38]) ).
cnf(h40,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h39]) ).
cnf(h41,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h40]) ).
cnf(h42,plain,
p(s0,s0,s0,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h41]) ).
cnf(h43,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h42]) ).
cnf(h44,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h43]) ).
cnf(h45,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h44]) ).
cnf(h46,plain,
p(s0,s0,s0,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h45]) ).
cnf(h47,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h46]) ).
cnf(h48,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h47]) ).
cnf(h49,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h48]) ).
cnf(h50,plain,
p(s0,s0,s0,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h49]) ).
cnf(h51,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h50]) ).
cnf(h52,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h51]) ).
cnf(h53,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h52]) ).
cnf(h54,plain,
p(s0,s0,s0,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h53]) ).
cnf(h55,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h54]) ).
cnf(h56,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h55]) ).
cnf(h57,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h56]) ).
cnf(h58,plain,
p(s0,s0,s0,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h57]) ).
cnf(h59,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h58]) ).
cnf(h60,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h59]) ).
cnf(h61,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h60]) ).
cnf(h62,plain,
p(s0,s0,s0,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h61]) ).
cnf(f7,axiom,
( p(X0,X1,X2,s1,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,s0,s1,s1,s1,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule7) ).
fof(f7_nnf,plain,
! [X0,X1,X2] :
( p(X0,X1,X2,s1,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,s0,s1,s1,s1,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0,X1,X2] :
( p(X0,X1,X2,s1,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,s0,s1,s1,s1,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( p(X0,X1,X2,s1,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,X2,s0,s1,s1,s1,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi7,axiom,
ifeq(p(X0,X1,X2,s0,s1,s1,s1,s1,s1,s1),true,p(X0,X1,X2,s1,s0,s0,s0,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(h63,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h62]) ).
cnf(h64,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h63]) ).
cnf(h65,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h64]) ).
cnf(h66,plain,
p(s0,s0,s0,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h65]) ).
cnf(h67,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h66]) ).
cnf(h68,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h67]) ).
cnf(h69,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h68]) ).
cnf(h70,plain,
p(s0,s0,s0,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h69]) ).
cnf(h71,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h70]) ).
cnf(h72,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h71]) ).
cnf(h73,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h72]) ).
cnf(h74,plain,
p(s0,s0,s0,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h73]) ).
cnf(h75,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h74]) ).
cnf(h76,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h75]) ).
cnf(h77,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h76]) ).
cnf(h78,plain,
p(s0,s0,s0,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h77]) ).
cnf(h79,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h78]) ).
cnf(h80,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h79]) ).
cnf(h81,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h80]) ).
cnf(h82,plain,
p(s0,s0,s0,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h81]) ).
cnf(h83,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h82]) ).
cnf(h84,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h83]) ).
cnf(h85,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h84]) ).
cnf(h86,plain,
p(s0,s0,s0,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h85]) ).
cnf(h87,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h86]) ).
cnf(h88,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h87]) ).
cnf(h89,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h88]) ).
cnf(h90,plain,
p(s0,s0,s0,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h89]) ).
cnf(h91,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h90]) ).
cnf(h92,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h91]) ).
cnf(h93,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h92]) ).
cnf(h94,plain,
p(s0,s0,s0,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h93]) ).
cnf(h95,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h94]) ).
cnf(h96,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h95]) ).
cnf(h97,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h96]) ).
cnf(h98,plain,
p(s0,s0,s0,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h97]) ).
cnf(h99,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h98]) ).
cnf(h100,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h99]) ).
cnf(h101,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h100]) ).
cnf(h102,plain,
p(s0,s0,s0,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h101]) ).
cnf(h103,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h102]) ).
cnf(h104,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h103]) ).
cnf(h105,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h104]) ).
cnf(h106,plain,
p(s0,s0,s0,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h105]) ).
cnf(h107,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h106]) ).
cnf(h108,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h107]) ).
cnf(h109,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h108]) ).
cnf(h110,plain,
p(s0,s0,s0,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h109]) ).
cnf(h111,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h110]) ).
cnf(h112,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h111]) ).
cnf(h113,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h112]) ).
cnf(h114,plain,
p(s0,s0,s0,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h113]) ).
cnf(h115,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h114]) ).
cnf(h116,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h115]) ).
cnf(h117,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h116]) ).
cnf(h118,plain,
p(s0,s0,s0,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h117]) ).
cnf(h119,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h118]) ).
cnf(h120,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h119]) ).
cnf(h121,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h120]) ).
cnf(h122,plain,
p(s0,s0,s0,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h121]) ).
cnf(h123,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h122]) ).
cnf(h124,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h123]) ).
cnf(h125,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h124]) ).
cnf(h126,plain,
p(s0,s0,s0,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h125]) ).
cnf(f8,axiom,
( p(X0,X1,s1,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,s0,s1,s1,s1,s1,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule8) ).
fof(f8_nnf,plain,
! [X0,X1] :
( p(X0,X1,s1,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,s0,s1,s1,s1,s1,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] :
( p(X0,X1,s1,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,s0,s1,s1,s1,s1,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( p(X0,X1,s1,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,X1,s0,s1,s1,s1,s1,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi8,axiom,
ifeq(p(X0,X1,s0,s1,s1,s1,s1,s1,s1,s1),true,p(X0,X1,s1,s0,s0,s0,s0,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h127,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi8,h126]) ).
cnf(h128,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h127]) ).
cnf(h129,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h128]) ).
cnf(h130,plain,
p(s0,s0,s1,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h129]) ).
cnf(h131,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h130]) ).
cnf(h132,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h131]) ).
cnf(h133,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h132]) ).
cnf(h134,plain,
p(s0,s0,s1,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h133]) ).
cnf(h135,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h134]) ).
cnf(h136,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h135]) ).
cnf(h137,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h136]) ).
cnf(h138,plain,
p(s0,s0,s1,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h137]) ).
cnf(h139,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h138]) ).
cnf(h140,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h139]) ).
cnf(h141,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h140]) ).
cnf(h142,plain,
p(s0,s0,s1,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h141]) ).
cnf(h143,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h142]) ).
cnf(h144,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h143]) ).
cnf(h145,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h144]) ).
cnf(h146,plain,
p(s0,s0,s1,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h145]) ).
cnf(h147,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h146]) ).
cnf(h148,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h147]) ).
cnf(h149,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h148]) ).
cnf(h150,plain,
p(s0,s0,s1,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h149]) ).
cnf(h151,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h150]) ).
cnf(h152,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h151]) ).
cnf(h153,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h152]) ).
cnf(h154,plain,
p(s0,s0,s1,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h153]) ).
cnf(h155,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h154]) ).
cnf(h156,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h155]) ).
cnf(h157,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h156]) ).
cnf(h158,plain,
p(s0,s0,s1,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h157]) ).
cnf(h159,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h158]) ).
cnf(h160,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h159]) ).
cnf(h161,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h160]) ).
cnf(h162,plain,
p(s0,s0,s1,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h161]) ).
cnf(h163,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h162]) ).
cnf(h164,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h163]) ).
cnf(h165,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h164]) ).
cnf(h166,plain,
p(s0,s0,s1,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h165]) ).
cnf(h167,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h166]) ).
cnf(h168,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h167]) ).
cnf(h169,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h168]) ).
cnf(h170,plain,
p(s0,s0,s1,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h169]) ).
cnf(h171,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h170]) ).
cnf(h172,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h171]) ).
cnf(h173,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h172]) ).
cnf(h174,plain,
p(s0,s0,s1,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h173]) ).
cnf(h175,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h174]) ).
cnf(h176,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h175]) ).
cnf(h177,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h176]) ).
cnf(h178,plain,
p(s0,s0,s1,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h177]) ).
cnf(h179,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h178]) ).
cnf(h180,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h179]) ).
cnf(h181,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h180]) ).
cnf(h182,plain,
p(s0,s0,s1,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h181]) ).
cnf(h183,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h182]) ).
cnf(h184,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h183]) ).
cnf(h185,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h184]) ).
cnf(h186,plain,
p(s0,s0,s1,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h185]) ).
cnf(h187,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h186]) ).
cnf(h188,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h187]) ).
cnf(h189,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h188]) ).
cnf(h190,plain,
p(s0,s0,s1,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h189]) ).
cnf(h191,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h190]) ).
cnf(h192,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h191]) ).
cnf(h193,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h192]) ).
cnf(h194,plain,
p(s0,s0,s1,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h193]) ).
cnf(h195,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h194]) ).
cnf(h196,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h195]) ).
cnf(h197,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h196]) ).
cnf(h198,plain,
p(s0,s0,s1,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h197]) ).
cnf(h199,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h198]) ).
cnf(h200,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h199]) ).
cnf(h201,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h200]) ).
cnf(h202,plain,
p(s0,s0,s1,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h201]) ).
cnf(h203,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h202]) ).
cnf(h204,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h203]) ).
cnf(h205,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h204]) ).
cnf(h206,plain,
p(s0,s0,s1,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h205]) ).
cnf(h207,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h206]) ).
cnf(h208,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h207]) ).
cnf(h209,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h208]) ).
cnf(h210,plain,
p(s0,s0,s1,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h209]) ).
cnf(h211,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h210]) ).
cnf(h212,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h211]) ).
cnf(h213,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h212]) ).
cnf(h214,plain,
p(s0,s0,s1,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h213]) ).
cnf(h215,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h214]) ).
cnf(h216,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h215]) ).
cnf(h217,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h216]) ).
cnf(h218,plain,
p(s0,s0,s1,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h217]) ).
cnf(h219,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h218]) ).
cnf(h220,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h219]) ).
cnf(h221,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h220]) ).
cnf(h222,plain,
p(s0,s0,s1,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h221]) ).
cnf(h223,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h222]) ).
cnf(h224,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h223]) ).
cnf(h225,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h224]) ).
cnf(h226,plain,
p(s0,s0,s1,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h225]) ).
cnf(h227,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h226]) ).
cnf(h228,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h227]) ).
cnf(h229,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h228]) ).
cnf(h230,plain,
p(s0,s0,s1,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h229]) ).
cnf(h231,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h230]) ).
cnf(h232,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h231]) ).
cnf(h233,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h232]) ).
cnf(h234,plain,
p(s0,s0,s1,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h233]) ).
cnf(h235,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h234]) ).
cnf(h236,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h235]) ).
cnf(h237,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h236]) ).
cnf(h238,plain,
p(s0,s0,s1,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h237]) ).
cnf(h239,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h238]) ).
cnf(h240,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h239]) ).
cnf(h241,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h240]) ).
cnf(h242,plain,
p(s0,s0,s1,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h241]) ).
cnf(h243,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h242]) ).
cnf(h244,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h243]) ).
cnf(h245,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h244]) ).
cnf(h246,plain,
p(s0,s0,s1,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h245]) ).
cnf(h247,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h246]) ).
cnf(h248,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h247]) ).
cnf(h249,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h248]) ).
cnf(h250,plain,
p(s0,s0,s1,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h249]) ).
cnf(h251,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h250]) ).
cnf(h252,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h251]) ).
cnf(h253,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h252]) ).
cnf(h254,plain,
p(s0,s0,s1,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h253]) ).
cnf(f9,axiom,
( p(X0,s1,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,s0,s1,s1,s1,s1,s1,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule9) ).
fof(f9_nnf,plain,
! [X0] :
( p(X0,s1,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,s0,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0] :
( p(X0,s1,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,s0,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( p(X0,s1,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(X0,s0,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi9,axiom,
ifeq(p(X0,s0,s1,s1,s1,s1,s1,s1,s1,s1),true,p(X0,s1,s0,s0,s0,s0,s0,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h255,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi9,h254]) ).
cnf(h256,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h255]) ).
cnf(h257,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h256]) ).
cnf(h258,plain,
p(s0,s1,s0,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h257]) ).
cnf(h259,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h258]) ).
cnf(h260,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h259]) ).
cnf(h261,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h260]) ).
cnf(h262,plain,
p(s0,s1,s0,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h261]) ).
cnf(h263,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h262]) ).
cnf(h264,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h263]) ).
cnf(h265,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h264]) ).
cnf(h266,plain,
p(s0,s1,s0,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h265]) ).
cnf(h267,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h266]) ).
cnf(h268,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h267]) ).
cnf(h269,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h268]) ).
cnf(h270,plain,
p(s0,s1,s0,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h269]) ).
cnf(h271,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h270]) ).
cnf(h272,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h271]) ).
cnf(h273,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h272]) ).
cnf(h274,plain,
p(s0,s1,s0,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h273]) ).
cnf(h275,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h274]) ).
cnf(h276,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h275]) ).
cnf(h277,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h276]) ).
cnf(h278,plain,
p(s0,s1,s0,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h277]) ).
cnf(h279,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h278]) ).
cnf(h280,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h279]) ).
cnf(h281,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h280]) ).
cnf(h282,plain,
p(s0,s1,s0,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h281]) ).
cnf(h283,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h282]) ).
cnf(h284,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h283]) ).
cnf(h285,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h284]) ).
cnf(h286,plain,
p(s0,s1,s0,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h285]) ).
cnf(h287,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h286]) ).
cnf(h288,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h287]) ).
cnf(h289,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h288]) ).
cnf(h290,plain,
p(s0,s1,s0,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h289]) ).
cnf(h291,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h290]) ).
cnf(h292,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h291]) ).
cnf(h293,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h292]) ).
cnf(h294,plain,
p(s0,s1,s0,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h293]) ).
cnf(h295,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h294]) ).
cnf(h296,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h295]) ).
cnf(h297,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h296]) ).
cnf(h298,plain,
p(s0,s1,s0,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h297]) ).
cnf(h299,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h298]) ).
cnf(h300,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h299]) ).
cnf(h301,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h300]) ).
cnf(h302,plain,
p(s0,s1,s0,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h301]) ).
cnf(h303,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h302]) ).
cnf(h304,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h303]) ).
cnf(h305,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h304]) ).
cnf(h306,plain,
p(s0,s1,s0,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h305]) ).
cnf(h307,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h306]) ).
cnf(h308,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h307]) ).
cnf(h309,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h308]) ).
cnf(h310,plain,
p(s0,s1,s0,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h309]) ).
cnf(h311,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h310]) ).
cnf(h312,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h311]) ).
cnf(h313,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h312]) ).
cnf(h314,plain,
p(s0,s1,s0,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h313]) ).
cnf(h315,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h314]) ).
cnf(h316,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h315]) ).
cnf(h317,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h316]) ).
cnf(h318,plain,
p(s0,s1,s0,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h317]) ).
cnf(h319,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h318]) ).
cnf(h320,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h319]) ).
cnf(h321,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h320]) ).
cnf(h322,plain,
p(s0,s1,s0,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h321]) ).
cnf(h323,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h322]) ).
cnf(h324,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h323]) ).
cnf(h325,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h324]) ).
cnf(h326,plain,
p(s0,s1,s0,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h325]) ).
cnf(h327,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h326]) ).
cnf(h328,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h327]) ).
cnf(h329,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h328]) ).
cnf(h330,plain,
p(s0,s1,s0,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h329]) ).
cnf(h331,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h330]) ).
cnf(h332,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h331]) ).
cnf(h333,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h332]) ).
cnf(h334,plain,
p(s0,s1,s0,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h333]) ).
cnf(h335,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h334]) ).
cnf(h336,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h335]) ).
cnf(h337,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h336]) ).
cnf(h338,plain,
p(s0,s1,s0,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h337]) ).
cnf(h339,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h338]) ).
cnf(h340,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h339]) ).
cnf(h341,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h340]) ).
cnf(h342,plain,
p(s0,s1,s0,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h341]) ).
cnf(h343,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h342]) ).
cnf(h344,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h343]) ).
cnf(h345,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h344]) ).
cnf(h346,plain,
p(s0,s1,s0,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h345]) ).
cnf(h347,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h346]) ).
cnf(h348,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h347]) ).
cnf(h349,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h348]) ).
cnf(h350,plain,
p(s0,s1,s0,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h349]) ).
cnf(h351,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h350]) ).
cnf(h352,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h351]) ).
cnf(h353,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h352]) ).
cnf(h354,plain,
p(s0,s1,s0,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h353]) ).
cnf(h355,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h354]) ).
cnf(h356,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h355]) ).
cnf(h357,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h356]) ).
cnf(h358,plain,
p(s0,s1,s0,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h357]) ).
cnf(h359,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h358]) ).
cnf(h360,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h359]) ).
cnf(h361,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h360]) ).
cnf(h362,plain,
p(s0,s1,s0,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h361]) ).
cnf(h363,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h362]) ).
cnf(h364,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h363]) ).
cnf(h365,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h364]) ).
cnf(h366,plain,
p(s0,s1,s0,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h365]) ).
cnf(h367,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h366]) ).
cnf(h368,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h367]) ).
cnf(h369,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h368]) ).
cnf(h370,plain,
p(s0,s1,s0,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h369]) ).
cnf(h371,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h370]) ).
cnf(h372,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h371]) ).
cnf(h373,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h372]) ).
cnf(h374,plain,
p(s0,s1,s0,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h373]) ).
cnf(h375,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h374]) ).
cnf(h376,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h375]) ).
cnf(h377,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h376]) ).
cnf(h378,plain,
p(s0,s1,s0,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h377]) ).
cnf(h379,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h378]) ).
cnf(h380,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h379]) ).
cnf(h381,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h380]) ).
cnf(h382,plain,
p(s0,s1,s0,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h381]) ).
cnf(h383,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi8,h382]) ).
cnf(h384,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h383]) ).
cnf(h385,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h384]) ).
cnf(h386,plain,
p(s0,s1,s1,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h385]) ).
cnf(h387,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h386]) ).
cnf(h388,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h387]) ).
cnf(h389,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h388]) ).
cnf(h390,plain,
p(s0,s1,s1,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h389]) ).
cnf(h391,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h390]) ).
cnf(h392,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h391]) ).
cnf(h393,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h392]) ).
cnf(h394,plain,
p(s0,s1,s1,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h393]) ).
cnf(h395,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h394]) ).
cnf(h396,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h395]) ).
cnf(h397,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h396]) ).
cnf(h398,plain,
p(s0,s1,s1,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h397]) ).
cnf(h399,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h398]) ).
cnf(h400,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h399]) ).
cnf(h401,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h400]) ).
cnf(h402,plain,
p(s0,s1,s1,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h401]) ).
cnf(h403,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h402]) ).
cnf(h404,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h403]) ).
cnf(h405,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h404]) ).
cnf(h406,plain,
p(s0,s1,s1,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h405]) ).
cnf(h407,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h406]) ).
cnf(h408,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h407]) ).
cnf(h409,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h408]) ).
cnf(h410,plain,
p(s0,s1,s1,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h409]) ).
cnf(h411,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h410]) ).
cnf(h412,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h411]) ).
cnf(h413,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h412]) ).
cnf(h414,plain,
p(s0,s1,s1,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h413]) ).
cnf(h415,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h414]) ).
cnf(h416,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h415]) ).
cnf(h417,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h416]) ).
cnf(h418,plain,
p(s0,s1,s1,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h417]) ).
cnf(h419,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h418]) ).
cnf(h420,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h419]) ).
cnf(h421,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h420]) ).
cnf(h422,plain,
p(s0,s1,s1,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h421]) ).
cnf(h423,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h422]) ).
cnf(h424,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h423]) ).
cnf(h425,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h424]) ).
cnf(h426,plain,
p(s0,s1,s1,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h425]) ).
cnf(h427,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h426]) ).
cnf(h428,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h427]) ).
cnf(h429,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h428]) ).
cnf(h430,plain,
p(s0,s1,s1,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h429]) ).
cnf(h431,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h430]) ).
cnf(h432,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h431]) ).
cnf(h433,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h432]) ).
cnf(h434,plain,
p(s0,s1,s1,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h433]) ).
cnf(h435,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h434]) ).
cnf(h436,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h435]) ).
cnf(h437,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h436]) ).
cnf(h438,plain,
p(s0,s1,s1,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h437]) ).
cnf(h439,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h438]) ).
cnf(h440,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h439]) ).
cnf(h441,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h440]) ).
cnf(h442,plain,
p(s0,s1,s1,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h441]) ).
cnf(h443,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h442]) ).
cnf(h444,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h443]) ).
cnf(h445,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h444]) ).
cnf(h446,plain,
p(s0,s1,s1,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h445]) ).
cnf(h447,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h446]) ).
cnf(h448,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h447]) ).
cnf(h449,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h448]) ).
cnf(h450,plain,
p(s0,s1,s1,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h449]) ).
cnf(h451,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h450]) ).
cnf(h452,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h451]) ).
cnf(h453,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h452]) ).
cnf(h454,plain,
p(s0,s1,s1,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h453]) ).
cnf(h455,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h454]) ).
cnf(h456,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h455]) ).
cnf(h457,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h456]) ).
cnf(h458,plain,
p(s0,s1,s1,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h457]) ).
cnf(h459,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h458]) ).
cnf(h460,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h459]) ).
cnf(h461,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h460]) ).
cnf(h462,plain,
p(s0,s1,s1,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h461]) ).
cnf(h463,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h462]) ).
cnf(h464,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h463]) ).
cnf(h465,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h464]) ).
cnf(h466,plain,
p(s0,s1,s1,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h465]) ).
cnf(h467,plain,
p(s0,s1,s1,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h466]) ).
cnf(h468,plain,
p(s0,s1,s1,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h467]) ).
cnf(h469,plain,
p(s0,s1,s1,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h468]) ).
cnf(h470,plain,
p(s0,s1,s1,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h469]) ).
cnf(h471,plain,
p(s0,s1,s1,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h470]) ).
cnf(h472,plain,
p(s0,s1,s1,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h471]) ).
cnf(h473,plain,
p(s0,s1,s1,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h472]) ).
cnf(h474,plain,
p(s0,s1,s1,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h473]) ).
cnf(h475,plain,
p(s0,s1,s1,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h474]) ).
cnf(h476,plain,
p(s0,s1,s1,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h475]) ).
cnf(h477,plain,
p(s0,s1,s1,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h476]) ).
cnf(h478,plain,
p(s0,s1,s1,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h477]) ).
cnf(h479,plain,
p(s0,s1,s1,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h478]) ).
cnf(h480,plain,
p(s0,s1,s1,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h479]) ).
cnf(h481,plain,
p(s0,s1,s1,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h480]) ).
cnf(h482,plain,
p(s0,s1,s1,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h481]) ).
cnf(h483,plain,
p(s0,s1,s1,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h482]) ).
cnf(h484,plain,
p(s0,s1,s1,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h483]) ).
cnf(h485,plain,
p(s0,s1,s1,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h484]) ).
cnf(h486,plain,
p(s0,s1,s1,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h485]) ).
cnf(h487,plain,
p(s0,s1,s1,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h486]) ).
cnf(h488,plain,
p(s0,s1,s1,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h487]) ).
cnf(h489,plain,
p(s0,s1,s1,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h488]) ).
cnf(h490,plain,
p(s0,s1,s1,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h489]) ).
cnf(h491,plain,
p(s0,s1,s1,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h490]) ).
cnf(h492,plain,
p(s0,s1,s1,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h491]) ).
cnf(h493,plain,
p(s0,s1,s1,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h492]) ).
cnf(h494,plain,
p(s0,s1,s1,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h493]) ).
cnf(h495,plain,
p(s0,s1,s1,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h494]) ).
cnf(h496,plain,
p(s0,s1,s1,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h495]) ).
cnf(h497,plain,
p(s0,s1,s1,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h496]) ).
cnf(h498,plain,
p(s0,s1,s1,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h497]) ).
cnf(h499,plain,
p(s0,s1,s1,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h498]) ).
cnf(h500,plain,
p(s0,s1,s1,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h499]) ).
cnf(h501,plain,
p(s0,s1,s1,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h500]) ).
cnf(h502,plain,
p(s0,s1,s1,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h501]) ).
cnf(h503,plain,
p(s0,s1,s1,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h502]) ).
cnf(h504,plain,
p(s0,s1,s1,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h503]) ).
cnf(h505,plain,
p(s0,s1,s1,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h504]) ).
cnf(h506,plain,
p(s0,s1,s1,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h505]) ).
cnf(h507,plain,
p(s0,s1,s1,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h506]) ).
cnf(h508,plain,
p(s0,s1,s1,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h507]) ).
cnf(h509,plain,
p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h508]) ).
cnf(h510,plain,
p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h509]) ).
cnf(f10,axiom,
( p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule10) ).
fof(f10_nnf,plain,
( p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0)
| ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi10,axiom,
ifeq(p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1),true,p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(h511,plain,
p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi10,h510]) ).
cnf(h512,plain,
p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h511]) ).
cnf(h513,plain,
p(s1,s0,s0,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h512]) ).
cnf(h514,plain,
p(s1,s0,s0,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h513]) ).
cnf(h515,plain,
p(s1,s0,s0,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h514]) ).
cnf(h516,plain,
p(s1,s0,s0,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h515]) ).
cnf(h517,plain,
p(s1,s0,s0,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h516]) ).
cnf(h518,plain,
p(s1,s0,s0,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h517]) ).
cnf(h519,plain,
p(s1,s0,s0,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h518]) ).
cnf(h520,plain,
p(s1,s0,s0,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h519]) ).
cnf(h521,plain,
p(s1,s0,s0,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h520]) ).
cnf(h522,plain,
p(s1,s0,s0,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h521]) ).
cnf(h523,plain,
p(s1,s0,s0,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h522]) ).
cnf(h524,plain,
p(s1,s0,s0,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h523]) ).
cnf(h525,plain,
p(s1,s0,s0,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h524]) ).
cnf(h526,plain,
p(s1,s0,s0,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h525]) ).
cnf(h527,plain,
p(s1,s0,s0,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h526]) ).
cnf(h528,plain,
p(s1,s0,s0,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h527]) ).
cnf(h529,plain,
p(s1,s0,s0,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h528]) ).
cnf(h530,plain,
p(s1,s0,s0,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h529]) ).
cnf(h531,plain,
p(s1,s0,s0,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h530]) ).
cnf(h532,plain,
p(s1,s0,s0,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h531]) ).
cnf(h533,plain,
p(s1,s0,s0,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h532]) ).
cnf(h534,plain,
p(s1,s0,s0,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h533]) ).
cnf(h535,plain,
p(s1,s0,s0,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h534]) ).
cnf(h536,plain,
p(s1,s0,s0,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h535]) ).
cnf(h537,plain,
p(s1,s0,s0,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h536]) ).
cnf(h538,plain,
p(s1,s0,s0,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h537]) ).
cnf(h539,plain,
p(s1,s0,s0,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h538]) ).
cnf(h540,plain,
p(s1,s0,s0,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h539]) ).
cnf(h541,plain,
p(s1,s0,s0,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h540]) ).
cnf(h542,plain,
p(s1,s0,s0,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h541]) ).
cnf(h543,plain,
p(s1,s0,s0,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h542]) ).
cnf(h544,plain,
p(s1,s0,s0,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h543]) ).
cnf(h545,plain,
p(s1,s0,s0,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h544]) ).
cnf(h546,plain,
p(s1,s0,s0,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h545]) ).
cnf(h547,plain,
p(s1,s0,s0,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h546]) ).
cnf(h548,plain,
p(s1,s0,s0,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h547]) ).
cnf(h549,plain,
p(s1,s0,s0,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h548]) ).
cnf(h550,plain,
p(s1,s0,s0,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h549]) ).
cnf(h551,plain,
p(s1,s0,s0,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h550]) ).
cnf(h552,plain,
p(s1,s0,s0,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h551]) ).
cnf(h553,plain,
p(s1,s0,s0,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h552]) ).
cnf(h554,plain,
p(s1,s0,s0,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h553]) ).
cnf(h555,plain,
p(s1,s0,s0,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h554]) ).
cnf(h556,plain,
p(s1,s0,s0,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h555]) ).
cnf(h557,plain,
p(s1,s0,s0,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h556]) ).
cnf(h558,plain,
p(s1,s0,s0,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h557]) ).
cnf(h559,plain,
p(s1,s0,s0,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h558]) ).
cnf(h560,plain,
p(s1,s0,s0,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h559]) ).
cnf(h561,plain,
p(s1,s0,s0,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h560]) ).
cnf(h562,plain,
p(s1,s0,s0,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h561]) ).
cnf(h563,plain,
p(s1,s0,s0,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h562]) ).
cnf(h564,plain,
p(s1,s0,s0,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h563]) ).
cnf(h565,plain,
p(s1,s0,s0,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h564]) ).
cnf(h566,plain,
p(s1,s0,s0,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h565]) ).
cnf(h567,plain,
p(s1,s0,s0,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h566]) ).
cnf(h568,plain,
p(s1,s0,s0,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h567]) ).
cnf(h569,plain,
p(s1,s0,s0,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h568]) ).
cnf(h570,plain,
p(s1,s0,s0,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h569]) ).
cnf(h571,plain,
p(s1,s0,s0,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h570]) ).
cnf(h572,plain,
p(s1,s0,s0,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h571]) ).
cnf(h573,plain,
p(s1,s0,s0,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h572]) ).
cnf(h574,plain,
p(s1,s0,s0,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h573]) ).
cnf(h575,plain,
p(s1,s0,s0,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h574]) ).
cnf(h576,plain,
p(s1,s0,s0,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h575]) ).
cnf(h577,plain,
p(s1,s0,s0,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h576]) ).
cnf(h578,plain,
p(s1,s0,s0,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h577]) ).
cnf(h579,plain,
p(s1,s0,s0,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h578]) ).
cnf(h580,plain,
p(s1,s0,s0,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h579]) ).
cnf(h581,plain,
p(s1,s0,s0,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h580]) ).
cnf(h582,plain,
p(s1,s0,s0,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h581]) ).
cnf(h583,plain,
p(s1,s0,s0,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h582]) ).
cnf(h584,plain,
p(s1,s0,s0,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h583]) ).
cnf(h585,plain,
p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h584]) ).
cnf(h586,plain,
p(s1,s0,s0,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h585]) ).
cnf(h587,plain,
p(s1,s0,s0,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h586]) ).
cnf(h588,plain,
p(s1,s0,s0,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h587]) ).
cnf(h589,plain,
p(s1,s0,s0,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h588]) ).
cnf(h590,plain,
p(s1,s0,s0,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h589]) ).
cnf(h591,plain,
p(s1,s0,s0,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h590]) ).
cnf(h592,plain,
p(s1,s0,s0,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h591]) ).
cnf(h593,plain,
p(s1,s0,s0,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h592]) ).
cnf(h594,plain,
p(s1,s0,s0,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h593]) ).
cnf(h595,plain,
p(s1,s0,s0,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h594]) ).
cnf(h596,plain,
p(s1,s0,s0,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h595]) ).
cnf(h597,plain,
p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h596]) ).
cnf(h598,plain,
p(s1,s0,s0,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h597]) ).
cnf(h599,plain,
p(s1,s0,s0,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h598]) ).
cnf(h600,plain,
p(s1,s0,s0,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h599]) ).
cnf(h601,plain,
p(s1,s0,s0,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h600]) ).
cnf(h602,plain,
p(s1,s0,s0,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h601]) ).
cnf(h603,plain,
p(s1,s0,s0,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h602]) ).
cnf(h604,plain,
p(s1,s0,s0,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h603]) ).
cnf(h605,plain,
p(s1,s0,s0,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h604]) ).
cnf(h606,plain,
p(s1,s0,s0,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h605]) ).
cnf(h607,plain,
p(s1,s0,s0,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h606]) ).
cnf(h608,plain,
p(s1,s0,s0,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h607]) ).
cnf(h609,plain,
p(s1,s0,s0,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h608]) ).
cnf(h610,plain,
p(s1,s0,s0,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h609]) ).
cnf(h611,plain,
p(s1,s0,s0,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h610]) ).
cnf(h612,plain,
p(s1,s0,s0,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h611]) ).
cnf(h613,plain,
p(s1,s0,s0,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h612]) ).
cnf(h614,plain,
p(s1,s0,s0,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h613]) ).
cnf(h615,plain,
p(s1,s0,s0,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h614]) ).
cnf(h616,plain,
p(s1,s0,s0,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h615]) ).
cnf(h617,plain,
p(s1,s0,s0,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h616]) ).
cnf(h618,plain,
p(s1,s0,s0,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h617]) ).
cnf(h619,plain,
p(s1,s0,s0,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h618]) ).
cnf(h620,plain,
p(s1,s0,s0,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h619]) ).
cnf(h621,plain,
p(s1,s0,s0,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h620]) ).
cnf(h622,plain,
p(s1,s0,s0,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h621]) ).
cnf(h623,plain,
p(s1,s0,s0,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h622]) ).
cnf(h624,plain,
p(s1,s0,s0,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h623]) ).
cnf(h625,plain,
p(s1,s0,s0,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h624]) ).
cnf(h626,plain,
p(s1,s0,s0,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h625]) ).
cnf(h627,plain,
p(s1,s0,s0,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h626]) ).
cnf(h628,plain,
p(s1,s0,s0,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h627]) ).
cnf(h629,plain,
p(s1,s0,s0,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h628]) ).
cnf(h630,plain,
p(s1,s0,s0,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h629]) ).
cnf(h631,plain,
p(s1,s0,s0,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h630]) ).
cnf(h632,plain,
p(s1,s0,s0,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h631]) ).
cnf(h633,plain,
p(s1,s0,s0,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h632]) ).
cnf(h634,plain,
p(s1,s0,s0,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h633]) ).
cnf(h635,plain,
p(s1,s0,s0,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h634]) ).
cnf(h636,plain,
p(s1,s0,s0,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h635]) ).
cnf(h637,plain,
p(s1,s0,s0,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h636]) ).
cnf(h638,plain,
p(s1,s0,s0,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h637]) ).
cnf(h639,plain,
p(s1,s0,s1,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi8,h638]) ).
cnf(h640,plain,
p(s1,s0,s1,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h639]) ).
cnf(h641,plain,
p(s1,s0,s1,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h640]) ).
cnf(h642,plain,
p(s1,s0,s1,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h641]) ).
cnf(h643,plain,
p(s1,s0,s1,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h642]) ).
cnf(h644,plain,
p(s1,s0,s1,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h643]) ).
cnf(h645,plain,
p(s1,s0,s1,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h644]) ).
cnf(h646,plain,
p(s1,s0,s1,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h645]) ).
cnf(h647,plain,
p(s1,s0,s1,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h646]) ).
cnf(h648,plain,
p(s1,s0,s1,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h647]) ).
cnf(h649,plain,
p(s1,s0,s1,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h648]) ).
cnf(h650,plain,
p(s1,s0,s1,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h649]) ).
cnf(h651,plain,
p(s1,s0,s1,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h650]) ).
cnf(h652,plain,
p(s1,s0,s1,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h651]) ).
cnf(h653,plain,
p(s1,s0,s1,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h652]) ).
cnf(h654,plain,
p(s1,s0,s1,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h653]) ).
cnf(h655,plain,
p(s1,s0,s1,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h654]) ).
cnf(h656,plain,
p(s1,s0,s1,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h655]) ).
cnf(h657,plain,
p(s1,s0,s1,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h656]) ).
cnf(h658,plain,
p(s1,s0,s1,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h657]) ).
cnf(h659,plain,
p(s1,s0,s1,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h658]) ).
cnf(h660,plain,
p(s1,s0,s1,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h659]) ).
cnf(h661,plain,
p(s1,s0,s1,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h660]) ).
cnf(h662,plain,
p(s1,s0,s1,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h661]) ).
cnf(h663,plain,
p(s1,s0,s1,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h662]) ).
cnf(h664,plain,
p(s1,s0,s1,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h663]) ).
cnf(h665,plain,
p(s1,s0,s1,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h664]) ).
cnf(h666,plain,
p(s1,s0,s1,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h665]) ).
cnf(h667,plain,
p(s1,s0,s1,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h666]) ).
cnf(h668,plain,
p(s1,s0,s1,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h667]) ).
cnf(h669,plain,
p(s1,s0,s1,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h668]) ).
cnf(h670,plain,
p(s1,s0,s1,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h669]) ).
cnf(h671,plain,
p(s1,s0,s1,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h670]) ).
cnf(h672,plain,
p(s1,s0,s1,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h671]) ).
cnf(h673,plain,
p(s1,s0,s1,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h672]) ).
cnf(h674,plain,
p(s1,s0,s1,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h673]) ).
cnf(h675,plain,
p(s1,s0,s1,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h674]) ).
cnf(h676,plain,
p(s1,s0,s1,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h675]) ).
cnf(h677,plain,
p(s1,s0,s1,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h676]) ).
cnf(h678,plain,
p(s1,s0,s1,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h677]) ).
cnf(h679,plain,
p(s1,s0,s1,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h678]) ).
cnf(h680,plain,
p(s1,s0,s1,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h679]) ).
cnf(h681,plain,
p(s1,s0,s1,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h680]) ).
cnf(h682,plain,
p(s1,s0,s1,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h681]) ).
cnf(h683,plain,
p(s1,s0,s1,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h682]) ).
cnf(h684,plain,
p(s1,s0,s1,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h683]) ).
cnf(h685,plain,
p(s1,s0,s1,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h684]) ).
cnf(h686,plain,
p(s1,s0,s1,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h685]) ).
cnf(h687,plain,
p(s1,s0,s1,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h686]) ).
cnf(h688,plain,
p(s1,s0,s1,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h687]) ).
cnf(h689,plain,
p(s1,s0,s1,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h688]) ).
cnf(h690,plain,
p(s1,s0,s1,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h689]) ).
cnf(h691,plain,
p(s1,s0,s1,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h690]) ).
cnf(h692,plain,
p(s1,s0,s1,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h691]) ).
cnf(h693,plain,
p(s1,s0,s1,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h692]) ).
cnf(h694,plain,
p(s1,s0,s1,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h693]) ).
cnf(h695,plain,
p(s1,s0,s1,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h694]) ).
cnf(h696,plain,
p(s1,s0,s1,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h695]) ).
cnf(h697,plain,
p(s1,s0,s1,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h696]) ).
cnf(h698,plain,
p(s1,s0,s1,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h697]) ).
cnf(h699,plain,
p(s1,s0,s1,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h698]) ).
cnf(h700,plain,
p(s1,s0,s1,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h699]) ).
cnf(h701,plain,
p(s1,s0,s1,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h700]) ).
cnf(h702,plain,
p(s1,s0,s1,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h701]) ).
cnf(h703,plain,
p(s1,s0,s1,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h702]) ).
cnf(h704,plain,
p(s1,s0,s1,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h703]) ).
cnf(h705,plain,
p(s1,s0,s1,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h704]) ).
cnf(h706,plain,
p(s1,s0,s1,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h705]) ).
cnf(h707,plain,
p(s1,s0,s1,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h706]) ).
cnf(h708,plain,
p(s1,s0,s1,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h707]) ).
cnf(h709,plain,
p(s1,s0,s1,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h708]) ).
cnf(h710,plain,
p(s1,s0,s1,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h709]) ).
cnf(h711,plain,
p(s1,s0,s1,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h710]) ).
cnf(h712,plain,
p(s1,s0,s1,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h711]) ).
cnf(h713,plain,
p(s1,s0,s1,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h712]) ).
cnf(h714,plain,
p(s1,s0,s1,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h713]) ).
cnf(h715,plain,
p(s1,s0,s1,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h714]) ).
cnf(h716,plain,
p(s1,s0,s1,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h715]) ).
cnf(h717,plain,
p(s1,s0,s1,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h716]) ).
cnf(h718,plain,
p(s1,s0,s1,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h717]) ).
cnf(h719,plain,
p(s1,s0,s1,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h718]) ).
cnf(h720,plain,
p(s1,s0,s1,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h719]) ).
cnf(h721,plain,
p(s1,s0,s1,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h720]) ).
cnf(h722,plain,
p(s1,s0,s1,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h721]) ).
cnf(h723,plain,
p(s1,s0,s1,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h722]) ).
cnf(h724,plain,
p(s1,s0,s1,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h723]) ).
cnf(h725,plain,
p(s1,s0,s1,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h724]) ).
cnf(h726,plain,
p(s1,s0,s1,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h725]) ).
cnf(h727,plain,
p(s1,s0,s1,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h726]) ).
cnf(h728,plain,
p(s1,s0,s1,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h727]) ).
cnf(h729,plain,
p(s1,s0,s1,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h728]) ).
cnf(h730,plain,
p(s1,s0,s1,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h729]) ).
cnf(h731,plain,
p(s1,s0,s1,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h730]) ).
cnf(h732,plain,
p(s1,s0,s1,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h731]) ).
cnf(h733,plain,
p(s1,s0,s1,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h732]) ).
cnf(h734,plain,
p(s1,s0,s1,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h733]) ).
cnf(h735,plain,
p(s1,s0,s1,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h734]) ).
cnf(h736,plain,
p(s1,s0,s1,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h735]) ).
cnf(h737,plain,
p(s1,s0,s1,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h736]) ).
cnf(h738,plain,
p(s1,s0,s1,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h737]) ).
cnf(h739,plain,
p(s1,s0,s1,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h738]) ).
cnf(h740,plain,
p(s1,s0,s1,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h739]) ).
cnf(h741,plain,
p(s1,s0,s1,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h740]) ).
cnf(h742,plain,
p(s1,s0,s1,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h741]) ).
cnf(h743,plain,
p(s1,s0,s1,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h742]) ).
cnf(h744,plain,
p(s1,s0,s1,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h743]) ).
cnf(h745,plain,
p(s1,s0,s1,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h744]) ).
cnf(h746,plain,
p(s1,s0,s1,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h745]) ).
cnf(h747,plain,
p(s1,s0,s1,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h746]) ).
cnf(h748,plain,
p(s1,s0,s1,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h747]) ).
cnf(h749,plain,
p(s1,s0,s1,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h748]) ).
cnf(h750,plain,
p(s1,s0,s1,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h749]) ).
cnf(h751,plain,
p(s1,s0,s1,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h750]) ).
cnf(h752,plain,
p(s1,s0,s1,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h751]) ).
cnf(h753,plain,
p(s1,s0,s1,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h752]) ).
cnf(h754,plain,
p(s1,s0,s1,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h753]) ).
cnf(h755,plain,
p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h754]) ).
cnf(h756,plain,
p(s1,s0,s1,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h755]) ).
cnf(h757,plain,
p(s1,s0,s1,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h756]) ).
cnf(h758,plain,
p(s1,s0,s1,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h757]) ).
cnf(h759,plain,
p(s1,s0,s1,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h758]) ).
cnf(h760,plain,
p(s1,s0,s1,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h759]) ).
cnf(h761,plain,
p(s1,s0,s1,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h760]) ).
cnf(h762,plain,
p(s1,s0,s1,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h761]) ).
cnf(h763,plain,
p(s1,s0,s1,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h762]) ).
cnf(h764,plain,
p(s1,s0,s1,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h763]) ).
cnf(h765,plain,
p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h764]) ).
cnf(h766,plain,
p(s1,s0,s1,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h765]) ).
cnf(h767,plain,
p(s1,s1,s0,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi9,h766]) ).
cnf(h768,plain,
p(s1,s1,s0,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h767]) ).
cnf(h769,plain,
p(s1,s1,s0,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h768]) ).
cnf(h770,plain,
p(s1,s1,s0,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h769]) ).
cnf(h771,plain,
p(s1,s1,s0,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h770]) ).
cnf(h772,plain,
p(s1,s1,s0,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h771]) ).
cnf(h773,plain,
p(s1,s1,s0,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h772]) ).
cnf(h774,plain,
p(s1,s1,s0,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h773]) ).
cnf(h775,plain,
p(s1,s1,s0,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h774]) ).
cnf(h776,plain,
p(s1,s1,s0,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h775]) ).
cnf(h777,plain,
p(s1,s1,s0,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h776]) ).
cnf(h778,plain,
p(s1,s1,s0,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h777]) ).
cnf(h779,plain,
p(s1,s1,s0,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h778]) ).
cnf(h780,plain,
p(s1,s1,s0,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h779]) ).
cnf(h781,plain,
p(s1,s1,s0,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h780]) ).
cnf(h782,plain,
p(s1,s1,s0,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h781]) ).
cnf(h783,plain,
p(s1,s1,s0,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h782]) ).
cnf(h784,plain,
p(s1,s1,s0,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h783]) ).
cnf(h785,plain,
p(s1,s1,s0,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h784]) ).
cnf(h786,plain,
p(s1,s1,s0,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h785]) ).
cnf(h787,plain,
p(s1,s1,s0,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h786]) ).
cnf(h788,plain,
p(s1,s1,s0,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h787]) ).
cnf(h789,plain,
p(s1,s1,s0,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h788]) ).
cnf(h790,plain,
p(s1,s1,s0,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h789]) ).
cnf(h791,plain,
p(s1,s1,s0,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h790]) ).
cnf(h792,plain,
p(s1,s1,s0,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h791]) ).
cnf(h793,plain,
p(s1,s1,s0,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h792]) ).
cnf(h794,plain,
p(s1,s1,s0,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h793]) ).
cnf(h795,plain,
p(s1,s1,s0,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h794]) ).
cnf(h796,plain,
p(s1,s1,s0,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h795]) ).
cnf(h797,plain,
p(s1,s1,s0,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h796]) ).
cnf(h798,plain,
p(s1,s1,s0,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h797]) ).
cnf(h799,plain,
p(s1,s1,s0,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h798]) ).
cnf(h800,plain,
p(s1,s1,s0,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h799]) ).
cnf(h801,plain,
p(s1,s1,s0,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h800]) ).
cnf(h802,plain,
p(s1,s1,s0,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h801]) ).
cnf(h803,plain,
p(s1,s1,s0,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h802]) ).
cnf(h804,plain,
p(s1,s1,s0,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h803]) ).
cnf(h805,plain,
p(s1,s1,s0,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h804]) ).
cnf(h806,plain,
p(s1,s1,s0,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h805]) ).
cnf(h807,plain,
p(s1,s1,s0,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h806]) ).
cnf(h808,plain,
p(s1,s1,s0,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h807]) ).
cnf(h809,plain,
p(s1,s1,s0,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h808]) ).
cnf(h810,plain,
p(s1,s1,s0,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h809]) ).
cnf(h811,plain,
p(s1,s1,s0,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h810]) ).
cnf(h812,plain,
p(s1,s1,s0,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h811]) ).
cnf(h813,plain,
p(s1,s1,s0,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h812]) ).
cnf(h814,plain,
p(s1,s1,s0,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h813]) ).
cnf(h815,plain,
p(s1,s1,s0,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h814]) ).
cnf(h816,plain,
p(s1,s1,s0,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h815]) ).
cnf(h817,plain,
p(s1,s1,s0,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h816]) ).
cnf(h818,plain,
p(s1,s1,s0,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h817]) ).
cnf(h819,plain,
p(s1,s1,s0,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h818]) ).
cnf(h820,plain,
p(s1,s1,s0,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h819]) ).
cnf(h821,plain,
p(s1,s1,s0,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h820]) ).
cnf(h822,plain,
p(s1,s1,s0,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h821]) ).
cnf(h823,plain,
p(s1,s1,s0,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h822]) ).
cnf(h824,plain,
p(s1,s1,s0,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h823]) ).
cnf(h825,plain,
p(s1,s1,s0,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h824]) ).
cnf(h826,plain,
p(s1,s1,s0,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h825]) ).
cnf(h827,plain,
p(s1,s1,s0,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h826]) ).
cnf(h828,plain,
p(s1,s1,s0,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h827]) ).
cnf(h829,plain,
p(s1,s1,s0,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h828]) ).
cnf(h830,plain,
p(s1,s1,s0,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h829]) ).
cnf(h831,plain,
p(s1,s1,s0,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h830]) ).
cnf(h832,plain,
p(s1,s1,s0,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h831]) ).
cnf(h833,plain,
p(s1,s1,s0,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h832]) ).
cnf(h834,plain,
p(s1,s1,s0,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h833]) ).
cnf(h835,plain,
p(s1,s1,s0,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h834]) ).
cnf(h836,plain,
p(s1,s1,s0,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h835]) ).
cnf(h837,plain,
p(s1,s1,s0,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h836]) ).
cnf(h838,plain,
p(s1,s1,s0,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h837]) ).
cnf(h839,plain,
p(s1,s1,s0,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h838]) ).
cnf(h840,plain,
p(s1,s1,s0,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h839]) ).
cnf(h841,plain,
p(s1,s1,s0,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h840]) ).
cnf(h842,plain,
p(s1,s1,s0,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h841]) ).
cnf(h843,plain,
p(s1,s1,s0,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h842]) ).
cnf(h844,plain,
p(s1,s1,s0,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h843]) ).
cnf(h845,plain,
p(s1,s1,s0,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h844]) ).
cnf(h846,plain,
p(s1,s1,s0,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h845]) ).
cnf(h847,plain,
p(s1,s1,s0,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h846]) ).
cnf(h848,plain,
p(s1,s1,s0,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h847]) ).
cnf(h849,plain,
p(s1,s1,s0,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h848]) ).
cnf(h850,plain,
p(s1,s1,s0,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h849]) ).
cnf(h851,plain,
p(s1,s1,s0,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h850]) ).
cnf(h852,plain,
p(s1,s1,s0,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h851]) ).
cnf(h853,plain,
p(s1,s1,s0,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h852]) ).
cnf(h854,plain,
p(s1,s1,s0,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h853]) ).
cnf(h855,plain,
p(s1,s1,s0,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h854]) ).
cnf(h856,plain,
p(s1,s1,s0,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h855]) ).
cnf(h857,plain,
p(s1,s1,s0,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h856]) ).
cnf(h858,plain,
p(s1,s1,s0,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h857]) ).
cnf(h859,plain,
p(s1,s1,s0,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h858]) ).
cnf(h860,plain,
p(s1,s1,s0,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h859]) ).
cnf(h861,plain,
p(s1,s1,s0,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h860]) ).
cnf(h862,plain,
p(s1,s1,s0,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h861]) ).
cnf(h863,plain,
p(s1,s1,s0,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h862]) ).
cnf(h864,plain,
p(s1,s1,s0,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h863]) ).
cnf(h865,plain,
p(s1,s1,s0,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h864]) ).
cnf(h866,plain,
p(s1,s1,s0,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h865]) ).
cnf(h867,plain,
p(s1,s1,s0,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h866]) ).
cnf(h868,plain,
p(s1,s1,s0,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h867]) ).
cnf(h869,plain,
p(s1,s1,s0,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h868]) ).
cnf(h870,plain,
p(s1,s1,s0,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h869]) ).
cnf(h871,plain,
p(s1,s1,s0,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h870]) ).
cnf(h872,plain,
p(s1,s1,s0,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h871]) ).
cnf(h873,plain,
p(s1,s1,s0,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h872]) ).
cnf(h874,plain,
p(s1,s1,s0,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h873]) ).
cnf(h875,plain,
p(s1,s1,s0,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h874]) ).
cnf(h876,plain,
p(s1,s1,s0,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h875]) ).
cnf(h877,plain,
p(s1,s1,s0,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h876]) ).
cnf(h878,plain,
p(s1,s1,s0,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h877]) ).
cnf(h879,plain,
p(s1,s1,s0,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h878]) ).
cnf(h880,plain,
p(s1,s1,s0,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h879]) ).
cnf(h881,plain,
p(s1,s1,s0,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h880]) ).
cnf(h882,plain,
p(s1,s1,s0,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h881]) ).
cnf(h883,plain,
p(s1,s1,s0,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h882]) ).
cnf(h884,plain,
p(s1,s1,s0,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h883]) ).
cnf(h885,plain,
p(s1,s1,s0,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h884]) ).
cnf(h886,plain,
p(s1,s1,s0,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h885]) ).
cnf(h887,plain,
p(s1,s1,s0,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h886]) ).
cnf(h888,plain,
p(s1,s1,s0,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h887]) ).
cnf(h889,plain,
p(s1,s1,s0,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h888]) ).
cnf(h890,plain,
p(s1,s1,s0,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h889]) ).
cnf(h891,plain,
p(s1,s1,s0,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h890]) ).
cnf(h892,plain,
p(s1,s1,s0,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h891]) ).
cnf(h893,plain,
p(s1,s1,s0,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h892]) ).
cnf(h894,plain,
p(s1,s1,s0,s1,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h893]) ).
cnf(h895,plain,
p(s1,s1,s1,s0,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi8,h894]) ).
cnf(h896,plain,
p(s1,s1,s1,s0,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h895]) ).
cnf(h897,plain,
p(s1,s1,s1,s0,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h896]) ).
cnf(h898,plain,
p(s1,s1,s1,s0,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h897]) ).
cnf(h899,plain,
p(s1,s1,s1,s0,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h898]) ).
cnf(h900,plain,
p(s1,s1,s1,s0,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h899]) ).
cnf(h901,plain,
p(s1,s1,s1,s0,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h900]) ).
cnf(h902,plain,
p(s1,s1,s1,s0,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h901]) ).
cnf(h903,plain,
p(s1,s1,s1,s0,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h902]) ).
cnf(h904,plain,
p(s1,s1,s1,s0,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h903]) ).
cnf(h905,plain,
p(s1,s1,s1,s0,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h904]) ).
cnf(h906,plain,
p(s1,s1,s1,s0,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h905]) ).
cnf(h907,plain,
p(s1,s1,s1,s0,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h906]) ).
cnf(h908,plain,
p(s1,s1,s1,s0,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h907]) ).
cnf(h909,plain,
p(s1,s1,s1,s0,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h908]) ).
cnf(h910,plain,
p(s1,s1,s1,s0,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h909]) ).
cnf(h911,plain,
p(s1,s1,s1,s0,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h910]) ).
cnf(h912,plain,
p(s1,s1,s1,s0,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h911]) ).
cnf(h913,plain,
p(s1,s1,s1,s0,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h912]) ).
cnf(h914,plain,
p(s1,s1,s1,s0,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h913]) ).
cnf(h915,plain,
p(s1,s1,s1,s0,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h914]) ).
cnf(h916,plain,
p(s1,s1,s1,s0,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h915]) ).
cnf(h917,plain,
p(s1,s1,s1,s0,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h916]) ).
cnf(h918,plain,
p(s1,s1,s1,s0,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h917]) ).
cnf(h919,plain,
p(s1,s1,s1,s0,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h918]) ).
cnf(h920,plain,
p(s1,s1,s1,s0,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h919]) ).
cnf(h921,plain,
p(s1,s1,s1,s0,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h920]) ).
cnf(h922,plain,
p(s1,s1,s1,s0,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h921]) ).
cnf(h923,plain,
p(s1,s1,s1,s0,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h922]) ).
cnf(h924,plain,
p(s1,s1,s1,s0,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h923]) ).
cnf(h925,plain,
p(s1,s1,s1,s0,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h924]) ).
cnf(h926,plain,
p(s1,s1,s1,s0,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h925]) ).
cnf(h927,plain,
p(s1,s1,s1,s0,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h926]) ).
cnf(h928,plain,
p(s1,s1,s1,s0,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h927]) ).
cnf(h929,plain,
p(s1,s1,s1,s0,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h928]) ).
cnf(h930,plain,
p(s1,s1,s1,s0,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h929]) ).
cnf(h931,plain,
p(s1,s1,s1,s0,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h930]) ).
cnf(h932,plain,
p(s1,s1,s1,s0,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h931]) ).
cnf(h933,plain,
p(s1,s1,s1,s0,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h932]) ).
cnf(h934,plain,
p(s1,s1,s1,s0,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h933]) ).
cnf(h935,plain,
p(s1,s1,s1,s0,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h934]) ).
cnf(h936,plain,
p(s1,s1,s1,s0,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h935]) ).
cnf(h937,plain,
p(s1,s1,s1,s0,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h936]) ).
cnf(h938,plain,
p(s1,s1,s1,s0,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h937]) ).
cnf(h939,plain,
p(s1,s1,s1,s0,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h938]) ).
cnf(h940,plain,
p(s1,s1,s1,s0,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h939]) ).
cnf(h941,plain,
p(s1,s1,s1,s0,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h940]) ).
cnf(h942,plain,
p(s1,s1,s1,s0,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h941]) ).
cnf(h943,plain,
p(s1,s1,s1,s0,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h942]) ).
cnf(h944,plain,
p(s1,s1,s1,s0,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h943]) ).
cnf(h945,plain,
p(s1,s1,s1,s0,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h944]) ).
cnf(h946,plain,
p(s1,s1,s1,s0,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h945]) ).
cnf(h947,plain,
p(s1,s1,s1,s0,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h946]) ).
cnf(h948,plain,
p(s1,s1,s1,s0,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h947]) ).
cnf(h949,plain,
p(s1,s1,s1,s0,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h948]) ).
cnf(h950,plain,
p(s1,s1,s1,s0,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h949]) ).
cnf(h951,plain,
p(s1,s1,s1,s0,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h950]) ).
cnf(h952,plain,
p(s1,s1,s1,s0,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h951]) ).
cnf(h953,plain,
p(s1,s1,s1,s0,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h952]) ).
cnf(h954,plain,
p(s1,s1,s1,s0,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h953]) ).
cnf(h955,plain,
p(s1,s1,s1,s0,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h954]) ).
cnf(h956,plain,
p(s1,s1,s1,s0,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h955]) ).
cnf(h957,plain,
p(s1,s1,s1,s0,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h956]) ).
cnf(h958,plain,
p(s1,s1,s1,s0,s1,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h957]) ).
cnf(h959,plain,
p(s1,s1,s1,s1,s0,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi7,h958]) ).
cnf(h960,plain,
p(s1,s1,s1,s1,s0,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h959]) ).
cnf(h961,plain,
p(s1,s1,s1,s1,s0,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h960]) ).
cnf(h962,plain,
p(s1,s1,s1,s1,s0,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h961]) ).
cnf(h963,plain,
p(s1,s1,s1,s1,s0,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h962]) ).
cnf(h964,plain,
p(s1,s1,s1,s1,s0,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h963]) ).
cnf(h965,plain,
p(s1,s1,s1,s1,s0,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h964]) ).
cnf(h966,plain,
p(s1,s1,s1,s1,s0,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h965]) ).
cnf(h967,plain,
p(s1,s1,s1,s1,s0,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h966]) ).
cnf(h968,plain,
p(s1,s1,s1,s1,s0,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h967]) ).
cnf(h969,plain,
p(s1,s1,s1,s1,s0,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h968]) ).
cnf(h970,plain,
p(s1,s1,s1,s1,s0,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h969]) ).
cnf(h971,plain,
p(s1,s1,s1,s1,s0,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h970]) ).
cnf(h972,plain,
p(s1,s1,s1,s1,s0,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h971]) ).
cnf(h973,plain,
p(s1,s1,s1,s1,s0,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h972]) ).
cnf(h974,plain,
p(s1,s1,s1,s1,s0,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h973]) ).
cnf(h975,plain,
p(s1,s1,s1,s1,s0,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h974]) ).
cnf(h976,plain,
p(s1,s1,s1,s1,s0,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h975]) ).
cnf(h977,plain,
p(s1,s1,s1,s1,s0,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h976]) ).
cnf(h978,plain,
p(s1,s1,s1,s1,s0,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h977]) ).
cnf(h979,plain,
p(s1,s1,s1,s1,s0,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h978]) ).
cnf(h980,plain,
p(s1,s1,s1,s1,s0,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h979]) ).
cnf(h981,plain,
p(s1,s1,s1,s1,s0,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h980]) ).
cnf(h982,plain,
p(s1,s1,s1,s1,s0,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h981]) ).
cnf(h983,plain,
p(s1,s1,s1,s1,s0,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h982]) ).
cnf(h984,plain,
p(s1,s1,s1,s1,s0,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h983]) ).
cnf(h985,plain,
p(s1,s1,s1,s1,s0,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h984]) ).
cnf(h986,plain,
p(s1,s1,s1,s1,s0,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h985]) ).
cnf(h987,plain,
p(s1,s1,s1,s1,s0,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h986]) ).
cnf(h988,plain,
p(s1,s1,s1,s1,s0,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h987]) ).
cnf(h989,plain,
p(s1,s1,s1,s1,s0,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h988]) ).
cnf(h990,plain,
p(s1,s1,s1,s1,s0,s1,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h989]) ).
cnf(h991,plain,
p(s1,s1,s1,s1,s1,s0,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi6,h990]) ).
cnf(h992,plain,
p(s1,s1,s1,s1,s1,s0,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h991]) ).
cnf(h993,plain,
p(s1,s1,s1,s1,s1,s0,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h992]) ).
cnf(h994,plain,
p(s1,s1,s1,s1,s1,s0,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h993]) ).
cnf(h995,plain,
p(s1,s1,s1,s1,s1,s0,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h994]) ).
cnf(h996,plain,
p(s1,s1,s1,s1,s1,s0,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h995]) ).
cnf(h997,plain,
p(s1,s1,s1,s1,s1,s0,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h996]) ).
cnf(h998,plain,
p(s1,s1,s1,s1,s1,s0,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h997]) ).
cnf(h999,plain,
p(s1,s1,s1,s1,s1,s0,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h998]) ).
cnf(h1000,plain,
p(s1,s1,s1,s1,s1,s0,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h999]) ).
cnf(h1001,plain,
p(s1,s1,s1,s1,s1,s0,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h1000]) ).
cnf(h1002,plain,
p(s1,s1,s1,s1,s1,s0,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1001]) ).
cnf(h1003,plain,
p(s1,s1,s1,s1,s1,s0,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h1002]) ).
cnf(h1004,plain,
p(s1,s1,s1,s1,s1,s0,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1003]) ).
cnf(h1005,plain,
p(s1,s1,s1,s1,s1,s0,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h1004]) ).
cnf(h1006,plain,
p(s1,s1,s1,s1,s1,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1005]) ).
cnf(h1007,plain,
p(s1,s1,s1,s1,s1,s1,s0,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h1006]) ).
cnf(h1008,plain,
p(s1,s1,s1,s1,s1,s1,s0,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1007]) ).
cnf(h1009,plain,
p(s1,s1,s1,s1,s1,s1,s0,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h1008]) ).
cnf(h1010,plain,
p(s1,s1,s1,s1,s1,s1,s0,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1009]) ).
cnf(h1011,plain,
p(s1,s1,s1,s1,s1,s1,s0,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h1010]) ).
cnf(h1012,plain,
p(s1,s1,s1,s1,s1,s1,s0,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1011]) ).
cnf(h1013,plain,
p(s1,s1,s1,s1,s1,s1,s0,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h1012]) ).
cnf(h1014,plain,
p(s1,s1,s1,s1,s1,s1,s0,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1013]) ).
cnf(h1015,plain,
p(s1,s1,s1,s1,s1,s1,s1,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h1014]) ).
cnf(h1016,plain,
p(s1,s1,s1,s1,s1,s1,s1,s0,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1015]) ).
cnf(h1017,plain,
p(s1,s1,s1,s1,s1,s1,s1,s0,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h1016]) ).
cnf(h1018,plain,
p(s1,s1,s1,s1,s1,s1,s1,s0,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1017]) ).
cnf(h1019,plain,
p(s1,s1,s1,s1,s1,s1,s1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi3,h1018]) ).
cnf(h1020,plain,
p(s1,s1,s1,s1,s1,s1,s1,s1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1019]) ).
cnf(h1021,plain,
p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h1020]) ).
cnf(t245,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(p,s1),s1),s1),s1),s1),s1),s1),s1),s1),s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h1021]) ).
cnf(t501,plain,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(p,s1),s1),s1),s1),s1),s1),s1),s1),s1),s1) = true,
inference(orient,[status(thm)],[t245]) ).
cnf(f11,negated_conjecture,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f11_nnf,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(goal_0,negated_conjecture,
ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(ap2(p,s1),s1),s1),s1),s1),s1),s1),s1),s1),s1) != true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t501]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MSC015-1.010 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n010.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 01:30:59 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 40.98/5.64 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.98/5.64 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------