%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS162+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 : n015.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:08:08 PM UTC 2025
% Result : Theorem 10.10s 4.08s
% Output : CNFRefutation 10.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 8
% Syntax : Number of formulae : 509 ( 240 unt; 0 typ; 0 def)
% Number of atoms : 2222 (1125 equ)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 2446 ( 733 ~;1679 |; 27 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 420 ( 410 !; 10 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rr > rq > rp > xsd_string > xsd_integer > cowlThing > cowlNothing > cB > cA > #nlpp > #skF_7 > #skF_10 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_9 > #skF_8 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(rr,type,
rr: ( $i * $i ) > $o ).
tff(cA,type,
cA: $i > $o ).
tff(rq,type,
rq: ( $i * $i ) > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(cB,type,
cB: $i > $o ).
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_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $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_107,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
tff(f_216,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ( ? [Y0,Y1] :
( rp(X,Y0)
& rp(X,Y1)
& ( Y0 != Y1 ) )
& ? [Y0,Y1,Y2] :
( rq(X,Y0)
& rq(X,Y1)
& rq(X,Y2)
& ( Y0 != Y1 )
& ( Y0 != Y2 )
& ( Y1 != Y2 ) ) )
=> ? [Y0,Y1,Y2,Y3,Y4] :
( rr(X,Y0)
& rr(X,Y1)
& rr(X,Y2)
& rr(X,Y3)
& rr(X,Y4)
& ( Y0 != Y1 )
& ( Y0 != Y2 )
& ( Y0 != Y3 )
& ( Y0 != Y4 )
& ( Y1 != Y2 )
& ( Y1 != Y3 )
& ( Y1 != Y4 )
& ( Y2 != Y3 )
& ( Y2 != Y4 )
& ( Y3 != Y4 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
tff(f_113,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
tff(f_123,axiom,
! [X,Y] :
( rq(X,Y)
=> cB(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
tff(f_128,axiom,
! [X] :
~ ( cB(X)
& cA(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
tff(f_118,axiom,
! [X,Y] :
( rp(X,Y)
=> cA(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
tff(f_132,axiom,
! [X,Y] :
( rq(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
tff(f_136,axiom,
! [X,Y] :
( rp(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
tff(c_26,plain,
! [X_31] : cowlThing(X_31),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_28,plain,
! [X_31] : ~ cowlNothing(X_31),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_62,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_147,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_62]) ).
tff(c_178,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_147]) ).
tff(c_255,plain,
'#skF_10' != '#skF_8',
inference(splitLeft,[status(thm)],[c_178]) ).
tff(c_72,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_131,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_72]) ).
tff(c_180,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_9' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_131]) ).
tff(c_256,plain,
'#skF_9' != '#skF_8',
inference(splitLeft,[status(thm)],[c_180]) ).
tff(c_32,plain,
! [X_32] :
( xsd_string(X_32)
| xsd_integer(X_32) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_84,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_157,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_84]) ).
tff(c_232,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_157]) ).
tff(c_260,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_232]) ).
tff(c_264,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_32,c_260]) ).
tff(c_98,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_142,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_98]) ).
tff(c_202,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_142]) ).
tff(c_280,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_202]) ).
tff(c_281,plain,
rq('#skF_5','#skF_8'),
inference(splitLeft,[status(thm)],[c_280]) ).
tff(c_36,plain,
! [Y_36,X_35] :
( cB(Y_36)
| ~ rq(X_35,Y_36) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_285,plain,
cB('#skF_8'),
inference(resolution,[status(thm)],[c_281,c_36]) ).
tff(c_38,plain,
! [X_37] :
( ~ cA(X_37)
| ~ cB(X_37) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_289,plain,
~ cA('#skF_8'),
inference(resolution,[status(thm)],[c_285,c_38]) ).
tff(c_118,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_130,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_118]) ).
tff(c_212,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_130]) ).
tff(c_273,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_212]) ).
tff(c_274,plain,
rp('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_273]) ).
tff(c_34,plain,
! [Y_34,X_33] :
( cA(Y_34)
| ~ rp(X_33,Y_34) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_278,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_274,c_34]) ).
tff(c_56,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_135,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_56]) ).
tff(c_188,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_9' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_135]) ).
tff(c_257,plain,
'#skF_10' != '#skF_9',
inference(splitLeft,[status(thm)],[c_188]) ).
tff(c_82,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_158,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_82]) ).
tff(c_234,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_158]) ).
tff(c_297,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_234]) ).
tff(c_298,plain,
rq('#skF_5','#skF_10'),
inference(splitLeft,[status(thm)],[c_297]) ).
tff(c_90,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_150,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_90]) ).
tff(c_218,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_150]) ).
tff(c_310,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_218]) ).
tff(c_311,plain,
rq('#skF_5','#skF_9'),
inference(splitLeft,[status(thm)],[c_310]) ).
tff(c_40,plain,
! [X_38,Y_39] :
( rr(X_38,Y_39)
| ~ rq(X_38,Y_39) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_42,plain,
! [X_40,Y_41] :
( rr(X_40,Y_41)
| ~ rp(X_40,Y_41) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_315,plain,
cB('#skF_9'),
inference(resolution,[status(thm)],[c_311,c_36]) ).
tff(c_319,plain,
~ cA('#skF_9'),
inference(resolution,[status(thm)],[c_315,c_38]) ).
tff(c_50,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_153,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_50]) ).
tff(c_224,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_153]) ).
tff(c_329,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_224]) ).
tff(c_330,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_329]) ).
tff(c_30,plain,
! [X_32] :
( ~ xsd_integer(X_32)
| ~ xsd_string(X_32) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_334,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_330,c_30]) ).
tff(c_46,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_155,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_46]) ).
tff(c_228,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_155]) ).
tff(c_336,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_228]) ).
tff(c_338,plain,
! [Y3_71,Y1_70,Y0_73,Y2_74,Y4_72] :
( ( Y4_72 = Y3_71 )
| ( Y4_72 = Y2_74 )
| ( Y3_71 = Y2_74 )
| ( Y4_72 = Y1_70 )
| ( Y3_71 = Y1_70 )
| ( Y2_74 = Y1_70 )
| ( Y4_72 = Y0_73 )
| ( Y3_71 = Y0_73 )
| ( Y2_74 = Y0_73 )
| ( Y1_70 = Y0_73 )
| ~ rr('#skF_5',Y4_72)
| ~ rr('#skF_5',Y3_71)
| ~ rr('#skF_5',Y2_74)
| ~ rr('#skF_5',Y1_70)
| ~ rr('#skF_5',Y0_73) ),
inference(negUnitSimplification,[status(thm)],[c_334,c_336]) ).
tff(c_347,plain,
! [Y1_75,Y_77,Y3_76,Y0_79,Y2_78] :
( ( Y_77 = Y3_76 )
| ( Y_77 = Y2_78 )
| ( Y3_76 = Y2_78 )
| ( Y_77 = Y1_75 )
| ( Y3_76 = Y1_75 )
| ( Y2_78 = Y1_75 )
| ( Y_77 = Y0_79 )
| ( Y3_76 = Y0_79 )
| ( Y2_78 = Y0_79 )
| ( Y1_75 = Y0_79 )
| ~ rr('#skF_5',Y3_76)
| ~ rr('#skF_5',Y2_78)
| ~ rr('#skF_5',Y1_75)
| ~ rr('#skF_5',Y0_79)
| ~ rp('#skF_5',Y_77) ),
inference(resolution,[status(thm)],[c_42,c_338]) ).
tff(c_365,plain,
! [Y_87,Y2_85,Y_88,Y1_89,Y0_86] :
( ( Y_88 = Y_87 )
| ( Y_87 = Y2_85 )
| ( Y_88 = Y2_85 )
| ( Y_87 = Y1_89 )
| ( Y_88 = Y1_89 )
| ( Y2_85 = Y1_89 )
| ( Y_87 = Y0_86 )
| ( Y_88 = Y0_86 )
| ( Y2_85 = Y0_86 )
| ( Y1_89 = Y0_86 )
| ~ rr('#skF_5',Y2_85)
| ~ rr('#skF_5',Y1_89)
| ~ rr('#skF_5',Y0_86)
| ~ rp('#skF_5',Y_87)
| ~ rq('#skF_5',Y_88) ),
inference(resolution,[status(thm)],[c_40,c_347]) ).
tff(c_392,plain,
! [Y0_104,Y1_100,Y_103,Y_101,Y_102] :
( ( Y_102 = Y_101 )
| ( Y_103 = Y_102 )
| ( Y_103 = Y_101 )
| ( Y_102 = Y1_100 )
| ( Y_101 = Y1_100 )
| ( Y_103 = Y1_100 )
| ( Y_102 = Y0_104 )
| ( Y_101 = Y0_104 )
| ( Y_103 = Y0_104 )
| ( Y1_100 = Y0_104 )
| ~ rr('#skF_5',Y1_100)
| ~ rr('#skF_5',Y0_104)
| ~ rp('#skF_5',Y_102)
| ~ rq('#skF_5',Y_101)
| ~ rq('#skF_5',Y_103) ),
inference(resolution,[status(thm)],[c_40,c_365]) ).
tff(c_536,plain,
! [Y_181,Y_182,Y_183,Y0_180,Y_184] :
( ( Y_182 = Y_181 )
| ( Y_184 = Y_181 )
| ( Y_184 = Y_182 )
| ( Y_183 = Y_181 )
| ( Y_183 = Y_182 )
| ( Y_184 = Y_183 )
| ( Y_181 = Y0_180 )
| ( Y_182 = Y0_180 )
| ( Y_184 = Y0_180 )
| ( Y_183 = Y0_180 )
| ~ rr('#skF_5',Y0_180)
| ~ rp('#skF_5',Y_181)
| ~ rq('#skF_5',Y_182)
| ~ rq('#skF_5',Y_184)
| ~ rp('#skF_5',Y_183) ),
inference(resolution,[status(thm)],[c_42,c_392]) ).
tff(c_554,plain,
! [Y_193,Y_192,Y_191,Y_194,Y_190] :
( ( Y_191 = Y_190 )
| ( Y_193 = Y_191 )
| ( Y_193 = Y_190 )
| ( Y_194 = Y_191 )
| ( Y_194 = Y_190 )
| ( Y_194 = Y_193 )
| ( Y_192 = Y_191 )
| ( Y_192 = Y_190 )
| ( Y_193 = Y_192 )
| ( Y_194 = Y_192 )
| ~ rp('#skF_5',Y_191)
| ~ rq('#skF_5',Y_190)
| ~ rq('#skF_5',Y_193)
| ~ rp('#skF_5',Y_194)
| ~ rq('#skF_5',Y_192) ),
inference(resolution,[status(thm)],[c_40,c_536]) ).
tff(c_571,plain,
! [Y_200,Y_201,Y_202,Y_203] :
( ( Y_200 = '#skF_6' )
| ( Y_201 = '#skF_6' )
| ( Y_201 = Y_200 )
| ( Y_202 = '#skF_6' )
| ( Y_202 = Y_200 )
| ( Y_202 = Y_201 )
| ( Y_203 = '#skF_6' )
| ( Y_203 = Y_200 )
| ( Y_203 = Y_201 )
| ( Y_203 = Y_202 )
| ~ rq('#skF_5',Y_200)
| ~ rq('#skF_5',Y_201)
| ~ rp('#skF_5',Y_202)
| ~ rq('#skF_5',Y_203) ),
inference(resolution,[status(thm)],[c_274,c_554]) ).
tff(c_578,plain,
! [Y_201,Y_202,Y_203] :
( ( '#skF_6' = '#skF_9' )
| ( Y_201 = '#skF_6' )
| ( Y_201 = '#skF_9' )
| ( Y_202 = '#skF_6' )
| ( Y_202 = '#skF_9' )
| ( Y_202 = Y_201 )
| ( Y_203 = '#skF_6' )
| ( Y_203 = '#skF_9' )
| ( Y_203 = Y_201 )
| ( Y_203 = Y_202 )
| ~ rq('#skF_5',Y_201)
| ~ rp('#skF_5',Y_202)
| ~ rq('#skF_5',Y_203) ),
inference(resolution,[status(thm)],[c_311,c_571]) ).
tff(c_581,plain,
'#skF_6' = '#skF_9',
inference(splitLeft,[status(thm)],[c_578]) ).
tff(c_583,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_581,c_278]) ).
tff(c_587,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_319,c_583]) ).
tff(c_601,plain,
! [Y_204,Y_205,Y_206] :
( ( Y_204 = '#skF_6' )
| ( Y_204 = '#skF_9' )
| ( Y_205 = '#skF_6' )
| ( Y_205 = '#skF_9' )
| ( Y_205 = Y_204 )
| ( Y_206 = '#skF_6' )
| ( Y_206 = '#skF_9' )
| ( Y_206 = Y_204 )
| ( Y_206 = Y_205 )
| ~ rq('#skF_5',Y_204)
| ~ rp('#skF_5',Y_205)
| ~ rq('#skF_5',Y_206) ),
inference(splitRight,[status(thm)],[c_578]) ).
tff(c_607,plain,
! [Y_205,Y_206] :
( ( '#skF_6' = '#skF_8' )
| ( '#skF_9' = '#skF_8' )
| ( Y_205 = '#skF_6' )
| ( Y_205 = '#skF_9' )
| ( Y_205 = '#skF_8' )
| ( Y_206 = '#skF_6' )
| ( Y_206 = '#skF_9' )
| ( Y_206 = '#skF_8' )
| ( Y_206 = Y_205 )
| ~ rp('#skF_5',Y_205)
| ~ rq('#skF_5',Y_206) ),
inference(resolution,[status(thm)],[c_281,c_601]) ).
tff(c_617,plain,
! [Y_205,Y_206] :
( ( '#skF_6' = '#skF_8' )
| ( Y_205 = '#skF_6' )
| ( Y_205 = '#skF_9' )
| ( Y_205 = '#skF_8' )
| ( Y_206 = '#skF_6' )
| ( Y_206 = '#skF_9' )
| ( Y_206 = '#skF_8' )
| ( Y_206 = Y_205 )
| ~ rp('#skF_5',Y_205)
| ~ rq('#skF_5',Y_206) ),
inference(negUnitSimplification,[status(thm)],[c_256,c_607]) ).
tff(c_645,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_617]) ).
tff(c_651,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_645,c_278]) ).
tff(c_655,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_289,c_651]) ).
tff(c_657,plain,
'#skF_6' != '#skF_8',
inference(splitRight,[status(thm)],[c_617]) ).
tff(c_302,plain,
cB('#skF_10'),
inference(resolution,[status(thm)],[c_298,c_36]) ).
tff(c_306,plain,
~ cA('#skF_10'),
inference(resolution,[status(thm)],[c_302,c_38]) ).
tff(c_102,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_159,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_102]) ).
tff(c_190,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_6' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_159]) ).
tff(c_254,plain,
'#skF_7' != '#skF_6',
inference(splitLeft,[status(thm)],[c_190]) ).
tff(c_114,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_138,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_114]) ).
tff(c_194,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_138]) ).
tff(c_266,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_194]) ).
tff(c_267,plain,
rp('#skF_5','#skF_7'),
inference(splitLeft,[status(thm)],[c_266]) ).
tff(c_579,plain,
! [Y_201,Y_202,Y_203] :
( ( '#skF_10' = '#skF_6' )
| ( Y_201 = '#skF_6' )
| ( Y_201 = '#skF_10' )
| ( Y_202 = '#skF_6' )
| ( Y_202 = '#skF_10' )
| ( Y_202 = Y_201 )
| ( Y_203 = '#skF_6' )
| ( Y_203 = '#skF_10' )
| ( Y_203 = Y_201 )
| ( Y_203 = Y_202 )
| ~ rq('#skF_5',Y_201)
| ~ rp('#skF_5',Y_202)
| ~ rq('#skF_5',Y_203) ),
inference(resolution,[status(thm)],[c_298,c_571]) ).
tff(c_590,plain,
'#skF_10' = '#skF_6',
inference(splitLeft,[status(thm)],[c_579]) ).
tff(c_591,plain,
~ cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_590,c_306]) ).
tff(c_598,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_278,c_591]) ).
tff(c_600,plain,
'#skF_10' != '#skF_6',
inference(splitRight,[status(thm)],[c_579]) ).
tff(c_605,plain,
! [Y_205,Y_206] :
( ( '#skF_10' = '#skF_6' )
| ( '#skF_10' = '#skF_9' )
| ( Y_205 = '#skF_6' )
| ( Y_205 = '#skF_9' )
| ( Y_205 = '#skF_10' )
| ( Y_206 = '#skF_6' )
| ( Y_206 = '#skF_9' )
| ( Y_206 = '#skF_10' )
| ( Y_206 = Y_205 )
| ~ rp('#skF_5',Y_205)
| ~ rq('#skF_5',Y_206) ),
inference(resolution,[status(thm)],[c_298,c_601]) ).
tff(c_618,plain,
! [Y_207,Y_208] :
( ( Y_207 = '#skF_6' )
| ( Y_207 = '#skF_9' )
| ( Y_207 = '#skF_10' )
| ( Y_208 = '#skF_6' )
| ( Y_208 = '#skF_9' )
| ( Y_208 = '#skF_10' )
| ( Y_208 = Y_207 )
| ~ rp('#skF_5',Y_207)
| ~ rq('#skF_5',Y_208) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_600,c_605]) ).
tff(c_622,plain,
! [Y_208] :
( ( '#skF_7' = '#skF_6' )
| ( '#skF_7' = '#skF_9' )
| ( '#skF_7' = '#skF_10' )
| ( Y_208 = '#skF_6' )
| ( Y_208 = '#skF_9' )
| ( Y_208 = '#skF_10' )
| ( Y_208 = '#skF_7' )
| ~ rq('#skF_5',Y_208) ),
inference(resolution,[status(thm)],[c_267,c_618]) ).
tff(c_629,plain,
! [Y_208] :
( ( '#skF_7' = '#skF_9' )
| ( '#skF_7' = '#skF_10' )
| ( Y_208 = '#skF_6' )
| ( Y_208 = '#skF_9' )
| ( Y_208 = '#skF_10' )
| ( Y_208 = '#skF_7' )
| ~ rq('#skF_5',Y_208) ),
inference(negUnitSimplification,[status(thm)],[c_254,c_622]) ).
tff(c_637,plain,
'#skF_7' = '#skF_10',
inference(splitLeft,[status(thm)],[c_629]) ).
tff(c_271,plain,
cA('#skF_7'),
inference(resolution,[status(thm)],[c_267,c_34]) ).
tff(c_638,plain,
cA('#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_637,c_271]) ).
tff(c_642,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_306,c_638]) ).
tff(c_643,plain,
! [Y_208] :
( ( '#skF_7' = '#skF_9' )
| ( Y_208 = '#skF_6' )
| ( Y_208 = '#skF_9' )
| ( Y_208 = '#skF_10' )
| ( Y_208 = '#skF_7' )
| ~ rq('#skF_5',Y_208) ),
inference(splitRight,[status(thm)],[c_629]) ).
tff(c_658,plain,
'#skF_7' = '#skF_9',
inference(splitLeft,[status(thm)],[c_643]) ).
tff(c_660,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_658,c_271]) ).
tff(c_664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_319,c_660]) ).
tff(c_674,plain,
! [Y_219] :
( ( Y_219 = '#skF_6' )
| ( Y_219 = '#skF_9' )
| ( Y_219 = '#skF_10' )
| ( Y_219 = '#skF_7' )
| ~ rq('#skF_5',Y_219) ),
inference(splitRight,[status(thm)],[c_643]) ).
tff(c_683,plain,
( ( '#skF_6' = '#skF_8' )
| ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_8' )
| ( '#skF_7' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_281,c_674]) ).
tff(c_694,plain,
'#skF_7' = '#skF_8',
inference(negUnitSimplification,[status(thm)],[c_255,c_256,c_657,c_683]) ).
tff(c_698,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_694,c_271]) ).
tff(c_702,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_289,c_698]) ).
tff(c_713,plain,
! [Y2_224,Y3_221,Y0_223,Y4_222,Y1_220] :
( ( Y4_222 = Y3_221 )
| ( Y4_222 = Y2_224 )
| ( Y3_221 = Y2_224 )
| ( Y4_222 = Y1_220 )
| ( Y3_221 = Y1_220 )
| ( Y2_224 = Y1_220 )
| ( Y4_222 = Y0_223 )
| ( Y3_221 = Y0_223 )
| ( Y2_224 = Y0_223 )
| ( Y1_220 = Y0_223 )
| ~ rr('#skF_5',Y4_222)
| ~ rr('#skF_5',Y3_221)
| ~ rr('#skF_5',Y2_224)
| ~ rr('#skF_5',Y1_220)
| ~ rr('#skF_5',Y0_223) ),
inference(splitRight,[status(thm)],[c_329]) ).
tff(c_731,plain,
! [Y_231,Y1_233,Y2_230,Y3_234,Y0_232] :
( ( Y_231 = Y3_234 )
| ( Y_231 = Y2_230 )
| ( Y3_234 = Y2_230 )
| ( Y_231 = Y1_233 )
| ( Y3_234 = Y1_233 )
| ( Y2_230 = Y1_233 )
| ( Y_231 = Y0_232 )
| ( Y3_234 = Y0_232 )
| ( Y2_230 = Y0_232 )
| ( Y1_233 = Y0_232 )
| ~ rr('#skF_5',Y3_234)
| ~ rr('#skF_5',Y2_230)
| ~ rr('#skF_5',Y1_233)
| ~ rr('#skF_5',Y0_232)
| ~ rq('#skF_5',Y_231) ),
inference(resolution,[status(thm)],[c_40,c_713]) ).
tff(c_758,plain,
! [Y0_249,Y2_247,Y_248,Y_246,Y1_245] :
( ( Y_248 = Y_246 )
| ( Y_246 = Y2_247 )
| ( Y_248 = Y2_247 )
| ( Y_246 = Y1_245 )
| ( Y_248 = Y1_245 )
| ( Y2_247 = Y1_245 )
| ( Y_246 = Y0_249 )
| ( Y_248 = Y0_249 )
| ( Y2_247 = Y0_249 )
| ( Y1_245 = Y0_249 )
| ~ rr('#skF_5',Y2_247)
| ~ rr('#skF_5',Y1_245)
| ~ rr('#skF_5',Y0_249)
| ~ rq('#skF_5',Y_246)
| ~ rq('#skF_5',Y_248) ),
inference(resolution,[status(thm)],[c_40,c_731]) ).
tff(c_803,plain,
! [Y1_270,Y0_274,Y_272,Y_273,Y_271] :
( ( Y_273 = Y_271 )
| ( Y_272 = Y_271 )
| ( Y_273 = Y_272 )
| ( Y_271 = Y1_270 )
| ( Y_273 = Y1_270 )
| ( Y_272 = Y1_270 )
| ( Y_271 = Y0_274 )
| ( Y_273 = Y0_274 )
| ( Y_272 = Y0_274 )
| ( Y1_270 = Y0_274 )
| ~ rr('#skF_5',Y1_270)
| ~ rr('#skF_5',Y0_274)
| ~ rq('#skF_5',Y_271)
| ~ rq('#skF_5',Y_273)
| ~ rq('#skF_5',Y_272) ),
inference(resolution,[status(thm)],[c_40,c_758]) ).
tff(c_920,plain,
! [Y_339,Y_335,Y_336,Y_337,Y0_338] :
( ( Y_339 = Y_337 )
| ( Y_339 = Y_335 )
| ( Y_337 = Y_335 )
| ( Y_339 = Y_336 )
| ( Y_337 = Y_336 )
| ( Y_336 = Y_335 )
| ( Y_339 = Y0_338 )
| ( Y_337 = Y0_338 )
| ( Y_335 = Y0_338 )
| ( Y_336 = Y0_338 )
| ~ rr('#skF_5',Y0_338)
| ~ rq('#skF_5',Y_339)
| ~ rq('#skF_5',Y_337)
| ~ rq('#skF_5',Y_335)
| ~ rp('#skF_5',Y_336) ),
inference(resolution,[status(thm)],[c_42,c_803]) ).
tff(c_1030,plain,
! [Y_373,Y_372,Y_370,Y_374,Y_371] :
( ( Y_372 = Y_370 )
| ( Y_374 = Y_370 )
| ( Y_374 = Y_372 )
| ( Y_373 = Y_370 )
| ( Y_373 = Y_372 )
| ( Y_374 = Y_373 )
| ( Y_371 = Y_370 )
| ( Y_372 = Y_371 )
| ( Y_374 = Y_371 )
| ( Y_373 = Y_371 )
| ~ rq('#skF_5',Y_370)
| ~ rq('#skF_5',Y_372)
| ~ rq('#skF_5',Y_374)
| ~ rp('#skF_5',Y_373)
| ~ rq('#skF_5',Y_371) ),
inference(resolution,[status(thm)],[c_40,c_920]) ).
tff(c_1088,plain,
! [Y_385,Y_386,Y_387,Y_388] :
( ( Y_385 = '#skF_8' )
| ( Y_386 = '#skF_8' )
| ( Y_386 = Y_385 )
| ( Y_387 = '#skF_8' )
| ( Y_387 = Y_385 )
| ( Y_387 = Y_386 )
| ( Y_388 = '#skF_8' )
| ( Y_388 = Y_385 )
| ( Y_388 = Y_386 )
| ( Y_388 = Y_387 )
| ~ rq('#skF_5',Y_385)
| ~ rq('#skF_5',Y_386)
| ~ rp('#skF_5',Y_387)
| ~ rq('#skF_5',Y_388) ),
inference(resolution,[status(thm)],[c_281,c_1030]) ).
tff(c_1090,plain,
! [Y_386,Y_387,Y_388] :
( ( '#skF_9' = '#skF_8' )
| ( Y_386 = '#skF_8' )
| ( Y_386 = '#skF_9' )
| ( Y_387 = '#skF_8' )
| ( Y_387 = '#skF_9' )
| ( Y_387 = Y_386 )
| ( Y_388 = '#skF_8' )
| ( Y_388 = '#skF_9' )
| ( Y_388 = Y_386 )
| ( Y_388 = Y_387 )
| ~ rq('#skF_5',Y_386)
| ~ rp('#skF_5',Y_387)
| ~ rq('#skF_5',Y_388) ),
inference(resolution,[status(thm)],[c_311,c_1088]) ).
tff(c_1103,plain,
! [Y_389,Y_390,Y_391] :
( ( Y_389 = '#skF_8' )
| ( Y_389 = '#skF_9' )
| ( Y_390 = '#skF_8' )
| ( Y_390 = '#skF_9' )
| ( Y_390 = Y_389 )
| ( Y_391 = '#skF_8' )
| ( Y_391 = '#skF_9' )
| ( Y_391 = Y_389 )
| ( Y_391 = Y_390 )
| ~ rq('#skF_5',Y_389)
| ~ rp('#skF_5',Y_390)
| ~ rq('#skF_5',Y_391) ),
inference(negUnitSimplification,[status(thm)],[c_256,c_1090]) ).
tff(c_1107,plain,
! [Y_390,Y_391] :
( ( '#skF_10' = '#skF_8' )
| ( '#skF_10' = '#skF_9' )
| ( Y_390 = '#skF_8' )
| ( Y_390 = '#skF_9' )
| ( Y_390 = '#skF_10' )
| ( Y_391 = '#skF_8' )
| ( Y_391 = '#skF_9' )
| ( Y_391 = '#skF_10' )
| ( Y_391 = Y_390 )
| ~ rp('#skF_5',Y_390)
| ~ rq('#skF_5',Y_391) ),
inference(resolution,[status(thm)],[c_298,c_1103]) ).
tff(c_1121,plain,
! [Y_392,Y_393] :
( ( Y_392 = '#skF_8' )
| ( Y_392 = '#skF_9' )
| ( Y_392 = '#skF_10' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = Y_392 )
| ~ rp('#skF_5',Y_392)
| ~ rq('#skF_5',Y_393) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_255,c_1107]) ).
tff(c_1126,plain,
! [Y_393] :
( ( '#skF_6' = '#skF_8' )
| ( '#skF_6' = '#skF_9' )
| ( '#skF_10' = '#skF_6' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = '#skF_6' )
| ~ rq('#skF_5',Y_393) ),
inference(resolution,[status(thm)],[c_274,c_1121]) ).
tff(c_1128,plain,
'#skF_10' = '#skF_6',
inference(splitLeft,[status(thm)],[c_1126]) ).
tff(c_1134,plain,
~ cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1128,c_306]) ).
tff(c_1141,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_278,c_1134]) ).
tff(c_1142,plain,
! [Y_393] :
( ( '#skF_6' = '#skF_9' )
| ( '#skF_6' = '#skF_8' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = '#skF_6' )
| ~ rq('#skF_5',Y_393) ),
inference(splitRight,[status(thm)],[c_1126]) ).
tff(c_1151,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1142]) ).
tff(c_1155,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1151,c_278]) ).
tff(c_1159,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_289,c_1155]) ).
tff(c_1161,plain,
'#skF_6' != '#skF_8',
inference(splitRight,[status(thm)],[c_1142]) ).
tff(c_1127,plain,
! [Y_393] :
( ( '#skF_7' = '#skF_8' )
| ( '#skF_7' = '#skF_9' )
| ( '#skF_7' = '#skF_10' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = '#skF_7' )
| ~ rq('#skF_5',Y_393) ),
inference(resolution,[status(thm)],[c_267,c_1121]) ).
tff(c_1213,plain,
'#skF_7' = '#skF_10',
inference(splitLeft,[status(thm)],[c_1127]) ).
tff(c_1223,plain,
cA('#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_1213,c_271]) ).
tff(c_1227,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_306,c_1223]) ).
tff(c_1228,plain,
! [Y_393] :
( ( '#skF_7' = '#skF_9' )
| ( '#skF_7' = '#skF_8' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = '#skF_7' )
| ~ rq('#skF_5',Y_393) ),
inference(splitRight,[status(thm)],[c_1127]) ).
tff(c_1230,plain,
'#skF_7' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1228]) ).
tff(c_1247,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1230,c_271]) ).
tff(c_1251,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_289,c_1247]) ).
tff(c_1253,plain,
'#skF_7' != '#skF_8',
inference(splitRight,[status(thm)],[c_1228]) ).
tff(c_1143,plain,
'#skF_10' != '#skF_6',
inference(splitRight,[status(thm)],[c_1126]) ).
tff(c_1160,plain,
! [Y_393] :
( ( '#skF_6' = '#skF_9' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = '#skF_6' )
| ~ rq('#skF_5',Y_393) ),
inference(splitRight,[status(thm)],[c_1142]) ).
tff(c_1179,plain,
'#skF_6' = '#skF_9',
inference(splitLeft,[status(thm)],[c_1160]) ).
tff(c_1184,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_278]) ).
tff(c_1188,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_319,c_1184]) ).
tff(c_1190,plain,
'#skF_6' != '#skF_9',
inference(splitRight,[status(thm)],[c_1160]) ).
tff(c_1229,plain,
'#skF_7' != '#skF_10',
inference(splitRight,[status(thm)],[c_1127]) ).
tff(c_1252,plain,
! [Y_393] :
( ( '#skF_7' = '#skF_9' )
| ( Y_393 = '#skF_8' )
| ( Y_393 = '#skF_9' )
| ( Y_393 = '#skF_10' )
| ( Y_393 = '#skF_7' )
| ~ rq('#skF_5',Y_393) ),
inference(splitRight,[status(thm)],[c_1228]) ).
tff(c_1254,plain,
'#skF_7' = '#skF_9',
inference(splitLeft,[status(thm)],[c_1252]) ).
tff(c_1259,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_1254,c_271]) ).
tff(c_1263,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_319,c_1259]) ).
tff(c_1265,plain,
'#skF_7' != '#skF_9',
inference(splitRight,[status(thm)],[c_1252]) ).
tff(c_722,plain,
! [Y_227,Y1_228,Y3_229,Y0_226,Y2_225] :
( ( Y_227 = Y3_229 )
| ( Y_227 = Y2_225 )
| ( Y3_229 = Y2_225 )
| ( Y_227 = Y1_228 )
| ( Y3_229 = Y1_228 )
| ( Y2_225 = Y1_228 )
| ( Y_227 = Y0_226 )
| ( Y3_229 = Y0_226 )
| ( Y2_225 = Y0_226 )
| ( Y1_228 = Y0_226 )
| ~ rr('#skF_5',Y3_229)
| ~ rr('#skF_5',Y2_225)
| ~ rr('#skF_5',Y1_228)
| ~ rr('#skF_5',Y0_226)
| ~ rp('#skF_5',Y_227) ),
inference(resolution,[status(thm)],[c_42,c_713]) ).
tff(c_740,plain,
! [Y_237,Y0_238,Y_236,Y1_235,Y2_239] :
( ( Y_237 = Y_236 )
| ( Y_237 = Y2_239 )
| ( Y_236 = Y2_239 )
| ( Y_237 = Y1_235 )
| ( Y_236 = Y1_235 )
| ( Y2_239 = Y1_235 )
| ( Y_237 = Y0_238 )
| ( Y_236 = Y0_238 )
| ( Y2_239 = Y0_238 )
| ( Y1_235 = Y0_238 )
| ~ rr('#skF_5',Y2_239)
| ~ rr('#skF_5',Y1_235)
| ~ rr('#skF_5',Y0_238)
| ~ rp('#skF_5',Y_237)
| ~ rq('#skF_5',Y_236) ),
inference(resolution,[status(thm)],[c_40,c_722]) ).
tff(c_776,plain,
! [Y_257,Y_258,Y0_259,Y_256,Y1_255] :
( ( Y_258 = Y_257 )
| ( Y_258 = Y_256 )
| ( Y_257 = Y_256 )
| ( Y_258 = Y1_255 )
| ( Y_257 = Y1_255 )
| ( Y_256 = Y1_255 )
| ( Y_258 = Y0_259 )
| ( Y_257 = Y0_259 )
| ( Y_256 = Y0_259 )
| ( Y1_255 = Y0_259 )
| ~ rr('#skF_5',Y1_255)
| ~ rr('#skF_5',Y0_259)
| ~ rp('#skF_5',Y_258)
| ~ rq('#skF_5',Y_257)
| ~ rq('#skF_5',Y_256) ),
inference(resolution,[status(thm)],[c_40,c_740]) ).
tff(c_875,plain,
! [Y_313,Y_310,Y_314,Y0_311,Y_312] :
( ( Y_314 = Y_310 )
| ( Y_314 = Y_313 )
| ( Y_313 = Y_310 )
| ( Y_314 = Y_312 )
| ( Y_312 = Y_310 )
| ( Y_313 = Y_312 )
| ( Y_314 = Y0_311 )
| ( Y_310 = Y0_311 )
| ( Y_313 = Y0_311 )
| ( Y_312 = Y0_311 )
| ~ rr('#skF_5',Y0_311)
| ~ rp('#skF_5',Y_314)
| ~ rq('#skF_5',Y_310)
| ~ rq('#skF_5',Y_313)
| ~ rp('#skF_5',Y_312) ),
inference(resolution,[status(thm)],[c_42,c_776]) ).
tff(c_1266,plain,
! [Y_413,Y_415,Y_414,Y_416,Y_412] :
( ( Y_414 = Y_412 )
| ( Y_416 = Y_412 )
| ( Y_416 = Y_414 )
| ( Y_413 = Y_412 )
| ( Y_414 = Y_413 )
| ( Y_416 = Y_413 )
| ( Y_415 = Y_412 )
| ( Y_415 = Y_414 )
| ( Y_416 = Y_415 )
| ( Y_415 = Y_413 )
| ~ rp('#skF_5',Y_412)
| ~ rq('#skF_5',Y_414)
| ~ rq('#skF_5',Y_416)
| ~ rp('#skF_5',Y_413)
| ~ rq('#skF_5',Y_415) ),
inference(resolution,[status(thm)],[c_40,c_875]) ).
tff(c_1326,plain,
! [Y_425,Y_426,Y_427,Y_428] :
( ( Y_425 = '#skF_7' )
| ( Y_426 = '#skF_7' )
| ( Y_426 = Y_425 )
| ( Y_427 = '#skF_7' )
| ( Y_427 = Y_425 )
| ( Y_427 = Y_426 )
| ( Y_428 = '#skF_7' )
| ( Y_428 = Y_425 )
| ( Y_428 = Y_426 )
| ( Y_428 = Y_427 )
| ~ rq('#skF_5',Y_425)
| ~ rq('#skF_5',Y_426)
| ~ rp('#skF_5',Y_427)
| ~ rq('#skF_5',Y_428) ),
inference(resolution,[status(thm)],[c_267,c_1266]) ).
tff(c_1328,plain,
! [Y_426,Y_427,Y_428] :
( ( '#skF_7' = '#skF_9' )
| ( Y_426 = '#skF_7' )
| ( Y_426 = '#skF_9' )
| ( Y_427 = '#skF_7' )
| ( Y_427 = '#skF_9' )
| ( Y_427 = Y_426 )
| ( Y_428 = '#skF_7' )
| ( Y_428 = '#skF_9' )
| ( Y_428 = Y_426 )
| ( Y_428 = Y_427 )
| ~ rq('#skF_5',Y_426)
| ~ rp('#skF_5',Y_427)
| ~ rq('#skF_5',Y_428) ),
inference(resolution,[status(thm)],[c_311,c_1326]) ).
tff(c_1342,plain,
! [Y_429,Y_430,Y_431] :
( ( Y_429 = '#skF_7' )
| ( Y_429 = '#skF_9' )
| ( Y_430 = '#skF_7' )
| ( Y_430 = '#skF_9' )
| ( Y_430 = Y_429 )
| ( Y_431 = '#skF_7' )
| ( Y_431 = '#skF_9' )
| ( Y_431 = Y_429 )
| ( Y_431 = Y_430 )
| ~ rq('#skF_5',Y_429)
| ~ rp('#skF_5',Y_430)
| ~ rq('#skF_5',Y_431) ),
inference(negUnitSimplification,[status(thm)],[c_1265,c_1328]) ).
tff(c_1346,plain,
! [Y_430,Y_431] :
( ( '#skF_7' = '#skF_10' )
| ( '#skF_10' = '#skF_9' )
| ( Y_430 = '#skF_7' )
| ( Y_430 = '#skF_9' )
| ( Y_430 = '#skF_10' )
| ( Y_431 = '#skF_7' )
| ( Y_431 = '#skF_9' )
| ( Y_431 = '#skF_10' )
| ( Y_431 = Y_430 )
| ~ rp('#skF_5',Y_430)
| ~ rq('#skF_5',Y_431) ),
inference(resolution,[status(thm)],[c_298,c_1342]) ).
tff(c_1359,plain,
! [Y_432,Y_433] :
( ( Y_432 = '#skF_7' )
| ( Y_432 = '#skF_9' )
| ( Y_432 = '#skF_10' )
| ( Y_433 = '#skF_7' )
| ( Y_433 = '#skF_9' )
| ( Y_433 = '#skF_10' )
| ( Y_433 = Y_432 )
| ~ rp('#skF_5',Y_432)
| ~ rq('#skF_5',Y_433) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_1229,c_1346]) ).
tff(c_1361,plain,
! [Y_433] :
( ( '#skF_7' = '#skF_6' )
| ( '#skF_6' = '#skF_9' )
| ( '#skF_10' = '#skF_6' )
| ( Y_433 = '#skF_7' )
| ( Y_433 = '#skF_9' )
| ( Y_433 = '#skF_10' )
| ( Y_433 = '#skF_6' )
| ~ rq('#skF_5',Y_433) ),
inference(resolution,[status(thm)],[c_274,c_1359]) ).
tff(c_1371,plain,
! [Y_434] :
( ( Y_434 = '#skF_7' )
| ( Y_434 = '#skF_9' )
| ( Y_434 = '#skF_10' )
| ( Y_434 = '#skF_6' )
| ~ rq('#skF_5',Y_434) ),
inference(negUnitSimplification,[status(thm)],[c_1143,c_1190,c_254,c_1361]) ).
tff(c_1380,plain,
( ( '#skF_7' = '#skF_8' )
| ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_8' )
| ( '#skF_6' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_281,c_1371]) ).
tff(c_1392,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1161,c_255,c_256,c_1253,c_1380]) ).
tff(c_1394,plain,
~ rq('#skF_5','#skF_9'),
inference(splitRight,[status(thm)],[c_310]) ).
tff(c_1393,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_310]) ).
tff(c_1398,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1393,c_30]) ).
tff(c_86,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_137,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_86]) ).
tff(c_192,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_137]) ).
tff(c_1403,plain,
( xsd_integer('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_192]) ).
tff(c_1404,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1394,c_1398,c_1403]) ).
tff(c_1406,plain,
~ rq('#skF_5','#skF_10'),
inference(splitRight,[status(thm)],[c_297]) ).
tff(c_1405,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_297]) ).
tff(c_1410,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1405,c_30]) ).
tff(c_78,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_162,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_78]) ).
tff(c_242,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_162]) ).
tff(c_1433,plain,
( xsd_integer('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_242]) ).
tff(c_1434,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1406,c_1410,c_1433]) ).
tff(c_1436,plain,
~ rq('#skF_5','#skF_8'),
inference(splitRight,[status(thm)],[c_280]) ).
tff(c_1435,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_280]) ).
tff(c_1440,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1435,c_30]) ).
tff(c_94,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_146,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_94]) ).
tff(c_210,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_146]) ).
tff(c_1479,plain,
( xsd_integer('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_210]) ).
tff(c_1480,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1436,c_1440,c_1479]) ).
tff(c_1481,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_273]) ).
tff(c_1482,plain,
~ rp('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_273]) ).
tff(c_122,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_161,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_122]) ).
tff(c_240,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_161]) ).
tff(c_1485,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_240]) ).
tff(c_1486,plain,
xsd_string('#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1482,c_1485]) ).
tff(c_1489,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1486,c_30]) ).
tff(c_1493,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1481,c_1489]) ).
tff(c_1495,plain,
~ rp('#skF_5','#skF_7'),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_1494,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_266]) ).
tff(c_1499,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1494,c_30]) ).
tff(c_110,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_145,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_110]) ).
tff(c_208,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_145]) ).
tff(c_1529,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_264,c_208]) ).
tff(c_1530,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1495,c_1499,c_1529]) ).
tff(c_1532,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_232]) ).
tff(c_96,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_144,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_96]) ).
tff(c_206,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_144]) ).
tff(c_2051,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_206]) ).
tff(c_2052,plain,
rq('#skF_5','#skF_8'),
inference(splitLeft,[status(thm)],[c_2051]) ).
tff(c_2056,plain,
cB('#skF_8'),
inference(resolution,[status(thm)],[c_2052,c_36]) ).
tff(c_2060,plain,
~ cA('#skF_8'),
inference(resolution,[status(thm)],[c_2056,c_38]) ).
tff(c_1531,plain,
( rq('#skF_5','#skF_9')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_232]) ).
tff(c_1537,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_1531]) ).
tff(c_1554,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_206]) ).
tff(c_1555,plain,
rq('#skF_5','#skF_8'),
inference(splitLeft,[status(thm)],[c_1554]) ).
tff(c_1559,plain,
cB('#skF_8'),
inference(resolution,[status(thm)],[c_1555,c_36]) ).
tff(c_1563,plain,
~ cA('#skF_8'),
inference(resolution,[status(thm)],[c_1559,c_38]) ).
tff(c_88,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_152,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_9')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_88]) ).
tff(c_222,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_152]) ).
tff(c_1585,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_222]) ).
tff(c_1586,plain,
rq('#skF_5','#skF_9'),
inference(splitLeft,[status(thm)],[c_1585]) ).
tff(c_1590,plain,
cB('#skF_9'),
inference(resolution,[status(thm)],[c_1586,c_36]) ).
tff(c_1594,plain,
~ cA('#skF_9'),
inference(resolution,[status(thm)],[c_1590,c_38]) ).
tff(c_120,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_134,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_120]) ).
tff(c_186,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_134]) ).
tff(c_1545,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_186]) ).
tff(c_1546,plain,
rp('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_1545]) ).
tff(c_1550,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_1546,c_34]) ).
tff(c_80,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_160,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_80]) ).
tff(c_238,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_160]) ).
tff(c_1566,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_238]) ).
tff(c_1567,plain,
rq('#skF_5','#skF_10'),
inference(splitLeft,[status(thm)],[c_1566]) ).
tff(c_1571,plain,
cB('#skF_10'),
inference(resolution,[status(thm)],[c_1567,c_36]) ).
tff(c_1575,plain,
~ cA('#skF_10'),
inference(resolution,[status(thm)],[c_1571,c_38]) ).
tff(c_112,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_141,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_112]) ).
tff(c_200,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_141]) ).
tff(c_1577,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_200]) ).
tff(c_1578,plain,
rp('#skF_5','#skF_7'),
inference(splitLeft,[status(thm)],[c_1577]) ).
tff(c_48,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_154,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_48]) ).
tff(c_226,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_154]) ).
tff(c_1599,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( xsd_string('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_226]) ).
tff(c_1600,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_1599]) ).
tff(c_1603,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1600,c_30]) ).
tff(c_1607,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1537,c_1603]) ).
tff(c_1617,plain,
! [Y0_438,Y2_439,Y3_436,Y4_437,Y1_435] :
( ( Y4_437 = Y3_436 )
| ( Y4_437 = Y2_439 )
| ( Y3_436 = Y2_439 )
| ( Y4_437 = Y1_435 )
| ( Y3_436 = Y1_435 )
| ( Y2_439 = Y1_435 )
| ( Y4_437 = Y0_438 )
| ( Y3_436 = Y0_438 )
| ( Y2_439 = Y0_438 )
| ( Y1_435 = Y0_438 )
| ~ rr('#skF_5',Y4_437)
| ~ rr('#skF_5',Y3_436)
| ~ rr('#skF_5',Y2_439)
| ~ rr('#skF_5',Y1_435)
| ~ rr('#skF_5',Y0_438) ),
inference(splitRight,[status(thm)],[c_1599]) ).
tff(c_1635,plain,
! [Y0_447,Y3_449,Y2_448,Y1_445,Y_446] :
( ( Y_446 = Y3_449 )
| ( Y_446 = Y2_448 )
| ( Y3_449 = Y2_448 )
| ( Y_446 = Y1_445 )
| ( Y3_449 = Y1_445 )
| ( Y2_448 = Y1_445 )
| ( Y_446 = Y0_447 )
| ( Y3_449 = Y0_447 )
| ( Y2_448 = Y0_447 )
| ( Y1_445 = Y0_447 )
| ~ rr('#skF_5',Y3_449)
| ~ rr('#skF_5',Y2_448)
| ~ rr('#skF_5',Y1_445)
| ~ rr('#skF_5',Y0_447)
| ~ rq('#skF_5',Y_446) ),
inference(resolution,[status(thm)],[c_40,c_1617]) ).
tff(c_1654,plain,
! [Y2_456,Y1_457,Y_459,Y0_455,Y_458] :
( ( Y_459 = Y_458 )
| ( Y_459 = Y2_456 )
| ( Y_458 = Y2_456 )
| ( Y_459 = Y1_457 )
| ( Y_458 = Y1_457 )
| ( Y2_456 = Y1_457 )
| ( Y_459 = Y0_455 )
| ( Y_458 = Y0_455 )
| ( Y2_456 = Y0_455 )
| ( Y1_457 = Y0_455 )
| ~ rr('#skF_5',Y2_456)
| ~ rr('#skF_5',Y1_457)
| ~ rr('#skF_5',Y0_455)
| ~ rq('#skF_5',Y_459)
| ~ rq('#skF_5',Y_458) ),
inference(resolution,[status(thm)],[c_40,c_1635]) ).
tff(c_1672,plain,
! [Y_468,Y0_469,Y_465,Y_466,Y1_467] :
( ( Y_466 = Y_465 )
| ( Y_468 = Y_465 )
| ( Y_468 = Y_466 )
| ( Y_465 = Y1_467 )
| ( Y_466 = Y1_467 )
| ( Y_468 = Y1_467 )
| ( Y_465 = Y0_469 )
| ( Y_466 = Y0_469 )
| ( Y_468 = Y0_469 )
| ( Y1_467 = Y0_469 )
| ~ rr('#skF_5',Y1_467)
| ~ rr('#skF_5',Y0_469)
| ~ rq('#skF_5',Y_465)
| ~ rq('#skF_5',Y_466)
| ~ rp('#skF_5',Y_468) ),
inference(resolution,[status(thm)],[c_42,c_1654]) ).
tff(c_1816,plain,
! [Y0_547,Y_546,Y_549,Y_545,Y_548] :
( ( Y_546 = Y_545 )
| ( Y_549 = Y_546 )
| ( Y_549 = Y_545 )
| ( Y_548 = Y_546 )
| ( Y_548 = Y_545 )
| ( Y_549 = Y_548 )
| ( Y_546 = Y0_547 )
| ( Y_545 = Y0_547 )
| ( Y_549 = Y0_547 )
| ( Y_548 = Y0_547 )
| ~ rr('#skF_5',Y0_547)
| ~ rq('#skF_5',Y_546)
| ~ rq('#skF_5',Y_545)
| ~ rp('#skF_5',Y_549)
| ~ rp('#skF_5',Y_548) ),
inference(resolution,[status(thm)],[c_42,c_1672]) ).
tff(c_1834,plain,
! [Y_558,Y_555,Y_557,Y_556,Y_559] :
( ( Y_556 = Y_555 )
| ( Y_557 = Y_556 )
| ( Y_557 = Y_555 )
| ( Y_559 = Y_556 )
| ( Y_559 = Y_555 )
| ( Y_559 = Y_557 )
| ( Y_558 = Y_556 )
| ( Y_558 = Y_555 )
| ( Y_558 = Y_557 )
| ( Y_559 = Y_558 )
| ~ rq('#skF_5',Y_556)
| ~ rq('#skF_5',Y_555)
| ~ rp('#skF_5',Y_557)
| ~ rp('#skF_5',Y_559)
| ~ rq('#skF_5',Y_558) ),
inference(resolution,[status(thm)],[c_40,c_1816]) ).
tff(c_1844,plain,
! [Y_560,Y_561,Y_562,Y_563] :
( ( Y_560 = '#skF_9' )
| ( Y_561 = '#skF_9' )
| ( Y_561 = Y_560 )
| ( Y_562 = '#skF_9' )
| ( Y_562 = Y_560 )
| ( Y_562 = Y_561 )
| ( Y_563 = '#skF_9' )
| ( Y_563 = Y_560 )
| ( Y_563 = Y_561 )
| ( Y_563 = Y_562 )
| ~ rq('#skF_5',Y_560)
| ~ rp('#skF_5',Y_561)
| ~ rp('#skF_5',Y_562)
| ~ rq('#skF_5',Y_563) ),
inference(resolution,[status(thm)],[c_1586,c_1834]) ).
tff(c_1848,plain,
! [Y_561,Y_562,Y_563] :
( ( '#skF_10' = '#skF_9' )
| ( Y_561 = '#skF_9' )
| ( Y_561 = '#skF_10' )
| ( Y_562 = '#skF_9' )
| ( Y_562 = '#skF_10' )
| ( Y_562 = Y_561 )
| ( Y_563 = '#skF_9' )
| ( Y_563 = '#skF_10' )
| ( Y_563 = Y_561 )
| ( Y_563 = Y_562 )
| ~ rp('#skF_5',Y_561)
| ~ rp('#skF_5',Y_562)
| ~ rq('#skF_5',Y_563) ),
inference(resolution,[status(thm)],[c_1567,c_1844]) ).
tff(c_1859,plain,
! [Y_564,Y_565,Y_566] :
( ( Y_564 = '#skF_9' )
| ( Y_564 = '#skF_10' )
| ( Y_565 = '#skF_9' )
| ( Y_565 = '#skF_10' )
| ( Y_565 = Y_564 )
| ( Y_566 = '#skF_9' )
| ( Y_566 = '#skF_10' )
| ( Y_566 = Y_564 )
| ( Y_566 = Y_565 )
| ~ rp('#skF_5',Y_564)
| ~ rp('#skF_5',Y_565)
| ~ rq('#skF_5',Y_566) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_1848]) ).
tff(c_1864,plain,
! [Y_565,Y_566] :
( ( '#skF_7' = '#skF_9' )
| ( '#skF_7' = '#skF_10' )
| ( Y_565 = '#skF_9' )
| ( Y_565 = '#skF_10' )
| ( Y_565 = '#skF_7' )
| ( Y_566 = '#skF_9' )
| ( Y_566 = '#skF_10' )
| ( Y_566 = '#skF_7' )
| ( Y_566 = Y_565 )
| ~ rp('#skF_5',Y_565)
| ~ rq('#skF_5',Y_566) ),
inference(resolution,[status(thm)],[c_1578,c_1859]) ).
tff(c_1866,plain,
'#skF_7' = '#skF_10',
inference(splitLeft,[status(thm)],[c_1864]) ).
tff(c_1582,plain,
cA('#skF_7'),
inference(resolution,[status(thm)],[c_1578,c_34]) ).
tff(c_1867,plain,
cA('#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_1866,c_1582]) ).
tff(c_1871,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1575,c_1867]) ).
tff(c_1872,plain,
! [Y_565,Y_566] :
( ( '#skF_7' = '#skF_9' )
| ( Y_565 = '#skF_9' )
| ( Y_565 = '#skF_10' )
| ( Y_565 = '#skF_7' )
| ( Y_566 = '#skF_9' )
| ( Y_566 = '#skF_10' )
| ( Y_566 = '#skF_7' )
| ( Y_566 = Y_565 )
| ~ rp('#skF_5',Y_565)
| ~ rq('#skF_5',Y_566) ),
inference(splitRight,[status(thm)],[c_1864]) ).
tff(c_1874,plain,
'#skF_7' = '#skF_9',
inference(splitLeft,[status(thm)],[c_1872]) ).
tff(c_1876,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_1874,c_1582]) ).
tff(c_1880,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1594,c_1876]) ).
tff(c_1890,plain,
! [Y_572,Y_573] :
( ( Y_572 = '#skF_9' )
| ( Y_572 = '#skF_10' )
| ( Y_572 = '#skF_7' )
| ( Y_573 = '#skF_9' )
| ( Y_573 = '#skF_10' )
| ( Y_573 = '#skF_7' )
| ( Y_573 = Y_572 )
| ~ rp('#skF_5',Y_572)
| ~ rq('#skF_5',Y_573) ),
inference(splitRight,[status(thm)],[c_1872]) ).
tff(c_1894,plain,
! [Y_573] :
( ( '#skF_6' = '#skF_9' )
| ( '#skF_10' = '#skF_6' )
| ( '#skF_7' = '#skF_6' )
| ( Y_573 = '#skF_9' )
| ( Y_573 = '#skF_10' )
| ( Y_573 = '#skF_7' )
| ( Y_573 = '#skF_6' )
| ~ rq('#skF_5',Y_573) ),
inference(resolution,[status(thm)],[c_1546,c_1890]) ).
tff(c_1901,plain,
! [Y_573] :
( ( '#skF_6' = '#skF_9' )
| ( '#skF_10' = '#skF_6' )
| ( Y_573 = '#skF_9' )
| ( Y_573 = '#skF_10' )
| ( Y_573 = '#skF_7' )
| ( Y_573 = '#skF_6' )
| ~ rq('#skF_5',Y_573) ),
inference(negUnitSimplification,[status(thm)],[c_254,c_1894]) ).
tff(c_1902,plain,
'#skF_10' = '#skF_6',
inference(splitLeft,[status(thm)],[c_1901]) ).
tff(c_1915,plain,
~ cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1902,c_1575]) ).
tff(c_1922,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1550,c_1915]) ).
tff(c_1923,plain,
! [Y_573] :
( ( '#skF_6' = '#skF_9' )
| ( Y_573 = '#skF_9' )
| ( Y_573 = '#skF_10' )
| ( Y_573 = '#skF_7' )
| ( Y_573 = '#skF_6' )
| ~ rq('#skF_5',Y_573) ),
inference(splitRight,[status(thm)],[c_1901]) ).
tff(c_1925,plain,
'#skF_6' = '#skF_9',
inference(splitLeft,[status(thm)],[c_1923]) ).
tff(c_1927,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_1925,c_1550]) ).
tff(c_1931,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1594,c_1927]) ).
tff(c_1941,plain,
! [Y_582] :
( ( Y_582 = '#skF_9' )
| ( Y_582 = '#skF_10' )
| ( Y_582 = '#skF_7' )
| ( Y_582 = '#skF_6' )
| ~ rq('#skF_5',Y_582) ),
inference(splitRight,[status(thm)],[c_1923]) ).
tff(c_1950,plain,
( ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_8' )
| ( '#skF_7' = '#skF_8' )
| ( '#skF_6' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1555,c_1941]) ).
tff(c_1961,plain,
( ( '#skF_7' = '#skF_8' )
| ( '#skF_6' = '#skF_8' ) ),
inference(negUnitSimplification,[status(thm)],[c_255,c_256,c_1950]) ).
tff(c_1962,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1961]) ).
tff(c_1966,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1962,c_1550]) ).
tff(c_1970,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1563,c_1966]) ).
tff(c_1971,plain,
'#skF_7' = '#skF_8',
inference(splitRight,[status(thm)],[c_1961]) ).
tff(c_1988,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1971,c_1582]) ).
tff(c_1992,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1563,c_1988]) ).
tff(c_1993,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1585]) ).
tff(c_1997,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1993,c_30]) ).
tff(c_2001,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1537,c_1997]) ).
tff(c_2002,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1577]) ).
tff(c_2006,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2002,c_30]) ).
tff(c_2010,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1537,c_2006]) ).
tff(c_2011,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1566]) ).
tff(c_2015,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2011,c_30]) ).
tff(c_2019,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1537,c_2015]) ).
tff(c_2020,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1554]) ).
tff(c_2024,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2020,c_30]) ).
tff(c_2028,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1537,c_2024]) ).
tff(c_2029,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1545]) ).
tff(c_2033,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2029,c_30]) ).
tff(c_2037,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1537,c_2033]) ).
tff(c_2038,plain,
rq('#skF_5','#skF_9'),
inference(splitRight,[status(thm)],[c_1531]) ).
tff(c_2043,plain,
cB('#skF_9'),
inference(resolution,[status(thm)],[c_2038,c_36]) ).
tff(c_2049,plain,
~ cA('#skF_9'),
inference(resolution,[status(thm)],[c_2043,c_38]) ).
tff(c_2039,plain,
~ xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1531]) ).
tff(c_108,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_149,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_108]) ).
tff(c_216,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_149]) ).
tff(c_2062,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_216]) ).
tff(c_2063,plain,
rp('#skF_5','#skF_7'),
inference(negUnitSimplification,[status(thm)],[c_2039,c_2062]) ).
tff(c_44,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_156,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52)
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_44]) ).
tff(c_230,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_156]) ).
tff(c_2112,plain,
! [Y3_55,Y2_54,Y0_52,Y1_53,Y4_56] :
( xsd_integer('#skF_4')
| ( Y4_56 = Y3_55 )
| ( Y4_56 = Y2_54 )
| ( Y3_55 = Y2_54 )
| ( Y4_56 = Y1_53 )
| ( Y3_55 = Y1_53 )
| ( Y2_54 = Y1_53 )
| ( Y4_56 = Y0_52 )
| ( Y3_55 = Y0_52 )
| ( Y2_54 = Y0_52 )
| ( Y1_53 = Y0_52 )
| ~ rr('#skF_5',Y4_56)
| ~ rr('#skF_5',Y3_55)
| ~ rr('#skF_5',Y2_54)
| ~ rr('#skF_5',Y1_53)
| ~ rr('#skF_5',Y0_52) ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_230]) ).
tff(c_2114,plain,
! [Y4_588,Y0_589,Y2_590,Y1_586,Y3_587] :
( ( Y4_588 = Y3_587 )
| ( Y4_588 = Y2_590 )
| ( Y3_587 = Y2_590 )
| ( Y4_588 = Y1_586 )
| ( Y3_587 = Y1_586 )
| ( Y2_590 = Y1_586 )
| ( Y4_588 = Y0_589 )
| ( Y3_587 = Y0_589 )
| ( Y2_590 = Y0_589 )
| ( Y1_586 = Y0_589 )
| ~ rr('#skF_5',Y4_588)
| ~ rr('#skF_5',Y3_587)
| ~ rr('#skF_5',Y2_590)
| ~ rr('#skF_5',Y1_586)
| ~ rr('#skF_5',Y0_589) ),
inference(negUnitSimplification,[status(thm)],[c_2039,c_2112]) ).
tff(c_2125,plain,
! [Y_594,Y0_592,Y1_595,Y3_593,Y2_591] :
( ( Y_594 = Y3_593 )
| ( Y_594 = Y2_591 )
| ( Y3_593 = Y2_591 )
| ( Y_594 = Y1_595 )
| ( Y3_593 = Y1_595 )
| ( Y2_591 = Y1_595 )
| ( Y_594 = Y0_592 )
| ( Y3_593 = Y0_592 )
| ( Y2_591 = Y0_592 )
| ( Y1_595 = Y0_592 )
| ~ rr('#skF_5',Y3_593)
| ~ rr('#skF_5',Y2_591)
| ~ rr('#skF_5',Y1_595)
| ~ rr('#skF_5',Y0_592)
| ~ rq('#skF_5',Y_594) ),
inference(resolution,[status(thm)],[c_40,c_2114]) ).
tff(c_2152,plain,
! [Y0_606,Y_609,Y1_607,Y2_610,Y_608] :
( ( Y_609 = Y_608 )
| ( Y_609 = Y2_610 )
| ( Y_608 = Y2_610 )
| ( Y_609 = Y1_607 )
| ( Y_608 = Y1_607 )
| ( Y2_610 = Y1_607 )
| ( Y_609 = Y0_606 )
| ( Y_608 = Y0_606 )
| ( Y2_610 = Y0_606 )
| ( Y1_607 = Y0_606 )
| ~ rr('#skF_5',Y2_610)
| ~ rr('#skF_5',Y1_607)
| ~ rr('#skF_5',Y0_606)
| ~ rq('#skF_5',Y_609)
| ~ rp('#skF_5',Y_608) ),
inference(resolution,[status(thm)],[c_42,c_2125]) ).
tff(c_2171,plain,
! [Y0_617,Y_620,Y_618,Y1_616,Y_619] :
( ( Y_620 = Y_618 )
| ( Y_620 = Y_619 )
| ( Y_619 = Y_618 )
| ( Y_620 = Y1_616 )
| ( Y_618 = Y1_616 )
| ( Y_619 = Y1_616 )
| ( Y_620 = Y0_617 )
| ( Y_618 = Y0_617 )
| ( Y_619 = Y0_617 )
| ( Y1_616 = Y0_617 )
| ~ rr('#skF_5',Y1_616)
| ~ rr('#skF_5',Y0_617)
| ~ rq('#skF_5',Y_620)
| ~ rp('#skF_5',Y_618)
| ~ rq('#skF_5',Y_619) ),
inference(resolution,[status(thm)],[c_40,c_2152]) ).
tff(c_2270,plain,
! [Y_673,Y_675,Y_671,Y0_674,Y_672] :
( ( Y_675 = Y_673 )
| ( Y_673 = Y_671 )
| ( Y_675 = Y_671 )
| ( Y_673 = Y_672 )
| ( Y_675 = Y_672 )
| ( Y_672 = Y_671 )
| ( Y_673 = Y0_674 )
| ( Y_675 = Y0_674 )
| ( Y_671 = Y0_674 )
| ( Y_672 = Y0_674 )
| ~ rr('#skF_5',Y0_674)
| ~ rq('#skF_5',Y_673)
| ~ rp('#skF_5',Y_675)
| ~ rq('#skF_5',Y_671)
| ~ rq('#skF_5',Y_672) ),
inference(resolution,[status(thm)],[c_40,c_2171]) ).
tff(c_2333,plain,
! [Y_707,Y_710,Y_709,Y_706,Y_708] :
( ( Y_710 = Y_706 )
| ( Y_709 = Y_706 )
| ( Y_710 = Y_709 )
| ( Y_707 = Y_706 )
| ( Y_710 = Y_707 )
| ( Y_709 = Y_707 )
| ( Y_708 = Y_706 )
| ( Y_710 = Y_708 )
| ( Y_709 = Y_708 )
| ( Y_708 = Y_707 )
| ~ rq('#skF_5',Y_706)
| ~ rp('#skF_5',Y_710)
| ~ rq('#skF_5',Y_709)
| ~ rq('#skF_5',Y_707)
| ~ rq('#skF_5',Y_708) ),
inference(resolution,[status(thm)],[c_40,c_2270]) ).
tff(c_2343,plain,
! [Y_711,Y_712,Y_713,Y_714] :
( ( Y_711 = '#skF_9' )
| ( Y_712 = '#skF_9' )
| ( Y_712 = Y_711 )
| ( Y_713 = '#skF_9' )
| ( Y_713 = Y_711 )
| ( Y_713 = Y_712 )
| ( Y_714 = '#skF_9' )
| ( Y_714 = Y_711 )
| ( Y_714 = Y_712 )
| ( Y_714 = Y_713 )
| ~ rp('#skF_5',Y_711)
| ~ rq('#skF_5',Y_712)
| ~ rq('#skF_5',Y_713)
| ~ rq('#skF_5',Y_714) ),
inference(resolution,[status(thm)],[c_2038,c_2333]) ).
tff(c_2349,plain,
! [Y_712,Y_713,Y_714] :
( ( '#skF_7' = '#skF_9' )
| ( Y_712 = '#skF_9' )
| ( Y_712 = '#skF_7' )
| ( Y_713 = '#skF_9' )
| ( Y_713 = '#skF_7' )
| ( Y_713 = Y_712 )
| ( Y_714 = '#skF_9' )
| ( Y_714 = '#skF_7' )
| ( Y_714 = Y_712 )
| ( Y_714 = Y_713 )
| ~ rq('#skF_5',Y_712)
| ~ rq('#skF_5',Y_713)
| ~ rq('#skF_5',Y_714) ),
inference(resolution,[status(thm)],[c_2063,c_2343]) ).
tff(c_2478,plain,
'#skF_7' = '#skF_9',
inference(splitLeft,[status(thm)],[c_2349]) ).
tff(c_2067,plain,
cA('#skF_7'),
inference(resolution,[status(thm)],[c_2063,c_34]) ).
tff(c_2479,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_2478,c_2067]) ).
tff(c_2483,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2049,c_2479]) ).
tff(c_2501,plain,
! [Y_737,Y_738,Y_739] :
( ( Y_737 = '#skF_9' )
| ( Y_737 = '#skF_7' )
| ( Y_738 = '#skF_9' )
| ( Y_738 = '#skF_7' )
| ( Y_738 = Y_737 )
| ( Y_739 = '#skF_9' )
| ( Y_739 = '#skF_7' )
| ( Y_739 = Y_737 )
| ( Y_739 = Y_738 )
| ~ rq('#skF_5',Y_737)
| ~ rq('#skF_5',Y_738)
| ~ rq('#skF_5',Y_739) ),
inference(splitRight,[status(thm)],[c_2349]) ).
tff(c_2505,plain,
! [Y_738,Y_739] :
( ( '#skF_9' = '#skF_8' )
| ( '#skF_7' = '#skF_8' )
| ( Y_738 = '#skF_9' )
| ( Y_738 = '#skF_7' )
| ( Y_738 = '#skF_8' )
| ( Y_739 = '#skF_9' )
| ( Y_739 = '#skF_7' )
| ( Y_739 = '#skF_8' )
| ( Y_739 = Y_738 )
| ~ rq('#skF_5',Y_738)
| ~ rq('#skF_5',Y_739) ),
inference(resolution,[status(thm)],[c_2052,c_2501]) ).
tff(c_2513,plain,
! [Y_738,Y_739] :
( ( '#skF_7' = '#skF_8' )
| ( Y_738 = '#skF_9' )
| ( Y_738 = '#skF_7' )
| ( Y_738 = '#skF_8' )
| ( Y_739 = '#skF_9' )
| ( Y_739 = '#skF_7' )
| ( Y_739 = '#skF_8' )
| ( Y_739 = Y_738 )
| ~ rq('#skF_5',Y_738)
| ~ rq('#skF_5',Y_739) ),
inference(negUnitSimplification,[status(thm)],[c_256,c_2505]) ).
tff(c_2565,plain,
'#skF_7' = '#skF_8',
inference(splitLeft,[status(thm)],[c_2513]) ).
tff(c_2570,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2565,c_2067]) ).
tff(c_2574,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2060,c_2570]) ).
tff(c_2576,plain,
'#skF_7' != '#skF_8',
inference(splitRight,[status(thm)],[c_2513]) ).
tff(c_116,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_136,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_116]) ).
tff(c_236,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_136]) ).
tff(c_2082,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_236]) ).
tff(c_2083,plain,
rp('#skF_5','#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_2039,c_2082]) ).
tff(c_2348,plain,
! [Y_712,Y_713,Y_714] :
( ( '#skF_6' = '#skF_9' )
| ( Y_712 = '#skF_9' )
| ( Y_712 = '#skF_6' )
| ( Y_713 = '#skF_9' )
| ( Y_713 = '#skF_6' )
| ( Y_713 = Y_712 )
| ( Y_714 = '#skF_9' )
| ( Y_714 = '#skF_6' )
| ( Y_714 = Y_712 )
| ( Y_714 = Y_713 )
| ~ rq('#skF_5',Y_712)
| ~ rq('#skF_5',Y_713)
| ~ rq('#skF_5',Y_714) ),
inference(resolution,[status(thm)],[c_2083,c_2343]) ).
tff(c_2350,plain,
'#skF_6' = '#skF_9',
inference(splitLeft,[status(thm)],[c_2348]) ).
tff(c_2087,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_2083,c_34]) ).
tff(c_2352,plain,
cA('#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_2350,c_2087]) ).
tff(c_2356,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2049,c_2352]) ).
tff(c_2359,plain,
! [Y_715,Y_716,Y_717] :
( ( Y_715 = '#skF_9' )
| ( Y_715 = '#skF_6' )
| ( Y_716 = '#skF_9' )
| ( Y_716 = '#skF_6' )
| ( Y_716 = Y_715 )
| ( Y_717 = '#skF_9' )
| ( Y_717 = '#skF_6' )
| ( Y_717 = Y_715 )
| ( Y_717 = Y_716 )
| ~ rq('#skF_5',Y_715)
| ~ rq('#skF_5',Y_716)
| ~ rq('#skF_5',Y_717) ),
inference(splitRight,[status(thm)],[c_2348]) ).
tff(c_2363,plain,
! [Y_716,Y_717] :
( ( '#skF_9' = '#skF_8' )
| ( '#skF_6' = '#skF_8' )
| ( Y_716 = '#skF_9' )
| ( Y_716 = '#skF_6' )
| ( Y_716 = '#skF_8' )
| ( Y_717 = '#skF_9' )
| ( Y_717 = '#skF_6' )
| ( Y_717 = '#skF_8' )
| ( Y_717 = Y_716 )
| ~ rq('#skF_5',Y_716)
| ~ rq('#skF_5',Y_717) ),
inference(resolution,[status(thm)],[c_2052,c_2359]) ).
tff(c_2371,plain,
! [Y_716,Y_717] :
( ( '#skF_6' = '#skF_8' )
| ( Y_716 = '#skF_9' )
| ( Y_716 = '#skF_6' )
| ( Y_716 = '#skF_8' )
| ( Y_717 = '#skF_9' )
| ( Y_717 = '#skF_6' )
| ( Y_717 = '#skF_8' )
| ( Y_717 = Y_716 )
| ~ rq('#skF_5',Y_716)
| ~ rq('#skF_5',Y_717) ),
inference(negUnitSimplification,[status(thm)],[c_256,c_2363]) ).
tff(c_2416,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_2371]) ).
tff(c_2421,plain,
cA('#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2416,c_2087]) ).
tff(c_2425,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2060,c_2421]) ).
tff(c_2427,plain,
'#skF_6' != '#skF_8',
inference(splitRight,[status(thm)],[c_2371]) ).
tff(c_2070,plain,
( xsd_string('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_238]) ).
tff(c_2071,plain,
rq('#skF_5','#skF_10'),
inference(splitLeft,[status(thm)],[c_2070]) ).
tff(c_2361,plain,
! [Y_716,Y_717] :
( ( '#skF_10' = '#skF_9' )
| ( '#skF_10' = '#skF_6' )
| ( Y_716 = '#skF_9' )
| ( Y_716 = '#skF_6' )
| ( Y_716 = '#skF_10' )
| ( Y_717 = '#skF_9' )
| ( Y_717 = '#skF_6' )
| ( Y_717 = '#skF_10' )
| ( Y_717 = Y_716 )
| ~ rq('#skF_5',Y_716)
| ~ rq('#skF_5',Y_717) ),
inference(resolution,[status(thm)],[c_2071,c_2359]) ).
tff(c_2368,plain,
! [Y_716,Y_717] :
( ( '#skF_10' = '#skF_6' )
| ( Y_716 = '#skF_9' )
| ( Y_716 = '#skF_6' )
| ( Y_716 = '#skF_10' )
| ( Y_717 = '#skF_9' )
| ( Y_717 = '#skF_6' )
| ( Y_717 = '#skF_10' )
| ( Y_717 = Y_716 )
| ~ rq('#skF_5',Y_716)
| ~ rq('#skF_5',Y_717) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_2361]) ).
tff(c_2376,plain,
'#skF_10' = '#skF_6',
inference(splitLeft,[status(thm)],[c_2368]) ).
tff(c_2075,plain,
cB('#skF_10'),
inference(resolution,[status(thm)],[c_2071,c_36]) ).
tff(c_2079,plain,
~ cA('#skF_10'),
inference(resolution,[status(thm)],[c_2075,c_38]) ).
tff(c_2377,plain,
~ cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_2376,c_2079]) ).
tff(c_2384,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2087,c_2377]) ).
tff(c_2397,plain,
! [Y_723,Y_724] :
( ( Y_723 = '#skF_9' )
| ( Y_723 = '#skF_6' )
| ( Y_723 = '#skF_10' )
| ( Y_724 = '#skF_9' )
| ( Y_724 = '#skF_6' )
| ( Y_724 = '#skF_10' )
| ( Y_724 = Y_723 )
| ~ rq('#skF_5',Y_723)
| ~ rq('#skF_5',Y_724) ),
inference(splitRight,[status(thm)],[c_2368]) ).
tff(c_2401,plain,
! [Y_724] :
( ( '#skF_9' = '#skF_8' )
| ( '#skF_6' = '#skF_8' )
| ( '#skF_10' = '#skF_8' )
| ( Y_724 = '#skF_9' )
| ( Y_724 = '#skF_6' )
| ( Y_724 = '#skF_10' )
| ( Y_724 = '#skF_8' )
| ~ rq('#skF_5',Y_724) ),
inference(resolution,[status(thm)],[c_2052,c_2397]) ).
tff(c_2410,plain,
! [Y_724] :
( ( '#skF_6' = '#skF_8' )
| ( Y_724 = '#skF_9' )
| ( Y_724 = '#skF_6' )
| ( Y_724 = '#skF_10' )
| ( Y_724 = '#skF_8' )
| ~ rq('#skF_5',Y_724) ),
inference(negUnitSimplification,[status(thm)],[c_255,c_256,c_2401]) ).
tff(c_2415,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_2410]) ).
tff(c_2428,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2427,c_2415]) ).
tff(c_2430,plain,
'#skF_6' != '#skF_8',
inference(splitRight,[status(thm)],[c_2410]) ).
tff(c_2503,plain,
! [Y_738,Y_739] :
( ( '#skF_10' = '#skF_9' )
| ( '#skF_7' = '#skF_10' )
| ( Y_738 = '#skF_9' )
| ( Y_738 = '#skF_7' )
| ( Y_738 = '#skF_10' )
| ( Y_739 = '#skF_9' )
| ( Y_739 = '#skF_7' )
| ( Y_739 = '#skF_10' )
| ( Y_739 = Y_738 )
| ~ rq('#skF_5',Y_738)
| ~ rq('#skF_5',Y_739) ),
inference(resolution,[status(thm)],[c_2071,c_2501]) ).
tff(c_2510,plain,
! [Y_738,Y_739] :
( ( '#skF_7' = '#skF_10' )
| ( Y_738 = '#skF_9' )
| ( Y_738 = '#skF_7' )
| ( Y_738 = '#skF_10' )
| ( Y_739 = '#skF_9' )
| ( Y_739 = '#skF_7' )
| ( Y_739 = '#skF_10' )
| ( Y_739 = Y_738 )
| ~ rq('#skF_5',Y_738)
| ~ rq('#skF_5',Y_739) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_2503]) ).
tff(c_2518,plain,
'#skF_7' = '#skF_10',
inference(splitLeft,[status(thm)],[c_2510]) ).
tff(c_2521,plain,
cA('#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_2518,c_2067]) ).
tff(c_2525,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2079,c_2521]) ).
tff(c_2527,plain,
'#skF_7' != '#skF_10',
inference(splitRight,[status(thm)],[c_2510]) ).
tff(c_2386,plain,
'#skF_10' != '#skF_6',
inference(splitRight,[status(thm)],[c_2368]) ).
tff(c_2485,plain,
'#skF_7' != '#skF_9',
inference(splitRight,[status(thm)],[c_2349]) ).
tff(c_2358,plain,
'#skF_6' != '#skF_9',
inference(splitRight,[status(thm)],[c_2348]) ).
tff(c_2134,plain,
! [Y2_596,Y1_600,Y_599,Y0_597,Y3_598] :
( ( Y_599 = Y3_598 )
| ( Y_599 = Y2_596 )
| ( Y3_598 = Y2_596 )
| ( Y_599 = Y1_600 )
| ( Y3_598 = Y1_600 )
| ( Y2_596 = Y1_600 )
| ( Y_599 = Y0_597 )
| ( Y3_598 = Y0_597 )
| ( Y2_596 = Y0_597 )
| ( Y1_600 = Y0_597 )
| ~ rr('#skF_5',Y3_598)
| ~ rr('#skF_5',Y2_596)
| ~ rr('#skF_5',Y1_600)
| ~ rr('#skF_5',Y0_597)
| ~ rp('#skF_5',Y_599) ),
inference(resolution,[status(thm)],[c_42,c_2114]) ).
tff(c_2161,plain,
! [Y_614,Y0_613,Y_612,Y1_611,Y2_615] :
( ( Y_614 = Y_612 )
| ( Y_614 = Y2_615 )
| ( Y_612 = Y2_615 )
| ( Y_614 = Y1_611 )
| ( Y_612 = Y1_611 )
| ( Y2_615 = Y1_611 )
| ( Y_614 = Y0_613 )
| ( Y_612 = Y0_613 )
| ( Y2_615 = Y0_613 )
| ( Y1_611 = Y0_613 )
| ~ rr('#skF_5',Y2_615)
| ~ rr('#skF_5',Y1_611)
| ~ rr('#skF_5',Y0_613)
| ~ rp('#skF_5',Y_614)
| ~ rp('#skF_5',Y_612) ),
inference(resolution,[status(thm)],[c_42,c_2134]) ).
tff(c_2189,plain,
! [Y_628,Y_630,Y1_629,Y_627,Y0_626] :
( ( Y_630 = Y_628 )
| ( Y_628 = Y_627 )
| ( Y_630 = Y_627 )
| ( Y_628 = Y1_629 )
| ( Y_630 = Y1_629 )
| ( Y_627 = Y1_629 )
| ( Y_628 = Y0_626 )
| ( Y_630 = Y0_626 )
| ( Y_627 = Y0_626 )
| ( Y1_629 = Y0_626 )
| ~ rr('#skF_5',Y1_629)
| ~ rr('#skF_5',Y0_626)
| ~ rp('#skF_5',Y_628)
| ~ rp('#skF_5',Y_630)
| ~ rq('#skF_5',Y_627) ),
inference(resolution,[status(thm)],[c_40,c_2161]) ).
tff(c_2306,plain,
! [Y_695,Y_692,Y_693,Y0_691,Y_694] :
( ( Y_695 = Y_694 )
| ( Y_695 = Y_692 )
| ( Y_694 = Y_692 )
| ( Y_695 = Y_693 )
| ( Y_694 = Y_693 )
| ( Y_693 = Y_692 )
| ( Y_695 = Y0_691 )
| ( Y_694 = Y0_691 )
| ( Y_692 = Y0_691 )
| ( Y_693 = Y0_691 )
| ~ rr('#skF_5',Y0_691)
| ~ rp('#skF_5',Y_695)
| ~ rp('#skF_5',Y_694)
| ~ rq('#skF_5',Y_692)
| ~ rq('#skF_5',Y_693) ),
inference(resolution,[status(thm)],[c_40,c_2189]) ).
tff(c_2528,plain,
! [Y_742,Y_744,Y_741,Y_743,Y_740] :
( ( Y_743 = Y_742 )
| ( Y_744 = Y_742 )
| ( Y_744 = Y_743 )
| ( Y_742 = Y_740 )
| ( Y_743 = Y_740 )
| ( Y_744 = Y_740 )
| ( Y_742 = Y_741 )
| ( Y_743 = Y_741 )
| ( Y_744 = Y_741 )
| ( Y_741 = Y_740 )
| ~ rp('#skF_5',Y_742)
| ~ rp('#skF_5',Y_743)
| ~ rq('#skF_5',Y_744)
| ~ rq('#skF_5',Y_740)
| ~ rq('#skF_5',Y_741) ),
inference(resolution,[status(thm)],[c_40,c_2306]) ).
tff(c_2641,plain,
! [Y_761,Y_762,Y_763,Y_764] :
( ( Y_761 = '#skF_6' )
| ( Y_762 = '#skF_6' )
| ( Y_762 = Y_761 )
| ( Y_763 = '#skF_6' )
| ( Y_763 = Y_761 )
| ( Y_763 = Y_762 )
| ( Y_764 = '#skF_6' )
| ( Y_764 = Y_761 )
| ( Y_764 = Y_762 )
| ( Y_764 = Y_763 )
| ~ rp('#skF_5',Y_761)
| ~ rq('#skF_5',Y_762)
| ~ rq('#skF_5',Y_763)
| ~ rq('#skF_5',Y_764) ),
inference(resolution,[status(thm)],[c_2083,c_2528]) ).
tff(c_2645,plain,
! [Y_762,Y_763,Y_764] :
( ( '#skF_7' = '#skF_6' )
| ( Y_762 = '#skF_6' )
| ( Y_762 = '#skF_7' )
| ( Y_763 = '#skF_6' )
| ( Y_763 = '#skF_7' )
| ( Y_763 = Y_762 )
| ( Y_764 = '#skF_6' )
| ( Y_764 = '#skF_7' )
| ( Y_764 = Y_762 )
| ( Y_764 = Y_763 )
| ~ rq('#skF_5',Y_762)
| ~ rq('#skF_5',Y_763)
| ~ rq('#skF_5',Y_764) ),
inference(resolution,[status(thm)],[c_2063,c_2641]) ).
tff(c_2651,plain,
! [Y_765,Y_766,Y_767] :
( ( Y_765 = '#skF_6' )
| ( Y_765 = '#skF_7' )
| ( Y_766 = '#skF_6' )
| ( Y_766 = '#skF_7' )
| ( Y_766 = Y_765 )
| ( Y_767 = '#skF_6' )
| ( Y_767 = '#skF_7' )
| ( Y_767 = Y_765 )
| ( Y_767 = Y_766 )
| ~ rq('#skF_5',Y_765)
| ~ rq('#skF_5',Y_766)
| ~ rq('#skF_5',Y_767) ),
inference(negUnitSimplification,[status(thm)],[c_254,c_2645]) ).
tff(c_2657,plain,
! [Y_766,Y_767] :
( ( '#skF_6' = '#skF_9' )
| ( '#skF_7' = '#skF_9' )
| ( Y_766 = '#skF_6' )
| ( Y_766 = '#skF_7' )
| ( Y_766 = '#skF_9' )
| ( Y_767 = '#skF_6' )
| ( Y_767 = '#skF_7' )
| ( Y_767 = '#skF_9' )
| ( Y_767 = Y_766 )
| ~ rq('#skF_5',Y_766)
| ~ rq('#skF_5',Y_767) ),
inference(resolution,[status(thm)],[c_2038,c_2651]) ).
tff(c_2667,plain,
! [Y_768,Y_769] :
( ( Y_768 = '#skF_6' )
| ( Y_768 = '#skF_7' )
| ( Y_768 = '#skF_9' )
| ( Y_769 = '#skF_6' )
| ( Y_769 = '#skF_7' )
| ( Y_769 = '#skF_9' )
| ( Y_769 = Y_768 )
| ~ rq('#skF_5',Y_768)
| ~ rq('#skF_5',Y_769) ),
inference(negUnitSimplification,[status(thm)],[c_2485,c_2358,c_2657]) ).
tff(c_2669,plain,
! [Y_769] :
( ( '#skF_10' = '#skF_6' )
| ( '#skF_7' = '#skF_10' )
| ( '#skF_10' = '#skF_9' )
| ( Y_769 = '#skF_6' )
| ( Y_769 = '#skF_7' )
| ( Y_769 = '#skF_9' )
| ( Y_769 = '#skF_10' )
| ~ rq('#skF_5',Y_769) ),
inference(resolution,[status(thm)],[c_2071,c_2667]) ).
tff(c_2684,plain,
! [Y_770] :
( ( Y_770 = '#skF_6' )
| ( Y_770 = '#skF_7' )
| ( Y_770 = '#skF_9' )
| ( Y_770 = '#skF_10' )
| ~ rq('#skF_5',Y_770) ),
inference(negUnitSimplification,[status(thm)],[c_257,c_2527,c_2386,c_2669]) ).
tff(c_2690,plain,
( ( '#skF_6' = '#skF_8' )
| ( '#skF_7' = '#skF_8' )
| ( '#skF_9' = '#skF_8' )
| ( '#skF_10' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_2052,c_2684]) ).
tff(c_2701,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_255,c_256,c_2576,c_2430,c_2690]) ).
tff(c_2703,plain,
~ rq('#skF_5','#skF_10'),
inference(splitRight,[status(thm)],[c_2070]) ).
tff(c_76,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_140,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_10')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_76]) ).
tff(c_198,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_140]) ).
tff(c_2723,plain,
( xsd_integer('#skF_4')
| rq('#skF_5','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_198]) ).
tff(c_2724,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2703,c_2039,c_2723]) ).
tff(c_2726,plain,
~ rq('#skF_5','#skF_8'),
inference(splitRight,[status(thm)],[c_2051]) ).
tff(c_92,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_148,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_92]) ).
tff(c_214,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_148]) ).
tff(c_2759,plain,
( xsd_integer('#skF_4')
| rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1532,c_214]) ).
tff(c_2760,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2726,c_2039,c_2759]) ).
tff(c_2762,plain,
'#skF_10' = '#skF_9',
inference(splitRight,[status(thm)],[c_188]) ).
tff(c_2761,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_188]) ).
tff(c_2768,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2761]) ).
tff(c_2772,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_32,c_2768]) ).
tff(c_54,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_151,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_54]) ).
tff(c_220,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_9' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_151]) ).
tff(c_2774,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2762,c_2772,c_220]) ).
tff(c_58,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_127,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_58]) ).
tff(c_172,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_9' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_127]) ).
tff(c_2783,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2762,c_2772,c_172]) ).
tff(c_2786,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2783,c_30]) ).
tff(c_2790,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2774,c_2786]) ).
tff(c_2791,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_2761]) ).
tff(c_2796,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2791,c_30]) ).
tff(c_2792,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2761]) ).
tff(c_52,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_128,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_9' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_52]) ).
tff(c_174,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_9' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_128]) ).
tff(c_2813,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2762,c_2792,c_174]) ).
tff(c_2814,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2796,c_2813]) ).
tff(c_2816,plain,
'#skF_9' = '#skF_8',
inference(splitRight,[status(thm)],[c_180]) ).
tff(c_2815,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_180]) ).
tff(c_2821,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2815]) ).
tff(c_2825,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_32,c_2821]) ).
tff(c_74,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_125,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_74]) ).
tff(c_168,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_9' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_125]) ).
tff(c_2839,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2816,c_2825,c_168]) ).
tff(c_2843,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2839,c_30]) ).
tff(c_70,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_143,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_70]) ).
tff(c_204,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_9' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_143]) ).
tff(c_2845,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2816,c_2825,c_204]) ).
tff(c_2846,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2843,c_2845]) ).
tff(c_2847,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_2815]) ).
tff(c_2852,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2847,c_30]) ).
tff(c_2848,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2815]) ).
tff(c_68,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_126,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_9' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_68]) ).
tff(c_170,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_9' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_126]) ).
tff(c_2872,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2816,c_2848,c_170]) ).
tff(c_2873,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2852,c_2872]) ).
tff(c_2874,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_178]) ).
tff(c_2880,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_2874]) ).
tff(c_2875,plain,
'#skF_10' = '#skF_8',
inference(splitRight,[status(thm)],[c_178]) ).
tff(c_60,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_124,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_60]) ).
tff(c_166,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_10' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_124]) ).
tff(c_2885,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_2875,c_166]) ).
tff(c_2886,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2885]) ).
tff(c_2889,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_32,c_2886]) ).
tff(c_2893,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2880,c_2889]) ).
tff(c_2894,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2885]) ).
tff(c_2895,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2885]) ).
tff(c_64,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_133,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_64]) ).
tff(c_184,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_133]) ).
tff(c_2903,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2875,c_2895,c_184]) ).
tff(c_2906,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2903,c_30]) ).
tff(c_2910,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2894,c_2906]) ).
tff(c_2911,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2874]) ).
tff(c_2912,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_2874]) ).
tff(c_66,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_132,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_8' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_66]) ).
tff(c_182,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_10' != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_132]) ).
tff(c_2915,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2875,c_2912,c_182]) ).
tff(c_2918,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2915,c_30]) ).
tff(c_2922,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2911,c_2918]) ).
tff(c_2923,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_2929,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_2923]) ).
tff(c_2924,plain,
'#skF_7' = '#skF_6',
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_100,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_123,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_100]) ).
tff(c_164,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_6' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_123]) ).
tff(c_2936,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_2924,c_164]) ).
tff(c_2937,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2936]) ).
tff(c_2940,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_32,c_2937]) ).
tff(c_2944,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2929,c_2940]) ).
tff(c_2945,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2936]) ).
tff(c_2946,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2936]) ).
tff(c_104,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_139,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_104]) ).
tff(c_196,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_6' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_139]) ).
tff(c_2959,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2924,c_2946,c_196]) ).
tff(c_2962,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2959,c_30]) ).
tff(c_2966,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2945,c_2962]) ).
tff(c_2967,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2923]) ).
tff(c_2968,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_2923]) ).
tff(c_106,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_129,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_6' )
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_28,c_106]) ).
tff(c_176,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_6' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_129]) ).
tff(c_2983,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2924,c_2968,c_176]) ).
tff(c_2986,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2983,c_30]) ).
tff(c_2990,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2967,c_2986]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS162+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/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.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 03:00:35 EDT 2025
% 0.13/0.34 % CPUTime :
% 10.10/4.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.32/4.12
% 10.32/4.12 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------