%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS144+1 : TPTP v9.0.0. Released v3.1.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 : n028.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 07:07:26 PM UTC 2025
% Result : Theorem 6.04s 2.41s
% Output : CNFRefutation 6.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 4
% Syntax : Number of formulae : 643 ( 220 unt; 0 typ; 0 def)
% Number of atoms : 2064 ( 494 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 2358 ( 937 ~;1400 |; 14 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-1 aty)
% Number of variables : 472 ( 468 !; 4 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rp > xsd_string > xsd_integer > cowlThing > cowlNothing > cc > #nlpp > #skF_2 > #skF_11 > #skF_1 > #skF_7 > #skF_10 > #skF_5 > #skF_6 > #skF_3 > #skF_9 > #skF_8 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff(cc,type,
cc: $i > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_9',type,
'#skF_9': $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(rp,type,
rp: ( $i * $i ) > $o ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(f_82,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
tff(f_76,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
tff(f_149,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( cc(X)
=> ! [Y0,Y1,Y2] :
( ( rp(X,Y0)
& rp(X,Y1)
& rp(X,Y2) )
=> ( ( Y0 = Y1 )
| ( Y0 = Y2 )
| ( Y1 = Y2 ) ) ) )
& ! [X] :
( cc(X)
=> ? [Y0,Y1] :
( rp(X,Y0)
& rp(X,Y1)
& ( Y0 != Y1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
tff(f_106,axiom,
! [X] :
( cc(X)
=> ( ? [Y0,Y1] :
( rp(X,Y0)
& rp(X,Y1)
& ( Y0 != Y1 ) )
& ! [Y0,Y1,Y2] :
( ( rp(X,Y0)
& rp(X,Y1)
& rp(X,Y2) )
=> ( ( Y0 = Y1 )
| ( Y0 = Y2 )
| ( Y1 = Y2 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
tff(c_22,plain,
! [X_18] :
( xsd_string(X_18)
| xsd_integer(X_18) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_16,plain,
! [X_17] : cowlThing(X_17),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_18,plain,
! [X_17] : ~ cowlNothing(X_17),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_88,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_196,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_88]) ).
tff(c_306,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_196]) ).
tff(c_322,plain,
'#skF_10' != '#skF_9',
inference(splitLeft,[status(thm)],[c_306]) ).
tff(c_96,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_146,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_96]) ).
tff(c_208,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_146]) ).
tff(c_324,plain,
'#skF_10' != '#skF_8',
inference(splitLeft,[status(thm)],[c_208]) ).
tff(c_108,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_148,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_108]) ).
tff(c_212,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_148]) ).
tff(c_323,plain,
'#skF_9' != '#skF_8',
inference(splitLeft,[status(thm)],[c_212]) ).
tff(c_138,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_167,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_138]) ).
tff(c_250,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_167]) ).
tff(c_325,plain,
~ xsd_integer('#skF_5'),
inference(splitLeft,[status(thm)],[c_250]) ).
tff(c_140,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_143,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_140]) ).
tff(c_202,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_143]) ).
tff(c_326,plain,
~ xsd_string('#skF_5'),
inference(splitLeft,[status(thm)],[c_202]) ).
tff(c_329,plain,
xsd_integer('#skF_5'),
inference(resolution,[status(thm)],[c_22,c_326]) ).
tff(c_333,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_325,c_329]) ).
tff(c_334,plain,
( cc('#skF_11')
| cc('#skF_7')
| xsd_string('#skF_6') ),
inference(splitRight,[status(thm)],[c_202]) ).
tff(c_340,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_334]) ).
tff(c_20,plain,
! [X_18] :
( ~ xsd_integer(X_18)
| ~ xsd_string(X_18) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_344,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_340,c_20]) ).
tff(c_335,plain,
xsd_string('#skF_5'),
inference(splitRight,[status(thm)],[c_202]) ).
tff(c_136,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_144,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_136]) ).
tff(c_204,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_144]) ).
tff(c_350,plain,
( xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_204]) ).
tff(c_351,plain,
( cc('#skF_7')
| cc('#skF_11') ),
inference(negUnitSimplification,[status(thm)],[c_344,c_350]) ).
tff(c_352,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_351]) ).
tff(c_26,plain,
! [X_19] :
( ( '#skF_2'(X_19) != '#skF_1'(X_19) )
| ~ cc(X_19) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_357,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_352,c_26]) ).
tff(c_28,plain,
! [X_19] :
( rp(X_19,'#skF_2'(X_19))
| ~ cc(X_19) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_30,plain,
! [X_19] :
( rp(X_19,'#skF_1'(X_19))
| ~ cc(X_19) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_72,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_173,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_72]) ).
tff(c_262,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_173]) ).
tff(c_420,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_262]) ).
tff(c_421,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_344,c_420]) ).
tff(c_422,plain,
rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_421]) ).
tff(c_56,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_181,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_56]) ).
tff(c_278,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_181]) ).
tff(c_430,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_278]) ).
tff(c_431,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_344,c_430]) ).
tff(c_432,plain,
rp('#skF_7','#skF_10'),
inference(splitLeft,[status(thm)],[c_431]) ).
tff(c_80,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_169,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_80]) ).
tff(c_254,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_169]) ).
tff(c_396,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_254]) ).
tff(c_397,plain,
! [Y1_34,Y0_33] :
( cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_344,c_396]) ).
tff(c_398,plain,
cc('#skF_7'),
inference(splitLeft,[status(thm)],[c_397]) ).
tff(c_64,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_177,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_64]) ).
tff(c_270,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_177]) ).
tff(c_438,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_270]) ).
tff(c_439,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_344,c_438]) ).
tff(c_440,plain,
rp('#skF_7','#skF_9'),
inference(splitLeft,[status(thm)],[c_439]) ).
tff(c_444,plain,
! [Y2_42,Y1_43,Y0_44,X_45] :
( ( Y2_42 = Y1_43 )
| ( Y2_42 = Y0_44 )
| ( Y1_43 = Y0_44 )
| ~ rp(X_45,Y2_42)
| ~ rp(X_45,Y1_43)
| ~ rp(X_45,Y0_44)
| ~ cc(X_45) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_446,plain,
! [Y1_43,Y0_44] :
( ( Y1_43 = '#skF_9' )
| ( Y0_44 = '#skF_9' )
| ( Y1_43 = Y0_44 )
| ~ rp('#skF_7',Y1_43)
| ~ rp('#skF_7',Y0_44)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_440,c_444]) ).
tff(c_466,plain,
! [Y1_46,Y0_47] :
( ( Y1_46 = '#skF_9' )
| ( Y0_47 = '#skF_9' )
| ( Y1_46 = Y0_47 )
| ~ rp('#skF_7',Y1_46)
| ~ rp('#skF_7',Y0_47) ),
inference(demodulation,[status(thm),theory(equality)],[c_398,c_446]) ).
tff(c_470,plain,
! [Y0_47] :
( ( '#skF_10' = '#skF_9' )
| ( Y0_47 = '#skF_9' )
| ( Y0_47 = '#skF_10' )
| ~ rp('#skF_7',Y0_47) ),
inference(resolution,[status(thm)],[c_432,c_466]) ).
tff(c_493,plain,
! [Y0_48] :
( ( Y0_48 = '#skF_9' )
| ( Y0_48 = '#skF_10' )
| ~ rp('#skF_7',Y0_48) ),
inference(negUnitSimplification,[status(thm)],[c_322,c_470]) ).
tff(c_502,plain,
( ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_422,c_493]) ).
tff(c_522,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_324,c_323,c_502]) ).
tff(c_525,plain,
! [Y1_49,Y0_50] :
( ( Y1_49 = Y0_50 )
| ~ rp('#skF_11',Y1_49)
| ~ rp('#skF_11',Y0_50) ),
inference(splitRight,[status(thm)],[c_439]) ).
tff(c_528,plain,
! [Y0_50] :
( ( Y0_50 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_50)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_525]) ).
tff(c_538,plain,
! [Y0_51] :
( ( Y0_51 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_51) ),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_528]) ).
tff(c_546,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_538]) ).
tff(c_553,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_546]) ).
tff(c_555,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_357,c_553]) ).
tff(c_558,plain,
! [Y1_52,Y0_53] :
( ( Y1_52 = Y0_53 )
| ~ rp('#skF_11',Y1_52)
| ~ rp('#skF_11',Y0_53) ),
inference(splitRight,[status(thm)],[c_431]) ).
tff(c_561,plain,
! [Y0_53] :
( ( Y0_53 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_53)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_558]) ).
tff(c_571,plain,
! [Y0_54] :
( ( Y0_54 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_54) ),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_561]) ).
tff(c_579,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_571]) ).
tff(c_586,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_579]) ).
tff(c_588,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_357,c_586]) ).
tff(c_592,plain,
! [Y1_55,Y0_56] :
( ( Y1_55 = Y0_56 )
| ~ rp('#skF_11',Y1_55)
| ~ rp('#skF_11',Y0_56) ),
inference(splitRight,[status(thm)],[c_421]) ).
tff(c_595,plain,
! [Y0_56] :
( ( Y0_56 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_56)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_592]) ).
tff(c_605,plain,
! [Y0_57] :
( ( Y0_57 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_57) ),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_595]) ).
tff(c_613,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_605]) ).
tff(c_620,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_613]) ).
tff(c_622,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_357,c_620]) ).
tff(c_625,plain,
! [Y1_58,Y0_59] :
( ( Y1_58 = Y0_59 )
| ~ rp('#skF_11',Y1_58)
| ~ rp('#skF_11',Y0_59) ),
inference(splitRight,[status(thm)],[c_397]) ).
tff(c_628,plain,
! [Y0_59] :
( ( Y0_59 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_59)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_625]) ).
tff(c_638,plain,
! [Y0_60] :
( ( Y0_60 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_60) ),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_628]) ).
tff(c_646,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_638]) ).
tff(c_653,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_352,c_646]) ).
tff(c_655,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_357,c_653]) ).
tff(c_657,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_351]) ).
tff(c_120,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_162,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_120]) ).
tff(c_240,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_162]) ).
tff(c_669,plain,
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_240]) ).
tff(c_670,plain,
rp('#skF_7','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_657,c_344,c_669]) ).
tff(c_112,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_154,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_112]) ).
tff(c_224,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_154]) ).
tff(c_684,plain,
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_224]) ).
tff(c_685,plain,
rp('#skF_7','#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_657,c_344,c_684]) ).
tff(c_656,plain,
cc('#skF_7'),
inference(splitRight,[status(thm)],[c_351]) ).
tff(c_128,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_155,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_128]) ).
tff(c_226,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_155]) ).
tff(c_687,plain,
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_226]) ).
tff(c_688,plain,
rp('#skF_7','#skF_8'),
inference(negUnitSimplification,[status(thm)],[c_657,c_344,c_687]) ).
tff(c_749,plain,
! [Y2_61,Y1_62,Y0_63,X_64] :
( ( Y2_61 = Y1_62 )
| ( Y2_61 = Y0_63 )
| ( Y1_62 = Y0_63 )
| ~ rp(X_64,Y2_61)
| ~ rp(X_64,Y1_62)
| ~ rp(X_64,Y0_63)
| ~ cc(X_64) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_751,plain,
! [Y1_62,Y0_63] :
( ( Y1_62 = '#skF_8' )
| ( Y0_63 = '#skF_8' )
| ( Y1_62 = Y0_63 )
| ~ rp('#skF_7',Y1_62)
| ~ rp('#skF_7',Y0_63)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_688,c_749]) ).
tff(c_771,plain,
! [Y1_65,Y0_66] :
( ( Y1_65 = '#skF_8' )
| ( Y0_66 = '#skF_8' )
| ( Y1_65 = Y0_66 )
| ~ rp('#skF_7',Y1_65)
| ~ rp('#skF_7',Y0_66) ),
inference(demodulation,[status(thm),theory(equality)],[c_656,c_751]) ).
tff(c_775,plain,
! [Y0_66] :
( ( '#skF_10' = '#skF_8' )
| ( Y0_66 = '#skF_8' )
| ( Y0_66 = '#skF_10' )
| ~ rp('#skF_7',Y0_66) ),
inference(resolution,[status(thm)],[c_685,c_771]) ).
tff(c_798,plain,
! [Y0_67] :
( ( Y0_67 = '#skF_8' )
| ( Y0_67 = '#skF_10' )
| ~ rp('#skF_7',Y0_67) ),
inference(negUnitSimplification,[status(thm)],[c_324,c_775]) ).
tff(c_807,plain,
( ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_9' ) ),
inference(resolution,[status(thm)],[c_670,c_798]) ).
tff(c_827,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_322,c_323,c_807]) ).
tff(c_828,plain,
( cc('#skF_7')
| cc('#skF_11') ),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_834,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_828]) ).
tff(c_838,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_834,c_26]) ).
tff(c_829,plain,
~ xsd_string('#skF_6'),
inference(splitRight,[status(thm)],[c_334]) ).
tff(c_68,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_175,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_68]) ).
tff(c_266,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_175]) ).
tff(c_920,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_266]) ).
tff(c_921,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_829,c_920]) ).
tff(c_922,plain,
rp('#skF_7','#skF_9'),
inference(splitLeft,[status(thm)],[c_921]) ).
tff(c_60,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_179,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_60]) ).
tff(c_274,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_179]) ).
tff(c_924,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_274]) ).
tff(c_925,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_829,c_924]) ).
tff(c_926,plain,
rp('#skF_7','#skF_10'),
inference(splitLeft,[status(thm)],[c_925]) ).
tff(c_84,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_197,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_84]) ).
tff(c_308,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_197]) ).
tff(c_895,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_308]) ).
tff(c_896,plain,
! [Y1_34,Y0_33] :
( cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_829,c_895]) ).
tff(c_897,plain,
cc('#skF_7'),
inference(splitLeft,[status(thm)],[c_896]) ).
tff(c_76,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_171,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_76]) ).
tff(c_258,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_171]) ).
tff(c_930,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_258]) ).
tff(c_931,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_829,c_930]) ).
tff(c_932,plain,
rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_931]) ).
tff(c_934,plain,
! [Y2_68,Y1_69,Y0_70,X_71] :
( ( Y2_68 = Y1_69 )
| ( Y2_68 = Y0_70 )
| ( Y1_69 = Y0_70 )
| ~ rp(X_71,Y2_68)
| ~ rp(X_71,Y1_69)
| ~ rp(X_71,Y0_70)
| ~ cc(X_71) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_936,plain,
! [Y1_69,Y0_70] :
( ( Y1_69 = '#skF_8' )
| ( Y0_70 = '#skF_8' )
| ( Y1_69 = Y0_70 )
| ~ rp('#skF_7',Y1_69)
| ~ rp('#skF_7',Y0_70)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_932,c_934]) ).
tff(c_956,plain,
! [Y1_72,Y0_73] :
( ( Y1_72 = '#skF_8' )
| ( Y0_73 = '#skF_8' )
| ( Y1_72 = Y0_73 )
| ~ rp('#skF_7',Y1_72)
| ~ rp('#skF_7',Y0_73) ),
inference(demodulation,[status(thm),theory(equality)],[c_897,c_936]) ).
tff(c_960,plain,
! [Y0_73] :
( ( '#skF_10' = '#skF_8' )
| ( Y0_73 = '#skF_8' )
| ( Y0_73 = '#skF_10' )
| ~ rp('#skF_7',Y0_73) ),
inference(resolution,[status(thm)],[c_926,c_956]) ).
tff(c_983,plain,
! [Y0_74] :
( ( Y0_74 = '#skF_8' )
| ( Y0_74 = '#skF_10' )
| ~ rp('#skF_7',Y0_74) ),
inference(negUnitSimplification,[status(thm)],[c_324,c_960]) ).
tff(c_992,plain,
( ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_9' ) ),
inference(resolution,[status(thm)],[c_922,c_983]) ).
tff(c_1012,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_322,c_323,c_992]) ).
tff(c_1015,plain,
! [Y1_75,Y0_76] :
( ( Y1_75 = Y0_76 )
| ~ rp('#skF_11',Y1_75)
| ~ rp('#skF_11',Y0_76) ),
inference(splitRight,[status(thm)],[c_931]) ).
tff(c_1018,plain,
! [Y0_76] :
( ( Y0_76 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_76)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1015]) ).
tff(c_1028,plain,
! [Y0_77] :
( ( Y0_77 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_77) ),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1018]) ).
tff(c_1036,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1028]) ).
tff(c_1043,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1036]) ).
tff(c_1045,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_838,c_1043]) ).
tff(c_1048,plain,
! [Y1_78,Y0_79] :
( ( Y1_78 = Y0_79 )
| ~ rp('#skF_11',Y1_78)
| ~ rp('#skF_11',Y0_79) ),
inference(splitRight,[status(thm)],[c_925]) ).
tff(c_1051,plain,
! [Y0_79] :
( ( Y0_79 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_79)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1048]) ).
tff(c_1064,plain,
! [Y0_80] :
( ( Y0_80 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_80) ),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1051]) ).
tff(c_1072,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1064]) ).
tff(c_1079,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1072]) ).
tff(c_1081,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_838,c_1079]) ).
tff(c_1084,plain,
! [Y1_81,Y0_82] :
( ( Y1_81 = Y0_82 )
| ~ rp('#skF_11',Y1_81)
| ~ rp('#skF_11',Y0_82) ),
inference(splitRight,[status(thm)],[c_921]) ).
tff(c_1087,plain,
! [Y0_82] :
( ( Y0_82 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_82)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1084]) ).
tff(c_1097,plain,
! [Y0_83] :
( ( Y0_83 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_83) ),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1087]) ).
tff(c_1105,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1097]) ).
tff(c_1112,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1105]) ).
tff(c_1114,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_838,c_1112]) ).
tff(c_1117,plain,
! [Y1_84,Y0_85] :
( ( Y1_84 = Y0_85 )
| ~ rp('#skF_11',Y1_84)
| ~ rp('#skF_11',Y0_85) ),
inference(splitRight,[status(thm)],[c_896]) ).
tff(c_1120,plain,
! [Y0_85] :
( ( Y0_85 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_85)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1117]) ).
tff(c_1130,plain,
! [Y0_86] :
( ( Y0_86 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_86) ),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1120]) ).
tff(c_1138,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1130]) ).
tff(c_1145,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_834,c_1138]) ).
tff(c_1147,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_838,c_1145]) ).
tff(c_1149,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_828]) ).
tff(c_124,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_158,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_124]) ).
tff(c_232,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_158]) ).
tff(c_1174,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_232]) ).
tff(c_1175,plain,
rp('#skF_7','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_1149,c_829,c_1174]) ).
tff(c_116,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_194,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_116]) ).
tff(c_302,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_194]) ).
tff(c_1177,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_302]) ).
tff(c_1178,plain,
rp('#skF_7','#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_1149,c_829,c_1177]) ).
tff(c_1148,plain,
cc('#skF_7'),
inference(splitRight,[status(thm)],[c_828]) ).
tff(c_132,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_163,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_132]) ).
tff(c_242,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_163]) ).
tff(c_1193,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_242]) ).
tff(c_1194,plain,
rp('#skF_7','#skF_8'),
inference(negUnitSimplification,[status(thm)],[c_1149,c_829,c_1193]) ).
tff(c_1248,plain,
! [Y2_87,Y1_88,Y0_89,X_90] :
( ( Y2_87 = Y1_88 )
| ( Y2_87 = Y0_89 )
| ( Y1_88 = Y0_89 )
| ~ rp(X_90,Y2_87)
| ~ rp(X_90,Y1_88)
| ~ rp(X_90,Y0_89)
| ~ cc(X_90) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_1250,plain,
! [Y1_88,Y0_89] :
( ( Y1_88 = '#skF_8' )
| ( Y0_89 = '#skF_8' )
| ( Y1_88 = Y0_89 )
| ~ rp('#skF_7',Y1_88)
| ~ rp('#skF_7',Y0_89)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_1194,c_1248]) ).
tff(c_1270,plain,
! [Y1_91,Y0_92] :
( ( Y1_91 = '#skF_8' )
| ( Y0_92 = '#skF_8' )
| ( Y1_91 = Y0_92 )
| ~ rp('#skF_7',Y1_91)
| ~ rp('#skF_7',Y0_92) ),
inference(demodulation,[status(thm),theory(equality)],[c_1148,c_1250]) ).
tff(c_1274,plain,
! [Y0_92] :
( ( '#skF_10' = '#skF_8' )
| ( Y0_92 = '#skF_8' )
| ( Y0_92 = '#skF_10' )
| ~ rp('#skF_7',Y0_92) ),
inference(resolution,[status(thm)],[c_1178,c_1270]) ).
tff(c_1297,plain,
! [Y0_93] :
( ( Y0_93 = '#skF_8' )
| ( Y0_93 = '#skF_10' )
| ~ rp('#skF_7',Y0_93) ),
inference(negUnitSimplification,[status(thm)],[c_324,c_1274]) ).
tff(c_1306,plain,
( ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_9' ) ),
inference(resolution,[status(thm)],[c_1175,c_1297]) ).
tff(c_1326,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_322,c_323,c_1306]) ).
tff(c_1328,plain,
xsd_integer('#skF_5'),
inference(splitRight,[status(thm)],[c_250]) ).
tff(c_142,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_153,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_142]) ).
tff(c_222,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_153]) ).
tff(c_1348,plain,
( xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_222]) ).
tff(c_1349,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_1348]) ).
tff(c_1353,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_1349,c_26]) ).
tff(c_1327,plain,
( cc('#skF_11')
| cc('#skF_7')
| xsd_integer('#skF_6') ),
inference(splitRight,[status(thm)],[c_250]) ).
tff(c_1329,plain,
xsd_integer('#skF_6'),
inference(splitLeft,[status(thm)],[c_1327]) ).
tff(c_62,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_178,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_62]) ).
tff(c_272,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_178]) ).
tff(c_1400,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_272]) ).
tff(c_1401,plain,
rp('#skF_7','#skF_10'),
inference(splitLeft,[status(thm)],[c_1400]) ).
tff(c_70,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_174,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_70]) ).
tff(c_264,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_174]) ).
tff(c_1411,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_264]) ).
tff(c_1412,plain,
rp('#skF_7','#skF_9'),
inference(splitLeft,[status(thm)],[c_1411]) ).
tff(c_86,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_195,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_86]) ).
tff(c_304,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_195]) ).
tff(c_1378,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_304]) ).
tff(c_1379,plain,
cc('#skF_7'),
inference(splitLeft,[status(thm)],[c_1378]) ).
tff(c_78,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_170,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_78]) ).
tff(c_256,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_170]) ).
tff(c_1415,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_256]) ).
tff(c_1416,plain,
rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1415]) ).
tff(c_1418,plain,
! [Y2_94,Y1_95,Y0_96,X_97] :
( ( Y2_94 = Y1_95 )
| ( Y2_94 = Y0_96 )
| ( Y1_95 = Y0_96 )
| ~ rp(X_97,Y2_94)
| ~ rp(X_97,Y1_95)
| ~ rp(X_97,Y0_96)
| ~ cc(X_97) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_1420,plain,
! [Y1_95,Y0_96] :
( ( Y1_95 = '#skF_8' )
| ( Y0_96 = '#skF_8' )
| ( Y1_95 = Y0_96 )
| ~ rp('#skF_7',Y1_95)
| ~ rp('#skF_7',Y0_96)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_1416,c_1418]) ).
tff(c_1440,plain,
! [Y1_98,Y0_99] :
( ( Y1_98 = '#skF_8' )
| ( Y0_99 = '#skF_8' )
| ( Y1_98 = Y0_99 )
| ~ rp('#skF_7',Y1_98)
| ~ rp('#skF_7',Y0_99) ),
inference(demodulation,[status(thm),theory(equality)],[c_1379,c_1420]) ).
tff(c_1444,plain,
! [Y0_99] :
( ( '#skF_9' = '#skF_8' )
| ( Y0_99 = '#skF_8' )
| ( Y0_99 = '#skF_9' )
| ~ rp('#skF_7',Y0_99) ),
inference(resolution,[status(thm)],[c_1412,c_1440]) ).
tff(c_1467,plain,
! [Y0_100] :
( ( Y0_100 = '#skF_8' )
| ( Y0_100 = '#skF_9' )
| ~ rp('#skF_7',Y0_100) ),
inference(negUnitSimplification,[status(thm)],[c_323,c_1444]) ).
tff(c_1476,plain,
( ( '#skF_10' = '#skF_8' )
| ( '#skF_10' = '#skF_9' ) ),
inference(resolution,[status(thm)],[c_1401,c_1467]) ).
tff(c_1496,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_322,c_324,c_1476]) ).
tff(c_1497,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(splitRight,[status(thm)],[c_1415]) ).
tff(c_1499,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_1497]) ).
tff(c_1502,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_1499,c_20]) ).
tff(c_1506,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1329,c_1502]) ).
tff(c_1515,plain,
! [Y1_101,Y0_102] :
( ( Y1_101 = Y0_102 )
| ~ rp('#skF_11',Y1_101)
| ~ rp('#skF_11',Y0_102) ),
inference(splitRight,[status(thm)],[c_1497]) ).
tff(c_1518,plain,
! [Y0_102] :
( ( Y0_102 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_102)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1515]) ).
tff(c_1528,plain,
! [Y0_103] :
( ( Y0_103 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_103) ),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1518]) ).
tff(c_1536,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1528]) ).
tff(c_1543,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1536]) ).
tff(c_1545,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1353,c_1543]) ).
tff(c_1546,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(splitRight,[status(thm)],[c_1411]) ).
tff(c_1548,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_1546]) ).
tff(c_1551,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_1548,c_20]) ).
tff(c_1555,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1329,c_1551]) ).
tff(c_1563,plain,
! [Y1_104,Y0_105] :
( ( Y1_104 = Y0_105 )
| ~ rp('#skF_11',Y1_104)
| ~ rp('#skF_11',Y0_105) ),
inference(splitRight,[status(thm)],[c_1546]) ).
tff(c_1566,plain,
! [Y0_105] :
( ( Y0_105 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_105)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1563]) ).
tff(c_1576,plain,
! [Y0_106] :
( ( Y0_106 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_106) ),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1566]) ).
tff(c_1584,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1576]) ).
tff(c_1591,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1584]) ).
tff(c_1593,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1353,c_1591]) ).
tff(c_1594,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(splitRight,[status(thm)],[c_1400]) ).
tff(c_1596,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_1594]) ).
tff(c_1599,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_1596,c_20]) ).
tff(c_1603,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1329,c_1599]) ).
tff(c_1611,plain,
! [Y1_107,Y0_108] :
( ( Y1_107 = Y0_108 )
| ~ rp('#skF_11',Y1_107)
| ~ rp('#skF_11',Y0_108) ),
inference(splitRight,[status(thm)],[c_1594]) ).
tff(c_1614,plain,
! [Y0_108] :
( ( Y0_108 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_108)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1611]) ).
tff(c_1624,plain,
! [Y0_109] :
( ( Y0_109 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_109) ),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1614]) ).
tff(c_1632,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1624]) ).
tff(c_1639,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1632]) ).
tff(c_1641,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1353,c_1639]) ).
tff(c_1642,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(splitRight,[status(thm)],[c_1378]) ).
tff(c_1644,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_1642]) ).
tff(c_1647,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_1644,c_20]) ).
tff(c_1651,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1329,c_1647]) ).
tff(c_1660,plain,
! [Y1_110,Y0_111] :
( ( Y1_110 = Y0_111 )
| ~ rp('#skF_11',Y1_110)
| ~ rp('#skF_11',Y0_111) ),
inference(splitRight,[status(thm)],[c_1642]) ).
tff(c_1663,plain,
! [Y0_111] :
( ( Y0_111 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_111)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_1660]) ).
tff(c_1673,plain,
! [Y0_112] :
( ( Y0_112 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_112) ),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1663]) ).
tff(c_1681,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_1673]) ).
tff(c_1688,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1349,c_1681]) ).
tff(c_1690,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1353,c_1688]) ).
tff(c_1692,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_1348]) ).
tff(c_1691,plain,
( cc('#skF_7')
| xsd_string('#skF_6') ),
inference(splitRight,[status(thm)],[c_1348]) ).
tff(c_1693,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_1691]) ).
tff(c_1696,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_1693,c_20]) ).
tff(c_1700,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1329,c_1696]) ).
tff(c_1702,plain,
~ xsd_string('#skF_6'),
inference(splitRight,[status(thm)],[c_1691]) ).
tff(c_118,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_164,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_118]) ).
tff(c_244,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_164]) ).
tff(c_1720,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_244]) ).
tff(c_1721,plain,
rp('#skF_7','#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_1692,c_1702,c_1720]) ).
tff(c_126,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_156,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_126]) ).
tff(c_228,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_156]) ).
tff(c_1727,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_228]) ).
tff(c_1728,plain,
rp('#skF_7','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_1692,c_1702,c_1727]) ).
tff(c_1701,plain,
cc('#skF_7'),
inference(splitRight,[status(thm)],[c_1691]) ).
tff(c_134,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_159,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_134]) ).
tff(c_210,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_159]) ).
tff(c_1741,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_210]) ).
tff(c_1742,plain,
rp('#skF_7','#skF_8'),
inference(negUnitSimplification,[status(thm)],[c_1692,c_1702,c_1741]) ).
tff(c_1796,plain,
! [Y2_113,Y1_114,Y0_115,X_116] :
( ( Y2_113 = Y1_114 )
| ( Y2_113 = Y0_115 )
| ( Y1_114 = Y0_115 )
| ~ rp(X_116,Y2_113)
| ~ rp(X_116,Y1_114)
| ~ rp(X_116,Y0_115)
| ~ cc(X_116) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_1798,plain,
! [Y1_114,Y0_115] :
( ( Y1_114 = '#skF_8' )
| ( Y0_115 = '#skF_8' )
| ( Y1_114 = Y0_115 )
| ~ rp('#skF_7',Y1_114)
| ~ rp('#skF_7',Y0_115)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_1742,c_1796]) ).
tff(c_1818,plain,
! [Y1_117,Y0_118] :
( ( Y1_117 = '#skF_8' )
| ( Y0_118 = '#skF_8' )
| ( Y1_117 = Y0_118 )
| ~ rp('#skF_7',Y1_117)
| ~ rp('#skF_7',Y0_118) ),
inference(demodulation,[status(thm),theory(equality)],[c_1701,c_1798]) ).
tff(c_1822,plain,
! [Y0_118] :
( ( '#skF_9' = '#skF_8' )
| ( Y0_118 = '#skF_8' )
| ( Y0_118 = '#skF_9' )
| ~ rp('#skF_7',Y0_118) ),
inference(resolution,[status(thm)],[c_1728,c_1818]) ).
tff(c_1845,plain,
! [Y0_119] :
( ( Y0_119 = '#skF_8' )
| ( Y0_119 = '#skF_9' )
| ~ rp('#skF_7',Y0_119) ),
inference(negUnitSimplification,[status(thm)],[c_323,c_1822]) ).
tff(c_1854,plain,
( ( '#skF_10' = '#skF_8' )
| ( '#skF_10' = '#skF_9' ) ),
inference(resolution,[status(thm)],[c_1721,c_1845]) ).
tff(c_1874,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_322,c_324,c_1854]) ).
tff(c_1875,plain,
( cc('#skF_7')
| cc('#skF_11') ),
inference(splitRight,[status(thm)],[c_1327]) ).
tff(c_1877,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_1875]) ).
tff(c_1881,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_1877,c_26]) ).
tff(c_1876,plain,
~ xsd_integer('#skF_6'),
inference(splitRight,[status(thm)],[c_1327]) ).
tff(c_58,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_180,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_58]) ).
tff(c_276,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_180]) ).
tff(c_1958,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_276]) ).
tff(c_1959,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_10')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_1876,c_1958]) ).
tff(c_1960,plain,
rp('#skF_7','#skF_10'),
inference(splitLeft,[status(thm)],[c_1959]) ).
tff(c_1970,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_264]) ).
tff(c_1971,plain,
rp('#skF_7','#skF_9'),
inference(splitLeft,[status(thm)],[c_1970]) ).
tff(c_1934,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_304]) ).
tff(c_1935,plain,
cc('#skF_7'),
inference(splitLeft,[status(thm)],[c_1934]) ).
tff(c_74,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_172,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_74]) ).
tff(c_260,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_172]) ).
tff(c_1976,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_260]) ).
tff(c_1977,plain,
! [Y1_34,Y0_33] :
( rp('#skF_7','#skF_8')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(negUnitSimplification,[status(thm)],[c_1876,c_1976]) ).
tff(c_1978,plain,
rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1977]) ).
tff(c_1989,plain,
! [Y2_120,Y1_121,Y0_122,X_123] :
( ( Y2_120 = Y1_121 )
| ( Y2_120 = Y0_122 )
| ( Y1_121 = Y0_122 )
| ~ rp(X_123,Y2_120)
| ~ rp(X_123,Y1_121)
| ~ rp(X_123,Y0_122)
| ~ cc(X_123) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_1991,plain,
! [Y1_121,Y0_122] :
( ( Y1_121 = '#skF_8' )
| ( Y0_122 = '#skF_8' )
| ( Y1_121 = Y0_122 )
| ~ rp('#skF_7',Y1_121)
| ~ rp('#skF_7',Y0_122)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_1978,c_1989]) ).
tff(c_2011,plain,
! [Y1_124,Y0_125] :
( ( Y1_124 = '#skF_8' )
| ( Y0_125 = '#skF_8' )
| ( Y1_124 = Y0_125 )
| ~ rp('#skF_7',Y1_124)
| ~ rp('#skF_7',Y0_125) ),
inference(demodulation,[status(thm),theory(equality)],[c_1935,c_1991]) ).
tff(c_2015,plain,
! [Y0_125] :
( ( '#skF_9' = '#skF_8' )
| ( Y0_125 = '#skF_8' )
| ( Y0_125 = '#skF_9' )
| ~ rp('#skF_7',Y0_125) ),
inference(resolution,[status(thm)],[c_1971,c_2011]) ).
tff(c_2038,plain,
! [Y0_126] :
( ( Y0_126 = '#skF_8' )
| ( Y0_126 = '#skF_9' )
| ~ rp('#skF_7',Y0_126) ),
inference(negUnitSimplification,[status(thm)],[c_323,c_2015]) ).
tff(c_2047,plain,
( ( '#skF_10' = '#skF_8' )
| ( '#skF_10' = '#skF_9' ) ),
inference(resolution,[status(thm)],[c_1960,c_2038]) ).
tff(c_2067,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_322,c_324,c_2047]) ).
tff(c_2070,plain,
! [Y1_127,Y0_128] :
( ( Y1_127 = Y0_128 )
| ~ rp('#skF_11',Y1_127)
| ~ rp('#skF_11',Y0_128) ),
inference(splitRight,[status(thm)],[c_1977]) ).
tff(c_2073,plain,
! [Y0_128] :
( ( Y0_128 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_128)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2070]) ).
tff(c_2083,plain,
! [Y0_129] :
( ( Y0_129 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_129) ),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2073]) ).
tff(c_2091,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2083]) ).
tff(c_2098,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2091]) ).
tff(c_2100,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1881,c_2098]) ).
tff(c_2102,plain,
~ rp('#skF_7','#skF_9'),
inference(splitRight,[status(thm)],[c_1970]) ).
tff(c_66,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_176,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_66]) ).
tff(c_268,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_176]) ).
tff(c_2122,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_268]) ).
tff(c_2124,plain,
! [Y1_130,Y0_131] :
( ( Y1_130 = Y0_131 )
| ~ rp('#skF_11',Y1_130)
| ~ rp('#skF_11',Y0_131) ),
inference(negUnitSimplification,[status(thm)],[c_2102,c_1876,c_2122]) ).
tff(c_2127,plain,
! [Y0_131] :
( ( Y0_131 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_131)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2124]) ).
tff(c_2137,plain,
! [Y0_132] :
( ( Y0_132 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_132) ),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2127]) ).
tff(c_2145,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2137]) ).
tff(c_2152,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2145]) ).
tff(c_2154,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1881,c_2152]) ).
tff(c_2157,plain,
! [Y1_133,Y0_134] :
( ( Y1_133 = Y0_134 )
| ~ rp('#skF_11',Y1_133)
| ~ rp('#skF_11',Y0_134) ),
inference(splitRight,[status(thm)],[c_1959]) ).
tff(c_2160,plain,
! [Y0_134] :
( ( Y0_134 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_134)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2157]) ).
tff(c_2170,plain,
! [Y0_135] :
( ( Y0_135 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_135) ),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2160]) ).
tff(c_2178,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2170]) ).
tff(c_2185,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2178]) ).
tff(c_2187,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1881,c_2185]) ).
tff(c_2189,plain,
~ cc('#skF_7'),
inference(splitRight,[status(thm)],[c_1934]) ).
tff(c_82,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_198,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_82]) ).
tff(c_310,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_198]) ).
tff(c_2209,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| cc('#skF_7')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_310]) ).
tff(c_2211,plain,
! [Y1_136,Y0_137] :
( ( Y1_136 = Y0_137 )
| ~ rp('#skF_11',Y1_136)
| ~ rp('#skF_11',Y0_137) ),
inference(negUnitSimplification,[status(thm)],[c_2189,c_1876,c_2209]) ).
tff(c_2214,plain,
! [Y0_137] :
( ( Y0_137 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_137)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2211]) ).
tff(c_2224,plain,
! [Y0_138] :
( ( Y0_138 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_138) ),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2214]) ).
tff(c_2232,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2224]) ).
tff(c_2239,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1877,c_2232]) ).
tff(c_2241,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1881,c_2239]) ).
tff(c_2243,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_1875]) ).
tff(c_2291,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_228]) ).
tff(c_2292,plain,
( xsd_string('#skF_6')
| rp('#skF_7','#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_2243,c_2291]) ).
tff(c_2293,plain,
rp('#skF_7','#skF_9'),
inference(splitLeft,[status(thm)],[c_2292]) ).
tff(c_130,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_166,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_130]) ).
tff(c_248,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_166]) ).
tff(c_2273,plain,
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_8')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_248]) ).
tff(c_2274,plain,
rp('#skF_7','#skF_8'),
inference(negUnitSimplification,[status(thm)],[c_2243,c_1876,c_2273]) ).
tff(c_2242,plain,
cc('#skF_7'),
inference(splitRight,[status(thm)],[c_1875]) ).
tff(c_114,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_168,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_114]) ).
tff(c_252,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_168]) ).
tff(c_2284,plain,
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_10')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_252]) ).
tff(c_2285,plain,
rp('#skF_7','#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_2243,c_1876,c_2284]) ).
tff(c_2356,plain,
! [Y2_139,Y1_140,Y0_141,X_142] :
( ( Y2_139 = Y1_140 )
| ( Y2_139 = Y0_141 )
| ( Y1_140 = Y0_141 )
| ~ rp(X_142,Y2_139)
| ~ rp(X_142,Y1_140)
| ~ rp(X_142,Y0_141)
| ~ cc(X_142) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_2360,plain,
! [Y1_140,Y0_141] :
( ( Y1_140 = '#skF_10' )
| ( Y0_141 = '#skF_10' )
| ( Y1_140 = Y0_141 )
| ~ rp('#skF_7',Y1_140)
| ~ rp('#skF_7',Y0_141)
| ~ cc('#skF_7') ),
inference(resolution,[status(thm)],[c_2285,c_2356]) ).
tff(c_2378,plain,
! [Y1_143,Y0_144] :
( ( Y1_143 = '#skF_10' )
| ( Y0_144 = '#skF_10' )
| ( Y1_143 = Y0_144 )
| ~ rp('#skF_7',Y1_143)
| ~ rp('#skF_7',Y0_144) ),
inference(demodulation,[status(thm),theory(equality)],[c_2242,c_2360]) ).
tff(c_2384,plain,
! [Y0_144] :
( ( '#skF_10' = '#skF_8' )
| ( Y0_144 = '#skF_10' )
| ( Y0_144 = '#skF_8' )
| ~ rp('#skF_7',Y0_144) ),
inference(resolution,[status(thm)],[c_2274,c_2378]) ).
tff(c_2405,plain,
! [Y0_145] :
( ( Y0_145 = '#skF_10' )
| ( Y0_145 = '#skF_8' )
| ~ rp('#skF_7',Y0_145) ),
inference(negUnitSimplification,[status(thm)],[c_324,c_2384]) ).
tff(c_2408,plain,
( ( '#skF_10' = '#skF_9' )
| ( '#skF_9' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_2293,c_2405]) ).
tff(c_2426,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_323,c_322,c_2408]) ).
tff(c_2428,plain,
~ rp('#skF_7','#skF_9'),
inference(splitRight,[status(thm)],[c_2292]) ).
tff(c_122,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_160,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_122]) ).
tff(c_236,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_160]) ).
tff(c_2434,plain,
( xsd_integer('#skF_6')
| rp('#skF_7','#skF_9')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1328,c_236]) ).
tff(c_2435,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2243,c_2428,c_1876,c_2434]) ).
tff(c_2437,plain,
'#skF_10' = '#skF_8',
inference(splitRight,[status(thm)],[c_208]) ).
tff(c_102,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_149,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_102]) ).
tff(c_214,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_149]) ).
tff(c_2449,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_214]) ).
tff(c_2450,plain,
~ xsd_integer('#skF_5'),
inference(splitLeft,[status(thm)],[c_2449]) ).
tff(c_2436,plain,
( ~ xsd_string('#skF_5')
| cc('#skF_11')
| xsd_integer('#skF_6') ),
inference(splitRight,[status(thm)],[c_208]) ).
tff(c_2443,plain,
~ xsd_string('#skF_5'),
inference(splitLeft,[status(thm)],[c_2436]) ).
tff(c_2447,plain,
xsd_integer('#skF_5'),
inference(resolution,[status(thm)],[c_22,c_2443]) ).
tff(c_2451,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2450,c_2447]) ).
tff(c_2452,plain,
( cc('#skF_11')
| xsd_string('#skF_6') ),
inference(splitRight,[status(thm)],[c_2449]) ).
tff(c_2455,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_2452]) ).
tff(c_2459,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_2455,c_20]) ).
tff(c_2453,plain,
xsd_integer('#skF_5'),
inference(splitRight,[status(thm)],[c_2449]) ).
tff(c_98,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_161,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_98]) ).
tff(c_238,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_161]) ).
tff(c_2468,plain,
( xsd_integer('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_2453,c_238]) ).
tff(c_2469,plain,
cc('#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_2459,c_2468]) ).
tff(c_2473,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_2469,c_26]) ).
tff(c_42,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_188,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_42]) ).
tff(c_290,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_188]) ).
tff(c_2543,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_2453,c_290]) ).
tff(c_2545,plain,
! [Y1_146,Y0_147] :
( ( Y1_146 = Y0_147 )
| ~ rp('#skF_11',Y1_146)
| ~ rp('#skF_11',Y0_147) ),
inference(negUnitSimplification,[status(thm)],[c_2459,c_2543]) ).
tff(c_2548,plain,
! [Y0_147] :
( ( Y0_147 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_147)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2545]) ).
tff(c_2558,plain,
! [Y0_148] :
( ( Y0_148 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_148) ),
inference(demodulation,[status(thm),theory(equality)],[c_2469,c_2548]) ).
tff(c_2566,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2558]) ).
tff(c_2573,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2469,c_2566]) ).
tff(c_2575,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2473,c_2573]) ).
tff(c_2576,plain,
cc('#skF_11'),
inference(splitRight,[status(thm)],[c_2452]) ).
tff(c_2581,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_2576,c_26]) ).
tff(c_2577,plain,
~ xsd_string('#skF_6'),
inference(splitRight,[status(thm)],[c_2452]) ).
tff(c_46,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_186,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_46]) ).
tff(c_286,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_186]) ).
tff(c_2654,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_2453,c_286]) ).
tff(c_2656,plain,
! [Y1_149,Y0_150] :
( ( Y1_149 = Y0_150 )
| ~ rp('#skF_11',Y1_149)
| ~ rp('#skF_11',Y0_150) ),
inference(negUnitSimplification,[status(thm)],[c_2577,c_2654]) ).
tff(c_2659,plain,
! [Y0_150] :
( ( Y0_150 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_150)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2656]) ).
tff(c_2669,plain,
! [Y0_151] :
( ( Y0_151 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_151) ),
inference(demodulation,[status(thm),theory(equality)],[c_2576,c_2659]) ).
tff(c_2677,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2669]) ).
tff(c_2684,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2576,c_2677]) ).
tff(c_2686,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2581,c_2684]) ).
tff(c_2688,plain,
xsd_string('#skF_5'),
inference(splitRight,[status(thm)],[c_2436]) ).
tff(c_2694,plain,
( xsd_string('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2688,c_202]) ).
tff(c_2695,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_2694]) ).
tff(c_2699,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_2695,c_26]) ).
tff(c_40,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_189,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_40]) ).
tff(c_292,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_189]) ).
tff(c_2738,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_2688,c_292]) ).
tff(c_2739,plain,
xsd_integer('#skF_6'),
inference(splitLeft,[status(thm)],[c_2738]) ).
tff(c_44,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_187,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_44]) ).
tff(c_288,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_187]) ).
tff(c_2763,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_2688,c_288]) ).
tff(c_2764,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_2763]) ).
tff(c_2767,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_2764,c_20]) ).
tff(c_2771,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2739,c_2767]) ).
tff(c_2779,plain,
! [Y1_152,Y0_153] :
( ( Y1_152 = Y0_153 )
| ~ rp('#skF_11',Y1_152)
| ~ rp('#skF_11',Y0_153) ),
inference(splitRight,[status(thm)],[c_2763]) ).
tff(c_2782,plain,
! [Y0_153] :
( ( Y0_153 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_153)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2779]) ).
tff(c_2792,plain,
! [Y0_154] :
( ( Y0_154 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_154) ),
inference(demodulation,[status(thm),theory(equality)],[c_2695,c_2782]) ).
tff(c_2800,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2792]) ).
tff(c_2807,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2695,c_2800]) ).
tff(c_2809,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2699,c_2807]) ).
tff(c_2812,plain,
! [Y1_155,Y0_156] :
( ( Y1_155 = Y0_156 )
| ~ rp('#skF_11',Y1_155)
| ~ rp('#skF_11',Y0_156) ),
inference(splitRight,[status(thm)],[c_2738]) ).
tff(c_2815,plain,
! [Y0_156] :
( ( Y0_156 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_156)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2812]) ).
tff(c_2827,plain,
! [Y0_157] :
( ( Y0_157 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_157) ),
inference(demodulation,[status(thm),theory(equality)],[c_2695,c_2815]) ).
tff(c_2835,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2827]) ).
tff(c_2842,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2695,c_2835]) ).
tff(c_2844,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2699,c_2842]) ).
tff(c_2846,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_2694]) ).
tff(c_2687,plain,
( xsd_integer('#skF_6')
| cc('#skF_11') ),
inference(splitRight,[status(thm)],[c_2436]) ).
tff(c_2847,plain,
xsd_integer('#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_2846,c_2687]) ).
tff(c_2845,plain,
( cc('#skF_7')
| xsd_string('#skF_6') ),
inference(splitRight,[status(thm)],[c_2694]) ).
tff(c_2848,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_2845]) ).
tff(c_2851,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_2848,c_20]) ).
tff(c_2855,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2847,c_2851]) ).
tff(c_2857,plain,
~ xsd_string('#skF_6'),
inference(splitRight,[status(thm)],[c_2845]) ).
tff(c_100,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_150,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_100]) ).
tff(c_216,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_150]) ).
tff(c_2881,plain,
( xsd_string('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2437,c_2688,c_216]) ).
tff(c_2882,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2846,c_2857,c_2881]) ).
tff(c_2883,plain,
( ~ xsd_string('#skF_5')
| cc('#skF_11')
| xsd_string('#skF_6') ),
inference(splitRight,[status(thm)],[c_212]) ).
tff(c_2890,plain,
~ xsd_string('#skF_5'),
inference(splitLeft,[status(thm)],[c_2883]) ).
tff(c_2894,plain,
xsd_integer('#skF_5'),
inference(resolution,[status(thm)],[c_22,c_2890]) ).
tff(c_2899,plain,
( xsd_integer('#skF_6')
| cc('#skF_7')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2894,c_250]) ).
tff(c_2900,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_2899]) ).
tff(c_2906,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_2900,c_26]) ).
tff(c_2884,plain,
'#skF_9' = '#skF_8',
inference(splitRight,[status(thm)],[c_212]) ).
tff(c_54,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_182,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_54]) ).
tff(c_280,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_182]) ).
tff(c_2950,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_2894,c_280]) ).
tff(c_2951,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_2950]) ).
tff(c_2955,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_2951,c_20]) ).
tff(c_50,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_184,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_50]) ).
tff(c_282,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_184]) ).
tff(c_2960,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_2894,c_282]) ).
tff(c_2962,plain,
! [Y1_158,Y0_159] :
( ( Y1_158 = Y0_159 )
| ~ rp('#skF_11',Y1_158)
| ~ rp('#skF_11',Y0_159) ),
inference(negUnitSimplification,[status(thm)],[c_2955,c_2960]) ).
tff(c_2965,plain,
! [Y0_159] :
( ( Y0_159 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_159)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_2962]) ).
tff(c_2975,plain,
! [Y0_160] :
( ( Y0_160 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_160) ),
inference(demodulation,[status(thm),theory(equality)],[c_2900,c_2965]) ).
tff(c_2983,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_2975]) ).
tff(c_2990,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2900,c_2983]) ).
tff(c_2992,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2906,c_2990]) ).
tff(c_3000,plain,
! [Y1_161,Y0_162] :
( ( Y1_161 = Y0_162 )
| ~ rp('#skF_11',Y1_161)
| ~ rp('#skF_11',Y0_162) ),
inference(splitRight,[status(thm)],[c_2950]) ).
tff(c_3003,plain,
! [Y0_162] :
( ( Y0_162 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_162)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3000]) ).
tff(c_3013,plain,
! [Y0_163] :
( ( Y0_163 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_163) ),
inference(demodulation,[status(thm),theory(equality)],[c_2900,c_3003]) ).
tff(c_3021,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3013]) ).
tff(c_3028,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2900,c_3021]) ).
tff(c_3030,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2906,c_3028]) ).
tff(c_3032,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_2899]) ).
tff(c_3031,plain,
( cc('#skF_7')
| xsd_integer('#skF_6') ),
inference(splitRight,[status(thm)],[c_2899]) ).
tff(c_3033,plain,
xsd_integer('#skF_6'),
inference(splitLeft,[status(thm)],[c_3031]) ).
tff(c_110,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_147,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_110]) ).
tff(c_200,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_147]) ).
tff(c_3056,plain,
( xsd_string('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_2894,c_200]) ).
tff(c_3057,plain,
xsd_string('#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_3032,c_3056]) ).
tff(c_3060,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3057,c_20]) ).
tff(c_3064,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3033,c_3060]) ).
tff(c_3066,plain,
~ xsd_integer('#skF_6'),
inference(splitRight,[status(thm)],[c_3031]) ).
tff(c_106,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_157,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_106]) ).
tff(c_230,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_157]) ).
tff(c_3097,plain,
( xsd_integer('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_2894,c_230]) ).
tff(c_3098,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3032,c_3066,c_3097]) ).
tff(c_3099,plain,
( xsd_string('#skF_6')
| cc('#skF_11') ),
inference(splitRight,[status(thm)],[c_2883]) ).
tff(c_3105,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_3099]) ).
tff(c_3109,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_3105,c_26]) ).
tff(c_3100,plain,
xsd_string('#skF_5'),
inference(splitRight,[status(thm)],[c_2883]) ).
tff(c_52,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_183,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_52]) ).
tff(c_234,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_183]) ).
tff(c_3152,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_3100,c_234]) ).
tff(c_3153,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_3152]) ).
tff(c_3157,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3153,c_20]) ).
tff(c_48,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_185,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_48]) ).
tff(c_284,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_185]) ).
tff(c_3185,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_3100,c_284]) ).
tff(c_3187,plain,
! [Y1_164,Y0_165] :
( ( Y1_164 = Y0_165 )
| ~ rp('#skF_11',Y1_164)
| ~ rp('#skF_11',Y0_165) ),
inference(negUnitSimplification,[status(thm)],[c_3157,c_3185]) ).
tff(c_3190,plain,
! [Y0_165] :
( ( Y0_165 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_165)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3187]) ).
tff(c_3200,plain,
! [Y0_166] :
( ( Y0_166 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_166) ),
inference(demodulation,[status(thm),theory(equality)],[c_3105,c_3190]) ).
tff(c_3208,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3200]) ).
tff(c_3215,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_3105,c_3208]) ).
tff(c_3217,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3109,c_3215]) ).
tff(c_3231,plain,
! [Y1_167,Y0_168] :
( ( Y1_167 = Y0_168 )
| ~ rp('#skF_11',Y1_167)
| ~ rp('#skF_11',Y0_168) ),
inference(splitRight,[status(thm)],[c_3152]) ).
tff(c_3234,plain,
! [Y0_168] :
( ( Y0_168 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_168)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3231]) ).
tff(c_3244,plain,
! [Y0_169] :
( ( Y0_169 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_169) ),
inference(demodulation,[status(thm),theory(equality)],[c_3105,c_3234]) ).
tff(c_3252,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3244]) ).
tff(c_3259,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_3105,c_3252]) ).
tff(c_3261,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3109,c_3259]) ).
tff(c_3263,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_3099]) ).
tff(c_3262,plain,
xsd_string('#skF_6'),
inference(splitRight,[status(thm)],[c_3099]) ).
tff(c_3267,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3262,c_20]) ).
tff(c_104,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_145,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_104]) ).
tff(c_206,plain,
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_9' != '#skF_8' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_145]) ).
tff(c_3300,plain,
( xsd_integer('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_2884,c_3100,c_206]) ).
tff(c_3301,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3263,c_3267,c_3300]) ).
tff(c_3303,plain,
'#skF_10' = '#skF_9',
inference(splitRight,[status(thm)],[c_306]) ).
tff(c_3302,plain,
( ~ xsd_string('#skF_5')
| cc('#skF_11')
| xsd_integer('#skF_6') ),
inference(splitRight,[status(thm)],[c_306]) ).
tff(c_3308,plain,
~ xsd_string('#skF_5'),
inference(splitLeft,[status(thm)],[c_3302]) ).
tff(c_3312,plain,
xsd_integer('#skF_5'),
inference(resolution,[status(thm)],[c_22,c_3308]) ).
tff(c_90,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_165,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_90]) ).
tff(c_246,plain,
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_165]) ).
tff(c_3314,plain,
( xsd_integer('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3312,c_246]) ).
tff(c_3315,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_3314]) ).
tff(c_3319,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_3315,c_26]) ).
tff(c_34,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_192,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_34]) ).
tff(c_298,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_192]) ).
tff(c_3367,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3312,c_298]) ).
tff(c_3368,plain,
xsd_integer('#skF_6'),
inference(splitLeft,[status(thm)],[c_3367]) ).
tff(c_38,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_190,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_38]) ).
tff(c_294,plain,
! [Y1_34,Y0_33] :
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_190]) ).
tff(c_3388,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3312,c_294]) ).
tff(c_3389,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_3388]) ).
tff(c_3392,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3389,c_20]) ).
tff(c_3396,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3368,c_3392]) ).
tff(c_3405,plain,
! [Y1_170,Y0_171] :
( ( Y1_170 = Y0_171 )
| ~ rp('#skF_11',Y1_170)
| ~ rp('#skF_11',Y0_171) ),
inference(splitRight,[status(thm)],[c_3388]) ).
tff(c_3408,plain,
! [Y0_171] :
( ( Y0_171 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_171)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3405]) ).
tff(c_3418,plain,
! [Y0_172] :
( ( Y0_172 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_172) ),
inference(demodulation,[status(thm),theory(equality)],[c_3315,c_3408]) ).
tff(c_3426,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3418]) ).
tff(c_3433,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_3315,c_3426]) ).
tff(c_3435,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3319,c_3433]) ).
tff(c_3440,plain,
! [Y1_173,Y0_174] :
( ( Y1_173 = Y0_174 )
| ~ rp('#skF_11',Y1_173)
| ~ rp('#skF_11',Y0_174) ),
inference(splitRight,[status(thm)],[c_3367]) ).
tff(c_3443,plain,
! [Y0_174] :
( ( Y0_174 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_174)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3440]) ).
tff(c_3453,plain,
! [Y0_175] :
( ( Y0_175 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_175) ),
inference(demodulation,[status(thm),theory(equality)],[c_3315,c_3443]) ).
tff(c_3461,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3453]) ).
tff(c_3468,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_3315,c_3461]) ).
tff(c_3470,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3319,c_3468]) ).
tff(c_3471,plain,
xsd_integer('#skF_6'),
inference(splitRight,[status(thm)],[c_3314]) ).
tff(c_3472,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_3314]) ).
tff(c_94,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_151,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_94]) ).
tff(c_218,plain,
( ~ xsd_integer('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_151]) ).
tff(c_3501,plain,
( xsd_string('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3312,c_218]) ).
tff(c_3502,plain,
xsd_string('#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_3472,c_3501]) ).
tff(c_3505,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3502,c_20]) ).
tff(c_3509,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3471,c_3505]) ).
tff(c_3510,plain,
( xsd_integer('#skF_6')
| cc('#skF_11') ),
inference(splitRight,[status(thm)],[c_3302]) ).
tff(c_3516,plain,
cc('#skF_11'),
inference(splitLeft,[status(thm)],[c_3510]) ).
tff(c_3523,plain,
'#skF_2'('#skF_11') != '#skF_1'('#skF_11'),
inference(resolution,[status(thm)],[c_3516,c_26]) ).
tff(c_3511,plain,
xsd_string('#skF_5'),
inference(splitRight,[status(thm)],[c_3302]) ).
tff(c_32,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_193,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_32]) ).
tff(c_300,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_integer('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_193]) ).
tff(c_3577,plain,
! [Y1_34,Y0_33] :
( xsd_integer('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3511,c_300]) ).
tff(c_3578,plain,
xsd_integer('#skF_6'),
inference(splitLeft,[status(thm)],[c_3577]) ).
tff(c_36,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_191,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33)
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_36]) ).
tff(c_296,plain,
! [Y1_34,Y0_33] :
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_191]) ).
tff(c_3591,plain,
! [Y1_34,Y0_33] :
( xsd_string('#skF_6')
| ( Y1_34 = Y0_33 )
| ~ rp('#skF_11',Y1_34)
| ~ rp('#skF_11',Y0_33) ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3511,c_296]) ).
tff(c_3592,plain,
xsd_string('#skF_6'),
inference(splitLeft,[status(thm)],[c_3591]) ).
tff(c_3595,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3592,c_20]) ).
tff(c_3599,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3578,c_3595]) ).
tff(c_3607,plain,
! [Y1_176,Y0_177] :
( ( Y1_176 = Y0_177 )
| ~ rp('#skF_11',Y1_176)
| ~ rp('#skF_11',Y0_177) ),
inference(splitRight,[status(thm)],[c_3591]) ).
tff(c_3610,plain,
! [Y0_177] :
( ( Y0_177 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_177)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3607]) ).
tff(c_3622,plain,
! [Y0_178] :
( ( Y0_178 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_178) ),
inference(demodulation,[status(thm),theory(equality)],[c_3516,c_3610]) ).
tff(c_3630,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3622]) ).
tff(c_3637,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_3516,c_3630]) ).
tff(c_3639,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3523,c_3637]) ).
tff(c_3642,plain,
! [Y1_179,Y0_180] :
( ( Y1_179 = Y0_180 )
| ~ rp('#skF_11',Y1_179)
| ~ rp('#skF_11',Y0_180) ),
inference(splitRight,[status(thm)],[c_3577]) ).
tff(c_3645,plain,
! [Y0_180] :
( ( Y0_180 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_180)
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_30,c_3642]) ).
tff(c_3655,plain,
! [Y0_181] :
( ( Y0_181 = '#skF_1'('#skF_11') )
| ~ rp('#skF_11',Y0_181) ),
inference(demodulation,[status(thm),theory(equality)],[c_3516,c_3645]) ).
tff(c_3663,plain,
( ( '#skF_2'('#skF_11') = '#skF_1'('#skF_11') )
| ~ cc('#skF_11') ),
inference(resolution,[status(thm)],[c_28,c_3655]) ).
tff(c_3670,plain,
'#skF_2'('#skF_11') = '#skF_1'('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_3516,c_3663]) ).
tff(c_3672,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3523,c_3670]) ).
tff(c_3673,plain,
xsd_integer('#skF_6'),
inference(splitRight,[status(thm)],[c_3510]) ).
tff(c_3674,plain,
~ cc('#skF_11'),
inference(splitRight,[status(thm)],[c_3510]) ).
tff(c_92,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4')
| cowlNothing('#skF_3') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_152,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11')
| ~ cowlThing('#skF_4') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_92]) ).
tff(c_220,plain,
( ~ xsd_string('#skF_5')
| xsd_string('#skF_6')
| ( '#skF_10' != '#skF_9' )
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_152]) ).
tff(c_3694,plain,
( xsd_string('#skF_6')
| cc('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_3303,c_3511,c_220]) ).
tff(c_3695,plain,
xsd_string('#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_3674,c_3694]) ).
tff(c_3698,plain,
~ xsd_integer('#skF_6'),
inference(resolution,[status(thm)],[c_3695,c_20]) ).
tff(c_3702,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3673,c_3698]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS144+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/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.14/0.34 % Computer : n028.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 02:59:50 EDT 2025
% 0.14/0.34 % CPUTime :
% 6.04/2.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.04/2.46
% 6.04/2.46 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------