%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PRO009+1 : TPTP v9.0.0. Released v4.0.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 : n012.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 08:24:10 PM UTC 2025
% Result : Theorem 82.92s 65.02s
% Output : CNFRefutation 83.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 29
% Syntax : Number of formulae : 303 ( 77 unt; 0 typ; 0 def)
% Number of atoms : 831 ( 84 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 997 ( 469 ~; 466 |; 36 &)
% ( 7 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 6 con; 0-4 aty)
% Number of variables : 396 ( 381 !; 15 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ next_subocc > min_precedes > subactivity_occurrence > subactivity > root_occ > root > precedes > occurrence_of > leaf_occ > leaf > earlier > atocc > legal > atomic > arboreal > activity_occurrence > activity > #nlpp > tptp4 > tptp3 > tptp2 > tptp1 > tptp0 > #skF_11 > #skF_16 > #skF_6 > #skF_18 > #skF_13 > #skF_1 > #skF_19 > #skF_14 > #skF_12 > #skF_5 > #skF_2 > #skF_17 > #skF_3 > #skF_8 > #skF_7 > #skF_9 > #skF_15 > #skF_4 > #skF_10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_11',type,
'#skF_11': ( $i * $i ) > $i ).
tff(arboreal,type,
arboreal: $i > $o ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(tptp1,type,
tptp1: $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i ) > $i ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff('#skF_13',type,
'#skF_13': ( $i * $i * $i * $i ) > $i ).
tff(subactivity,type,
subactivity: ( $i * $i ) > $o ).
tff(root,type,
root: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(tptp2,type,
tptp2: $i ).
tff(leaf,type,
leaf: ( $i * $i ) > $o ).
tff(tptp0,type,
tptp0: $i ).
tff('#skF_19',type,
'#skF_19': $i ).
tff(root_occ,type,
root_occ: ( $i * $i ) > $o ).
tff(tptp3,type,
tptp3: $i ).
tff(occurrence_of,type,
occurrence_of: ( $i * $i ) > $o ).
tff(atomic,type,
atomic: $i > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff(tptp4,type,
tptp4: $i ).
tff('#skF_12',type,
'#skF_12': ( $i * $i ) > $i ).
tff(legal,type,
legal: $i > $o ).
tff(earlier,type,
earlier: ( $i * $i ) > $o ).
tff(activity_occurrence,type,
activity_occurrence: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(leaf_occ,type,
leaf_occ: ( $i * $i ) > $o ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff(activity,type,
activity: $i > $o ).
tff(min_precedes,type,
min_precedes: ( $i * $i * $i ) > $o ).
tff(precedes,type,
precedes: ( $i * $i ) > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff(subactivity_occurrence,type,
subactivity_occurrence: ( $i * $i ) > $o ).
tff(next_subocc,type,
next_subocc: ( $i * $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff(atocc,type,
atocc: ( $i * $i ) > $o ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i * $i ) > $i ).
tff(f_328,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_45) ).
tff(f_348,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( occurrence_of(X110,tptp3)
& root_occ(X110,X109)
& ( occurrence_of(X111,tptp2)
| occurrence_of(X111,tptp1) )
& min_precedes(X110,X111,tptp0)
& leaf_occ(X111,X109) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
tff(f_313,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( occurrence_of(X106,tptp3)
& root_occ(X106,X105)
& occurrence_of(X107,tptp4)
& next_subocc(X106,X107,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(X107,X108,tptp0)
& leaf_occ(X108,X105) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
tff(f_30,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos) ).
tff(f_285,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( occurrence_of(X100,X101)
& subactivity_occurrence(X99,X100)
& root(X99,X101) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
tff(f_43,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X5)
& occurrence_of(X4,X6) )
=> ( X5 = X6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
tff(f_108,axiom,
! [X28,X29] :
( root(X29,X28)
=> ? [X30] :
( subactivity(X30,X28)
& atocc(X29,X30) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
tff(f_185,axiom,
! [X64,X65] :
( atocc(X64,X65)
<=> ? [X66] :
( subactivity(X65,X66)
& atomic(X66)
& occurrence_of(X64,X66) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_23) ).
tff(f_176,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( min_precedes(X60,X61,X62)
& ~ ? [X63] :
( min_precedes(X60,X63,X62)
& min_precedes(X63,X61,X62) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
tff(f_37,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( activity(X3)
& occurrence_of(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
tff(f_320,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
tff(f_47,axiom,
! [X7] :
( activity(X7)
=> subactivity(X7,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
tff(f_330,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_46) ).
tff(f_294,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( occurrence_of(X103,X104)
& subactivity_occurrence(X102,X103)
& leaf(X102,X104) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
tff(f_191,axiom,
! [X67,X68] :
( subactivity_occurrence(X67,X68)
=> ( activity_occurrence(X67)
& activity_occurrence(X68) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
tff(f_166,axiom,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ( root(X56,X57)
| ? [X58] : min_precedes(X58,X56,X57) )
& ~ ? [X59] : min_precedes(X56,X59,X57) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
tff(f_115,axiom,
! [X31,X32,X33] :
( min_precedes(X31,X32,X33)
=> ? [X34] :
( root(X34,X33)
& min_precedes(X34,X32,X33) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_13) ).
tff(f_124,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_15) ).
tff(f_90,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( earlier(X21,X22)
& legal(X22) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_10) ).
tff(f_128,axiom,
! [X41,X42] :
( root(X41,X42)
=> legal(X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
tff(f_78,axiom,
! [X18] :
( legal(X18)
=> arboreal(X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
tff(f_74,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
tff(f_276,axiom,
! [X94,X95,X96,X97] :
( ( occurrence_of(X96,X94)
& occurrence_of(X97,X95)
& subactivity(X94,X95)
& ~ subactivity_occurrence(X96,X97) )
=> ? [X98] :
( subactivity_occurrence(X98,X97)
& ~ subactivity_occurrence(X98,X96) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
tff(f_134,axiom,
! [X43,X44] :
( ( atocc(X43,X44)
& legal(X43) )
=> root(X43,X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_17) ).
tff(f_236,axiom,
! [X79,X80,X81,X82] :
( ( occurrence_of(X80,X79)
& arboreal(X81)
& arboreal(X82)
& subactivity_occurrence(X81,X80)
& subactivity_occurrence(X82,X80) )
=> ( min_precedes(X81,X82,X79)
| min_precedes(X82,X81,X79)
| ( X81 = X82 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
tff(f_318,axiom,
atomic(tptp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_39) ).
tff(f_261,axiom,
! [X91,X92,X93] :
( ( subactivity_occurrence(X91,X92)
& subactivity_occurrence(X92,X93) )
=> subactivity_occurrence(X91,X93) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_31) ).
tff(f_147,axiom,
! [X49,X50,X51] :
( min_precedes(X49,X50,X51)
=> ~ atomic(X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_19) ).
tff(f_120,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
tff(c_166,plain,
tptp3 != tptp2,
inference(cnfTransformation,[status(thm)],[f_328]) ).
tff(c_172,plain,
occurrence_of('#skF_19',tptp0),
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_231,plain,
! [X105_165] :
( occurrence_of('#skF_16'(X105_165),tptp3)
| ~ occurrence_of(X105_165,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_4,plain,
! [X0_1,X1_2] :
( activity(X0_1)
| ~ occurrence_of(X1_2,X0_1) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_238,plain,
! [X105_165] :
( activity(tptp3)
| ~ occurrence_of(X105_165,tptp0) ),
inference(resolution,[status(thm)],[c_231,c_4]) ).
tff(c_240,plain,
! [X105_165] : ~ occurrence_of(X105_165,tptp0),
inference(splitLeft,[status(thm)],[c_238]) ).
tff(c_242,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_240,c_172]) ).
tff(c_243,plain,
activity(tptp3),
inference(splitRight,[status(thm)],[c_238]) ).
tff(c_144,plain,
! [X105_118] :
( root_occ('#skF_16'(X105_118),X105_118)
| ~ occurrence_of(X105_118,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_124,plain,
! [X100_109,X99_108] :
( occurrence_of(X100_109,'#skF_14'(X99_108,X100_109))
| ~ root_occ(X99_108,X100_109) ),
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_381,plain,
! [X6_208,X5_209,X4_210] :
( ( X6_208 = X5_209 )
| ~ occurrence_of(X4_210,X6_208)
| ~ occurrence_of(X4_210,X5_209) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_397,plain,
! [X5_211] :
( ( tptp0 = X5_211 )
| ~ occurrence_of('#skF_19',X5_211) ),
inference(resolution,[status(thm)],[c_172,c_381]) ).
tff(c_441,plain,
! [X99_212] :
( ( '#skF_14'(X99_212,'#skF_19') = tptp0 )
| ~ root_occ(X99_212,'#skF_19') ),
inference(resolution,[status(thm)],[c_124,c_397]) ).
tff(c_445,plain,
( ( '#skF_14'('#skF_16'('#skF_19'),'#skF_19') = tptp0 )
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_144,c_441]) ).
tff(c_448,plain,
'#skF_14'('#skF_16'('#skF_19'),'#skF_19') = tptp0,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_445]) ).
tff(c_120,plain,
! [X99_108,X100_109] :
( root(X99_108,'#skF_14'(X99_108,X100_109))
| ~ root_occ(X99_108,X100_109) ),
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_458,plain,
( root('#skF_16'('#skF_19'),tptp0)
| ~ root_occ('#skF_16'('#skF_19'),'#skF_19') ),
inference(superposition,[status(thm),theory(equality)],[c_448,c_120]) ).
tff(c_595,plain,
~ root_occ('#skF_16'('#skF_19'),'#skF_19'),
inference(splitLeft,[status(thm)],[c_458]) ).
tff(c_598,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_144,c_595]) ).
tff(c_602,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_598]) ).
tff(c_603,plain,
root('#skF_16'('#skF_19'),tptp0),
inference(splitRight,[status(thm)],[c_458]) ).
tff(c_539,plain,
! [X29_227,X28_228] :
( atocc(X29_227,'#skF_4'(X28_228,X29_227))
| ~ root(X29_227,X28_228) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_490,plain,
! [X64_217,X65_218] :
( occurrence_of(X64_217,'#skF_9'(X64_217,X65_218))
| ~ atocc(X64_217,X65_218) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_2,plain,
! [X1_2,X0_1] :
( activity_occurrence(X1_2)
| ~ occurrence_of(X1_2,X0_1) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_514,plain,
! [X64_217,X65_218] :
( activity_occurrence(X64_217)
| ~ atocc(X64_217,X65_218) ),
inference(resolution,[status(thm)],[c_490,c_2]) ).
tff(c_548,plain,
! [X29_227,X28_228] :
( activity_occurrence(X29_227)
| ~ root(X29_227,X28_228) ),
inference(resolution,[status(thm)],[c_539,c_514]) ).
tff(c_635,plain,
activity_occurrence('#skF_16'('#skF_19')),
inference(resolution,[status(thm)],[c_603,c_548]) ).
tff(c_146,plain,
! [X105_118] :
( occurrence_of('#skF_16'(X105_118),tptp3)
| ~ occurrence_of(X105_118,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_661,plain,
! [X105_239] :
( next_subocc('#skF_16'(X105_239),'#skF_17'(X105_239),tptp0)
| ~ occurrence_of(X105_239,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_74,plain,
! [X60_65,X61_66,X62_67] :
( min_precedes(X60_65,X61_66,X62_67)
| ~ next_subocc(X60_65,X61_66,X62_67) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_886,plain,
! [X105_285] :
( min_precedes('#skF_16'(X105_285),'#skF_17'(X105_285),tptp0)
| ~ occurrence_of(X105_285,tptp0) ),
inference(resolution,[status(thm)],[c_661,c_74]) ).
tff(c_176,plain,
! [X111_125,X110_124] :
( ~ occurrence_of(X111_125,tptp2)
| ~ leaf_occ(X111_125,'#skF_19')
| ~ min_precedes(X110_124,X111_125,tptp0)
| ~ root_occ(X110_124,'#skF_19')
| ~ occurrence_of(X110_124,tptp3) ),
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_1078,plain,
! [X105_320] :
( ~ occurrence_of('#skF_17'(X105_320),tptp2)
| ~ leaf_occ('#skF_17'(X105_320),'#skF_19')
| ~ root_occ('#skF_16'(X105_320),'#skF_19')
| ~ occurrence_of('#skF_16'(X105_320),tptp3)
| ~ occurrence_of(X105_320,tptp0) ),
inference(resolution,[status(thm)],[c_886,c_176]) ).
tff(c_1085,plain,
( ~ occurrence_of('#skF_17'('#skF_19'),tptp2)
| ~ leaf_occ('#skF_17'('#skF_19'),'#skF_19')
| ~ occurrence_of('#skF_16'('#skF_19'),tptp3)
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_144,c_1078]) ).
tff(c_1091,plain,
( ~ occurrence_of('#skF_17'('#skF_19'),tptp2)
| ~ leaf_occ('#skF_17'('#skF_19'),'#skF_19')
| ~ occurrence_of('#skF_16'('#skF_19'),tptp3) ),
inference(demodulation,[status(thm),theory(equality)],[c_172,c_1085]) ).
tff(c_1202,plain,
~ occurrence_of('#skF_16'('#skF_19'),tptp3),
inference(splitLeft,[status(thm)],[c_1091]) ).
tff(c_1205,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_146,c_1202]) ).
tff(c_1209,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_1205]) ).
tff(c_1211,plain,
occurrence_of('#skF_16'('#skF_19'),tptp3),
inference(splitRight,[status(thm)],[c_1091]) ).
tff(c_6,plain,
! [X2_3] :
( occurrence_of(X2_3,'#skF_1'(X2_3))
| ~ activity_occurrence(X2_3) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_395,plain,
! [X5_209,X2_3] :
( ( X5_209 = '#skF_1'(X2_3) )
| ~ occurrence_of(X2_3,X5_209)
| ~ activity_occurrence(X2_3) ),
inference(resolution,[status(thm)],[c_6,c_381]) ).
tff(c_1217,plain,
( ( '#skF_1'('#skF_16'('#skF_19')) = tptp3 )
| ~ activity_occurrence('#skF_16'('#skF_19')) ),
inference(resolution,[status(thm)],[c_1211,c_395]) ).
tff(c_1238,plain,
'#skF_1'('#skF_16'('#skF_19')) = tptp3,
inference(demodulation,[status(thm),theory(equality)],[c_635,c_1217]) ).
tff(c_158,plain,
atomic(tptp3),
inference(cnfTransformation,[status(thm)],[f_320]) ).
tff(c_12,plain,
! [X7_8] :
( subactivity(X7_8,X7_8)
| ~ activity(X7_8) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_1739,plain,
! [X64_426,X65_427,X66_428] :
( atocc(X64_426,X65_427)
| ~ occurrence_of(X64_426,X66_428)
| ~ atomic(X66_428)
| ~ subactivity(X65_427,X66_428) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_3145,plain,
! [X2_597,X65_598] :
( atocc(X2_597,X65_598)
| ~ atomic('#skF_1'(X2_597))
| ~ subactivity(X65_598,'#skF_1'(X2_597))
| ~ activity_occurrence(X2_597) ),
inference(resolution,[status(thm)],[c_6,c_1739]) ).
tff(c_3599,plain,
! [X2_652] :
( atocc(X2_652,'#skF_1'(X2_652))
| ~ atomic('#skF_1'(X2_652))
| ~ activity_occurrence(X2_652)
| ~ activity('#skF_1'(X2_652)) ),
inference(resolution,[status(thm)],[c_12,c_3145]) ).
tff(c_82,plain,
! [X64_71,X65_72] :
( occurrence_of(X64_71,'#skF_9'(X64_71,X65_72))
| ~ atocc(X64_71,X65_72) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_10,plain,
! [X6_7,X5_6,X4_5] :
( ( X6_7 = X5_6 )
| ~ occurrence_of(X4_5,X6_7)
| ~ occurrence_of(X4_5,X5_6) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_1274,plain,
! [X5_348] :
( ( tptp3 = X5_348 )
| ~ occurrence_of('#skF_16'('#skF_19'),X5_348) ),
inference(resolution,[status(thm)],[c_1211,c_10]) ).
tff(c_1300,plain,
! [X65_72] :
( ( '#skF_9'('#skF_16'('#skF_19'),X65_72) = tptp3 )
| ~ atocc('#skF_16'('#skF_19'),X65_72) ),
inference(resolution,[status(thm)],[c_82,c_1274]) ).
tff(c_3620,plain,
( ( '#skF_9'('#skF_16'('#skF_19'),'#skF_1'('#skF_16'('#skF_19'))) = tptp3 )
| ~ atomic('#skF_1'('#skF_16'('#skF_19')))
| ~ activity_occurrence('#skF_16'('#skF_19'))
| ~ activity('#skF_1'('#skF_16'('#skF_19'))) ),
inference(resolution,[status(thm)],[c_3599,c_1300]) ).
tff(c_3654,plain,
'#skF_9'('#skF_16'('#skF_19'),tptp3) = tptp3,
inference(demodulation,[status(thm),theory(equality)],[c_243,c_1238,c_635,c_158,c_1238,c_1238,c_3620]) ).
tff(c_168,plain,
tptp3 != tptp1,
inference(cnfTransformation,[status(thm)],[f_330]) ).
tff(c_134,plain,
! [X105_118] :
( leaf_occ('#skF_18'(X105_118),X105_118)
| ~ occurrence_of(X105_118,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_465,plain,
! [X103_215,X102_216] :
( occurrence_of(X103_215,'#skF_15'(X102_216,X103_215))
| ~ leaf_occ(X102_216,X103_215) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_396,plain,
! [X5_209] :
( ( tptp0 = X5_209 )
| ~ occurrence_of('#skF_19',X5_209) ),
inference(resolution,[status(thm)],[c_172,c_381]) ).
tff(c_518,plain,
! [X102_225] :
( ( '#skF_15'(X102_225,'#skF_19') = tptp0 )
| ~ leaf_occ(X102_225,'#skF_19') ),
inference(resolution,[status(thm)],[c_465,c_396]) ).
tff(c_522,plain,
( ( '#skF_15'('#skF_18'('#skF_19'),'#skF_19') = tptp0 )
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_134,c_518]) ).
tff(c_525,plain,
'#skF_15'('#skF_18'('#skF_19'),'#skF_19') = tptp0,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_522]) ).
tff(c_559,plain,
! [X102_234,X103_235] :
( leaf(X102_234,'#skF_15'(X102_234,X103_235))
| ~ leaf_occ(X102_234,X103_235) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_562,plain,
( leaf('#skF_18'('#skF_19'),tptp0)
| ~ leaf_occ('#skF_18'('#skF_19'),'#skF_19') ),
inference(superposition,[status(thm),theory(equality)],[c_525,c_559]) ).
tff(c_666,plain,
~ leaf_occ('#skF_18'('#skF_19'),'#skF_19'),
inference(splitLeft,[status(thm)],[c_562]) ).
tff(c_669,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_134,c_666]) ).
tff(c_673,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_669]) ).
tff(c_675,plain,
leaf_occ('#skF_18'('#skF_19'),'#skF_19'),
inference(splitRight,[status(thm)],[c_562]) ).
tff(c_219,plain,
! [X102_157,X103_158] :
( subactivity_occurrence(X102_157,X103_158)
| ~ leaf_occ(X102_157,X103_158) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_90,plain,
! [X67_76,X68_77] :
( activity_occurrence(X67_76)
| ~ subactivity_occurrence(X67_76,X68_77) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_226,plain,
! [X102_157,X103_158] :
( activity_occurrence(X102_157)
| ~ leaf_occ(X102_157,X103_158) ),
inference(resolution,[status(thm)],[c_219,c_90]) ).
tff(c_690,plain,
activity_occurrence('#skF_18'('#skF_19')),
inference(resolution,[status(thm)],[c_675,c_226]) ).
tff(c_674,plain,
leaf('#skF_18'('#skF_19'),tptp0),
inference(splitRight,[status(thm)],[c_562]) ).
tff(c_2015,plain,
! [X56_444,X57_445] :
( min_precedes('#skF_7'(X56_444,X57_445),X56_444,X57_445)
| root(X56_444,X57_445)
| ~ leaf(X56_444,X57_445) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_1630,plain,
! [X31_404,X32_405,X33_406] :
( min_precedes('#skF_5'(X31_404,X32_405,X33_406),X32_405,X33_406)
| ~ min_precedes(X31_404,X32_405,X33_406) ),
inference(cnfTransformation,[status(thm)],[f_115]) ).
tff(c_52,plain,
! [X38_39,X39_40,X40_41] :
( precedes(X38_39,X39_40)
| ~ min_precedes(X38_39,X39_40,X40_41) ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_1678,plain,
! [X31_410,X32_411,X33_412] :
( precedes('#skF_5'(X31_410,X32_411,X33_412),X32_411)
| ~ min_precedes(X31_410,X32_411,X33_412) ),
inference(resolution,[status(thm)],[c_1630,c_52]) ).
tff(c_30,plain,
! [X22_23,X21_22] :
( legal(X22_23)
| ~ precedes(X21_22,X22_23) ),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_1686,plain,
! [X32_411,X31_410,X33_412] :
( legal(X32_411)
| ~ min_precedes(X31_410,X32_411,X33_412) ),
inference(resolution,[status(thm)],[c_1678,c_30]) ).
tff(c_2225,plain,
! [X56_473,X57_474] :
( legal(X56_473)
| root(X56_473,X57_474)
| ~ leaf(X56_473,X57_474) ),
inference(resolution,[status(thm)],[c_2015,c_1686]) ).
tff(c_54,plain,
! [X41_42,X42_43] :
( legal(X41_42)
| ~ root(X41_42,X42_43) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_2277,plain,
! [X56_481,X57_482] :
( legal(X56_481)
| ~ leaf(X56_481,X57_482) ),
inference(resolution,[status(thm)],[c_2225,c_54]) ).
tff(c_2284,plain,
legal('#skF_18'('#skF_19')),
inference(resolution,[status(thm)],[c_674,c_2277]) ).
tff(c_24,plain,
! [X18_19] :
( arboreal(X18_19)
| ~ legal(X18_19) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_2289,plain,
arboreal('#skF_18'('#skF_19')),
inference(resolution,[status(thm)],[c_2284,c_24]) ).
tff(c_8,plain,
! [X2_3] :
( activity('#skF_1'(X2_3))
| ~ activity_occurrence(X2_3) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_305,plain,
! [X17_186,X16_187] :
( atomic(X17_186)
| ~ arboreal(X16_187)
| ~ occurrence_of(X16_187,X17_186) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_322,plain,
! [X2_3] :
( atomic('#skF_1'(X2_3))
| ~ arboreal(X2_3)
| ~ activity_occurrence(X2_3) ),
inference(resolution,[status(thm)],[c_6,c_305]) ).
tff(c_3181,plain,
! [X2_597] :
( atocc(X2_597,'#skF_1'(X2_597))
| ~ atomic('#skF_1'(X2_597))
| ~ activity_occurrence(X2_597)
| ~ activity('#skF_1'(X2_597)) ),
inference(resolution,[status(thm)],[c_12,c_3145]) ).
tff(c_4017,plain,
! [X94_674,X95_675,X96_676,X97_677] :
( subactivity_occurrence('#skF_13'(X94_674,X95_675,X96_676,X97_677),X97_677)
| subactivity_occurrence(X96_676,X97_677)
| ~ subactivity(X94_674,X95_675)
| ~ occurrence_of(X97_677,X95_675)
| ~ occurrence_of(X96_676,X94_674) ),
inference(cnfTransformation,[status(thm)],[f_276]) ).
tff(c_114,plain,
! [X94_103,X95_104,X96_105,X97_106] :
( ~ subactivity_occurrence('#skF_13'(X94_103,X95_104,X96_105,X97_106),X96_105)
| subactivity_occurrence(X96_105,X97_106)
| ~ subactivity(X94_103,X95_104)
| ~ occurrence_of(X97_106,X95_104)
| ~ occurrence_of(X96_105,X94_103) ),
inference(cnfTransformation,[status(thm)],[f_276]) ).
tff(c_4046,plain,
! [X97_678,X94_679,X95_680] :
( subactivity_occurrence(X97_678,X97_678)
| ~ subactivity(X94_679,X95_680)
| ~ occurrence_of(X97_678,X95_680)
| ~ occurrence_of(X97_678,X94_679) ),
inference(resolution,[status(thm)],[c_4017,c_114]) ).
tff(c_4101,plain,
! [X97_682,X7_683] :
( subactivity_occurrence(X97_682,X97_682)
| ~ occurrence_of(X97_682,X7_683)
| ~ activity(X7_683) ),
inference(resolution,[status(thm)],[c_12,c_4046]) ).
tff(c_4199,plain,
! [X2_684] :
( subactivity_occurrence(X2_684,X2_684)
| ~ activity('#skF_1'(X2_684))
| ~ activity_occurrence(X2_684) ),
inference(resolution,[status(thm)],[c_6,c_4101]) ).
tff(c_4218,plain,
! [X2_3] :
( subactivity_occurrence(X2_3,X2_3)
| ~ activity_occurrence(X2_3) ),
inference(resolution,[status(thm)],[c_8,c_4199]) ).
tff(c_56,plain,
! [X43_44,X44_45] :
( root(X43_44,X44_45)
| ~ legal(X43_44)
| ~ atocc(X43_44,X44_45) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_2515,plain,
! [X99_504,X100_505,X101_506] :
( root_occ(X99_504,X100_505)
| ~ root(X99_504,X101_506)
| ~ subactivity_occurrence(X99_504,X100_505)
| ~ occurrence_of(X100_505,X101_506) ),
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_6195,plain,
! [X43_899,X100_900,X44_901] :
( root_occ(X43_899,X100_900)
| ~ subactivity_occurrence(X43_899,X100_900)
| ~ occurrence_of(X100_900,X44_901)
| ~ legal(X43_899)
| ~ atocc(X43_899,X44_901) ),
inference(resolution,[status(thm)],[c_56,c_2515]) ).
tff(c_7830,plain,
! [X2_949,X44_950] :
( root_occ(X2_949,X2_949)
| ~ occurrence_of(X2_949,X44_950)
| ~ legal(X2_949)
| ~ atocc(X2_949,X44_950)
| ~ activity_occurrence(X2_949) ),
inference(resolution,[status(thm)],[c_4218,c_6195]) ).
tff(c_7875,plain,
! [X2_951] :
( root_occ(X2_951,X2_951)
| ~ legal(X2_951)
| ~ atocc(X2_951,'#skF_1'(X2_951))
| ~ activity_occurrence(X2_951) ),
inference(resolution,[status(thm)],[c_6,c_7830]) ).
tff(c_8422,plain,
! [X2_988] :
( root_occ(X2_988,X2_988)
| ~ legal(X2_988)
| ~ atomic('#skF_1'(X2_988))
| ~ activity_occurrence(X2_988)
| ~ activity('#skF_1'(X2_988)) ),
inference(resolution,[status(thm)],[c_3181,c_7875]) ).
tff(c_8449,plain,
! [X2_989] :
( root_occ(X2_989,X2_989)
| ~ legal(X2_989)
| ~ activity('#skF_1'(X2_989))
| ~ arboreal(X2_989)
| ~ activity_occurrence(X2_989) ),
inference(resolution,[status(thm)],[c_322,c_8422]) ).
tff(c_8469,plain,
! [X2_3] :
( root_occ(X2_3,X2_3)
| ~ legal(X2_3)
| ~ arboreal(X2_3)
| ~ activity_occurrence(X2_3) ),
inference(resolution,[status(thm)],[c_8,c_8449]) ).
tff(c_8471,plain,
! [X2_993] :
( root_occ(X2_993,X2_993)
| ~ legal(X2_993)
| ~ arboreal(X2_993)
| ~ activity_occurrence(X2_993) ),
inference(resolution,[status(thm)],[c_8,c_8449]) ).
tff(c_563,plain,
! [X5_236,X2_237] :
( ( X5_236 = '#skF_1'(X2_237) )
| ~ occurrence_of(X2_237,X5_236)
| ~ activity_occurrence(X2_237) ),
inference(resolution,[status(thm)],[c_6,c_381]) ).
tff(c_587,plain,
! [X99_108,X100_109] :
( ( '#skF_14'(X99_108,X100_109) = '#skF_1'(X100_109) )
| ~ activity_occurrence(X100_109)
| ~ root_occ(X99_108,X100_109) ),
inference(resolution,[status(thm)],[c_124,c_563]) ).
tff(c_8735,plain,
! [X2_995] :
( ( '#skF_14'(X2_995,X2_995) = '#skF_1'(X2_995) )
| ~ legal(X2_995)
| ~ arboreal(X2_995)
| ~ activity_occurrence(X2_995) ),
inference(resolution,[status(thm)],[c_8471,c_587]) ).
tff(c_8743,plain,
( ( '#skF_14'('#skF_18'('#skF_19'),'#skF_18'('#skF_19')) = '#skF_1'('#skF_18'('#skF_19')) )
| ~ arboreal('#skF_18'('#skF_19'))
| ~ activity_occurrence('#skF_18'('#skF_19')) ),
inference(resolution,[status(thm)],[c_2284,c_8735]) ).
tff(c_8761,plain,
'#skF_14'('#skF_18'('#skF_19'),'#skF_18'('#skF_19')) = '#skF_1'('#skF_18'('#skF_19')),
inference(demodulation,[status(thm),theory(equality)],[c_690,c_2289,c_8743]) ).
tff(c_358,plain,
! [X100_202,X99_203] :
( occurrence_of(X100_202,'#skF_14'(X99_203,X100_202))
| ~ root_occ(X99_203,X100_202) ),
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_22,plain,
! [X17_18,X16_17] :
( atomic(X17_18)
| ~ arboreal(X16_17)
| ~ occurrence_of(X16_17,X17_18) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_371,plain,
! [X99_203,X100_202] :
( atomic('#skF_14'(X99_203,X100_202))
| ~ arboreal(X100_202)
| ~ root_occ(X99_203,X100_202) ),
inference(resolution,[status(thm)],[c_358,c_22]) ).
tff(c_8788,plain,
( atomic('#skF_1'('#skF_18'('#skF_19')))
| ~ arboreal('#skF_18'('#skF_19'))
| ~ root_occ('#skF_18'('#skF_19'),'#skF_18'('#skF_19')) ),
inference(superposition,[status(thm),theory(equality)],[c_8761,c_371]) ).
tff(c_8806,plain,
( atomic('#skF_1'('#skF_18'('#skF_19')))
| ~ root_occ('#skF_18'('#skF_19'),'#skF_18'('#skF_19')) ),
inference(demodulation,[status(thm),theory(equality)],[c_2289,c_8788]) ).
tff(c_8824,plain,
~ root_occ('#skF_18'('#skF_19'),'#skF_18'('#skF_19')),
inference(splitLeft,[status(thm)],[c_8806]) ).
tff(c_8827,plain,
( ~ legal('#skF_18'('#skF_19'))
| ~ arboreal('#skF_18'('#skF_19'))
| ~ activity_occurrence('#skF_18'('#skF_19')) ),
inference(resolution,[status(thm)],[c_8469,c_8824]) ).
tff(c_8831,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_690,c_2289,c_2284,c_8827]) ).
tff(c_8833,plain,
root_occ('#skF_18'('#skF_19'),'#skF_18'('#skF_19')),
inference(splitRight,[status(thm)],[c_8806]) ).
tff(c_8794,plain,
( occurrence_of('#skF_18'('#skF_19'),'#skF_1'('#skF_18'('#skF_19')))
| ~ root_occ('#skF_18'('#skF_19'),'#skF_18'('#skF_19')) ),
inference(superposition,[status(thm),theory(equality)],[c_8761,c_124]) ).
tff(c_9391,plain,
occurrence_of('#skF_18'('#skF_19'),'#skF_1'('#skF_18'('#skF_19'))),
inference(demodulation,[status(thm),theory(equality)],[c_8833,c_8794]) ).
tff(c_1928,plain,
! [X105_440] :
( occurrence_of('#skF_18'(X105_440),tptp1)
| occurrence_of('#skF_18'(X105_440),tptp2)
| ~ occurrence_of(X105_440,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_1961,plain,
! [X5_6,X105_440] :
( ( tptp2 = X5_6 )
| ~ occurrence_of('#skF_18'(X105_440),X5_6)
| occurrence_of('#skF_18'(X105_440),tptp1)
| ~ occurrence_of(X105_440,tptp0) ),
inference(resolution,[status(thm)],[c_1928,c_10]) ).
tff(c_9418,plain,
( ( '#skF_1'('#skF_18'('#skF_19')) = tptp2 )
| occurrence_of('#skF_18'('#skF_19'),tptp1)
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_9391,c_1961]) ).
tff(c_9471,plain,
( ( '#skF_1'('#skF_18'('#skF_19')) = tptp2 )
| occurrence_of('#skF_18'('#skF_19'),tptp1) ),
inference(demodulation,[status(thm),theory(equality)],[c_172,c_9418]) ).
tff(c_9575,plain,
occurrence_of('#skF_18'('#skF_19'),tptp1),
inference(splitLeft,[status(thm)],[c_9471]) ).
tff(c_636,plain,
legal('#skF_16'('#skF_19')),
inference(resolution,[status(thm)],[c_603,c_54]) ).
tff(c_640,plain,
arboreal('#skF_16'('#skF_19')),
inference(resolution,[status(thm)],[c_636,c_24]) ).
tff(c_604,plain,
root_occ('#skF_16'('#skF_19'),'#skF_19'),
inference(splitRight,[status(thm)],[c_458]) ).
tff(c_130,plain,
! [X102_113,X103_114] :
( subactivity_occurrence(X102_113,X103_114)
| ~ leaf_occ(X102_113,X103_114) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_122,plain,
! [X99_108,X100_109] :
( subactivity_occurrence(X99_108,X100_109)
| ~ root_occ(X99_108,X100_109) ),
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_4312,plain,
! [X82_688,X81_689,X79_690,X80_691] :
( ( X82_688 = X81_689 )
| min_precedes(X82_688,X81_689,X79_690)
| min_precedes(X81_689,X82_688,X79_690)
| ~ subactivity_occurrence(X82_688,X80_691)
| ~ subactivity_occurrence(X81_689,X80_691)
| ~ arboreal(X82_688)
| ~ arboreal(X81_689)
| ~ occurrence_of(X80_691,X79_690) ),
inference(cnfTransformation,[status(thm)],[f_236]) ).
tff(c_16594,plain,
! [X99_1289,X81_1290,X79_1291,X100_1292] :
( ( X99_1289 = X81_1290 )
| min_precedes(X99_1289,X81_1290,X79_1291)
| min_precedes(X81_1290,X99_1289,X79_1291)
| ~ subactivity_occurrence(X81_1290,X100_1292)
| ~ arboreal(X99_1289)
| ~ arboreal(X81_1290)
| ~ occurrence_of(X100_1292,X79_1291)
| ~ root_occ(X99_1289,X100_1292) ),
inference(resolution,[status(thm)],[c_122,c_4312]) ).
tff(c_110272,plain,
! [X99_3755,X102_3756,X79_3757,X103_3758] :
( ( X99_3755 = X102_3756 )
| min_precedes(X99_3755,X102_3756,X79_3757)
| min_precedes(X102_3756,X99_3755,X79_3757)
| ~ arboreal(X99_3755)
| ~ arboreal(X102_3756)
| ~ occurrence_of(X103_3758,X79_3757)
| ~ root_occ(X99_3755,X103_3758)
| ~ leaf_occ(X102_3756,X103_3758) ),
inference(resolution,[status(thm)],[c_130,c_16594]) ).
tff(c_110697,plain,
! [X99_3765,X102_3766] :
( ( X99_3765 = X102_3766 )
| min_precedes(X99_3765,X102_3766,tptp0)
| min_precedes(X102_3766,X99_3765,tptp0)
| ~ arboreal(X99_3765)
| ~ arboreal(X102_3766)
| ~ root_occ(X99_3765,'#skF_19')
| ~ leaf_occ(X102_3766,'#skF_19') ),
inference(resolution,[status(thm)],[c_172,c_110272]) ).
tff(c_64,plain,
! [X56_57,X59_64,X57_58] :
( ~ min_precedes(X56_57,X59_64,X57_58)
| ~ leaf(X56_57,X57_58) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_124425,plain,
! [X102_3921,X99_3922] :
( ~ leaf(X102_3921,tptp0)
| ( X99_3922 = X102_3921 )
| min_precedes(X99_3922,X102_3921,tptp0)
| ~ arboreal(X99_3922)
| ~ arboreal(X102_3921)
| ~ root_occ(X99_3922,'#skF_19')
| ~ leaf_occ(X102_3921,'#skF_19') ),
inference(resolution,[status(thm)],[c_110697,c_64]) ).
tff(c_174,plain,
! [X111_125,X110_124] :
( ~ occurrence_of(X111_125,tptp1)
| ~ leaf_occ(X111_125,'#skF_19')
| ~ min_precedes(X110_124,X111_125,tptp0)
| ~ root_occ(X110_124,'#skF_19')
| ~ occurrence_of(X110_124,tptp3) ),
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_133271,plain,
! [X102_3999,X99_4000] :
( ~ occurrence_of(X102_3999,tptp1)
| ~ occurrence_of(X99_4000,tptp3)
| ~ leaf(X102_3999,tptp0)
| ( X99_4000 = X102_3999 )
| ~ arboreal(X99_4000)
| ~ arboreal(X102_3999)
| ~ root_occ(X99_4000,'#skF_19')
| ~ leaf_occ(X102_3999,'#skF_19') ),
inference(resolution,[status(thm)],[c_124425,c_174]) ).
tff(c_133277,plain,
! [X99_4000] :
( ~ occurrence_of(X99_4000,tptp3)
| ~ leaf('#skF_18'('#skF_19'),tptp0)
| ( X99_4000 = '#skF_18'('#skF_19') )
| ~ arboreal(X99_4000)
| ~ arboreal('#skF_18'('#skF_19'))
| ~ root_occ(X99_4000,'#skF_19')
| ~ leaf_occ('#skF_18'('#skF_19'),'#skF_19') ),
inference(resolution,[status(thm)],[c_9575,c_133271]) ).
tff(c_133295,plain,
! [X99_4001] :
( ~ occurrence_of(X99_4001,tptp3)
| ( X99_4001 = '#skF_18'('#skF_19') )
| ~ arboreal(X99_4001)
| ~ root_occ(X99_4001,'#skF_19') ),
inference(demodulation,[status(thm),theory(equality)],[c_675,c_2289,c_674,c_133277]) ).
tff(c_133409,plain,
( ~ occurrence_of('#skF_16'('#skF_19'),tptp3)
| ( '#skF_16'('#skF_19') = '#skF_18'('#skF_19') )
| ~ arboreal('#skF_16'('#skF_19')) ),
inference(resolution,[status(thm)],[c_604,c_133295]) ).
tff(c_133479,plain,
'#skF_16'('#skF_19') = '#skF_18'('#skF_19'),
inference(demodulation,[status(thm),theory(equality)],[c_640,c_1211,c_133409]) ).
tff(c_3642,plain,
( atocc('#skF_16'('#skF_19'),tptp3)
| ~ atomic('#skF_1'('#skF_16'('#skF_19')))
| ~ activity_occurrence('#skF_16'('#skF_19'))
| ~ activity('#skF_1'('#skF_16'('#skF_19'))) ),
inference(superposition,[status(thm),theory(equality)],[c_1238,c_3599]) ).
tff(c_3662,plain,
atocc('#skF_16'('#skF_19'),tptp3),
inference(demodulation,[status(thm),theory(equality)],[c_243,c_1238,c_635,c_158,c_1238,c_3642]) ).
tff(c_4107,plain,
( subactivity_occurrence('#skF_16'('#skF_19'),'#skF_16'('#skF_19'))
| ~ activity(tptp3) ),
inference(resolution,[status(thm)],[c_1211,c_4101]) ).
tff(c_4130,plain,
subactivity_occurrence('#skF_16'('#skF_19'),'#skF_16'('#skF_19')),
inference(demodulation,[status(thm),theory(equality)],[c_243,c_4107]) ).
tff(c_6237,plain,
! [X44_901] :
( root_occ('#skF_16'('#skF_19'),'#skF_16'('#skF_19'))
| ~ occurrence_of('#skF_16'('#skF_19'),X44_901)
| ~ legal('#skF_16'('#skF_19'))
| ~ atocc('#skF_16'('#skF_19'),X44_901) ),
inference(resolution,[status(thm)],[c_4130,c_6195]) ).
tff(c_6288,plain,
! [X44_901] :
( root_occ('#skF_16'('#skF_19'),'#skF_16'('#skF_19'))
| ~ occurrence_of('#skF_16'('#skF_19'),X44_901)
| ~ atocc('#skF_16'('#skF_19'),X44_901) ),
inference(demodulation,[status(thm),theory(equality)],[c_636,c_6237]) ).
tff(c_6384,plain,
! [X44_909] :
( ~ occurrence_of('#skF_16'('#skF_19'),X44_909)
| ~ atocc('#skF_16'('#skF_19'),X44_909) ),
inference(splitLeft,[status(thm)],[c_6288]) ).
tff(c_6387,plain,
~ atocc('#skF_16'('#skF_19'),tptp3),
inference(resolution,[status(thm)],[c_1211,c_6384]) ).
tff(c_6411,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3662,c_6387]) ).
tff(c_6412,plain,
root_occ('#skF_16'('#skF_19'),'#skF_16'('#skF_19')),
inference(splitRight,[status(thm)],[c_6288]) ).
tff(c_1302,plain,
! [X99_108] :
( ( '#skF_14'(X99_108,'#skF_16'('#skF_19')) = tptp3 )
| ~ root_occ(X99_108,'#skF_16'('#skF_19')) ),
inference(resolution,[status(thm)],[c_124,c_1274]) ).
tff(c_6475,plain,
'#skF_14'('#skF_16'('#skF_19'),'#skF_16'('#skF_19')) = tptp3,
inference(resolution,[status(thm)],[c_6412,c_1302]) ).
tff(c_2536,plain,
! [X99_108,X100_505,X100_109] :
( root_occ(X99_108,X100_505)
| ~ subactivity_occurrence(X99_108,X100_505)
| ~ occurrence_of(X100_505,'#skF_14'(X99_108,X100_109))
| ~ root_occ(X99_108,X100_109) ),
inference(resolution,[status(thm)],[c_120,c_2515]) ).
tff(c_6622,plain,
! [X100_505] :
( root_occ('#skF_16'('#skF_19'),X100_505)
| ~ subactivity_occurrence('#skF_16'('#skF_19'),X100_505)
| ~ occurrence_of(X100_505,tptp3)
| ~ root_occ('#skF_16'('#skF_19'),'#skF_16'('#skF_19')) ),
inference(superposition,[status(thm),theory(equality)],[c_6475,c_2536]) ).
tff(c_6934,plain,
! [X100_921] :
( root_occ('#skF_16'('#skF_19'),X100_921)
| ~ subactivity_occurrence('#skF_16'('#skF_19'),X100_921)
| ~ occurrence_of(X100_921,tptp3) ),
inference(demodulation,[status(thm),theory(equality)],[c_6412,c_6622]) ).
tff(c_7026,plain,
! [X103_114] :
( root_occ('#skF_16'('#skF_19'),X103_114)
| ~ occurrence_of(X103_114,tptp3)
| ~ leaf_occ('#skF_16'('#skF_19'),X103_114) ),
inference(resolution,[status(thm)],[c_130,c_6934]) ).
tff(c_392,plain,
! [X5_209,X99_108,X100_109] :
( ( X5_209 = '#skF_14'(X99_108,X100_109) )
| ~ occurrence_of(X100_109,X5_209)
| ~ root_occ(X99_108,X100_109) ),
inference(resolution,[status(thm)],[c_124,c_381]) ).
tff(c_10415,plain,
! [X99_1060] :
( ( '#skF_14'(X99_1060,'#skF_18'('#skF_19')) = tptp1 )
| ~ root_occ(X99_1060,'#skF_18'('#skF_19')) ),
inference(resolution,[status(thm)],[c_9575,c_392]) ).
tff(c_10440,plain,
( ( '#skF_14'('#skF_16'('#skF_19'),'#skF_18'('#skF_19')) = tptp1 )
| ~ occurrence_of('#skF_18'('#skF_19'),tptp3)
| ~ leaf_occ('#skF_16'('#skF_19'),'#skF_18'('#skF_19')) ),
inference(resolution,[status(thm)],[c_7026,c_10415]) ).
tff(c_39260,plain,
~ leaf_occ('#skF_16'('#skF_19'),'#skF_18'('#skF_19')),
inference(splitLeft,[status(thm)],[c_10440]) ).
tff(c_154,plain,
atomic(tptp2),
inference(cnfTransformation,[status(thm)],[f_318]) ).
tff(c_80,plain,
! [X64_71,X65_72,X66_75] :
( atocc(X64_71,X65_72)
| ~ occurrence_of(X64_71,X66_75)
| ~ atomic(X66_75)
| ~ subactivity(X65_72,X66_75) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_1930,plain,
! [X105_440,X65_72] :
( atocc('#skF_18'(X105_440),X65_72)
| ~ atomic(tptp2)
| ~ subactivity(X65_72,tptp2)
| occurrence_of('#skF_18'(X105_440),tptp1)
| ~ occurrence_of(X105_440,tptp0) ),
inference(resolution,[status(thm)],[c_1928,c_80]) ).
tff(c_6487,plain,
! [X105_910,X65_911] :
( atocc('#skF_18'(X105_910),X65_911)
| ~ subactivity(X65_911,tptp2)
| occurrence_of('#skF_18'(X105_910),tptp1)
| ~ occurrence_of(X105_910,tptp0) ),
inference(demodulation,[status(thm),theory(equality)],[c_154,c_1930]) ).
tff(c_6575,plain,
! [X105_910,X65_911] :
( activity(tptp1)
| atocc('#skF_18'(X105_910),X65_911)
| ~ subactivity(X65_911,tptp2)
| ~ occurrence_of(X105_910,tptp0) ),
inference(resolution,[status(thm)],[c_6487,c_4]) ).
tff(c_7499,plain,
activity(tptp1),
inference(splitLeft,[status(thm)],[c_6575]) ).
tff(c_715,plain,
! [X91_245,X93_246,X92_247] :
( subactivity_occurrence(X91_245,X93_246)
| ~ subactivity_occurrence(X92_247,X93_246)
| ~ subactivity_occurrence(X91_245,X92_247) ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_721,plain,
! [X91_245,X100_109,X99_108] :
( subactivity_occurrence(X91_245,X100_109)
| ~ subactivity_occurrence(X91_245,X99_108)
| ~ root_occ(X99_108,X100_109) ),
inference(resolution,[status(thm)],[c_122,c_715]) ).
tff(c_88004,plain,
! [X95_3434,X100_3431,X96_3433,X97_3430,X94_3432] :
( subactivity_occurrence('#skF_13'(X94_3432,X95_3434,X96_3433,X97_3430),X100_3431)
| ~ root_occ(X97_3430,X100_3431)
| subactivity_occurrence(X96_3433,X97_3430)
| ~ subactivity(X94_3432,X95_3434)
| ~ occurrence_of(X97_3430,X95_3434)
| ~ occurrence_of(X96_3433,X94_3432) ),
inference(resolution,[status(thm)],[c_4017,c_721]) ).
tff(c_88204,plain,
! [X97_3435,X100_3436,X94_3437,X95_3438] :
( ~ root_occ(X97_3435,X100_3436)
| subactivity_occurrence(X100_3436,X97_3435)
| ~ subactivity(X94_3437,X95_3438)
| ~ occurrence_of(X97_3435,X95_3438)
| ~ occurrence_of(X100_3436,X94_3437) ),
inference(resolution,[status(thm)],[c_88004,c_114]) ).
tff(c_91286,plain,
! [X97_3472,X100_3473,X7_3474] :
( ~ root_occ(X97_3472,X100_3473)
| subactivity_occurrence(X100_3473,X97_3472)
| ~ occurrence_of(X97_3472,X7_3474)
| ~ occurrence_of(X100_3473,X7_3474)
| ~ activity(X7_3474) ),
inference(resolution,[status(thm)],[c_12,c_88204]) ).
tff(c_91320,plain,
! [X100_3473] :
( ~ root_occ('#skF_18'('#skF_19'),X100_3473)
| subactivity_occurrence(X100_3473,'#skF_18'('#skF_19'))
| ~ occurrence_of(X100_3473,tptp1)
| ~ activity(tptp1) ),
inference(resolution,[status(thm)],[c_9575,c_91286]) ).
tff(c_91588,plain,
! [X100_3476] :
( ~ root_occ('#skF_18'('#skF_19'),X100_3476)
| subactivity_occurrence(X100_3476,'#skF_18'('#skF_19'))
| ~ occurrence_of(X100_3476,tptp1) ),
inference(demodulation,[status(thm),theory(equality)],[c_7499,c_91320]) ).
tff(c_2342,plain,
! [X56_491,X57_492] :
( ~ root(X56_491,X57_492)
| leaf(X56_491,X57_492)
| min_precedes(X56_491,'#skF_6'(X56_491,X57_492),X57_492) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_60,plain,
! [X51_52,X49_50,X50_51] :
( ~ atomic(X51_52)
| ~ min_precedes(X49_50,X50_51,X51_52) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_2396,plain,
! [X57_493,X56_494] :
( ~ atomic(X57_493)
| ~ root(X56_494,X57_493)
| leaf(X56_494,X57_493) ),
inference(resolution,[status(thm)],[c_2342,c_60]) ).
tff(c_2424,plain,
! [X99_108,X100_109] :
( ~ atomic('#skF_14'(X99_108,X100_109))
| leaf(X99_108,'#skF_14'(X99_108,X100_109))
| ~ root_occ(X99_108,X100_109) ),
inference(resolution,[status(thm)],[c_120,c_2396]) ).
tff(c_6625,plain,
( ~ atomic('#skF_14'('#skF_16'('#skF_19'),'#skF_16'('#skF_19')))
| leaf('#skF_16'('#skF_19'),tptp3)
| ~ root_occ('#skF_16'('#skF_19'),'#skF_16'('#skF_19')) ),
inference(superposition,[status(thm),theory(equality)],[c_6475,c_2424]) ).
tff(c_6646,plain,
leaf('#skF_16'('#skF_19'),tptp3),
inference(demodulation,[status(thm),theory(equality)],[c_6412,c_158,c_6475,c_6625]) ).
tff(c_126,plain,
! [X102_113,X103_114,X104_117] :
( leaf_occ(X102_113,X103_114)
| ~ leaf(X102_113,X104_117)
| ~ subactivity_occurrence(X102_113,X103_114)
| ~ occurrence_of(X103_114,X104_117) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_6725,plain,
! [X103_114] :
( leaf_occ('#skF_16'('#skF_19'),X103_114)
| ~ subactivity_occurrence('#skF_16'('#skF_19'),X103_114)
| ~ occurrence_of(X103_114,tptp3) ),
inference(resolution,[status(thm)],[c_6646,c_126]) ).
tff(c_91658,plain,
( leaf_occ('#skF_16'('#skF_19'),'#skF_18'('#skF_19'))
| ~ occurrence_of('#skF_18'('#skF_19'),tptp3)
| ~ root_occ('#skF_18'('#skF_19'),'#skF_16'('#skF_19'))
| ~ occurrence_of('#skF_16'('#skF_19'),tptp1) ),
inference(resolution,[status(thm)],[c_91588,c_6725]) ).
tff(c_91728,plain,
( ~ occurrence_of('#skF_18'('#skF_19'),tptp3)
| ~ root_occ('#skF_18'('#skF_19'),'#skF_16'('#skF_19'))
| ~ occurrence_of('#skF_16'('#skF_19'),tptp1) ),
inference(negUnitSimplification,[status(thm)],[c_39260,c_91658]) ).
tff(c_91944,plain,
~ occurrence_of('#skF_16'('#skF_19'),tptp1),
inference(splitLeft,[status(thm)],[c_91728]) ).
tff(c_133519,plain,
~ occurrence_of('#skF_18'('#skF_19'),tptp1),
inference(demodulation,[status(thm),theory(equality)],[c_133479,c_91944]) ).
tff(c_133677,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9575,c_133519]) ).
tff(c_133679,plain,
occurrence_of('#skF_16'('#skF_19'),tptp1),
inference(splitRight,[status(thm)],[c_91728]) ).
tff(c_239,plain,
! [X105_165] :
( activity_occurrence('#skF_16'(X105_165))
| ~ occurrence_of(X105_165,tptp0) ),
inference(resolution,[status(thm)],[c_231,c_2]) ).
tff(c_244,plain,
! [X16_166,X17_167] :
( arboreal(X16_166)
| ~ atomic(X17_167)
| ~ occurrence_of(X16_166,X17_167) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_247,plain,
! [X105_118] :
( arboreal('#skF_16'(X105_118))
| ~ atomic(tptp3)
| ~ occurrence_of(X105_118,tptp0) ),
inference(resolution,[status(thm)],[c_146,c_244]) ).
tff(c_256,plain,
! [X105_118] :
( arboreal('#skF_16'(X105_118))
| ~ occurrence_of(X105_118,tptp0) ),
inference(demodulation,[status(thm),theory(equality)],[c_158,c_247]) ).
tff(c_971,plain,
! [X5_301,X105_302] :
( ( tptp3 = X5_301 )
| ~ occurrence_of('#skF_16'(X105_302),X5_301)
| ~ occurrence_of(X105_302,tptp0) ),
inference(resolution,[status(thm)],[c_146,c_381]) ).
tff(c_1917,plain,
! [X105_439] :
( ( '#skF_1'('#skF_16'(X105_439)) = tptp3 )
| ~ occurrence_of(X105_439,tptp0)
| ~ activity_occurrence('#skF_16'(X105_439)) ),
inference(resolution,[status(thm)],[c_6,c_971]) ).
tff(c_1927,plain,
! [X105_165] :
( ( '#skF_1'('#skF_16'(X105_165)) = tptp3 )
| ~ occurrence_of(X105_165,tptp0) ),
inference(resolution,[status(thm)],[c_239,c_1917]) ).
tff(c_585,plain,
! [X64_71,X65_72] :
( ( '#skF_9'(X64_71,X65_72) = '#skF_1'(X64_71) )
| ~ activity_occurrence(X64_71)
| ~ atocc(X64_71,X65_72) ),
inference(resolution,[status(thm)],[c_82,c_563]) ).
tff(c_20347,plain,
! [X2_1443] :
( ( '#skF_9'(X2_1443,'#skF_1'(X2_1443)) = '#skF_1'(X2_1443) )
| ~ atomic('#skF_1'(X2_1443))
| ~ activity_occurrence(X2_1443)
| ~ activity('#skF_1'(X2_1443)) ),
inference(resolution,[status(thm)],[c_3599,c_585]) ).
tff(c_20389,plain,
! [X2_1444] :
( ( '#skF_9'(X2_1444,'#skF_1'(X2_1444)) = '#skF_1'(X2_1444) )
| ~ activity('#skF_1'(X2_1444))
| ~ arboreal(X2_1444)
| ~ activity_occurrence(X2_1444) ),
inference(resolution,[status(thm)],[c_322,c_20347]) ).
tff(c_20419,plain,
! [X2_1445] :
( ( '#skF_9'(X2_1445,'#skF_1'(X2_1445)) = '#skF_1'(X2_1445) )
| ~ arboreal(X2_1445)
| ~ activity_occurrence(X2_1445) ),
inference(resolution,[status(thm)],[c_8,c_20389]) ).
tff(c_74731,plain,
! [X105_3143] :
( ( '#skF_1'('#skF_16'(X105_3143)) = '#skF_9'('#skF_16'(X105_3143),tptp3) )
| ~ arboreal('#skF_16'(X105_3143))
| ~ activity_occurrence('#skF_16'(X105_3143))
| ~ occurrence_of(X105_3143,tptp0) ),
inference(superposition,[status(thm),theory(equality)],[c_1927,c_20419]) ).
tff(c_74763,plain,
! [X105_3148] :
( ( '#skF_1'('#skF_16'(X105_3148)) = '#skF_9'('#skF_16'(X105_3148),tptp3) )
| ~ activity_occurrence('#skF_16'(X105_3148))
| ~ occurrence_of(X105_3148,tptp0) ),
inference(resolution,[status(thm)],[c_256,c_74731]) ).
tff(c_74774,plain,
! [X105_3149] :
( ( '#skF_1'('#skF_16'(X105_3149)) = '#skF_9'('#skF_16'(X105_3149),tptp3) )
| ~ occurrence_of(X105_3149,tptp0) ),
inference(resolution,[status(thm)],[c_239,c_74763]) ).
tff(c_1755,plain,
! [X105_118,X65_427] :
( atocc('#skF_16'(X105_118),X65_427)
| ~ atomic(tptp3)
| ~ subactivity(X65_427,tptp3)
| ~ occurrence_of(X105_118,tptp0) ),
inference(resolution,[status(thm)],[c_146,c_1739]) ).
tff(c_1773,plain,
! [X105_118,X65_427] :
( atocc('#skF_16'(X105_118),X65_427)
| ~ subactivity(X65_427,tptp3)
| ~ occurrence_of(X105_118,tptp0) ),
inference(demodulation,[status(thm),theory(equality)],[c_158,c_1755]) ).
tff(c_1876,plain,
! [X105_435,X65_436] :
( atocc('#skF_16'(X105_435),X65_436)
| ~ subactivity(X65_436,tptp3)
| ~ occurrence_of(X105_435,tptp0) ),
inference(demodulation,[status(thm),theory(equality)],[c_158,c_1755]) ).
tff(c_52300,plain,
! [X105_2503,X65_2504] :
( ( '#skF_9'('#skF_16'(X105_2503),X65_2504) = '#skF_1'('#skF_16'(X105_2503)) )
| ~ activity_occurrence('#skF_16'(X105_2503))
| ~ subactivity(X65_2504,tptp3)
| ~ occurrence_of(X105_2503,tptp0) ),
inference(resolution,[status(thm)],[c_1876,c_585]) ).
tff(c_52309,plain,
! [X105_2505,X65_2506] :
( ( '#skF_9'('#skF_16'(X105_2505),X65_2506) = '#skF_1'('#skF_16'(X105_2505)) )
| ~ subactivity(X65_2506,tptp3)
| ~ occurrence_of(X105_2505,tptp0) ),
inference(resolution,[status(thm)],[c_239,c_52300]) ).
tff(c_58544,plain,
! [X105_2745,X65_2746] :
( occurrence_of('#skF_16'(X105_2745),'#skF_1'('#skF_16'(X105_2745)))
| ~ atocc('#skF_16'(X105_2745),X65_2746)
| ~ subactivity(X65_2746,tptp3)
| ~ occurrence_of(X105_2745,tptp0) ),
inference(superposition,[status(thm),theory(equality)],[c_52309,c_82]) ).
tff(c_58588,plain,
! [X105_118,X65_427] :
( occurrence_of('#skF_16'(X105_118),'#skF_1'('#skF_16'(X105_118)))
| ~ subactivity(X65_427,tptp3)
| ~ occurrence_of(X105_118,tptp0) ),
inference(resolution,[status(thm)],[c_1773,c_58544]) ).
tff(c_58595,plain,
! [X65_427] : ~ subactivity(X65_427,tptp3),
inference(splitLeft,[status(thm)],[c_58588]) ).
tff(c_86,plain,
! [X65_72,X64_71] :
( subactivity(X65_72,'#skF_9'(X64_71,X65_72))
| ~ atocc(X64_71,X65_72) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_3789,plain,
( subactivity(tptp3,tptp3)
| ~ atocc('#skF_16'('#skF_19'),tptp3) ),
inference(superposition,[status(thm),theory(equality)],[c_3654,c_86]) ).
tff(c_3810,plain,
subactivity(tptp3,tptp3),
inference(demodulation,[status(thm),theory(equality)],[c_3662,c_3789]) ).
tff(c_58633,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58595,c_3810]) ).
tff(c_58634,plain,
! [X105_118] :
( occurrence_of('#skF_16'(X105_118),'#skF_1'('#skF_16'(X105_118)))
| ~ occurrence_of(X105_118,tptp0) ),
inference(splitRight,[status(thm)],[c_58588]) ).
tff(c_75883,plain,
! [X105_3163] :
( occurrence_of('#skF_16'(X105_3163),'#skF_9'('#skF_16'(X105_3163),tptp3))
| ~ occurrence_of(X105_3163,tptp0)
| ~ occurrence_of(X105_3163,tptp0) ),
inference(superposition,[status(thm),theory(equality)],[c_74774,c_58634]) ).
tff(c_76173,plain,
! [X5_6,X105_3163] :
( ( X5_6 = '#skF_9'('#skF_16'(X105_3163),tptp3) )
| ~ occurrence_of('#skF_16'(X105_3163),X5_6)
| ~ occurrence_of(X105_3163,tptp0) ),
inference(resolution,[status(thm)],[c_75883,c_10]) ).
tff(c_133697,plain,
( ( '#skF_9'('#skF_16'('#skF_19'),tptp3) = tptp1 )
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_133679,c_76173]) ).
tff(c_133887,plain,
tptp3 = tptp1,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_3654,c_133697]) ).
tff(c_133889,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_168,c_133887]) ).
tff(c_133890,plain,
'#skF_1'('#skF_18'('#skF_19')) = tptp2,
inference(splitRight,[status(thm)],[c_9471]) ).
tff(c_133893,plain,
occurrence_of('#skF_18'('#skF_19'),tptp2),
inference(demodulation,[status(thm),theory(equality)],[c_133890,c_9391]) ).
tff(c_140591,plain,
! [X81_4237,X102_4238,X79_4239,X103_4240] :
( ( X81_4237 = X102_4238 )
| min_precedes(X102_4238,X81_4237,X79_4239)
| min_precedes(X81_4237,X102_4238,X79_4239)
| ~ subactivity_occurrence(X81_4237,X103_4240)
| ~ arboreal(X102_4238)
| ~ arboreal(X81_4237)
| ~ occurrence_of(X103_4240,X79_4239)
| ~ leaf_occ(X102_4238,X103_4240) ),
inference(resolution,[status(thm)],[c_130,c_4312]) ).
tff(c_250363,plain,
! [X99_6956,X102_6957,X79_6958,X100_6959] :
( ( X99_6956 = X102_6957 )
| min_precedes(X102_6957,X99_6956,X79_6958)
| min_precedes(X99_6956,X102_6957,X79_6958)
| ~ arboreal(X102_6957)
| ~ arboreal(X99_6956)
| ~ occurrence_of(X100_6959,X79_6958)
| ~ leaf_occ(X102_6957,X100_6959)
| ~ root_occ(X99_6956,X100_6959) ),
inference(resolution,[status(thm)],[c_122,c_140591]) ).
tff(c_250627,plain,
! [X99_6966,X102_6967] :
( ( X99_6966 = X102_6967 )
| min_precedes(X102_6967,X99_6966,tptp0)
| min_precedes(X99_6966,X102_6967,tptp0)
| ~ arboreal(X102_6967)
| ~ arboreal(X99_6966)
| ~ leaf_occ(X102_6967,'#skF_19')
| ~ root_occ(X99_6966,'#skF_19') ),
inference(resolution,[status(thm)],[c_172,c_250363]) ).
tff(c_50,plain,
! [X36_37,X37_38,X35_36] :
( ~ root(X36_37,X37_38)
| ~ min_precedes(X35_36,X36_37,X37_38) ),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_263699,plain,
! [X99_7077,X102_7078] :
( ~ root(X99_7077,tptp0)
| ( X99_7077 = X102_7078 )
| min_precedes(X99_7077,X102_7078,tptp0)
| ~ arboreal(X102_7078)
| ~ arboreal(X99_7077)
| ~ leaf_occ(X102_7078,'#skF_19')
| ~ root_occ(X99_7077,'#skF_19') ),
inference(resolution,[status(thm)],[c_250627,c_50]) ).
tff(c_266874,plain,
! [X102_7112,X99_7113] :
( ~ occurrence_of(X102_7112,tptp2)
| ~ occurrence_of(X99_7113,tptp3)
| ~ root(X99_7113,tptp0)
| ( X99_7113 = X102_7112 )
| ~ arboreal(X102_7112)
| ~ arboreal(X99_7113)
| ~ leaf_occ(X102_7112,'#skF_19')
| ~ root_occ(X99_7113,'#skF_19') ),
inference(resolution,[status(thm)],[c_263699,c_176]) ).
tff(c_266878,plain,
! [X99_7113] :
( ~ occurrence_of(X99_7113,tptp3)
| ~ root(X99_7113,tptp0)
| ( X99_7113 = '#skF_18'('#skF_19') )
| ~ arboreal('#skF_18'('#skF_19'))
| ~ arboreal(X99_7113)
| ~ leaf_occ('#skF_18'('#skF_19'),'#skF_19')
| ~ root_occ(X99_7113,'#skF_19') ),
inference(resolution,[status(thm)],[c_133893,c_266874]) ).
tff(c_269725,plain,
! [X99_7129] :
( ~ occurrence_of(X99_7129,tptp3)
| ~ root(X99_7129,tptp0)
| ( X99_7129 = '#skF_18'('#skF_19') )
| ~ arboreal(X99_7129)
| ~ root_occ(X99_7129,'#skF_19') ),
inference(demodulation,[status(thm),theory(equality)],[c_675,c_2289,c_266878]) ).
tff(c_269847,plain,
( ~ occurrence_of('#skF_16'('#skF_19'),tptp3)
| ~ root('#skF_16'('#skF_19'),tptp0)
| ( '#skF_16'('#skF_19') = '#skF_18'('#skF_19') )
| ~ arboreal('#skF_16'('#skF_19')) ),
inference(resolution,[status(thm)],[c_604,c_269725]) ).
tff(c_269923,plain,
'#skF_16'('#skF_19') = '#skF_18'('#skF_19'),
inference(demodulation,[status(thm),theory(equality)],[c_640,c_603,c_1211,c_269847]) ).
tff(c_1967,plain,
! [X105_440] :
( activity(tptp2)
| occurrence_of('#skF_18'(X105_440),tptp1)
| ~ occurrence_of(X105_440,tptp0) ),
inference(resolution,[status(thm)],[c_1928,c_4]) ).
tff(c_2006,plain,
activity(tptp2),
inference(splitLeft,[status(thm)],[c_1967]) ).
tff(c_133932,plain,
( atocc('#skF_18'('#skF_19'),tptp2)
| ~ atomic('#skF_1'('#skF_18'('#skF_19')))
| ~ activity_occurrence('#skF_18'('#skF_19'))
| ~ activity('#skF_1'('#skF_18'('#skF_19'))) ),
inference(superposition,[status(thm),theory(equality)],[c_133890,c_3181]) ).
tff(c_133971,plain,
atocc('#skF_18'('#skF_19'),tptp2),
inference(demodulation,[status(thm),theory(equality)],[c_2006,c_133890,c_690,c_154,c_133890,c_133932]) ).
tff(c_134219,plain,
( ( '#skF_1'('#skF_18'('#skF_19')) = '#skF_9'('#skF_18'('#skF_19'),tptp2) )
| ~ activity_occurrence('#skF_18'('#skF_19')) ),
inference(resolution,[status(thm)],[c_133971,c_585]) ).
tff(c_134240,plain,
'#skF_9'('#skF_18'('#skF_19'),tptp2) = tptp2,
inference(demodulation,[status(thm),theory(equality)],[c_690,c_133890,c_134219]) ).
tff(c_134260,plain,
( subactivity(tptp2,tptp2)
| ~ atocc('#skF_18'('#skF_19'),tptp2) ),
inference(superposition,[status(thm),theory(equality)],[c_134240,c_86]) ).
tff(c_134273,plain,
subactivity(tptp2,tptp2),
inference(demodulation,[status(thm),theory(equality)],[c_133971,c_134260]) ).
tff(c_720,plain,
! [X91_245,X103_114,X102_113] :
( subactivity_occurrence(X91_245,X103_114)
| ~ subactivity_occurrence(X91_245,X102_113)
| ~ leaf_occ(X102_113,X103_114) ),
inference(resolution,[status(thm)],[c_130,c_715]) ).
tff(c_218881,plain,
! [X97_6538,X95_6542,X103_6539,X96_6541,X94_6540] :
( subactivity_occurrence('#skF_13'(X94_6540,X95_6542,X96_6541,X97_6538),X103_6539)
| ~ leaf_occ(X97_6538,X103_6539)
| subactivity_occurrence(X96_6541,X97_6538)
| ~ subactivity(X94_6540,X95_6542)
| ~ occurrence_of(X97_6538,X95_6542)
| ~ occurrence_of(X96_6541,X94_6540) ),
inference(resolution,[status(thm)],[c_4017,c_720]) ).
tff(c_219081,plain,
! [X97_6543,X103_6544,X94_6545,X95_6546] :
( ~ leaf_occ(X97_6543,X103_6544)
| subactivity_occurrence(X103_6544,X97_6543)
| ~ subactivity(X94_6545,X95_6546)
| ~ occurrence_of(X97_6543,X95_6546)
| ~ occurrence_of(X103_6544,X94_6545) ),
inference(resolution,[status(thm)],[c_218881,c_114]) ).
tff(c_220585,plain,
! [X97_6564,X103_6565] :
( ~ leaf_occ(X97_6564,X103_6565)
| subactivity_occurrence(X103_6565,X97_6564)
| ~ occurrence_of(X97_6564,tptp2)
| ~ occurrence_of(X103_6565,tptp2) ),
inference(resolution,[status(thm)],[c_134273,c_219081]) ).
tff(c_723,plain,
! [X91_251,X100_252,X99_253] :
( subactivity_occurrence(X91_251,X100_252)
| ~ subactivity_occurrence(X91_251,X99_253)
| ~ root_occ(X99_253,X100_252) ),
inference(resolution,[status(thm)],[c_122,c_715]) ).
tff(c_1105,plain,
! [X99_325,X100_326,X100_327] :
( subactivity_occurrence(X99_325,X100_326)
| ~ root_occ(X100_327,X100_326)
| ~ root_occ(X99_325,X100_327) ),
inference(resolution,[status(thm)],[c_122,c_723]) ).
tff(c_1111,plain,
! [X99_325,X105_118] :
( subactivity_occurrence(X99_325,X105_118)
| ~ root_occ(X99_325,'#skF_16'(X105_118))
| ~ occurrence_of(X105_118,tptp0) ),
inference(resolution,[status(thm)],[c_144,c_1105]) ).
tff(c_6430,plain,
( subactivity_occurrence('#skF_16'('#skF_19'),'#skF_19')
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_6412,c_1111]) ).
tff(c_6471,plain,
subactivity_occurrence('#skF_16'('#skF_19'),'#skF_19'),
inference(demodulation,[status(thm),theory(equality)],[c_172,c_6430]) ).
tff(c_112,plain,
! [X91_100,X93_102,X92_101] :
( subactivity_occurrence(X91_100,X93_102)
| ~ subactivity_occurrence(X92_101,X93_102)
| ~ subactivity_occurrence(X91_100,X92_101) ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_6613,plain,
! [X91_100] :
( subactivity_occurrence(X91_100,'#skF_19')
| ~ subactivity_occurrence(X91_100,'#skF_16'('#skF_19')) ),
inference(resolution,[status(thm)],[c_6471,c_112]) ).
tff(c_220859,plain,
! [X103_6565] :
( subactivity_occurrence(X103_6565,'#skF_19')
| ~ leaf_occ('#skF_16'('#skF_19'),X103_6565)
| ~ occurrence_of('#skF_16'('#skF_19'),tptp2)
| ~ occurrence_of(X103_6565,tptp2) ),
inference(resolution,[status(thm)],[c_220585,c_6613]) ).
tff(c_225824,plain,
~ occurrence_of('#skF_16'('#skF_19'),tptp2),
inference(splitLeft,[status(thm)],[c_220859]) ).
tff(c_269957,plain,
~ occurrence_of('#skF_18'('#skF_19'),tptp2),
inference(demodulation,[status(thm),theory(equality)],[c_269923,c_225824]) ).
tff(c_270137,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_133893,c_269957]) ).
tff(c_270139,plain,
occurrence_of('#skF_16'('#skF_19'),tptp2),
inference(splitRight,[status(thm)],[c_220859]) ).
tff(c_145191,plain,
! [X2_4428] :
( ( '#skF_9'(X2_4428,'#skF_1'(X2_4428)) = '#skF_1'(X2_4428) )
| ~ atomic('#skF_1'(X2_4428))
| ~ activity_occurrence(X2_4428)
| ~ activity('#skF_1'(X2_4428)) ),
inference(resolution,[status(thm)],[c_3599,c_585]) ).
tff(c_145656,plain,
! [X2_4433] :
( ( '#skF_9'(X2_4433,'#skF_1'(X2_4433)) = '#skF_1'(X2_4433) )
| ~ activity('#skF_1'(X2_4433))
| ~ arboreal(X2_4433)
| ~ activity_occurrence(X2_4433) ),
inference(resolution,[status(thm)],[c_322,c_145191]) ).
tff(c_145690,plain,
! [X2_4434] :
( ( '#skF_9'(X2_4434,'#skF_1'(X2_4434)) = '#skF_1'(X2_4434) )
| ~ arboreal(X2_4434)
| ~ activity_occurrence(X2_4434) ),
inference(resolution,[status(thm)],[c_8,c_145656]) ).
tff(c_196581,plain,
! [X105_6054] :
( ( '#skF_1'('#skF_16'(X105_6054)) = '#skF_9'('#skF_16'(X105_6054),tptp3) )
| ~ arboreal('#skF_16'(X105_6054))
| ~ activity_occurrence('#skF_16'(X105_6054))
| ~ occurrence_of(X105_6054,tptp0) ),
inference(superposition,[status(thm),theory(equality)],[c_1927,c_145690]) ).
tff(c_196680,plain,
! [X105_6060] :
( ( '#skF_1'('#skF_16'(X105_6060)) = '#skF_9'('#skF_16'(X105_6060),tptp3) )
| ~ activity_occurrence('#skF_16'(X105_6060))
| ~ occurrence_of(X105_6060,tptp0) ),
inference(resolution,[status(thm)],[c_256,c_196581]) ).
tff(c_196691,plain,
! [X105_6061] :
( ( '#skF_1'('#skF_16'(X105_6061)) = '#skF_9'('#skF_16'(X105_6061),tptp3) )
| ~ occurrence_of(X105_6061,tptp0) ),
inference(resolution,[status(thm)],[c_239,c_196680]) ).
tff(c_177055,plain,
! [X105_5478,X65_5479] :
( ( '#skF_9'('#skF_16'(X105_5478),X65_5479) = '#skF_1'('#skF_16'(X105_5478)) )
| ~ activity_occurrence('#skF_16'(X105_5478))
| ~ subactivity(X65_5479,tptp3)
| ~ occurrence_of(X105_5478,tptp0) ),
inference(resolution,[status(thm)],[c_1876,c_585]) ).
tff(c_177085,plain,
! [X105_5484,X65_5485] :
( ( '#skF_9'('#skF_16'(X105_5484),X65_5485) = '#skF_1'('#skF_16'(X105_5484)) )
| ~ subactivity(X65_5485,tptp3)
| ~ occurrence_of(X105_5484,tptp0) ),
inference(resolution,[status(thm)],[c_239,c_177055]) ).
tff(c_186775,plain,
! [X105_5803,X65_5804] :
( occurrence_of('#skF_16'(X105_5803),'#skF_1'('#skF_16'(X105_5803)))
| ~ atocc('#skF_16'(X105_5803),X65_5804)
| ~ subactivity(X65_5804,tptp3)
| ~ occurrence_of(X105_5803,tptp0) ),
inference(superposition,[status(thm),theory(equality)],[c_177085,c_82]) ).
tff(c_186827,plain,
! [X105_118,X65_427] :
( occurrence_of('#skF_16'(X105_118),'#skF_1'('#skF_16'(X105_118)))
| ~ subactivity(X65_427,tptp3)
| ~ occurrence_of(X105_118,tptp0) ),
inference(resolution,[status(thm)],[c_1773,c_186775]) ).
tff(c_186855,plain,
! [X65_427] : ~ subactivity(X65_427,tptp3),
inference(splitLeft,[status(thm)],[c_186827]) ).
tff(c_186869,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_186855,c_3810]) ).
tff(c_186870,plain,
! [X105_118] :
( occurrence_of('#skF_16'(X105_118),'#skF_1'('#skF_16'(X105_118)))
| ~ occurrence_of(X105_118,tptp0) ),
inference(splitRight,[status(thm)],[c_186827]) ).
tff(c_197430,plain,
! [X105_6070] :
( occurrence_of('#skF_16'(X105_6070),'#skF_9'('#skF_16'(X105_6070),tptp3))
| ~ occurrence_of(X105_6070,tptp0)
| ~ occurrence_of(X105_6070,tptp0) ),
inference(superposition,[status(thm),theory(equality)],[c_196691,c_186870]) ).
tff(c_197720,plain,
! [X5_6,X105_6070] :
( ( X5_6 = '#skF_9'('#skF_16'(X105_6070),tptp3) )
| ~ occurrence_of('#skF_16'(X105_6070),X5_6)
| ~ occurrence_of(X105_6070,tptp0) ),
inference(resolution,[status(thm)],[c_197430,c_10]) ).
tff(c_270165,plain,
( ( '#skF_9'('#skF_16'('#skF_19'),tptp3) = tptp2 )
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_270139,c_197720]) ).
tff(c_270363,plain,
tptp3 = tptp2,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_3654,c_270165]) ).
tff(c_270365,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_166,c_270363]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO009+1 : TPTP v9.0.0. Released v4.0.0.
% 0.03/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.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 16:57:14 EDT 2025
% 0.12/0.34 % CPUTime :
% 82.92/65.02 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 82.92/65.06
% 82.92/65.06 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------