%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRA014+1 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:23:20 PM UTC 2025
% Result : Theorem 17.60s 8.79s
% Output : CNFRefutation 18.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 1625 ( 884 unt; 0 typ; 0 def)
% Number of atoms : 3133 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 2867 (1359 ~;1495 |; 9 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 460 ( 460 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ red > less_than > green > #nlpp > n6 > n5 > n4 > n3 > n2 > n1 > goal
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(green,type,
green: ( $i * $i ) > $o ).
tff(n3,type,
n3: $i ).
tff(goal,type,
goal: $o ).
tff(n1,type,
n1: $i ).
tff(red,type,
red: ( $i * $i ) > $o ).
tff(less_than,type,
less_than: ( $i * $i ) > $o ).
tff(n6,type,
n6: $i ).
tff(n4,type,
n4: $i ).
tff(n2,type,
n2: $i ).
tff(n5,type,
n5: $i ).
tff(f_50,axiom,
( less_than(n1,n2)
& less_than(n2,n3)
& less_than(n3,n4)
& less_than(n4,n5)
& less_than(n5,n6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordering) ).
tff(f_56,axiom,
! [A,B,C] :
( ( less_than(A,B)
& less_than(B,C) )
=> less_than(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_than_transitive) ).
tff(f_62,axiom,
! [A,B] :
( less_than(A,B)
=> ( red(A,B)
| green(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partition) ).
tff(f_64,negated_conjecture,
~ goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
tff(f_33,axiom,
! [A,B,C] :
( ( red(A,B)
& red(B,C)
& red(A,C) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',red_clique) ).
tff(f_41,axiom,
! [A,B,C] :
( ( green(A,B)
& green(B,C)
& green(A,C) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',green_clique) ).
tff(c_14,plain,
less_than(n1,n2),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_12,plain,
less_than(n2,n3),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_33,plain,
! [A_23,C_24,B_25] :
( less_than(A_23,C_24)
| ~ less_than(B_25,C_24)
| ~ less_than(A_23,B_25) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_46,plain,
! [A_23] :
( less_than(A_23,n3)
| ~ less_than(A_23,n2) ),
inference(resolution,[status(thm)],[c_12,c_33]) ).
tff(c_10,plain,
less_than(n3,n4),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_8,plain,
less_than(n4,n5),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_45,plain,
! [A_23] :
( less_than(A_23,n5)
| ~ less_than(A_23,n4) ),
inference(resolution,[status(thm)],[c_8,c_33]) ).
tff(c_6,plain,
less_than(n5,n6),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_61,plain,
! [A_29] :
( less_than(A_29,n6)
| ~ less_than(A_29,n5) ),
inference(resolution,[status(thm)],[c_6,c_33]) ).
tff(c_16,plain,
! [A_7,C_9,B_8] :
( less_than(A_7,C_9)
| ~ less_than(B_8,C_9)
| ~ less_than(A_7,B_8) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_211,plain,
! [A_41,A_42] :
( less_than(A_41,n6)
| ~ less_than(A_41,A_42)
| ~ less_than(A_42,n5) ),
inference(resolution,[status(thm)],[c_61,c_16]) ).
tff(c_237,plain,
! [A_23] :
( less_than(A_23,n6)
| ~ less_than(n3,n5)
| ~ less_than(A_23,n2) ),
inference(resolution,[status(thm)],[c_46,c_211]) ).
tff(c_135618,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_237]) ).
tff(c_135627,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_135618]) ).
tff(c_135633,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_135627]) ).
tff(c_135635,plain,
less_than(n3,n5),
inference(splitRight,[status(thm)],[c_237]) ).
tff(c_18,plain,
! [A_10,B_11] :
( green(A_10,B_11)
| red(A_10,B_11)
| ~ less_than(A_10,B_11) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_20,plain,
~ goal,
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_2,plain,
! [A_1,C_3,B_2] :
( goal
| ~ red(A_1,C_3)
| ~ red(B_2,C_3)
| ~ red(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_25,plain,
! [A_17,C_18,B_19] :
( ~ red(A_17,C_18)
| ~ red(B_19,C_18)
| ~ red(A_17,B_19) ),
inference(negUnitSimplification,[status(thm)],[c_20,c_2]) ).
tff(c_29,plain,
! [B_20,B_21,A_22] :
( ~ red(B_20,B_21)
| ~ red(A_22,B_20)
| green(A_22,B_21)
| ~ less_than(A_22,B_21) ),
inference(resolution,[status(thm)],[c_18,c_25]) ).
tff(c_106,plain,
! [A_33,A_34,B_35] :
( ~ red(A_33,A_34)
| green(A_33,B_35)
| ~ less_than(A_33,B_35)
| green(A_34,B_35)
| ~ less_than(A_34,B_35) ),
inference(resolution,[status(thm)],[c_18,c_29]) ).
tff(c_109,plain,
! [A_10,B_35,B_11] :
( green(A_10,B_35)
| ~ less_than(A_10,B_35)
| green(B_11,B_35)
| ~ less_than(B_11,B_35)
| green(A_10,B_11)
| ~ less_than(A_10,B_11) ),
inference(resolution,[status(thm)],[c_18,c_106]) ).
tff(c_135655,plain,
! [B_11] :
( green(n3,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n3,B_11)
| ~ less_than(n3,B_11) ),
inference(resolution,[status(thm)],[c_135635,c_109]) ).
tff(c_136181,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_135655]) ).
tff(c_44,plain,
! [A_23] :
( less_than(A_23,n4)
| ~ less_than(A_23,n3) ),
inference(resolution,[status(thm)],[c_10,c_33]) ).
tff(c_65,plain,
! [A_30] :
( less_than(A_30,n5)
| ~ less_than(A_30,n4) ),
inference(resolution,[status(thm)],[c_8,c_33]) ).
tff(c_116,plain,
! [A_36,A_37] :
( less_than(A_36,n5)
| ~ less_than(A_36,A_37)
| ~ less_than(A_37,n4) ),
inference(resolution,[status(thm)],[c_65,c_16]) ).
tff(c_151,plain,
( less_than(n1,n5)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_14,c_116]) ).
tff(c_108637,plain,
~ less_than(n2,n4),
inference(splitLeft,[status(thm)],[c_151]) ).
tff(c_108641,plain,
~ less_than(n2,n3),
inference(resolution,[status(thm)],[c_44,c_108637]) ).
tff(c_108645,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12,c_108641]) ).
tff(c_108646,plain,
less_than(n1,n5),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_108664,plain,
! [B_11] :
( green(n1,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_108646,c_109]) ).
tff(c_135712,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_108664]) ).
tff(c_4,plain,
! [A_4,C_6,B_5] :
( goal
| ~ green(A_4,C_6)
| ~ green(B_5,C_6)
| ~ green(A_4,B_5) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_21,plain,
! [A_4,C_6,B_5] :
( ~ green(A_4,C_6)
| ~ green(B_5,C_6)
| ~ green(A_4,B_5) ),
inference(negUnitSimplification,[status(thm)],[c_20,c_4]) ).
tff(c_135715,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_135712,c_21]) ).
tff(c_136186,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_136181,c_135715]) ).
tff(c_167,plain,
! [A_38,B_39,B_40] :
( green(A_38,B_39)
| ~ less_than(A_38,B_39)
| green(B_40,B_39)
| ~ less_than(B_40,B_39)
| green(A_38,B_40)
| ~ less_than(A_38,B_40) ),
inference(resolution,[status(thm)],[c_18,c_106]) ).
tff(c_198,plain,
! [B_40] :
( green(n2,n3)
| green(B_40,n3)
| ~ less_than(B_40,n3)
| green(n2,B_40)
| ~ less_than(n2,B_40) ),
inference(resolution,[status(thm)],[c_12,c_167]) ).
tff(c_133512,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_225,plain,
( less_than(n3,n6)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_10,c_211]) ).
tff(c_246,plain,
less_than(n3,n6),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_225]) ).
tff(c_266,plain,
! [B_11] :
( green(n3,n6)
| green(B_11,n6)
| ~ less_than(B_11,n6)
| green(n3,B_11)
| ~ less_than(n3,B_11) ),
inference(resolution,[status(thm)],[c_246,c_109]) ).
tff(c_133069,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_200,plain,
! [B_40] :
( green(n1,n2)
| green(B_40,n2)
| ~ less_than(B_40,n2)
| green(n1,B_40)
| ~ less_than(n1,B_40) ),
inference(resolution,[status(thm)],[c_14,c_167]) ).
tff(c_50735,plain,
green(n1,n2),
inference(splitLeft,[status(thm)],[c_200]) ).
tff(c_69585,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_237]) ).
tff(c_69594,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_69585]) ).
tff(c_69600,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_69594]) ).
tff(c_69602,plain,
less_than(n3,n5),
inference(splitRight,[status(thm)],[c_237]) ).
tff(c_69623,plain,
! [B_11] :
( green(n3,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n3,B_11)
| ~ less_than(n3,B_11) ),
inference(resolution,[status(thm)],[c_69602,c_109]) ).
tff(c_69651,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_69623]) ).
tff(c_50747,plain,
~ less_than(n2,n4),
inference(splitLeft,[status(thm)],[c_151]) ).
tff(c_50750,plain,
~ less_than(n2,n3),
inference(resolution,[status(thm)],[c_44,c_50747]) ).
tff(c_50754,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12,c_50750]) ).
tff(c_50755,plain,
less_than(n1,n5),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_50824,plain,
! [B_11] :
( green(n1,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_50755,c_109]) ).
tff(c_70902,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_50824]) ).
tff(c_70909,plain,
! [B_1648] :
( ~ green(B_1648,n5)
| ~ green(n1,B_1648) ),
inference(resolution,[status(thm)],[c_70902,c_21]) ).
tff(c_70915,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_69651,c_70909]) ).
tff(c_70452,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_50824]) ).
tff(c_70462,plain,
! [B_1634] :
( ~ green(B_1634,n5)
| ~ green(n1,B_1634) ),
inference(resolution,[status(thm)],[c_70452,c_21]) ).
tff(c_70471,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_69651,c_70462]) ).
tff(c_197,plain,
! [B_40] :
( green(n4,n5)
| green(B_40,n5)
| ~ less_than(B_40,n5)
| green(n4,B_40)
| ~ less_than(n4,B_40) ),
inference(resolution,[status(thm)],[c_8,c_167]) ).
tff(c_70067,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_69654,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_69651,c_21]) ).
tff(c_70072,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_70067,c_69654]) ).
tff(c_70470,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_70067,c_70462]) ).
tff(c_49,plain,
! [A_26] :
( less_than(A_26,n4)
| ~ less_than(A_26,n3) ),
inference(resolution,[status(thm)],[c_10,c_33]) ).
tff(c_50757,plain,
! [A_1241,A_1242] :
( less_than(A_1241,n4)
| ~ less_than(A_1241,A_1242)
| ~ less_than(A_1242,n3) ),
inference(resolution,[status(thm)],[c_49,c_16]) ).
tff(c_50783,plain,
( less_than(n1,n4)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_14,c_50757]) ).
tff(c_50804,plain,
less_than(n1,n4),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_50783]) ).
tff(c_50850,plain,
! [B_11] :
( green(n1,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_50804,c_109]) ).
tff(c_70664,plain,
! [B_1640] :
( green(B_1640,n4)
| ~ less_than(B_1640,n4)
| green(n1,B_1640)
| ~ less_than(n1,B_1640) ),
inference(negUnitSimplification,[status(thm)],[c_70470,c_50850]) ).
tff(c_70676,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_70664]) ).
tff(c_70687,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_70471,c_70072,c_70676]) ).
tff(c_70690,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_70687]) ).
tff(c_70694,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_70690]) ).
tff(c_70696,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_50824]) ).
tff(c_199,plain,
! [B_40] :
( green(n5,n6)
| green(B_40,n6)
| ~ less_than(B_40,n6)
| green(n5,B_40)
| ~ less_than(n5,B_40) ),
inference(resolution,[status(thm)],[c_6,c_167]) ).
tff(c_69688,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_69468,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_69471,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_69468,c_21]) ).
tff(c_69690,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_69688,c_69471]) ).
tff(c_69696,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_69651,c_69690]) ).
tff(c_69698,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_294,plain,
~ less_than(n2,n4),
inference(splitLeft,[status(thm)],[c_151]) ).
tff(c_297,plain,
~ less_than(n2,n3),
inference(resolution,[status(thm)],[c_44,c_294]) ).
tff(c_301,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12,c_297]) ).
tff(c_303,plain,
less_than(n2,n4),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_334,plain,
! [B_11] :
( green(n2,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_303,c_109]) ).
tff(c_47121,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_334]) ).
tff(c_196,plain,
! [B_40] :
( green(n3,n4)
| green(B_40,n4)
| ~ less_than(B_40,n4)
| green(n3,B_40)
| ~ less_than(n3,B_40) ),
inference(resolution,[status(thm)],[c_10,c_167]) ).
tff(c_576,plain,
green(n3,n4),
inference(splitLeft,[status(thm)],[c_196]) ).
tff(c_747,plain,
green(n1,n2),
inference(splitLeft,[status(thm)],[c_200]) ).
tff(c_132,plain,
( less_than(n2,n5)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_12,c_116]) ).
tff(c_149,plain,
less_than(n2,n5),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_132]) ).
tff(c_190,plain,
! [B_40] :
( green(n2,n5)
| green(B_40,n5)
| ~ less_than(B_40,n5)
| green(n2,B_40)
| ~ less_than(n2,B_40) ),
inference(resolution,[status(thm)],[c_149,c_167]) ).
tff(c_290,plain,
green(n2,n5),
inference(splitLeft,[status(thm)],[c_190]) ).
tff(c_450,plain,
! [A_47,A_48] :
( less_than(A_47,n4)
| ~ less_than(A_47,A_48)
| ~ less_than(A_48,n3) ),
inference(resolution,[status(thm)],[c_49,c_16]) ).
tff(c_484,plain,
( less_than(n1,n4)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_14,c_450]) ).
tff(c_513,plain,
less_than(n1,n4),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_484]) ).
tff(c_535,plain,
! [B_11] :
( green(n1,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_513,c_109]) ).
tff(c_731,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_535]) ).
tff(c_738,plain,
! [B_56] :
( ~ green(B_56,n4)
| ~ green(n1,B_56) ),
inference(resolution,[status(thm)],[c_731,c_21]) ).
tff(c_744,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_576,c_738]) ).
tff(c_1382,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_1550,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_233,plain,
( less_than(n1,n6)
| ~ less_than(n2,n5) ),
inference(resolution,[status(thm)],[c_14,c_211]) ).
tff(c_253,plain,
less_than(n1,n6),
inference(demodulation,[status(thm),theory(equality)],[c_149,c_233]) ).
tff(c_282,plain,
! [B_11] :
( green(n1,n6)
| green(B_11,n6)
| ~ less_than(B_11,n6)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_253,c_109]) ).
tff(c_1637,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_1644,plain,
! [B_78] :
( ~ green(B_78,n6)
| ~ green(n1,B_78) ),
inference(resolution,[status(thm)],[c_1637,c_21]) ).
tff(c_1650,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_1382,c_1644]) ).
tff(c_302,plain,
less_than(n1,n5),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_316,plain,
! [B_11] :
( green(n1,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_302,c_109]) ).
tff(c_1652,plain,
! [B_79] :
( green(B_79,n5)
| ~ less_than(B_79,n5)
| green(n1,B_79)
| ~ less_than(n1,B_79) ),
inference(negUnitSimplification,[status(thm)],[c_1650,c_316]) ).
tff(c_1782,plain,
! [A_82] :
( green(A_82,n5)
| green(n1,A_82)
| ~ less_than(n1,A_82)
| ~ less_than(A_82,n4) ),
inference(resolution,[status(thm)],[c_45,c_1652]) ).
tff(c_1818,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_1782]) ).
tff(c_1860,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_1818]) ).
tff(c_1861,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_744,c_1860]) ).
tff(c_293,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_290,c_21]) ).
tff(c_1883,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_1861,c_293]) ).
tff(c_1890,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1550,c_1883]) ).
tff(c_1937,plain,
! [B_85] :
( green(B_85,n6)
| ~ less_than(B_85,n6)
| green(n1,B_85)
| ~ less_than(n1,B_85) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_1949,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_1937]) ).
tff(c_1964,plain,
( green(n3,n6)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_744,c_1949]) ).
tff(c_1970,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_1964]) ).
tff(c_1973,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_1970]) ).
tff(c_1977,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_1973]) ).
tff(c_1978,plain,
green(n3,n6),
inference(splitRight,[status(thm)],[c_1964]) ).
tff(c_2116,plain,
! [B_87] :
( ~ green(B_87,n6)
| ~ green(n3,B_87) ),
inference(resolution,[status(thm)],[c_1978,c_21]) ).
tff(c_2122,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_1382,c_2116]) ).
tff(c_1979,plain,
less_than(n1,n3),
inference(splitRight,[status(thm)],[c_1964]) ).
tff(c_1893,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_1900,plain,
! [B_83] :
( ~ green(B_83,n5)
| ~ green(n1,B_83) ),
inference(resolution,[status(thm)],[c_1893,c_21]) ).
tff(c_1904,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_1900]) ).
tff(c_1909,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_1904]) ).
tff(c_1912,plain,
! [B_84] :
( green(B_84,n5)
| ~ less_than(B_84,n5)
| green(n1,B_84)
| ~ less_than(n1,B_84) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_2229,plain,
! [A_91] :
( green(A_91,n5)
| green(n1,A_91)
| ~ less_than(n1,A_91)
| ~ less_than(A_91,n4) ),
inference(resolution,[status(thm)],[c_45,c_1912]) ).
tff(c_2234,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_1979,c_2229]) ).
tff(c_2285,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_2234]) ).
tff(c_2287,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_744,c_2122,c_2285]) ).
tff(c_2289,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_2675,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_2685,plain,
! [B_99] :
( ~ green(B_99,n6)
| ~ green(n3,B_99) ),
inference(resolution,[status(thm)],[c_2675,c_21]) ).
tff(c_2694,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_1382,c_2685]) ).
tff(c_2459,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_2470,plain,
! [B_95] :
( ~ green(B_95,n6)
| ~ green(n1,B_95) ),
inference(resolution,[status(thm)],[c_2459,c_21]) ).
tff(c_2476,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_1382,c_2470]) ).
tff(c_2478,plain,
! [B_96] :
( green(B_96,n5)
| ~ less_than(B_96,n5)
| green(n1,B_96)
| ~ less_than(n1,B_96) ),
inference(negUnitSimplification,[status(thm)],[c_2476,c_316]) ).
tff(c_2695,plain,
! [A_100] :
( green(A_100,n5)
| green(n1,A_100)
| ~ less_than(n1,A_100)
| ~ less_than(A_100,n4) ),
inference(resolution,[status(thm)],[c_45,c_2478]) ).
tff(c_2731,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_2695]) ).
tff(c_2773,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_2731]) ).
tff(c_2775,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_744,c_2694,c_2773]) ).
tff(c_2777,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_64,plain,
! [A_7,A_29] :
( less_than(A_7,n6)
| ~ less_than(A_7,A_29)
| ~ less_than(A_29,n5) ),
inference(resolution,[status(thm)],[c_61,c_16]) ).
tff(c_322,plain,
( less_than(n2,n6)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_303,c_64]) ).
tff(c_333,plain,
less_than(n2,n6),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_322]) ).
tff(c_411,plain,
! [B_11] :
( green(n2,n6)
| green(B_11,n6)
| ~ less_than(B_11,n6)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_333,c_109]) ).
tff(c_3192,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_411]) ).
tff(c_2465,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_2459,c_21]) ).
tff(c_3194,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_3192,c_2465]) ).
tff(c_3202,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_3194]) ).
tff(c_3205,plain,
! [B_112] :
( green(B_112,n6)
| ~ less_than(B_112,n6)
| green(n2,B_112)
| ~ less_than(n2,B_112) ),
inference(splitRight,[status(thm)],[c_411]) ).
tff(c_3217,plain,
( green(n3,n6)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_246,c_3205]) ).
tff(c_3231,plain,
( green(n3,n6)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_3217]) ).
tff(c_3233,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2289,c_2777,c_3231]) ).
tff(c_3240,plain,
! [B_113] :
( green(B_113,n6)
| ~ less_than(B_113,n6)
| green(n1,B_113)
| ~ less_than(n1,B_113) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_3252,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_3240]) ).
tff(c_3268,plain,
( green(n3,n6)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_744,c_3252]) ).
tff(c_3273,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_3268]) ).
tff(c_3276,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_3273]) ).
tff(c_3280,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_3276]) ).
tff(c_3281,plain,
green(n3,n6),
inference(splitRight,[status(thm)],[c_3268]) ).
tff(c_3433,plain,
! [B_115] :
( ~ green(B_115,n6)
| ~ green(n3,B_115) ),
inference(resolution,[status(thm)],[c_3281,c_21]) ).
tff(c_3439,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_1382,c_3433]) ).
tff(c_3282,plain,
less_than(n1,n3),
inference(splitRight,[status(thm)],[c_3268]) ).
tff(c_3440,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_3447,plain,
! [B_116] :
( ~ green(B_116,n5)
| ~ green(n1,B_116) ),
inference(resolution,[status(thm)],[c_3440,c_21]) ).
tff(c_3451,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_3447]) ).
tff(c_3456,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_3451]) ).
tff(c_3566,plain,
! [B_120] :
( green(B_120,n5)
| ~ less_than(B_120,n5)
| green(n1,B_120)
| ~ less_than(n1,B_120) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_3804,plain,
! [A_124] :
( green(A_124,n5)
| green(n1,A_124)
| ~ less_than(n1,A_124)
| ~ less_than(A_124,n4) ),
inference(resolution,[status(thm)],[c_45,c_3566]) ).
tff(c_3809,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_3282,c_3804]) ).
tff(c_3860,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_3809]) ).
tff(c_3862,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_744,c_3439,c_3860]) ).
tff(c_3864,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_4049,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_4278,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_4297,plain,
! [B_133] :
( ~ green(B_133,n5)
| ~ green(n1,B_133) ),
inference(resolution,[status(thm)],[c_4278,c_21]) ).
tff(c_4301,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_4297]) ).
tff(c_4306,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_4301]) ).
tff(c_4321,plain,
! [B_134] :
( green(B_134,n5)
| ~ less_than(B_134,n5)
| green(n1,B_134)
| ~ less_than(n1,B_134) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_4446,plain,
! [A_137] :
( green(A_137,n5)
| green(n1,A_137)
| ~ less_than(n1,A_137)
| ~ less_than(A_137,n4) ),
inference(resolution,[status(thm)],[c_45,c_4321]) ).
tff(c_4482,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_4446]) ).
tff(c_4524,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_4482]) ).
tff(c_4525,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_744,c_4524]) ).
tff(c_4535,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_4525,c_293]) ).
tff(c_4541,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4049,c_4535]) ).
tff(c_4543,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_4845,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_4787,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_4794,plain,
! [B_143] :
( ~ green(B_143,n5)
| ~ green(n1,B_143) ),
inference(resolution,[status(thm)],[c_4787,c_21]) ).
tff(c_4798,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_4794]) ).
tff(c_4803,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_4798]) ).
tff(c_4806,plain,
! [B_144] :
( green(B_144,n5)
| ~ less_than(B_144,n5)
| green(n1,B_144)
| ~ less_than(n1,B_144) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_5060,plain,
! [A_151] :
( green(A_151,n5)
| green(n1,A_151)
| ~ less_than(n1,A_151)
| ~ less_than(A_151,n4) ),
inference(resolution,[status(thm)],[c_45,c_4806]) ).
tff(c_5096,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_5060]) ).
tff(c_5138,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_5096]) ).
tff(c_5139,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_744,c_5138]) ).
tff(c_5157,plain,
! [B_152] :
( ~ green(B_152,n5)
| ~ green(n3,B_152) ),
inference(resolution,[status(thm)],[c_5139,c_21]) ).
tff(c_5161,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_4845,c_5157]) ).
tff(c_5168,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_5161]) ).
tff(c_5170,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_47,plain,
! [A_23] :
( less_than(A_23,n6)
| ~ less_than(A_23,n5) ),
inference(resolution,[status(thm)],[c_6,c_33]) ).
tff(c_5913,plain,
! [A_185,B_186] :
( green(A_185,n6)
| green(B_186,n6)
| ~ less_than(B_186,n6)
| green(A_185,B_186)
| ~ less_than(A_185,B_186)
| ~ less_than(A_185,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_5929,plain,
! [A_185] :
( green(A_185,n6)
| green(n5,n6)
| green(A_185,n5)
| ~ less_than(A_185,n5) ),
inference(resolution,[status(thm)],[c_6,c_5913]) ).
tff(c_5944,plain,
! [A_187] :
( green(A_187,n6)
| green(A_187,n5)
| ~ less_than(A_187,n5) ),
inference(negUnitSimplification,[status(thm)],[c_3864,c_5929]) ).
tff(c_5962,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_5944]) ).
tff(c_5974,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_5170,c_5962]) ).
tff(c_4831,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_4837,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_4831,c_21]) ).
tff(c_5976,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_5974,c_4837]) ).
tff(c_5984,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_5976]) ).
tff(c_5986,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_6448,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_411]) ).
tff(c_4719,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_4722,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_4719,c_21]) ).
tff(c_6450,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_6448,c_4722]) ).
tff(c_6456,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_6450]) ).
tff(c_6651,plain,
! [B_199] :
( green(B_199,n6)
| ~ less_than(B_199,n6)
| green(n2,B_199)
| ~ less_than(n2,B_199) ),
inference(splitRight,[status(thm)],[c_411]) ).
tff(c_6663,plain,
( green(n3,n6)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_246,c_6651]) ).
tff(c_6677,plain,
( green(n3,n6)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_6663]) ).
tff(c_6679,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4543,c_5986,c_6677]) ).
tff(c_6682,plain,
! [B_200] :
( green(B_200,n6)
| ~ less_than(B_200,n6)
| green(n1,B_200)
| ~ less_than(n1,B_200) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_6698,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_6682]) ).
tff(c_6714,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_302,c_6698]) ).
tff(c_6715,plain,
green(n1,n5),
inference(negUnitSimplification,[status(thm)],[c_3864,c_6714]) ).
tff(c_6722,plain,
! [B_201] :
( ~ green(B_201,n5)
| ~ green(n1,B_201) ),
inference(resolution,[status(thm)],[c_6715,c_21]) ).
tff(c_6726,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_6722]) ).
tff(c_6731,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_6726]) ).
tff(c_6733,plain,
~ green(n1,n2),
inference(splitRight,[status(thm)],[c_200]) ).
tff(c_13312,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_11795,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_9727,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_9837,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_10117,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_9924,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_10098,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_10105,plain,
! [B_292] :
( ~ green(B_292,n6)
| ~ green(n1,B_292) ),
inference(resolution,[status(thm)],[c_10098,c_21]) ).
tff(c_10109,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_9727,c_10105]) ).
tff(c_10114,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9924,c_10109]) ).
tff(c_10131,plain,
! [B_294] :
( green(B_294,n6)
| ~ less_than(B_294,n6)
| green(n1,B_294)
| ~ less_than(n1,B_294) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_10139,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_333,c_10131]) ).
tff(c_10153,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10139]) ).
tff(c_10154,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_6733,c_10153]) ).
tff(c_10173,plain,
! [B_295] :
( ~ green(B_295,n6)
| ~ green(n2,B_295) ),
inference(resolution,[status(thm)],[c_10154,c_21]) ).
tff(c_10177,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_10117,c_10173]) ).
tff(c_10184,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9837,c_10177]) ).
tff(c_10186,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_10187,plain,
! [B_296] :
( green(B_296,n6)
| ~ less_than(B_296,n6)
| green(n1,B_296)
| ~ less_than(n1,B_296) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_10199,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_10187]) ).
tff(c_10215,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_744,c_10186,c_10199]) ).
tff(c_10228,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_10215]) ).
tff(c_10232,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10228]) ).
tff(c_10235,plain,
! [B_297] :
( green(B_297,n5)
| ~ less_than(B_297,n5)
| green(n1,B_297)
| ~ less_than(n1,B_297) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_10434,plain,
! [A_301] :
( green(A_301,n5)
| green(n1,A_301)
| ~ less_than(n1,A_301)
| ~ less_than(A_301,n4) ),
inference(resolution,[status(thm)],[c_45,c_10235]) ).
tff(c_10470,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_10434]) ).
tff(c_10512,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_10470]) ).
tff(c_10513,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_744,c_10512]) ).
tff(c_10525,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_10513,c_293]) ).
tff(c_10531,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9837,c_10525]) ).
tff(c_10533,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_10706,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_10713,plain,
! [B_305] :
( ~ green(B_305,n6)
| ~ green(n1,B_305) ),
inference(resolution,[status(thm)],[c_10706,c_21]) ).
tff(c_10719,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_9727,c_10713]) ).
tff(c_10802,plain,
! [B_307] :
( green(B_307,n5)
| ~ less_than(B_307,n5)
| green(n1,B_307)
| ~ less_than(n1,B_307) ),
inference(negUnitSimplification,[status(thm)],[c_10719,c_316]) ).
tff(c_11008,plain,
! [A_310] :
( green(A_310,n5)
| green(n1,A_310)
| ~ less_than(n1,A_310)
| ~ less_than(A_310,n4) ),
inference(resolution,[status(thm)],[c_45,c_10802]) ).
tff(c_11044,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_11008]) ).
tff(c_11086,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_11044]) ).
tff(c_11087,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_744,c_11086]) ).
tff(c_11190,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_11200,plain,
! [B_313] :
( ~ green(B_313,n6)
| ~ green(n3,B_313) ),
inference(resolution,[status(thm)],[c_11190,c_21]) ).
tff(c_11206,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_9727,c_11200]) ).
tff(c_11212,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11087,c_11206]) ).
tff(c_11214,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_223,plain,
! [A_23] :
( less_than(A_23,n6)
| ~ less_than(n4,n5)
| ~ less_than(A_23,n3) ),
inference(resolution,[status(thm)],[c_44,c_211]) ).
tff(c_597,plain,
! [A_50] :
( less_than(A_50,n6)
| ~ less_than(A_50,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_223]) ).
tff(c_11281,plain,
! [A_316,B_317] :
( green(A_316,n6)
| green(B_317,n6)
| ~ less_than(B_317,n6)
| green(A_316,B_317)
| ~ less_than(A_316,B_317)
| ~ less_than(A_316,n3) ),
inference(resolution,[status(thm)],[c_597,c_109]) ).
tff(c_11293,plain,
! [A_316] :
( green(A_316,n6)
| green(n3,n6)
| green(A_316,n3)
| ~ less_than(A_316,n3) ),
inference(resolution,[status(thm)],[c_246,c_11281]) ).
tff(c_11314,plain,
! [A_318] :
( green(A_318,n6)
| green(A_318,n3)
| ~ less_than(A_318,n3) ),
inference(negUnitSimplification,[status(thm)],[c_11214,c_11293]) ).
tff(c_11320,plain,
( green(n2,n6)
| green(n2,n3) ),
inference(resolution,[status(thm)],[c_12,c_11314]) ).
tff(c_11324,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_10533,c_11320]) ).
tff(c_11334,plain,
! [B_319] :
( ~ green(B_319,n6)
| ~ green(n2,B_319) ),
inference(resolution,[status(thm)],[c_11324,c_21]) ).
tff(c_11340,plain,
~ green(n2,n5),
inference(resolution,[status(thm)],[c_9727,c_11334]) ).
tff(c_11346,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_11340]) ).
tff(c_11349,plain,
! [B_320] :
( green(B_320,n6)
| ~ less_than(B_320,n6)
| green(n1,B_320)
| ~ less_than(n1,B_320) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_11357,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_333,c_11349]) ).
tff(c_11371,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_11357]) ).
tff(c_11372,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_6733,c_11371]) ).
tff(c_11470,plain,
! [B_321] :
( ~ green(B_321,n6)
| ~ green(n2,B_321) ),
inference(resolution,[status(thm)],[c_11372,c_21]) ).
tff(c_11474,plain,
~ green(n2,n5),
inference(resolution,[status(thm)],[c_9727,c_11470]) ).
tff(c_11479,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_11474]) ).
tff(c_11481,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_12099,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_11691,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_11697,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_11691,c_21]) ).
tff(c_12101,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_12099,c_11697]) ).
tff(c_12109,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_731,c_12101]) ).
tff(c_12111,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_12220,plain,
! [A_338,B_339] :
( green(A_338,n6)
| green(B_339,n6)
| ~ less_than(B_339,n6)
| green(A_338,B_339)
| ~ less_than(A_338,B_339)
| ~ less_than(A_338,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_12236,plain,
! [A_338] :
( green(A_338,n6)
| green(n5,n6)
| green(A_338,n5)
| ~ less_than(A_338,n5) ),
inference(resolution,[status(thm)],[c_6,c_12220]) ).
tff(c_12251,plain,
! [A_340] :
( green(A_340,n6)
| green(A_340,n5)
| ~ less_than(A_340,n5) ),
inference(negUnitSimplification,[status(thm)],[c_11481,c_12236]) ).
tff(c_12269,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_12251]) ).
tff(c_12280,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_12111,c_12269]) ).
tff(c_11882,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_11888,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_11882,c_21]) ).
tff(c_12282,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_12280,c_11888]) ).
tff(c_12290,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_12282]) ).
tff(c_12328,plain,
! [B_342] :
( green(B_342,n6)
| ~ less_than(B_342,n6)
| green(n3,B_342)
| ~ less_than(n3,B_342) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_12344,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_12328]) ).
tff(c_12358,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_11481,c_12344]) ).
tff(c_12397,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_12358]) ).
tff(c_12406,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_12397]) ).
tff(c_12412,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12406]) ).
tff(c_12413,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_12358]) ).
tff(c_12482,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_12413,c_293]) ).
tff(c_12489,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11795,c_12482]) ).
tff(c_12491,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_13174,plain,
! [A_364,B_365] :
( green(A_364,n3)
| green(B_365,n3)
| ~ less_than(B_365,n3)
| green(A_364,B_365)
| ~ less_than(A_364,B_365)
| ~ less_than(A_364,n2) ),
inference(resolution,[status(thm)],[c_46,c_167]) ).
tff(c_13178,plain,
! [A_364] :
( green(A_364,n3)
| green(n2,n3)
| green(A_364,n2)
| ~ less_than(A_364,n2) ),
inference(resolution,[status(thm)],[c_12,c_13174]) ).
tff(c_13183,plain,
! [A_366] :
( green(A_366,n3)
| green(A_366,n2)
| ~ less_than(A_366,n2) ),
inference(negUnitSimplification,[status(thm)],[c_12491,c_13178]) ).
tff(c_13189,plain,
( green(n1,n3)
| green(n1,n2) ),
inference(resolution,[status(thm)],[c_14,c_13183]) ).
tff(c_13194,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6733,c_744,c_13189]) ).
tff(c_13197,plain,
! [B_367] :
( green(B_367,n5)
| ~ less_than(B_367,n5)
| green(n1,B_367)
| ~ less_than(n1,B_367) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_13320,plain,
! [A_371] :
( green(A_371,n5)
| green(n1,A_371)
| ~ less_than(n1,A_371)
| ~ less_than(A_371,n4) ),
inference(resolution,[status(thm)],[c_45,c_13197]) ).
tff(c_13356,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_13320]) ).
tff(c_13398,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_13356]) ).
tff(c_13399,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_744,c_13398]) ).
tff(c_13411,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_13399,c_293]) ).
tff(c_13417,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13312,c_13411]) ).
tff(c_13419,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_14783,plain,
! [A_406,B_407] :
( green(A_406,n3)
| green(B_407,n3)
| ~ less_than(B_407,n3)
| green(A_406,B_407)
| ~ less_than(A_406,B_407)
| ~ less_than(A_406,n2) ),
inference(resolution,[status(thm)],[c_46,c_167]) ).
tff(c_14787,plain,
! [A_406] :
( green(A_406,n3)
| green(n2,n3)
| green(A_406,n2)
| ~ less_than(A_406,n2) ),
inference(resolution,[status(thm)],[c_12,c_14783]) ).
tff(c_14792,plain,
! [A_408] :
( green(A_408,n3)
| green(A_408,n2)
| ~ less_than(A_408,n2) ),
inference(negUnitSimplification,[status(thm)],[c_13419,c_14787]) ).
tff(c_14798,plain,
( green(n1,n3)
| green(n1,n2) ),
inference(resolution,[status(thm)],[c_14,c_14792]) ).
tff(c_14803,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6733,c_744,c_14798]) ).
tff(c_14805,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_339,plain,
! [A_7] :
( less_than(A_7,n4)
| ~ less_than(A_7,n2) ),
inference(resolution,[status(thm)],[c_303,c_16]) ).
tff(c_19608,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_17023,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_16844,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_16847,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_16844,c_21]) ).
tff(c_17028,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_17023,c_16847]) ).
tff(c_17291,plain,
! [B_465] :
( green(B_465,n5)
| ~ less_than(B_465,n5)
| green(n1,B_465)
| ~ less_than(n1,B_465) ),
inference(negUnitSimplification,[status(thm)],[c_17028,c_316]) ).
tff(c_17303,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_17291]) ).
tff(c_17315,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_17303]) ).
tff(c_17316,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_14805,c_17315]) ).
tff(c_14806,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_15246,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_15253,plain,
! [B_421] :
( ~ green(B_421,n5)
| ~ green(n1,B_421) ),
inference(resolution,[status(thm)],[c_15246,c_21]) ).
tff(c_15259,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_15253]) ).
tff(c_15260,plain,
! [B_422] :
( green(B_422,n4)
| ~ less_than(B_422,n4)
| green(n1,B_422)
| ~ less_than(n1,B_422) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_15268,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_303,c_15260]) ).
tff(c_15280,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_15268]) ).
tff(c_15281,plain,
green(n2,n4),
inference(negUnitSimplification,[status(thm)],[c_15259,c_15280]) ).
tff(c_15291,plain,
! [B_423] :
( ~ green(B_423,n4)
| ~ green(n2,B_423) ),
inference(resolution,[status(thm)],[c_15281,c_21]) ).
tff(c_15295,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_576,c_15291]) ).
tff(c_15300,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14806,c_15295]) ).
tff(c_15497,plain,
! [B_429] :
( green(B_429,n5)
| ~ less_than(B_429,n5)
| green(n1,B_429)
| ~ less_than(n1,B_429) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_15509,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_15497]) ).
tff(c_15521,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_15509]) ).
tff(c_15522,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_14805,c_15521]) ).
tff(c_15527,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_15522,c_293]) ).
tff(c_15472,plain,
! [B_428] :
( green(B_428,n4)
| ~ less_than(B_428,n4)
| green(n1,B_428)
| ~ less_than(n1,B_428) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_15480,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_303,c_15472]) ).
tff(c_15492,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_15480]) ).
tff(c_15536,plain,
green(n1,n2),
inference(negUnitSimplification,[status(thm)],[c_15527,c_15492]) ).
tff(c_16705,plain,
! [A_450] :
( green(A_450,n5)
| green(n1,A_450)
| ~ less_than(n1,A_450)
| ~ less_than(A_450,n4) ),
inference(resolution,[status(thm)],[c_45,c_15497]) ).
tff(c_16741,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_16705]) ).
tff(c_16783,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_16741]) ).
tff(c_16793,plain,
green(n1,n3),
inference(splitLeft,[status(thm)],[c_16783]) ).
tff(c_16819,plain,
! [B_452] :
( ~ green(B_452,n3)
| ~ green(n1,B_452) ),
inference(resolution,[status(thm)],[c_16793,c_21]) ).
tff(c_16823,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_14806,c_16819]) ).
tff(c_16828,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_15536,c_16823]) ).
tff(c_16829,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_16783]) ).
tff(c_16834,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_16829,c_293]) ).
tff(c_16841,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14806,c_16834]) ).
tff(c_16843,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_17361,plain,
! [A_469] :
( green(A_469,n5)
| green(n1,A_469)
| ~ less_than(n1,A_469)
| ~ less_than(A_469,n4) ),
inference(resolution,[status(thm)],[c_45,c_17291]) ).
tff(c_17397,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_17361]) ).
tff(c_17442,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_17397]) ).
tff(c_17452,plain,
green(n1,n3),
inference(splitLeft,[status(thm)],[c_17442]) ).
tff(c_18437,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_18441,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_18437,c_16847]) ).
tff(c_18448,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17452,c_18441]) ).
tff(c_18450,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_17321,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_17316,c_293]) ).
tff(c_17330,plain,
! [B_467] :
( green(B_467,n4)
| ~ less_than(B_467,n4)
| green(n1,B_467)
| ~ less_than(n1,B_467) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_17338,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_303,c_17330]) ).
tff(c_17349,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_17338]) ).
tff(c_17350,plain,
green(n1,n2),
inference(negUnitSimplification,[status(thm)],[c_17321,c_17349]) ).
tff(c_18644,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_411]) ).
tff(c_18648,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_18644,c_16847]) ).
tff(c_18655,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_17350,c_18648]) ).
tff(c_18757,plain,
! [B_496] :
( green(B_496,n6)
| ~ less_than(B_496,n6)
| green(n2,B_496)
| ~ less_than(n2,B_496) ),
inference(splitRight,[status(thm)],[c_411]) ).
tff(c_18769,plain,
( green(n3,n6)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_246,c_18757]) ).
tff(c_18783,plain,
( green(n3,n6)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_18769]) ).
tff(c_18785,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16843,c_18450,c_18783]) ).
tff(c_18786,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_17442]) ).
tff(c_18797,plain,
! [B_497] :
( ~ green(B_497,n5)
| ~ green(n3,B_497) ),
inference(resolution,[status(thm)],[c_18786,c_21]) ).
tff(c_18801,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_17316,c_18797]) ).
tff(c_18808,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_18801]) ).
tff(c_18810,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_19913,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_19918,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_19913,c_16847]) ).
tff(c_19241,plain,
! [B_509] :
( green(B_509,n4)
| ~ less_than(B_509,n4)
| green(n1,B_509)
| ~ less_than(n1,B_509) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_19249,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_303,c_19241]) ).
tff(c_19261,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_19249]) ).
tff(c_19265,plain,
green(n1,n2),
inference(splitLeft,[status(thm)],[c_19261]) ).
tff(c_19547,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_19554,plain,
! [B_515] :
( ~ green(B_515,n5)
| ~ green(n1,B_515) ),
inference(resolution,[status(thm)],[c_19547,c_21]) ).
tff(c_19558,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_19554]) ).
tff(c_19563,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_19265,c_19558]) ).
tff(c_19566,plain,
! [B_516] :
( green(B_516,n5)
| ~ less_than(B_516,n5)
| green(n1,B_516)
| ~ less_than(n1,B_516) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_19927,plain,
! [A_523] :
( green(A_523,n5)
| green(n1,A_523)
| ~ less_than(n1,A_523)
| ~ less_than(A_523,n4) ),
inference(resolution,[status(thm)],[c_45,c_19566]) ).
tff(c_19963,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n3,n4)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_46,c_19927]) ).
tff(c_20008,plain,
( green(n3,n5)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_10,c_19963]) ).
tff(c_20009,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_19918,c_20008]) ).
tff(c_20052,plain,
! [B_526] :
( ~ green(B_526,n5)
| ~ green(n3,B_526) ),
inference(resolution,[status(thm)],[c_20009,c_21]) ).
tff(c_20056,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_19608,c_20052]) ).
tff(c_20063,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_20056]) ).
tff(c_20077,plain,
! [B_527] :
( green(B_527,n6)
| ~ less_than(B_527,n6)
| green(n3,B_527)
| ~ less_than(n3,B_527) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_20093,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_20077]) ).
tff(c_20107,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_18810,c_20093]) ).
tff(c_20120,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_20107]) ).
tff(c_20129,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_20120]) ).
tff(c_20135,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_20129]) ).
tff(c_20136,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_20107]) ).
tff(c_20314,plain,
! [B_533] :
( ~ green(B_533,n5)
| ~ green(n3,B_533) ),
inference(resolution,[status(thm)],[c_20136,c_21]) ).
tff(c_20318,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_19608,c_20314]) ).
tff(c_20325,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_20318]) ).
tff(c_20327,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_19578,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_19566]) ).
tff(c_19589,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_19578]) ).
tff(c_19590,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_14805,c_19589]) ).
tff(c_20328,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20327,c_19590]) ).
tff(c_20329,plain,
green(n2,n4),
inference(splitRight,[status(thm)],[c_19261]) ).
tff(c_20330,plain,
~ green(n1,n2),
inference(splitRight,[status(thm)],[c_19261]) ).
tff(c_21100,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_21104,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_21100,c_293]) ).
tff(c_21111,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20329,c_21104]) ).
tff(c_21113,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_21983,plain,
! [A_590,B_591] :
( green(A_590,n6)
| green(B_591,n6)
| ~ less_than(B_591,n6)
| green(A_590,B_591)
| ~ less_than(A_590,B_591)
| ~ less_than(A_590,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_21999,plain,
! [A_590] :
( green(A_590,n6)
| green(n5,n6)
| green(A_590,n5)
| ~ less_than(A_590,n5) ),
inference(resolution,[status(thm)],[c_6,c_21983]) ).
tff(c_22014,plain,
! [A_592] :
( green(A_592,n6)
| green(A_592,n5)
| ~ less_than(A_592,n5) ),
inference(negUnitSimplification,[status(thm)],[c_18810,c_21999]) ).
tff(c_22032,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_22014]) ).
tff(c_22043,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_21113,c_22032]) ).
tff(c_21025,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_21031,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_21025,c_21]) ).
tff(c_22045,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_22043,c_21031]) ).
tff(c_22053,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_22045]) ).
tff(c_22056,plain,
! [B_593] :
( green(B_593,n6)
| ~ less_than(B_593,n6)
| green(n3,B_593)
| ~ less_than(n3,B_593) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_22072,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_22056]) ).
tff(c_22086,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_18810,c_22072]) ).
tff(c_22105,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_22086]) ).
tff(c_22115,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_22105]) ).
tff(c_22121,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_22115]) ).
tff(c_22122,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_22086]) ).
tff(c_20538,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_20544,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_20538,c_21]) ).
tff(c_22184,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_22122,c_20544]) ).
tff(c_22855,plain,
! [A_613,B_614] :
( green(A_613,n3)
| green(B_614,n3)
| ~ less_than(B_614,n3)
| green(A_613,B_614)
| ~ less_than(A_613,B_614)
| ~ less_than(A_613,n2) ),
inference(resolution,[status(thm)],[c_46,c_167]) ).
tff(c_22859,plain,
! [A_613] :
( green(A_613,n3)
| green(n2,n3)
| green(A_613,n2)
| ~ less_than(A_613,n2) ),
inference(resolution,[status(thm)],[c_12,c_22855]) ).
tff(c_22864,plain,
! [A_615] :
( green(A_615,n3)
| green(A_615,n2)
| ~ less_than(A_615,n2) ),
inference(negUnitSimplification,[status(thm)],[c_16843,c_22859]) ).
tff(c_22870,plain,
( green(n1,n3)
| green(n1,n2) ),
inference(resolution,[status(thm)],[c_14,c_22864]) ).
tff(c_22875,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20330,c_22184,c_22870]) ).
tff(c_22878,plain,
! [B_616] :
( green(B_616,n5)
| ~ less_than(B_616,n5)
| green(n1,B_616)
| ~ less_than(n1,B_616) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_22890,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_22878]) ).
tff(c_22902,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_22890]) ).
tff(c_22903,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_14805,c_22902]) ).
tff(c_22914,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_22903,c_293]) ).
tff(c_22920,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20329,c_22914]) ).
tff(c_25927,plain,
! [B_680] :
( green(B_680,n6)
| ~ less_than(B_680,n6)
| green(n1,B_680)
| ~ less_than(n1,B_680) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_26317,plain,
! [A_688] :
( green(A_688,n6)
| green(n1,A_688)
| ~ less_than(n1,A_688)
| ~ less_than(A_688,n5) ),
inference(resolution,[status(thm)],[c_47,c_25927]) ).
tff(c_26328,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_339,c_26317]) ).
tff(c_26377,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_26328]) ).
tff(c_26378,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_14805,c_26377]) ).
tff(c_25954,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_25927]) ).
tff(c_25982,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_25954]) ).
tff(c_25985,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_25982]) ).
tff(c_25989,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_25985]) ).
tff(c_25990,plain,
( green(n1,n3)
| green(n3,n6) ),
inference(splitRight,[status(thm)],[c_25954]) ).
tff(c_26052,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_25990]) ).
tff(c_26058,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_26052,c_21]) ).
tff(c_26430,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_26378,c_26058]) ).
tff(c_26438,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_26430]) ).
tff(c_26439,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_25990]) ).
tff(c_23181,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_23532,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_23539,plain,
! [B_634] :
( ~ green(B_634,n5)
| ~ green(n1,B_634) ),
inference(resolution,[status(thm)],[c_23532,c_21]) ).
tff(c_23545,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_23539]) ).
tff(c_23584,plain,
! [B_637] :
( green(B_637,n6)
| ~ less_than(B_637,n6)
| green(n1,B_637)
| ~ less_than(n1,B_637) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_23592,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_333,c_23584]) ).
tff(c_23606,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_23592]) ).
tff(c_23607,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_23545,c_23606]) ).
tff(c_23621,plain,
! [B_638] :
( ~ green(B_638,n6)
| ~ green(n2,B_638) ),
inference(resolution,[status(thm)],[c_23607,c_21]) ).
tff(c_23625,plain,
~ green(n2,n5),
inference(resolution,[status(thm)],[c_23181,c_23621]) ).
tff(c_23630,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_23625]) ).
tff(c_23699,plain,
! [B_642] :
( green(B_642,n5)
| ~ less_than(B_642,n5)
| green(n1,B_642)
| ~ less_than(n1,B_642) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_23711,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_23699]) ).
tff(c_23722,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_23711]) ).
tff(c_23723,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_14805,c_23722]) ).
tff(c_23668,plain,
! [B_641] :
( green(B_641,n6)
| ~ less_than(B_641,n6)
| green(n1,B_641)
| ~ less_than(n1,B_641) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_23693,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_23668]) ).
tff(c_23737,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_23693]) ).
tff(c_23740,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_23737]) ).
tff(c_23744,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_23740]) ).
tff(c_23746,plain,
less_than(n1,n3),
inference(splitRight,[status(thm)],[c_23693]) ).
tff(c_25385,plain,
! [A_666] :
( green(A_666,n6)
| green(n1,A_666)
| ~ less_than(n1,A_666)
| ~ less_than(A_666,n5) ),
inference(resolution,[status(thm)],[c_47,c_23668]) ).
tff(c_25432,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_44,c_25385]) ).
tff(c_25493,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_23746,c_8,c_25432]) ).
tff(c_25494,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_14805,c_25493]) ).
tff(c_25507,plain,
! [B_667] :
( ~ green(B_667,n6)
| ~ green(n4,B_667) ),
inference(resolution,[status(thm)],[c_25494,c_21]) ).
tff(c_25511,plain,
~ green(n4,n5),
inference(resolution,[status(thm)],[c_23181,c_25507]) ).
tff(c_25516,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_23723,c_25511]) ).
tff(c_25518,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_26441,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_26440,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_25990]) ).
tff(c_26452,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26441,c_26440]) ).
tff(c_26472,plain,
! [B_689] :
( green(B_689,n6)
| ~ less_than(B_689,n6)
| green(n3,B_689)
| ~ less_than(n3,B_689) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_26488,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_26472]) ).
tff(c_26503,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_25518,c_26488]) ).
tff(c_26512,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_26503]) ).
tff(c_26525,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_26512]) ).
tff(c_26531,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_26525]) ).
tff(c_26532,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_26503]) ).
tff(c_25913,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_25919,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_25913,c_21]) ).
tff(c_26589,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_26532,c_25919]) ).
tff(c_26597,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26439,c_26589]) ).
tff(c_26599,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_26601,plain,
! [B_691] :
( green(B_691,n6)
| ~ less_than(B_691,n6)
| green(n1,B_691)
| ~ less_than(n1,B_691) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_26617,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_26601]) ).
tff(c_26631,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_302,c_26617]) ).
tff(c_26633,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26599,c_25518,c_26631]) ).
tff(c_26635,plain,
~ green(n3,n4),
inference(splitRight,[status(thm)],[c_196]) ).
tff(c_26645,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_535]) ).
tff(c_26854,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_26871,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_26971,plain,
green(n1,n2),
inference(splitLeft,[status(thm)],[c_200]) ).
tff(c_26859,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_26854,c_293]) ).
tff(c_27440,plain,
! [B_714] :
( green(B_714,n4)
| ~ less_than(B_714,n4)
| green(n2,B_714)
| ~ less_than(n2,B_714) ),
inference(negUnitSimplification,[status(thm)],[c_26859,c_334]) ).
tff(c_27452,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_27440]) ).
tff(c_27462,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_27452]) ).
tff(c_27463,plain,
green(n2,n3),
inference(negUnitSimplification,[status(thm)],[c_26635,c_27462]) ).
tff(c_26702,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_237]) ).
tff(c_26708,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_26702]) ).
tff(c_26713,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_26708]) ).
tff(c_26715,plain,
less_than(n3,n5),
inference(splitRight,[status(thm)],[c_237]) ).
tff(c_26735,plain,
! [B_11] :
( green(n3,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n3,B_11)
| ~ less_than(n3,B_11) ),
inference(resolution,[status(thm)],[c_26715,c_109]) ).
tff(c_27682,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_26735]) ).
tff(c_27686,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_27682,c_293]) ).
tff(c_27693,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27463,c_27686]) ).
tff(c_27695,plain,
~ green(n3,n5),
inference(splitRight,[status(thm)],[c_26735]) ).
tff(c_27815,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_27825,plain,
! [B_723] :
( ~ green(B_723,n5)
| ~ green(n1,B_723) ),
inference(resolution,[status(thm)],[c_27815,c_21]) ).
tff(c_27829,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_26854,c_27825]) ).
tff(c_27836,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26645,c_27829]) ).
tff(c_27839,plain,
! [B_724] :
( green(B_724,n5)
| ~ less_than(B_724,n5)
| green(n1,B_724)
| ~ less_than(n1,B_724) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_27845,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_26715,c_27839]) ).
tff(c_27860,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_27695,c_27845]) ).
tff(c_27872,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_27860]) ).
tff(c_27875,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_27872]) ).
tff(c_27879,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_27875]) ).
tff(c_27880,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_27860]) ).
tff(c_28033,plain,
! [B_727] :
( ~ green(B_727,n3)
| ~ green(n1,B_727) ),
inference(resolution,[status(thm)],[c_27880,c_21]) ).
tff(c_28037,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_27463,c_28033]) ).
tff(c_28042,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26971,c_28037]) ).
tff(c_28044,plain,
~ green(n1,n2),
inference(splitRight,[status(thm)],[c_200]) ).
tff(c_28228,plain,
! [B_732] :
( green(B_732,n4)
| ~ less_than(B_732,n4)
| green(n2,B_732)
| ~ less_than(n2,B_732) ),
inference(negUnitSimplification,[status(thm)],[c_26859,c_334]) ).
tff(c_28240,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_28228]) ).
tff(c_28250,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_28240]) ).
tff(c_28251,plain,
green(n2,n3),
inference(negUnitSimplification,[status(thm)],[c_26635,c_28250]) ).
tff(c_29334,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_26735]) ).
tff(c_29338,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_29334,c_293]) ).
tff(c_29345,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28251,c_29338]) ).
tff(c_29347,plain,
~ green(n3,n5),
inference(splitRight,[status(thm)],[c_26735]) ).
tff(c_29622,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_29629,plain,
! [B_757] :
( ~ green(B_757,n6)
| ~ green(n1,B_757) ),
inference(resolution,[status(thm)],[c_29622,c_21]) ).
tff(c_29635,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_26871,c_29629]) ).
tff(c_29721,plain,
! [B_759] :
( green(B_759,n5)
| ~ less_than(B_759,n5)
| green(n1,B_759)
| ~ less_than(n1,B_759) ),
inference(negUnitSimplification,[status(thm)],[c_29635,c_316]) ).
tff(c_29727,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_26715,c_29721]) ).
tff(c_29742,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_29347,c_29727]) ).
tff(c_29754,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_29742]) ).
tff(c_29757,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_29754]) ).
tff(c_29761,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_29757]) ).
tff(c_29762,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_29742]) ).
tff(c_30172,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_29628,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_29622,c_21]) ).
tff(c_30174,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_30172,c_29628]) ).
tff(c_30182,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_29762,c_30174]) ).
tff(c_30185,plain,
! [B_765] :
( green(B_765,n6)
| ~ less_than(B_765,n6)
| green(n3,B_765)
| ~ less_than(n3,B_765) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_30846,plain,
! [A_774] :
( green(A_774,n6)
| green(n3,A_774)
| ~ less_than(n3,A_774)
| ~ less_than(A_774,n5) ),
inference(resolution,[status(thm)],[c_47,c_30185]) ).
tff(c_30894,plain,
( green(n4,n6)
| green(n3,n4)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_10,c_30846]) ).
tff(c_30949,plain,
( green(n4,n6)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_30894]) ).
tff(c_30950,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_26635,c_30949]) ).
tff(c_30952,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_30950,c_29628]) ).
tff(c_30960,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26645,c_30952]) ).
tff(c_31303,plain,
! [B_782] :
( green(B_782,n6)
| ~ less_than(B_782,n6)
| green(n1,B_782)
| ~ less_than(n1,B_782) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_31311,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_333,c_31303]) ).
tff(c_31325,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_31311]) ).
tff(c_31326,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_28044,c_31325]) ).
tff(c_31470,plain,
! [B_785] :
( ~ green(B_785,n6)
| ~ green(n2,B_785) ),
inference(resolution,[status(thm)],[c_31326,c_21]) ).
tff(c_31474,plain,
~ green(n2,n5),
inference(resolution,[status(thm)],[c_26871,c_31470]) ).
tff(c_31479,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_31474]) ).
tff(c_31481,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_32043,plain,
! [B_799] :
( green(B_799,n4)
| ~ less_than(B_799,n4)
| green(n2,B_799)
| ~ less_than(n2,B_799) ),
inference(negUnitSimplification,[status(thm)],[c_26859,c_334]) ).
tff(c_32055,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_32043]) ).
tff(c_32065,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_32055]) ).
tff(c_32066,plain,
green(n2,n3),
inference(negUnitSimplification,[status(thm)],[c_26635,c_32065]) ).
tff(c_33033,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_26735]) ).
tff(c_33037,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_33033,c_293]) ).
tff(c_33044,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_32066,c_33037]) ).
tff(c_33046,plain,
~ green(n3,n5),
inference(splitRight,[status(thm)],[c_26735]) ).
tff(c_33077,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_33087,plain,
! [B_818] :
( ~ green(B_818,n5)
| ~ green(n1,B_818) ),
inference(resolution,[status(thm)],[c_33077,c_21]) ).
tff(c_33091,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_26854,c_33087]) ).
tff(c_33098,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26645,c_33091]) ).
tff(c_33101,plain,
! [B_819] :
( green(B_819,n5)
| ~ less_than(B_819,n5)
| green(n1,B_819)
| ~ less_than(n1,B_819) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_33107,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_26715,c_33101]) ).
tff(c_33122,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_33046,c_33107]) ).
tff(c_33134,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_33122]) ).
tff(c_33137,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_33134]) ).
tff(c_33141,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_33137]) ).
tff(c_33142,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_33122]) ).
tff(c_33144,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_32932,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_32935,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_32932,c_21]) ).
tff(c_33149,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_33144,c_32935]) ).
tff(c_33218,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33142,c_33149]) ).
tff(c_33221,plain,
! [B_820] :
( green(B_820,n6)
| ~ less_than(B_820,n6)
| green(n3,B_820)
| ~ less_than(n3,B_820) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_33237,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_33221]) ).
tff(c_33249,plain,
( green(n5,n6)
| green(n3,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_26715,c_33237]) ).
tff(c_33251,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33046,c_31481,c_33249]) ).
tff(c_33254,plain,
! [B_821] :
( green(B_821,n6)
| ~ less_than(B_821,n6)
| green(n1,B_821)
| ~ less_than(n1,B_821) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_33270,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_33254]) ).
tff(c_33284,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_302,c_33270]) ).
tff(c_33285,plain,
green(n1,n5),
inference(negUnitSimplification,[status(thm)],[c_31481,c_33284]) ).
tff(c_33340,plain,
! [B_823] :
( ~ green(B_823,n5)
| ~ green(n1,B_823) ),
inference(resolution,[status(thm)],[c_33285,c_21]) ).
tff(c_33344,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_26854,c_33340]) ).
tff(c_33351,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26645,c_33344]) ).
tff(c_33353,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_33355,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_33365,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_26735]) ).
tff(c_33367,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_33365,c_293]) ).
tff(c_33373,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33355,c_33367]) ).
tff(c_34204,plain,
! [B_845] :
( green(B_845,n5)
| ~ less_than(B_845,n5)
| green(n3,B_845)
| ~ less_than(n3,B_845) ),
inference(splitRight,[status(thm)],[c_26735]) ).
tff(c_34220,plain,
( green(n4,n5)
| green(n3,n4)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_8,c_34204]) ).
tff(c_34233,plain,
( green(n4,n5)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_34220]) ).
tff(c_34235,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26635,c_33353,c_34233]) ).
tff(c_34237,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_41766,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_334]) ).
tff(c_42336,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_40367,plain,
green(n1,n2),
inference(splitLeft,[status(thm)],[c_200]) ).
tff(c_41073,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_334]) ).
tff(c_26656,plain,
! [B_5] :
( ~ green(B_5,n4)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_26645,c_21]) ).
tff(c_41075,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_41073,c_26656]) ).
tff(c_41081,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40367,c_41075]) ).
tff(c_41634,plain,
! [B_1020] :
( green(B_1020,n4)
| ~ less_than(B_1020,n4)
| green(n2,B_1020)
| ~ less_than(n2,B_1020) ),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_41646,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_41634]) ).
tff(c_41656,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_41646]) ).
tff(c_41658,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34237,c_26635,c_41656]) ).
tff(c_41660,plain,
~ green(n1,n2),
inference(splitRight,[status(thm)],[c_200]) ).
tff(c_35313,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_26735]) ).
tff(c_35696,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_37091,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_37129,plain,
! [B_909] :
( ~ green(B_909,n6)
| ~ green(n3,B_909) ),
inference(resolution,[status(thm)],[c_37091,c_21]) ).
tff(c_37133,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_35696,c_37129]) ).
tff(c_37140,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_35313,c_37133]) ).
tff(c_37167,plain,
! [B_911] :
( green(B_911,n6)
| ~ less_than(B_911,n6)
| green(n3,B_911)
| ~ less_than(n3,B_911) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_37197,plain,
! [A_912] :
( green(A_912,n6)
| green(n3,A_912)
| ~ less_than(n3,A_912)
| ~ less_than(A_912,n5) ),
inference(resolution,[status(thm)],[c_47,c_37167]) ).
tff(c_37242,plain,
( green(n4,n6)
| green(n3,n4)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_10,c_37197]) ).
tff(c_37289,plain,
( green(n4,n6)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_37242]) ).
tff(c_37290,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_26635,c_37289]) ).
tff(c_34238,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_34241,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_34238,c_21]) ).
tff(c_37294,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_37290,c_34241]) ).
tff(c_37301,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26645,c_37294]) ).
tff(c_37303,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_39200,plain,
! [A_963,B_964] :
( green(A_963,n6)
| green(B_964,n6)
| ~ less_than(B_964,n6)
| green(A_963,B_964)
| ~ less_than(A_963,B_964)
| ~ less_than(A_963,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_39216,plain,
! [A_963] :
( green(A_963,n6)
| green(n5,n6)
| green(A_963,n5)
| ~ less_than(A_963,n5) ),
inference(resolution,[status(thm)],[c_6,c_39200]) ).
tff(c_39231,plain,
! [A_965] :
( green(A_965,n6)
| green(A_965,n5)
| ~ less_than(A_965,n5) ),
inference(negUnitSimplification,[status(thm)],[c_37303,c_39216]) ).
tff(c_39255,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_39231]) ).
tff(c_39270,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_33353,c_39255]) ).
tff(c_39274,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_39270,c_34241]) ).
tff(c_39281,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26645,c_39274]) ).
tff(c_40331,plain,
! [B_989] :
( green(B_989,n5)
| ~ less_than(B_989,n5)
| green(n3,B_989)
| ~ less_than(n3,B_989) ),
inference(splitRight,[status(thm)],[c_26735]) ).
tff(c_40347,plain,
( green(n4,n5)
| green(n3,n4)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_8,c_40331]) ).
tff(c_40360,plain,
( green(n4,n5)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_40347]) ).
tff(c_40362,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26635,c_33353,c_40360]) ).
tff(c_42496,plain,
! [B_1043] :
( green(B_1043,n6)
| ~ less_than(B_1043,n6)
| green(n1,B_1043)
| ~ less_than(n1,B_1043) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_42504,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_333,c_42496]) ).
tff(c_42518,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_42504]) ).
tff(c_42519,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_41660,c_42518]) ).
tff(c_42536,plain,
! [B_1044] :
( ~ green(B_1044,n6)
| ~ green(n2,B_1044) ),
inference(resolution,[status(thm)],[c_42519,c_21]) ).
tff(c_42540,plain,
~ green(n2,n5),
inference(resolution,[status(thm)],[c_42336,c_42536]) ).
tff(c_42545,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_290,c_42540]) ).
tff(c_42547,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_44039,plain,
! [A_1074,B_1075] :
( green(A_1074,n6)
| green(B_1075,n6)
| ~ less_than(B_1075,n6)
| green(A_1074,B_1075)
| ~ less_than(A_1074,B_1075)
| ~ less_than(A_1074,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_44055,plain,
! [A_1074] :
( green(A_1074,n6)
| green(n5,n6)
| green(A_1074,n5)
| ~ less_than(A_1074,n5) ),
inference(resolution,[status(thm)],[c_6,c_44039]) ).
tff(c_44070,plain,
! [A_1076] :
( green(A_1076,n6)
| green(A_1076,n5)
| ~ less_than(A_1076,n5) ),
inference(negUnitSimplification,[status(thm)],[c_42547,c_44055]) ).
tff(c_44094,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_44070]) ).
tff(c_44108,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_33353,c_44094]) ).
tff(c_42668,plain,
! [B_1048] :
( green(B_1048,n6)
| ~ less_than(B_1048,n6)
| green(n1,B_1048)
| ~ less_than(n1,B_1048) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_42676,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_333,c_42668]) ).
tff(c_42690,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_42676]) ).
tff(c_42691,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_41660,c_42690]) ).
tff(c_42703,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_42691,c_21]) ).
tff(c_44112,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_44108,c_42703]) ).
tff(c_44119,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_41766,c_44112]) ).
tff(c_44666,plain,
! [B_1091] :
( green(B_1091,n4)
| ~ less_than(B_1091,n4)
| green(n2,B_1091)
| ~ less_than(n2,B_1091) ),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_44678,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_44666]) ).
tff(c_44689,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_44678]) ).
tff(c_44691,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34237,c_26635,c_44689]) ).
tff(c_44693,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_44724,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_316]) ).
tff(c_44814,plain,
! [B_1095] :
( ~ green(B_1095,n5)
| ~ green(n1,B_1095) ),
inference(resolution,[status(thm)],[c_44724,c_21]) ).
tff(c_44820,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_290,c_44814]) ).
tff(c_46697,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_334]) ).
tff(c_44754,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_237]) ).
tff(c_44760,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_44754]) ).
tff(c_44765,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_44760]) ).
tff(c_44767,plain,
less_than(n3,n5),
inference(splitRight,[status(thm)],[c_237]) ).
tff(c_44787,plain,
! [B_11] :
( green(n3,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n3,B_11)
| ~ less_than(n3,B_11) ),
inference(resolution,[status(thm)],[c_44767,c_109]) ).
tff(c_44884,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_44787]) ).
tff(c_44730,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_44724,c_21]) ).
tff(c_44891,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_44884,c_44730]) ).
tff(c_45800,plain,
! [B_1119] :
( green(B_1119,n4)
| ~ less_than(B_1119,n4)
| green(n1,B_1119)
| ~ less_than(n1,B_1119) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_45812,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_45800]) ).
tff(c_45824,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_44891,c_26635,c_45812]) ).
tff(c_45839,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_45824]) ).
tff(c_45843,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_45839]) ).
tff(c_47052,plain,
! [B_1151] :
( green(B_1151,n5)
| ~ less_than(B_1151,n5)
| green(n3,B_1151)
| ~ less_than(n3,B_1151) ),
inference(splitRight,[status(thm)],[c_44787]) ).
tff(c_47068,plain,
( green(n4,n5)
| green(n3,n4)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_8,c_47052]) ).
tff(c_47081,plain,
( green(n4,n5)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_47068]) ).
tff(c_47082,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_26635,c_47081]) ).
tff(c_47086,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_47082,c_293]) ).
tff(c_47093,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_46697,c_47086]) ).
tff(c_47095,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_47096,plain,
! [B_1152] :
( green(B_1152,n4)
| ~ less_than(B_1152,n4)
| green(n1,B_1152)
| ~ less_than(n1,B_1152) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_47104,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_303,c_47096]) ).
tff(c_47116,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_47104]) ).
tff(c_47118,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44820,c_47095,c_47116]) ).
tff(c_47974,plain,
! [B_1176] :
( green(B_1176,n5)
| ~ less_than(B_1176,n5)
| green(n1,B_1176)
| ~ less_than(n1,B_1176) ),
inference(splitRight,[status(thm)],[c_316]) ).
tff(c_47990,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_47974]) ).
tff(c_48004,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_513,c_47990]) ).
tff(c_48005,plain,
green(n4,n5),
inference(negUnitSimplification,[status(thm)],[c_44693,c_48004]) ).
tff(c_48007,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_48005,c_293]) ).
tff(c_48013,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_47121,c_48007]) ).
tff(c_48015,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_49122,plain,
! [B_1205] :
( green(B_1205,n4)
| ~ less_than(B_1205,n4)
| green(n1,B_1205)
| ~ less_than(n1,B_1205) ),
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_49130,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_303,c_49122]) ).
tff(c_49142,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_49130]) ).
tff(c_49143,plain,
green(n1,n2),
inference(negUnitSimplification,[status(thm)],[c_48015,c_49142]) ).
tff(c_48210,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_49134,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_49122]) ).
tff(c_49147,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_26635,c_49134]) ).
tff(c_49173,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_49147]) ).
tff(c_49176,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_49173]) ).
tff(c_49180,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_49176]) ).
tff(c_49181,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_49147]) ).
tff(c_49359,plain,
! [B_1210] :
( ~ green(B_1210,n3)
| ~ green(n1,B_1210) ),
inference(resolution,[status(thm)],[c_49181,c_21]) ).
tff(c_49363,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_48210,c_49359]) ).
tff(c_49368,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49143,c_49363]) ).
tff(c_49370,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_50660,plain,
! [B_1238] :
( green(B_1238,n4)
| ~ less_than(B_1238,n4)
| green(n2,B_1238)
| ~ less_than(n2,B_1238) ),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_50672,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_50660]) ).
tff(c_50682,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_50672]) ).
tff(c_50684,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_49370,c_26635,c_50682]) ).
tff(c_50686,plain,
~ green(n2,n5),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_50756,plain,
less_than(n2,n4),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_50876,plain,
! [B_11] :
( green(n2,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_50756,c_109]) ).
tff(c_51191,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_50876]) ).
tff(c_56483,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_56506,plain,
! [B_1358] :
( ~ green(B_1358,n4)
| ~ green(n1,B_1358) ),
inference(resolution,[status(thm)],[c_56483,c_21]) ).
tff(c_56510,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_51191,c_56506]) ).
tff(c_56515,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_56510]) ).
tff(c_56517,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_52827,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_52774,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_51202,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_51576,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_51583,plain,
! [B_1263] :
( ~ green(B_1263,n4)
| ~ green(n1,B_1263) ),
inference(resolution,[status(thm)],[c_51576,c_21]) ).
tff(c_51587,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_51191,c_51583]) ).
tff(c_51592,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_51587]) ).
tff(c_52119,plain,
! [B_1275] :
( green(B_1275,n4)
| ~ less_than(B_1275,n4)
| green(n1,B_1275)
| ~ less_than(n1,B_1275) ),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_52141,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_52119]) ).
tff(c_52142,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_52141]) ).
tff(c_52175,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_52142]) ).
tff(c_52179,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_52175]) ).
tff(c_52180,plain,
( green(n1,n3)
| green(n3,n4) ),
inference(splitRight,[status(thm)],[c_52141]) ).
tff(c_52242,plain,
green(n3,n4),
inference(splitLeft,[status(thm)],[c_52180]) ).
tff(c_51194,plain,
! [B_5] :
( ~ green(B_5,n4)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_51191,c_21]) ).
tff(c_52248,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_52242,c_51194]) ).
tff(c_52254,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_51202,c_52248]) ).
tff(c_52255,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_52180]) ).
tff(c_52302,plain,
! [B_1278] :
( ~ green(B_1278,n3)
| ~ green(n1,B_1278) ),
inference(resolution,[status(thm)],[c_52255,c_21]) ).
tff(c_52306,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_51202,c_52302]) ).
tff(c_52311,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_52306]) ).
tff(c_52313,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_51073,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_237]) ).
tff(c_51079,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_51073]) ).
tff(c_51084,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_51079]) ).
tff(c_51086,plain,
less_than(n3,n5),
inference(splitRight,[status(thm)],[c_237]) ).
tff(c_52788,plain,
! [B_1290] :
( green(B_1290,n5)
| ~ less_than(B_1290,n5)
| green(n2,B_1290)
| ~ less_than(n2,B_1290) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_52794,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_51086,c_52788]) ).
tff(c_52809,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_52794]) ).
tff(c_52810,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_52313,c_52809]) ).
tff(c_52822,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_52810,c_21]) ).
tff(c_52832,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_52827,c_52822]) ).
tff(c_53128,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_53138,plain,
! [B_1300] :
( ~ green(B_1300,n6)
| ~ green(n3,B_1300) ),
inference(resolution,[status(thm)],[c_53128,c_21]) ).
tff(c_53142,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_52774,c_53138]) ).
tff(c_53149,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52810,c_53142]) ).
tff(c_53152,plain,
! [B_1301] :
( green(B_1301,n6)
| ~ less_than(B_1301,n6)
| green(n3,B_1301)
| ~ less_than(n3,B_1301) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_55323,plain,
! [A_1337] :
( green(A_1337,n6)
| green(n3,A_1337)
| ~ less_than(n3,A_1337)
| ~ less_than(A_1337,n5) ),
inference(resolution,[status(thm)],[c_47,c_53152]) ).
tff(c_55371,plain,
( green(n4,n6)
| green(n3,n4)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_10,c_55323]) ).
tff(c_55422,plain,
( green(n4,n6)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_55371]) ).
tff(c_55423,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_52832,c_55422]) ).
tff(c_55464,plain,
! [B_1340] :
( ~ green(B_1340,n6)
| ~ green(n4,B_1340) ),
inference(resolution,[status(thm)],[c_55423,c_21]) ).
tff(c_55468,plain,
~ green(n4,n5),
inference(resolution,[status(thm)],[c_52774,c_55464]) ).
tff(c_55475,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52827,c_55468]) ).
tff(c_55477,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_50974,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_50977,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_50974,c_21]) ).
tff(c_52779,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_52774,c_50977]) ).
tff(c_56573,plain,
! [B_1361] :
( green(B_1361,n5)
| ~ less_than(B_1361,n5)
| green(n1,B_1361)
| ~ less_than(n1,B_1361) ),
inference(negUnitSimplification,[status(thm)],[c_52779,c_50824]) ).
tff(c_56589,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_56573]) ).
tff(c_56604,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50804,c_56589]) ).
tff(c_56606,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56517,c_55477,c_56604]) ).
tff(c_56608,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_50860,plain,
( less_than(n2,n6)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_50756,c_64]) ).
tff(c_50875,plain,
less_than(n2,n6),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_50860]) ).
tff(c_50910,plain,
! [B_11] :
( green(n2,n6)
| green(B_11,n6)
| ~ less_than(B_11,n6)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_50875,c_109]) ).
tff(c_61072,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_50910]) ).
tff(c_61076,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_61072,c_50977]) ).
tff(c_61083,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_61076]) ).
tff(c_61176,plain,
! [B_1445] :
( green(B_1445,n6)
| ~ less_than(B_1445,n6)
| green(n2,B_1445)
| ~ less_than(n2,B_1445) ),
inference(splitRight,[status(thm)],[c_50910]) ).
tff(c_61192,plain,
( green(n5,n6)
| green(n2,n5)
| ~ less_than(n2,n5) ),
inference(resolution,[status(thm)],[c_6,c_61176]) ).
tff(c_61207,plain,
( green(n5,n6)
| green(n2,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_149,c_61192]) ).
tff(c_61209,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50686,c_56608,c_61207]) ).
tff(c_61211,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_50876]) ).
tff(c_61213,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_61697,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_61314,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_61319,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_61314,c_50977]) ).
tff(c_62233,plain,
! [B_1471] :
( green(B_1471,n5)
| ~ less_than(B_1471,n5)
| green(n1,B_1471)
| ~ less_than(n1,B_1471) ),
inference(negUnitSimplification,[status(thm)],[c_61319,c_50824]) ).
tff(c_62252,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_51086,c_62233]) ).
tff(c_62265,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_62252]) ).
tff(c_62360,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_62265]) ).
tff(c_62364,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_62360]) ).
tff(c_62365,plain,
( green(n1,n3)
| green(n3,n5) ),
inference(splitRight,[status(thm)],[c_62252]) ).
tff(c_62427,plain,
green(n3,n5),
inference(splitLeft,[status(thm)],[c_62365]) ).
tff(c_63923,plain,
! [B_1492] :
( ~ green(B_1492,n5)
| ~ green(n3,B_1492) ),
inference(resolution,[status(thm)],[c_62427,c_21]) ).
tff(c_63929,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_61697,c_63923]) ).
tff(c_62366,plain,
less_than(n1,n3),
inference(splitRight,[status(thm)],[c_62252]) ).
tff(c_62434,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_62513,plain,
! [B_1475] :
( ~ green(B_1475,n5)
| ~ green(n3,B_1475) ),
inference(resolution,[status(thm)],[c_62427,c_21]) ).
tff(c_62519,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_61697,c_62513]) ).
tff(c_62128,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_62138,plain,
! [B_1468] :
( ~ green(B_1468,n6)
| ~ green(n3,B_1468) ),
inference(resolution,[status(thm)],[c_62128,c_21]) ).
tff(c_62146,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_61314,c_62138]) ).
tff(c_62136,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_62128,c_50977]) ).
tff(c_62149,plain,
! [B_1469] :
( green(B_1469,n5)
| ~ less_than(B_1469,n5)
| green(n1,B_1469)
| ~ less_than(n1,B_1469) ),
inference(negUnitSimplification,[status(thm)],[c_61319,c_50824]) ).
tff(c_62155,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_51086,c_62149]) ).
tff(c_62170,plain,
( green(n3,n5)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_62136,c_62155]) ).
tff(c_62183,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_62146,c_62170]) ).
tff(c_62186,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_62183]) ).
tff(c_62190,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_62186]) ).
tff(c_62193,plain,
! [B_1470] :
( green(B_1470,n6)
| ~ less_than(B_1470,n6)
| green(n3,B_1470)
| ~ less_than(n3,B_1470) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_63810,plain,
! [A_1491] :
( green(A_1491,n6)
| green(n3,A_1491)
| ~ less_than(n3,A_1491)
| ~ less_than(A_1491,n5) ),
inference(resolution,[status(thm)],[c_47,c_62193]) ).
tff(c_63858,plain,
( green(n4,n6)
| green(n3,n4)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_10,c_63810]) ).
tff(c_63908,plain,
( green(n4,n6)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_63858]) ).
tff(c_63909,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_62519,c_63908]) ).
tff(c_63913,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_63909,c_50977]) ).
tff(c_63920,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_62434,c_63913]) ).
tff(c_64100,plain,
! [B_1496] :
( green(B_1496,n4)
| ~ less_than(B_1496,n4)
| green(n1,B_1496)
| ~ less_than(n1,B_1496) ),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_64112,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_64100]) ).
tff(c_64124,plain,
( green(n3,n4)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_62366,c_64112]) ).
tff(c_64125,plain,
green(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_63929,c_64124]) ).
tff(c_64132,plain,
! [B_1497] :
( ~ green(B_1497,n3)
| ~ green(n1,B_1497) ),
inference(resolution,[status(thm)],[c_64125,c_21]) ).
tff(c_64136,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_61213,c_64132]) ).
tff(c_64141,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_64136]) ).
tff(c_64142,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_62365]) ).
tff(c_64327,plain,
! [B_1500] :
( ~ green(B_1500,n3)
| ~ green(n1,B_1500) ),
inference(resolution,[status(thm)],[c_64142,c_21]) ).
tff(c_64331,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_61213,c_64327]) ).
tff(c_64336,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_64331]) ).
tff(c_64338,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_64638,plain,
! [B_1508] :
( green(B_1508,n5)
| ~ less_than(B_1508,n5)
| green(n2,B_1508)
| ~ less_than(n2,B_1508) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_64654,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_64638]) ).
tff(c_64668,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50756,c_64654]) ).
tff(c_64670,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61211,c_64338,c_64668]) ).
tff(c_64672,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_68102,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_50910]) ).
tff(c_68106,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_68102,c_50977]) ).
tff(c_68113,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_68106]) ).
tff(c_68116,plain,
! [B_1575] :
( green(B_1575,n6)
| ~ less_than(B_1575,n6)
| green(n2,B_1575)
| ~ less_than(n2,B_1575) ),
inference(splitRight,[status(thm)],[c_50910]) ).
tff(c_68132,plain,
( green(n5,n6)
| green(n2,n5)
| ~ less_than(n2,n5) ),
inference(resolution,[status(thm)],[c_6,c_68116]) ).
tff(c_68146,plain,
( green(n5,n6)
| green(n2,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_149,c_68132]) ).
tff(c_68148,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50686,c_64672,c_68146]) ).
tff(c_68150,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_68533,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_68730,plain,
! [B_1590] :
( green(B_1590,n5)
| ~ less_than(B_1590,n5)
| green(n2,B_1590)
| ~ less_than(n2,B_1590) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_68736,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_51086,c_68730]) ).
tff(c_68751,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_68736]) ).
tff(c_68752,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_68150,c_68751]) ).
tff(c_68769,plain,
! [B_1591] :
( ~ green(B_1591,n5)
| ~ green(n3,B_1591) ),
inference(resolution,[status(thm)],[c_68752,c_21]) ).
tff(c_68775,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_68533,c_68769]) ).
tff(c_68968,plain,
! [B_1597] :
( green(B_1597,n4)
| ~ less_than(B_1597,n4)
| green(n2,B_1597)
| ~ less_than(n2,B_1597) ),
inference(splitRight,[status(thm)],[c_50876]) ).
tff(c_68980,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_68968]) ).
tff(c_68989,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_68980]) ).
tff(c_68991,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68150,c_68775,c_68989]) ).
tff(c_68993,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_69409,plain,
! [B_1608] :
( green(B_1608,n5)
| ~ less_than(B_1608,n5)
| green(n2,B_1608)
| ~ less_than(n2,B_1608) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_69425,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_69409]) ).
tff(c_69440,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50756,c_69425]) ).
tff(c_69442,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61211,c_68993,c_69440]) ).
tff(c_70736,plain,
! [B_1643] :
( green(B_1643,n6)
| ~ less_than(B_1643,n6)
| green(n1,B_1643)
| ~ less_than(n1,B_1643) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_70752,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_70736]) ).
tff(c_70767,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_50755,c_70752]) ).
tff(c_70769,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_70696,c_69698,c_70767]) ).
tff(c_70771,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_70864,plain,
! [B_1646] :
( green(B_1646,n5)
| ~ less_than(B_1646,n5)
| green(n2,B_1646)
| ~ less_than(n2,B_1646) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_70880,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_70864]) ).
tff(c_70893,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50756,c_70880]) ).
tff(c_70894,plain,
green(n2,n4),
inference(negUnitSimplification,[status(thm)],[c_70771,c_70893]) ).
tff(c_71516,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_71523,plain,
! [B_1662] :
( ~ green(B_1662,n4)
| ~ green(n1,B_1662) ),
inference(resolution,[status(thm)],[c_71516,c_21]) ).
tff(c_71527,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_70894,c_71523]) ).
tff(c_71532,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_71527]) ).
tff(c_71563,plain,
! [B_1664] :
( green(B_1664,n4)
| ~ less_than(B_1664,n4)
| green(n1,B_1664)
| ~ less_than(n1,B_1664) ),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_71575,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_71563]) ).
tff(c_71586,plain,
( green(n3,n4)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_70915,c_71575]) ).
tff(c_71587,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_71586]) ).
tff(c_71590,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_71587]) ).
tff(c_71594,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_71590]) ).
tff(c_71595,plain,
green(n3,n4),
inference(splitRight,[status(thm)],[c_71586]) ).
tff(c_71534,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_50881,plain,
! [A_7] :
( less_than(A_7,n4)
| ~ less_than(A_7,n2) ),
inference(resolution,[status(thm)],[c_50756,c_16]) ).
tff(c_71008,plain,
! [B_1651] :
( green(B_1651,n6)
| ~ less_than(B_1651,n6)
| green(n1,B_1651)
| ~ less_than(n1,B_1651) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_72639,plain,
! [A_1679] :
( green(A_1679,n6)
| green(n1,A_1679)
| ~ less_than(n1,A_1679)
| ~ less_than(A_1679,n5) ),
inference(resolution,[status(thm)],[c_47,c_71008]) ).
tff(c_72656,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_50881,c_72639]) ).
tff(c_72713,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_72656]) ).
tff(c_72714,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_71534,c_72713]) ).
tff(c_72762,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_72714,c_69471]) ).
tff(c_72768,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_71595,c_72762]) ).
tff(c_72770,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_50824]) ).
tff(c_73083,plain,
! [B_1688] :
( green(B_1688,n6)
| ~ less_than(B_1688,n6)
| green(n1,B_1688)
| ~ less_than(n1,B_1688) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_73099,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_73083]) ).
tff(c_73114,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_50755,c_73099]) ).
tff(c_73116,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72770,c_69698,c_73114]) ).
tff(c_73118,plain,
~ green(n3,n5),
inference(splitRight,[status(thm)],[c_69623]) ).
tff(c_77060,plain,
! [B_1776] :
( green(B_1776,n5)
| ~ less_than(B_1776,n5)
| green(n2,B_1776)
| ~ less_than(n2,B_1776) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_77064,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_69602,c_77060]) ).
tff(c_77080,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_77064]) ).
tff(c_77081,plain,
green(n2,n3),
inference(negUnitSimplification,[status(thm)],[c_73118,c_77080]) ).
tff(c_75829,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_73148,plain,
green(n3,n4),
inference(splitLeft,[status(thm)],[c_196]) ).
tff(c_75220,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_75227,plain,
! [B_1733] :
( ~ green(B_1733,n4)
| ~ green(n1,B_1733) ),
inference(resolution,[status(thm)],[c_75220,c_21]) ).
tff(c_75233,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_73148,c_75227]) ).
tff(c_73975,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_73156,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_73942,plain,
! [B_1710] :
( green(B_1710,n6)
| ~ less_than(B_1710,n6)
| green(n1,B_1710)
| ~ less_than(n1,B_1710) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_73958,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_73942]) ).
tff(c_73973,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_50755,c_73958]) ).
tff(c_73974,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_73973]) ).
tff(c_74026,plain,
! [B_1713] :
( ~ green(B_1713,n5)
| ~ green(n1,B_1713) ),
inference(resolution,[status(thm)],[c_73974,c_21]) ).
tff(c_74030,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_73156,c_74026]) ).
tff(c_74035,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_73975,c_74030]) ).
tff(c_74037,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_74706,plain,
! [A_1726] :
( green(A_1726,n6)
| green(n1,A_1726)
| ~ less_than(n1,A_1726)
| ~ less_than(A_1726,n5) ),
inference(resolution,[status(thm)],[c_47,c_73942]) ).
tff(c_74718,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_50881,c_74706]) ).
tff(c_74764,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_74718]) ).
tff(c_74765,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_74037,c_74764]) ).
tff(c_74810,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_74765,c_69471]) ).
tff(c_74817,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_73148,c_74810]) ).
tff(c_74819,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_73973]) ).
tff(c_75368,plain,
! [B_1735] :
( green(B_1735,n5)
| ~ less_than(B_1735,n5)
| green(n1,B_1735)
| ~ less_than(n1,B_1735) ),
inference(negUnitSimplification,[status(thm)],[c_74819,c_50824]) ).
tff(c_75372,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_69602,c_75368]) ).
tff(c_75388,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_75233,c_73118,c_75372]) ).
tff(c_75403,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_75388]) ).
tff(c_75407,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_75403]) ).
tff(c_75409,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_75433,plain,
! [A_1737] :
( green(A_1737,n6)
| green(n1,A_1737)
| ~ less_than(n1,A_1737)
| ~ less_than(A_1737,n5) ),
inference(resolution,[status(thm)],[c_47,c_73942]) ).
tff(c_75445,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_50881,c_75433]) ).
tff(c_75493,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_75445]) ).
tff(c_75494,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_75409,c_75493]) ).
tff(c_75542,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_75494,c_69471]) ).
tff(c_75549,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_73148,c_75542]) ).
tff(c_75551,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_76020,plain,
! [B_1749] :
( green(B_1749,n5)
| ~ less_than(B_1749,n5)
| green(n2,B_1749)
| ~ less_than(n2,B_1749) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_76036,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_76020]) ).
tff(c_76050,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50756,c_76036]) ).
tff(c_76051,plain,
green(n2,n4),
inference(negUnitSimplification,[status(thm)],[c_75551,c_76050]) ).
tff(c_76058,plain,
! [B_1750] :
( ~ green(B_1750,n4)
| ~ green(n2,B_1750) ),
inference(resolution,[status(thm)],[c_76051,c_21]) ).
tff(c_76062,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_73148,c_76058]) ).
tff(c_76067,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75829,c_76062]) ).
tff(c_76069,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_76261,plain,
! [B_1756] :
( green(B_1756,n5)
| ~ less_than(B_1756,n5)
| green(n2,B_1756)
| ~ less_than(n2,B_1756) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_76265,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_69602,c_76261]) ).
tff(c_76281,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_76265]) ).
tff(c_76283,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_76069,c_73118,c_76281]) ).
tff(c_76285,plain,
~ green(n3,n4),
inference(splitRight,[status(thm)],[c_196]) ).
tff(c_76286,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_50876]) ).
tff(c_76386,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_76393,plain,
! [B_1760] :
( ~ green(B_1760,n4)
| ~ green(n1,B_1760) ),
inference(resolution,[status(thm)],[c_76386,c_21]) ).
tff(c_76397,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_76286,c_76393]) ).
tff(c_76402,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_76397]) ).
tff(c_77166,plain,
! [B_1781] :
( green(B_1781,n4)
| ~ less_than(B_1781,n4)
| green(n1,B_1781)
| ~ less_than(n1,B_1781) ),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_77178,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_77166]) ).
tff(c_77189,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_76285,c_77178]) ).
tff(c_77190,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_77189]) ).
tff(c_77193,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_77190]) ).
tff(c_77197,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_77193]) ).
tff(c_77198,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_77189]) ).
tff(c_77333,plain,
! [B_1783] :
( ~ green(B_1783,n3)
| ~ green(n1,B_1783) ),
inference(resolution,[status(thm)],[c_77198,c_21]) ).
tff(c_77337,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_77081,c_77333]) ).
tff(c_77342,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_77337]) ).
tff(c_77344,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_50876]) ).
tff(c_77345,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_77813,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_78164,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_50824]) ).
tff(c_78172,plain,
! [B_1804] :
( ~ green(B_1804,n5)
| ~ green(n1,B_1804) ),
inference(resolution,[status(thm)],[c_78164,c_21]) ).
tff(c_78178,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_77813,c_78172]) ).
tff(c_78457,plain,
! [B_1811] :
( green(B_1811,n4)
| ~ less_than(B_1811,n4)
| green(n1,B_1811)
| ~ less_than(n1,B_1811) ),
inference(negUnitSimplification,[status(thm)],[c_78178,c_50850]) ).
tff(c_78469,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_78457]) ).
tff(c_78481,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_76285,c_78469]) ).
tff(c_78482,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_78481]) ).
tff(c_78485,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_78482]) ).
tff(c_78489,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_78485]) ).
tff(c_78490,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_78481]) ).
tff(c_78745,plain,
! [B_1814] :
( ~ green(B_1814,n3)
| ~ green(n1,B_1814) ),
inference(resolution,[status(thm)],[c_78490,c_21]) ).
tff(c_78749,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_77345,c_78745]) ).
tff(c_78754,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_78749]) ).
tff(c_78846,plain,
! [B_1819] :
( green(B_1819,n5)
| ~ less_than(B_1819,n5)
| green(n1,B_1819)
| ~ less_than(n1,B_1819) ),
inference(splitRight,[status(thm)],[c_50824]) ).
tff(c_78850,plain,
( green(n3,n5)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_69602,c_78846]) ).
tff(c_78866,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_73118,c_78850]) ).
tff(c_78879,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_78866]) ).
tff(c_78882,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_78879]) ).
tff(c_78886,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_78882]) ).
tff(c_78887,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_78866]) ).
tff(c_78956,plain,
! [B_1820] :
( ~ green(B_1820,n3)
| ~ green(n1,B_1820) ),
inference(resolution,[status(thm)],[c_78887,c_21]) ).
tff(c_78960,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_77345,c_78956]) ).
tff(c_78965,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_78960]) ).
tff(c_78967,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_79247,plain,
! [B_1827] :
( green(B_1827,n5)
| ~ less_than(B_1827,n5)
| green(n2,B_1827)
| ~ less_than(n2,B_1827) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_79263,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_79247]) ).
tff(c_79277,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50756,c_79263]) ).
tff(c_79279,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_77344,c_78967,c_79277]) ).
tff(c_79281,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_80037,plain,
! [B_1846] :
( green(B_1846,n5)
| ~ less_than(B_1846,n5)
| green(n2,B_1846)
| ~ less_than(n2,B_1846) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_80041,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_69602,c_80037]) ).
tff(c_80057,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_80041]) ).
tff(c_80059,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_79281,c_73118,c_80057]) ).
tff(c_80061,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_80862,plain,
! [B_1870] :
( green(B_1870,n6)
| ~ less_than(B_1870,n6)
| green(n1,B_1870)
| ~ less_than(n1,B_1870) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_80874,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_80862]) ).
tff(c_80890,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_80061,c_80874]) ).
tff(c_80895,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_80890]) ).
tff(c_80902,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_80895]) ).
tff(c_80906,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_80902]) ).
tff(c_80907,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_80890]) ).
tff(c_81028,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_81039,plain,
! [B_1873] :
( ~ green(B_1873,n3)
| ~ green(n1,B_1873) ),
inference(resolution,[status(thm)],[c_80907,c_21]) ).
tff(c_81041,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_81028,c_81039]) ).
tff(c_81047,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_81041]) ).
tff(c_81049,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_80811,plain,
! [B_1868] :
( green(B_1868,n5)
| ~ less_than(B_1868,n5)
| green(n2,B_1868)
| ~ less_than(n2,B_1868) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_81343,plain,
! [A_1881] :
( green(A_1881,n5)
| green(n2,A_1881)
| ~ less_than(n2,A_1881)
| ~ less_than(A_1881,n4) ),
inference(resolution,[status(thm)],[c_45,c_80811]) ).
tff(c_81390,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_12,c_81343]) ).
tff(c_81433,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_81390]) ).
tff(c_81434,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_81049,c_81433]) ).
tff(c_80108,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_50824]) ).
tff(c_80111,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_80108,c_21]) ).
tff(c_81436,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_81434,c_80111]) ).
tff(c_81442,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_80907,c_81436]) ).
tff(c_81444,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_50824]) ).
tff(c_82752,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_82718,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_81446,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_82426,plain,
! [B_1907] :
( green(B_1907,n6)
| ~ less_than(B_1907,n6)
| green(n1,B_1907)
| ~ less_than(n1,B_1907) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_82438,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_82426]) ).
tff(c_82454,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_80061,c_82438]) ).
tff(c_82464,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_82454]) ).
tff(c_82467,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_82464]) ).
tff(c_82471,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_82467]) ).
tff(c_82472,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_82454]) ).
tff(c_82577,plain,
! [B_1910] :
( ~ green(B_1910,n3)
| ~ green(n1,B_1910) ),
inference(resolution,[status(thm)],[c_82472,c_21]) ).
tff(c_82581,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_81446,c_82577]) ).
tff(c_82586,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_82581]) ).
tff(c_82588,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_82652,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_237]) ).
tff(c_82661,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_82652]) ).
tff(c_82667,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_82661]) ).
tff(c_82669,plain,
less_than(n3,n5),
inference(splitRight,[status(thm)],[c_237]) ).
tff(c_85694,plain,
! [B_1966] :
( green(B_1966,n5)
| ~ less_than(B_1966,n5)
| green(n2,B_1966)
| ~ less_than(n2,B_1966) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_85698,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_82669,c_85694]) ).
tff(c_85714,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_85698]) ).
tff(c_85715,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_82588,c_85714]) ).
tff(c_85732,plain,
! [B_1967] :
( ~ green(B_1967,n5)
| ~ green(n3,B_1967) ),
inference(resolution,[status(thm)],[c_85715,c_21]) ).
tff(c_85738,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_82752,c_85732]) ).
tff(c_85926,plain,
! [B_1972] :
( green(B_1972,n6)
| ~ less_than(B_1972,n6)
| green(n3,B_1972)
| ~ less_than(n3,B_1972) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_87147,plain,
! [A_1991] :
( green(A_1991,n6)
| green(n3,A_1991)
| ~ less_than(n3,A_1991)
| ~ less_than(A_1991,n5) ),
inference(resolution,[status(thm)],[c_47,c_85926]) ).
tff(c_87195,plain,
( green(n4,n6)
| green(n3,n4)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_10,c_87147]) ).
tff(c_87245,plain,
( green(n4,n6)
| green(n3,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_87195]) ).
tff(c_87246,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_85738,c_87245]) ).
tff(c_87300,plain,
! [B_1994] :
( ~ green(B_1994,n6)
| ~ green(n4,B_1994) ),
inference(resolution,[status(thm)],[c_87246,c_21]) ).
tff(c_87304,plain,
~ green(n4,n5),
inference(resolution,[status(thm)],[c_82718,c_87300]) ).
tff(c_87309,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_82752,c_87304]) ).
tff(c_87311,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_87977,plain,
! [B_2011] :
( green(B_2011,n5)
| ~ less_than(B_2011,n5)
| green(n2,B_2011)
| ~ less_than(n2,B_2011) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_87993,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_87977]) ).
tff(c_88008,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50756,c_87993]) ).
tff(c_88009,plain,
green(n2,n4),
inference(negUnitSimplification,[status(thm)],[c_87311,c_88008]) ).
tff(c_87690,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_50850]) ).
tff(c_87693,plain,
! [B_5] :
( ~ green(B_5,n4)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_87690,c_21]) ).
tff(c_88011,plain,
~ green(n1,n2),
inference(resolution,[status(thm)],[c_88009,c_87693]) ).
tff(c_88017,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_50735,c_88011]) ).
tff(c_88019,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_50850]) ).
tff(c_88483,plain,
! [B_2025] :
( green(B_2025,n5)
| ~ less_than(B_2025,n5)
| green(n1,B_2025)
| ~ less_than(n1,B_2025) ),
inference(splitRight,[status(thm)],[c_50824]) ).
tff(c_88499,plain,
( green(n4,n5)
| green(n1,n4)
| ~ less_than(n1,n4) ),
inference(resolution,[status(thm)],[c_8,c_88483]) ).
tff(c_88515,plain,
( green(n4,n5)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_50804,c_88499]) ).
tff(c_88517,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_88019,c_87311,c_88515]) ).
tff(c_88519,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_89414,plain,
! [B_2050] :
( green(B_2050,n6)
| ~ less_than(B_2050,n6)
| green(n1,B_2050)
| ~ less_than(n1,B_2050) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_89430,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_89414]) ).
tff(c_89446,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_50755,c_89430]) ).
tff(c_89448,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_81444,c_88519,c_89446]) ).
tff(c_89450,plain,
~ green(n1,n2),
inference(splitRight,[status(thm)],[c_200]) ).
tff(c_108647,plain,
less_than(n2,n4),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_108672,plain,
( less_than(n2,n6)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_108647,c_64]) ).
tff(c_108685,plain,
less_than(n2,n6),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_108672]) ).
tff(c_99579,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_89455,plain,
green(n1,n6),
inference(splitLeft,[status(thm)],[c_282]) ).
tff(c_89462,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_89455,c_21]) ).
tff(c_99584,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_99579,c_89462]) ).
tff(c_89463,plain,
~ less_than(n2,n4),
inference(splitLeft,[status(thm)],[c_151]) ).
tff(c_89466,plain,
~ less_than(n2,n3),
inference(resolution,[status(thm)],[c_44,c_89463]) ).
tff(c_89470,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12,c_89466]) ).
tff(c_89471,plain,
less_than(n1,n5),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_89489,plain,
! [B_11] :
( green(n1,n5)
| green(B_11,n5)
| ~ less_than(B_11,n5)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_89471,c_109]) ).
tff(c_101158,plain,
! [B_2369] :
( green(B_2369,n5)
| ~ less_than(B_2369,n5)
| green(n1,B_2369)
| ~ less_than(n1,B_2369) ),
inference(negUnitSimplification,[status(thm)],[c_99584,c_89489]) ).
tff(c_101166,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_101158]) ).
tff(c_101177,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_101166]) ).
tff(c_101179,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_101177]) ).
tff(c_101181,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_98156,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_97577,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_97582,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_97577,c_89462]) ).
tff(c_89472,plain,
less_than(n2,n4),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_89566,plain,
! [B_11] :
( green(n2,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_89472,c_109]) ).
tff(c_89846,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_89566]) ).
tff(c_89494,plain,
! [A_2051,A_2052] :
( less_than(A_2051,n4)
| ~ less_than(A_2051,A_2052)
| ~ less_than(A_2052,n3) ),
inference(resolution,[status(thm)],[c_49,c_16]) ).
tff(c_89522,plain,
( less_than(n1,n4)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_14,c_89494]) ).
tff(c_89544,plain,
less_than(n1,n4),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_89522]) ).
tff(c_89593,plain,
! [B_11] :
( green(n1,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_89544,c_109]) ).
tff(c_89733,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_89593]) ).
tff(c_89860,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_91086,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_89489]) ).
tff(c_91093,plain,
! [B_2095] :
( ~ green(B_2095,n5)
| ~ green(n1,B_2095) ),
inference(resolution,[status(thm)],[c_91086,c_21]) ).
tff(c_91097,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_89860,c_91093]) ).
tff(c_91102,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_89733,c_91097]) ).
tff(c_91106,plain,
! [B_2096] :
( green(B_2096,n5)
| ~ less_than(B_2096,n5)
| green(n1,B_2096)
| ~ less_than(n1,B_2096) ),
inference(splitRight,[status(thm)],[c_89489]) ).
tff(c_91114,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_91106]) ).
tff(c_91125,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_91114]) ).
tff(c_91127,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_91125]) ).
tff(c_91129,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_92117,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_92122,plain,
~ green(n1,n5),
inference(resolution,[status(thm)],[c_92117,c_89462]) ).
tff(c_92377,plain,
! [B_2124] :
( green(B_2124,n5)
| ~ less_than(B_2124,n5)
| green(n1,B_2124)
| ~ less_than(n1,B_2124) ),
inference(negUnitSimplification,[status(thm)],[c_92122,c_89489]) ).
tff(c_92385,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_92377]) ).
tff(c_92396,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_92385]) ).
tff(c_92398,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_92396]) ).
tff(c_92400,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_94081,plain,
! [A_2184,B_2185] :
( green(A_2184,n6)
| green(B_2185,n6)
| ~ less_than(B_2185,n6)
| green(A_2184,B_2185)
| ~ less_than(A_2184,B_2185)
| ~ less_than(A_2184,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_94097,plain,
! [A_2184] :
( green(A_2184,n6)
| green(n5,n6)
| green(A_2184,n5)
| ~ less_than(A_2184,n5) ),
inference(resolution,[status(thm)],[c_6,c_94081]) ).
tff(c_94111,plain,
! [A_2186] :
( green(A_2186,n6)
| green(A_2186,n5)
| ~ less_than(A_2186,n5) ),
inference(negUnitSimplification,[status(thm)],[c_92400,c_94097]) ).
tff(c_94135,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_94111]) ).
tff(c_94150,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_91129,c_94135]) ).
tff(c_89550,plain,
( less_than(n2,n6)
| ~ less_than(n4,n5) ),
inference(resolution,[status(thm)],[c_89472,c_64]) ).
tff(c_89565,plain,
less_than(n2,n6),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_89550]) ).
tff(c_89626,plain,
! [B_11] :
( green(n2,n6)
| green(B_11,n6)
| ~ less_than(B_11,n6)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_89565,c_109]) ).
tff(c_93126,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_89626]) ).
tff(c_93132,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_93126,c_21]) ).
tff(c_94152,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_94150,c_93132]) ).
tff(c_94160,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_89846,c_94152]) ).
tff(c_94162,plain,
~ green(n2,n6),
inference(splitRight,[status(thm)],[c_89626]) ).
tff(c_95337,plain,
! [A_2224,B_2225] :
( green(A_2224,n6)
| green(B_2225,n6)
| ~ less_than(B_2225,n6)
| green(A_2224,B_2225)
| ~ less_than(A_2224,B_2225)
| ~ less_than(A_2224,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_95353,plain,
! [A_2224] :
( green(A_2224,n6)
| green(n5,n6)
| green(A_2224,n5)
| ~ less_than(A_2224,n5) ),
inference(resolution,[status(thm)],[c_6,c_95337]) ).
tff(c_95369,plain,
! [A_2226] :
( green(A_2226,n6)
| green(A_2226,n5)
| ~ less_than(A_2226,n5) ),
inference(negUnitSimplification,[status(thm)],[c_92400,c_95353]) ).
tff(c_95387,plain,
( green(n2,n6)
| green(n2,n5) ),
inference(resolution,[status(thm)],[c_149,c_95369]) ).
tff(c_95405,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50686,c_94162,c_95387]) ).
tff(c_95407,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_89566]) ).
tff(c_95576,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_97133,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_89489]) ).
tff(c_97152,plain,
! [B_2265] :
( ~ green(B_2265,n5)
| ~ green(n1,B_2265) ),
inference(resolution,[status(thm)],[c_97133,c_21]) ).
tff(c_97156,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_95576,c_97152]) ).
tff(c_97161,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_89733,c_97156]) ).
tff(c_97164,plain,
! [B_2266] :
( green(B_2266,n5)
| ~ less_than(B_2266,n5)
| green(n1,B_2266)
| ~ less_than(n1,B_2266) ),
inference(splitRight,[status(thm)],[c_89489]) ).
tff(c_97172,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_97164]) ).
tff(c_97183,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_97172]) ).
tff(c_97185,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_97183]) ).
tff(c_97187,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_97535,plain,
! [B_2276] :
( green(B_2276,n5)
| ~ less_than(B_2276,n5)
| green(n2,B_2276)
| ~ less_than(n2,B_2276) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_97547,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_97535]) ).
tff(c_97556,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_89472,c_97547]) ).
tff(c_97558,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_95407,c_97187,c_97556]) ).
tff(c_98579,plain,
! [B_2308] :
( green(B_2308,n4)
| ~ less_than(B_2308,n4)
| green(n1,B_2308)
| ~ less_than(n1,B_2308) ),
inference(splitRight,[status(thm)],[c_89593]) ).
tff(c_98591,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_98579]) ).
tff(c_98603,plain,
( green(n3,n4)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_97582,c_98591]) ).
tff(c_98604,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_98603]) ).
tff(c_98607,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_98604]) ).
tff(c_98611,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_98607]) ).
tff(c_98612,plain,
green(n3,n4),
inference(splitRight,[status(thm)],[c_98603]) ).
tff(c_98520,plain,
! [B_2305] :
( green(B_2305,n5)
| ~ less_than(B_2305,n5)
| green(n2,B_2305)
| ~ less_than(n2,B_2305) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_98532,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_98520]) ).
tff(c_98542,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_89472,c_98532]) ).
tff(c_98543,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_98542]) ).
tff(c_98574,plain,
! [B_5] :
( ~ green(B_5,n4)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_98543,c_21]) ).
tff(c_98672,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_98612,c_98574]) ).
tff(c_98678,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_98156,c_98672]) ).
tff(c_98680,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_98542]) ).
tff(c_98723,plain,
! [B_2311] :
( green(B_2311,n4)
| ~ less_than(B_2311,n4)
| green(n1,B_2311)
| ~ less_than(n1,B_2311) ),
inference(splitRight,[status(thm)],[c_89593]) ).
tff(c_98731,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_89472,c_98723]) ).
tff(c_98742,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_98731]) ).
tff(c_98744,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_98680,c_98742]) ).
tff(c_98746,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_99130,plain,
! [B_2323] :
( green(B_2323,n4)
| ~ less_than(B_2323,n4)
| green(n1,B_2323)
| ~ less_than(n1,B_2323) ),
inference(splitRight,[status(thm)],[c_89593]) ).
tff(c_99142,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_99130]) ).
tff(c_99154,plain,
( green(n3,n4)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_97582,c_99142]) ).
tff(c_99155,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_99154]) ).
tff(c_99158,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_99155]) ).
tff(c_99162,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_99158]) ).
tff(c_99164,plain,
less_than(n1,n3),
inference(splitRight,[status(thm)],[c_99154]) ).
tff(c_99186,plain,
! [B_11] :
( green(n1,n3)
| green(B_11,n3)
| ~ less_than(B_11,n3)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_99164,c_109]) ).
tff(c_99521,plain,
! [B_2332] :
( green(B_2332,n3)
| ~ less_than(B_2332,n3)
| green(n1,B_2332)
| ~ less_than(n1,B_2332) ),
inference(negUnitSimplification,[status(thm)],[c_97582,c_99186]) ).
tff(c_99529,plain,
( green(n2,n3)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_12,c_99521]) ).
tff(c_99536,plain,
( green(n2,n3)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_99529]) ).
tff(c_99538,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_98746,c_99536]) ).
tff(c_107304,plain,
! [B_2544] :
( green(B_2544,n6)
| ~ less_than(B_2544,n6)
| green(n3,B_2544)
| ~ less_than(n3,B_2544) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_107320,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_107304]) ).
tff(c_107333,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_101181,c_107320]) ).
tff(c_107347,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_107333]) ).
tff(c_107378,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_107347]) ).
tff(c_107384,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_107378]) ).
tff(c_107385,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_107333]) ).
tff(c_104875,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_89489]) ).
tff(c_104878,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_104875,c_21]) ).
tff(c_107450,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_107385,c_104878]) ).
tff(c_105515,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_105222,plain,
green(n3,n4),
inference(splitLeft,[status(thm)],[c_196]) ).
tff(c_102853,plain,
! [B_2417] :
( green(B_2417,n6)
| ~ less_than(B_2417,n6)
| green(n3,B_2417)
| ~ less_than(n3,B_2417) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_102869,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_102853]) ).
tff(c_102882,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_101181,c_102869]) ).
tff(c_102920,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_102882]) ).
tff(c_102933,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_102920]) ).
tff(c_102939,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_102933]) ).
tff(c_102940,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_102882]) ).
tff(c_101239,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_89489]) ).
tff(c_101245,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_101239,c_21]) ).
tff(c_103007,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_102940,c_101245]) ).
tff(c_101422,plain,
green(n3,n4),
inference(splitLeft,[status(thm)],[c_196]) ).
tff(c_101209,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_102227,plain,
! [B_2400] :
( green(B_2400,n6)
| ~ less_than(B_2400,n6)
| green(n3,B_2400)
| ~ less_than(n3,B_2400) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_102243,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_102227]) ).
tff(c_102256,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_101181,c_102243]) ).
tff(c_102278,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_102256]) ).
tff(c_102287,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_102278]) ).
tff(c_102293,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_102287]) ).
tff(c_102294,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_102256]) ).
tff(c_102374,plain,
! [B_2403] :
( ~ green(B_2403,n5)
| ~ green(n3,B_2403) ),
inference(resolution,[status(thm)],[c_102294,c_21]) ).
tff(c_102380,plain,
~ green(n3,n4),
inference(resolution,[status(thm)],[c_101209,c_102374]) ).
tff(c_102386,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_101422,c_102380]) ).
tff(c_102388,plain,
~ green(n3,n4),
inference(splitRight,[status(thm)],[c_196]) ).
tff(c_103010,plain,
! [B_2419] :
( green(B_2419,n4)
| ~ less_than(B_2419,n4)
| green(n1,B_2419)
| ~ less_than(n1,B_2419) ),
inference(splitRight,[status(thm)],[c_89593]) ).
tff(c_103022,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_103010]) ).
tff(c_103034,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_103007,c_102388,c_103022]) ).
tff(c_103040,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_103034]) ).
tff(c_103044,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_103040]) ).
tff(c_103046,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_89489]) ).
tff(c_122,plain,
! [A_23] :
( less_than(A_23,n5)
| ~ less_than(n3,n4)
| ~ less_than(A_23,n2) ),
inference(resolution,[status(thm)],[c_46,c_116]) ).
tff(c_89676,plain,
! [A_2056] :
( less_than(A_2056,n5)
| ~ less_than(A_2056,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_122]) ).
tff(c_104637,plain,
! [A_2464,B_2465] :
( green(A_2464,n5)
| green(B_2465,n5)
| ~ less_than(B_2465,n5)
| green(A_2464,B_2465)
| ~ less_than(A_2464,B_2465)
| ~ less_than(A_2464,n2) ),
inference(resolution,[status(thm)],[c_89676,c_109]) ).
tff(c_104645,plain,
! [A_2464] :
( green(A_2464,n5)
| green(n2,n5)
| green(A_2464,n2)
| ~ less_than(A_2464,n2) ),
inference(resolution,[status(thm)],[c_149,c_104637]) ).
tff(c_104837,plain,
! [A_2469] :
( green(A_2469,n5)
| green(A_2469,n2)
| ~ less_than(A_2469,n2) ),
inference(negUnitSimplification,[status(thm)],[c_50686,c_104645]) ).
tff(c_104843,plain,
( green(n1,n5)
| green(n1,n2) ),
inference(resolution,[status(thm)],[c_14,c_104837]) ).
tff(c_104848,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_103046,c_104843]) ).
tff(c_104850,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_105491,plain,
! [B_2488] :
( green(B_2488,n5)
| ~ less_than(B_2488,n5)
| green(n2,B_2488)
| ~ less_than(n2,B_2488) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_105503,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_105491]) ).
tff(c_105513,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_89472,c_105503]) ).
tff(c_105514,plain,
green(n2,n4),
inference(negUnitSimplification,[status(thm)],[c_104850,c_105513]) ).
tff(c_105553,plain,
! [B_2491] :
( ~ green(B_2491,n4)
| ~ green(n2,B_2491) ),
inference(resolution,[status(thm)],[c_105514,c_21]) ).
tff(c_105557,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_105222,c_105553]) ).
tff(c_105562,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_105515,c_105557]) ).
tff(c_105564,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_106872,plain,
! [A_2528,B_2529] :
( green(A_2528,n6)
| green(B_2529,n6)
| ~ less_than(B_2529,n6)
| green(A_2528,B_2529)
| ~ less_than(A_2528,B_2529)
| ~ less_than(A_2528,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_106888,plain,
! [A_2528] :
( green(A_2528,n6)
| green(n5,n6)
| green(A_2528,n5)
| ~ less_than(A_2528,n5) ),
inference(resolution,[status(thm)],[c_6,c_106872]) ).
tff(c_106902,plain,
! [A_2530] :
( green(A_2530,n6)
| green(A_2530,n5)
| ~ less_than(A_2530,n5) ),
inference(negUnitSimplification,[status(thm)],[c_101181,c_106888]) ).
tff(c_106926,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_106902]) ).
tff(c_106941,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_104850,c_106926]) ).
tff(c_106389,plain,
green(n2,n6),
inference(splitLeft,[status(thm)],[c_89626]) ).
tff(c_106395,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_106389,c_21]) ).
tff(c_106943,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_106941,c_106395]) ).
tff(c_106951,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_105514,c_106943]) ).
tff(c_106953,plain,
~ green(n2,n6),
inference(splitRight,[status(thm)],[c_89626]) ).
tff(c_99540,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_89632,plain,
! [A_2054] :
( less_than(A_2054,n6)
| ~ less_than(A_2054,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_223]) ).
tff(c_106965,plain,
! [A_2532,B_2533] :
( green(A_2532,n6)
| green(B_2533,n6)
| ~ less_than(B_2533,n6)
| green(A_2532,B_2533)
| ~ less_than(A_2532,B_2533)
| ~ less_than(A_2532,n3) ),
inference(resolution,[status(thm)],[c_89632,c_109]) ).
tff(c_106977,plain,
! [A_2532] :
( green(A_2532,n6)
| green(n3,n6)
| green(A_2532,n3)
| ~ less_than(A_2532,n3) ),
inference(resolution,[status(thm)],[c_246,c_106965]) ).
tff(c_106997,plain,
! [A_2534] :
( green(A_2534,n6)
| green(A_2534,n3)
| ~ less_than(A_2534,n3) ),
inference(negUnitSimplification,[status(thm)],[c_99540,c_106977]) ).
tff(c_107003,plain,
( green(n2,n6)
| green(n2,n3) ),
inference(resolution,[status(thm)],[c_12,c_106997]) ).
tff(c_107008,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_105564,c_106953,c_107003]) ).
tff(c_107010,plain,
~ green(n3,n4),
inference(splitRight,[status(thm)],[c_196]) ).
tff(c_107673,plain,
! [B_2554] :
( green(B_2554,n4)
| ~ less_than(B_2554,n4)
| green(n1,B_2554)
| ~ less_than(n1,B_2554) ),
inference(splitRight,[status(thm)],[c_89593]) ).
tff(c_107685,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_107673]) ).
tff(c_107697,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_107450,c_107010,c_107685]) ).
tff(c_107700,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_107697]) ).
tff(c_107704,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_107700]) ).
tff(c_108609,plain,
! [B_2583] :
( green(B_2583,n5)
| ~ less_than(B_2583,n5)
| green(n1,B_2583)
| ~ less_than(n1,B_2583) ),
inference(splitRight,[status(thm)],[c_89489]) ).
tff(c_108617,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_108609]) ).
tff(c_108628,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_108617]) ).
tff(c_108630,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_108628]) ).
tff(c_133849,plain,
! [B_3245] :
( green(B_3245,n6)
| ~ less_than(B_3245,n6)
| green(n1,B_3245)
| ~ less_than(n1,B_3245) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_133857,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_133849]) ).
tff(c_133871,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_133857]) ).
tff(c_133872,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_133871]) ).
tff(c_133905,plain,
! [B_3247] :
( ~ green(B_3247,n6)
| ~ green(n2,B_3247) ),
inference(resolution,[status(thm)],[c_133872,c_21]) ).
tff(c_133909,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_133069,c_133905]) ).
tff(c_133914,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_133512,c_133909]) ).
tff(c_133916,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_108686,plain,
! [B_11] :
( green(n2,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n2,B_11)
| ~ less_than(n2,B_11) ),
inference(resolution,[status(thm)],[c_108647,c_109]) ).
tff(c_114563,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_108686]) ).
tff(c_108810,plain,
green(n3,n4),
inference(splitLeft,[status(thm)],[c_196]) ).
tff(c_108715,plain,
! [A_2584,A_2585] :
( less_than(A_2584,n4)
| ~ less_than(A_2584,A_2585)
| ~ less_than(A_2585,n3) ),
inference(resolution,[status(thm)],[c_49,c_16]) ).
tff(c_108747,plain,
( less_than(n1,n4)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_14,c_108715]) ).
tff(c_108775,plain,
less_than(n1,n4),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_108747]) ).
tff(c_108797,plain,
! [B_11] :
( green(n1,n4)
| green(B_11,n4)
| ~ less_than(B_11,n4)
| green(n1,B_11)
| ~ less_than(n1,B_11) ),
inference(resolution,[status(thm)],[c_108775,c_109]) ).
tff(c_114577,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_108797]) ).
tff(c_114587,plain,
! [B_2742] :
( ~ green(B_2742,n4)
| ~ green(n1,B_2742) ),
inference(resolution,[status(thm)],[c_114577,c_21]) ).
tff(c_114596,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_108810,c_114587]) ).
tff(c_110925,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_108686]) ).
tff(c_111028,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_111540,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_108664]) ).
tff(c_111547,plain,
! [B_2657] :
( ~ green(B_2657,n5)
| ~ green(n1,B_2657) ),
inference(resolution,[status(thm)],[c_111540,c_21]) ).
tff(c_111553,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_111028,c_111547]) ).
tff(c_108691,plain,
! [A_7] :
( less_than(A_7,n4)
| ~ less_than(A_7,n2) ),
inference(resolution,[status(thm)],[c_108647,c_16]) ).
tff(c_111586,plain,
! [B_2660] :
( green(B_2660,n6)
| ~ less_than(B_2660,n6)
| green(n1,B_2660)
| ~ less_than(n1,B_2660) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_111670,plain,
! [A_2664] :
( green(A_2664,n6)
| green(n1,A_2664)
| ~ less_than(n1,A_2664)
| ~ less_than(A_2664,n5) ),
inference(resolution,[status(thm)],[c_47,c_111586]) ).
tff(c_111679,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108691,c_111670]) ).
tff(c_111724,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_111679]) ).
tff(c_111725,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_111553,c_111724]) ).
tff(c_111594,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_111586]) ).
tff(c_111608,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_111594]) ).
tff(c_111609,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_111608]) ).
tff(c_111633,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_111609,c_21]) ).
tff(c_111773,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_111725,c_111633]) ).
tff(c_111781,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_110925,c_111773]) ).
tff(c_111783,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_108664]) ).
tff(c_110789,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_108993,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_110748,plain,
! [B_2635] :
( green(B_2635,n6)
| ~ less_than(B_2635,n6)
| green(n1,B_2635)
| ~ less_than(n1,B_2635) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_110756,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_110748]) ).
tff(c_110770,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_110756]) ).
tff(c_110771,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_110770]) ).
tff(c_110797,plain,
! [B_2637] :
( ~ green(B_2637,n6)
| ~ green(n2,B_2637) ),
inference(resolution,[status(thm)],[c_110771,c_21]) ).
tff(c_110803,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_108993,c_110797]) ).
tff(c_110809,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_110789,c_110803]) ).
tff(c_110811,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_109023,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_108996,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n3,B_5) ),
inference(resolution,[status(thm)],[c_108993,c_21]) ).
tff(c_109028,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_109023,c_108996]) ).
tff(c_109386,plain,
! [B_2605] :
( green(B_2605,n5)
| ~ less_than(B_2605,n5)
| green(n2,B_2605)
| ~ less_than(n2,B_2605) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_110830,plain,
! [A_2640] :
( green(A_2640,n5)
| green(n2,A_2640)
| ~ less_than(n2,A_2640)
| ~ less_than(A_2640,n4) ),
inference(resolution,[status(thm)],[c_45,c_109386]) ).
tff(c_110874,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_12,c_110830]) ).
tff(c_110920,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_110874]) ).
tff(c_110922,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_110811,c_109028,c_110920]) ).
tff(c_110924,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_111784,plain,
! [B_2665] :
( green(B_2665,n6)
| ~ less_than(B_2665,n6)
| green(n1,B_2665)
| ~ less_than(n1,B_2665) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_111800,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_111784]) ).
tff(c_111816,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_108646,c_111800]) ).
tff(c_111818,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_111783,c_110924,c_111816]) ).
tff(c_111820,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_112814,plain,
! [A_2694,B_2695] :
( green(A_2694,n6)
| green(B_2695,n6)
| ~ less_than(B_2695,n6)
| green(A_2694,B_2695)
| ~ less_than(A_2694,B_2695)
| ~ less_than(A_2694,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_112830,plain,
! [A_2694] :
( green(A_2694,n6)
| green(n5,n6)
| green(A_2694,n5)
| ~ less_than(A_2694,n5) ),
inference(resolution,[status(thm)],[c_6,c_112814]) ).
tff(c_112845,plain,
! [A_2696] :
( green(A_2696,n6)
| green(A_2696,n5)
| ~ less_than(A_2696,n5) ),
inference(negUnitSimplification,[status(thm)],[c_110924,c_112830]) ).
tff(c_112863,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_112845]) ).
tff(c_112875,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_111820,c_112863]) ).
tff(c_112081,plain,
! [B_2673] :
( green(B_2673,n6)
| ~ less_than(B_2673,n6)
| green(n1,B_2673)
| ~ less_than(n1,B_2673) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_112089,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_112081]) ).
tff(c_112103,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_112089]) ).
tff(c_112104,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_112103]) ).
tff(c_112120,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_112104,c_21]) ).
tff(c_112877,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_112875,c_112120]) ).
tff(c_112885,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_110925,c_112877]) ).
tff(c_112887,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_108686]) ).
tff(c_113150,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_112888,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_108664]) ).
tff(c_112891,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_112888,c_21]) ).
tff(c_113155,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_113150,c_112891]) ).
tff(c_113504,plain,
! [B_2713] :
( green(B_2713,n4)
| ~ less_than(B_2713,n4)
| green(n1,B_2713)
| ~ less_than(n1,B_2713) ),
inference(negUnitSimplification,[status(thm)],[c_113155,c_108797]) ).
tff(c_113512,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108647,c_113504]) ).
tff(c_113524,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_113512]) ).
tff(c_113526,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_112887,c_113524]) ).
tff(c_113528,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_113868,plain,
! [B_2722] :
( green(B_2722,n5)
| ~ less_than(B_2722,n5)
| green(n2,B_2722)
| ~ less_than(n2,B_2722) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_113880,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_113868]) ).
tff(c_113890,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_108647,c_113880]) ).
tff(c_113892,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_112887,c_113528,c_113890]) ).
tff(c_113894,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_108664]) ).
tff(c_114504,plain,
! [B_2739] :
( green(B_2739,n6)
| ~ less_than(B_2739,n6)
| green(n1,B_2739)
| ~ less_than(n1,B_2739) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_114520,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_114504]) ).
tff(c_114536,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_108646,c_114520]) ).
tff(c_114538,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_113894,c_110924,c_114536]) ).
tff(c_114540,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_115287,plain,
! [B_2763] :
( green(B_2763,n6)
| ~ less_than(B_2763,n6)
| green(n1,B_2763)
| ~ less_than(n1,B_2763) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_115299,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_115287]) ).
tff(c_115315,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_114596,c_114540,c_115299]) ).
tff(c_115328,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_115315]) ).
tff(c_115332,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_115328]) ).
tff(c_115334,plain,
~ green(n1,n4),
inference(splitRight,[status(thm)],[c_108797]) ).
tff(c_115976,plain,
! [B_2782] :
( green(B_2782,n6)
| ~ less_than(B_2782,n6)
| green(n1,B_2782)
| ~ less_than(n1,B_2782) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_116689,plain,
! [A_2796] :
( green(A_2796,n6)
| green(n1,A_2796)
| ~ less_than(n1,A_2796)
| ~ less_than(A_2796,n5) ),
inference(resolution,[status(thm)],[c_47,c_115976]) ).
tff(c_116703,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108691,c_116689]) ).
tff(c_116753,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_116703]) ).
tff(c_116754,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_115334,c_116753]) ).
tff(c_115984,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_115976]) ).
tff(c_115998,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_115984]) ).
tff(c_115999,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_115998]) ).
tff(c_116015,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_115999,c_21]) ).
tff(c_116801,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_116754,c_116015]) ).
tff(c_116809,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_114563,c_116801]) ).
tff(c_116811,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_108686]) ).
tff(c_117979,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_108797]) ).
tff(c_117986,plain,
! [B_2831] :
( ~ green(B_2831,n4)
| ~ green(n1,B_2831) ),
inference(resolution,[status(thm)],[c_117979,c_21]) ).
tff(c_117992,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_108810,c_117986]) ).
tff(c_118508,plain,
! [B_2845] :
( green(B_2845,n6)
| ~ less_than(B_2845,n6)
| green(n1,B_2845)
| ~ less_than(n1,B_2845) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_118520,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_118508]) ).
tff(c_118537,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_117992,c_114540,c_118520]) ).
tff(c_118551,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_118537]) ).
tff(c_118555,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_118551]) ).
tff(c_119308,plain,
! [B_2868] :
( green(B_2868,n4)
| ~ less_than(B_2868,n4)
| green(n1,B_2868)
| ~ less_than(n1,B_2868) ),
inference(splitRight,[status(thm)],[c_108797]) ).
tff(c_119316,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108647,c_119308]) ).
tff(c_119327,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_119316]) ).
tff(c_119329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_116811,c_119327]) ).
tff(c_119331,plain,
~ green(n3,n4),
inference(splitRight,[status(thm)],[c_196]) ).
tff(c_131322,plain,
! [B_3178] :
( green(B_3178,n6)
| ~ less_than(B_3178,n6)
| green(n1,B_3178)
| ~ less_than(n1,B_3178) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_131349,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_131322]) ).
tff(c_131370,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_131349]) ).
tff(c_131373,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_131370]) ).
tff(c_131377,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_131373]) ).
tff(c_131379,plain,
less_than(n1,n3),
inference(splitRight,[status(thm)],[c_131349]) ).
tff(c_127321,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_108686]) ).
tff(c_127653,plain,
green(n1,n4),
inference(splitLeft,[status(thm)],[c_108797]) ).
tff(c_128254,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_127475,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_108664]) ).
tff(c_127478,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_127475,c_21]) ).
tff(c_128256,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_128254,c_127478]) ).
tff(c_128262,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_127653,c_128256]) ).
tff(c_128264,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_119539,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_121616,plain,
! [B_2929] :
( green(B_2929,n6)
| ~ less_than(B_2929,n6)
| green(n1,B_2929)
| ~ less_than(n1,B_2929) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_121624,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_121616]) ).
tff(c_121638,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_121624]) ).
tff(c_121639,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_121638]) ).
tff(c_121662,plain,
! [B_2930] :
( ~ green(B_2930,n6)
| ~ green(n2,B_2930) ),
inference(resolution,[status(thm)],[c_121639,c_21]) ).
tff(c_121670,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_119539,c_121662]) ).
tff(c_119362,plain,
green(n5,n6),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_119546,plain,
! [B_2877] :
( ~ green(B_2877,n6)
| ~ green(n3,B_2877) ),
inference(resolution,[status(thm)],[c_119539,c_21]) ).
tff(c_119552,plain,
~ green(n3,n5),
inference(resolution,[status(thm)],[c_119362,c_119546]) ).
tff(c_121676,plain,
! [B_2931] :
( green(B_2931,n5)
| ~ less_than(B_2931,n5)
| green(n2,B_2931)
| ~ less_than(n2,B_2931) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_121827,plain,
! [A_2936] :
( green(A_2936,n5)
| green(n2,A_2936)
| ~ less_than(n2,A_2936)
| ~ less_than(A_2936,n4) ),
inference(resolution,[status(thm)],[c_45,c_121676]) ).
tff(c_121871,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_12,c_121827]) ).
tff(c_121917,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_121871]) ).
tff(c_121919,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_121670,c_119552,c_121917]) ).
tff(c_121921,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_123289,plain,
! [B_2973] :
( green(B_2973,n6)
| ~ less_than(B_2973,n6)
| green(n1,B_2973)
| ~ less_than(n1,B_2973) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_123301,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_123289]) ).
tff(c_123317,plain,
( green(n1,n3)
| ~ less_than(n1,n3) ),
inference(negUnitSimplification,[status(thm)],[c_121921,c_123301]) ).
tff(c_123332,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_123317]) ).
tff(c_123335,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_123332]) ).
tff(c_123339,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_123335]) ).
tff(c_123340,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_123317]) ).
tff(c_121922,plain,
green(n2,n4),
inference(splitLeft,[status(thm)],[c_108686]) ).
tff(c_122476,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_122269,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_108664]) ).
tff(c_122272,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_122269,c_21]) ).
tff(c_122481,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_122476,c_122272]) ).
tff(c_122614,plain,
! [B_2958] :
( green(B_2958,n6)
| ~ less_than(B_2958,n6)
| green(n1,B_2958)
| ~ less_than(n1,B_2958) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_123034,plain,
! [A_2967] :
( green(A_2967,n6)
| green(n1,A_2967)
| ~ less_than(n1,A_2967)
| ~ less_than(A_2967,n5) ),
inference(resolution,[status(thm)],[c_47,c_122614]) ).
tff(c_123045,plain,
( green(n4,n6)
| green(n1,n4)
| ~ less_than(n4,n5)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108691,c_123034]) ).
tff(c_123096,plain,
( green(n4,n6)
| green(n1,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_8,c_123045]) ).
tff(c_123097,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_122481,c_123096]) ).
tff(c_122622,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_122614]) ).
tff(c_122636,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_122622]) ).
tff(c_122637,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_122636]) ).
tff(c_122652,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_122637,c_21]) ).
tff(c_123146,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_123097,c_122652]) ).
tff(c_123154,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_121922,c_123146]) ).
tff(c_123156,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_124895,plain,
! [A_3010,B_3011] :
( green(A_3010,n5)
| green(B_3011,n5)
| ~ less_than(B_3011,n5)
| green(A_3010,B_3011)
| ~ less_than(A_3010,B_3011)
| ~ less_than(A_3010,n4) ),
inference(resolution,[status(thm)],[c_45,c_167]) ).
tff(c_124907,plain,
! [A_3010] :
( green(A_3010,n5)
| green(n4,n5)
| green(A_3010,n4)
| ~ less_than(A_3010,n4) ),
inference(resolution,[status(thm)],[c_8,c_124895]) ).
tff(c_124918,plain,
! [A_3012] :
( green(A_3012,n5)
| green(A_3012,n4)
| ~ less_than(A_3012,n4) ),
inference(negUnitSimplification,[status(thm)],[c_123156,c_124907]) ).
tff(c_124936,plain,
( green(n3,n5)
| green(n3,n4) ),
inference(resolution,[status(thm)],[c_10,c_124918]) ).
tff(c_124947,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_119331,c_124936]) ).
tff(c_124949,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_124947,c_122272]) ).
tff(c_124955,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_123340,c_124949]) ).
tff(c_125610,plain,
! [B_3032] :
( green(B_3032,n5)
| ~ less_than(B_3032,n5)
| green(n1,B_3032)
| ~ less_than(n1,B_3032) ),
inference(splitRight,[status(thm)],[c_108664]) ).
tff(c_125618,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_125610]) ).
tff(c_125629,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_125618]) ).
tff(c_125631,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_125629]) ).
tff(c_125633,plain,
~ green(n2,n4),
inference(splitRight,[status(thm)],[c_108686]) ).
tff(c_126013,plain,
green(n4,n5),
inference(splitLeft,[status(thm)],[c_197]) ).
tff(c_125801,plain,
green(n1,n5),
inference(splitLeft,[status(thm)],[c_108664]) ).
tff(c_125804,plain,
! [B_5] :
( ~ green(B_5,n5)
| ~ green(n1,B_5) ),
inference(resolution,[status(thm)],[c_125801,c_21]) ).
tff(c_126018,plain,
~ green(n1,n4),
inference(resolution,[status(thm)],[c_126013,c_125804]) ).
tff(c_126122,plain,
! [B_3047] :
( green(B_3047,n4)
| ~ less_than(B_3047,n4)
| green(n1,B_3047)
| ~ less_than(n1,B_3047) ),
inference(negUnitSimplification,[status(thm)],[c_126018,c_108797]) ).
tff(c_126130,plain,
( green(n2,n4)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108647,c_126122]) ).
tff(c_126141,plain,
( green(n2,n4)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_126130]) ).
tff(c_126143,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_125633,c_126141]) ).
tff(c_126145,plain,
~ green(n4,n5),
inference(splitRight,[status(thm)],[c_197]) ).
tff(c_126518,plain,
! [B_3057] :
( green(B_3057,n5)
| ~ less_than(B_3057,n5)
| green(n2,B_3057)
| ~ less_than(n2,B_3057) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_126530,plain,
( green(n4,n5)
| green(n2,n4)
| ~ less_than(n2,n4) ),
inference(resolution,[status(thm)],[c_8,c_126518]) ).
tff(c_126540,plain,
( green(n4,n5)
| green(n2,n4) ),
inference(demodulation,[status(thm),theory(equality)],[c_108647,c_126530]) ).
tff(c_126542,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_125633,c_126145,c_126540]) ).
tff(c_127274,plain,
! [B_3079] :
( green(B_3079,n5)
| ~ less_than(B_3079,n5)
| green(n1,B_3079)
| ~ less_than(n1,B_3079) ),
inference(splitRight,[status(thm)],[c_108664]) ).
tff(c_127282,plain,
( green(n2,n5)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_149,c_127274]) ).
tff(c_127293,plain,
( green(n2,n5)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_127282]) ).
tff(c_127295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_89450,c_50686,c_127293]) ).
tff(c_127297,plain,
~ green(n5,n6),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_130278,plain,
! [A_3151,B_3152] :
( green(A_3151,n6)
| green(B_3152,n6)
| ~ less_than(B_3152,n6)
| green(A_3151,B_3152)
| ~ less_than(A_3151,B_3152)
| ~ less_than(A_3151,n5) ),
inference(resolution,[status(thm)],[c_47,c_167]) ).
tff(c_130294,plain,
! [A_3151] :
( green(A_3151,n6)
| green(n5,n6)
| green(A_3151,n5)
| ~ less_than(A_3151,n5) ),
inference(resolution,[status(thm)],[c_6,c_130278]) ).
tff(c_130308,plain,
! [A_3153] :
( green(A_3153,n6)
| green(A_3153,n5)
| ~ less_than(A_3153,n5) ),
inference(negUnitSimplification,[status(thm)],[c_127297,c_130294]) ).
tff(c_130326,plain,
( green(n4,n6)
| green(n4,n5) ),
inference(resolution,[status(thm)],[c_8,c_130308]) ).
tff(c_130338,plain,
green(n4,n6),
inference(negUnitSimplification,[status(thm)],[c_128264,c_130326]) ).
tff(c_128121,plain,
! [B_3105] :
( green(B_3105,n6)
| ~ less_than(B_3105,n6)
| green(n1,B_3105)
| ~ less_than(n1,B_3105) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_128129,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_128121]) ).
tff(c_128143,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_128129]) ).
tff(c_128144,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_128143]) ).
tff(c_128155,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_128144,c_21]) ).
tff(c_130342,plain,
~ green(n2,n4),
inference(resolution,[status(thm)],[c_130338,c_128155]) ).
tff(c_130349,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_127321,c_130342]) ).
tff(c_131700,plain,
! [B_3189] :
( green(B_3189,n4)
| ~ less_than(B_3189,n4)
| green(n1,B_3189)
| ~ less_than(n1,B_3189) ),
inference(splitRight,[status(thm)],[c_108797]) ).
tff(c_131712,plain,
( green(n3,n4)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_10,c_131700]) ).
tff(c_131724,plain,
( green(n3,n4)
| green(n1,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_131379,c_131712]) ).
tff(c_131725,plain,
green(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_119331,c_131724]) ).
tff(c_130787,plain,
green(n2,n3),
inference(splitLeft,[status(thm)],[c_198]) ).
tff(c_130823,plain,
! [B_3167] :
( green(B_3167,n6)
| ~ less_than(B_3167,n6)
| green(n1,B_3167)
| ~ less_than(n1,B_3167) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_130850,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_130823]) ).
tff(c_130867,plain,
~ less_than(n1,n3),
inference(splitLeft,[status(thm)],[c_130850]) ).
tff(c_130870,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_130867]) ).
tff(c_130874,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_130870]) ).
tff(c_130875,plain,
( green(n1,n3)
| green(n3,n6) ),
inference(splitRight,[status(thm)],[c_130850]) ).
tff(c_130932,plain,
green(n3,n6),
inference(splitLeft,[status(thm)],[c_130875]) ).
tff(c_130831,plain,
( green(n2,n6)
| green(n1,n2)
| ~ less_than(n1,n2) ),
inference(resolution,[status(thm)],[c_108685,c_130823]) ).
tff(c_130845,plain,
( green(n2,n6)
| green(n1,n2) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_130831]) ).
tff(c_130846,plain,
green(n2,n6),
inference(negUnitSimplification,[status(thm)],[c_89450,c_130845]) ).
tff(c_130858,plain,
! [B_5] :
( ~ green(B_5,n6)
| ~ green(n2,B_5) ),
inference(resolution,[status(thm)],[c_130846,c_21]) ).
tff(c_130934,plain,
~ green(n2,n3),
inference(resolution,[status(thm)],[c_130932,c_130858]) ).
tff(c_130940,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_130787,c_130934]) ).
tff(c_130941,plain,
green(n1,n3),
inference(splitRight,[status(thm)],[c_130875]) ).
tff(c_130942,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_130875]) ).
tff(c_131197,plain,
! [B_3177] :
( green(B_3177,n6)
| ~ less_than(B_3177,n6)
| green(n3,B_3177)
| ~ less_than(n3,B_3177) ),
inference(negUnitSimplification,[status(thm)],[c_130942,c_266]) ).
tff(c_131213,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_131197]) ).
tff(c_131226,plain,
( green(n3,n5)
| ~ less_than(n3,n5) ),
inference(negUnitSimplification,[status(thm)],[c_127297,c_131213]) ).
tff(c_131227,plain,
~ less_than(n3,n5),
inference(splitLeft,[status(thm)],[c_131226]) ).
tff(c_131236,plain,
~ less_than(n3,n4),
inference(resolution,[status(thm)],[c_45,c_131227]) ).
tff(c_131242,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_131236]) ).
tff(c_131243,plain,
green(n3,n5),
inference(splitRight,[status(thm)],[c_131226]) ).
tff(c_131312,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_131243,c_127478]) ).
tff(c_131319,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_130941,c_131312]) ).
tff(c_131321,plain,
~ green(n2,n3),
inference(splitRight,[status(thm)],[c_198]) ).
tff(c_131450,plain,
! [B_3182] :
( green(B_3182,n5)
| ~ less_than(B_3182,n5)
| green(n2,B_3182)
| ~ less_than(n2,B_3182) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_132215,plain,
! [A_3199] :
( green(A_3199,n5)
| green(n2,A_3199)
| ~ less_than(n2,A_3199)
| ~ less_than(A_3199,n4) ),
inference(resolution,[status(thm)],[c_45,c_131450]) ).
tff(c_132262,plain,
( green(n3,n5)
| green(n2,n3)
| ~ less_than(n3,n4) ),
inference(resolution,[status(thm)],[c_12,c_132215]) ).
tff(c_132308,plain,
( green(n3,n5)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_132262]) ).
tff(c_132309,plain,
green(n3,n5),
inference(negUnitSimplification,[status(thm)],[c_131321,c_132308]) ).
tff(c_132313,plain,
~ green(n1,n3),
inference(resolution,[status(thm)],[c_132309,c_127478]) ).
tff(c_132320,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_131725,c_132313]) ).
tff(c_132322,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_108664]) ).
tff(c_132976,plain,
! [B_3219] :
( green(B_3219,n6)
| ~ less_than(B_3219,n6)
| green(n1,B_3219)
| ~ less_than(n1,B_3219) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_132992,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_132976]) ).
tff(c_133006,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_108646,c_132992]) ).
tff(c_133008,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_132322,c_127297,c_133006]) ).
tff(c_134253,plain,
! [B_3258] :
( green(B_3258,n4)
| ~ less_than(B_3258,n4)
| green(n2,B_3258)
| ~ less_than(n2,B_3258) ),
inference(splitRight,[status(thm)],[c_108686]) ).
tff(c_134265,plain,
( green(n3,n4)
| green(n2,n3)
| ~ less_than(n2,n3) ),
inference(resolution,[status(thm)],[c_10,c_134253]) ).
tff(c_134275,plain,
( green(n3,n4)
| green(n2,n3) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_134265]) ).
tff(c_134277,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_133916,c_119331,c_134275]) ).
tff(c_134279,plain,
~ green(n3,n6),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_136521,plain,
! [B_3318] :
( green(B_3318,n6)
| ~ less_than(B_3318,n6)
| green(n1,B_3318)
| ~ less_than(n1,B_3318) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_136533,plain,
( green(n3,n6)
| green(n1,n3)
| ~ less_than(n1,n3) ),
inference(resolution,[status(thm)],[c_246,c_136521]) ).
tff(c_136549,plain,
~ less_than(n1,n3),
inference(negUnitSimplification,[status(thm)],[c_136186,c_134279,c_136533]) ).
tff(c_136584,plain,
~ less_than(n1,n2),
inference(resolution,[status(thm)],[c_46,c_136549]) ).
tff(c_136588,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14,c_136584]) ).
tff(c_136590,plain,
~ green(n3,n5),
inference(splitRight,[status(thm)],[c_135655]) ).
tff(c_137233,plain,
! [B_3336] :
( green(B_3336,n6)
| ~ less_than(B_3336,n6)
| green(n3,B_3336)
| ~ less_than(n3,B_3336) ),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_137249,plain,
( green(n5,n6)
| green(n3,n5)
| ~ less_than(n3,n5) ),
inference(resolution,[status(thm)],[c_6,c_137233]) ).
tff(c_137263,plain,
( green(n5,n6)
| green(n3,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_135635,c_137249]) ).
tff(c_137265,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_136590,c_127297,c_137263]) ).
tff(c_137267,plain,
~ green(n1,n5),
inference(splitRight,[status(thm)],[c_108664]) ).
tff(c_138015,plain,
! [B_3354] :
( green(B_3354,n6)
| ~ less_than(B_3354,n6)
| green(n1,B_3354)
| ~ less_than(n1,B_3354) ),
inference(splitRight,[status(thm)],[c_282]) ).
tff(c_138031,plain,
( green(n5,n6)
| green(n1,n5)
| ~ less_than(n1,n5) ),
inference(resolution,[status(thm)],[c_6,c_138015]) ).
tff(c_138048,plain,
( green(n5,n6)
| green(n1,n5) ),
inference(demodulation,[status(thm),theory(equality)],[c_108646,c_138031]) ).
tff(c_138050,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_137267,c_127297,c_138048]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA014+1 : TPTP v9.0.0. Released v3.2.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 20:51:18 EDT 2025
% 0.12/0.34 % CPUTime :
% 17.60/8.79 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.96/9.02
% 17.96/9.02 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------