%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ015-2.006 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.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:32:41 PM UTC 2026
% Result : Unsatisfiable 1.39s 1.27s
% Output : CNFRefutation 1.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 98
% Syntax : Number of formulae : 197 ( 9 unt; 0 def)
% Number of atoms : 433 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 548 ( 312 ~; 236 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 61 ( 60 usr; 61 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
~ horizontal_1_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered1_1_1) ).
fof(f2,negated_conjecture,
~ vertical_1_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered2_1_1) ).
fof(f3,negated_conjecture,
~ horizontal_6_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered3_6_6) ).
fof(f4,negated_conjecture,
~ vertical_5_6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered4_6_6) ).
fof(f5,negated_conjecture,
( horizontal_1_1
| vertical_1_2
| horizontal_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_2) ).
fof(f7,negated_conjecture,
( horizontal_1_3
| vertical_1_4
| horizontal_1_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_4) ).
fof(f9,negated_conjecture,
( horizontal_1_5
| vertical_1_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_6) ).
fof(f10,negated_conjecture,
( vertical_1_1
| vertical_2_1
| horizontal_2_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_1) ).
fof(f12,negated_conjecture,
( vertical_1_3
| horizontal_2_2
| vertical_2_3
| horizontal_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_3) ).
fof(f14,negated_conjecture,
( vertical_1_5
| horizontal_2_4
| vertical_2_5
| horizontal_2_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_5) ).
fof(f17,negated_conjecture,
( vertical_2_2
| horizontal_3_1
| vertical_3_2
| horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_2) ).
fof(f19,negated_conjecture,
( vertical_2_4
| horizontal_3_3
| vertical_3_4
| horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_4) ).
fof(f21,negated_conjecture,
( vertical_2_6
| horizontal_3_5
| vertical_3_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_6) ).
fof(f22,negated_conjecture,
( vertical_3_1
| vertical_4_1
| horizontal_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_1) ).
fof(f24,negated_conjecture,
( vertical_3_3
| horizontal_4_2
| vertical_4_3
| horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_3) ).
fof(f26,negated_conjecture,
( vertical_3_5
| horizontal_4_4
| vertical_4_5
| horizontal_4_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_5) ).
fof(f29,negated_conjecture,
( vertical_4_2
| horizontal_5_1
| vertical_5_2
| horizontal_5_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_2) ).
fof(f31,negated_conjecture,
( vertical_4_4
| horizontal_5_3
| vertical_5_4
| horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_4) ).
fof(f33,negated_conjecture,
( vertical_4_6
| horizontal_5_5
| vertical_5_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_6) ).
fof(f34,negated_conjecture,
( vertical_5_1
| horizontal_6_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_6_1) ).
fof(f36,negated_conjecture,
( vertical_5_3
| horizontal_6_2
| horizontal_6_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_6_3) ).
fof(f38,negated_conjecture,
( vertical_5_5
| horizontal_6_4
| horizontal_6_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_6_5) ).
fof(f42,negated_conjecture,
( ~ vertical_1_3
| ~ horizontal_1_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_1_3) ).
fof(f43,negated_conjecture,
( ~ horizontal_1_2
| ~ horizontal_1_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_1_3) ).
fof(f44,negated_conjecture,
( ~ horizontal_1_2
| ~ vertical_1_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_1_3) ).
fof(f48,negated_conjecture,
( ~ vertical_1_5
| ~ horizontal_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_1_5) ).
fof(f49,negated_conjecture,
( ~ horizontal_1_4
| ~ horizontal_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_1_5) ).
fof(f50,negated_conjecture,
( ~ horizontal_1_4
| ~ vertical_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_1_5) ).
fof(f55,negated_conjecture,
( ~ vertical_2_2
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_2_2) ).
fof(f56,negated_conjecture,
( ~ horizontal_2_1
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_2_2) ).
fof(f57,negated_conjecture,
( ~ vertical_1_2
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_2_2) ).
fof(f58,negated_conjecture,
( ~ horizontal_2_1
| ~ vertical_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_2) ).
fof(f59,negated_conjecture,
( ~ vertical_1_2
| ~ vertical_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_2) ).
fof(f60,negated_conjecture,
( ~ vertical_1_2
| ~ horizontal_2_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_2_2) ).
fof(f67,negated_conjecture,
( ~ vertical_2_4
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_2_4) ).
fof(f68,negated_conjecture,
( ~ horizontal_2_3
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_2_4) ).
fof(f69,negated_conjecture,
( ~ vertical_1_4
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_2_4) ).
fof(f70,negated_conjecture,
( ~ horizontal_2_3
| ~ vertical_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_4) ).
fof(f71,negated_conjecture,
( ~ vertical_1_4
| ~ vertical_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_4) ).
fof(f72,negated_conjecture,
( ~ vertical_1_4
| ~ horizontal_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_2_4) ).
fof(f79,negated_conjecture,
( ~ horizontal_2_5
| ~ vertical_2_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_6) ).
fof(f80,negated_conjecture,
( ~ vertical_1_6
| ~ vertical_2_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_6) ).
fof(f81,negated_conjecture,
( ~ vertical_1_6
| ~ horizontal_2_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_2_6) ).
fof(f82,negated_conjecture,
( ~ vertical_3_1
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_1) ).
fof(f83,negated_conjecture,
( ~ vertical_2_1
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_1) ).
fof(f84,negated_conjecture,
( ~ vertical_2_1
| ~ vertical_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_1) ).
fof(f91,negated_conjecture,
( ~ vertical_3_3
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_3) ).
fof(f92,negated_conjecture,
( ~ horizontal_3_2
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_3_3) ).
fof(f93,negated_conjecture,
( ~ vertical_2_3
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_3) ).
fof(f94,negated_conjecture,
( ~ horizontal_3_2
| ~ vertical_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_3_3) ).
fof(f95,negated_conjecture,
( ~ vertical_2_3
| ~ vertical_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_3) ).
fof(f96,negated_conjecture,
( ~ vertical_2_3
| ~ horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_3_3) ).
fof(f99,negated_conjecture,
( ~ vertical_2_4
| ~ horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_4) ).
fof(f103,negated_conjecture,
( ~ vertical_3_5
| ~ horizontal_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_5) ).
fof(f104,negated_conjecture,
( ~ horizontal_3_4
| ~ horizontal_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_3_5) ).
fof(f105,negated_conjecture,
( ~ vertical_2_5
| ~ horizontal_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_5) ).
fof(f106,negated_conjecture,
( ~ horizontal_3_4
| ~ vertical_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_3_5) ).
fof(f107,negated_conjecture,
( ~ vertical_2_5
| ~ vertical_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_5) ).
fof(f108,negated_conjecture,
( ~ vertical_2_5
| ~ horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_3_5) ).
fof(f115,negated_conjecture,
( ~ vertical_4_2
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_4_2) ).
fof(f116,negated_conjecture,
( ~ horizontal_4_1
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_4_2) ).
fof(f117,negated_conjecture,
( ~ vertical_3_2
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_4_2) ).
fof(f118,negated_conjecture,
( ~ horizontal_4_1
| ~ vertical_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_2) ).
fof(f119,negated_conjecture,
( ~ vertical_3_2
| ~ vertical_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_2) ).
fof(f120,negated_conjecture,
( ~ vertical_3_2
| ~ horizontal_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_2) ).
fof(f127,negated_conjecture,
( ~ vertical_4_4
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_4_4) ).
fof(f128,negated_conjecture,
( ~ horizontal_4_3
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_4_4) ).
fof(f129,negated_conjecture,
( ~ vertical_3_4
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_4_4) ).
fof(f130,negated_conjecture,
( ~ horizontal_4_3
| ~ vertical_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_4) ).
fof(f131,negated_conjecture,
( ~ vertical_3_4
| ~ vertical_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_4) ).
fof(f132,negated_conjecture,
( ~ vertical_3_4
| ~ horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_4) ).
fof(f139,negated_conjecture,
( ~ horizontal_4_5
| ~ vertical_4_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_6) ).
fof(f140,negated_conjecture,
( ~ vertical_3_6
| ~ vertical_4_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_6) ).
fof(f141,negated_conjecture,
( ~ vertical_3_6
| ~ horizontal_4_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_6) ).
fof(f142,negated_conjecture,
( ~ vertical_5_1
| ~ horizontal_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_5_1) ).
fof(f143,negated_conjecture,
( ~ vertical_4_1
| ~ horizontal_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_1) ).
fof(f144,negated_conjecture,
( ~ vertical_4_1
| ~ vertical_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_5_1) ).
fof(f151,negated_conjecture,
( ~ vertical_5_3
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_5_3) ).
fof(f152,negated_conjecture,
( ~ horizontal_5_2
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_3) ).
fof(f153,negated_conjecture,
( ~ vertical_4_3
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_3) ).
fof(f154,negated_conjecture,
( ~ horizontal_5_2
| ~ vertical_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_5_3) ).
fof(f155,negated_conjecture,
( ~ vertical_4_3
| ~ vertical_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_5_3) ).
fof(f156,negated_conjecture,
( ~ vertical_4_3
| ~ horizontal_5_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_5_3) ).
fof(f158,negated_conjecture,
( ~ horizontal_5_3
| ~ horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_4) ).
fof(f160,negated_conjecture,
( ~ horizontal_5_3
| ~ vertical_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_5_4) ).
fof(f163,negated_conjecture,
( ~ vertical_5_5
| ~ horizontal_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_5_5) ).
fof(f164,negated_conjecture,
( ~ horizontal_5_4
| ~ horizontal_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_5) ).
fof(f165,negated_conjecture,
( ~ vertical_4_5
| ~ horizontal_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_5) ).
fof(f166,negated_conjecture,
( ~ horizontal_5_4
| ~ vertical_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_5_5) ).
fof(f167,negated_conjecture,
( ~ vertical_4_5
| ~ vertical_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_5_5) ).
fof(f168,negated_conjecture,
( ~ vertical_4_5
| ~ horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_5_5) ).
fof(f173,negated_conjecture,
( ~ horizontal_6_1
| ~ horizontal_6_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_6_2) ).
fof(f174,negated_conjecture,
( ~ vertical_5_2
| ~ horizontal_6_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_6_2) ).
fof(f175,negated_conjecture,
( ~ vertical_5_2
| ~ horizontal_6_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_6_2) ).
fof(f176,negated_conjecture,
( ~ horizontal_6_2
| ~ horizontal_6_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_6_3) ).
fof(f179,negated_conjecture,
( ~ horizontal_6_3
| ~ horizontal_6_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_6_4) ).
fof(f180,negated_conjecture,
( ~ vertical_5_4
| ~ horizontal_6_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_6_4) ).
fof(f181,negated_conjecture,
( ~ vertical_5_4
| ~ horizontal_6_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_6_4) ).
tcf(c_233,negated_conjecture,
~ horizontal_1_1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_234,negated_conjecture,
~ vertical_1_1,
inference(cnf_transformation,[],[f2]) ).
tcf(c_235,negated_conjecture,
~ horizontal_6_5,
inference(cnf_transformation,[],[f3]) ).
tcf(c_236,negated_conjecture,
~ vertical_5_6,
inference(cnf_transformation,[],[f4]) ).
tcf(c_237,negated_conjecture,
( vertical_1_2
| horizontal_1_2
| horizontal_1_1 ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_239,negated_conjecture,
( vertical_1_4
| horizontal_1_4
| horizontal_1_3 ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_241,negated_conjecture,
( vertical_1_6
| horizontal_1_5 ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_242,negated_conjecture,
( vertical_2_1
| horizontal_2_1
| vertical_1_1 ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_244,negated_conjecture,
( vertical_2_3
| horizontal_2_3
| horizontal_2_2
| vertical_1_3 ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_246,negated_conjecture,
( vertical_2_5
| horizontal_2_5
| horizontal_2_4
| vertical_1_5 ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_249,negated_conjecture,
( vertical_3_2
| horizontal_3_2
| horizontal_3_1
| vertical_2_2 ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_251,negated_conjecture,
( vertical_3_4
| horizontal_3_4
| horizontal_3_3
| vertical_2_4 ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_253,negated_conjecture,
( vertical_3_6
| horizontal_3_5
| vertical_2_6 ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_254,negated_conjecture,
( vertical_4_1
| horizontal_4_1
| vertical_3_1 ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_256,negated_conjecture,
( vertical_4_3
| horizontal_4_3
| horizontal_4_2
| vertical_3_3 ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_258,negated_conjecture,
( vertical_4_5
| horizontal_4_5
| horizontal_4_4
| vertical_3_5 ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_261,negated_conjecture,
( vertical_5_2
| horizontal_5_2
| horizontal_5_1
| vertical_4_2 ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_263,negated_conjecture,
( vertical_5_4
| horizontal_5_4
| horizontal_5_3
| vertical_4_4 ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_265,negated_conjecture,
( horizontal_5_5
| vertical_4_6
| vertical_5_6 ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_266,negated_conjecture,
( horizontal_6_1
| vertical_5_1 ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_268,negated_conjecture,
( horizontal_6_3
| horizontal_6_2
| vertical_5_3 ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_270,negated_conjecture,
( horizontal_6_4
| vertical_5_5
| horizontal_6_5 ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_274,negated_conjecture,
( ~ vertical_1_3
| ~ horizontal_1_3 ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_275,negated_conjecture,
( ~ horizontal_1_3
| ~ horizontal_1_2 ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_276,negated_conjecture,
( ~ vertical_1_3
| ~ horizontal_1_2 ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_280,negated_conjecture,
( ~ vertical_1_5
| ~ horizontal_1_5 ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_281,negated_conjecture,
( ~ horizontal_1_5
| ~ horizontal_1_4 ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_282,negated_conjecture,
( ~ vertical_1_5
| ~ horizontal_1_4 ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_287,negated_conjecture,
( ~ vertical_2_2
| ~ horizontal_2_2 ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_288,negated_conjecture,
( ~ horizontal_2_2
| ~ horizontal_2_1 ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_289,negated_conjecture,
( ~ horizontal_2_2
| ~ vertical_1_2 ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_290,negated_conjecture,
( ~ vertical_2_2
| ~ horizontal_2_1 ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_291,negated_conjecture,
( ~ vertical_2_2
| ~ vertical_1_2 ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_292,negated_conjecture,
( ~ horizontal_2_1
| ~ vertical_1_2 ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_299,negated_conjecture,
( ~ vertical_2_4
| ~ horizontal_2_4 ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_300,negated_conjecture,
( ~ horizontal_2_4
| ~ horizontal_2_3 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_301,negated_conjecture,
( ~ horizontal_2_4
| ~ vertical_1_4 ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_302,negated_conjecture,
( ~ vertical_2_4
| ~ horizontal_2_3 ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_303,negated_conjecture,
( ~ vertical_2_4
| ~ vertical_1_4 ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_304,negated_conjecture,
( ~ horizontal_2_3
| ~ vertical_1_4 ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_311,negated_conjecture,
( ~ vertical_2_6
| ~ horizontal_2_5 ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_312,negated_conjecture,
( ~ vertical_2_6
| ~ vertical_1_6 ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_313,negated_conjecture,
( ~ horizontal_2_5
| ~ vertical_1_6 ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_314,negated_conjecture,
( ~ vertical_3_1
| ~ horizontal_3_1 ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_315,negated_conjecture,
( ~ horizontal_3_1
| ~ vertical_2_1 ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_316,negated_conjecture,
( ~ vertical_3_1
| ~ vertical_2_1 ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_323,negated_conjecture,
( ~ vertical_3_3
| ~ horizontal_3_3 ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_324,negated_conjecture,
( ~ horizontal_3_3
| ~ horizontal_3_2 ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_325,negated_conjecture,
( ~ horizontal_3_3
| ~ vertical_2_3 ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_326,negated_conjecture,
( ~ vertical_3_3
| ~ horizontal_3_2 ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_327,negated_conjecture,
( ~ vertical_3_3
| ~ vertical_2_3 ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_328,negated_conjecture,
( ~ horizontal_3_2
| ~ vertical_2_3 ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_331,negated_conjecture,
( ~ horizontal_3_4
| ~ vertical_2_4 ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_335,negated_conjecture,
( ~ vertical_3_5
| ~ horizontal_3_5 ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_336,negated_conjecture,
( ~ horizontal_3_5
| ~ horizontal_3_4 ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_337,negated_conjecture,
( ~ horizontal_3_5
| ~ vertical_2_5 ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_338,negated_conjecture,
( ~ vertical_3_5
| ~ horizontal_3_4 ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_339,negated_conjecture,
( ~ vertical_3_5
| ~ vertical_2_5 ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_340,negated_conjecture,
( ~ horizontal_3_4
| ~ vertical_2_5 ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_347,negated_conjecture,
( ~ vertical_4_2
| ~ horizontal_4_2 ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_348,negated_conjecture,
( ~ horizontal_4_2
| ~ horizontal_4_1 ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_349,negated_conjecture,
( ~ horizontal_4_2
| ~ vertical_3_2 ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_350,negated_conjecture,
( ~ vertical_4_2
| ~ horizontal_4_1 ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_351,negated_conjecture,
( ~ vertical_4_2
| ~ vertical_3_2 ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_352,negated_conjecture,
( ~ horizontal_4_1
| ~ vertical_3_2 ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_359,negated_conjecture,
( ~ vertical_4_4
| ~ horizontal_4_4 ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_360,negated_conjecture,
( ~ horizontal_4_4
| ~ horizontal_4_3 ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_361,negated_conjecture,
( ~ horizontal_4_4
| ~ vertical_3_4 ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_362,negated_conjecture,
( ~ vertical_4_4
| ~ horizontal_4_3 ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_363,negated_conjecture,
( ~ vertical_4_4
| ~ vertical_3_4 ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_364,negated_conjecture,
( ~ horizontal_4_3
| ~ vertical_3_4 ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_371,negated_conjecture,
( ~ vertical_4_6
| ~ horizontal_4_5 ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_372,negated_conjecture,
( ~ vertical_4_6
| ~ vertical_3_6 ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_373,negated_conjecture,
( ~ horizontal_4_5
| ~ vertical_3_6 ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_374,negated_conjecture,
( ~ vertical_5_1
| ~ horizontal_5_1 ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_375,negated_conjecture,
( ~ horizontal_5_1
| ~ vertical_4_1 ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_376,negated_conjecture,
( ~ vertical_5_1
| ~ vertical_4_1 ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_383,negated_conjecture,
( ~ vertical_5_3
| ~ horizontal_5_3 ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_384,negated_conjecture,
( ~ horizontal_5_3
| ~ horizontal_5_2 ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_385,negated_conjecture,
( ~ horizontal_5_3
| ~ vertical_4_3 ),
inference(cnf_transformation,[],[f153]) ).
tcf(c_386,negated_conjecture,
( ~ vertical_5_3
| ~ horizontal_5_2 ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_387,negated_conjecture,
( ~ vertical_5_3
| ~ vertical_4_3 ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_388,negated_conjecture,
( ~ horizontal_5_2
| ~ vertical_4_3 ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_390,negated_conjecture,
( ~ horizontal_5_4
| ~ horizontal_5_3 ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_392,negated_conjecture,
( ~ vertical_5_4
| ~ horizontal_5_3 ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_395,negated_conjecture,
( ~ vertical_5_5
| ~ horizontal_5_5 ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_396,negated_conjecture,
( ~ horizontal_5_5
| ~ horizontal_5_4 ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_397,negated_conjecture,
( ~ horizontal_5_5
| ~ vertical_4_5 ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_398,negated_conjecture,
( ~ vertical_5_5
| ~ horizontal_5_4 ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_399,negated_conjecture,
( ~ vertical_5_5
| ~ vertical_4_5 ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_400,negated_conjecture,
( ~ horizontal_5_4
| ~ vertical_4_5 ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_405,negated_conjecture,
( ~ horizontal_6_2
| ~ horizontal_6_1 ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_406,negated_conjecture,
( ~ horizontal_6_2
| ~ vertical_5_2 ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_407,negated_conjecture,
( ~ horizontal_6_1
| ~ vertical_5_2 ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_408,negated_conjecture,
( ~ horizontal_6_3
| ~ horizontal_6_2 ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_411,negated_conjecture,
( ~ horizontal_6_4
| ~ horizontal_6_3 ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_412,negated_conjecture,
( ~ horizontal_6_4
| ~ vertical_5_4 ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_413,negated_conjecture,
( ~ horizontal_6_3
| ~ vertical_5_4 ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_417,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_244,c_246,c_249,c_251,c_256,c_258,c_261,c_263,c_274,c_275,c_276,c_280,c_281,c_282,c_287,c_288,c_289,c_290,c_291,c_292,c_299,c_300,c_301,c_302,c_303,c_304,c_311,c_312,c_313,c_314,c_315,c_316,c_323,c_324,c_325,c_326,c_327,c_328,c_331,c_335,c_336,c_337,c_338,c_339,c_340,c_347,c_348,c_349,c_350,c_351,c_352,c_359,c_360,c_361,c_362,c_363,c_364,c_371,c_372,c_373,c_374,c_375,c_376,c_383,c_384,c_385,c_386,c_387,c_388,c_390,c_392,c_395,c_396,c_397,c_398,c_399,c_400,c_405,c_406,c_407,c_408,c_411,c_412,c_413,c_237,c_239,c_242,c_253,c_254,c_265,c_268,c_270,c_233,c_234,c_235,c_236,c_241,c_266]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ015-2.006 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n003.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 06:40:35 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.42 % Proving...
% 1.39/1.27 % SZS status Started for theBenchmark.p
% 1.39/1.27 % SZS status Unsatisfiable for theBenchmark.p
% 1.39/1.27
% 1.39/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.39/1.27
% 1.39/1.27 % ------ iProver source info
% 1.39/1.27
% 1.39/1.27 % git: date: 2026-07-19 20:42:38 +0200
% 1.39/1.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.39/1.27 % git: non_committed_changes: false
% 1.39/1.27
% 1.39/1.27 % ------ Parsing...% successful
% 1.39/1.27
% 1.39/1.27
% 1.39/1.27 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 1.39/1.27 %
% 1.39/1.27
% 1.39/1.27 % ------ Preprocessing...%
% 1.39/1.27
% 1.39/1.27 % SZS status Unsatisfiable for theBenchmark.p
% 1.39/1.27
% 1.39/1.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.39/1.27
% 1.39/1.27
%------------------------------------------------------------------------------