%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS138+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:07:25 PM UTC 2025
% Result : Theorem 6.62s 2.49s
% Output : CNFRefutation 7.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 11
% Syntax : Number of formulae : 666 ( 374 unt; 0 typ; 0 def)
% Number of atoms : 1872 ( 337 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 2147 ( 941 ~;1189 |; 10 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 11 con; 0-0 aty)
% Number of variables : 73 ( 73 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ requalityOnA > xsd_string > xsd_integer > cowlThing > cowlNothing > cA > #nlpp > ic > ib > ia > #skF_7 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_8 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(requalityOnA,type,
requalityOnA: ( $i * $i ) > $o ).
tff(cA,type,
cA: $i > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff('#skF_7',type,
'#skF_7': $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(ib,type,
ib: $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(ia,type,
ia: $i ).
tff(ic,type,
ic: $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(f_81,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
tff(f_75,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
tff(f_102,axiom,
cowlThing(ia),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
tff(f_103,axiom,
requalityOnA(ia,ia),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
tff(f_105,axiom,
cowlThing(ib),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
tff(f_108,axiom,
cowlThing(ic),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
tff(f_149,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X,Y] :
( requalityOnA(X,Y)
=> ( ( X = ia )
| ( X = ib )
| ( X = ic ) ) )
& ! [X,Y] :
( requalityOnA(X,Y)
=> requalityOnA(Y,X) )
& cowlThing(ia)
& requalityOnA(ia,ia)
& cowlThing(ib)
& cowlThing(ic) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
tff(f_100,axiom,
! [X,Y] :
( requalityOnA(X,Y)
=> cA(Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
tff(f_88,axiom,
! [X] :
( cA(X)
<=> ( ( X = ib )
| ( X = ia ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
tff(f_106,axiom,
requalityOnA(ib,ib),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
tff(f_95,axiom,
! [X,Y,Z] :
( ( requalityOnA(Y,X)
& requalityOnA(Z,X) )
=> ( Y = Z ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
tff(c_22,plain,
! [X_18] :
( xsd_string(X_18)
| xsd_integer(X_18) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_16,plain,
! [X_17] : cowlThing(X_17),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_18,plain,
! [X_17] : ~ cowlNothing(X_17),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_34,plain,
cowlThing(ia),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_36,plain,
requalityOnA(ia,ia),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_38,plain,
cowlThing(ib),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_42,plain,
cowlThing(ic),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_104,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_148,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_104]) ).
tff(c_210,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_148]) ).
tff(c_274,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_210]) ).
tff(c_338,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_274]) ).
tff(c_376,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_338]) ).
tff(c_425,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_376]) ).
tff(c_515,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_425]) ).
tff(c_519,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_515]) ).
tff(c_102,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_154,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_102]) ).
tff(c_216,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_154]) ).
tff(c_280,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_216]) ).
tff(c_344,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_280]) ).
tff(c_379,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_344]) ).
tff(c_431,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_379]) ).
tff(c_523,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_519,c_431]) ).
tff(c_524,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_523]) ).
tff(c_32,plain,
! [Y_24,X_23] :
( cA(Y_24)
| ~ requalityOnA(X_23,Y_24) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_531,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_524,c_32]) ).
tff(c_24,plain,
! [X_19] :
( ( ia = X_19 )
| ( ib = X_19 )
| ~ cA(X_19) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_535,plain,
( ( ia = '#skF_8' )
| ( ib = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_531,c_24]) ).
tff(c_536,plain,
ib = '#skF_8',
inference(splitLeft,[status(thm)],[c_535]) ).
tff(c_40,plain,
requalityOnA(ib,ib),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_540,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_536,c_536,c_40]) ).
tff(c_30,plain,
! [Z_22,Y_21,X_20] :
( ( Z_22 = Y_21 )
| ~ requalityOnA(Z_22,X_20)
| ~ requalityOnA(Y_21,X_20) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_557,plain,
! [Y_37] :
( ( Y_37 = '#skF_7' )
| ~ requalityOnA(Y_37,'#skF_8') ),
inference(resolution,[status(thm)],[c_524,c_30]) ).
tff(c_564,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_540,c_557]) ).
tff(c_46,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_168,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_46]) ).
tff(c_230,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_168]) ).
tff(c_294,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_230]) ).
tff(c_358,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_294]) ).
tff(c_386,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_358]) ).
tff(c_445,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ic != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_386]) ).
tff(c_481,plain,
~ requalityOnA('#skF_8','#skF_7'),
inference(splitLeft,[status(thm)],[c_445]) ).
tff(c_569,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_564,c_481]) ).
tff(c_573,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_540,c_569]) ).
tff(c_574,plain,
ia = '#skF_8',
inference(splitRight,[status(thm)],[c_535]) ).
tff(c_581,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_574,c_574,c_36]) ).
tff(c_596,plain,
! [Y_38] :
( ( Y_38 = '#skF_7' )
| ~ requalityOnA(Y_38,'#skF_8') ),
inference(resolution,[status(thm)],[c_524,c_30]) ).
tff(c_603,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_581,c_596]) ).
tff(c_618,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_603,c_481]) ).
tff(c_622,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_581,c_618]) ).
tff(c_623,plain,
( requalityOnA('#skF_5','#skF_6')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_523]) ).
tff(c_625,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_623]) ).
tff(c_624,plain,
~ requalityOnA('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_523]) ).
tff(c_106,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_124,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_106]) ).
tff(c_186,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_124]) ).
tff(c_250,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_186]) ).
tff(c_340,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_250]) ).
tff(c_377,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_340]) ).
tff(c_427,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_377]) ).
tff(c_628,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_519,c_427]) ).
tff(c_629,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(negUnitSimplification,[status(thm)],[c_624,c_628]) ).
tff(c_630,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_629]) ).
tff(c_637,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_630,c_32]) ).
tff(c_641,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_637,c_24]) ).
tff(c_642,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_641]) ).
tff(c_88,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_116,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_88]) ).
tff(c_178,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_116]) ).
tff(c_242,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_178]) ).
tff(c_306,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_242]) ).
tff(c_390,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_306]) ).
tff(c_453,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_390]) ).
tff(c_512,plain,
ib != '#skF_5',
inference(splitLeft,[status(thm)],[c_453]) ).
tff(c_649,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_642,c_512]) ).
tff(c_652,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_642,c_642,c_40]) ).
tff(c_636,plain,
! [Y_21] :
( ( Y_21 = '#skF_5' )
| ~ requalityOnA(Y_21,'#skF_6') ),
inference(resolution,[status(thm)],[c_630,c_30]) ).
tff(c_661,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_652,c_636]) ).
tff(c_670,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_649,c_661]) ).
tff(c_671,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_641]) ).
tff(c_96,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_112,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_96]) ).
tff(c_182,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_112]) ).
tff(c_246,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_182]) ).
tff(c_310,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_246]) ).
tff(c_373,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_310]) ).
tff(c_419,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_373]) ).
tff(c_513,plain,
ia != '#skF_5',
inference(splitLeft,[status(thm)],[c_419]) ).
tff(c_679,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_671,c_513]) ).
tff(c_682,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_671,c_671,c_36]) ).
tff(c_691,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_682,c_636]) ).
tff(c_700,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_679,c_691]) ).
tff(c_701,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_629]) ).
tff(c_20,plain,
! [X_18] :
( ~ xsd_integer(X_18)
| ~ xsd_string(X_18) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_705,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_701,c_20]) ).
tff(c_709,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_625,c_705]) ).
tff(c_710,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_623]) ).
tff(c_719,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_710,c_32]) ).
tff(c_723,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_719,c_24]) ).
tff(c_727,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_723]) ).
tff(c_728,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_727,c_512]) ).
tff(c_731,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_727,c_727,c_40]) ).
tff(c_746,plain,
! [Y_42] :
( ( Y_42 = '#skF_5' )
| ~ requalityOnA(Y_42,'#skF_6') ),
inference(resolution,[status(thm)],[c_710,c_30]) ).
tff(c_749,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_731,c_746]) ).
tff(c_756,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_728,c_749]) ).
tff(c_757,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_723]) ).
tff(c_765,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_757,c_513]) ).
tff(c_768,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_757,c_757,c_36]) ).
tff(c_718,plain,
! [Y_21] :
( ( Y_21 = '#skF_5' )
| ~ requalityOnA(Y_21,'#skF_6') ),
inference(resolution,[status(thm)],[c_710,c_30]) ).
tff(c_777,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_768,c_718]) ).
tff(c_786,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_765,c_777]) ).
tff(c_787,plain,
( requalityOnA('#skF_7','#skF_8')
| requalityOnA('#skF_5','#skF_6')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_425]) ).
tff(c_793,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_787]) ).
tff(c_797,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_793,c_20]) ).
tff(c_788,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_425]) ).
tff(c_100,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_170,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_100]) ).
tff(c_232,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_170]) ).
tff(c_296,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_232]) ).
tff(c_360,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_296]) ).
tff(c_387,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_360]) ).
tff(c_447,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_387]) ).
tff(c_802,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_788,c_447]) ).
tff(c_803,plain,
( requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(negUnitSimplification,[status(thm)],[c_797,c_802]) ).
tff(c_804,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_803]) ).
tff(c_814,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_804,c_32]) ).
tff(c_818,plain,
( ( ia = '#skF_8' )
| ( ib = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_814,c_24]) ).
tff(c_819,plain,
ib = '#skF_8',
inference(splitLeft,[status(thm)],[c_818]) ).
tff(c_823,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_819,c_819,c_40]) ).
tff(c_813,plain,
! [Y_21] :
( ( Y_21 = '#skF_7' )
| ~ requalityOnA(Y_21,'#skF_8') ),
inference(resolution,[status(thm)],[c_804,c_30]) ).
tff(c_844,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_823,c_813]) ).
tff(c_850,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_844,c_481]) ).
tff(c_854,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_823,c_850]) ).
tff(c_855,plain,
ia = '#skF_8',
inference(splitRight,[status(thm)],[c_818]) ).
tff(c_860,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_855,c_855,c_36]) ).
tff(c_875,plain,
! [Y_45] :
( ( Y_45 = '#skF_7' )
| ~ requalityOnA(Y_45,'#skF_8') ),
inference(resolution,[status(thm)],[c_804,c_30]) ).
tff(c_882,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_860,c_875]) ).
tff(c_887,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_882,c_481]) ).
tff(c_891,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_860,c_887]) ).
tff(c_892,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_803]) ).
tff(c_900,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_892,c_32]) ).
tff(c_904,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_900,c_24]) ).
tff(c_905,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_904]) ).
tff(c_906,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_905,c_512]) ).
tff(c_909,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_905,c_905,c_40]) ).
tff(c_927,plain,
! [Y_46] :
( ( Y_46 = '#skF_5' )
| ~ requalityOnA(Y_46,'#skF_6') ),
inference(resolution,[status(thm)],[c_892,c_30]) ).
tff(c_930,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_909,c_927]) ).
tff(c_937,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_906,c_930]) ).
tff(c_938,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_904]) ).
tff(c_940,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_938,c_513]) ).
tff(c_943,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_938,c_938,c_36]) ).
tff(c_961,plain,
! [Y_47] :
( ( Y_47 = '#skF_5' )
| ~ requalityOnA(Y_47,'#skF_6') ),
inference(resolution,[status(thm)],[c_892,c_30]) ).
tff(c_964,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_943,c_961]) ).
tff(c_971,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_940,c_964]) ).
tff(c_972,plain,
( requalityOnA('#skF_5','#skF_6')
| requalityOnA('#skF_7','#skF_8') ),
inference(splitRight,[status(thm)],[c_787]) ).
tff(c_980,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_972]) ).
tff(c_987,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_980,c_32]) ).
tff(c_991,plain,
( ( ia = '#skF_8' )
| ( ib = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_987,c_24]) ).
tff(c_993,plain,
ib = '#skF_8',
inference(splitLeft,[status(thm)],[c_991]) ).
tff(c_997,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_993,c_993,c_40]) ).
tff(c_1014,plain,
! [Y_48] :
( ( Y_48 = '#skF_7' )
| ~ requalityOnA(Y_48,'#skF_8') ),
inference(resolution,[status(thm)],[c_980,c_30]) ).
tff(c_1021,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_997,c_1014]) ).
tff(c_1026,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1021,c_481]) ).
tff(c_1030,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_997,c_1026]) ).
tff(c_1031,plain,
ia = '#skF_8',
inference(splitRight,[status(thm)],[c_991]) ).
tff(c_1036,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1031,c_1031,c_36]) ).
tff(c_1053,plain,
! [Y_49] :
( ( Y_49 = '#skF_7' )
| ~ requalityOnA(Y_49,'#skF_8') ),
inference(resolution,[status(thm)],[c_980,c_30]) ).
tff(c_1060,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1036,c_1053]) ).
tff(c_1066,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1060,c_481]) ).
tff(c_1070,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1036,c_1066]) ).
tff(c_1071,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_972]) ).
tff(c_1079,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_1071,c_32]) ).
tff(c_1083,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_1079,c_24]) ).
tff(c_1084,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_1083]) ).
tff(c_1087,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_1084,c_512]) ).
tff(c_1090,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1084,c_1084,c_40]) ).
tff(c_1107,plain,
! [Y_50] :
( ( Y_50 = '#skF_5' )
| ~ requalityOnA(Y_50,'#skF_6') ),
inference(resolution,[status(thm)],[c_1071,c_30]) ).
tff(c_1110,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1090,c_1107]) ).
tff(c_1117,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1087,c_1110]) ).
tff(c_1118,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_1083]) ).
tff(c_1120,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_1118,c_513]) ).
tff(c_1123,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1118,c_1118,c_36]) ).
tff(c_1140,plain,
! [Y_51] :
( ( Y_51 = '#skF_5' )
| ~ requalityOnA(Y_51,'#skF_6') ),
inference(resolution,[status(thm)],[c_1071,c_30]) ).
tff(c_1143,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1123,c_1140]) ).
tff(c_1150,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1120,c_1143]) ).
tff(c_1152,plain,
ia = '#skF_5',
inference(splitRight,[status(thm)],[c_419]) ).
tff(c_1151,plain,
( ~ xsd_string('#skF_3')
| requalityOnA('#skF_7','#skF_8')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_419]) ).
tff(c_1190,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1151]) ).
tff(c_1194,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_1190]) ).
tff(c_94,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_120,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_94]) ).
tff(c_200,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_120]) ).
tff(c_264,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_200]) ).
tff(c_328,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_264]) ).
tff(c_391,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_328]) ).
tff(c_455,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_391]) ).
tff(c_1196,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1152,c_1194,c_455]) ).
tff(c_1197,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1196]) ).
tff(c_1204,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_1197,c_32]) ).
tff(c_1154,plain,
! [X_19] :
( ( X_19 = '#skF_5' )
| ( ib = X_19 )
| ~ cA(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_1152,c_24]) ).
tff(c_1210,plain,
( ( '#skF_5' = '#skF_8' )
| ( ib = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1204,c_1154]) ).
tff(c_1211,plain,
ib = '#skF_8',
inference(splitLeft,[status(thm)],[c_1210]) ).
tff(c_1215,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1211,c_1211,c_40]) ).
tff(c_1230,plain,
! [Y_54] :
( ( Y_54 = '#skF_7' )
| ~ requalityOnA(Y_54,'#skF_8') ),
inference(resolution,[status(thm)],[c_1197,c_30]) ).
tff(c_1237,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1215,c_1230]) ).
tff(c_1242,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1237,c_481]) ).
tff(c_1246,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1215,c_1242]) ).
tff(c_1247,plain,
'#skF_5' = '#skF_8',
inference(splitRight,[status(thm)],[c_1210]) ).
tff(c_1155,plain,
requalityOnA('#skF_5','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1152,c_1152,c_36]) ).
tff(c_1251,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1247,c_1247,c_1155]) ).
tff(c_1272,plain,
! [Y_55] :
( ( Y_55 = '#skF_7' )
| ~ requalityOnA(Y_55,'#skF_8') ),
inference(resolution,[status(thm)],[c_1197,c_30]) ).
tff(c_1279,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1251,c_1272]) ).
tff(c_1284,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1279,c_481]) ).
tff(c_1288,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1251,c_1284]) ).
tff(c_1289,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1196]) ).
tff(c_98,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_108,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_98]) ).
tff(c_174,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_108]) ).
tff(c_238,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_174]) ).
tff(c_302,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_238]) ).
tff(c_364,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_302]) ).
tff(c_401,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_364]) ).
tff(c_1292,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1152,c_1194,c_401]) ).
tff(c_1293,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1292]) ).
tff(c_1290,plain,
~ requalityOnA('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1196]) ).
tff(c_1306,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1293,c_1290]) ).
tff(c_1307,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1292]) ).
tff(c_1311,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1307,c_20]) ).
tff(c_1315,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1289,c_1311]) ).
tff(c_1316,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(splitRight,[status(thm)],[c_1151]) ).
tff(c_1322,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1316]) ).
tff(c_1329,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_1322,c_32]) ).
tff(c_1333,plain,
( ( '#skF_5' = '#skF_8' )
| ( ib = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1329,c_1154]) ).
tff(c_1334,plain,
ib = '#skF_8',
inference(splitLeft,[status(thm)],[c_1333]) ).
tff(c_1340,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1334,c_1334,c_40]) ).
tff(c_1355,plain,
! [Y_56] :
( ( Y_56 = '#skF_7' )
| ~ requalityOnA(Y_56,'#skF_8') ),
inference(resolution,[status(thm)],[c_1322,c_30]) ).
tff(c_1362,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1340,c_1355]) ).
tff(c_1367,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1362,c_481]) ).
tff(c_1371,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1340,c_1367]) ).
tff(c_1372,plain,
'#skF_5' = '#skF_8',
inference(splitRight,[status(thm)],[c_1333]) ).
tff(c_1378,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1372,c_1372,c_1155]) ).
tff(c_1400,plain,
! [Y_57] :
( ( Y_57 = '#skF_7' )
| ~ requalityOnA(Y_57,'#skF_8') ),
inference(resolution,[status(thm)],[c_1322,c_30]) ).
tff(c_1407,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1378,c_1400]) ).
tff(c_1412,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1407,c_481]) ).
tff(c_1416,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1378,c_1412]) ).
tff(c_1418,plain,
~ requalityOnA('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1316]) ).
tff(c_1417,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1316]) ).
tff(c_1422,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1417,c_20]) ).
tff(c_1317,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1151]) ).
tff(c_92,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_110,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_92]) ).
tff(c_172,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_110]) ).
tff(c_236,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_172]) ).
tff(c_300,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_236]) ).
tff(c_363,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_300]) ).
tff(c_399,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_363]) ).
tff(c_1433,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1152,c_1317,c_399]) ).
tff(c_1434,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1418,c_1422,c_1433]) ).
tff(c_1436,plain,
ib = '#skF_5',
inference(splitRight,[status(thm)],[c_453]) ).
tff(c_1435,plain,
( ~ xsd_string('#skF_3')
| requalityOnA('#skF_7','#skF_8')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_453]) ).
tff(c_1470,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1435]) ).
tff(c_1474,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_1470]) ).
tff(c_86,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_128,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_86]) ).
tff(c_190,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_128]) ).
tff(c_254,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_190]) ).
tff(c_318,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_254]) ).
tff(c_369,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_318]) ).
tff(c_411,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_369]) ).
tff(c_1480,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1436,c_1474,c_411]) ).
tff(c_1481,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1480]) ).
tff(c_1488,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_1481,c_32]) ).
tff(c_1438,plain,
! [X_19] :
( ( ia = X_19 )
| ( X_19 = '#skF_5' )
| ~ cA(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_1436,c_24]) ).
tff(c_1494,plain,
( ( ia = '#skF_8' )
| ( '#skF_5' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1488,c_1438]) ).
tff(c_1495,plain,
'#skF_5' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1494]) ).
tff(c_1439,plain,
requalityOnA('#skF_5','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1436,c_1436,c_40]) ).
tff(c_1500,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1495,c_1495,c_1439]) ).
tff(c_1521,plain,
! [Y_60] :
( ( Y_60 = '#skF_7' )
| ~ requalityOnA(Y_60,'#skF_8') ),
inference(resolution,[status(thm)],[c_1481,c_30]) ).
tff(c_1528,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1500,c_1521]) ).
tff(c_1535,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1528,c_481]) ).
tff(c_1539,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1500,c_1535]) ).
tff(c_1540,plain,
ia = '#skF_8',
inference(splitRight,[status(thm)],[c_1494]) ).
tff(c_1545,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1540,c_1540,c_36]) ).
tff(c_1561,plain,
! [Y_61] :
( ( Y_61 = '#skF_7' )
| ~ requalityOnA(Y_61,'#skF_8') ),
inference(resolution,[status(thm)],[c_1481,c_30]) ).
tff(c_1568,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1545,c_1561]) ).
tff(c_1573,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1568,c_481]) ).
tff(c_1577,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1545,c_1573]) ).
tff(c_1578,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1480]) ).
tff(c_1579,plain,
~ requalityOnA('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1480]) ).
tff(c_90,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_114,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_90]) ).
tff(c_176,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_114]) ).
tff(c_240,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_176]) ).
tff(c_304,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_240]) ).
tff(c_365,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_304]) ).
tff(c_403,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_365]) ).
tff(c_1584,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1436,c_1474,c_403]) ).
tff(c_1585,plain,
xsd_string('#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1579,c_1584]) ).
tff(c_1588,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1585,c_20]) ).
tff(c_1592,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1578,c_1588]) ).
tff(c_1593,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(splitRight,[status(thm)],[c_1435]) ).
tff(c_1599,plain,
requalityOnA('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1593]) ).
tff(c_1606,plain,
cA('#skF_8'),
inference(resolution,[status(thm)],[c_1599,c_32]) ).
tff(c_1610,plain,
( ( ia = '#skF_8' )
| ( '#skF_5' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1606,c_1438]) ).
tff(c_1611,plain,
'#skF_5' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1610]) ).
tff(c_1615,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1611,c_1611,c_1439]) ).
tff(c_1635,plain,
! [Y_62] :
( ( Y_62 = '#skF_7' )
| ~ requalityOnA(Y_62,'#skF_8') ),
inference(resolution,[status(thm)],[c_1599,c_30]) ).
tff(c_1642,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1615,c_1635]) ).
tff(c_1647,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1642,c_481]) ).
tff(c_1651,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1615,c_1647]) ).
tff(c_1652,plain,
ia = '#skF_8',
inference(splitRight,[status(thm)],[c_1610]) ).
tff(c_1657,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1652,c_1652,c_36]) ).
tff(c_1674,plain,
! [Y_63] :
( ( Y_63 = '#skF_7' )
| ~ requalityOnA(Y_63,'#skF_8') ),
inference(resolution,[status(thm)],[c_1599,c_30]) ).
tff(c_1681,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1657,c_1674]) ).
tff(c_1686,plain,
~ requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1681,c_481]) ).
tff(c_1690,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1657,c_1686]) ).
tff(c_1692,plain,
~ requalityOnA('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1593]) ).
tff(c_1691,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1593]) ).
tff(c_1696,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1691,c_20]) ).
tff(c_1594,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1435]) ).
tff(c_84,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_118,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_84]) ).
tff(c_180,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_118]) ).
tff(c_244,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_180]) ).
tff(c_308,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_244]) ).
tff(c_392,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_308]) ).
tff(c_457,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_392]) ).
tff(c_1704,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1436,c_1594,c_457]) ).
tff(c_1705,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1692,c_1696,c_1704]) ).
tff(c_1707,plain,
requalityOnA('#skF_8','#skF_7'),
inference(splitRight,[status(thm)],[c_445]) ).
tff(c_1712,plain,
cA('#skF_7'),
inference(resolution,[status(thm)],[c_1707,c_32]) ).
tff(c_1713,plain,
! [X_64] :
( ( ia = X_64 )
| ( ib = X_64 )
| ~ cA(X_64) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_1723,plain,
( ( ia = '#skF_7' )
| ( ib = '#skF_7' ) ),
inference(resolution,[status(thm)],[c_1712,c_1713]) ).
tff(c_1738,plain,
ib = '#skF_7',
inference(splitLeft,[status(thm)],[c_1723]) ).
tff(c_1728,plain,
! [Z_65,Y_66,X_67] :
( ( Z_65 = Y_66 )
| ~ requalityOnA(Z_65,X_67)
| ~ requalityOnA(Y_66,X_67) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_1736,plain,
! [Y_66] :
( ( ib = Y_66 )
| ~ requalityOnA(Y_66,ib) ),
inference(resolution,[status(thm)],[c_40,c_1728]) ).
tff(c_1765,plain,
! [Y_69] :
( ( Y_69 = '#skF_7' )
| ~ requalityOnA(Y_69,'#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_1738,c_1738,c_1736]) ).
tff(c_1774,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1707,c_1765]) ).
tff(c_1780,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1774,c_1707]) ).
tff(c_58,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_156,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_58]) ).
tff(c_218,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_156]) ).
tff(c_282,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_218]) ).
tff(c_346,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_282]) ).
tff(c_380,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_346]) ).
tff(c_433,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_380]) ).
tff(c_1756,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( '#skF_7' != '#skF_5' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1707,c_1738,c_433]) ).
tff(c_1757,plain,
'#skF_7' != '#skF_5',
inference(splitLeft,[status(thm)],[c_1756]) ).
tff(c_1776,plain,
'#skF_5' != '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1774,c_1757]) ).
tff(c_72,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_142,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_72]) ).
tff(c_204,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_142]) ).
tff(c_268,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_204]) ).
tff(c_332,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_268]) ).
tff(c_394,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_332]) ).
tff(c_461,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_394]) ).
tff(c_1852,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_461]) ).
tff(c_1853,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1852]) ).
tff(c_1857,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_1853]) ).
tff(c_74,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_140,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_74]) ).
tff(c_202,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_140]) ).
tff(c_266,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_202]) ).
tff(c_330,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_266]) ).
tff(c_393,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_330]) ).
tff(c_459,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_393]) ).
tff(c_1860,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_1857,c_459]) ).
tff(c_1861,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_1860]) ).
tff(c_1868,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_1861,c_32]) ).
tff(c_1739,plain,
! [X_19] :
( ( ia = X_19 )
| ( X_19 = '#skF_7' )
| ~ cA(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_1738,c_24]) ).
tff(c_1810,plain,
! [X_19] :
( ( ia = X_19 )
| ( X_19 = '#skF_8' )
| ~ cA(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_1774,c_1739]) ).
tff(c_1872,plain,
( ( ia = '#skF_6' )
| ( '#skF_6' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1868,c_1810]) ).
tff(c_1873,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1872]) ).
tff(c_1877,plain,
requalityOnA('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1873,c_1861]) ).
tff(c_1735,plain,
! [Y_66] :
( ( Y_66 = '#skF_8' )
| ~ requalityOnA(Y_66,'#skF_7') ),
inference(resolution,[status(thm)],[c_1707,c_1728]) ).
tff(c_1801,plain,
! [Y_66] :
( ( Y_66 = '#skF_8' )
| ~ requalityOnA(Y_66,'#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1774,c_1735]) ).
tff(c_1885,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_1877,c_1801]) ).
tff(c_1894,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1776,c_1885]) ).
tff(c_1895,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_1872]) ).
tff(c_60,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_130,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_60]) ).
tff(c_192,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_130]) ).
tff(c_256,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_192]) ).
tff(c_320,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_256]) ).
tff(c_370,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_320]) ).
tff(c_413,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_370]) ).
tff(c_1823,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_413]) ).
tff(c_1824,plain,
ia != '#skF_5',
inference(splitLeft,[status(thm)],[c_1823]) ).
tff(c_1897,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_1895,c_1824]) ).
tff(c_1900,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1895,c_1895,c_36]) ).
tff(c_1916,plain,
! [Y_72] :
( ( Y_72 = '#skF_5' )
| ~ requalityOnA(Y_72,'#skF_6') ),
inference(resolution,[status(thm)],[c_1861,c_30]) ).
tff(c_1919,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1900,c_1916]) ).
tff(c_1926,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1897,c_1919]) ).
tff(c_1928,plain,
~ requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_1860]) ).
tff(c_1927,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1860]) ).
tff(c_1932,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1927,c_20]) ).
tff(c_70,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_144,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_70]) ).
tff(c_206,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_144]) ).
tff(c_270,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_206]) ).
tff(c_334,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_270]) ).
tff(c_374,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_334]) ).
tff(c_421,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_374]) ).
tff(c_1941,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_1857,c_421]) ).
tff(c_1942,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1928,c_1932,c_1941]) ).
tff(c_1943,plain,
( requalityOnA('#skF_5','#skF_6')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_1852]) ).
tff(c_1949,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_1943]) ).
tff(c_1953,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1949,c_20]) ).
tff(c_1944,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1852]) ).
tff(c_68,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_146,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_68]) ).
tff(c_208,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_146]) ).
tff(c_272,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_208]) ).
tff(c_336,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_272]) ).
tff(c_375,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_336]) ).
tff(c_423,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6')
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_375]) ).
tff(c_1959,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_1944,c_423]) ).
tff(c_1960,plain,
requalityOnA('#skF_5','#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_1953,c_1959]) ).
tff(c_1967,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_1960,c_32]) ).
tff(c_1974,plain,
( ( ia = '#skF_6' )
| ( '#skF_6' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1967,c_1810]) ).
tff(c_1975,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_1974]) ).
tff(c_1977,plain,
requalityOnA('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1975,c_1960]) ).
tff(c_1985,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_1977,c_1801]) ).
tff(c_1994,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1776,c_1985]) ).
tff(c_1995,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_1974]) ).
tff(c_1997,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_1995,c_1824]) ).
tff(c_2000,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1995,c_1995,c_36]) ).
tff(c_2019,plain,
! [Y_73] :
( ( Y_73 = '#skF_5' )
| ~ requalityOnA(Y_73,'#skF_6') ),
inference(resolution,[status(thm)],[c_1960,c_30]) ).
tff(c_2022,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_2000,c_2019]) ).
tff(c_2029,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1997,c_2022]) ).
tff(c_2030,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_1943]) ).
tff(c_2042,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_2030,c_32]) ).
tff(c_2046,plain,
( ( ia = '#skF_6' )
| ( '#skF_6' = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_2042,c_1810]) ).
tff(c_2050,plain,
'#skF_6' = '#skF_8',
inference(splitLeft,[status(thm)],[c_2046]) ).
tff(c_2052,plain,
requalityOnA('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2050,c_2030]) ).
tff(c_2060,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2052,c_1801]) ).
tff(c_2069,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1776,c_2060]) ).
tff(c_2070,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_2046]) ).
tff(c_2074,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_2070,c_1824]) ).
tff(c_2077,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_2070,c_2070,c_36]) ).
tff(c_2092,plain,
! [Y_74] :
( ( Y_74 = '#skF_5' )
| ~ requalityOnA(Y_74,'#skF_6') ),
inference(resolution,[status(thm)],[c_2030,c_30]) ).
tff(c_2095,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_2077,c_2092]) ).
tff(c_2102,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2074,c_2095]) ).
tff(c_2104,plain,
ia = '#skF_5',
inference(splitRight,[status(thm)],[c_1823]) ).
tff(c_62,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_152,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_62]) ).
tff(c_214,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_152]) ).
tff(c_278,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_214]) ).
tff(c_342,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_278]) ).
tff(c_378,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_342]) ).
tff(c_429,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_378]) ).
tff(c_2123,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_2104,c_429]) ).
tff(c_2124,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_2123]) ).
tff(c_2103,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_1823]) ).
tff(c_2125,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2103]) ).
tff(c_2128,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_2125]) ).
tff(c_2132,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2124,c_2128]) ).
tff(c_2133,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2103]) ).
tff(c_2134,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2103]) ).
tff(c_64,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_150,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_64]) ).
tff(c_212,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_150]) ).
tff(c_276,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_212]) ).
tff(c_314,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_276]) ).
tff(c_367,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_314]) ).
tff(c_407,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_367]) ).
tff(c_2167,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_2104,c_2134,c_407]) ).
tff(c_2170,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2167,c_20]) ).
tff(c_2174,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2133,c_2170]) ).
tff(c_2175,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2123]) ).
tff(c_2176,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_2123]) ).
tff(c_66,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_126,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_66]) ).
tff(c_188,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_126]) ).
tff(c_252,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_188]) ).
tff(c_316,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_252]) ).
tff(c_368,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_316]) ).
tff(c_409,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ia != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_368]) ).
tff(c_2202,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1780,c_1774,c_2104,c_2176,c_409]) ).
tff(c_2205,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2202,c_20]) ).
tff(c_2209,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2175,c_2205]) ).
tff(c_2211,plain,
'#skF_7' = '#skF_5',
inference(splitRight,[status(thm)],[c_1756]) ).
tff(c_1740,plain,
requalityOnA('#skF_7','#skF_7'),
inference(demodulation,[status(thm),theory(equality)],[c_1738,c_1738,c_40]) ).
tff(c_2212,plain,
requalityOnA('#skF_5','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_2211,c_2211,c_1740]) ).
tff(c_2244,plain,
! [Y_79] :
( ( Y_79 = '#skF_8' )
| ~ requalityOnA(Y_79,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_2211,c_1735]) ).
tff(c_2253,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2212,c_2244]) ).
tff(c_2272,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2253,c_2253,c_2212]) ).
tff(c_2275,plain,
'#skF_7' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2253,c_2211]) ).
tff(c_2213,plain,
ib = '#skF_5',
inference(demodulation,[status(thm),theory(equality)],[c_2211,c_1738]) ).
tff(c_2274,plain,
ib = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2253,c_2213]) ).
tff(c_2210,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_1756]) ).
tff(c_2242,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_2210]) ).
tff(c_2255,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_2211,c_2213,c_457]) ).
tff(c_2256,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2255]) ).
tff(c_2259,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_2256]) ).
tff(c_2263,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2242,c_2259]) ).
tff(c_2265,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2255]) ).
tff(c_52,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_162,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_52]) ).
tff(c_224,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_162]) ).
tff(c_288,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_224]) ).
tff(c_352,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_288]) ).
tff(c_383,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_352]) ).
tff(c_439,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_383]) ).
tff(c_2335,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2272,c_2275,c_2274,c_2253,c_2265,c_439]) ).
tff(c_56,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_158,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_56]) ).
tff(c_220,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_158]) ).
tff(c_284,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_220]) ).
tff(c_348,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_284]) ).
tff(c_381,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_348]) ).
tff(c_435,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_381]) ).
tff(c_2354,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2272,c_2275,c_2274,c_2253,c_2265,c_435]) ).
tff(c_2357,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2354,c_20]) ).
tff(c_2361,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2335,c_2357]) ).
tff(c_2362,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_2210]) ).
tff(c_2367,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2362,c_20]) ).
tff(c_2215,plain,
requalityOnA('#skF_8','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_2211,c_1707]) ).
tff(c_2370,plain,
! [Y_83] :
( ( Y_83 = '#skF_5' )
| ~ requalityOnA(Y_83,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_2213,c_2213,c_1736]) ).
tff(c_2377,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2215,c_2370]) ).
tff(c_2384,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2377,c_2377,c_2212]) ).
tff(c_2387,plain,
'#skF_7' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2377,c_2211]) ).
tff(c_2386,plain,
ib = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2377,c_2213]) ).
tff(c_2363,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_2210]) ).
tff(c_54,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ic)
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_160,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ib)
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_54]) ).
tff(c_222,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ requalityOnA(ia,ia)
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_160]) ).
tff(c_286,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing(ia)
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_222]) ).
tff(c_350,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_286]) ).
tff(c_382,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_350]) ).
tff(c_437,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( ib != '#skF_5' )
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_382]) ).
tff(c_2458,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2384,c_2387,c_2386,c_2377,c_2363,c_437]) ).
tff(c_2459,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2367,c_2458]) ).
tff(c_2460,plain,
ia = '#skF_7',
inference(splitRight,[status(thm)],[c_1723]) ).
tff(c_1737,plain,
! [Y_66] :
( ( ia = Y_66 )
| ~ requalityOnA(Y_66,ia) ),
inference(resolution,[status(thm)],[c_36,c_1728]) ).
tff(c_2490,plain,
! [Y_88] :
( ( Y_88 = '#skF_7' )
| ~ requalityOnA(Y_88,'#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_2460,c_2460,c_1737]) ).
tff(c_2499,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1707,c_2490]) ).
tff(c_2487,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ( '#skF_7' != '#skF_5' )
| requalityOnA('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_2460,c_455]) ).
tff(c_2488,plain,
'#skF_7' != '#skF_5',
inference(splitLeft,[status(thm)],[c_2487]) ).
tff(c_2501,plain,
'#skF_5' != '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2499,c_2488]) ).
tff(c_2506,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2499,c_1707]) ).
tff(c_2579,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_2506,c_2499,c_423]) ).
tff(c_2580,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2579]) ).
tff(c_2585,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_2580]) ).
tff(c_2589,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_2506,c_2499,c_2585,c_459]) ).
tff(c_2590,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_2589]) ).
tff(c_2597,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_2590,c_32]) ).
tff(c_2462,plain,
! [X_19] :
( ( X_19 = '#skF_7' )
| ( ib = X_19 )
| ~ cA(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_2460,c_24]) ).
tff(c_2536,plain,
! [X_19] :
( ( X_19 = '#skF_8' )
| ( ib = X_19 )
| ~ cA(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_2499,c_2462]) ).
tff(c_2601,plain,
( ( '#skF_6' = '#skF_8' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_2597,c_2536]) ).
tff(c_2602,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_2601]) ).
tff(c_2471,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ( ib != '#skF_5' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1707,c_433]) ).
tff(c_2472,plain,
ib != '#skF_5',
inference(splitLeft,[status(thm)],[c_2471]) ).
tff(c_2606,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_2602,c_2472]) ).
tff(c_2607,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_2602,c_2602,c_40]) ).
tff(c_2624,plain,
! [Y_91] :
( ( Y_91 = '#skF_5' )
| ~ requalityOnA(Y_91,'#skF_6') ),
inference(resolution,[status(thm)],[c_2590,c_30]) ).
tff(c_2627,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_2607,c_2624]) ).
tff(c_2634,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2606,c_2627]) ).
tff(c_2635,plain,
'#skF_6' = '#skF_8',
inference(splitRight,[status(thm)],[c_2601]) ).
tff(c_2640,plain,
requalityOnA('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2635,c_2590]) ).
tff(c_2526,plain,
! [Y_66] :
( ( Y_66 = '#skF_8' )
| ~ requalityOnA(Y_66,'#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_2499,c_1735]) ).
tff(c_2649,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2640,c_2526]) ).
tff(c_2658,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2501,c_2649]) ).
tff(c_2659,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_2589]) ).
tff(c_2664,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2659,c_20]) ).
tff(c_2666,plain,
( xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_2506,c_2499,c_2585,c_421]) ).
tff(c_2667,plain,
requalityOnA('#skF_5','#skF_6'),
inference(negUnitSimplification,[status(thm)],[c_2664,c_2666]) ).
tff(c_2660,plain,
~ requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_2589]) ).
tff(c_2680,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2667,c_2660]) ).
tff(c_2681,plain,
( requalityOnA('#skF_5','#skF_6')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_2579]) ).
tff(c_2689,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_2681]) ).
tff(c_2682,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2579]) ).
tff(c_2697,plain,
( xsd_string('#skF_4')
| requalityOnA('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_2506,c_2499,c_2682,c_461]) ).
tff(c_2698,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_2697]) ).
tff(c_2705,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_2698,c_32]) ).
tff(c_2711,plain,
( ( '#skF_6' = '#skF_8' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_2705,c_2536]) ).
tff(c_2712,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_2711]) ).
tff(c_2716,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_2712,c_2472]) ).
tff(c_2717,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_2712,c_2712,c_40]) ).
tff(c_2704,plain,
! [Y_21] :
( ( Y_21 = '#skF_5' )
| ~ requalityOnA(Y_21,'#skF_6') ),
inference(resolution,[status(thm)],[c_2698,c_30]) ).
tff(c_2732,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_2717,c_2704]) ).
tff(c_2741,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2716,c_2732]) ).
tff(c_2742,plain,
'#skF_6' = '#skF_8',
inference(splitRight,[status(thm)],[c_2711]) ).
tff(c_2745,plain,
requalityOnA('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2742,c_2698]) ).
tff(c_2754,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2745,c_2526]) ).
tff(c_2763,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2501,c_2754]) ).
tff(c_2764,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_2697]) ).
tff(c_2768,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2764,c_20]) ).
tff(c_2772,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2689,c_2768]) ).
tff(c_2773,plain,
requalityOnA('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_2681]) ).
tff(c_2781,plain,
cA('#skF_6'),
inference(resolution,[status(thm)],[c_2773,c_32]) ).
tff(c_2785,plain,
( ( '#skF_6' = '#skF_8' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_2781,c_2536]) ).
tff(c_2786,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_2785]) ).
tff(c_2793,plain,
'#skF_5' != '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_2786,c_2472]) ).
tff(c_2794,plain,
requalityOnA('#skF_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_2786,c_2786,c_40]) ).
tff(c_2811,plain,
! [Y_93] :
( ( Y_93 = '#skF_5' )
| ~ requalityOnA(Y_93,'#skF_6') ),
inference(resolution,[status(thm)],[c_2773,c_30]) ).
tff(c_2814,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_2794,c_2811]) ).
tff(c_2821,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2793,c_2814]) ).
tff(c_2822,plain,
'#skF_6' = '#skF_8',
inference(splitRight,[status(thm)],[c_2785]) ).
tff(c_2825,plain,
requalityOnA('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2822,c_2773]) ).
tff(c_2834,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2825,c_2526]) ).
tff(c_2843,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2501,c_2834]) ).
tff(c_2845,plain,
'#skF_7' = '#skF_5',
inference(splitRight,[status(thm)],[c_2487]) ).
tff(c_2852,plain,
requalityOnA('#skF_8','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_1707]) ).
tff(c_2850,plain,
ia = '#skF_5',
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_2460]) ).
tff(c_2463,plain,
requalityOnA('#skF_7','#skF_7'),
inference(demodulation,[status(thm),theory(equality)],[c_2460,c_2460,c_36]) ).
tff(c_2848,plain,
requalityOnA('#skF_5','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_2845,c_2463]) ).
tff(c_2885,plain,
! [Y_94] :
( ( Y_94 = '#skF_8' )
| ~ requalityOnA(Y_94,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_1735]) ).
tff(c_2894,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2848,c_2885]) ).
tff(c_2898,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2894,c_2852]) ).
tff(c_2902,plain,
'#skF_7' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2894,c_2845]) ).
tff(c_2901,plain,
ia = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_2894,c_2850]) ).
tff(c_2862,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| requalityOnA('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_2850,c_399]) ).
tff(c_2863,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_2862]) ).
tff(c_2867,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_2863]) ).
tff(c_2914,plain,
( xsd_integer('#skF_4')
| ~ requalityOnA('#skF_8','#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_2901,c_2894,c_2867,c_429]) ).
tff(c_2915,plain,
~ requalityOnA('#skF_8','#skF_7'),
inference(splitLeft,[status(thm)],[c_2914]) ).
tff(c_2931,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2898,c_2902,c_2915]) ).
tff(c_2932,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2914]) ).
tff(c_2933,plain,
requalityOnA('#skF_8','#skF_7'),
inference(splitRight,[status(thm)],[c_2914]) ).
tff(c_2939,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2902,c_2933]) ).
tff(c_2951,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2939,c_2902,c_2894,c_2901,c_2867,c_409]) ).
tff(c_2954,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_2951,c_20]) ).
tff(c_2958,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2932,c_2954]) ).
tff(c_2960,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_2862]) ).
tff(c_2974,plain,
( xsd_integer('#skF_4')
| ~ requalityOnA('#skF_8','#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_2850,c_2960,c_413]) ).
tff(c_2975,plain,
~ requalityOnA('#skF_8','#skF_5'),
inference(splitLeft,[status(thm)],[c_2974]) ).
tff(c_2985,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2852,c_2975]) ).
tff(c_2986,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_2974]) ).
tff(c_3000,plain,
! [Y_95] :
( ( Y_95 = '#skF_8' )
| ~ requalityOnA(Y_95,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_2845,c_1735]) ).
tff(c_3009,plain,
'#skF_5' = '#skF_8',
inference(resolution,[status(thm)],[c_2848,c_3000]) ).
tff(c_3011,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_3009,c_2852]) ).
tff(c_3015,plain,
'#skF_7' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_3009,c_2845]) ).
tff(c_3014,plain,
ia = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_3009,c_2850]) ).
tff(c_3086,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_3011,c_3015,c_3014,c_3009,c_2960,c_407]) ).
tff(c_3089,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_3086,c_20]) ).
tff(c_3093,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2986,c_3089]) ).
tff(c_3095,plain,
ib = '#skF_5',
inference(splitRight,[status(thm)],[c_2471]) ).
tff(c_3104,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_1707,c_3095,c_439]) ).
tff(c_3105,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_3104]) ).
tff(c_3109,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_3105]) ).
tff(c_3133,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1707,c_3095,c_3109,c_437]) ).
tff(c_3094,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_2471]) ).
tff(c_3127,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_3109,c_3094]) ).
tff(c_3131,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_3127,c_20]) ).
tff(c_3135,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3133,c_3131]) ).
tff(c_3136,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_3104]) ).
tff(c_3168,plain,
! [Y_99] :
( ( Y_99 = '#skF_7' )
| ~ requalityOnA(Y_99,'#skF_7') ),
inference(demodulation,[status(thm),theory(equality)],[c_2460,c_2460,c_1737]) ).
tff(c_3177,plain,
'#skF_7' = '#skF_8',
inference(resolution,[status(thm)],[c_1707,c_3168]) ).
tff(c_3179,plain,
requalityOnA('#skF_8','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_3177,c_3177,c_2463]) ).
tff(c_3137,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_3104]) ).
tff(c_3257,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_3179,c_3177,c_3095,c_3137,c_435]) ).
tff(c_3260,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_3257,c_20]) ).
tff(c_3264,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3136,c_3260]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS138+1 : TPTP v9.0.0. Released v3.1.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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 02:59:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 6.62/2.49 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.06/2.56
% 7.06/2.56 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------