%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ016-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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:31:51 PM UTC 2026
% Result : Unsatisfiable 2.48s 0.78s
% Output : Proof 2.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 51
% Syntax : Number of formulae : 506 ( 10 unt; 0 def)
% Number of atoms : 2288 ( 0 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 2165 ( 383 ~;1782 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 38 ( 37 usr; 38 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f115,negated_conjecture,
( ~ vertical_4_4
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_5_4) ).
fof(f115_nnf,plain,
( ~ vertical_4_4
| ~ horizontal_5_3 ),
inference(nnf_transformation,[status(thm)],[f115]) ).
fof(f115_sk,plain,
( ~ vertical_4_4
| ~ horizontal_5_3 ),
inference(skolemisation,[status(esa)],[f115_nnf]) ).
cnf(c115,plain,
( ~ vertical_4_4
| ~ horizontal_5_3 ),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
cnf(f26,negated_conjecture,
( vertical_4_3
| horizontal_5_2
| horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_3) ).
fof(f26_nnf,plain,
( vertical_4_3
| horizontal_5_2
| horizontal_5_3 ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( vertical_4_3
| horizontal_5_2
| horizontal_5_3 ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( vertical_4_3
| horizontal_5_2
| horizontal_5_3 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p121,plain,
( vertical_4_3
| horizontal_5_2
| ~ vertical_4_4 ),
inference(resolution,[status(thm)],[c115,c26]) ).
cnf(f22,negated_conjecture,
( vertical_3_4
| horizontal_4_3
| vertical_4_4
| horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_4) ).
fof(f22_nnf,plain,
( vertical_3_4
| horizontal_4_3
| vertical_4_4
| horizontal_4_4 ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
( vertical_3_4
| horizontal_4_3
| vertical_4_4
| horizontal_4_4 ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( vertical_3_4
| horizontal_4_3
| vertical_4_4
| horizontal_4_4 ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p127,plain,
( vertical_3_4
| horizontal_4_3
| horizontal_4_4
| vertical_4_3
| horizontal_5_2 ),
inference(resolution,[status(thm)],[p121,c22]) ).
cnf(f107,negated_conjecture,
( ~ horizontal_5_1
| ~ horizontal_5_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_2) ).
fof(f107_nnf,plain,
( ~ horizontal_5_1
| ~ horizontal_5_2 ),
inference(nnf_transformation,[status(thm)],[f107]) ).
fof(f107_sk,plain,
( ~ horizontal_5_1
| ~ horizontal_5_2 ),
inference(skolemisation,[status(esa)],[f107_nnf]) ).
cnf(c107,plain,
( ~ horizontal_5_1
| ~ horizontal_5_2 ),
inference(cnf_transformation,[status(esa)],[f107_sk]) ).
cnf(p143,plain,
( ~ horizontal_5_1
| vertical_3_4
| horizontal_4_3
| horizontal_4_4
| vertical_4_3 ),
inference(resolution,[status(thm)],[p127,c107]) ).
cnf(f24,negated_conjecture,
( vertical_4_1
| horizontal_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_1) ).
fof(f24_nnf,plain,
( vertical_4_1
| horizontal_5_1 ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
( vertical_4_1
| horizontal_5_1 ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( vertical_4_1
| horizontal_5_1 ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p157,plain,
( vertical_4_1
| vertical_3_4
| horizontal_4_3
| horizontal_4_4
| vertical_4_3 ),
inference(resolution,[status(thm)],[p143,c24]) ).
cnf(f113,negated_conjecture,
( ~ horizontal_5_3
| ~ horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_4) ).
fof(f113_nnf,plain,
( ~ horizontal_5_3
| ~ horizontal_5_4 ),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
( ~ horizontal_5_3
| ~ horizontal_5_4 ),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
( ~ horizontal_5_3
| ~ horizontal_5_4 ),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(f28,negated_conjecture,
( vertical_4_5
| horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_5) ).
fof(f28_nnf,plain,
( vertical_4_5
| horizontal_5_4 ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
( vertical_4_5
| horizontal_5_4 ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( vertical_4_5
| horizontal_5_4 ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p119,plain,
( vertical_4_5
| ~ horizontal_5_3 ),
inference(resolution,[status(thm)],[c113,c28]) ).
cnf(p124,plain,
( vertical_4_3
| horizontal_5_2
| vertical_4_5 ),
inference(resolution,[status(thm)],[p119,c26]) ).
cnf(p129,plain,
( ~ horizontal_5_1
| vertical_4_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[p124,c107]) ).
cnf(p132,plain,
( vertical_4_1
| vertical_4_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[p129,c24]) ).
cnf(f103,negated_conjecture,
( ~ horizontal_4_4
| ~ vertical_4_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_5) ).
fof(f103_nnf,plain,
( ~ horizontal_4_4
| ~ vertical_4_5 ),
inference(nnf_transformation,[status(thm)],[f103]) ).
fof(f103_sk,plain,
( ~ horizontal_4_4
| ~ vertical_4_5 ),
inference(skolemisation,[status(esa)],[f103_nnf]) ).
cnf(c103,plain,
( ~ horizontal_4_4
| ~ vertical_4_5 ),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(p134,plain,
( ~ horizontal_4_4
| vertical_4_1
| vertical_4_3 ),
inference(resolution,[status(thm)],[p132,c103]) ).
cnf(p166,plain,
( vertical_4_1
| vertical_4_3
| vertical_4_1
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[p157,p134]) ).
cnf(p182,plain,
( vertical_4_1
| vertical_4_1
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(factoring,[status(thm)],[p166]) ).
cnf(p184,plain,
( vertical_4_1
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(factoring,[status(thm)],[p182]) ).
cnf(f95,negated_conjecture,
( ~ vertical_3_3
| ~ vertical_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_3) ).
fof(f95_nnf,plain,
( ~ vertical_3_3
| ~ vertical_4_3 ),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
( ~ vertical_3_3
| ~ vertical_4_3 ),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c95,plain,
( ~ vertical_3_3
| ~ vertical_4_3 ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(p186,plain,
( ~ vertical_3_3
| vertical_4_1
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p184,c95]) ).
cnf(f16,negated_conjecture,
( vertical_2_3
| horizontal_3_2
| vertical_3_3
| horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_3) ).
fof(f16_nnf,plain,
( vertical_2_3
| horizontal_3_2
| vertical_3_3
| horizontal_3_3 ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( vertical_2_3
| horizontal_3_2
| vertical_3_3
| horizontal_3_3 ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( vertical_2_3
| horizontal_3_2
| vertical_3_3
| horizontal_3_3 ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p188,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_4_1
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p186,c16]) ).
cnf(f93,negated_conjecture,
( ~ vertical_3_3
| ~ horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_4_3) ).
fof(f93_nnf,plain,
( ~ vertical_3_3
| ~ horizontal_4_3 ),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
( ~ vertical_3_3
| ~ horizontal_4_3 ),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c93,plain,
( ~ vertical_3_3
| ~ horizontal_4_3 ),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(p216,plain,
( ~ vertical_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p188,c93]) ).
cnf(p238,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p216,c16]) ).
cnf(p303,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p238]) ).
cnf(p312,plain,
( vertical_2_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p303]) ).
cnf(p314,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p312]) ).
cnf(f84,negated_conjecture,
( ~ vertical_3_1
| ~ vertical_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_1) ).
fof(f84_nnf,plain,
( ~ vertical_3_1
| ~ vertical_4_1 ),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
( ~ vertical_3_1
| ~ vertical_4_1 ),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
( ~ vertical_3_1
| ~ vertical_4_1 ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(p315,plain,
( ~ vertical_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[p314,c84]) ).
cnf(f14,negated_conjecture,
( vertical_2_1
| vertical_3_1
| horizontal_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_1) ).
fof(f14_nnf,plain,
( vertical_2_1
| vertical_3_1
| horizontal_3_1 ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( vertical_2_1
| vertical_3_1
| horizontal_3_1 ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( vertical_2_1
| vertical_3_1
| horizontal_3_1 ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p318,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[p315,c14]) ).
cnf(f77,negated_conjecture,
( ~ vertical_2_4
| ~ vertical_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_4) ).
fof(f77_nnf,plain,
( ~ vertical_2_4
| ~ vertical_3_4 ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
( ~ vertical_2_4
| ~ vertical_3_4 ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c77,plain,
( ~ vertical_2_4
| ~ vertical_3_4 ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(p319,plain,
( ~ vertical_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(resolution,[status(thm)],[p318,c77]) ).
cnf(f12,negated_conjecture,
( vertical_1_4
| horizontal_2_3
| vertical_2_4
| horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_4) ).
fof(f12_nnf,plain,
( vertical_1_4
| horizontal_2_3
| vertical_2_4
| horizontal_2_4 ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
( vertical_1_4
| horizontal_2_3
| vertical_2_4
| horizontal_2_4 ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( vertical_1_4
| horizontal_2_3
| vertical_2_4
| horizontal_2_4 ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p321,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(resolution,[status(thm)],[p319,c12]) ).
cnf(f78,negated_conjecture,
( ~ vertical_2_4
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_3_4) ).
fof(f78_nnf,plain,
( ~ vertical_2_4
| ~ horizontal_3_3 ),
inference(nnf_transformation,[status(thm)],[f78]) ).
fof(f78_sk,plain,
( ~ vertical_2_4
| ~ horizontal_3_3 ),
inference(skolemisation,[status(esa)],[f78_nnf]) ).
cnf(c78,plain,
( ~ vertical_2_4
| ~ horizontal_3_3 ),
inference(cnf_transformation,[status(esa)],[f78_sk]) ).
cnf(p385,plain,
( ~ vertical_2_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p321,c78]) ).
cnf(p449,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p385,c12]) ).
cnf(p537,plain,
( vertical_1_4
| horizontal_2_3
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p449]) ).
cnf(p603,plain,
( vertical_1_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p537]) ).
cnf(p605,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p603]) ).
cnf(f61,negated_conjecture,
( ~ vertical_3_2
| ~ horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_2) ).
fof(f61_nnf,plain,
( ~ vertical_3_2
| ~ horizontal_3_2 ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
( ~ vertical_3_2
| ~ horizontal_3_2 ),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c61,plain,
( ~ vertical_3_2
| ~ horizontal_3_2 ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(p606,plain,
( ~ vertical_3_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p605,c61]) ).
cnf(f94,negated_conjecture,
( ~ horizontal_4_2
| ~ vertical_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_3) ).
fof(f94_nnf,plain,
( ~ horizontal_4_2
| ~ vertical_4_3 ),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
( ~ horizontal_4_2
| ~ vertical_4_3 ),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
( ~ horizontal_4_2
| ~ vertical_4_3 ),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(p185,plain,
( ~ horizontal_4_2
| vertical_4_1
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p184,c94]) ).
cnf(f109,negated_conjecture,
( ~ vertical_4_2
| ~ horizontal_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_5_2) ).
fof(f109_nnf,plain,
( ~ vertical_4_2
| ~ horizontal_5_1 ),
inference(nnf_transformation,[status(thm)],[f109]) ).
fof(f109_sk,plain,
( ~ vertical_4_2
| ~ horizontal_5_1 ),
inference(skolemisation,[status(esa)],[f109_nnf]) ).
cnf(c109,plain,
( ~ vertical_4_2
| ~ horizontal_5_1 ),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
cnf(p117,plain,
( vertical_4_1
| ~ vertical_4_2 ),
inference(resolution,[status(thm)],[c109,c24]) ).
cnf(f20,negated_conjecture,
( vertical_3_2
| horizontal_4_1
| vertical_4_2
| horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_2) ).
fof(f20_nnf,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_2
| horizontal_4_2 ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_2
| horizontal_4_2 ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_2
| horizontal_4_2 ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p123,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_4_1 ),
inference(resolution,[status(thm)],[p117,c20]) ).
cnf(p187,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_4_1
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p185,p123]) ).
cnf(p210,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_4
| horizontal_4_3 ),
inference(factoring,[status(thm)],[p187]) ).
cnf(f92,negated_conjecture,
( ~ horizontal_4_2
| ~ horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_4_3) ).
fof(f92_nnf,plain,
( ~ horizontal_4_2
| ~ horizontal_4_3 ),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
( ~ horizontal_4_2
| ~ horizontal_4_3 ),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c92,plain,
( ~ horizontal_4_2
| ~ horizontal_4_3 ),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(p212,plain,
( ~ horizontal_4_2
| vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p210,c92]) ).
cnf(p213,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p212,p123]) ).
cnf(p242,plain,
( vertical_3_2
| horizontal_4_1
| vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p213]) ).
cnf(p245,plain,
( vertical_3_2
| vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p242]) ).
cnf(p247,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p245]) ).
cnf(p248,plain,
( ~ vertical_3_1
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p247,c84]) ).
cnf(p251,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p248,c14]) ).
cnf(f83,negated_conjecture,
( ~ vertical_3_1
| ~ horizontal_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_4_1) ).
fof(f83_nnf,plain,
( ~ vertical_3_1
| ~ horizontal_4_1 ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
( ~ vertical_3_1
| ~ horizontal_4_1 ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
( ~ vertical_3_1
| ~ horizontal_4_1 ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(p253,plain,
( ~ vertical_3_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[p251,c83]) ).
cnf(p254,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[p253,c14]) ).
cnf(p256,plain,
( vertical_2_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p254]) ).
cnf(p258,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p256]) ).
cnf(p260,plain,
( ~ vertical_2_4
| vertical_2_1
| horizontal_3_1
| vertical_3_2 ),
inference(resolution,[status(thm)],[p258,c77]) ).
cnf(p264,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_3_2 ),
inference(resolution,[status(thm)],[p260,c12]) ).
cnf(p607,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p606,p264]) ).
cnf(p681,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p607]) ).
cnf(p779,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p681]) ).
cnf(p893,plain,
( vertical_1_4
| horizontal_2_3
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p779]) ).
cnf(p929,plain,
( vertical_1_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p893]) ).
cnf(p931,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p929]) ).
cnf(f108,negated_conjecture,
( ~ vertical_4_2
| ~ horizontal_5_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_2) ).
fof(f108_nnf,plain,
( ~ vertical_4_2
| ~ horizontal_5_2 ),
inference(nnf_transformation,[status(thm)],[f108]) ).
fof(f108_sk,plain,
( ~ vertical_4_2
| ~ horizontal_5_2 ),
inference(skolemisation,[status(esa)],[f108_nnf]) ).
cnf(c108,plain,
( ~ vertical_4_2
| ~ horizontal_5_2 ),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(p144,plain,
( ~ vertical_4_2
| vertical_3_4
| horizontal_4_3
| horizontal_4_4
| vertical_4_3 ),
inference(resolution,[status(thm)],[p127,c108]) ).
cnf(p158,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3
| horizontal_4_4
| vertical_4_3 ),
inference(resolution,[status(thm)],[p144,c20]) ).
cnf(p130,plain,
( ~ vertical_4_2
| vertical_4_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[p124,c108]) ).
cnf(p133,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_4_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[p130,c20]) ).
cnf(p150,plain,
( ~ horizontal_4_4
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_4_3 ),
inference(resolution,[status(thm)],[p133,c103]) ).
cnf(p179,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_4_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[p158,p150]) ).
cnf(p218,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(factoring,[status(thm)],[p179]) ).
cnf(p287,plain,
( vertical_3_2
| horizontal_4_1
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(factoring,[status(thm)],[p218]) ).
cnf(p353,plain,
( vertical_3_2
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(factoring,[status(thm)],[p287]) ).
cnf(p367,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3
| vertical_4_3 ),
inference(factoring,[status(thm)],[p353]) ).
cnf(p368,plain,
( ~ vertical_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p367,c95]) ).
cnf(p369,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p368,c16]) ).
cnf(p445,plain,
( ~ vertical_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[p369,c93]) ).
cnf(p450,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[p445,c16]) ).
cnf(p545,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p450]) ).
cnf(p608,plain,
( vertical_2_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p545]) ).
cnf(p613,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p608]) ).
cnf(f96,negated_conjecture,
( ~ vertical_3_3
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_3) ).
fof(f96_nnf,plain,
( ~ vertical_3_3
| ~ horizontal_4_2 ),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
( ~ vertical_3_3
| ~ horizontal_4_2 ),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c96,plain,
( ~ vertical_3_3
| ~ horizontal_4_2 ),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(p615,plain,
( ~ vertical_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p613,c96]) ).
cnf(p616,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(resolution,[status(thm)],[p615,c16]) ).
cnf(p676,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p616]) ).
cnf(p679,plain,
( vertical_2_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p676]) ).
cnf(p686,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| vertical_3_4 ),
inference(factoring,[status(thm)],[p679]) ).
cnf(f82,negated_conjecture,
( ~ vertical_4_1
| ~ horizontal_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_4_1) ).
fof(f82_nnf,plain,
( ~ vertical_4_1
| ~ horizontal_4_1 ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
( ~ vertical_4_1
| ~ horizontal_4_1 ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
( ~ vertical_4_1
| ~ horizontal_4_1 ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(p687,plain,
( ~ vertical_4_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[p686,c82]) ).
cnf(p688,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_4
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[p687,p314]) ).
cnf(p729,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p688]) ).
cnf(p733,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p729]) ).
cnf(p737,plain,
( vertical_2_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p733]) ).
cnf(p739,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| vertical_3_4 ),
inference(factoring,[status(thm)],[p737]) ).
cnf(p740,plain,
( ~ vertical_2_4
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(resolution,[status(thm)],[p739,c77]) ).
cnf(p744,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(resolution,[status(thm)],[p740,c12]) ).
cnf(p751,plain,
( ~ vertical_2_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[p744,c78]) ).
cnf(p752,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[p751,c12]) ).
cnf(p822,plain,
( vertical_1_4
| horizontal_2_3
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p752]) ).
cnf(p910,plain,
( vertical_1_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p822]) ).
cnf(p912,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p910]) ).
cnf(f64,negated_conjecture,
( ~ horizontal_3_1
| ~ vertical_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_3_2) ).
fof(f64_nnf,plain,
( ~ horizontal_3_1
| ~ vertical_3_2 ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
( ~ horizontal_3_1
| ~ vertical_3_2 ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c64,plain,
( ~ horizontal_3_1
| ~ vertical_3_2 ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(p913,plain,
( ~ horizontal_3_1
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p912,c64]) ).
cnf(p937,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_3
| horizontal_3_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p931,p913]) ).
cnf(p1003,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| horizontal_3_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p937]) ).
cnf(p1129,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_3_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1003]) ).
cnf(p1132,plain,
( vertical_1_4
| horizontal_3_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1129]) ).
cnf(p1134,plain,
( horizontal_3_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1132]) ).
cnf(f62,negated_conjecture,
( ~ horizontal_3_1
| ~ horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_3_2) ).
fof(f62_nnf,plain,
( ~ horizontal_3_1
| ~ horizontal_3_2 ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
( ~ horizontal_3_1
| ~ horizontal_3_2 ),
inference(skolemisation,[status(esa)],[f62_nnf]) ).
cnf(c62,plain,
( ~ horizontal_3_1
| ~ horizontal_3_2 ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p1136,plain,
( ~ horizontal_3_1
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p1134,c62]) ).
cnf(p1142,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p1136,p931]) ).
cnf(p1242,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1142]) ).
cnf(p1247,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1242]) ).
cnf(p1251,plain,
( vertical_1_4
| horizontal_2_3
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1247]) ).
cnf(p1254,plain,
( vertical_1_4
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1251]) ).
cnf(p1260,plain,
( vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1254]) ).
cnf(f104,negated_conjecture,
( ~ vertical_3_5
| ~ vertical_4_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_5) ).
fof(f104_nnf,plain,
( ~ vertical_3_5
| ~ vertical_4_5 ),
inference(nnf_transformation,[status(thm)],[f104]) ).
fof(f104_sk,plain,
( ~ vertical_3_5
| ~ vertical_4_5 ),
inference(skolemisation,[status(esa)],[f104_nnf]) ).
cnf(c104,plain,
( ~ vertical_3_5
| ~ vertical_4_5 ),
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
cnf(p151,plain,
( ~ vertical_3_5
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_4_3 ),
inference(resolution,[status(thm)],[p133,c104]) ).
cnf(f18,negated_conjecture,
( vertical_2_5
| horizontal_3_4
| vertical_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_5) ).
fof(f18_nnf,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_5 ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_5 ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_5 ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p164,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_4_3 ),
inference(resolution,[status(thm)],[p151,c18]) ).
cnf(p181,plain,
( ~ vertical_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1
| horizontal_4_2 ),
inference(resolution,[status(thm)],[p164,c95]) ).
cnf(p209,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1
| horizontal_4_2 ),
inference(resolution,[status(thm)],[p181,c16]) ).
cnf(p276,plain,
( ~ vertical_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1 ),
inference(resolution,[status(thm)],[p209,c96]) ).
cnf(p337,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1 ),
inference(resolution,[status(thm)],[p276,c16]) ).
cnf(p439,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1 ),
inference(factoring,[status(thm)],[p337]) ).
cnf(p481,plain,
( vertical_2_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1 ),
inference(factoring,[status(thm)],[p439]) ).
cnf(p483,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1 ),
inference(factoring,[status(thm)],[p481]) ).
cnf(p484,plain,
( ~ vertical_4_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(resolution,[status(thm)],[p483,c82]) ).
cnf(p135,plain,
( ~ vertical_3_5
| vertical_4_1
| vertical_4_3 ),
inference(resolution,[status(thm)],[p132,c104]) ).
cnf(p138,plain,
( vertical_2_5
| horizontal_3_4
| vertical_4_1
| vertical_4_3 ),
inference(resolution,[status(thm)],[p135,c18]) ).
cnf(p147,plain,
( ~ vertical_3_3
| vertical_2_5
| horizontal_3_4
| vertical_4_1 ),
inference(resolution,[status(thm)],[p138,c95]) ).
cnf(p155,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_4_1 ),
inference(resolution,[status(thm)],[p147,c16]) ).
cnf(p485,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(resolution,[status(thm)],[p484,p155]) ).
cnf(p570,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(factoring,[status(thm)],[p485]) ).
cnf(p636,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(factoring,[status(thm)],[p570]) ).
cnf(p711,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(factoring,[status(thm)],[p636]) ).
cnf(p714,plain,
( vertical_2_3
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(factoring,[status(thm)],[p711]) ).
cnf(p716,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4
| vertical_3_2 ),
inference(factoring,[status(thm)],[p714]) ).
cnf(f73,negated_conjecture,
( ~ vertical_3_4
| ~ horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_4) ).
fof(f73_nnf,plain,
( ~ vertical_3_4
| ~ horizontal_3_4 ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
( ~ vertical_3_4
| ~ horizontal_3_4 ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c73,plain,
( ~ vertical_3_4
| ~ horizontal_3_4 ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(p717,plain,
( ~ vertical_3_4
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| vertical_3_2 ),
inference(resolution,[status(thm)],[p716,c73]) ).
cnf(p743,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| vertical_3_2
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(resolution,[status(thm)],[p739,p717]) ).
cnf(p788,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(factoring,[status(thm)],[p743]) ).
cnf(p792,plain,
( vertical_2_3
| horizontal_3_2
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(factoring,[status(thm)],[p788]) ).
cnf(p797,plain,
( vertical_2_3
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(factoring,[status(thm)],[p792]) ).
cnf(p799,plain,
( vertical_2_5
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(factoring,[status(thm)],[p797]) ).
cnf(f114,negated_conjecture,
( ~ vertical_4_4
| ~ horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_4) ).
fof(f114_nnf,plain,
( ~ vertical_4_4
| ~ horizontal_5_4 ),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
( ~ vertical_4_4
| ~ horizontal_5_4 ),
inference(skolemisation,[status(esa)],[f114_nnf]) ).
cnf(c114,plain,
( ~ vertical_4_4
| ~ horizontal_5_4 ),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(p120,plain,
( vertical_4_5
| ~ vertical_4_4 ),
inference(resolution,[status(thm)],[c114,c28]) ).
cnf(p126,plain,
( vertical_3_4
| horizontal_4_3
| horizontal_4_4
| vertical_4_5 ),
inference(resolution,[status(thm)],[p120,c22]) ).
cnf(p139,plain,
( ~ vertical_3_5
| vertical_3_4
| horizontal_4_3
| horizontal_4_4 ),
inference(resolution,[status(thm)],[p126,c104]) ).
cnf(p148,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_4
| horizontal_4_3
| horizontal_4_4 ),
inference(resolution,[status(thm)],[p139,c18]) ).
cnf(f105,negated_conjecture,
( ~ vertical_3_5
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_5) ).
fof(f105_nnf,plain,
( ~ vertical_3_5
| ~ horizontal_4_4 ),
inference(nnf_transformation,[status(thm)],[f105]) ).
fof(f105_sk,plain,
( ~ vertical_3_5
| ~ horizontal_4_4 ),
inference(skolemisation,[status(esa)],[f105_nnf]) ).
cnf(c105,plain,
( ~ vertical_3_5
| ~ horizontal_4_4 ),
inference(cnf_transformation,[status(esa)],[f105_sk]) ).
cnf(p160,plain,
( ~ vertical_3_5
| vertical_2_5
| horizontal_3_4
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p148,c105]) ).
cnf(p168,plain,
( vertical_2_5
| horizontal_3_4
| vertical_2_5
| horizontal_3_4
| vertical_3_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[p160,c18]) ).
cnf(p189,plain,
( vertical_2_5
| vertical_2_5
| horizontal_3_4
| vertical_3_4
| horizontal_4_3 ),
inference(factoring,[status(thm)],[p168]) ).
cnf(p194,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_4
| horizontal_4_3 ),
inference(factoring,[status(thm)],[p189]) ).
cnf(f91,negated_conjecture,
( ~ vertical_4_3
| ~ horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_4_3) ).
fof(f91_nnf,plain,
( ~ vertical_4_3
| ~ horizontal_4_3 ),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
( ~ vertical_4_3
| ~ horizontal_4_3 ),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c91,plain,
( ~ vertical_4_3
| ~ horizontal_4_3 ),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(p195,plain,
( ~ vertical_4_3
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p194,c91]) ).
cnf(p199,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p195,p164]) ).
cnf(p236,plain,
( vertical_2_5
| vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p199]) ).
cnf(p280,plain,
( vertical_3_2
| horizontal_4_1
| horizontal_4_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p236]) ).
cnf(p196,plain,
( ~ horizontal_4_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p194,c92]) ).
cnf(p285,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_4
| vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p280,p196]) ).
cnf(p338,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p285]) ).
cnf(p341,plain,
( vertical_2_5
| vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p338]) ).
cnf(p343,plain,
( vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p341]) ).
cnf(p346,plain,
( ~ vertical_4_1
| vertical_3_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p343,c82]) ).
cnf(p198,plain,
( vertical_2_5
| horizontal_3_4
| vertical_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p195,p138]) ).
cnf(p223,plain,
( vertical_2_5
| vertical_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p198]) ).
cnf(p225,plain,
( vertical_4_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p223]) ).
cnf(p347,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_4
| vertical_3_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p346,p225]) ).
cnf(p348,plain,
( vertical_2_5
| horizontal_3_4
| vertical_3_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p347]) ).
cnf(p351,plain,
( vertical_2_5
| vertical_3_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p348]) ).
cnf(p355,plain,
( vertical_3_2
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(factoring,[status(thm)],[p351]) ).
cnf(f76,negated_conjecture,
( ~ horizontal_3_3
| ~ vertical_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_3_4) ).
fof(f76_nnf,plain,
( ~ horizontal_3_3
| ~ vertical_3_4 ),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
( ~ horizontal_3_3
| ~ vertical_3_4 ),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c76,plain,
( ~ horizontal_3_3
| ~ vertical_3_4 ),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(p356,plain,
( ~ horizontal_3_3
| vertical_3_2
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p355,c76]) ).
cnf(p802,plain,
( vertical_3_2
| vertical_2_5
| horizontal_3_4
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[p799,p356]) ).
cnf(p807,plain,
( vertical_2_5
| horizontal_3_4
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p802]) ).
cnf(p809,plain,
( horizontal_3_4
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p807]) ).
cnf(f74,negated_conjecture,
( ~ horizontal_3_3
| ~ horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_3_4) ).
fof(f74_nnf,plain,
( ~ horizontal_3_3
| ~ horizontal_3_4 ),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
( ~ horizontal_3_3
| ~ horizontal_3_4 ),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c74,plain,
( ~ horizontal_3_3
| ~ horizontal_3_4 ),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(p811,plain,
( ~ horizontal_3_3
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[p809,c74]) ).
cnf(p816,plain,
( vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[p811,p799]) ).
cnf(p843,plain,
( vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p816]) ).
cnf(p847,plain,
( vertical_2_5
| vertical_2_3
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p843]) ).
cnf(p850,plain,
( vertical_2_5
| vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p847]) ).
cnf(p854,plain,
( vertical_2_5
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p850]) ).
cnf(p855,plain,
( ~ horizontal_3_1
| vertical_2_5
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p854,c64]) ).
cnf(p175,plain,
( ~ vertical_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p155,c84]) ).
cnf(p207,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p175,c14]) ).
cnf(p240,plain,
( ~ vertical_3_4
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5 ),
inference(resolution,[status(thm)],[p207,c73]) ).
cnf(p320,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(resolution,[status(thm)],[p318,p240]) ).
cnf(p394,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(factoring,[status(thm)],[p320]) ).
cnf(p499,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(factoring,[status(thm)],[p394]) ).
cnf(p584,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(factoring,[status(thm)],[p499]) ).
cnf(p591,plain,
( vertical_2_1
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(factoring,[status(thm)],[p584]) ).
cnf(p593,plain,
( vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3 ),
inference(factoring,[status(thm)],[p591]) ).
cnf(p226,plain,
( ~ vertical_3_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p225,c84]) ).
cnf(p229,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_5
| horizontal_3_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[p226,c14]) ).
cnf(p230,plain,
( ~ horizontal_3_3
| vertical_2_1
| horizontal_3_1
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p229,c76]) ).
cnf(p596,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_5
| horizontal_3_4
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p593,p230]) ).
cnf(p655,plain,
( vertical_2_1
| vertical_2_5
| horizontal_3_4
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p596]) ).
cnf(p662,plain,
( vertical_2_5
| horizontal_3_4
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p655]) ).
cnf(p666,plain,
( horizontal_3_4
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p662]) ).
cnf(p668,plain,
( ~ horizontal_3_3
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p666,c74]) ).
cnf(p669,plain,
( vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p668,p593]) ).
cnf(p745,plain,
( vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p669]) ).
cnf(p812,plain,
( vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p745]) ).
cnf(p817,plain,
( vertical_2_5
| vertical_2_1
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p812]) ).
cnf(p820,plain,
( vertical_2_5
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p817]) ).
cnf(p825,plain,
( vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p820]) ).
cnf(p826,plain,
( ~ vertical_3_2
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p825,c61]) ).
cnf(p146,plain,
( ~ horizontal_4_2
| vertical_2_5
| horizontal_3_4
| vertical_4_1 ),
inference(resolution,[status(thm)],[p138,c94]) ).
cnf(p154,plain,
( vertical_3_2
| horizontal_4_1
| vertical_4_1
| vertical_2_5
| horizontal_3_4
| vertical_4_1 ),
inference(resolution,[status(thm)],[p146,p123]) ).
cnf(p172,plain,
( vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4
| vertical_4_1 ),
inference(factoring,[status(thm)],[p154]) ).
cnf(p173,plain,
( ~ vertical_3_1
| vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p172,c84]) ).
cnf(p174,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| horizontal_4_1
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p173,c14]) ).
cnf(p206,plain,
( ~ vertical_3_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p174,c83]) ).
cnf(p235,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[p206,c14]) ).
cnf(p273,plain,
( vertical_2_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5
| horizontal_3_4 ),
inference(factoring,[status(thm)],[p235]) ).
cnf(p277,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5
| horizontal_3_4 ),
inference(factoring,[status(thm)],[p273]) ).
cnf(p278,plain,
( ~ vertical_3_4
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5 ),
inference(resolution,[status(thm)],[p277,c73]) ).
cnf(p279,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5 ),
inference(resolution,[status(thm)],[p278,p258]) ).
cnf(p296,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5 ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p299,plain,
( vertical_2_1
| vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5 ),
inference(factoring,[status(thm)],[p296]) ).
cnf(p301,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_5 ),
inference(factoring,[status(thm)],[p299]) ).
cnf(p827,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_5
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p826,p301]) ).
cnf(p828,plain,
( vertical_2_1
| vertical_2_5
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p827]) ).
cnf(p833,plain,
( vertical_2_5
| vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p828]) ).
cnf(p835,plain,
( vertical_2_5
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p833]) ).
cnf(p859,plain,
( vertical_2_5
| vertical_2_1
| vertical_2_3
| vertical_2_5
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p855,p835]) ).
cnf(p861,plain,
( vertical_2_5
| vertical_2_1
| vertical_2_5
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p859]) ).
cnf(p863,plain,
( vertical_2_1
| vertical_2_5
| vertical_2_3
| horizontal_3_2 ),
inference(factoring,[status(thm)],[p861]) ).
cnf(p865,plain,
( ~ horizontal_3_1
| vertical_2_1
| vertical_2_5
| vertical_2_3 ),
inference(resolution,[status(thm)],[p863,c62]) ).
cnf(p868,plain,
( vertical_2_5
| vertical_2_1
| vertical_2_3
| vertical_2_1
| vertical_2_5
| vertical_2_3 ),
inference(resolution,[status(thm)],[p865,p835]) ).
cnf(p872,plain,
( vertical_2_5
| vertical_2_1
| vertical_2_1
| vertical_2_5
| vertical_2_3 ),
inference(factoring,[status(thm)],[p868]) ).
cnf(p875,plain,
( vertical_2_1
| vertical_2_1
| vertical_2_5
| vertical_2_3 ),
inference(factoring,[status(thm)],[p872]) ).
cnf(p881,plain,
( vertical_2_1
| vertical_2_5
| vertical_2_3 ),
inference(factoring,[status(thm)],[p875]) ).
cnf(f55,negated_conjecture,
( ~ horizontal_2_4
| ~ vertical_2_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_5) ).
fof(f55_nnf,plain,
( ~ horizontal_2_4
| ~ vertical_2_5 ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
( ~ horizontal_2_4
| ~ vertical_2_5 ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c55,plain,
( ~ horizontal_2_4
| ~ vertical_2_5 ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(p882,plain,
( ~ horizontal_2_4
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p881,c55]) ).
cnf(p1262,plain,
( vertical_2_1
| vertical_2_3
| vertical_1_4
| horizontal_2_3
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p1260,p882]) ).
cnf(p1263,plain,
( vertical_2_1
| vertical_1_4
| horizontal_2_3
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1262]) ).
cnf(p1269,plain,
( vertical_1_4
| horizontal_2_3
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p1263]) ).
cnf(f46,negated_conjecture,
( ~ horizontal_2_2
| ~ vertical_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_3) ).
fof(f46_nnf,plain,
( ~ horizontal_2_2
| ~ vertical_2_3 ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
( ~ horizontal_2_2
| ~ vertical_2_3 ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
( ~ horizontal_2_2
| ~ vertical_2_3 ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p1270,plain,
( ~ horizontal_2_2
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(resolution,[status(thm)],[p1269,c46]) ).
cnf(f65,negated_conjecture,
( ~ vertical_2_2
| ~ vertical_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_2) ).
fof(f65_nnf,plain,
( ~ vertical_2_2
| ~ vertical_3_2 ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
( ~ vertical_2_2
| ~ vertical_3_2 ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
( ~ vertical_2_2
| ~ vertical_3_2 ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(p265,plain,
( ~ vertical_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1 ),
inference(resolution,[status(thm)],[p264,c65]) ).
cnf(f10,negated_conjecture,
( vertical_1_2
| horizontal_2_1
| vertical_2_2
| horizontal_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_2) ).
fof(f10_nnf,plain,
( vertical_1_2
| horizontal_2_1
| vertical_2_2
| horizontal_2_2 ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( vertical_1_2
| horizontal_2_1
| vertical_2_2
| horizontal_2_2 ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( vertical_1_2
| horizontal_2_1
| vertical_2_2
| horizontal_2_2 ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p266,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1
| horizontal_3_1 ),
inference(resolution,[status(thm)],[p265,c10]) ).
cnf(f66,negated_conjecture,
( ~ vertical_2_2
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_3_2) ).
fof(f66_nnf,plain,
( ~ vertical_2_2
| ~ horizontal_3_1 ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
( ~ vertical_2_2
| ~ horizontal_3_1 ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c66,plain,
( ~ vertical_2_2
| ~ horizontal_3_1 ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p327,plain,
( ~ vertical_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p266,c66]) ).
cnf(p390,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p327,c10]) ).
cnf(p486,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p390]) ).
cnf(p579,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p486]) ).
cnf(p581,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| horizontal_2_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p579]) ).
cnf(p302,plain,
( ~ vertical_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_5 ),
inference(resolution,[status(thm)],[p301,c65]) ).
cnf(p306,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_5 ),
inference(resolution,[status(thm)],[p302,c10]) ).
cnf(p308,plain,
( ~ vertical_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_5 ),
inference(resolution,[status(thm)],[p306,c66]) ).
cnf(p309,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_5 ),
inference(resolution,[status(thm)],[p308,c10]) ).
cnf(p371,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_5 ),
inference(factoring,[status(thm)],[p309]) ).
cnf(p374,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_5 ),
inference(factoring,[status(thm)],[p371]) ).
cnf(p376,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_5 ),
inference(factoring,[status(thm)],[p374]) ).
cnf(p377,plain,
( ~ horizontal_2_4
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1 ),
inference(resolution,[status(thm)],[p376,c55]) ).
cnf(p583,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(resolution,[status(thm)],[p581,p377]) ).
cnf(p643,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(factoring,[status(thm)],[p583]) ).
cnf(p719,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(factoring,[status(thm)],[p643]) ).
cnf(p722,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(factoring,[status(thm)],[p719]) ).
cnf(p724,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(factoring,[status(thm)],[p722]) ).
cnf(f43,negated_conjecture,
( ~ vertical_2_3
| ~ horizontal_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_2_3) ).
fof(f43_nnf,plain,
( ~ vertical_2_3
| ~ horizontal_2_3 ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
( ~ vertical_2_3
| ~ horizontal_2_3 ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( ~ vertical_2_3
| ~ horizontal_2_3 ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p727,plain,
( ~ vertical_2_3
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p724,c43]) ).
cnf(p131,plain,
( ~ vertical_3_3
| vertical_3_2
| horizontal_4_1
| vertical_4_1 ),
inference(resolution,[status(thm)],[p123,c96]) ).
cnf(p142,plain,
( vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1
| vertical_4_1 ),
inference(resolution,[status(thm)],[p131,c16]) ).
cnf(p162,plain,
( ~ vertical_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1 ),
inference(resolution,[status(thm)],[p142,c84]) ).
cnf(p180,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2
| horizontal_4_1 ),
inference(resolution,[status(thm)],[p162,c14]) ).
cnf(p228,plain,
( ~ vertical_3_1
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(resolution,[status(thm)],[p180,c83]) ).
cnf(p269,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(resolution,[status(thm)],[p228,c14]) ).
cnf(p332,plain,
( vertical_2_1
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(factoring,[status(thm)],[p269]) ).
cnf(p334,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| horizontal_3_3
| vertical_3_2 ),
inference(factoring,[status(thm)],[p332]) ).
cnf(p259,plain,
( ~ horizontal_3_3
| vertical_2_1
| horizontal_3_1
| vertical_3_2 ),
inference(resolution,[status(thm)],[p258,c76]) ).
cnf(p336,plain,
( vertical_2_1
| horizontal_3_1
| vertical_3_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[p334,p259]) ).
cnf(p391,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p336]) ).
cnf(p399,plain,
( vertical_2_1
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p391]) ).
cnf(p401,plain,
( vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2
| vertical_3_2 ),
inference(factoring,[status(thm)],[p399]) ).
cnf(p402,plain,
( ~ vertical_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p401,c65]) ).
cnf(p403,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[p402,c10]) ).
cnf(f63,negated_conjecture,
( ~ vertical_2_2
| ~ horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_2) ).
fof(f63_nnf,plain,
( ~ vertical_2_2
| ~ horizontal_3_2 ),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
( ~ vertical_2_2
| ~ horizontal_3_2 ),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c63,plain,
( ~ vertical_2_2
| ~ horizontal_3_2 ),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(p408,plain,
( ~ vertical_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p403,c63]) ).
cnf(p409,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p408,c10]) ).
cnf(p462,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p409]) ).
cnf(p465,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p462]) ).
cnf(p467,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| horizontal_3_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p465]) ).
cnf(p469,plain,
( ~ vertical_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p467,c66]) ).
cnf(p470,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p469,c10]) ).
cnf(p472,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p470]) ).
cnf(p475,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p472]) ).
cnf(p477,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_2_3 ),
inference(factoring,[status(thm)],[p475]) ).
cnf(p728,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p727,p477]) ).
cnf(p765,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p728]) ).
cnf(p769,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p765]) ).
cnf(p775,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p769]) ).
cnf(p777,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p775]) ).
cnf(p1271,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(resolution,[status(thm)],[p1270,p777]) ).
cnf(p1272,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(factoring,[status(thm)],[p1271]) ).
cnf(p1278,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_4
| horizontal_2_3
| vertical_2_1 ),
inference(factoring,[status(thm)],[p1272]) ).
cnf(f44,negated_conjecture,
( ~ horizontal_2_2
| ~ horizontal_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_2_3) ).
fof(f44_nnf,plain,
( ~ horizontal_2_2
| ~ horizontal_2_3 ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
( ~ horizontal_2_2
| ~ horizontal_2_3 ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( ~ horizontal_2_2
| ~ horizontal_2_3 ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p1280,plain,
( ~ horizontal_2_2
| vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p1278,c44]) ).
cnf(p1281,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1
| vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p1280,p777]) ).
cnf(p1289,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p1281]) ).
cnf(p1293,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p1289]) ).
cnf(p1296,plain,
( vertical_1_2
| vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p1293]) ).
cnf(p1298,plain,
( vertical_1_2
| horizontal_2_1
| vertical_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p1296]) ).
cnf(f36,negated_conjecture,
( ~ vertical_1_1
| ~ vertical_2_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_1) ).
fof(f36_nnf,plain,
( ~ vertical_1_1
| ~ vertical_2_1 ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
( ~ vertical_1_1
| ~ vertical_2_1 ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( ~ vertical_1_1
| ~ vertical_2_1 ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p1303,plain,
( ~ vertical_1_1
| vertical_1_2
| horizontal_2_1
| vertical_1_4 ),
inference(resolution,[status(thm)],[p1298,c36]) ).
cnf(f6,negated_conjecture,
( vertical_1_1
| horizontal_1_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_1) ).
fof(f6_nnf,plain,
( vertical_1_1
| horizontal_1_1 ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
( vertical_1_1
| horizontal_1_1 ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( vertical_1_1
| horizontal_1_1 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1304,plain,
( horizontal_1_1
| vertical_1_2
| horizontal_2_1
| vertical_1_4 ),
inference(resolution,[status(thm)],[p1303,c6]) ).
cnf(f35,negated_conjecture,
( ~ vertical_1_1
| ~ horizontal_2_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_2_1) ).
fof(f35_nnf,plain,
( ~ vertical_1_1
| ~ horizontal_2_1 ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( ~ vertical_1_1
| ~ horizontal_2_1 ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( ~ vertical_1_1
| ~ horizontal_2_1 ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p1306,plain,
( ~ vertical_1_1
| horizontal_1_1
| vertical_1_2
| vertical_1_4 ),
inference(resolution,[status(thm)],[p1304,c35]) ).
cnf(p1307,plain,
( horizontal_1_1
| horizontal_1_1
| vertical_1_2
| vertical_1_4 ),
inference(resolution,[status(thm)],[p1306,c6]) ).
cnf(p1308,plain,
( horizontal_1_1
| vertical_1_2
| vertical_1_4 ),
inference(factoring,[status(thm)],[p1307]) ).
cnf(f56,negated_conjecture,
( ~ vertical_1_5
| ~ vertical_2_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_5) ).
fof(f56_nnf,plain,
( ~ vertical_1_5
| ~ vertical_2_5 ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
( ~ vertical_1_5
| ~ vertical_2_5 ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
( ~ vertical_1_5
| ~ vertical_2_5 ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p883,plain,
( ~ vertical_1_5
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p881,c56]) ).
cnf(f8,negated_conjecture,
( horizontal_1_4
| vertical_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_5) ).
fof(f8_nnf,plain,
( horizontal_1_4
| vertical_1_5 ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
( horizontal_1_4
| vertical_1_5 ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( horizontal_1_4
| vertical_1_5 ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p884,plain,
( horizontal_1_4
| vertical_2_1
| vertical_2_3 ),
inference(resolution,[status(thm)],[p883,c8]) ).
cnf(p887,plain,
( ~ horizontal_2_2
| horizontal_1_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p884,c46]) ).
cnf(p378,plain,
( ~ vertical_1_5
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1 ),
inference(resolution,[status(thm)],[p376,c56]) ).
cnf(p379,plain,
( horizontal_1_4
| vertical_1_2
| horizontal_2_1
| horizontal_2_2
| vertical_2_1 ),
inference(resolution,[status(thm)],[p378,c8]) ).
cnf(p889,plain,
( horizontal_1_4
| vertical_1_2
| horizontal_2_1
| vertical_2_1
| horizontal_1_4
| vertical_2_1 ),
inference(resolution,[status(thm)],[p887,p379]) ).
cnf(p899,plain,
( horizontal_1_4
| vertical_1_2
| horizontal_2_1
| horizontal_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p889]) ).
cnf(p901,plain,
( vertical_1_2
| horizontal_2_1
| horizontal_1_4
| vertical_2_1 ),
inference(factoring,[status(thm)],[p899]) ).
cnf(p903,plain,
( ~ vertical_1_1
| vertical_1_2
| horizontal_2_1
| horizontal_1_4 ),
inference(resolution,[status(thm)],[p901,c36]) ).
cnf(p904,plain,
( horizontal_1_1
| vertical_1_2
| horizontal_2_1
| horizontal_1_4 ),
inference(resolution,[status(thm)],[p903,c6]) ).
cnf(p906,plain,
( ~ vertical_1_1
| horizontal_1_1
| vertical_1_2
| horizontal_1_4 ),
inference(resolution,[status(thm)],[p904,c35]) ).
cnf(p907,plain,
( horizontal_1_1
| horizontal_1_1
| vertical_1_2
| horizontal_1_4 ),
inference(resolution,[status(thm)],[p906,c6]) ).
cnf(p908,plain,
( horizontal_1_1
| vertical_1_2
| horizontal_1_4 ),
inference(factoring,[status(thm)],[p907]) ).
cnf(f30,negated_conjecture,
( ~ vertical_1_4
| ~ horizontal_1_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_1_4) ).
fof(f30_nnf,plain,
( ~ vertical_1_4
| ~ horizontal_1_4 ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
( ~ vertical_1_4
| ~ horizontal_1_4 ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ vertical_1_4
| ~ horizontal_1_4 ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p909,plain,
( ~ vertical_1_4
| horizontal_1_1
| vertical_1_2 ),
inference(resolution,[status(thm)],[p908,c30]) ).
cnf(p1309,plain,
( horizontal_1_1
| vertical_1_2
| horizontal_1_1
| vertical_1_2 ),
inference(resolution,[status(thm)],[p1308,p909]) ).
cnf(p1310,plain,
( horizontal_1_1
| horizontal_1_1
| vertical_1_2 ),
inference(factoring,[status(thm)],[p1309]) ).
cnf(p1314,plain,
( horizontal_1_1
| vertical_1_2 ),
inference(factoring,[status(thm)],[p1310]) ).
cnf(f4,negated_conjecture,
~ horizontal_1_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered3_1_2) ).
fof(f4_nnf,plain,
~ horizontal_1_1,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
~ horizontal_1_1,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
~ horizontal_1_1,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1315,plain,
vertical_1_2,
inference(resolution,[status(thm)],[p1314,c4]) ).
cnf(f2,negated_conjecture,
~ vertical_1_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered2_1_2) ).
fof(f2_nnf,plain,
~ vertical_1_2,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
~ vertical_1_2,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
~ vertical_1_2,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p1316,plain,
$false,
inference(resolution,[status(thm)],[p1315,c2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ016-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 06:38:14 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 2.48/0.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.48/0.78 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------