%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PUZ015-2.006 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:21:05 AM UTC 2026
% Result : Unsatisfiable 69.58s 33.59s
% Output : Refutation 70.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 118
% Number of leaves : 93
% Syntax : Number of formulae : 1375 ( 31 unt; 0 typ; 0 def)
% Number of atoms : 6852 ( 688 equ; 0 cnn)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 6973 (2872 ~;4101 |; 0 &; 0 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 63 ( 60 usr; 62 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(horizontal_1_1_decl,type,
horizontal_1_1: $o ).
thf(vertical_1_1_decl,type,
vertical_1_1: $o ).
thf(horizontal_6_5_decl,type,
horizontal_6_5: $o ).
thf(vertical_5_6_decl,type,
vertical_5_6: $o ).
thf(horizontal_1_2_decl,type,
horizontal_1_2: $o ).
thf(vertical_1_2_decl,type,
vertical_1_2: $o ).
thf(horizontal_1_3_decl,type,
horizontal_1_3: $o ).
thf(vertical_1_3_decl,type,
vertical_1_3: $o ).
thf(horizontal_1_4_decl,type,
horizontal_1_4: $o ).
thf(vertical_1_4_decl,type,
vertical_1_4: $o ).
thf(horizontal_1_5_decl,type,
horizontal_1_5: $o ).
thf(vertical_1_5_decl,type,
vertical_1_5: $o ).
thf(vertical_1_6_decl,type,
vertical_1_6: $o ).
thf(horizontal_2_1_decl,type,
horizontal_2_1: $o ).
thf(vertical_2_1_decl,type,
vertical_2_1: $o ).
thf(horizontal_2_2_decl,type,
horizontal_2_2: $o ).
thf(vertical_2_2_decl,type,
vertical_2_2: $o ).
thf(horizontal_2_3_decl,type,
horizontal_2_3: $o ).
thf(vertical_2_3_decl,type,
vertical_2_3: $o ).
thf(horizontal_2_4_decl,type,
horizontal_2_4: $o ).
thf(vertical_2_4_decl,type,
vertical_2_4: $o ).
thf(horizontal_2_5_decl,type,
horizontal_2_5: $o ).
thf(vertical_2_5_decl,type,
vertical_2_5: $o ).
thf(vertical_2_6_decl,type,
vertical_2_6: $o ).
thf(horizontal_3_1_decl,type,
horizontal_3_1: $o ).
thf(vertical_3_1_decl,type,
vertical_3_1: $o ).
thf(horizontal_3_2_decl,type,
horizontal_3_2: $o ).
thf(vertical_3_2_decl,type,
vertical_3_2: $o ).
thf(horizontal_3_3_decl,type,
horizontal_3_3: $o ).
thf(vertical_3_3_decl,type,
vertical_3_3: $o ).
thf(horizontal_3_4_decl,type,
horizontal_3_4: $o ).
thf(vertical_3_4_decl,type,
vertical_3_4: $o ).
thf(horizontal_3_5_decl,type,
horizontal_3_5: $o ).
thf(vertical_3_5_decl,type,
vertical_3_5: $o ).
thf(vertical_3_6_decl,type,
vertical_3_6: $o ).
thf(horizontal_4_1_decl,type,
horizontal_4_1: $o ).
thf(vertical_4_1_decl,type,
vertical_4_1: $o ).
thf(horizontal_4_2_decl,type,
horizontal_4_2: $o ).
thf(vertical_4_2_decl,type,
vertical_4_2: $o ).
thf(horizontal_4_3_decl,type,
horizontal_4_3: $o ).
thf(vertical_4_3_decl,type,
vertical_4_3: $o ).
thf(horizontal_4_4_decl,type,
horizontal_4_4: $o ).
thf(vertical_4_4_decl,type,
vertical_4_4: $o ).
thf(horizontal_4_5_decl,type,
horizontal_4_5: $o ).
thf(vertical_4_5_decl,type,
vertical_4_5: $o ).
thf(vertical_4_6_decl,type,
vertical_4_6: $o ).
thf(horizontal_5_1_decl,type,
horizontal_5_1: $o ).
thf(vertical_5_1_decl,type,
vertical_5_1: $o ).
thf(horizontal_5_2_decl,type,
horizontal_5_2: $o ).
thf(vertical_5_2_decl,type,
vertical_5_2: $o ).
thf(horizontal_5_3_decl,type,
horizontal_5_3: $o ).
thf(vertical_5_3_decl,type,
vertical_5_3: $o ).
thf(horizontal_5_4_decl,type,
horizontal_5_4: $o ).
thf(vertical_5_4_decl,type,
vertical_5_4: $o ).
thf(horizontal_5_5_decl,type,
horizontal_5_5: $o ).
thf(vertical_5_5_decl,type,
vertical_5_5: $o ).
thf(horizontal_6_1_decl,type,
horizontal_6_1: $o ).
thf(horizontal_6_2_decl,type,
horizontal_6_2: $o ).
thf(horizontal_6_3_decl,type,
horizontal_6_3: $o ).
thf(horizontal_6_4_decl,type,
horizontal_6_4: $o ).
thf(19,negated_conjecture,
( vertical_2_4
| horizontal_3_3
| vertical_3_4
| horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_4) ).
thf(350,plain,
( vertical_2_4
| horizontal_3_3
| vertical_3_4
| horizontal_3_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(463,plain,
( vertical_2_4
| horizontal_3_3
| vertical_3_4
| horizontal_3_4 ),
inference(cnf,[status(esa)],[350]) ).
thf(7,negated_conjecture,
( horizontal_1_3
| vertical_1_4
| horizontal_1_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_4) ).
thf(290,plain,
( horizontal_1_3
| vertical_1_4
| horizontal_1_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(516,plain,
( horizontal_1_3
| vertical_1_4
| horizontal_1_4 ),
inference(cnf,[status(esa)],[290]) ).
thf(71,negated_conjecture,
( ~ vertical_1_4
| ~ vertical_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_4) ).
thf(278,plain,
( ~ vertical_1_4
| ~ vertical_2_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(482,plain,
( ~ vertical_1_4
| ~ vertical_2_4 ),
inference(cnf,[status(esa)],[278]) ).
thf(763,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ $true
| ~ vertical_2_4
| horizontal_1_3
| horizontal_1_4 ),
inference(paramod_ordered,[status(thm)],[516,482]) ).
thf(764,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ vertical_2_4
| horizontal_1_3
| horizontal_1_4 ),
inference(simp,[status(thm)],[763]) ).
thf(765,plain,
( ~ vertical_2_4
| horizontal_1_3
| horizontal_1_4 ),
inference(pattern_uni,[status(thm)],[764:[]]) ).
thf(17,negated_conjecture,
( vertical_2_2
| horizontal_3_1
| vertical_3_2
| horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_2) ).
thf(268,plain,
( vertical_2_2
| horizontal_3_1
| vertical_3_2
| horizontal_3_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(534,plain,
( vertical_2_2
| horizontal_3_1
| vertical_3_2
| horizontal_3_2 ),
inference(cnf,[status(esa)],[268]) ).
thf(26,negated_conjecture,
( vertical_3_5
| horizontal_4_4
| vertical_4_5
| horizontal_4_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_5) ).
thf(331,plain,
( vertical_3_5
| horizontal_4_4
| vertical_4_5
| horizontal_4_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(500,plain,
( vertical_3_5
| horizontal_4_4
| vertical_4_5
| horizontal_4_5 ),
inference(cnf,[status(esa)],[331]) ).
thf(29,negated_conjecture,
( vertical_4_2
| horizontal_5_1
| vertical_5_2
| horizontal_5_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_2) ).
thf(214,plain,
( vertical_4_2
| horizontal_5_1
| vertical_5_2
| horizontal_5_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(522,plain,
( vertical_4_2
| horizontal_5_1
| vertical_5_2
| horizontal_5_2 ),
inference(cnf,[status(esa)],[214]) ).
thf(31,negated_conjecture,
( vertical_4_4
| horizontal_5_3
| vertical_5_4
| horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_4) ).
thf(318,plain,
( vertical_4_4
| horizontal_5_3
| vertical_5_4
| horizontal_5_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(470,plain,
( vertical_4_4
| horizontal_5_3
| vertical_5_4
| horizontal_5_4 ),
inference(cnf,[status(esa)],[318]) ).
thf(38,negated_conjecture,
( vertical_5_5
| horizontal_6_4
| horizontal_6_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_6_5) ).
thf(238,plain,
( vertical_5_5
| horizontal_6_4
| horizontal_6_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(399,plain,
( vertical_5_5
| horizontal_6_4
| horizontal_6_5 ),
inference(cnf,[status(esa)],[238]) ).
thf(3,negated_conjecture,
~ horizontal_6_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered3_6_6) ).
thf(301,plain,
~ horizontal_6_5,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(384,plain,
~ horizontal_6_5,
inference(polarity_switch,[status(thm)],[301]) ).
thf(578,plain,
( vertical_5_5
| horizontal_6_4
| $false ),
inference(rewrite,[status(thm)],[399,384]) ).
thf(579,plain,
( vertical_5_5
| horizontal_6_4 ),
inference(simp,[status(thm)],[578]) ).
thf(180,negated_conjecture,
( ~ vertical_5_4
| ~ horizontal_6_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_6_4) ).
thf(267,plain,
( ~ vertical_5_4
| ~ horizontal_6_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(487,plain,
( ~ vertical_5_4
| ~ horizontal_6_4 ),
inference(cnf,[status(esa)],[267]) ).
thf(733,plain,
( ( horizontal_6_4 != horizontal_6_4 )
| ~ vertical_5_4
| ~ $true
| vertical_5_5 ),
inference(paramod_ordered,[status(thm)],[579,487]) ).
thf(734,plain,
( ( horizontal_6_4 != horizontal_6_4 )
| ~ vertical_5_4
| vertical_5_5 ),
inference(simp,[status(thm)],[733]) ).
thf(735,plain,
( ~ vertical_5_4
| vertical_5_5 ),
inference(pattern_uni,[status(thm)],[734:[]]) ).
thf(167,negated_conjecture,
( ~ vertical_4_5
| ~ vertical_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_5_5) ).
thf(303,plain,
( ~ vertical_4_5
| ~ vertical_5_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(471,plain,
( ~ vertical_4_5
| ~ vertical_5_5 ),
inference(cnf,[status(esa)],[303]) ).
thf(1064,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ vertical_4_5
| ~ $true
| ~ vertical_5_4 ),
inference(paramod_ordered,[status(thm)],[735,471]) ).
thf(1065,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ vertical_4_5
| ~ vertical_5_4 ),
inference(simp,[status(thm)],[1064]) ).
thf(1066,plain,
( ~ vertical_4_5
| ~ vertical_5_4 ),
inference(pattern_uni,[status(thm)],[1065:[]]) ).
thf(1082,plain,
( ( vertical_5_4 != vertical_5_4 )
| ~ vertical_4_5
| ~ $true
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(paramod_ordered,[status(thm)],[470,1066]) ).
thf(1083,plain,
( ( vertical_5_4 != vertical_5_4 )
| ~ vertical_4_5
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(simp,[status(thm)],[1082]) ).
thf(1084,plain,
( ~ vertical_4_5
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(pattern_uni,[status(thm)],[1083:[]]) ).
thf(168,negated_conjecture,
( ~ vertical_4_5
| ~ horizontal_5_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_5_5) ).
thf(345,plain,
( ~ vertical_4_5
| ~ horizontal_5_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(478,plain,
( ~ vertical_4_5
| ~ horizontal_5_4 ),
inference(cnf,[status(esa)],[345]) ).
thf(2201,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| ~ vertical_4_5
| ~ $true
| ~ vertical_4_5
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[1084,478]) ).
thf(2202,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| ~ vertical_4_5
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[2201]) ).
thf(2203,plain,
( ~ vertical_4_5
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[2202:[]]) ).
thf(36,negated_conjecture,
( vertical_5_3
| horizontal_6_2
| horizontal_6_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_6_3) ).
thf(344,plain,
( vertical_5_3
| horizontal_6_2
| horizontal_6_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(387,plain,
( vertical_5_3
| horizontal_6_2
| horizontal_6_3 ),
inference(cnf,[status(esa)],[344]) ).
thf(179,negated_conjecture,
( ~ horizontal_6_3
| ~ horizontal_6_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_6_4) ).
thf(216,plain,
( ~ horizontal_6_3
| ~ horizontal_6_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(397,plain,
( ~ horizontal_6_3
| ~ horizontal_6_4 ),
inference(cnf,[status(esa)],[216]) ).
thf(580,plain,
( ( horizontal_6_4 != horizontal_6_4 )
| ~ horizontal_6_3
| ~ $true
| vertical_5_5 ),
inference(paramod_ordered,[status(thm)],[579,397]) ).
thf(581,plain,
( ( horizontal_6_4 != horizontal_6_4 )
| ~ horizontal_6_3
| vertical_5_5 ),
inference(simp,[status(thm)],[580]) ).
thf(582,plain,
( ~ horizontal_6_3
| vertical_5_5 ),
inference(pattern_uni,[status(thm)],[581:[]]) ).
thf(1031,plain,
( ( horizontal_6_3 != horizontal_6_3 )
| ~ $true
| vertical_5_5
| vertical_5_3
| horizontal_6_2 ),
inference(paramod_ordered,[status(thm)],[387,582]) ).
thf(1032,plain,
( ( horizontal_6_3 != horizontal_6_3 )
| vertical_5_5
| vertical_5_3
| horizontal_6_2 ),
inference(simp,[status(thm)],[1031]) ).
thf(1033,plain,
( vertical_5_5
| vertical_5_3
| horizontal_6_2 ),
inference(pattern_uni,[status(thm)],[1032:[]]) ).
thf(174,negated_conjecture,
( ~ vertical_5_2
| ~ horizontal_6_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_6_2) ).
thf(197,plain,
( ~ vertical_5_2
| ~ horizontal_6_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(428,plain,
( ~ vertical_5_2
| ~ horizontal_6_2 ),
inference(cnf,[status(esa)],[197]) ).
thf(1088,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| ~ vertical_5_2
| ~ $true
| vertical_5_5
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1033,428]) ).
thf(1089,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| ~ vertical_5_2
| vertical_5_5
| vertical_5_3 ),
inference(simp,[status(thm)],[1088]) ).
thf(1090,plain,
( ~ vertical_5_2
| vertical_5_5
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1089:[]]) ).
thf(1328,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ vertical_4_5
| ~ $true
| ~ vertical_5_2
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1090,471]) ).
thf(1329,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ vertical_4_5
| ~ vertical_5_2
| vertical_5_3 ),
inference(simp,[status(thm)],[1328]) ).
thf(1330,plain,
( ~ vertical_4_5
| ~ vertical_5_2
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1329:[]]) ).
thf(151,negated_conjecture,
( ~ vertical_5_3
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_5_3) ).
thf(343,plain,
( ~ vertical_5_3
| ~ horizontal_5_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(448,plain,
( ~ vertical_5_3
| ~ horizontal_5_3 ),
inference(cnf,[status(esa)],[343]) ).
thf(1472,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ $true
| ~ horizontal_5_3
| ~ vertical_4_5
| ~ vertical_5_2 ),
inference(paramod_ordered,[status(thm)],[1330,448]) ).
thf(1473,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_3
| ~ vertical_4_5
| ~ vertical_5_2 ),
inference(simp,[status(thm)],[1472]) ).
thf(1474,plain,
( ~ horizontal_5_3
| ~ vertical_4_5
| ~ vertical_5_2 ),
inference(pattern_uni,[status(thm)],[1473:[]]) ).
thf(2240,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ $true
| ~ vertical_4_5
| ~ vertical_5_2
| ~ vertical_4_5
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[2203,1474]) ).
thf(2241,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_5_2
| ~ vertical_4_5
| vertical_4_4 ),
inference(simp,[status(thm)],[2240]) ).
thf(2242,plain,
( ~ vertical_5_2
| ~ vertical_4_5
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[2241:[]]) ).
thf(2285,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ $true
| ~ vertical_4_5
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(paramod_ordered,[status(thm)],[522,2242]) ).
thf(2286,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_5
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(simp,[status(thm)],[2285]) ).
thf(2287,plain,
( ~ vertical_4_5
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(pattern_uni,[status(thm)],[2286:[]]) ).
thf(152,negated_conjecture,
( ~ horizontal_5_2
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_3) ).
thf(211,plain,
( ~ horizontal_5_2
| ~ horizontal_5_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(402,plain,
( ~ horizontal_5_2
| ~ horizontal_5_3 ),
inference(cnf,[status(esa)],[211]) ).
thf(2228,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ horizontal_5_2
| ~ $true
| ~ vertical_4_5
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[2203,402]) ).
thf(2229,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ horizontal_5_2
| ~ vertical_4_5
| vertical_4_4 ),
inference(simp,[status(thm)],[2228]) ).
thf(2230,plain,
( ~ horizontal_5_2
| ~ vertical_4_5
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[2229:[]]) ).
thf(7433,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ $true
| ~ vertical_4_5
| vertical_4_4
| ~ vertical_4_5
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[2287,2230]) ).
thf(7434,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_5
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[7433]) ).
thf(7435,plain,
( ~ vertical_4_5
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[7434:[]]) ).
thf(34,negated_conjecture,
( vertical_5_1
| horizontal_6_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_6_1) ).
thf(271,plain,
( vertical_5_1
| horizontal_6_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(472,plain,
( vertical_5_1
| horizontal_6_1 ),
inference(cnf,[status(esa)],[271]) ).
thf(173,negated_conjecture,
( ~ horizontal_6_1
| ~ horizontal_6_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_6_2) ).
thf(253,plain,
( ~ horizontal_6_1
| ~ horizontal_6_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(403,plain,
( ~ horizontal_6_1
| ~ horizontal_6_2 ),
inference(cnf,[status(esa)],[253]) ).
thf(571,plain,
( ( horizontal_6_1 != horizontal_6_1 )
| ~ $true
| ~ horizontal_6_2
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[472,403]) ).
thf(572,plain,
( ( horizontal_6_1 != horizontal_6_1 )
| ~ horizontal_6_2
| vertical_5_1 ),
inference(simp,[status(thm)],[571]) ).
thf(573,plain,
( ~ horizontal_6_2
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[572:[]]) ).
thf(1097,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| ~ $true
| vertical_5_1
| vertical_5_5
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1033,573]) ).
thf(1098,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| vertical_5_1
| vertical_5_5
| vertical_5_3 ),
inference(simp,[status(thm)],[1097]) ).
thf(1099,plain,
( vertical_5_1
| vertical_5_5
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1098:[]]) ).
thf(1190,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ vertical_4_5
| ~ $true
| vertical_5_1
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1099,471]) ).
thf(1191,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ vertical_4_5
| vertical_5_1
| vertical_5_3 ),
inference(simp,[status(thm)],[1190]) ).
thf(1192,plain,
( ~ vertical_4_5
| vertical_5_1
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1191:[]]) ).
thf(1382,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ $true
| ~ horizontal_5_3
| ~ vertical_4_5
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[1192,448]) ).
thf(1383,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_3
| ~ vertical_4_5
| vertical_5_1 ),
inference(simp,[status(thm)],[1382]) ).
thf(1384,plain,
( ~ horizontal_5_3
| ~ vertical_4_5
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[1383:[]]) ).
thf(2243,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ $true
| ~ vertical_4_5
| vertical_5_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[2203,1384]) ).
thf(2244,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| vertical_5_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(simp,[status(thm)],[2243]) ).
thf(2245,plain,
( vertical_5_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[2244:[]]) ).
thf(142,negated_conjecture,
( ~ vertical_5_1
| ~ horizontal_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_5_1) ).
thf(195,plain,
( ~ vertical_5_1
| ~ horizontal_5_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(536,plain,
( ~ vertical_5_1
| ~ horizontal_5_1 ),
inference(cnf,[status(esa)],[195]) ).
thf(2300,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ $true
| ~ horizontal_5_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[2245,536]) ).
thf(2301,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ horizontal_5_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(simp,[status(thm)],[2300]) ).
thf(2302,plain,
( ~ horizontal_5_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[2301:[]]) ).
thf(7490,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ $true
| ~ vertical_4_5
| vertical_4_4
| ~ vertical_4_5
| vertical_4_4
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[7435,2302]) ).
thf(7491,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_5
| vertical_4_4
| vertical_4_2 ),
inference(simp,[status(thm)],[7490]) ).
thf(7492,plain,
( ~ vertical_4_5
| vertical_4_4
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[7491:[]]) ).
thf(7496,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ $true
| vertical_4_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,7492]) ).
thf(7497,plain,
( ( vertical_4_5 != vertical_4_5 )
| vertical_4_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[7496]) ).
thf(7498,plain,
( vertical_4_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[7497:[]]) ).
thf(33,negated_conjecture,
( vertical_4_6
| horizontal_5_5
| vertical_5_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_5_6) ).
thf(236,plain,
( vertical_4_6
| horizontal_5_5
| vertical_5_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(462,plain,
( vertical_4_6
| horizontal_5_5
| vertical_5_6 ),
inference(cnf,[status(esa)],[236]) ).
thf(4,negated_conjecture,
~ vertical_5_6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered4_6_6) ).
thf(352,plain,
~ vertical_5_6,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(373,plain,
~ vertical_5_6,
inference(polarity_switch,[status(thm)],[352]) ).
thf(676,plain,
( vertical_4_6
| horizontal_5_5
| $false ),
inference(rewrite,[status(thm)],[462,373]) ).
thf(677,plain,
( vertical_4_6
| horizontal_5_5 ),
inference(simp,[status(thm)],[676]) ).
thf(163,negated_conjecture,
( ~ vertical_5_5
| ~ horizontal_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_5_5) ).
thf(358,plain,
( ~ vertical_5_5
| ~ horizontal_5_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(535,plain,
( ~ vertical_5_5
| ~ horizontal_5_5 ),
inference(cnf,[status(esa)],[358]) ).
thf(914,plain,
( ( horizontal_5_5 != horizontal_5_5 )
| ~ vertical_5_5
| ~ $true
| vertical_4_6 ),
inference(paramod_ordered,[status(thm)],[677,535]) ).
thf(915,plain,
( ( horizontal_5_5 != horizontal_5_5 )
| ~ vertical_5_5
| vertical_4_6 ),
inference(simp,[status(thm)],[914]) ).
thf(916,plain,
( ~ vertical_5_5
| vertical_4_6 ),
inference(pattern_uni,[status(thm)],[915:[]]) ).
thf(1118,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ $true
| vertical_4_6
| ~ vertical_5_4 ),
inference(paramod_ordered,[status(thm)],[735,916]) ).
thf(1119,plain,
( ( vertical_5_5 != vertical_5_5 )
| vertical_4_6
| ~ vertical_5_4 ),
inference(simp,[status(thm)],[1118]) ).
thf(1120,plain,
( vertical_4_6
| ~ vertical_5_4 ),
inference(pattern_uni,[status(thm)],[1119:[]]) ).
thf(1136,plain,
( ( vertical_5_4 != vertical_5_4 )
| vertical_4_6
| ~ $true
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(paramod_ordered,[status(thm)],[470,1120]) ).
thf(1137,plain,
( ( vertical_5_4 != vertical_5_4 )
| vertical_4_6
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(simp,[status(thm)],[1136]) ).
thf(1138,plain,
( vertical_4_6
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(pattern_uni,[status(thm)],[1137:[]]) ).
thf(164,negated_conjecture,
( ~ horizontal_5_4
| ~ horizontal_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_5_5) ).
thf(215,plain,
( ~ horizontal_5_4
| ~ horizontal_5_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(547,plain,
( ~ horizontal_5_4
| ~ horizontal_5_5 ),
inference(cnf,[status(esa)],[215]) ).
thf(998,plain,
( ( horizontal_5_5 != horizontal_5_5 )
| ~ horizontal_5_4
| ~ $true
| vertical_4_6 ),
inference(paramod_ordered,[status(thm)],[677,547]) ).
thf(999,plain,
( ( horizontal_5_5 != horizontal_5_5 )
| ~ horizontal_5_4
| vertical_4_6 ),
inference(simp,[status(thm)],[998]) ).
thf(1000,plain,
( ~ horizontal_5_4
| vertical_4_6 ),
inference(pattern_uni,[status(thm)],[999:[]]) ).
thf(1769,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| ~ $true
| vertical_4_6
| vertical_4_6
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[1138,1000]) ).
thf(1770,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| vertical_4_6
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[1769]) ).
thf(1771,plain,
( vertical_4_6
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[1770:[]]) ).
thf(1325,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ $true
| vertical_4_6
| ~ vertical_5_2
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1090,916]) ).
thf(1326,plain,
( ( vertical_5_5 != vertical_5_5 )
| vertical_4_6
| ~ vertical_5_2
| vertical_5_3 ),
inference(simp,[status(thm)],[1325]) ).
thf(1327,plain,
( vertical_4_6
| ~ vertical_5_2
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1326:[]]) ).
thf(1535,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ $true
| ~ horizontal_5_3
| vertical_4_6
| ~ vertical_5_2 ),
inference(paramod_ordered,[status(thm)],[1327,448]) ).
thf(1536,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_3
| vertical_4_6
| ~ vertical_5_2 ),
inference(simp,[status(thm)],[1535]) ).
thf(1537,plain,
( ~ horizontal_5_3
| vertical_4_6
| ~ vertical_5_2 ),
inference(pattern_uni,[status(thm)],[1536:[]]) ).
thf(1808,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ $true
| vertical_4_6
| ~ vertical_5_2
| vertical_4_6
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1771,1537]) ).
thf(1809,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_5_2
| vertical_4_6
| vertical_4_4 ),
inference(simp,[status(thm)],[1808]) ).
thf(1810,plain,
( ~ vertical_5_2
| vertical_4_6
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1809:[]]) ).
thf(1859,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ $true
| vertical_4_6
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(paramod_ordered,[status(thm)],[522,1810]) ).
thf(1860,plain,
( ( vertical_5_2 != vertical_5_2 )
| vertical_4_6
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(simp,[status(thm)],[1859]) ).
thf(1861,plain,
( vertical_4_6
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(pattern_uni,[status(thm)],[1860:[]]) ).
thf(1793,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ horizontal_5_2
| ~ $true
| vertical_4_6
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1771,402]) ).
thf(1794,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ horizontal_5_2
| vertical_4_6
| vertical_4_4 ),
inference(simp,[status(thm)],[1793]) ).
thf(1795,plain,
( ~ horizontal_5_2
| vertical_4_6
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1794:[]]) ).
thf(4187,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ $true
| vertical_4_6
| vertical_4_4
| vertical_4_6
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1861,1795]) ).
thf(4188,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| vertical_4_6
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[4187]) ).
thf(4189,plain,
( vertical_4_6
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[4188:[]]) ).
thf(1187,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ $true
| vertical_4_6
| vertical_5_1
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1099,916]) ).
thf(1188,plain,
( ( vertical_5_5 != vertical_5_5 )
| vertical_4_6
| vertical_5_1
| vertical_5_3 ),
inference(simp,[status(thm)],[1187]) ).
thf(1189,plain,
( vertical_4_6
| vertical_5_1
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1188:[]]) ).
thf(1271,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ $true
| ~ horizontal_5_3
| vertical_4_6
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[1189,448]) ).
thf(1272,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_3
| vertical_4_6
| vertical_5_1 ),
inference(simp,[status(thm)],[1271]) ).
thf(1273,plain,
( ~ horizontal_5_3
| vertical_4_6
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[1272:[]]) ).
thf(1790,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ $true
| vertical_4_6
| vertical_5_1
| vertical_4_6
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1771,1273]) ).
thf(1791,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| vertical_5_1
| vertical_4_6
| vertical_4_4 ),
inference(simp,[status(thm)],[1790]) ).
thf(1792,plain,
( vertical_5_1
| vertical_4_6
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1791:[]]) ).
thf(1850,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ $true
| ~ horizontal_5_1
| vertical_4_6
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1792,536]) ).
thf(1851,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ horizontal_5_1
| vertical_4_6
| vertical_4_4 ),
inference(simp,[status(thm)],[1850]) ).
thf(1852,plain,
( ~ horizontal_5_1
| vertical_4_6
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1851:[]]) ).
thf(4286,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ $true
| vertical_4_6
| vertical_4_4
| vertical_4_6
| vertical_4_4
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4189,1852]) ).
thf(4287,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| vertical_4_6
| vertical_4_4
| vertical_4_2 ),
inference(simp,[status(thm)],[4286]) ).
thf(4288,plain,
( vertical_4_6
| vertical_4_4
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[4287:[]]) ).
thf(139,negated_conjecture,
( ~ horizontal_4_5
| ~ vertical_4_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_6) ).
thf(334,plain,
( ~ horizontal_4_5
| ~ vertical_4_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(419,plain,
( ~ horizontal_4_5
| ~ vertical_4_6 ),
inference(cnf,[status(esa)],[334]) ).
thf(4304,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ $true
| vertical_4_4
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4288,419]) ).
thf(4305,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| vertical_4_4
| vertical_4_2 ),
inference(simp,[status(thm)],[4304]) ).
thf(4306,plain,
( ~ horizontal_4_5
| vertical_4_4
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[4305:[]]) ).
thf(8432,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ $true
| vertical_4_4
| vertical_4_2
| vertical_4_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[7498,4306]) ).
thf(8433,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| vertical_4_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[8432]) ).
thf(8434,plain,
( vertical_4_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[8433:[]]) ).
thf(131,negated_conjecture,
( ~ vertical_3_4
| ~ vertical_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_4) ).
thf(362,plain,
( ~ vertical_3_4
| ~ vertical_4_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(468,plain,
( ~ vertical_3_4
| ~ vertical_4_4 ),
inference(cnf,[status(esa)],[362]) ).
thf(8522,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ $true
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[8434,468]) ).
thf(8523,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[8522]) ).
thf(8524,plain,
( ~ vertical_3_4
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[8523:[]]) ).
thf(129,negated_conjecture,
( ~ vertical_3_4
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_4_4) ).
thf(255,plain,
( ~ vertical_3_4
| ~ horizontal_4_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(489,plain,
( ~ vertical_3_4
| ~ horizontal_4_4 ),
inference(cnf,[status(esa)],[255]) ).
thf(8570,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_4
| vertical_4_2
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[8524,489]) ).
thf(8571,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_3_4
| vertical_4_2
| vertical_3_5 ),
inference(simp,[status(thm)],[8570]) ).
thf(8572,plain,
( ~ vertical_3_4
| vertical_4_2
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[8571:[]]) ).
thf(119,negated_conjecture,
( ~ vertical_3_2
| ~ vertical_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_2) ).
thf(341,plain,
( ~ vertical_3_2
| ~ vertical_4_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(533,plain,
( ~ vertical_3_2
| ~ vertical_4_2 ),
inference(cnf,[status(esa)],[341]) ).
thf(8621,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_4
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[8572,533]) ).
thf(8622,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ vertical_3_4
| vertical_3_5 ),
inference(simp,[status(thm)],[8621]) ).
thf(8623,plain,
( ~ vertical_3_2
| ~ vertical_3_4
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[8622:[]]) ).
thf(21,negated_conjecture,
( vertical_2_6
| horizontal_3_5
| vertical_3_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_3_6) ).
thf(239,plain,
( vertical_2_6
| horizontal_3_5
| vertical_3_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(538,plain,
( vertical_2_6
| horizontal_3_5
| vertical_3_6 ),
inference(cnf,[status(esa)],[239]) ).
thf(140,negated_conjecture,
( ~ vertical_3_6
| ~ vertical_4_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_4_6) ).
thf(294,plain,
( ~ vertical_3_6
| ~ vertical_4_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(532,plain,
( ~ vertical_3_6
| ~ vertical_4_6 ),
inference(cnf,[status(esa)],[294]) ).
thf(4313,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| vertical_4_4
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4288,532]) ).
thf(4314,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| vertical_4_4
| vertical_4_2 ),
inference(simp,[status(thm)],[4313]) ).
thf(4315,plain,
( ~ vertical_3_6
| vertical_4_4
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[4314:[]]) ).
thf(4337,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_6
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4315,468]) ).
thf(4338,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_4_2 ),
inference(simp,[status(thm)],[4337]) ).
thf(4339,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[4338:[]]) ).
thf(4367,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(paramod_ordered,[status(thm)],[4339,533]) ).
thf(4368,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(simp,[status(thm)],[4367]) ).
thf(4369,plain,
( ~ vertical_3_2
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(pattern_uni,[status(thm)],[4368:[]]) ).
thf(4406,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| ~ vertical_3_4
| ~ $true
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,4369]) ).
thf(4407,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| ~ vertical_3_4
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4406]) ).
thf(4408,plain,
( ~ vertical_3_2
| ~ vertical_3_4
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4407:[]]) ).
thf(103,negated_conjecture,
( ~ vertical_3_5
| ~ horizontal_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_5) ).
thf(293,plain,
( ~ vertical_3_5
| ~ horizontal_3_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(406,plain,
( ~ vertical_3_5
| ~ horizontal_3_5 ),
inference(cnf,[status(esa)],[293]) ).
thf(5219,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ $true
| ~ vertical_3_2
| ~ vertical_3_4
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[4408,406]) ).
thf(5220,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ vertical_3_2
| ~ vertical_3_4
| vertical_2_6 ),
inference(simp,[status(thm)],[5219]) ).
thf(5221,plain,
( ~ vertical_3_5
| ~ vertical_3_2
| ~ vertical_3_4
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5220:[]]) ).
thf(8675,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ $true
| ~ vertical_3_2
| ~ vertical_3_4
| vertical_2_6
| ~ vertical_3_2
| ~ vertical_3_4 ),
inference(paramod_ordered,[status(thm)],[8623,5221]) ).
thf(8676,plain,
( ( vertical_3_5 != vertical_3_5 )
| vertical_2_6
| ~ vertical_3_2
| ~ vertical_3_4 ),
inference(simp,[status(thm)],[8675]) ).
thf(8677,plain,
( vertical_2_6
| ~ vertical_3_2
| ~ vertical_3_4 ),
inference(pattern_uni,[status(thm)],[8676:[]]) ).
thf(8804,plain,
( ( vertical_3_4 != vertical_3_4 )
| vertical_2_6
| ~ vertical_3_2
| ~ $true
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(paramod_ordered,[status(thm)],[463,8677]) ).
thf(8805,plain,
( ( vertical_3_4 != vertical_3_4 )
| vertical_2_6
| ~ vertical_3_2
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(simp,[status(thm)],[8804]) ).
thf(8806,plain,
( vertical_2_6
| ~ vertical_3_2
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(pattern_uni,[status(thm)],[8805:[]]) ).
thf(165,negated_conjecture,
( ~ vertical_4_5
| ~ horizontal_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_5) ).
thf(235,plain,
( ~ vertical_4_5
| ~ horizontal_5_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(520,plain,
( ~ vertical_4_5
| ~ horizontal_5_5 ),
inference(cnf,[status(esa)],[235]) ).
thf(859,plain,
( ( horizontal_5_5 != horizontal_5_5 )
| ~ vertical_4_5
| ~ $true
| vertical_4_6 ),
inference(paramod_ordered,[status(thm)],[677,520]) ).
thf(860,plain,
( ( horizontal_5_5 != horizontal_5_5 )
| ~ vertical_4_5
| vertical_4_6 ),
inference(simp,[status(thm)],[859]) ).
thf(861,plain,
( ~ vertical_4_5
| vertical_4_6 ),
inference(pattern_uni,[status(thm)],[860:[]]) ).
thf(1109,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_4_5 ),
inference(paramod_ordered,[status(thm)],[861,532]) ).
thf(1110,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ vertical_4_5 ),
inference(simp,[status(thm)],[1109]) ).
thf(1111,plain,
( ~ vertical_3_6
| ~ vertical_4_5 ),
inference(pattern_uni,[status(thm)],[1110:[]]) ).
thf(1130,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_3_6
| ~ $true
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,1111]) ).
thf(1131,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_3_6
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[1130]) ).
thf(1132,plain,
( ~ vertical_3_6
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[1131:[]]) ).
thf(141,negated_conjecture,
( ~ vertical_3_6
| ~ horizontal_4_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_6) ).
thf(248,plain,
( ~ vertical_3_6
| ~ horizontal_4_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(414,plain,
( ~ vertical_3_6
| ~ horizontal_4_5 ),
inference(cnf,[status(esa)],[248]) ).
thf(2321,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_3_6
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[1132,414]) ).
thf(2322,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_3_6
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[2321]) ).
thf(2323,plain,
( ~ vertical_3_6
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[2322:[]]) ).
thf(127,negated_conjecture,
( ~ vertical_4_4
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_4_4) ).
thf(317,plain,
( ~ vertical_4_4
| ~ horizontal_4_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(434,plain,
( ~ vertical_4_4
| ~ horizontal_4_4 ),
inference(cnf,[status(esa)],[317]) ).
thf(2381,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_4
| ~ $true
| ~ vertical_3_6
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[2323,434]) ).
thf(2382,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_4
| ~ vertical_3_6
| vertical_3_5 ),
inference(simp,[status(thm)],[2381]) ).
thf(2383,plain,
( ~ vertical_4_4
| ~ vertical_3_6
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[2382:[]]) ).
thf(4358,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ $true
| ~ vertical_3_6
| vertical_3_5
| ~ vertical_3_6
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4315,2383]) ).
thf(4359,plain,
( ( vertical_4_4 != vertical_4_4 )
| vertical_3_5
| ~ vertical_3_6
| vertical_4_2 ),
inference(simp,[status(thm)],[4358]) ).
thf(4360,plain,
( vertical_3_5
| ~ vertical_3_6
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[4359:[]]) ).
thf(4490,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| vertical_3_5
| ~ vertical_3_6 ),
inference(paramod_ordered,[status(thm)],[4360,533]) ).
thf(4491,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| vertical_3_5
| ~ vertical_3_6 ),
inference(simp,[status(thm)],[4490]) ).
thf(4492,plain,
( ~ vertical_3_2
| vertical_3_5
| ~ vertical_3_6 ),
inference(pattern_uni,[status(thm)],[4491:[]]) ).
thf(4595,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| vertical_3_5
| ~ $true
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,4492]) ).
thf(4596,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| vertical_3_5
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4595]) ).
thf(4597,plain,
( ~ vertical_3_2
| vertical_3_5
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4596:[]]) ).
thf(106,negated_conjecture,
( ~ horizontal_3_4
| ~ vertical_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_3_5) ).
thf(217,plain,
( ~ horizontal_3_4
| ~ vertical_3_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(380,plain,
( ~ horizontal_3_4
| ~ vertical_3_5 ),
inference(cnf,[status(esa)],[217]) ).
thf(5342,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_4
| ~ $true
| ~ vertical_3_2
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[4597,380]) ).
thf(5343,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_4
| ~ vertical_3_2
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[5342]) ).
thf(5344,plain,
( ~ horizontal_3_4
| ~ vertical_3_2
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[5343:[]]) ).
thf(104,negated_conjecture,
( ~ horizontal_3_4
| ~ horizontal_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_3_5) ).
thf(329,plain,
( ~ horizontal_3_4
| ~ horizontal_3_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(430,plain,
( ~ horizontal_3_4
| ~ horizontal_3_5 ),
inference(cnf,[status(esa)],[329]) ).
thf(6398,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ horizontal_3_4
| ~ $true
| ~ horizontal_3_4
| ~ vertical_3_2
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[5344,430]) ).
thf(6399,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ horizontal_3_4
| ~ vertical_3_2
| vertical_2_6 ),
inference(simp,[status(thm)],[6398]) ).
thf(6400,plain,
( ~ horizontal_3_4
| ~ vertical_3_2
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[6399:[]]) ).
thf(22013,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| ~ $true
| ~ vertical_3_2
| vertical_2_6
| vertical_2_6
| ~ vertical_3_2
| vertical_2_4
| horizontal_3_3 ),
inference(paramod_ordered,[status(thm)],[8806,6400]) ).
thf(22014,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| vertical_2_6
| ~ vertical_3_2
| vertical_2_4
| horizontal_3_3 ),
inference(simp,[status(thm)],[22013]) ).
thf(22015,plain,
( vertical_2_6
| ~ vertical_3_2
| vertical_2_4
| horizontal_3_3 ),
inference(pattern_uni,[status(thm)],[22014:[]]) ).
thf(24,negated_conjecture,
( vertical_3_3
| horizontal_4_2
| vertical_4_3
| horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_3) ).
thf(199,plain,
( vertical_3_3
| horizontal_4_2
| vertical_4_3
| horizontal_4_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(499,plain,
( vertical_3_3
| horizontal_4_2
| vertical_4_3
| horizontal_4_3 ),
inference(cnf,[status(esa)],[199]) ).
thf(155,negated_conjecture,
( ~ vertical_4_3
| ~ vertical_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_5_3) ).
thf(297,plain,
( ~ vertical_4_3
| ~ vertical_5_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(421,plain,
( ~ vertical_4_3
| ~ vertical_5_3 ),
inference(cnf,[status(esa)],[297]) ).
thf(1532,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ $true
| vertical_4_6
| ~ vertical_5_2 ),
inference(paramod_ordered,[status(thm)],[1327,421]) ).
thf(1533,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| vertical_4_6
| ~ vertical_5_2 ),
inference(simp,[status(thm)],[1532]) ).
thf(1534,plain,
( ~ vertical_4_3
| vertical_4_6
| ~ vertical_5_2 ),
inference(pattern_uni,[status(thm)],[1533:[]]) ).
thf(1685,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_3
| vertical_4_6
| ~ $true
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(paramod_ordered,[status(thm)],[522,1534]) ).
thf(1686,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_3
| vertical_4_6
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(simp,[status(thm)],[1685]) ).
thf(1687,plain,
( ~ vertical_4_3
| vertical_4_6
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(pattern_uni,[status(thm)],[1686:[]]) ).
thf(156,negated_conjecture,
( ~ vertical_4_3
| ~ horizontal_5_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_5_3) ).
thf(244,plain,
( ~ vertical_4_3
| ~ horizontal_5_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(443,plain,
( ~ vertical_4_3
| ~ horizontal_5_2 ),
inference(cnf,[status(esa)],[244]) ).
thf(5375,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_3
| vertical_4_6
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1687,443]) ).
thf(5376,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| vertical_4_6
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[5375]) ).
thf(5377,plain,
( ~ vertical_4_3
| vertical_4_6
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[5376:[]]) ).
thf(1268,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ $true
| vertical_4_6
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[1189,421]) ).
thf(1269,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| vertical_4_6
| vertical_5_1 ),
inference(simp,[status(thm)],[1268]) ).
thf(1270,plain,
( ~ vertical_4_3
| vertical_4_6
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[1269:[]]) ).
thf(1445,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ $true
| ~ horizontal_5_1
| ~ vertical_4_3
| vertical_4_6 ),
inference(paramod_ordered,[status(thm)],[1270,536]) ).
thf(1446,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ horizontal_5_1
| ~ vertical_4_3
| vertical_4_6 ),
inference(simp,[status(thm)],[1445]) ).
thf(1447,plain,
( ~ horizontal_5_1
| ~ vertical_4_3
| vertical_4_6 ),
inference(pattern_uni,[status(thm)],[1446:[]]) ).
thf(6425,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ $true
| ~ vertical_4_3
| vertical_4_6
| ~ vertical_4_3
| vertical_4_6
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[5377,1447]) ).
thf(6426,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_3
| vertical_4_6
| vertical_4_2 ),
inference(simp,[status(thm)],[6425]) ).
thf(6427,plain,
( ~ vertical_4_3
| vertical_4_6
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[6426:[]]) ).
thf(6494,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_4_3
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[6427,532]) ).
thf(6495,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ vertical_4_3
| vertical_4_2 ),
inference(simp,[status(thm)],[6494]) ).
thf(6496,plain,
( ~ vertical_3_6
| ~ vertical_4_3
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[6495:[]]) ).
thf(6515,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_6
| ~ $true
| vertical_4_2
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,6496]) ).
thf(6516,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_6
| vertical_4_2
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[6515]) ).
thf(6517,plain,
( ~ vertical_3_6
| vertical_4_2
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[6516:[]]) ).
thf(130,negated_conjecture,
( ~ horizontal_4_3
| ~ vertical_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_4) ).
thf(299,plain,
( ~ horizontal_4_3
| ~ vertical_4_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(485,plain,
( ~ horizontal_4_3
| ~ vertical_4_4 ),
inference(cnf,[status(esa)],[299]) ).
thf(4346,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ vertical_3_6
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4315,485]) ).
thf(4347,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ vertical_3_6
| vertical_4_2 ),
inference(simp,[status(thm)],[4346]) ).
thf(4348,plain,
( ~ horizontal_4_3
| ~ vertical_3_6
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[4347:[]]) ).
thf(17489,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ $true
| ~ vertical_3_6
| vertical_4_2
| ~ vertical_3_6
| vertical_4_2
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[6517,4348]) ).
thf(17490,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_6
| vertical_4_2
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[17489]) ).
thf(17491,plain,
( ~ vertical_3_6
| vertical_4_2
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[17490:[]]) ).
thf(17579,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[17491,533]) ).
thf(17580,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[17579]) ).
thf(17581,plain,
( ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[17580:[]]) ).
thf(117,negated_conjecture,
( ~ vertical_3_2
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_4_2) ).
thf(232,plain,
( ~ vertical_3_2
| ~ horizontal_4_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(550,plain,
( ~ vertical_3_2
| ~ horizontal_4_2 ),
inference(cnf,[status(esa)],[232]) ).
thf(17615,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[17581,550]) ).
thf(17616,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_3 ),
inference(simp,[status(thm)],[17615]) ).
thf(17617,plain,
( ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[17616:[]]) ).
thf(17690,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| ~ $true
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,17617]) ).
thf(17691,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[17690]) ).
thf(17692,plain,
( ~ vertical_3_2
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[17691:[]]) ).
thf(1469,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_5
| ~ vertical_5_2 ),
inference(paramod_ordered,[status(thm)],[1330,421]) ).
thf(1470,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ vertical_4_5
| ~ vertical_5_2 ),
inference(simp,[status(thm)],[1469]) ).
thf(1471,plain,
( ~ vertical_4_3
| ~ vertical_4_5
| ~ vertical_5_2 ),
inference(pattern_uni,[status(thm)],[1470:[]]) ).
thf(1610,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_3
| ~ vertical_4_5
| ~ $true
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(paramod_ordered,[status(thm)],[522,1471]) ).
thf(1611,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(simp,[status(thm)],[1610]) ).
thf(1612,plain,
( ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(pattern_uni,[status(thm)],[1611:[]]) ).
thf(4772,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1612,443]) ).
thf(4773,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[4772]) ).
thf(4774,plain,
( ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[4773:[]]) ).
thf(1379,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_5
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[1192,421]) ).
thf(1380,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_5_1 ),
inference(simp,[status(thm)],[1379]) ).
thf(1381,plain,
( ~ vertical_4_3
| ~ vertical_4_5
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[1380:[]]) ).
thf(1601,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ $true
| ~ horizontal_5_1
| ~ vertical_4_3
| ~ vertical_4_5 ),
inference(paramod_ordered,[status(thm)],[1381,536]) ).
thf(1602,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ horizontal_5_1
| ~ vertical_4_3
| ~ vertical_4_5 ),
inference(simp,[status(thm)],[1601]) ).
thf(1603,plain,
( ~ horizontal_5_1
| ~ vertical_4_3
| ~ vertical_4_5 ),
inference(pattern_uni,[status(thm)],[1602:[]]) ).
thf(5585,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ $true
| ~ vertical_4_3
| ~ vertical_4_5
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4774,1603]) ).
thf(5586,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2 ),
inference(simp,[status(thm)],[5585]) ).
thf(5587,plain,
( ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[5586:[]]) ).
thf(5603,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_3
| ~ $true
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,5587]) ).
thf(5604,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[5603]) ).
thf(5605,plain,
( ~ vertical_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[5604:[]]) ).
thf(6485,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ $true
| ~ vertical_4_3
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[6427,419]) ).
thf(6486,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ vertical_4_3
| vertical_4_2 ),
inference(simp,[status(thm)],[6485]) ).
thf(6487,plain,
( ~ horizontal_4_5
| ~ vertical_4_3
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[6486:[]]) ).
thf(15656,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ $true
| ~ vertical_4_3
| vertical_4_2
| ~ vertical_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[5605,6487]) ).
thf(15657,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[15656]) ).
thf(15658,plain,
( ~ vertical_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[15657:[]]) ).
thf(181,negated_conjecture,
( ~ vertical_5_4
| ~ horizontal_6_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_6_4) ).
thf(283,plain,
( ~ vertical_5_4
| ~ horizontal_6_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(537,plain,
( ~ vertical_5_4
| ~ horizontal_6_3 ),
inference(cnf,[status(esa)],[283]) ).
thf(941,plain,
( ( horizontal_6_3 != horizontal_6_3 )
| ~ vertical_5_4
| ~ $true
| vertical_5_3
| horizontal_6_2 ),
inference(paramod_ordered,[status(thm)],[387,537]) ).
thf(942,plain,
( ( horizontal_6_3 != horizontal_6_3 )
| ~ vertical_5_4
| vertical_5_3
| horizontal_6_2 ),
inference(simp,[status(thm)],[941]) ).
thf(943,plain,
( ~ vertical_5_4
| vertical_5_3
| horizontal_6_2 ),
inference(pattern_uni,[status(thm)],[942:[]]) ).
thf(1292,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| ~ vertical_5_2
| ~ $true
| ~ vertical_5_4
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[943,428]) ).
thf(1293,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| ~ vertical_5_2
| ~ vertical_5_4
| vertical_5_3 ),
inference(simp,[status(thm)],[1292]) ).
thf(1294,plain,
( ~ vertical_5_2
| ~ vertical_5_4
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1293:[]]) ).
thf(1415,plain,
( ( vertical_5_4 != vertical_5_4 )
| ~ vertical_5_2
| ~ $true
| vertical_5_3
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(paramod_ordered,[status(thm)],[470,1294]) ).
thf(1416,plain,
( ( vertical_5_4 != vertical_5_4 )
| ~ vertical_5_2
| vertical_5_3
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(simp,[status(thm)],[1415]) ).
thf(1417,plain,
( ~ vertical_5_2
| vertical_5_3
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(pattern_uni,[status(thm)],[1416:[]]) ).
thf(166,negated_conjecture,
( ~ horizontal_5_4
| ~ vertical_5_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_5_5) ).
thf(262,plain,
( ~ horizontal_5_4
| ~ vertical_5_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(526,plain,
( ~ horizontal_5_4
| ~ vertical_5_5 ),
inference(cnf,[status(esa)],[262]) ).
thf(1331,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ horizontal_5_4
| ~ $true
| ~ vertical_5_2
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1090,526]) ).
thf(1332,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ horizontal_5_4
| ~ vertical_5_2
| vertical_5_3 ),
inference(simp,[status(thm)],[1331]) ).
thf(1333,plain,
( ~ horizontal_5_4
| ~ vertical_5_2
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1332:[]]) ).
thf(3542,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| ~ $true
| ~ vertical_5_2
| vertical_5_3
| ~ vertical_5_2
| vertical_5_3
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[1417,1333]) ).
thf(3543,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| ~ vertical_5_2
| vertical_5_3
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[3542]) ).
thf(3544,plain,
( ~ vertical_5_2
| vertical_5_3
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[3543:[]]) ).
thf(4238,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_5_2
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[3544,421]) ).
thf(4239,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ vertical_5_2
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[4238]) ).
thf(4240,plain,
( ~ vertical_4_3
| ~ vertical_5_2
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[4239:[]]) ).
thf(153,negated_conjecture,
( ~ vertical_4_3
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_3) ).
thf(196,plain,
( ~ vertical_4_3
| ~ horizontal_5_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(389,plain,
( ~ vertical_4_3
| ~ horizontal_5_3 ),
inference(cnf,[status(esa)],[196]) ).
thf(5093,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_3
| ~ vertical_5_2
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[4240,389]) ).
thf(5094,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| ~ vertical_5_2
| vertical_4_4 ),
inference(simp,[status(thm)],[5093]) ).
thf(5095,plain,
( ~ vertical_4_3
| ~ vertical_5_2
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[5094:[]]) ).
thf(5150,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_3
| ~ $true
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(paramod_ordered,[status(thm)],[522,5095]) ).
thf(5151,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ vertical_4_3
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(simp,[status(thm)],[5150]) ).
thf(5152,plain,
( ~ vertical_4_3
| vertical_4_4
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(pattern_uni,[status(thm)],[5151:[]]) ).
thf(15101,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_3
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[5152,443]) ).
thf(15102,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[15101]) ).
thf(15103,plain,
( ~ vertical_4_3
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[15102:[]]) ).
thf(1304,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| ~ $true
| vertical_5_1
| ~ vertical_5_4
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[943,573]) ).
thf(1305,plain,
( ( horizontal_6_2 != horizontal_6_2 )
| vertical_5_1
| ~ vertical_5_4
| vertical_5_3 ),
inference(simp,[status(thm)],[1304]) ).
thf(1306,plain,
( vertical_5_1
| ~ vertical_5_4
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1305:[]]) ).
thf(1460,plain,
( ( vertical_5_4 != vertical_5_4 )
| vertical_5_1
| ~ $true
| vertical_5_3
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(paramod_ordered,[status(thm)],[470,1306]) ).
thf(1461,plain,
( ( vertical_5_4 != vertical_5_4 )
| vertical_5_1
| vertical_5_3
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(simp,[status(thm)],[1460]) ).
thf(1462,plain,
( vertical_5_1
| vertical_5_3
| vertical_4_4
| horizontal_5_3
| horizontal_5_4 ),
inference(pattern_uni,[status(thm)],[1461:[]]) ).
thf(1193,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ horizontal_5_4
| ~ $true
| vertical_5_1
| vertical_5_3 ),
inference(paramod_ordered,[status(thm)],[1099,526]) ).
thf(1194,plain,
( ( vertical_5_5 != vertical_5_5 )
| ~ horizontal_5_4
| vertical_5_1
| vertical_5_3 ),
inference(simp,[status(thm)],[1193]) ).
thf(1195,plain,
( ~ horizontal_5_4
| vertical_5_1
| vertical_5_3 ),
inference(pattern_uni,[status(thm)],[1194:[]]) ).
thf(3632,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| ~ $true
| vertical_5_1
| vertical_5_3
| vertical_5_1
| vertical_5_3
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[1462,1195]) ).
thf(3633,plain,
( ( horizontal_5_4 != horizontal_5_4 )
| vertical_5_1
| vertical_5_3
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[3632]) ).
thf(3634,plain,
( vertical_5_1
| vertical_5_3
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[3633:[]]) ).
thf(3701,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| ~ $true
| vertical_5_1
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[3634,421]) ).
thf(3702,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ vertical_4_3
| vertical_5_1
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[3701]) ).
thf(3703,plain,
( ~ vertical_4_3
| vertical_5_1
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[3702:[]]) ).
thf(4679,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_3
| vertical_5_1
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[3703,389]) ).
thf(4680,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| vertical_5_1
| vertical_4_4 ),
inference(simp,[status(thm)],[4679]) ).
thf(4681,plain,
( ~ vertical_4_3
| vertical_5_1
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[4680:[]]) ).
thf(4742,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ $true
| ~ horizontal_5_1
| ~ vertical_4_3
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[4681,536]) ).
thf(4743,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ horizontal_5_1
| ~ vertical_4_3
| vertical_4_4 ),
inference(simp,[status(thm)],[4742]) ).
thf(4744,plain,
( ~ horizontal_5_1
| ~ vertical_4_3
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[4743:[]]) ).
thf(15215,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ $true
| ~ vertical_4_3
| vertical_4_4
| ~ vertical_4_3
| vertical_4_4
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[15103,4744]) ).
thf(15216,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_3
| vertical_4_4
| vertical_4_2 ),
inference(simp,[status(thm)],[15215]) ).
thf(15217,plain,
( ~ vertical_4_3
| vertical_4_4
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[15216:[]]) ).
thf(15293,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ $true
| ~ horizontal_4_4
| ~ vertical_4_3
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[15217,434]) ).
thf(15294,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_4
| ~ vertical_4_3
| vertical_4_2 ),
inference(simp,[status(thm)],[15293]) ).
thf(15295,plain,
( ~ horizontal_4_4
| ~ vertical_4_3
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[15294:[]]) ).
thf(15731,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ $true
| ~ vertical_4_3
| vertical_4_2
| ~ vertical_4_3
| vertical_4_2
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[15658,15295]) ).
thf(15732,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_3
| vertical_4_2
| vertical_3_5 ),
inference(simp,[status(thm)],[15731]) ).
thf(15733,plain,
( ~ vertical_4_3
| vertical_4_2
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[15732:[]]) ).
thf(15803,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ $true
| vertical_4_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,15733]) ).
thf(15804,plain,
( ( vertical_4_3 != vertical_4_3 )
| vertical_4_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[15803]) ).
thf(15805,plain,
( vertical_4_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[15804:[]]) ).
thf(8528,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ $true
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[8434,485]) ).
thf(8529,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[8528]) ).
thf(8530,plain,
( ~ horizontal_4_3
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[8529:[]]) ).
thf(128,negated_conjecture,
( ~ horizontal_4_3
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_4_4) ).
thf(259,plain,
( ~ horizontal_4_3
| ~ horizontal_4_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(457,plain,
( ~ horizontal_4_3
| ~ horizontal_4_4 ),
inference(cnf,[status(esa)],[259]) ).
thf(8900,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ horizontal_4_3
| vertical_4_2
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[8530,457]) ).
thf(8901,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ horizontal_4_3
| vertical_4_2
| vertical_3_5 ),
inference(simp,[status(thm)],[8900]) ).
thf(8902,plain,
( ~ horizontal_4_3
| vertical_4_2
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[8901:[]]) ).
thf(15818,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ $true
| vertical_4_2
| vertical_3_5
| vertical_4_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[15805,8902]) ).
thf(15819,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| vertical_4_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[15818]) ).
thf(15820,plain,
( vertical_4_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[15819:[]]) ).
thf(15878,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[15820,533]) ).
thf(15879,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[15878]) ).
thf(15880,plain,
( ~ vertical_3_2
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[15879:[]]) ).
thf(15908,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_2
| vertical_3_5
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[15880,550]) ).
thf(15909,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_2
| vertical_3_5
| vertical_3_3 ),
inference(simp,[status(thm)],[15908]) ).
thf(15910,plain,
( ~ vertical_3_2
| vertical_3_5
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[15909:[]]) ).
thf(16004,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ $true
| ~ horizontal_3_5
| ~ vertical_3_2
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[15910,406]) ).
thf(16005,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_5
| ~ vertical_3_2
| vertical_3_3 ),
inference(simp,[status(thm)],[16004]) ).
thf(16006,plain,
( ~ horizontal_3_5
| ~ vertical_3_2
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[16005:[]]) ).
thf(17975,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ $true
| ~ vertical_3_2
| vertical_3_3
| ~ vertical_3_2
| vertical_3_3
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[17692,16006]) ).
thf(17976,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_2
| vertical_3_3
| vertical_2_6 ),
inference(simp,[status(thm)],[17975]) ).
thf(17977,plain,
( ~ vertical_3_2
| vertical_3_3
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[17976:[]]) ).
thf(91,negated_conjecture,
( ~ vertical_3_3
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_3) ).
thf(295,plain,
( ~ vertical_3_3
| ~ horizontal_3_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(494,plain,
( ~ vertical_3_3
| ~ horizontal_3_3 ),
inference(cnf,[status(esa)],[295]) ).
thf(17999,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ $true
| ~ horizontal_3_3
| ~ vertical_3_2
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[17977,494]) ).
thf(18000,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_3
| ~ vertical_3_2
| vertical_2_6 ),
inference(simp,[status(thm)],[17999]) ).
thf(18001,plain,
( ~ horizontal_3_3
| ~ vertical_3_2
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[18000:[]]) ).
thf(22061,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ $true
| ~ vertical_3_2
| vertical_2_6
| vertical_2_6
| ~ vertical_3_2
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[22015,18001]) ).
thf(22062,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| vertical_2_6
| ~ vertical_3_2
| vertical_2_4 ),
inference(simp,[status(thm)],[22061]) ).
thf(22063,plain,
( vertical_2_6
| ~ vertical_3_2
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[22062:[]]) ).
thf(22121,plain,
( ( vertical_3_2 != vertical_3_2 )
| vertical_2_6
| ~ $true
| vertical_2_4
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(paramod_ordered,[status(thm)],[534,22063]) ).
thf(22122,plain,
( ( vertical_3_2 != vertical_3_2 )
| vertical_2_6
| vertical_2_4
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(simp,[status(thm)],[22121]) ).
thf(22123,plain,
( vertical_2_6
| vertical_2_4
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(pattern_uni,[status(thm)],[22122:[]]) ).
thf(2210,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| ~ $true
| ~ vertical_4_5
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[2203,389]) ).
thf(2211,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_4 ),
inference(simp,[status(thm)],[2210]) ).
thf(2212,plain,
( ~ vertical_4_3
| ~ vertical_4_5
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[2211:[]]) ).
thf(2252,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_3
| ~ $true
| vertical_4_4
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,2212]) ).
thf(2253,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_3
| vertical_4_4
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[2252]) ).
thf(2254,plain,
( ~ vertical_4_3
| vertical_4_4
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[2253:[]]) ).
thf(1781,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| ~ $true
| vertical_4_6
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1771,389]) ).
thf(1782,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ vertical_4_3
| vertical_4_6
| vertical_4_4 ),
inference(simp,[status(thm)],[1781]) ).
thf(1783,plain,
( ~ vertical_4_3
| vertical_4_6
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1782:[]]) ).
thf(1814,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ $true
| ~ vertical_4_3
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1783,419]) ).
thf(1815,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ vertical_4_3
| vertical_4_4 ),
inference(simp,[status(thm)],[1814]) ).
thf(1816,plain,
( ~ horizontal_4_5
| ~ vertical_4_3
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1815:[]]) ).
thf(7202,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ $true
| ~ vertical_4_3
| vertical_4_4
| ~ vertical_4_3
| vertical_4_4
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[2254,1816]) ).
thf(7203,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_4_3
| vertical_4_4
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[7202]) ).
thf(7204,plain,
( ~ vertical_4_3
| vertical_4_4
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[7203:[]]) ).
thf(7205,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[7204,468]) ).
thf(7206,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[7205]) ).
thf(7207,plain,
( ~ vertical_3_4
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[7206:[]]) ).
thf(7259,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_4
| ~ vertical_4_3
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[7207,489]) ).
thf(7260,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_3_4
| ~ vertical_4_3
| vertical_3_5 ),
inference(simp,[status(thm)],[7259]) ).
thf(7261,plain,
( ~ vertical_3_4
| ~ vertical_4_3
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[7260:[]]) ).
thf(7307,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_4
| ~ $true
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,7261]) ).
thf(7308,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_4
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[7307]) ).
thf(7309,plain,
( ~ vertical_3_4
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[7308:[]]) ).
thf(132,negated_conjecture,
( ~ vertical_3_4
| ~ horizontal_4_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_4) ).
thf(222,plain,
( ~ vertical_3_4
| ~ horizontal_4_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(548,plain,
( ~ vertical_3_4
| ~ horizontal_4_3 ),
inference(cnf,[status(esa)],[222]) ).
thf(20369,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_4
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[7309,548]) ).
thf(20370,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_4
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[20369]) ).
thf(20371,plain,
( ~ vertical_3_4
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[20370:[]]) ).
thf(115,negated_conjecture,
( ~ vertical_4_2
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_4_2) ).
thf(190,plain,
( ~ vertical_4_2
| ~ horizontal_4_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(527,plain,
( ~ vertical_4_2
| ~ horizontal_4_2 ),
inference(cnf,[status(esa)],[190]) ).
thf(8630,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ horizontal_4_2
| ~ vertical_3_4
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[8572,527]) ).
thf(8631,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_2
| ~ vertical_3_4
| vertical_3_5 ),
inference(simp,[status(thm)],[8630]) ).
thf(8632,plain,
( ~ horizontal_4_2
| ~ vertical_3_4
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[8631:[]]) ).
thf(20408,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ $true
| ~ vertical_3_4
| vertical_3_5
| ~ vertical_3_4
| vertical_3_5
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[20371,8632]) ).
thf(20409,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_4
| vertical_3_5
| vertical_3_3 ),
inference(simp,[status(thm)],[20408]) ).
thf(20410,plain,
( ~ vertical_3_4
| vertical_3_5
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[20409:[]]) ).
thf(1823,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_4_3
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1783,532]) ).
thf(1824,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ vertical_4_3
| vertical_4_4 ),
inference(simp,[status(thm)],[1823]) ).
thf(1825,plain,
( ~ vertical_3_6
| ~ vertical_4_3
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1824:[]]) ).
thf(1871,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_3 ),
inference(paramod_ordered,[status(thm)],[1825,468]) ).
thf(1872,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ vertical_3_6
| ~ vertical_4_3 ),
inference(simp,[status(thm)],[1871]) ).
thf(1873,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| ~ vertical_4_3 ),
inference(pattern_uni,[status(thm)],[1872:[]]) ).
thf(1901,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_4
| ~ vertical_3_6
| ~ $true
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,1873]) ).
thf(1902,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[1901]) ).
thf(1903,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[1902:[]]) ).
thf(6782,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[1903,548]) ).
thf(6783,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[6782]) ).
thf(6784,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[6783:[]]) ).
thf(4382,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ horizontal_4_2
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(paramod_ordered,[status(thm)],[4339,527]) ).
thf(4383,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_2
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(simp,[status(thm)],[4382]) ).
thf(4384,plain,
( ~ horizontal_4_2
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(pattern_uni,[status(thm)],[4383:[]]) ).
thf(6950,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ $true
| ~ vertical_3_4
| ~ vertical_3_6
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[6784,4384]) ).
thf(6951,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3 ),
inference(simp,[status(thm)],[6950]) ).
thf(6952,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[6951:[]]) ).
thf(6971,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_4
| ~ $true
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,6952]) ).
thf(6972,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_4
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[6971]) ).
thf(6973,plain,
( ~ vertical_3_4
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[6972:[]]) ).
thf(7040,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ $true
| ~ vertical_3_4
| vertical_3_3
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[6973,406]) ).
thf(7041,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ vertical_3_4
| vertical_3_3
| vertical_2_6 ),
inference(simp,[status(thm)],[7040]) ).
thf(7042,plain,
( ~ vertical_3_5
| ~ vertical_3_4
| vertical_3_3
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[7041:[]]) ).
thf(20483,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ $true
| ~ vertical_3_4
| vertical_3_3
| vertical_2_6
| ~ vertical_3_4
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[20410,7042]) ).
thf(20484,plain,
( ( vertical_3_5 != vertical_3_5 )
| vertical_2_6
| ~ vertical_3_4
| vertical_3_3 ),
inference(simp,[status(thm)],[20483]) ).
thf(20485,plain,
( vertical_2_6
| ~ vertical_3_4
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[20484:[]]) ).
thf(20510,plain,
( ( vertical_3_4 != vertical_3_4 )
| vertical_2_6
| ~ $true
| vertical_3_3
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(paramod_ordered,[status(thm)],[463,20485]) ).
thf(20511,plain,
( ( vertical_3_4 != vertical_3_4 )
| vertical_2_6
| vertical_3_3
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(simp,[status(thm)],[20510]) ).
thf(20512,plain,
( vertical_2_6
| vertical_3_3
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(pattern_uni,[status(thm)],[20511:[]]) ).
thf(1892,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ $true
| ~ horizontal_4_4
| ~ vertical_3_6
| ~ vertical_4_3 ),
inference(paramod_ordered,[status(thm)],[1825,434]) ).
thf(1893,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_4
| ~ vertical_3_6
| ~ vertical_4_3 ),
inference(simp,[status(thm)],[1892]) ).
thf(1894,plain,
( ~ horizontal_4_4
| ~ vertical_3_6
| ~ vertical_4_3 ),
inference(pattern_uni,[status(thm)],[1893:[]]) ).
thf(2378,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_3
| ~ vertical_3_6
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[2323,1894]) ).
thf(2379,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_3
| ~ vertical_3_6
| vertical_3_5 ),
inference(simp,[status(thm)],[2378]) ).
thf(2380,plain,
( ~ vertical_4_3
| ~ vertical_3_6
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[2379:[]]) ).
thf(2408,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ $true
| ~ vertical_3_6
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,2380]) ).
thf(2409,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_6
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[2408]) ).
thf(2410,plain,
( ~ vertical_3_6
| vertical_3_5
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[2409:[]]) ).
thf(2369,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ vertical_3_6
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[2323,457]) ).
thf(2370,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ horizontal_4_3
| ~ vertical_3_6
| vertical_3_5 ),
inference(simp,[status(thm)],[2369]) ).
thf(2371,plain,
( ~ horizontal_4_3
| ~ vertical_3_6
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[2370:[]]) ).
thf(8054,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ $true
| ~ vertical_3_6
| vertical_3_5
| ~ vertical_3_6
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[2410,2371]) ).
thf(8055,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_6
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[8054]) ).
thf(8056,plain,
( ~ vertical_3_6
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[8055:[]]) ).
thf(4505,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ horizontal_4_2
| vertical_3_5
| ~ vertical_3_6 ),
inference(paramod_ordered,[status(thm)],[4360,527]) ).
thf(4506,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_2
| vertical_3_5
| ~ vertical_3_6 ),
inference(simp,[status(thm)],[4505]) ).
thf(4507,plain,
( ~ horizontal_4_2
| vertical_3_5
| ~ vertical_3_6 ),
inference(pattern_uni,[status(thm)],[4506:[]]) ).
thf(8108,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ $true
| vertical_3_5
| ~ vertical_3_6
| ~ vertical_3_6
| vertical_3_5
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[8056,4507]) ).
thf(8109,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_6
| vertical_3_5
| vertical_3_3 ),
inference(simp,[status(thm)],[8108]) ).
thf(8110,plain,
( ~ vertical_3_6
| vertical_3_5
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[8109:[]]) ).
thf(8150,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ $true
| vertical_3_5
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,8110]) ).
thf(8151,plain,
( ( vertical_3_6 != vertical_3_6 )
| vertical_3_5
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[8150]) ).
thf(8152,plain,
( vertical_3_5
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[8151:[]]) ).
thf(8162,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_4
| ~ $true
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[8152,380]) ).
thf(8163,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_4
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[8162]) ).
thf(8164,plain,
( ~ horizontal_3_4
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[8163:[]]) ).
thf(8378,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ horizontal_3_4
| ~ $true
| ~ horizontal_3_4
| vertical_3_3
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[8164,430]) ).
thf(8379,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ horizontal_3_4
| vertical_3_3
| vertical_2_6 ),
inference(simp,[status(thm)],[8378]) ).
thf(8380,plain,
( ~ horizontal_3_4
| vertical_3_3
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[8379:[]]) ).
thf(20597,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| ~ $true
| vertical_3_3
| vertical_2_6
| vertical_2_6
| vertical_3_3
| vertical_2_4
| horizontal_3_3 ),
inference(paramod_ordered,[status(thm)],[20512,8380]) ).
thf(20598,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| vertical_2_6
| vertical_3_3
| vertical_2_4
| horizontal_3_3 ),
inference(simp,[status(thm)],[20597]) ).
thf(20599,plain,
( vertical_2_6
| vertical_3_3
| vertical_2_4
| horizontal_3_3 ),
inference(pattern_uni,[status(thm)],[20598:[]]) ).
thf(94,negated_conjecture,
( ~ horizontal_3_2
| ~ vertical_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_3_3) ).
thf(354,plain,
( ~ horizontal_3_2
| ~ vertical_3_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(545,plain,
( ~ horizontal_3_2
| ~ vertical_3_3 ),
inference(cnf,[status(esa)],[354]) ).
thf(20615,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_2
| ~ $true
| vertical_2_6
| vertical_2_4
| horizontal_3_3 ),
inference(paramod_ordered,[status(thm)],[20599,545]) ).
thf(20616,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_2
| vertical_2_6
| vertical_2_4
| horizontal_3_3 ),
inference(simp,[status(thm)],[20615]) ).
thf(20617,plain,
( ~ horizontal_3_2
| vertical_2_6
| vertical_2_4
| horizontal_3_3 ),
inference(pattern_uni,[status(thm)],[20616:[]]) ).
thf(92,negated_conjecture,
( ~ horizontal_3_2
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_3_3) ).
thf(241,plain,
( ~ horizontal_3_2
| ~ horizontal_3_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(488,plain,
( ~ horizontal_3_2
| ~ horizontal_3_3 ),
inference(cnf,[status(esa)],[241]) ).
thf(21230,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ horizontal_3_2
| ~ $true
| ~ horizontal_3_2
| vertical_2_6
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[20617,488]) ).
thf(21231,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ horizontal_3_2
| vertical_2_6
| vertical_2_4 ),
inference(simp,[status(thm)],[21230]) ).
thf(21232,plain,
( ~ horizontal_3_2
| vertical_2_6
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[21231:[]]) ).
thf(22130,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| ~ $true
| vertical_2_6
| vertical_2_4
| vertical_2_6
| vertical_2_4
| vertical_2_2
| horizontal_3_1 ),
inference(paramod_ordered,[status(thm)],[22123,21232]) ).
thf(22131,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| vertical_2_6
| vertical_2_4
| vertical_2_2
| horizontal_3_1 ),
inference(simp,[status(thm)],[22130]) ).
thf(22132,plain,
( vertical_2_6
| vertical_2_4
| vertical_2_2
| horizontal_3_1 ),
inference(pattern_uni,[status(thm)],[22131:[]]) ).
thf(22,negated_conjecture,
( vertical_3_1
| vertical_4_1
| horizontal_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_4_1) ).
thf(273,plain,
( vertical_3_1
| vertical_4_1
| horizontal_4_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(528,plain,
( vertical_3_1
| vertical_4_1
| horizontal_4_1 ),
inference(cnf,[status(esa)],[273]) ).
thf(144,negated_conjecture,
( ~ vertical_4_1
| ~ vertical_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_5_1) ).
thf(281,plain,
( ~ vertical_4_1
| ~ vertical_5_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(458,plain,
( ~ vertical_4_1
| ~ vertical_5_1 ),
inference(cnf,[status(esa)],[281]) ).
thf(1442,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_3
| vertical_4_6 ),
inference(paramod_ordered,[status(thm)],[1270,458]) ).
thf(1443,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_6 ),
inference(simp,[status(thm)],[1442]) ).
thf(1444,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_6 ),
inference(pattern_uni,[status(thm)],[1443:[]]) ).
thf(1664,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(paramod_ordered,[status(thm)],[1444,532]) ).
thf(1665,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(simp,[status(thm)],[1664]) ).
thf(1666,plain,
( ~ vertical_3_6
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(pattern_uni,[status(thm)],[1665:[]]) ).
thf(1739,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_6
| ~ vertical_4_1
| ~ $true
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,1666]) ).
thf(1740,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[1739]) ).
thf(1741,plain,
( ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[1740:[]]) ).
thf(1847,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| vertical_4_6
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1792,458]) ).
thf(1848,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| vertical_4_6
| vertical_4_4 ),
inference(simp,[status(thm)],[1847]) ).
thf(1849,plain,
( ~ vertical_4_1
| vertical_4_6
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1848:[]]) ).
thf(1931,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_4_1
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1849,532]) ).
thf(1932,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_4_4 ),
inference(simp,[status(thm)],[1931]) ).
thf(1933,plain,
( ~ vertical_3_6
| ~ vertical_4_1
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1932:[]]) ).
thf(1973,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(paramod_ordered,[status(thm)],[1933,485]) ).
thf(1974,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(simp,[status(thm)],[1973]) ).
thf(1975,plain,
( ~ horizontal_4_3
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(pattern_uni,[status(thm)],[1974:[]]) ).
thf(6266,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_1
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[1741,1975]) ).
thf(6267,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[6266]) ).
thf(6268,plain,
( ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[6267:[]]) ).
thf(175,negated_conjecture,
( ~ vertical_5_2
| ~ horizontal_6_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_6_2) ).
thf(324,plain,
( ~ vertical_5_2
| ~ horizontal_6_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(431,plain,
( ~ vertical_5_2
| ~ horizontal_6_1 ),
inference(cnf,[status(esa)],[324]) ).
thf(605,plain,
( ( horizontal_6_1 != horizontal_6_1 )
| ~ vertical_5_2
| ~ $true
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[472,431]) ).
thf(606,plain,
( ( horizontal_6_1 != horizontal_6_1 )
| ~ vertical_5_2
| vertical_5_1 ),
inference(simp,[status(thm)],[605]) ).
thf(607,plain,
( ~ vertical_5_2
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[606:[]]) ).
thf(1037,plain,
( ( vertical_5_2 != vertical_5_2 )
| ~ $true
| vertical_5_1
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(paramod_ordered,[status(thm)],[522,607]) ).
thf(1038,plain,
( ( vertical_5_2 != vertical_5_2 )
| vertical_5_1
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(simp,[status(thm)],[1037]) ).
thf(1039,plain,
( vertical_5_1
| vertical_4_2
| horizontal_5_1
| horizontal_5_2 ),
inference(pattern_uni,[status(thm)],[1038:[]]) ).
thf(154,negated_conjecture,
( ~ horizontal_5_2
| ~ vertical_5_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_5_3) ).
thf(321,plain,
( ~ horizontal_5_2
| ~ vertical_5_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(398,plain,
( ~ horizontal_5_2
| ~ vertical_5_3 ),
inference(cnf,[status(esa)],[321]) ).
thf(1280,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_2
| ~ $true
| vertical_4_6
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[1189,398]) ).
thf(1281,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_2
| vertical_4_6
| vertical_5_1 ),
inference(simp,[status(thm)],[1280]) ).
thf(1282,plain,
( ~ horizontal_5_2
| vertical_4_6
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[1281:[]]) ).
thf(1457,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ $true
| vertical_4_6
| vertical_5_1
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1039,1282]) ).
thf(1458,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| vertical_4_6
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[1457]) ).
thf(1459,plain,
( vertical_4_6
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[1458:[]]) ).
thf(2429,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| vertical_4_6
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1459,458]) ).
thf(2430,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| vertical_4_6
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[2429]) ).
thf(2431,plain,
( ~ vertical_4_1
| vertical_4_6
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[2430:[]]) ).
thf(143,negated_conjecture,
( ~ vertical_4_1
| ~ horizontal_5_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_5_1) ).
thf(325,plain,
( ~ vertical_4_1
| ~ horizontal_5_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(392,plain,
( ~ vertical_4_1
| ~ horizontal_5_1 ),
inference(cnf,[status(esa)],[325]) ).
thf(3386,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_1
| vertical_4_6
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[2431,392]) ).
thf(3387,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| vertical_4_6
| vertical_4_2 ),
inference(simp,[status(thm)],[3386]) ).
thf(3388,plain,
( ~ vertical_4_1
| vertical_4_6
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[3387:[]]) ).
thf(3422,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ $true
| ~ vertical_4_1
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[3388,532]) ).
thf(3423,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_4_2 ),
inference(simp,[status(thm)],[3422]) ).
thf(3424,plain,
( ~ vertical_3_6
| ~ vertical_4_1
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[3423:[]]) ).
thf(3452,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ horizontal_4_2
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(paramod_ordered,[status(thm)],[3424,527]) ).
thf(3453,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_2
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(simp,[status(thm)],[3452]) ).
thf(3454,plain,
( ~ horizontal_4_2
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(pattern_uni,[status(thm)],[3453:[]]) ).
thf(6872,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_1
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[6268,3454]) ).
thf(6873,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3 ),
inference(simp,[status(thm)],[6872]) ).
thf(6874,plain,
( ~ vertical_3_6
| ~ vertical_4_1
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[6873:[]]) ).
thf(6893,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_6
| ~ $true
| vertical_3_3
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,6874]) ).
thf(6894,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_6
| vertical_3_3
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[6893]) ).
thf(6895,plain,
( ~ vertical_3_6
| vertical_3_3
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[6894:[]]) ).
thf(118,negated_conjecture,
( ~ horizontal_4_1
| ~ vertical_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_4_2) ).
thf(277,plain,
( ~ horizontal_4_1
| ~ vertical_4_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(542,plain,
( ~ horizontal_4_1
| ~ vertical_4_2 ),
inference(cnf,[status(esa)],[277]) ).
thf(17585,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_1
| ~ $true
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[17491,542]) ).
thf(17586,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_1
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[17585]) ).
thf(17587,plain,
( ~ horizontal_4_1
| ~ vertical_3_6
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[17586:[]]) ).
thf(116,negated_conjecture,
( ~ horizontal_4_1
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_4_2) ).
thf(223,plain,
( ~ horizontal_4_1
| ~ horizontal_4_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(483,plain,
( ~ horizontal_4_1
| ~ horizontal_4_2 ),
inference(cnf,[status(esa)],[223]) ).
thf(17777,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ horizontal_4_1
| ~ $true
| ~ horizontal_4_1
| ~ vertical_3_6
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[17587,483]) ).
thf(17778,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ horizontal_4_1
| ~ vertical_3_6
| vertical_3_3 ),
inference(simp,[status(thm)],[17777]) ).
thf(17779,plain,
( ~ horizontal_4_1
| ~ vertical_3_6
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[17778:[]]) ).
thf(17798,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ $true
| ~ vertical_3_6
| vertical_3_3
| ~ vertical_3_6
| vertical_3_3
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[6895,17779]) ).
thf(17799,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_6
| vertical_3_3
| vertical_3_1 ),
inference(simp,[status(thm)],[17798]) ).
thf(17800,plain,
( ~ vertical_3_6
| vertical_3_3
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[17799:[]]) ).
thf(17876,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ $true
| vertical_3_3
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,17800]) ).
thf(17877,plain,
( ( vertical_3_6 != vertical_3_6 )
| vertical_3_3
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[17876]) ).
thf(17878,plain,
( vertical_3_3
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[17877:[]]) ).
thf(1598,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_3
| ~ vertical_4_5 ),
inference(paramod_ordered,[status(thm)],[1381,458]) ).
thf(1599,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ vertical_4_3
| ~ vertical_4_5 ),
inference(simp,[status(thm)],[1598]) ).
thf(1600,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| ~ vertical_4_5 ),
inference(pattern_uni,[status(thm)],[1599:[]]) ).
thf(1706,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_1
| ~ vertical_4_3
| ~ $true
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,1600]) ).
thf(1707,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[1706]) ).
thf(1708,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[1707:[]]) ).
thf(1655,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ $true
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(paramod_ordered,[status(thm)],[1444,419]) ).
thf(1656,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(simp,[status(thm)],[1655]) ).
thf(1657,plain,
( ~ horizontal_4_5
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(pattern_uni,[status(thm)],[1656:[]]) ).
thf(5828,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ $true
| ~ vertical_4_1
| ~ vertical_4_3
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[1708,1657]) ).
thf(5829,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[5828]) ).
thf(5830,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[5829:[]]) ).
thf(4736,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_3
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[4681,458]) ).
thf(4737,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_4 ),
inference(simp,[status(thm)],[4736]) ).
thf(4738,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[4737:[]]) ).
thf(4847,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ $true
| ~ horizontal_4_4
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(paramod_ordered,[status(thm)],[4738,434]) ).
thf(4848,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_4
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(simp,[status(thm)],[4847]) ).
thf(4849,plain,
( ~ horizontal_4_4
| ~ vertical_4_1
| ~ vertical_4_3 ),
inference(pattern_uni,[status(thm)],[4848:[]]) ).
thf(6536,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ $true
| ~ vertical_4_1
| ~ vertical_4_3
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[5830,4849]) ).
thf(6537,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5 ),
inference(simp,[status(thm)],[6536]) ).
thf(6538,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[6537:[]]) ).
thf(6590,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ $true
| ~ vertical_4_3
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,6538]) ).
thf(6591,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_4_3
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[6590]) ).
thf(6592,plain,
( ~ vertical_4_3
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[6591:[]]) ).
thf(6908,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,6592]) ).
thf(6909,plain,
( ( vertical_4_3 != vertical_4_3 )
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[6908]) ).
thf(6910,plain,
( vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[6909:[]]) ).
thf(2297,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_5
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[2245,458]) ).
thf(2298,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(simp,[status(thm)],[2297]) ).
thf(2299,plain,
( ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[2298:[]]) ).
thf(2348,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_1
| ~ $true
| vertical_4_4
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,2299]) ).
thf(2349,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_1
| vertical_4_4
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[2348]) ).
thf(2350,plain,
( ~ vertical_4_1
| vertical_4_4
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[2349:[]]) ).
thf(1922,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ $true
| ~ vertical_4_1
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[1849,419]) ).
thf(1923,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ vertical_4_1
| vertical_4_4 ),
inference(simp,[status(thm)],[1922]) ).
thf(1924,plain,
( ~ horizontal_4_5
| ~ vertical_4_1
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[1923:[]]) ).
thf(7511,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ $true
| ~ vertical_4_1
| vertical_4_4
| ~ vertical_4_1
| vertical_4_4
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[2350,1924]) ).
thf(7512,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_4_1
| vertical_4_4
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[7511]) ).
thf(7513,plain,
( ~ vertical_4_1
| vertical_4_4
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[7512:[]]) ).
thf(7574,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ vertical_4_1
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[7513,485]) ).
thf(7575,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ vertical_4_1
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[7574]) ).
thf(7576,plain,
( ~ horizontal_4_3
| ~ vertical_4_1
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[7575:[]]) ).
thf(7721,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ horizontal_4_3
| ~ vertical_4_1
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[7576,457]) ).
thf(7722,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ horizontal_4_3
| ~ vertical_4_1
| vertical_3_5 ),
inference(simp,[status(thm)],[7721]) ).
thf(7723,plain,
( ~ horizontal_4_3
| ~ vertical_4_1
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[7722:[]]) ).
thf(7766,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ horizontal_4_3
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,7723]) ).
thf(7767,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ horizontal_4_3
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[7766]) ).
thf(7768,plain,
( ~ horizontal_4_3
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[7767:[]]) ).
thf(17855,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[6910,7768]) ).
thf(17856,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[17855]) ).
thf(17857,plain,
( vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[17856:[]]) ).
thf(1391,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_2
| ~ $true
| ~ vertical_4_5
| vertical_5_1 ),
inference(paramod_ordered,[status(thm)],[1192,398]) ).
thf(1392,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_2
| ~ vertical_4_5
| vertical_5_1 ),
inference(simp,[status(thm)],[1391]) ).
thf(1393,plain,
( ~ horizontal_5_2
| ~ vertical_4_5
| vertical_5_1 ),
inference(pattern_uni,[status(thm)],[1392:[]]) ).
thf(1640,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ $true
| ~ vertical_4_5
| vertical_5_1
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1039,1393]) ).
thf(1641,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_5
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[1640]) ).
thf(1642,plain,
( ~ vertical_4_5
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[1641:[]]) ).
thf(2654,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1642,458]) ).
thf(2655,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[2654]) ).
thf(2656,plain,
( ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[2655:[]]) ).
thf(3803,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[2656,392]) ).
thf(3804,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_2 ),
inference(simp,[status(thm)],[3803]) ).
thf(3805,plain,
( ~ vertical_4_1
| ~ vertical_4_5
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[3804:[]]) ).
thf(3830,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_1
| ~ $true
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(paramod_ordered,[status(thm)],[500,3805]) ).
thf(3831,plain,
( ( vertical_4_5 != vertical_4_5 )
| ~ vertical_4_1
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(simp,[status(thm)],[3830]) ).
thf(3832,plain,
( ~ vertical_4_1
| vertical_4_2
| vertical_3_5
| horizontal_4_4
| horizontal_4_5 ),
inference(pattern_uni,[status(thm)],[3831:[]]) ).
thf(3413,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ $true
| ~ vertical_4_1
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[3388,419]) ).
thf(3414,plain,
( ( vertical_4_6 != vertical_4_6 )
| ~ horizontal_4_5
| ~ vertical_4_1
| vertical_4_2 ),
inference(simp,[status(thm)],[3413]) ).
thf(3415,plain,
( ~ horizontal_4_5
| ~ vertical_4_1
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[3414:[]]) ).
thf(11906,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ $true
| ~ vertical_4_1
| vertical_4_2
| ~ vertical_4_1
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[3832,3415]) ).
thf(11907,plain,
( ( horizontal_4_5 != horizontal_4_5 )
| ~ vertical_4_1
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[11906]) ).
thf(11908,plain,
( ~ vertical_4_1
| vertical_4_2
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[11907:[]]) ).
thf(3713,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_2
| ~ $true
| vertical_5_1
| vertical_4_4
| horizontal_5_3 ),
inference(paramod_ordered,[status(thm)],[3634,398]) ).
thf(3714,plain,
( ( vertical_5_3 != vertical_5_3 )
| ~ horizontal_5_2
| vertical_5_1
| vertical_4_4
| horizontal_5_3 ),
inference(simp,[status(thm)],[3713]) ).
thf(3715,plain,
( ~ horizontal_5_2
| vertical_5_1
| vertical_4_4
| horizontal_5_3 ),
inference(pattern_uni,[status(thm)],[3714:[]]) ).
thf(4952,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ horizontal_5_2
| ~ $true
| ~ horizontal_5_2
| vertical_5_1
| vertical_4_4 ),
inference(paramod_ordered,[status(thm)],[3715,402]) ).
thf(4953,plain,
( ( horizontal_5_3 != horizontal_5_3 )
| ~ horizontal_5_2
| vertical_5_1
| vertical_4_4 ),
inference(simp,[status(thm)],[4952]) ).
thf(4954,plain,
( ~ horizontal_5_2
| vertical_5_1
| vertical_4_4 ),
inference(pattern_uni,[status(thm)],[4953:[]]) ).
thf(4982,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ $true
| vertical_5_1
| vertical_4_4
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1039,4954]) ).
thf(4983,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| vertical_4_4
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[4982]) ).
thf(4984,plain,
( vertical_4_4
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[4983:[]]) ).
thf(4991,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[4984,458]) ).
thf(4992,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[4991]) ).
thf(4993,plain,
( ~ vertical_4_1
| vertical_4_4
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[4992:[]]) ).
thf(5975,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_1
| vertical_4_4
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[4993,392]) ).
thf(5976,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| vertical_4_4
| vertical_4_2 ),
inference(simp,[status(thm)],[5975]) ).
thf(5977,plain,
( ~ vertical_4_1
| vertical_4_4
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[5976:[]]) ).
thf(6044,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ $true
| ~ horizontal_4_4
| ~ vertical_4_1
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[5977,434]) ).
thf(6045,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_4
| ~ vertical_4_1
| vertical_4_2 ),
inference(simp,[status(thm)],[6044]) ).
thf(6046,plain,
( ~ horizontal_4_4
| ~ vertical_4_1
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[6045:[]]) ).
thf(11942,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ $true
| ~ vertical_4_1
| vertical_4_2
| ~ vertical_4_1
| vertical_4_2
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[11908,6046]) ).
thf(11943,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_1
| vertical_4_2
| vertical_3_5 ),
inference(simp,[status(thm)],[11942]) ).
thf(11944,plain,
( ~ vertical_4_1
| vertical_4_2
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[11943:[]]) ).
thf(12020,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ horizontal_4_2
| ~ vertical_4_1
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[11944,527]) ).
thf(12021,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_2
| ~ vertical_4_1
| vertical_3_5 ),
inference(simp,[status(thm)],[12020]) ).
thf(12022,plain,
( ~ horizontal_4_2
| ~ vertical_4_1
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[12021:[]]) ).
thf(12050,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ horizontal_4_2
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,12022]) ).
thf(12051,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ horizontal_4_2
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[12050]) ).
thf(12052,plain,
( ~ horizontal_4_2
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[12051:[]]) ).
thf(18062,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[17857,12052]) ).
thf(18063,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3 ),
inference(simp,[status(thm)],[18062]) ).
thf(18064,plain,
( vertical_3_5
| vertical_3_1
| horizontal_4_1
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[18063:[]]) ).
thf(15884,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_1
| ~ $true
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[15820,542]) ).
thf(15885,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ horizontal_4_1
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[15884]) ).
thf(15886,plain,
( ~ horizontal_4_1
| vertical_3_5
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[15885:[]]) ).
thf(16196,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ horizontal_4_1
| ~ $true
| ~ horizontal_4_1
| vertical_3_5
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[15886,483]) ).
thf(16197,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ horizontal_4_1
| vertical_3_5
| vertical_3_3 ),
inference(simp,[status(thm)],[16196]) ).
thf(16198,plain,
( ~ horizontal_4_1
| vertical_3_5
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[16197:[]]) ).
thf(18143,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ $true
| vertical_3_5
| vertical_3_3
| vertical_3_5
| vertical_3_1
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[18064,16198]) ).
thf(18144,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| vertical_3_5
| vertical_3_1
| vertical_3_3 ),
inference(simp,[status(thm)],[18143]) ).
thf(18145,plain,
( vertical_3_5
| vertical_3_1
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[18144:[]]) ).
thf(18176,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ $true
| ~ horizontal_3_5
| vertical_3_1
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[18145,406]) ).
thf(18177,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_5
| vertical_3_1
| vertical_3_3 ),
inference(simp,[status(thm)],[18176]) ).
thf(18178,plain,
( ~ horizontal_3_5
| vertical_3_1
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[18177:[]]) ).
thf(18221,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ $true
| vertical_3_1
| vertical_3_3
| vertical_3_3
| vertical_3_1
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[17878,18178]) ).
thf(18222,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| vertical_3_3
| vertical_3_1
| vertical_2_6 ),
inference(simp,[status(thm)],[18221]) ).
thf(18223,plain,
( vertical_3_3
| vertical_3_1
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[18222:[]]) ).
thf(7568,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_4_1
| vertical_3_5
| horizontal_4_4 ),
inference(paramod_ordered,[status(thm)],[7513,468]) ).
thf(7569,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ vertical_4_1
| vertical_3_5
| horizontal_4_4 ),
inference(simp,[status(thm)],[7568]) ).
thf(7570,plain,
( ~ vertical_3_4
| ~ vertical_4_1
| vertical_3_5
| horizontal_4_4 ),
inference(pattern_uni,[status(thm)],[7569:[]]) ).
thf(7619,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_4
| ~ vertical_4_1
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[7570,489]) ).
thf(7620,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_3_4
| ~ vertical_4_1
| vertical_3_5 ),
inference(simp,[status(thm)],[7619]) ).
thf(7621,plain,
( ~ vertical_3_4
| ~ vertical_4_1
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[7620:[]]) ).
thf(7673,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_4
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,7621]) ).
thf(7674,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_4
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[7673]) ).
thf(7675,plain,
( ~ vertical_3_4
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[7674:[]]) ).
thf(7808,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ $true
| ~ vertical_4_2
| ~ vertical_3_4
| vertical_3_5
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[7675,542]) ).
thf(7809,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_4_2
| ~ vertical_3_4
| vertical_3_5
| vertical_3_1 ),
inference(simp,[status(thm)],[7808]) ).
thf(7810,plain,
( ~ vertical_4_2
| ~ vertical_3_4
| vertical_3_5
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[7809:[]]) ).
thf(8636,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ vertical_3_4
| vertical_3_5
| vertical_3_1
| ~ vertical_3_4
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[8572,7810]) ).
thf(8637,plain,
( ( vertical_4_2 != vertical_4_2 )
| vertical_3_1
| ~ vertical_3_4
| vertical_3_5 ),
inference(simp,[status(thm)],[8636]) ).
thf(8638,plain,
( vertical_3_1
| ~ vertical_3_4
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[8637:[]]) ).
thf(1964,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(paramod_ordered,[status(thm)],[1933,468]) ).
thf(1965,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ vertical_3_4
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(simp,[status(thm)],[1964]) ).
thf(1966,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(pattern_uni,[status(thm)],[1965:[]]) ).
thf(2000,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_4
| ~ vertical_3_6
| ~ $true
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,1966]) ).
thf(2001,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[2000]) ).
thf(2002,plain,
( ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[2001:[]]) ).
thf(2873,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ $true
| ~ vertical_4_2
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[2002,542]) ).
thf(2874,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_4_2
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_1 ),
inference(simp,[status(thm)],[2873]) ).
thf(2875,plain,
( ~ vertical_4_2
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[2874:[]]) ).
thf(4394,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ vertical_3_4
| ~ vertical_3_6
| vertical_3_1
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(paramod_ordered,[status(thm)],[4339,2875]) ).
thf(4395,plain,
( ( vertical_4_2 != vertical_4_2 )
| vertical_3_1
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(simp,[status(thm)],[4394]) ).
thf(4396,plain,
( vertical_3_1
| ~ vertical_3_4
| ~ vertical_3_6 ),
inference(pattern_uni,[status(thm)],[4395:[]]) ).
thf(4556,plain,
( ( vertical_3_6 != vertical_3_6 )
| vertical_3_1
| ~ vertical_3_4
| ~ $true
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,4396]) ).
thf(4557,plain,
( ( vertical_3_6 != vertical_3_6 )
| vertical_3_1
| ~ vertical_3_4
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4556]) ).
thf(4558,plain,
( vertical_3_1
| ~ vertical_3_4
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4557:[]]) ).
thf(5321,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ $true
| vertical_3_1
| ~ vertical_3_4
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[4558,406]) ).
thf(5322,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| vertical_3_1
| ~ vertical_3_4
| vertical_2_6 ),
inference(simp,[status(thm)],[5321]) ).
thf(5323,plain,
( ~ vertical_3_5
| vertical_3_1
| ~ vertical_3_4
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5322:[]]) ).
thf(8756,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ $true
| vertical_3_1
| ~ vertical_3_4
| vertical_2_6
| vertical_3_1
| ~ vertical_3_4 ),
inference(paramod_ordered,[status(thm)],[8638,5323]) ).
thf(8757,plain,
( ( vertical_3_5 != vertical_3_5 )
| vertical_2_6
| vertical_3_1
| ~ vertical_3_4 ),
inference(simp,[status(thm)],[8756]) ).
thf(8758,plain,
( vertical_2_6
| vertical_3_1
| ~ vertical_3_4 ),
inference(pattern_uni,[status(thm)],[8757:[]]) ).
thf(8846,plain,
( ( vertical_3_4 != vertical_3_4 )
| vertical_2_6
| vertical_3_1
| ~ $true
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(paramod_ordered,[status(thm)],[463,8758]) ).
thf(8847,plain,
( ( vertical_3_4 != vertical_3_4 )
| vertical_2_6
| vertical_3_1
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(simp,[status(thm)],[8846]) ).
thf(8848,plain,
( vertical_2_6
| vertical_3_1
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(pattern_uni,[status(thm)],[8847:[]]) ).
thf(1982,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ $true
| ~ horizontal_4_4
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(paramod_ordered,[status(thm)],[1933,434]) ).
thf(1983,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_4
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(simp,[status(thm)],[1982]) ).
thf(1984,plain,
( ~ horizontal_4_4
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(pattern_uni,[status(thm)],[1983:[]]) ).
thf(2372,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_1
| ~ vertical_3_6
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[2323,1984]) ).
thf(2373,plain,
( ( horizontal_4_4 != horizontal_4_4 )
| ~ vertical_4_1
| ~ vertical_3_6
| vertical_3_5 ),
inference(simp,[status(thm)],[2372]) ).
thf(2374,plain,
( ~ vertical_4_1
| ~ vertical_3_6
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[2373:[]]) ).
thf(2402,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ $true
| ~ vertical_3_6
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,2374]) ).
thf(2403,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_6
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[2402]) ).
thf(2404,plain,
( ~ vertical_3_6
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[2403:[]]) ).
thf(3266,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ $true
| ~ vertical_4_2
| ~ vertical_3_6
| vertical_3_5
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[2404,542]) ).
thf(3267,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_4_2
| ~ vertical_3_6
| vertical_3_5
| vertical_3_1 ),
inference(simp,[status(thm)],[3266]) ).
thf(3268,plain,
( ~ vertical_4_2
| ~ vertical_3_6
| vertical_3_5
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[3267:[]]) ).
thf(4502,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ $true
| ~ vertical_3_6
| vertical_3_5
| vertical_3_1
| vertical_3_5
| ~ vertical_3_6 ),
inference(paramod_ordered,[status(thm)],[4360,3268]) ).
thf(4503,plain,
( ( vertical_4_2 != vertical_4_2 )
| vertical_3_1
| vertical_3_5
| ~ vertical_3_6 ),
inference(simp,[status(thm)],[4502]) ).
thf(4504,plain,
( vertical_3_1
| vertical_3_5
| ~ vertical_3_6 ),
inference(pattern_uni,[status(thm)],[4503:[]]) ).
thf(4613,plain,
( ( vertical_3_6 != vertical_3_6 )
| vertical_3_1
| vertical_3_5
| ~ $true
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,4504]) ).
thf(4614,plain,
( ( vertical_3_6 != vertical_3_6 )
| vertical_3_1
| vertical_3_5
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4613]) ).
thf(4615,plain,
( vertical_3_1
| vertical_3_5
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4614:[]]) ).
thf(4883,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_4
| ~ $true
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[4615,380]) ).
thf(4884,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ horizontal_3_4
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4883]) ).
thf(4885,plain,
( ~ horizontal_3_4
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4884:[]]) ).
thf(5867,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ horizontal_3_4
| ~ $true
| ~ horizontal_3_4
| vertical_3_1
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[4885,430]) ).
thf(5868,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ horizontal_3_4
| vertical_3_1
| vertical_2_6 ),
inference(simp,[status(thm)],[5867]) ).
thf(5869,plain,
( ~ horizontal_3_4
| vertical_3_1
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5868:[]]) ).
thf(9797,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| ~ $true
| vertical_3_1
| vertical_2_6
| vertical_2_6
| vertical_3_1
| vertical_2_4
| horizontal_3_3 ),
inference(paramod_ordered,[status(thm)],[8848,5869]) ).
thf(9798,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| vertical_2_6
| vertical_3_1
| vertical_2_4
| horizontal_3_3 ),
inference(simp,[status(thm)],[9797]) ).
thf(9799,plain,
( vertical_2_6
| vertical_3_1
| vertical_2_4
| horizontal_3_3 ),
inference(pattern_uni,[status(thm)],[9798:[]]) ).
thf(9824,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ vertical_3_3
| ~ $true
| vertical_2_6
| vertical_3_1
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[9799,494]) ).
thf(9825,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ vertical_3_3
| vertical_2_6
| vertical_3_1
| vertical_2_4 ),
inference(simp,[status(thm)],[9824]) ).
thf(9826,plain,
( ~ vertical_3_3
| vertical_2_6
| vertical_3_1
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[9825:[]]) ).
thf(18242,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ $true
| vertical_2_6
| vertical_3_1
| vertical_2_4
| vertical_3_1
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[18223,9826]) ).
thf(18243,plain,
( ( vertical_3_3 != vertical_3_3 )
| vertical_2_4
| vertical_3_1
| vertical_2_6 ),
inference(simp,[status(thm)],[18242]) ).
thf(18244,plain,
( vertical_2_4
| vertical_3_1
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[18243:[]]) ).
thf(82,negated_conjecture,
( ~ vertical_3_1
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_3_1) ).
thf(340,plain,
( ~ vertical_3_1
| ~ horizontal_3_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(369,plain,
( ~ vertical_3_1
| ~ horizontal_3_1 ),
inference(cnf,[status(esa)],[340]) ).
thf(18317,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ $true
| ~ horizontal_3_1
| vertical_2_4
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[18244,369]) ).
thf(18318,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ horizontal_3_1
| vertical_2_4
| vertical_2_6 ),
inference(simp,[status(thm)],[18317]) ).
thf(18319,plain,
( ~ horizontal_3_1
| vertical_2_4
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[18318:[]]) ).
thf(22187,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| ~ $true
| vertical_2_4
| vertical_2_6
| vertical_2_6
| vertical_2_4
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[22132,18319]) ).
thf(22188,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| vertical_2_6
| vertical_2_4
| vertical_2_2 ),
inference(simp,[status(thm)],[22187]) ).
thf(22189,plain,
( vertical_2_6
| vertical_2_4
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[22188:[]]) ).
thf(9,negated_conjecture,
( horizontal_1_5
| vertical_1_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_6) ).
thf(245,plain,
( horizontal_1_5
| vertical_1_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(469,plain,
( horizontal_1_5
| vertical_1_6 ),
inference(cnf,[status(esa)],[245]) ).
thf(80,negated_conjecture,
( ~ vertical_1_6
| ~ vertical_2_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_6) ).
thf(302,plain,
( ~ vertical_1_6
| ~ vertical_2_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(420,plain,
( ~ vertical_1_6
| ~ vertical_2_6 ),
inference(cnf,[status(esa)],[302]) ).
thf(583,plain,
( ( vertical_1_6 != vertical_1_6 )
| ~ $true
| ~ vertical_2_6
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[469,420]) ).
thf(584,plain,
( ( vertical_1_6 != vertical_1_6 )
| ~ vertical_2_6
| horizontal_1_5 ),
inference(simp,[status(thm)],[583]) ).
thf(585,plain,
( ~ vertical_2_6
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[584:[]]) ).
thf(22214,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ $true
| horizontal_1_5
| vertical_2_4
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[22189,585]) ).
thf(22215,plain,
( ( vertical_2_6 != vertical_2_6 )
| horizontal_1_5
| vertical_2_4
| vertical_2_2 ),
inference(simp,[status(thm)],[22214]) ).
thf(22216,plain,
( horizontal_1_5
| vertical_2_4
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[22215:[]]) ).
thf(14,negated_conjecture,
( vertical_1_5
| horizontal_2_4
| vertical_2_5
| horizontal_2_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_5) ).
thf(203,plain,
( vertical_1_5
| horizontal_2_4
| vertical_2_5
| horizontal_2_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(506,plain,
( vertical_1_5
| horizontal_2_4
| vertical_2_5
| horizontal_2_5 ),
inference(cnf,[status(esa)],[203]) ).
thf(107,negated_conjecture,
( ~ vertical_2_5
| ~ vertical_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_5) ).
thf(351,plain,
( ~ vertical_2_5
| ~ vertical_3_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(514,plain,
( ~ vertical_2_5
| ~ vertical_3_5 ),
inference(cnf,[status(esa)],[351]) ).
thf(5336,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ $true
| ~ vertical_3_2
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[4597,514]) ).
thf(5337,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ vertical_3_2
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[5336]) ).
thf(5338,plain,
( ~ vertical_2_5
| ~ vertical_3_2
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[5337:[]]) ).
thf(105,negated_conjecture,
( ~ vertical_2_5
| ~ horizontal_3_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_5) ).
thf(260,plain,
( ~ vertical_2_5
| ~ horizontal_3_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(424,plain,
( ~ vertical_2_5
| ~ horizontal_3_5 ),
inference(cnf,[status(esa)],[260]) ).
thf(6356,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_2_5
| ~ $true
| ~ vertical_2_5
| ~ vertical_3_2
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[5338,424]) ).
thf(6357,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_2_5
| ~ vertical_3_2
| vertical_2_6 ),
inference(simp,[status(thm)],[6356]) ).
thf(6358,plain,
( ~ vertical_2_5
| ~ vertical_3_2
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[6357:[]]) ).
thf(6377,plain,
( ( vertical_3_2 != vertical_3_2 )
| ~ vertical_2_5
| ~ $true
| vertical_2_6
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(paramod_ordered,[status(thm)],[534,6358]) ).
thf(6378,plain,
( ( vertical_3_2 != vertical_3_2 )
| ~ vertical_2_5
| vertical_2_6
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(simp,[status(thm)],[6377]) ).
thf(6379,plain,
( ~ vertical_2_5
| vertical_2_6
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(pattern_uni,[status(thm)],[6378:[]]) ).
thf(8156,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ $true
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[8152,514]) ).
thf(8157,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[8156]) ).
thf(8158,plain,
( ~ vertical_2_5
| vertical_3_3
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[8157:[]]) ).
thf(8189,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_2_5
| ~ $true
| ~ vertical_2_5
| vertical_3_3
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[8158,424]) ).
thf(8190,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_2_5
| vertical_3_3
| vertical_2_6 ),
inference(simp,[status(thm)],[8189]) ).
thf(8191,plain,
( ~ vertical_2_5
| vertical_3_3
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[8190:[]]) ).
thf(8222,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_2
| ~ $true
| ~ vertical_2_5
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[8191,545]) ).
thf(8223,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_2
| ~ vertical_2_5
| vertical_2_6 ),
inference(simp,[status(thm)],[8222]) ).
thf(8224,plain,
( ~ horizontal_3_2
| ~ vertical_2_5
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[8223:[]]) ).
thf(17126,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| ~ $true
| ~ vertical_2_5
| vertical_2_6
| ~ vertical_2_5
| vertical_2_6
| vertical_2_2
| horizontal_3_1 ),
inference(paramod_ordered,[status(thm)],[6379,8224]) ).
thf(17127,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| ~ vertical_2_5
| vertical_2_6
| vertical_2_2
| horizontal_3_1 ),
inference(simp,[status(thm)],[17126]) ).
thf(17128,plain,
( ~ vertical_2_5
| vertical_2_6
| vertical_2_2
| horizontal_3_1 ),
inference(pattern_uni,[status(thm)],[17127:[]]) ).
thf(4877,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ $true
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[4615,514]) ).
thf(4878,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4877]) ).
thf(4879,plain,
( ~ vertical_2_5
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4878:[]]) ).
thf(5660,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_2_5
| ~ $true
| ~ vertical_2_5
| vertical_3_1
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[4879,424]) ).
thf(5661,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_2_5
| vertical_3_1
| vertical_2_6 ),
inference(simp,[status(thm)],[5660]) ).
thf(5662,plain,
( ~ vertical_2_5
| vertical_3_1
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5661:[]]) ).
thf(5696,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ $true
| ~ horizontal_3_1
| ~ vertical_2_5
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[5662,369]) ).
thf(5697,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ horizontal_3_1
| ~ vertical_2_5
| vertical_2_6 ),
inference(simp,[status(thm)],[5696]) ).
thf(5698,plain,
( ~ horizontal_3_1
| ~ vertical_2_5
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5697:[]]) ).
thf(17177,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| ~ $true
| ~ vertical_2_5
| vertical_2_6
| ~ vertical_2_5
| vertical_2_6
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[17128,5698]) ).
thf(17178,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| ~ vertical_2_5
| vertical_2_6
| vertical_2_2 ),
inference(simp,[status(thm)],[17177]) ).
thf(17179,plain,
( ~ vertical_2_5
| vertical_2_6
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[17178:[]]) ).
thf(17276,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ $true
| horizontal_1_5
| ~ vertical_2_5
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[17179,585]) ).
thf(17277,plain,
( ( vertical_2_6 != vertical_2_6 )
| horizontal_1_5
| ~ vertical_2_5
| vertical_2_2 ),
inference(simp,[status(thm)],[17276]) ).
thf(17278,plain,
( horizontal_1_5
| ~ vertical_2_5
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[17277:[]]) ).
thf(17294,plain,
( ( vertical_2_5 != vertical_2_5 )
| horizontal_1_5
| ~ $true
| vertical_2_2
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(paramod_ordered,[status(thm)],[506,17278]) ).
thf(17295,plain,
( ( vertical_2_5 != vertical_2_5 )
| horizontal_1_5
| vertical_2_2
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(simp,[status(thm)],[17294]) ).
thf(17296,plain,
( horizontal_1_5
| vertical_2_2
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(pattern_uni,[status(thm)],[17295:[]]) ).
thf(81,negated_conjecture,
( ~ vertical_1_6
| ~ horizontal_2_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_2_6) ).
thf(288,plain,
( ~ vertical_1_6
| ~ horizontal_2_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(383,plain,
( ~ vertical_1_6
| ~ horizontal_2_5 ),
inference(cnf,[status(esa)],[288]) ).
thf(554,plain,
( ( vertical_1_6 != vertical_1_6 )
| ~ $true
| ~ horizontal_2_5
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[469,383]) ).
thf(555,plain,
( ( vertical_1_6 != vertical_1_6 )
| ~ horizontal_2_5
| horizontal_1_5 ),
inference(simp,[status(thm)],[554]) ).
thf(556,plain,
( ~ horizontal_2_5
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[555:[]]) ).
thf(17366,plain,
( ( horizontal_2_5 != horizontal_2_5 )
| ~ $true
| horizontal_1_5
| horizontal_1_5
| vertical_2_2
| vertical_1_5
| horizontal_2_4 ),
inference(paramod_ordered,[status(thm)],[17296,556]) ).
thf(17367,plain,
( ( horizontal_2_5 != horizontal_2_5 )
| horizontal_1_5
| vertical_2_2
| vertical_1_5
| horizontal_2_4 ),
inference(simp,[status(thm)],[17366]) ).
thf(17368,plain,
( horizontal_1_5
| vertical_2_2
| vertical_1_5
| horizontal_2_4 ),
inference(pattern_uni,[status(thm)],[17367:[]]) ).
thf(67,negated_conjecture,
( ~ vertical_2_4
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_2_4) ).
thf(315,plain,
( ~ vertical_2_4
| ~ horizontal_2_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(525,plain,
( ~ vertical_2_4
| ~ horizontal_2_4 ),
inference(cnf,[status(esa)],[315]) ).
thf(17405,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ vertical_2_4
| ~ $true
| horizontal_1_5
| vertical_2_2
| vertical_1_5 ),
inference(paramod_ordered,[status(thm)],[17368,525]) ).
thf(17406,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ vertical_2_4
| horizontal_1_5
| vertical_2_2
| vertical_1_5 ),
inference(simp,[status(thm)],[17405]) ).
thf(17407,plain,
( ~ vertical_2_4
| horizontal_1_5
| vertical_2_2
| vertical_1_5 ),
inference(pattern_uni,[status(thm)],[17406:[]]) ).
thf(22268,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ $true
| horizontal_1_5
| vertical_2_2
| vertical_1_5
| horizontal_1_5
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[22216,17407]) ).
thf(22269,plain,
( ( vertical_2_4 != vertical_2_4 )
| vertical_1_5
| horizontal_1_5
| vertical_2_2 ),
inference(simp,[status(thm)],[22268]) ).
thf(22270,plain,
( vertical_1_5
| horizontal_1_5
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[22269:[]]) ).
thf(10,negated_conjecture,
( vertical_1_1
| vertical_2_1
| horizontal_2_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_1) ).
thf(193,plain,
( vertical_1_1
| vertical_2_1
| horizontal_2_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(439,plain,
( vertical_1_1
| vertical_2_1
| horizontal_2_1 ),
inference(cnf,[status(esa)],[193]) ).
thf(2,negated_conjecture,
~ vertical_1_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered2_1_1) ).
thf(261,plain,
~ vertical_1_1,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(396,plain,
~ vertical_1_1,
inference(polarity_switch,[status(thm)],[261]) ).
thf(608,plain,
( $false
| vertical_2_1
| horizontal_2_1 ),
inference(rewrite,[status(thm)],[439,396]) ).
thf(609,plain,
( vertical_2_1
| horizontal_2_1 ),
inference(simp,[status(thm)],[608]) ).
thf(84,negated_conjecture,
( ~ vertical_2_1
| ~ vertical_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_1) ).
thf(219,plain,
( ~ vertical_2_1
| ~ vertical_3_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(465,plain,
( ~ vertical_2_1
| ~ vertical_3_1 ),
inference(cnf,[status(esa)],[219]) ).
thf(667,plain,
( ( vertical_2_1 != vertical_2_1 )
| ~ $true
| ~ vertical_3_1
| horizontal_2_1 ),
inference(paramod_ordered,[status(thm)],[609,465]) ).
thf(668,plain,
( ( vertical_2_1 != vertical_2_1 )
| ~ vertical_3_1
| horizontal_2_1 ),
inference(simp,[status(thm)],[667]) ).
thf(669,plain,
( ~ vertical_3_1
| horizontal_2_1 ),
inference(pattern_uni,[status(thm)],[668:[]]) ).
thf(18308,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ $true
| horizontal_2_1
| vertical_2_4
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[18244,669]) ).
thf(18309,plain,
( ( vertical_3_1 != vertical_3_1 )
| horizontal_2_1
| vertical_2_4
| vertical_2_6 ),
inference(simp,[status(thm)],[18308]) ).
thf(18310,plain,
( horizontal_2_1
| vertical_2_4
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[18309:[]]) ).
thf(18368,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ $true
| horizontal_1_5
| horizontal_2_1
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[18310,585]) ).
thf(18369,plain,
( ( vertical_2_6 != vertical_2_6 )
| horizontal_1_5
| horizontal_2_1
| vertical_2_4 ),
inference(simp,[status(thm)],[18368]) ).
thf(18370,plain,
( horizontal_1_5
| horizontal_2_1
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[18369:[]]) ).
thf(5684,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ $true
| horizontal_2_1
| ~ vertical_2_5
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[5662,669]) ).
thf(5685,plain,
( ( vertical_3_1 != vertical_3_1 )
| horizontal_2_1
| ~ vertical_2_5
| vertical_2_6 ),
inference(simp,[status(thm)],[5684]) ).
thf(5686,plain,
( horizontal_2_1
| ~ vertical_2_5
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5685:[]]) ).
thf(5708,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ $true
| horizontal_1_5
| horizontal_2_1
| ~ vertical_2_5 ),
inference(paramod_ordered,[status(thm)],[5686,585]) ).
thf(5709,plain,
( ( vertical_2_6 != vertical_2_6 )
| horizontal_1_5
| horizontal_2_1
| ~ vertical_2_5 ),
inference(simp,[status(thm)],[5708]) ).
thf(5710,plain,
( horizontal_1_5
| horizontal_2_1
| ~ vertical_2_5 ),
inference(pattern_uni,[status(thm)],[5709:[]]) ).
thf(5771,plain,
( ( vertical_2_5 != vertical_2_5 )
| horizontal_1_5
| horizontal_2_1
| ~ $true
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(paramod_ordered,[status(thm)],[506,5710]) ).
thf(5772,plain,
( ( vertical_2_5 != vertical_2_5 )
| horizontal_1_5
| horizontal_2_1
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(simp,[status(thm)],[5771]) ).
thf(5773,plain,
( horizontal_1_5
| horizontal_2_1
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(pattern_uni,[status(thm)],[5772:[]]) ).
thf(7847,plain,
( ( horizontal_2_5 != horizontal_2_5 )
| ~ $true
| horizontal_1_5
| horizontal_1_5
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(paramod_ordered,[status(thm)],[5773,556]) ).
thf(7848,plain,
( ( horizontal_2_5 != horizontal_2_5 )
| horizontal_1_5
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(simp,[status(thm)],[7847]) ).
thf(7849,plain,
( horizontal_1_5
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(pattern_uni,[status(thm)],[7848:[]]) ).
thf(7868,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ vertical_2_4
| ~ $true
| horizontal_1_5
| horizontal_2_1
| vertical_1_5 ),
inference(paramod_ordered,[status(thm)],[7849,525]) ).
thf(7869,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ vertical_2_4
| horizontal_1_5
| horizontal_2_1
| vertical_1_5 ),
inference(simp,[status(thm)],[7868]) ).
thf(7870,plain,
( ~ vertical_2_4
| horizontal_1_5
| horizontal_2_1
| vertical_1_5 ),
inference(pattern_uni,[status(thm)],[7869:[]]) ).
thf(18431,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ $true
| horizontal_1_5
| horizontal_2_1
| vertical_1_5
| horizontal_1_5
| horizontal_2_1 ),
inference(paramod_ordered,[status(thm)],[18370,7870]) ).
thf(18432,plain,
( ( vertical_2_4 != vertical_2_4 )
| vertical_1_5
| horizontal_1_5
| horizontal_2_1 ),
inference(simp,[status(thm)],[18431]) ).
thf(18433,plain,
( vertical_1_5
| horizontal_1_5
| horizontal_2_1 ),
inference(pattern_uni,[status(thm)],[18432:[]]) ).
thf(58,negated_conjecture,
( ~ horizontal_2_1
| ~ vertical_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_2) ).
thf(342,plain,
( ~ horizontal_2_1
| ~ vertical_2_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(491,plain,
( ~ horizontal_2_1
| ~ vertical_2_2 ),
inference(cnf,[status(esa)],[342]) ).
thf(18572,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ $true
| ~ vertical_2_2
| vertical_1_5
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[18433,491]) ).
thf(18573,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ vertical_2_2
| vertical_1_5
| horizontal_1_5 ),
inference(simp,[status(thm)],[18572]) ).
thf(18574,plain,
( ~ vertical_2_2
| vertical_1_5
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[18573:[]]) ).
thf(22409,plain,
( ( vertical_2_2 != vertical_2_2 )
| ~ $true
| vertical_1_5
| horizontal_1_5
| vertical_1_5
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[22270,18574]) ).
thf(22410,plain,
( ( vertical_2_2 != vertical_2_2 )
| vertical_1_5
| horizontal_1_5 ),
inference(simp,[status(thm)],[22409]) ).
thf(22411,plain,
( vertical_1_5
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[22410:[]]) ).
thf(50,negated_conjecture,
( ~ horizontal_1_4
| ~ vertical_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_1_5) ).
thf(314,plain,
( ~ horizontal_1_4
| ~ vertical_1_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(504,plain,
( ~ horizontal_1_4
| ~ vertical_1_5 ),
inference(cnf,[status(esa)],[314]) ).
thf(22427,plain,
( ( vertical_1_5 != vertical_1_5 )
| ~ horizontal_1_4
| ~ $true
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[22411,504]) ).
thf(22428,plain,
( ( vertical_1_5 != vertical_1_5 )
| ~ horizontal_1_4
| horizontal_1_5 ),
inference(simp,[status(thm)],[22427]) ).
thf(22429,plain,
( ~ horizontal_1_4
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[22428:[]]) ).
thf(49,negated_conjecture,
( ~ horizontal_1_4
| ~ horizontal_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_1_5) ).
thf(282,plain,
( ~ horizontal_1_4
| ~ horizontal_1_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(495,plain,
( ~ horizontal_1_4
| ~ horizontal_1_5 ),
inference(cnf,[status(esa)],[282]) ).
thf(22454,plain,
( ( horizontal_1_5 != horizontal_1_5 )
| ~ horizontal_1_4
| ~ $true
| ~ horizontal_1_4 ),
inference(paramod_ordered,[status(thm)],[22429,495]) ).
thf(22455,plain,
( ( horizontal_1_5 != horizontal_1_5 )
| ~ horizontal_1_4 ),
inference(simp,[status(thm)],[22454]) ).
thf(22456,plain,
~ horizontal_1_4,
inference(pattern_uni,[status(thm)],[22455:[]]) ).
thf(22476,plain,
( ~ vertical_2_4
| horizontal_1_3
| $false ),
inference(rewrite,[status(thm)],[765,22456]) ).
thf(22477,plain,
( ~ vertical_2_4
| horizontal_1_3 ),
inference(simp,[status(thm)],[22476]) ).
thf(43,negated_conjecture,
( ~ horizontal_1_2
| ~ horizontal_1_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_1_3) ).
thf(326,plain,
( ~ horizontal_1_2
| ~ horizontal_1_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(531,plain,
( ~ horizontal_1_2
| ~ horizontal_1_3 ),
inference(cnf,[status(esa)],[326]) ).
thf(12,negated_conjecture,
( vertical_1_3
| horizontal_2_2
| vertical_2_3
| horizontal_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_2_3) ).
thf(279,plain,
( vertical_1_3
| horizontal_2_2
| vertical_2_3
| horizontal_2_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(452,plain,
( vertical_1_3
| horizontal_2_2
| vertical_2_3
| horizontal_2_3 ),
inference(cnf,[status(esa)],[279]) ).
thf(1355,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| ~ $true
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1039,443]) ).
thf(1356,plain,
( ( horizontal_5_2 != horizontal_5_2 )
| ~ vertical_4_3
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[1355]) ).
thf(1357,plain,
( ~ vertical_4_3
| vertical_5_1
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[1356:[]]) ).
thf(2549,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_3
| vertical_4_2
| horizontal_5_1 ),
inference(paramod_ordered,[status(thm)],[1357,458]) ).
thf(2550,plain,
( ( vertical_5_1 != vertical_5_1 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_2
| horizontal_5_1 ),
inference(simp,[status(thm)],[2549]) ).
thf(2551,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_2
| horizontal_5_1 ),
inference(pattern_uni,[status(thm)],[2550:[]]) ).
thf(3593,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| ~ $true
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[2551,392]) ).
thf(3594,plain,
( ( horizontal_5_1 != horizontal_5_1 )
| ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_2 ),
inference(simp,[status(thm)],[3593]) ).
thf(3595,plain,
( ~ vertical_4_1
| ~ vertical_4_3
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[3594:[]]) ).
thf(3671,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_4_1
| ~ $true
| vertical_4_2
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(paramod_ordered,[status(thm)],[499,3595]) ).
thf(3672,plain,
( ( vertical_4_3 != vertical_4_3 )
| ~ vertical_4_1
| vertical_4_2
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(simp,[status(thm)],[3671]) ).
thf(3673,plain,
( ~ vertical_4_1
| vertical_4_2
| vertical_3_3
| horizontal_4_2
| horizontal_4_3 ),
inference(pattern_uni,[status(thm)],[3672:[]]) ).
thf(6029,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ $true
| ~ vertical_4_1
| vertical_4_2 ),
inference(paramod_ordered,[status(thm)],[5977,485]) ).
thf(6030,plain,
( ( vertical_4_4 != vertical_4_4 )
| ~ horizontal_4_3
| ~ vertical_4_1
| vertical_4_2 ),
inference(simp,[status(thm)],[6029]) ).
thf(6031,plain,
( ~ horizontal_4_3
| ~ vertical_4_1
| vertical_4_2 ),
inference(pattern_uni,[status(thm)],[6030:[]]) ).
thf(11447,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ $true
| ~ vertical_4_1
| vertical_4_2
| ~ vertical_4_1
| vertical_4_2
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[3673,6031]) ).
thf(11448,plain,
( ( horizontal_4_3 != horizontal_4_3 )
| ~ vertical_4_1
| vertical_4_2
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[11447]) ).
thf(11449,plain,
( ~ vertical_4_1
| vertical_4_2
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[11448:[]]) ).
thf(11516,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(paramod_ordered,[status(thm)],[11449,533]) ).
thf(11517,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(simp,[status(thm)],[11516]) ).
thf(11518,plain,
( ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_3
| horizontal_4_2 ),
inference(pattern_uni,[status(thm)],[11517:[]]) ).
thf(11546,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[11518,550]) ).
thf(11547,plain,
( ( horizontal_4_2 != horizontal_4_2 )
| ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_3 ),
inference(simp,[status(thm)],[11546]) ).
thf(11548,plain,
( ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[11547:[]]) ).
thf(11639,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_2
| ~ $true
| vertical_3_3
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,11548]) ).
thf(11640,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_2
| vertical_3_3
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[11639]) ).
thf(11641,plain,
( ~ vertical_3_2
| vertical_3_3
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[11640:[]]) ).
thf(120,negated_conjecture,
( ~ vertical_3_2
| ~ horizontal_4_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_4_2) ).
thf(192,plain,
( ~ vertical_3_2
| ~ horizontal_4_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(422,plain,
( ~ vertical_3_2
| ~ horizontal_4_1 ),
inference(cnf,[status(esa)],[192]) ).
thf(11699,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_2
| vertical_3_3
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[11641,422]) ).
thf(11700,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_2
| vertical_3_3
| vertical_3_1 ),
inference(simp,[status(thm)],[11699]) ).
thf(11701,plain,
( ~ vertical_3_2
| vertical_3_3
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[11700:[]]) ).
thf(95,negated_conjecture,
( ~ vertical_2_3
| ~ vertical_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_3_3) ).
thf(313,plain,
( ~ vertical_2_3
| ~ vertical_3_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(460,plain,
( ~ vertical_2_3
| ~ vertical_3_3 ),
inference(cnf,[status(esa)],[313]) ).
thf(11708,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ vertical_2_3
| ~ $true
| ~ vertical_3_2
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[11701,460]) ).
thf(11709,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ vertical_2_3
| ~ vertical_3_2
| vertical_3_1 ),
inference(simp,[status(thm)],[11708]) ).
thf(11710,plain,
( ~ vertical_2_3
| ~ vertical_3_2
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[11709:[]]) ).
thf(11738,plain,
( ( vertical_3_2 != vertical_3_2 )
| ~ vertical_2_3
| ~ $true
| vertical_3_1
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(paramod_ordered,[status(thm)],[534,11710]) ).
thf(11739,plain,
( ( vertical_3_2 != vertical_3_2 )
| ~ vertical_2_3
| vertical_3_1
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(simp,[status(thm)],[11738]) ).
thf(11740,plain,
( ~ vertical_2_3
| vertical_3_1
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(pattern_uni,[status(thm)],[11739:[]]) ).
thf(96,negated_conjecture,
( ~ vertical_2_3
| ~ horizontal_3_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_3_3) ).
thf(252,plain,
( ~ vertical_2_3
| ~ horizontal_3_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(427,plain,
( ~ vertical_2_3
| ~ horizontal_3_2 ),
inference(cnf,[status(esa)],[252]) ).
thf(24178,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| ~ vertical_2_3
| ~ $true
| ~ vertical_2_3
| vertical_3_1
| vertical_2_2
| horizontal_3_1 ),
inference(paramod_ordered,[status(thm)],[11740,427]) ).
thf(24179,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| ~ vertical_2_3
| vertical_3_1
| vertical_2_2
| horizontal_3_1 ),
inference(simp,[status(thm)],[24178]) ).
thf(24180,plain,
( ~ vertical_2_3
| vertical_3_1
| vertical_2_2
| horizontal_3_1 ),
inference(pattern_uni,[status(thm)],[24179:[]]) ).
thf(24193,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ vertical_2_1
| ~ $true
| ~ vertical_2_3
| vertical_2_2
| horizontal_3_1 ),
inference(paramod_ordered,[status(thm)],[24180,465]) ).
thf(24194,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ vertical_2_1
| ~ vertical_2_3
| vertical_2_2
| horizontal_3_1 ),
inference(simp,[status(thm)],[24193]) ).
thf(24195,plain,
( ~ vertical_2_1
| ~ vertical_2_3
| vertical_2_2
| horizontal_3_1 ),
inference(pattern_uni,[status(thm)],[24194:[]]) ).
thf(83,negated_conjecture,
( ~ vertical_2_1
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_1) ).
thf(365,plain,
( ~ vertical_2_1
| ~ horizontal_3_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(370,plain,
( ~ vertical_2_1
| ~ horizontal_3_1 ),
inference(cnf,[status(esa)],[365]) ).
thf(24238,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| ~ vertical_2_1
| ~ $true
| ~ vertical_2_1
| ~ vertical_2_3
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[24195,370]) ).
thf(24239,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| ~ vertical_2_1
| ~ vertical_2_3
| vertical_2_2 ),
inference(simp,[status(thm)],[24238]) ).
thf(24240,plain,
( ~ vertical_2_1
| ~ vertical_2_3
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[24239:[]]) ).
thf(24256,plain,
( ( vertical_2_1 != vertical_2_1 )
| ~ $true
| ~ vertical_2_3
| vertical_2_2
| horizontal_2_1 ),
inference(paramod_ordered,[status(thm)],[609,24240]) ).
thf(24257,plain,
( ( vertical_2_1 != vertical_2_1 )
| ~ vertical_2_3
| vertical_2_2
| horizontal_2_1 ),
inference(simp,[status(thm)],[24256]) ).
thf(24258,plain,
( ~ vertical_2_3
| vertical_2_2
| horizontal_2_1 ),
inference(pattern_uni,[status(thm)],[24257:[]]) ).
thf(24259,plain,
( ( vertical_2_3 != vertical_2_3 )
| ~ $true
| vertical_2_2
| horizontal_2_1
| vertical_1_3
| horizontal_2_2
| horizontal_2_3 ),
inference(paramod_ordered,[status(thm)],[452,24258]) ).
thf(24260,plain,
( ( vertical_2_3 != vertical_2_3 )
| vertical_2_2
| horizontal_2_1
| vertical_1_3
| horizontal_2_2
| horizontal_2_3 ),
inference(simp,[status(thm)],[24259]) ).
thf(24261,plain,
( vertical_2_2
| horizontal_2_1
| vertical_1_3
| horizontal_2_2
| horizontal_2_3 ),
inference(pattern_uni,[status(thm)],[24260:[]]) ).
thf(8759,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ $true
| vertical_3_1
| ~ vertical_3_4 ),
inference(paramod_ordered,[status(thm)],[8638,514]) ).
thf(8760,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| vertical_3_1
| ~ vertical_3_4 ),
inference(simp,[status(thm)],[8759]) ).
thf(8761,plain,
( ~ vertical_2_5
| vertical_3_1
| ~ vertical_3_4 ),
inference(pattern_uni,[status(thm)],[8760:[]]) ).
thf(8849,plain,
( ( vertical_3_4 != vertical_3_4 )
| ~ vertical_2_5
| vertical_3_1
| ~ $true
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(paramod_ordered,[status(thm)],[463,8761]) ).
thf(8850,plain,
( ( vertical_3_4 != vertical_3_4 )
| ~ vertical_2_5
| vertical_3_1
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(simp,[status(thm)],[8849]) ).
thf(8851,plain,
( ~ vertical_2_5
| vertical_3_1
| vertical_2_4
| horizontal_3_3
| horizontal_3_4 ),
inference(pattern_uni,[status(thm)],[8850:[]]) ).
thf(108,negated_conjecture,
( ~ vertical_2_5
| ~ horizontal_3_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_3_5) ).
thf(298,plain,
( ~ vertical_2_5
| ~ horizontal_3_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(450,plain,
( ~ vertical_2_5
| ~ horizontal_3_4 ),
inference(cnf,[status(esa)],[298]) ).
thf(22785,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| ~ vertical_2_5
| ~ $true
| ~ vertical_2_5
| vertical_3_1
| vertical_2_4
| horizontal_3_3 ),
inference(paramod_ordered,[status(thm)],[8851,450]) ).
thf(22786,plain,
( ( horizontal_3_4 != horizontal_3_4 )
| ~ vertical_2_5
| vertical_3_1
| vertical_2_4
| horizontal_3_3 ),
inference(simp,[status(thm)],[22785]) ).
thf(22787,plain,
( ~ vertical_2_5
| vertical_3_1
| vertical_2_4
| horizontal_3_3 ),
inference(pattern_uni,[status(thm)],[22786:[]]) ).
thf(18158,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ $true
| vertical_3_1
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[18145,514]) ).
thf(18159,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| vertical_3_1
| vertical_3_3 ),
inference(simp,[status(thm)],[18158]) ).
thf(18160,plain,
( ~ vertical_2_5
| vertical_3_1
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[18159:[]]) ).
thf(18197,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ $true
| ~ horizontal_3_3
| ~ vertical_2_5
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[18160,494]) ).
thf(18198,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_3
| ~ vertical_2_5
| vertical_3_1 ),
inference(simp,[status(thm)],[18197]) ).
thf(18199,plain,
( ~ horizontal_3_3
| ~ vertical_2_5
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[18198:[]]) ).
thf(22851,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ $true
| ~ vertical_2_5
| vertical_3_1
| ~ vertical_2_5
| vertical_3_1
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[22787,18199]) ).
thf(22852,plain,
( ( horizontal_3_3 != horizontal_3_3 )
| ~ vertical_2_5
| vertical_3_1
| vertical_2_4 ),
inference(simp,[status(thm)],[22851]) ).
thf(22853,plain,
( ~ vertical_2_5
| vertical_3_1
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[22852:[]]) ).
thf(22878,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ $true
| horizontal_2_1
| ~ vertical_2_5
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[22853,669]) ).
thf(22879,plain,
( ( vertical_3_1 != vertical_3_1 )
| horizontal_2_1
| ~ vertical_2_5
| vertical_2_4 ),
inference(simp,[status(thm)],[22878]) ).
thf(22880,plain,
( horizontal_2_1
| ~ vertical_2_5
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[22879:[]]) ).
thf(22899,plain,
( ( vertical_2_5 != vertical_2_5 )
| horizontal_2_1
| ~ $true
| vertical_2_4
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(paramod_ordered,[status(thm)],[506,22880]) ).
thf(22900,plain,
( ( vertical_2_5 != vertical_2_5 )
| horizontal_2_1
| vertical_2_4
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(simp,[status(thm)],[22899]) ).
thf(22901,plain,
( horizontal_2_1
| vertical_2_4
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(pattern_uni,[status(thm)],[22900:[]]) ).
thf(79,negated_conjecture,
( ~ horizontal_2_5
| ~ vertical_2_6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_6) ).
thf(353,plain,
( ~ horizontal_2_5
| ~ vertical_2_6 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(401,plain,
( ~ horizontal_2_5
| ~ vertical_2_6 ),
inference(cnf,[status(esa)],[353]) ).
thf(18374,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ horizontal_2_5
| ~ $true
| horizontal_2_1
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[18310,401]) ).
thf(18375,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ horizontal_2_5
| horizontal_2_1
| vertical_2_4 ),
inference(simp,[status(thm)],[18374]) ).
thf(18376,plain,
( ~ horizontal_2_5
| horizontal_2_1
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[18375:[]]) ).
thf(22944,plain,
( ( horizontal_2_5 != horizontal_2_5 )
| ~ $true
| horizontal_2_1
| vertical_2_4
| horizontal_2_1
| vertical_2_4
| vertical_1_5
| horizontal_2_4 ),
inference(paramod_ordered,[status(thm)],[22901,18376]) ).
thf(22945,plain,
( ( horizontal_2_5 != horizontal_2_5 )
| horizontal_2_1
| vertical_2_4
| vertical_1_5
| horizontal_2_4 ),
inference(simp,[status(thm)],[22944]) ).
thf(22946,plain,
( horizontal_2_1
| vertical_2_4
| vertical_1_5
| horizontal_2_4 ),
inference(pattern_uni,[status(thm)],[22945:[]]) ).
thf(70,negated_conjecture,
( ~ horizontal_2_3
| ~ vertical_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_2_4) ).
thf(234,plain,
( ~ horizontal_2_3
| ~ vertical_2_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(372,plain,
( ~ horizontal_2_3
| ~ vertical_2_4 ),
inference(cnf,[status(esa)],[234]) ).
thf(22977,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ horizontal_2_3
| ~ $true
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(paramod_ordered,[status(thm)],[22946,372]) ).
thf(22978,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ horizontal_2_3
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(simp,[status(thm)],[22977]) ).
thf(22979,plain,
( ~ horizontal_2_3
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(pattern_uni,[status(thm)],[22978:[]]) ).
thf(68,negated_conjecture,
( ~ horizontal_2_3
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_2_4) ).
thf(359,plain,
( ~ horizontal_2_3
| ~ horizontal_2_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(502,plain,
( ~ horizontal_2_3
| ~ horizontal_2_4 ),
inference(cnf,[status(esa)],[359]) ).
thf(23028,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ horizontal_2_3
| ~ $true
| ~ horizontal_2_3
| horizontal_2_1
| vertical_1_5 ),
inference(paramod_ordered,[status(thm)],[22979,502]) ).
thf(23029,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ horizontal_2_3
| horizontal_2_1
| vertical_1_5 ),
inference(simp,[status(thm)],[23028]) ).
thf(23030,plain,
( ~ horizontal_2_3
| horizontal_2_1
| vertical_1_5 ),
inference(pattern_uni,[status(thm)],[23029:[]]) ).
thf(24262,plain,
( ( horizontal_2_3 != horizontal_2_3 )
| ~ $true
| horizontal_2_1
| vertical_1_5
| vertical_2_2
| horizontal_2_1
| vertical_1_3
| horizontal_2_2 ),
inference(paramod_ordered,[status(thm)],[24261,23030]) ).
thf(24263,plain,
( ( horizontal_2_3 != horizontal_2_3 )
| vertical_1_5
| vertical_2_2
| horizontal_2_1
| vertical_1_3
| horizontal_2_2 ),
inference(simp,[status(thm)],[24262]) ).
thf(24264,plain,
( vertical_1_5
| vertical_2_2
| horizontal_2_1
| vertical_1_3
| horizontal_2_2 ),
inference(pattern_uni,[status(thm)],[24263:[]]) ).
thf(5,negated_conjecture,
( horizontal_1_1
| vertical_1_2
| horizontal_1_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',covered_1_2) ).
thf(191,plain,
( horizontal_1_1
| vertical_1_2
| horizontal_1_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(454,plain,
( horizontal_1_1
| vertical_1_2
| horizontal_1_2 ),
inference(cnf,[status(esa)],[191]) ).
thf(1,negated_conjecture,
~ horizontal_1_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uncovered1_1_1) ).
thf(224,plain,
~ horizontal_1_1,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(433,plain,
~ horizontal_1_1,
inference(polarity_switch,[status(thm)],[224]) ).
thf(638,plain,
( $false
| vertical_1_2
| horizontal_1_2 ),
inference(rewrite,[status(thm)],[454,433]) ).
thf(639,plain,
( vertical_1_2
| horizontal_1_2 ),
inference(simp,[status(thm)],[638]) ).
thf(59,negated_conjecture,
( ~ vertical_1_2
| ~ vertical_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover5_2_2) ).
thf(276,plain,
( ~ vertical_1_2
| ~ vertical_2_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(381,plain,
( ~ vertical_1_2
| ~ vertical_2_2 ),
inference(cnf,[status(esa)],[276]) ).
thf(643,plain,
( ( vertical_1_2 != vertical_1_2 )
| ~ $true
| ~ vertical_2_2
| horizontal_1_2 ),
inference(paramod_ordered,[status(thm)],[639,381]) ).
thf(644,plain,
( ( vertical_1_2 != vertical_1_2 )
| ~ vertical_2_2
| horizontal_1_2 ),
inference(simp,[status(thm)],[643]) ).
thf(645,plain,
( ~ vertical_2_2
| horizontal_1_2 ),
inference(pattern_uni,[status(thm)],[644:[]]) ).
thf(24307,plain,
( ( vertical_2_2 != vertical_2_2 )
| ~ $true
| horizontal_1_2
| vertical_1_5
| horizontal_2_1
| vertical_1_3
| horizontal_2_2 ),
inference(paramod_ordered,[status(thm)],[24264,645]) ).
thf(24308,plain,
( ( vertical_2_2 != vertical_2_2 )
| horizontal_1_2
| vertical_1_5
| horizontal_2_1
| vertical_1_3
| horizontal_2_2 ),
inference(simp,[status(thm)],[24307]) ).
thf(24309,plain,
( horizontal_1_2
| vertical_1_5
| horizontal_2_1
| vertical_1_3
| horizontal_2_2 ),
inference(pattern_uni,[status(thm)],[24308:[]]) ).
thf(57,negated_conjecture,
( ~ vertical_1_2
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_2_2) ).
thf(212,plain,
( ~ vertical_1_2
| ~ horizontal_2_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(440,plain,
( ~ vertical_1_2
| ~ horizontal_2_2 ),
inference(cnf,[status(esa)],[212]) ).
thf(640,plain,
( ( vertical_1_2 != vertical_1_2 )
| ~ $true
| ~ horizontal_2_2
| horizontal_1_2 ),
inference(paramod_ordered,[status(thm)],[639,440]) ).
thf(641,plain,
( ( vertical_1_2 != vertical_1_2 )
| ~ horizontal_2_2
| horizontal_1_2 ),
inference(simp,[status(thm)],[640]) ).
thf(642,plain,
( ~ horizontal_2_2
| horizontal_1_2 ),
inference(pattern_uni,[status(thm)],[641:[]]) ).
thf(24391,plain,
( ( horizontal_2_2 != horizontal_2_2 )
| ~ $true
| horizontal_1_2
| horizontal_1_2
| vertical_1_5
| horizontal_2_1
| vertical_1_3 ),
inference(paramod_ordered,[status(thm)],[24309,642]) ).
thf(24392,plain,
( ( horizontal_2_2 != horizontal_2_2 )
| horizontal_1_2
| vertical_1_5
| horizontal_2_1
| vertical_1_3 ),
inference(simp,[status(thm)],[24391]) ).
thf(24393,plain,
( horizontal_1_2
| vertical_1_5
| horizontal_2_1
| vertical_1_3 ),
inference(pattern_uni,[status(thm)],[24392:[]]) ).
thf(60,negated_conjecture,
( ~ vertical_1_2
| ~ horizontal_2_1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_2_2) ).
thf(231,plain,
( ~ vertical_1_2
| ~ horizontal_2_1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(510,plain,
( ~ vertical_1_2
| ~ horizontal_2_1 ),
inference(cnf,[status(esa)],[231]) ).
thf(808,plain,
( ( vertical_1_2 != vertical_1_2 )
| ~ $true
| ~ horizontal_2_1
| horizontal_1_2 ),
inference(paramod_ordered,[status(thm)],[639,510]) ).
thf(809,plain,
( ( vertical_1_2 != vertical_1_2 )
| ~ horizontal_2_1
| horizontal_1_2 ),
inference(simp,[status(thm)],[808]) ).
thf(810,plain,
( ~ horizontal_2_1
| horizontal_1_2 ),
inference(pattern_uni,[status(thm)],[809:[]]) ).
thf(24424,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ $true
| horizontal_1_2
| horizontal_1_2
| vertical_1_5
| vertical_1_3 ),
inference(paramod_ordered,[status(thm)],[24393,810]) ).
thf(24425,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| horizontal_1_2
| vertical_1_5
| vertical_1_3 ),
inference(simp,[status(thm)],[24424]) ).
thf(24426,plain,
( horizontal_1_2
| vertical_1_5
| vertical_1_3 ),
inference(pattern_uni,[status(thm)],[24425:[]]) ).
thf(12011,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_4_1
| vertical_3_5 ),
inference(paramod_ordered,[status(thm)],[11944,533]) ).
thf(12012,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_5 ),
inference(simp,[status(thm)],[12011]) ).
thf(12013,plain,
( ~ vertical_3_2
| ~ vertical_4_1
| vertical_3_5 ),
inference(pattern_uni,[status(thm)],[12012:[]]) ).
thf(12041,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_2
| ~ $true
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,12013]) ).
thf(12042,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_2
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[12041]) ).
thf(12043,plain,
( ~ vertical_3_2
| vertical_3_5
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[12042:[]]) ).
thf(12173,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_2
| vertical_3_5
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[12043,422]) ).
thf(12174,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_2
| vertical_3_5
| vertical_3_1 ),
inference(simp,[status(thm)],[12173]) ).
thf(12175,plain,
( ~ vertical_3_2
| vertical_3_5
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[12174:[]]) ).
thf(3440,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(paramod_ordered,[status(thm)],[3424,533]) ).
thf(3441,plain,
( ( vertical_4_2 != vertical_4_2 )
| ~ vertical_3_2
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(simp,[status(thm)],[3440]) ).
thf(3442,plain,
( ~ vertical_3_2
| ~ vertical_3_6
| ~ vertical_4_1 ),
inference(pattern_uni,[status(thm)],[3441:[]]) ).
thf(3488,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_2
| ~ vertical_3_6
| ~ $true
| vertical_3_1
| horizontal_4_1 ),
inference(paramod_ordered,[status(thm)],[528,3442]) ).
thf(3489,plain,
( ( vertical_4_1 != vertical_4_1 )
| ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_1
| horizontal_4_1 ),
inference(simp,[status(thm)],[3488]) ).
thf(3490,plain,
( ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_1
| horizontal_4_1 ),
inference(pattern_uni,[status(thm)],[3489:[]]) ).
thf(4127,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_2
| ~ $true
| ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[3490,422]) ).
thf(4128,plain,
( ( horizontal_4_1 != horizontal_4_1 )
| ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_1 ),
inference(simp,[status(thm)],[4127]) ).
thf(4129,plain,
( ~ vertical_3_2
| ~ vertical_3_6
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[4128:[]]) ).
thf(4133,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| ~ $true
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(paramod_ordered,[status(thm)],[538,4129]) ).
thf(4134,plain,
( ( vertical_3_6 != vertical_3_6 )
| ~ vertical_3_2
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(simp,[status(thm)],[4133]) ).
thf(4135,plain,
( ~ vertical_3_2
| vertical_3_1
| vertical_2_6
| horizontal_3_5 ),
inference(pattern_uni,[status(thm)],[4134:[]]) ).
thf(5051,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ $true
| ~ vertical_3_2
| vertical_3_1
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[4135,406]) ).
thf(5052,plain,
( ( horizontal_3_5 != horizontal_3_5 )
| ~ vertical_3_5
| ~ vertical_3_2
| vertical_3_1
| vertical_2_6 ),
inference(simp,[status(thm)],[5051]) ).
thf(5053,plain,
( ~ vertical_3_5
| ~ vertical_3_2
| vertical_3_1
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[5052:[]]) ).
thf(12200,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ $true
| ~ vertical_3_2
| vertical_3_1
| vertical_2_6
| ~ vertical_3_2
| vertical_3_1 ),
inference(paramod_ordered,[status(thm)],[12175,5053]) ).
thf(12201,plain,
( ( vertical_3_5 != vertical_3_5 )
| vertical_2_6
| ~ vertical_3_2
| vertical_3_1 ),
inference(simp,[status(thm)],[12200]) ).
thf(12202,plain,
( vertical_2_6
| ~ vertical_3_2
| vertical_3_1 ),
inference(pattern_uni,[status(thm)],[12201:[]]) ).
thf(12263,plain,
( ( vertical_3_2 != vertical_3_2 )
| vertical_2_6
| ~ $true
| vertical_3_1
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(paramod_ordered,[status(thm)],[534,12202]) ).
thf(12264,plain,
( ( vertical_3_2 != vertical_3_2 )
| vertical_2_6
| vertical_3_1
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(simp,[status(thm)],[12263]) ).
thf(12265,plain,
( vertical_2_6
| vertical_3_1
| vertical_2_2
| horizontal_3_1
| horizontal_3_2 ),
inference(pattern_uni,[status(thm)],[12264:[]]) ).
thf(18236,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_2
| ~ $true
| vertical_3_1
| vertical_2_6 ),
inference(paramod_ordered,[status(thm)],[18223,545]) ).
thf(18237,plain,
( ( vertical_3_3 != vertical_3_3 )
| ~ horizontal_3_2
| vertical_3_1
| vertical_2_6 ),
inference(simp,[status(thm)],[18236]) ).
thf(18238,plain,
( ~ horizontal_3_2
| vertical_3_1
| vertical_2_6 ),
inference(pattern_uni,[status(thm)],[18237:[]]) ).
thf(18344,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| ~ $true
| vertical_3_1
| vertical_2_6
| vertical_2_6
| vertical_3_1
| vertical_2_2
| horizontal_3_1 ),
inference(paramod_ordered,[status(thm)],[12265,18238]) ).
thf(18345,plain,
( ( horizontal_3_2 != horizontal_3_2 )
| vertical_2_6
| vertical_3_1
| vertical_2_2
| horizontal_3_1 ),
inference(simp,[status(thm)],[18344]) ).
thf(18346,plain,
( vertical_2_6
| vertical_3_1
| vertical_2_2
| horizontal_3_1 ),
inference(pattern_uni,[status(thm)],[18345:[]]) ).
thf(18683,plain,
( ( vertical_3_1 != vertical_3_1 )
| ~ $true
| horizontal_2_1
| vertical_2_6
| vertical_2_2
| horizontal_3_1 ),
inference(paramod_ordered,[status(thm)],[18346,669]) ).
thf(18684,plain,
( ( vertical_3_1 != vertical_3_1 )
| horizontal_2_1
| vertical_2_6
| vertical_2_2
| horizontal_3_1 ),
inference(simp,[status(thm)],[18683]) ).
thf(18685,plain,
( horizontal_2_1
| vertical_2_6
| vertical_2_2
| horizontal_3_1 ),
inference(pattern_uni,[status(thm)],[18684:[]]) ).
thf(610,plain,
( ( vertical_2_1 != vertical_2_1 )
| ~ $true
| ~ horizontal_3_1
| horizontal_2_1 ),
inference(paramod_ordered,[status(thm)],[609,370]) ).
thf(611,plain,
( ( vertical_2_1 != vertical_2_1 )
| ~ horizontal_3_1
| horizontal_2_1 ),
inference(simp,[status(thm)],[610]) ).
thf(612,plain,
( ~ horizontal_3_1
| horizontal_2_1 ),
inference(pattern_uni,[status(thm)],[611:[]]) ).
thf(18956,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| ~ $true
| horizontal_2_1
| horizontal_2_1
| vertical_2_6
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[18685,612]) ).
thf(18957,plain,
( ( horizontal_3_1 != horizontal_3_1 )
| horizontal_2_1
| vertical_2_6
| vertical_2_2 ),
inference(simp,[status(thm)],[18956]) ).
thf(18958,plain,
( horizontal_2_1
| vertical_2_6
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[18957:[]]) ).
thf(18998,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ $true
| horizontal_1_5
| horizontal_2_1
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[18958,585]) ).
thf(18999,plain,
( ( vertical_2_6 != vertical_2_6 )
| horizontal_1_5
| horizontal_2_1
| vertical_2_2 ),
inference(simp,[status(thm)],[18998]) ).
thf(19000,plain,
( horizontal_1_5
| horizontal_2_1
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[18999:[]]) ).
thf(19028,plain,
( ( vertical_2_2 != vertical_2_2 )
| ~ $true
| horizontal_1_2
| horizontal_1_5
| horizontal_2_1 ),
inference(paramod_ordered,[status(thm)],[19000,645]) ).
thf(19029,plain,
( ( vertical_2_2 != vertical_2_2 )
| horizontal_1_2
| horizontal_1_5
| horizontal_2_1 ),
inference(simp,[status(thm)],[19028]) ).
thf(19030,plain,
( horizontal_1_2
| horizontal_1_5
| horizontal_2_1 ),
inference(pattern_uni,[status(thm)],[19029:[]]) ).
thf(19058,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ $true
| horizontal_1_2
| horizontal_1_2
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[19030,810]) ).
thf(19059,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| horizontal_1_2
| horizontal_1_5 ),
inference(simp,[status(thm)],[19058]) ).
thf(19060,plain,
( horizontal_1_2
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[19059:[]]) ).
thf(48,negated_conjecture,
( ~ vertical_1_5
| ~ horizontal_1_5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_1_5) ).
thf(309,plain,
( ~ vertical_1_5
| ~ horizontal_1_5 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(546,plain,
( ~ vertical_1_5
| ~ horizontal_1_5 ),
inference(cnf,[status(esa)],[309]) ).
thf(19070,plain,
( ( horizontal_1_5 != horizontal_1_5 )
| ~ vertical_1_5
| ~ $true
| horizontal_1_2 ),
inference(paramod_ordered,[status(thm)],[19060,546]) ).
thf(19071,plain,
( ( horizontal_1_5 != horizontal_1_5 )
| ~ vertical_1_5
| horizontal_1_2 ),
inference(simp,[status(thm)],[19070]) ).
thf(19072,plain,
( ~ vertical_1_5
| horizontal_1_2 ),
inference(pattern_uni,[status(thm)],[19071:[]]) ).
thf(24457,plain,
( ( vertical_1_5 != vertical_1_5 )
| ~ $true
| horizontal_1_2
| horizontal_1_2
| vertical_1_3 ),
inference(paramod_ordered,[status(thm)],[24426,19072]) ).
thf(24458,plain,
( ( vertical_1_5 != vertical_1_5 )
| horizontal_1_2
| vertical_1_3 ),
inference(simp,[status(thm)],[24457]) ).
thf(24459,plain,
( horizontal_1_2
| vertical_1_3 ),
inference(pattern_uni,[status(thm)],[24458:[]]) ).
thf(22480,plain,
( horizontal_1_3
| vertical_1_4
| $false ),
inference(rewrite,[status(thm)],[516,22456]) ).
thf(22481,plain,
( horizontal_1_3
| vertical_1_4 ),
inference(simp,[status(thm)],[22480]) ).
thf(22986,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ vertical_1_4
| ~ $true
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(paramod_ordered,[status(thm)],[22946,482]) ).
thf(22987,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ vertical_1_4
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(simp,[status(thm)],[22986]) ).
thf(22988,plain,
( ~ vertical_1_4
| horizontal_2_1
| vertical_1_5
| horizontal_2_4 ),
inference(pattern_uni,[status(thm)],[22987:[]]) ).
thf(69,negated_conjecture,
( ~ vertical_1_4
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_2_4) ).
thf(185,plain,
( ~ vertical_1_4
| ~ horizontal_2_4 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(382,plain,
( ~ vertical_1_4
| ~ horizontal_2_4 ),
inference(cnf,[status(esa)],[185]) ).
thf(23055,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ vertical_1_4
| ~ $true
| ~ vertical_1_4
| horizontal_2_1
| vertical_1_5 ),
inference(paramod_ordered,[status(thm)],[22988,382]) ).
thf(23056,plain,
( ( horizontal_2_4 != horizontal_2_4 )
| ~ vertical_1_4
| horizontal_2_1
| vertical_1_5 ),
inference(simp,[status(thm)],[23055]) ).
thf(23057,plain,
( ~ vertical_1_4
| horizontal_2_1
| vertical_1_5 ),
inference(pattern_uni,[status(thm)],[23056:[]]) ).
thf(23079,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ $true
| horizontal_1_2
| ~ vertical_1_4
| vertical_1_5 ),
inference(paramod_ordered,[status(thm)],[23057,810]) ).
thf(23080,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| horizontal_1_2
| ~ vertical_1_4
| vertical_1_5 ),
inference(simp,[status(thm)],[23079]) ).
thf(23081,plain,
( horizontal_1_2
| ~ vertical_1_4
| vertical_1_5 ),
inference(pattern_uni,[status(thm)],[23080:[]]) ).
thf(22208,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ vertical_1_6
| ~ $true
| vertical_2_4
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[22189,420]) ).
thf(22209,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ vertical_1_6
| vertical_2_4
| vertical_2_2 ),
inference(simp,[status(thm)],[22208]) ).
thf(22210,plain,
( ~ vertical_1_6
| vertical_2_4
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[22209:[]]) ).
thf(22238,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ vertical_1_4
| ~ $true
| ~ vertical_1_6
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[22210,482]) ).
thf(22239,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ vertical_1_4
| ~ vertical_1_6
| vertical_2_2 ),
inference(simp,[status(thm)],[22238]) ).
thf(22240,plain,
( ~ vertical_1_4
| ~ vertical_1_6
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[22239:[]]) ).
thf(18362,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ vertical_1_6
| ~ $true
| horizontal_2_1
| vertical_2_4 ),
inference(paramod_ordered,[status(thm)],[18310,420]) ).
thf(18363,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ vertical_1_6
| horizontal_2_1
| vertical_2_4 ),
inference(simp,[status(thm)],[18362]) ).
thf(18364,plain,
( ~ vertical_1_6
| horizontal_2_1
| vertical_2_4 ),
inference(pattern_uni,[status(thm)],[18363:[]]) ).
thf(18527,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ vertical_1_4
| ~ $true
| ~ vertical_1_6
| horizontal_2_1 ),
inference(paramod_ordered,[status(thm)],[18364,482]) ).
thf(18528,plain,
( ( vertical_2_4 != vertical_2_4 )
| ~ vertical_1_4
| ~ vertical_1_6
| horizontal_2_1 ),
inference(simp,[status(thm)],[18527]) ).
thf(18529,plain,
( ~ vertical_1_4
| ~ vertical_1_6
| horizontal_2_1 ),
inference(pattern_uni,[status(thm)],[18528:[]]) ).
thf(18887,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ $true
| ~ vertical_2_2
| ~ vertical_1_4
| ~ vertical_1_6 ),
inference(paramod_ordered,[status(thm)],[18529,491]) ).
thf(18888,plain,
( ( horizontal_2_1 != horizontal_2_1 )
| ~ vertical_2_2
| ~ vertical_1_4
| ~ vertical_1_6 ),
inference(simp,[status(thm)],[18887]) ).
thf(18889,plain,
( ~ vertical_2_2
| ~ vertical_1_4
| ~ vertical_1_6 ),
inference(pattern_uni,[status(thm)],[18888:[]]) ).
thf(22319,plain,
( ( vertical_2_2 != vertical_2_2 )
| ~ $true
| ~ vertical_1_4
| ~ vertical_1_6
| ~ vertical_1_4
| ~ vertical_1_6 ),
inference(paramod_ordered,[status(thm)],[22240,18889]) ).
thf(22320,plain,
( ( vertical_2_2 != vertical_2_2 )
| ~ vertical_1_4
| ~ vertical_1_6 ),
inference(simp,[status(thm)],[22319]) ).
thf(22321,plain,
( ~ vertical_1_4
| ~ vertical_1_6 ),
inference(pattern_uni,[status(thm)],[22320:[]]) ).
thf(22358,plain,
( ( vertical_1_6 != vertical_1_6 )
| ~ vertical_1_4
| ~ $true
| horizontal_1_5 ),
inference(paramod_ordered,[status(thm)],[469,22321]) ).
thf(22359,plain,
( ( vertical_1_6 != vertical_1_6 )
| ~ vertical_1_4
| horizontal_1_5 ),
inference(simp,[status(thm)],[22358]) ).
thf(22360,plain,
( ~ vertical_1_4
| horizontal_1_5 ),
inference(pattern_uni,[status(thm)],[22359:[]]) ).
thf(22361,plain,
( ( horizontal_1_5 != horizontal_1_5 )
| ~ vertical_1_5
| ~ $true
| ~ vertical_1_4 ),
inference(paramod_ordered,[status(thm)],[22360,546]) ).
thf(22362,plain,
( ( horizontal_1_5 != horizontal_1_5 )
| ~ vertical_1_5
| ~ vertical_1_4 ),
inference(simp,[status(thm)],[22361]) ).
thf(22363,plain,
( ~ vertical_1_5
| ~ vertical_1_4 ),
inference(pattern_uni,[status(thm)],[22362:[]]) ).
thf(23136,plain,
( ( vertical_1_5 != vertical_1_5 )
| ~ $true
| ~ vertical_1_4
| horizontal_1_2
| ~ vertical_1_4 ),
inference(paramod_ordered,[status(thm)],[23081,22363]) ).
thf(23137,plain,
( ( vertical_1_5 != vertical_1_5 )
| horizontal_1_2
| ~ vertical_1_4 ),
inference(simp,[status(thm)],[23136]) ).
thf(23138,plain,
( horizontal_1_2
| ~ vertical_1_4 ),
inference(pattern_uni,[status(thm)],[23137:[]]) ).
thf(23142,plain,
( ( vertical_1_4 != vertical_1_4 )
| horizontal_1_2
| ~ $true
| horizontal_1_3 ),
inference(paramod_ordered,[status(thm)],[22481,23138]) ).
thf(23143,plain,
( ( vertical_1_4 != vertical_1_4 )
| horizontal_1_2
| horizontal_1_3 ),
inference(simp,[status(thm)],[23142]) ).
thf(23144,plain,
( horizontal_1_2
| horizontal_1_3 ),
inference(pattern_uni,[status(thm)],[23143:[]]) ).
thf(42,negated_conjecture,
( ~ vertical_1_3
| ~ horizontal_1_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover1_1_3) ).
thf(198,plain,
( ~ vertical_1_3
| ~ horizontal_1_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(476,plain,
( ~ vertical_1_3
| ~ horizontal_1_3 ),
inference(cnf,[status(esa)],[198]) ).
thf(23145,plain,
( ( horizontal_1_3 != horizontal_1_3 )
| ~ vertical_1_3
| ~ $true
| horizontal_1_2 ),
inference(paramod_ordered,[status(thm)],[23144,476]) ).
thf(23146,plain,
( ( horizontal_1_3 != horizontal_1_3 )
| ~ vertical_1_3
| horizontal_1_2 ),
inference(simp,[status(thm)],[23145]) ).
thf(23147,plain,
( ~ vertical_1_3
| horizontal_1_2 ),
inference(pattern_uni,[status(thm)],[23146:[]]) ).
thf(24463,plain,
( ( vertical_1_3 != vertical_1_3 )
| ~ $true
| horizontal_1_2
| horizontal_1_2 ),
inference(paramod_ordered,[status(thm)],[24459,23147]) ).
thf(24464,plain,
( ( vertical_1_3 != vertical_1_3 )
| horizontal_1_2 ),
inference(simp,[status(thm)],[24463]) ).
thf(24465,plain,
horizontal_1_2,
inference(pattern_uni,[status(thm)],[24464:[]]) ).
thf(24485,plain,
( ~ $true
| ~ horizontal_1_3 ),
inference(rewrite,[status(thm)],[531,24465]) ).
thf(24486,plain,
~ horizontal_1_3,
inference(simp,[status(thm)],[24485]) ).
thf(24549,plain,
( ~ vertical_2_4
| $false ),
inference(rewrite,[status(thm)],[22477,24486]) ).
thf(24550,plain,
~ vertical_2_4,
inference(simp,[status(thm)],[24549]) ).
thf(24769,plain,
( $false
| horizontal_3_3
| vertical_3_4
| horizontal_3_4 ),
inference(rewrite,[status(thm)],[463,24550]) ).
thf(24770,plain,
( horizontal_3_3
| vertical_3_4
| horizontal_3_4 ),
inference(simp,[status(thm)],[24769]) ).
thf(935,plain,
( ( vertical_2_5 != vertical_2_5 )
| ~ $true
| ~ horizontal_3_4
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(paramod_ordered,[status(thm)],[506,450]) ).
thf(936,plain,
( ( vertical_2_5 != vertical_2_5 )
| ~ horizontal_3_4
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(simp,[status(thm)],[935]) ).
thf(937,plain,
( ~ horizontal_3_4
| vertical_1_5
| horizontal_2_4
| horizontal_2_5 ),
inference(pattern_uni,[status(thm)],[936:[]]) ).
thf(757,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ $true
| ~ horizontal_2_4
| horizontal_1_3
| horizontal_1_4 ),
inference(paramod_ordered,[status(thm)],[516,382]) ).
thf(758,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ horizontal_2_4
| horizontal_1_3
| horizontal_1_4 ),
inference(simp,[status(thm)],[757]) ).
thf(759,plain,
( ~ horizontal_2_4
| horizontal_1_3
| horizontal_1_4 ),
inference(pattern_uni,[status(thm)],[758:[]]) ).
thf(22484,plain,
( ~ horizontal_2_4
| horizontal_1_3
| $false ),
inference(rewrite,[status(thm)],[759,22456]) ).
thf(22485,plain,
( ~ horizontal_2_4
| horizontal_1_3 ),
inference(simp,[status(thm)],[22484]) ).
thf(24531,plain,
( ~ horizontal_2_4
| $false ),
inference(rewrite,[status(thm)],[22485,24486]) ).
thf(24532,plain,
~ horizontal_2_4,
inference(simp,[status(thm)],[24531]) ).
thf(24563,plain,
( ~ horizontal_3_4
| vertical_1_5
| $false
| horizontal_2_5 ),
inference(rewrite,[status(thm)],[937,24532]) ).
thf(24564,plain,
( ~ horizontal_3_4
| vertical_1_5
| horizontal_2_5 ),
inference(simp,[status(thm)],[24563]) ).
thf(22220,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ horizontal_2_5
| ~ $true
| vertical_2_4
| vertical_2_2 ),
inference(paramod_ordered,[status(thm)],[22189,401]) ).
thf(22221,plain,
( ( vertical_2_6 != vertical_2_6 )
| ~ horizontal_2_5
| vertical_2_4
| vertical_2_2 ),
inference(simp,[status(thm)],[22220]) ).
thf(22222,plain,
( ~ horizontal_2_5
| vertical_2_4
| vertical_2_2 ),
inference(pattern_uni,[status(thm)],[22221:[]]) ).
thf(24775,plain,
( ~ horizontal_2_5
| $false
| vertical_2_2 ),
inference(rewrite,[status(thm)],[22222,24550]) ).
thf(24776,plain,
( ~ horizontal_2_5
| vertical_2_2 ),
inference(simp,[status(thm)],[24775]) ).
thf(23076,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ $true
| horizontal_2_1
| vertical_1_5
| horizontal_1_3 ),
inference(paramod_ordered,[status(thm)],[22481,23057]) ).
thf(23077,plain,
( ( vertical_1_4 != vertical_1_4 )
| horizontal_2_1
| vertical_1_5
| horizontal_1_3 ),
inference(simp,[status(thm)],[23076]) ).
thf(23078,plain,
( horizontal_2_1
| vertical_1_5
| horizontal_1_3 ),
inference(pattern_uni,[status(thm)],[23077:[]]) ).
thf(24541,plain,
( horizontal_2_1
| vertical_1_5
| $false ),
inference(rewrite,[status(thm)],[23078,24486]) ).
thf(24542,plain,
( horizontal_2_1
| vertical_1_5 ),
inference(simp,[status(thm)],[24541]) ).
thf(22503,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ vertical_1_5
| ~ $true
| horizontal_1_3 ),
inference(paramod_ordered,[status(thm)],[22481,22363]) ).
thf(22504,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ vertical_1_5
| horizontal_1_3 ),
inference(simp,[status(thm)],[22503]) ).
thf(22505,plain,
( ~ vertical_1_5
| horizontal_1_3 ),
inference(pattern_uni,[status(thm)],[22504:[]]) ).
thf(24537,plain,
( ~ vertical_1_5
| $false ),
inference(rewrite,[status(thm)],[22505,24486]) ).
thf(24538,plain,
~ vertical_1_5,
inference(simp,[status(thm)],[24537]) ).
thf(24905,plain,
( horizontal_2_1
| $false ),
inference(rewrite,[status(thm)],[24542,24538]) ).
thf(24906,plain,
horizontal_2_1,
inference(simp,[status(thm)],[24905]) ).
thf(24911,plain,
( ~ $true
| ~ vertical_2_2 ),
inference(rewrite,[status(thm)],[491,24906]) ).
thf(24912,plain,
~ vertical_2_2,
inference(simp,[status(thm)],[24911]) ).
thf(25190,plain,
( ~ horizontal_2_5
| $false ),
inference(rewrite,[status(thm)],[24776,24912]) ).
thf(25191,plain,
~ horizontal_2_5,
inference(simp,[status(thm)],[25190]) ).
thf(25520,plain,
( ~ horizontal_3_4
| $false
| $false ),
inference(rewrite,[status(thm)],[24564,25191,24538]) ).
thf(25521,plain,
~ horizontal_3_4,
inference(simp,[status(thm)],[25520]) ).
thf(93,negated_conjecture,
( ~ vertical_2_3
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover3_3_3) ).
thf(210,plain,
( ~ vertical_2_3
| ~ horizontal_3_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(530,plain,
( ~ vertical_2_3
| ~ horizontal_3_3 ),
inference(cnf,[status(esa)],[210]) ).
thf(44,negated_conjecture,
( ~ horizontal_1_2
| ~ vertical_1_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover4_1_3) ).
thf(274,plain,
( ~ horizontal_1_2
| ~ vertical_1_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(466,plain,
( ~ horizontal_1_2
| ~ vertical_1_3 ),
inference(cnf,[status(esa)],[274]) ).
thf(24483,plain,
( ~ $true
| ~ vertical_1_3 ),
inference(rewrite,[status(thm)],[466,24465]) ).
thf(24484,plain,
~ vertical_1_3,
inference(simp,[status(thm)],[24483]) ).
thf(24501,plain,
( $false
| horizontal_2_2
| vertical_2_3
| horizontal_2_3 ),
inference(rewrite,[status(thm)],[452,24484]) ).
thf(24502,plain,
( horizontal_2_2
| vertical_2_3
| horizontal_2_3 ),
inference(simp,[status(thm)],[24501]) ).
thf(72,negated_conjecture,
( ~ vertical_1_4
| ~ horizontal_2_3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover6_2_4) ).
thf(323,plain,
( ~ vertical_1_4
| ~ horizontal_2_3 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(474,plain,
( ~ vertical_1_4
| ~ horizontal_2_3 ),
inference(cnf,[status(esa)],[323]) ).
thf(766,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ $true
| ~ horizontal_2_3
| horizontal_1_3
| horizontal_1_4 ),
inference(paramod_ordered,[status(thm)],[516,474]) ).
thf(767,plain,
( ( vertical_1_4 != vertical_1_4 )
| ~ horizontal_2_3
| horizontal_1_3
| horizontal_1_4 ),
inference(simp,[status(thm)],[766]) ).
thf(768,plain,
( ~ horizontal_2_3
| horizontal_1_3
| horizontal_1_4 ),
inference(pattern_uni,[status(thm)],[767:[]]) ).
thf(22478,plain,
( ~ horizontal_2_3
| horizontal_1_3
| $false ),
inference(rewrite,[status(thm)],[768,22456]) ).
thf(22479,plain,
( ~ horizontal_2_3
| horizontal_1_3 ),
inference(simp,[status(thm)],[22478]) ).
thf(24545,plain,
( ~ horizontal_2_3
| $false ),
inference(rewrite,[status(thm)],[22479,24486]) ).
thf(24546,plain,
~ horizontal_2_3,
inference(simp,[status(thm)],[24545]) ).
thf(56,negated_conjecture,
( ~ horizontal_2_1
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unique_cover2_2_2) ).
thf(194,plain,
( ~ horizontal_2_1
| ~ horizontal_2_2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(493,plain,
( ~ horizontal_2_1
| ~ horizontal_2_2 ),
inference(cnf,[status(esa)],[194]) ).
thf(24909,plain,
( ~ $true
| ~ horizontal_2_2 ),
inference(rewrite,[status(thm)],[493,24906]) ).
thf(24910,plain,
~ horizontal_2_2,
inference(simp,[status(thm)],[24909]) ).
thf(25293,plain,
( $false
| vertical_2_3
| $false ),
inference(rewrite,[status(thm)],[24502,24546,24910]) ).
thf(25294,plain,
vertical_2_3,
inference(simp,[status(thm)],[25293]) ).
thf(25297,plain,
( ~ $true
| ~ horizontal_3_3 ),
inference(rewrite,[status(thm)],[530,25294]) ).
thf(25298,plain,
~ horizontal_3_3,
inference(simp,[status(thm)],[25297]) ).
thf(20471,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ $true
| ~ vertical_3_4
| vertical_3_3 ),
inference(paramod_ordered,[status(thm)],[20410,514]) ).
thf(20472,plain,
( ( vertical_3_5 != vertical_3_5 )
| ~ vertical_2_5
| ~ vertical_3_4
| vertical_3_3 ),
inference(simp,[status(thm)],[20471]) ).
thf(20473,plain,
( ~ vertical_2_5
| ~ vertical_3_4
| vertical_3_3 ),
inference(pattern_uni,[status(thm)],[20472:[]]) ).
thf(25295,plain,
( ~ $true
| ~ vertical_3_3 ),
inference(rewrite,[status(thm)],[460,25294]) ).
thf(25296,plain,
~ vertical_3_3,
inference(simp,[status(thm)],[25295]) ).
thf(25319,plain,
( ~ vertical_2_5
| ~ vertical_3_4
| $false ),
inference(rewrite,[status(thm)],[20473,25296]) ).
thf(25320,plain,
( ~ vertical_2_5
| ~ vertical_3_4 ),
inference(simp,[status(thm)],[25319]) ).
thf(24619,plain,
( vertical_1_5
| $false
| vertical_2_5
| horizontal_2_5 ),
inference(rewrite,[status(thm)],[506,24532]) ).
thf(24620,plain,
( vertical_1_5
| vertical_2_5
| horizontal_2_5 ),
inference(simp,[status(thm)],[24619]) ).
thf(25526,plain,
( $false
| vertical_2_5
| $false ),
inference(rewrite,[status(thm)],[24620,25191,24538]) ).
thf(25527,plain,
vertical_2_5,
inference(simp,[status(thm)],[25526]) ).
thf(25530,plain,
( ~ $true
| ~ vertical_3_4 ),
inference(rewrite,[status(thm)],[25320,25527]) ).
thf(25531,plain,
~ vertical_3_4,
inference(simp,[status(thm)],[25530]) ).
thf(25821,plain,
( $false
| $false
| $false ),
inference(rewrite,[status(thm)],[24770,25521,25298,25531]) ).
thf(25822,plain,
$false,
inference(simp,[status(thm)],[25821]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ015-2.006 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.14/0.41 % Computer : n007.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sat Sep 26 05:02:09 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.26/1.21 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.84/1.56 % [INFO] Parsing done (339ms).
% 1.84/1.58 % [INFO] Running in sequential loop mode.
% 3.24/2.16 % [INFO] eprover registered as external prover.
% 3.24/2.17 % [INFO] Scanning for conjecture ...
% 3.70/2.44 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 3.88/2.56 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 3.88/2.56 % [INFO] Problem is propositional (TPTP CNF).
% 3.88/2.57 % [INFO] Type checking passed.
% 3.88/2.58 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 69.58/33.57 % [INFO] Killing All external provers ...
% 69.58/33.58 % Time passed: 32949ms (effective reasoning time: 31990ms)
% 69.58/33.59 % Axioms used in derivation (0):
% 69.58/33.59 % No. of inferences in proof: 1375
% 69.58/33.59 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 32949 ms resp. 31990 ms w/o parsing
% 70.55/33.81 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 70.55/33.84 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------