%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS174+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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:08:10 PM UTC 2025
% Result : Theorem 4.75s 2.11s
% Output : CNFRefutation 5.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 394 ( 252 unt; 0 typ; 0 def)
% Number of atoms : 828 ( 75 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 713 ( 279 ~; 424 |; 4 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 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 : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 21 ( 21 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ xsd_string > xsd_integer > cowlThing > cowlNothing > cB > cA_and_B > cA > #nlpp > ib > ia > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(cA,type,
cA: $i > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(cB,type,
cB: $i > $o ).
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(cA_and_B,type,
cA_and_B: $i > $o ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(ia,type,
ia: $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(f_75,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
tff(f_124,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( cA_and_B(X)
<=> ( cB(X)
| cA(X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
tff(f_81,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
tff(f_93,axiom,
! [X] :
( cA_and_B(X)
<=> ( ( X = ib )
| ( X = ia ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
tff(f_98,axiom,
! [X] :
( cB(X)
<=> ( X = ib ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
tff(f_86,axiom,
! [X] :
( cA(X)
<=> ( X = ia ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
tff(c_16,plain,
! [X_15] : cowlThing(X_15),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_18,plain,
! [X_15] : ~ cowlNothing(X_15),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_44,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_101,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_44]) ).
tff(c_140,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_101]) ).
tff(c_178,plain,
~ cA('#skF_6'),
inference(splitLeft,[status(thm)],[c_140]) ).
tff(c_64,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_93,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_64]) ).
tff(c_124,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_93]) ).
tff(c_195,plain,
~ cB('#skF_6'),
inference(splitLeft,[status(thm)],[c_124]) ).
tff(c_74,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_112,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_74]) ).
tff(c_162,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_112]) ).
tff(c_196,plain,
~ cA_and_B('#skF_5'),
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_22,plain,
! [X_16] :
( xsd_string(X_16)
| xsd_integer(X_16) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_86,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_91,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_86]) ).
tff(c_150,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_91]) ).
tff(c_197,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_150]) ).
tff(c_201,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_197]) ).
tff(c_88,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_110,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_88]) ).
tff(c_158,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_110]) ).
tff(c_205,plain,
( xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_201,c_158]) ).
tff(c_206,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_205]) ).
tff(c_28,plain,
! [X_18] :
( ( ia = X_18 )
| ( ib = X_18 )
| ~ cA_and_B(X_18) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_210,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_206,c_28]) ).
tff(c_211,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_210]) ).
tff(c_36,plain,
cB(ib),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_214,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_211,c_36]) ).
tff(c_217,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_214]) ).
tff(c_218,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_210]) ).
tff(c_26,plain,
cA(ia),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_223,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_218,c_26]) ).
tff(c_226,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_223]) ).
tff(c_228,plain,
~ cA_and_B('#skF_6'),
inference(splitRight,[status(thm)],[c_205]) ).
tff(c_227,plain,
( cB('#skF_5')
| cA('#skF_5')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_205]) ).
tff(c_231,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_227]) ).
tff(c_20,plain,
! [X_16] :
( ~ xsd_integer(X_16)
| ~ xsd_string(X_16) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_235,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_231,c_20]) ).
tff(c_84,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_104,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_84]) ).
tff(c_146,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_104]) ).
tff(c_240,plain,
( xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_201,c_146]) ).
tff(c_241,plain,
( cA('#skF_5')
| cB('#skF_5') ),
inference(negUnitSimplification,[status(thm)],[c_228,c_235,c_240]) ).
tff(c_242,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_241]) ).
tff(c_34,plain,
! [X_19] :
( ( ib = X_19 )
| ~ cB(X_19) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_246,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_242,c_34]) ).
tff(c_32,plain,
cA_and_B(ib),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_252,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_246,c_32]) ).
tff(c_255,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_252]) ).
tff(c_256,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_241]) ).
tff(c_24,plain,
! [X_17] :
( ( ia = X_17 )
| ~ cA(X_17) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_261,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_256,c_24]) ).
tff(c_30,plain,
cA_and_B(ia),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_264,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_261,c_30]) ).
tff(c_267,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_264]) ).
tff(c_268,plain,
( cA('#skF_5')
| cB('#skF_5') ),
inference(splitRight,[status(thm)],[c_227]) ).
tff(c_275,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_268]) ).
tff(c_279,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_275,c_34]) ).
tff(c_285,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_279,c_32]) ).
tff(c_288,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_285]) ).
tff(c_289,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_268]) ).
tff(c_294,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_289,c_24]) ).
tff(c_297,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_294,c_30]) ).
tff(c_300,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_297]) ).
tff(c_301,plain,
( cA_and_B('#skF_6')
| cB('#skF_5')
| cA('#skF_5')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_150]) ).
tff(c_307,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_301]) ).
tff(c_311,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_307,c_20]) ).
tff(c_302,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_150]) ).
tff(c_82,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_109,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_82]) ).
tff(c_156,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_109]) ).
tff(c_327,plain,
( xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_302,c_156]) ).
tff(c_328,plain,
( cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(negUnitSimplification,[status(thm)],[c_311,c_327]) ).
tff(c_329,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_328]) ).
tff(c_333,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_329,c_28]) ).
tff(c_335,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_333]) ).
tff(c_338,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_335,c_36]) ).
tff(c_341,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_338]) ).
tff(c_342,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_333]) ).
tff(c_347,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_342,c_26]) ).
tff(c_350,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_347]) ).
tff(c_351,plain,
( cB('#skF_5')
| cA('#skF_5') ),
inference(splitRight,[status(thm)],[c_328]) ).
tff(c_353,plain,
cA('#skF_5'),
inference(splitLeft,[status(thm)],[c_351]) ).
tff(c_357,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_353,c_24]) ).
tff(c_360,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_357,c_30]) ).
tff(c_363,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_360]) ).
tff(c_364,plain,
cB('#skF_5'),
inference(splitRight,[status(thm)],[c_351]) ).
tff(c_371,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_364,c_34]) ).
tff(c_375,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_371,c_32]) ).
tff(c_378,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_375]) ).
tff(c_379,plain,
( cA('#skF_5')
| cB('#skF_5')
| cA_and_B('#skF_6') ),
inference(splitRight,[status(thm)],[c_301]) ).
tff(c_385,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_379]) ).
tff(c_389,plain,
( ( ia = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_385,c_28]) ).
tff(c_390,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_389]) ).
tff(c_393,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_390,c_36]) ).
tff(c_396,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_393]) ).
tff(c_397,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_389]) ).
tff(c_403,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_397,c_26]) ).
tff(c_406,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_403]) ).
tff(c_407,plain,
( cB('#skF_5')
| cA('#skF_5') ),
inference(splitRight,[status(thm)],[c_379]) ).
tff(c_409,plain,
cA('#skF_5'),
inference(splitLeft,[status(thm)],[c_407]) ).
tff(c_413,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_409,c_24]) ).
tff(c_417,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_413,c_30]) ).
tff(c_420,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_417]) ).
tff(c_421,plain,
cB('#skF_5'),
inference(splitRight,[status(thm)],[c_407]) ).
tff(c_426,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_421,c_34]) ).
tff(c_432,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_426,c_32]) ).
tff(c_435,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_432]) ).
tff(c_437,plain,
cA_and_B('#skF_5'),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_436,plain,
( ~ xsd_string('#skF_3')
| cA_and_B('#skF_6')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_619,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_436]) ).
tff(c_623,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_619]) ).
tff(c_80,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_94,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_80]) ).
tff(c_126,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_94]) ).
tff(c_634,plain,
( xsd_string('#skF_4')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_437,c_623,c_126]) ).
tff(c_635,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_634]) ).
tff(c_452,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_436]) ).
tff(c_456,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_452]) ).
tff(c_76,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_107,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_76]) ).
tff(c_152,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_107]) ).
tff(c_464,plain,
( xsd_integer('#skF_4')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_437,c_456,c_152]) ).
tff(c_465,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_464]) ).
tff(c_441,plain,
( ( ia = '#skF_5' )
| ( ib = '#skF_5' ) ),
inference(resolution,[status(thm)],[c_437,c_28]) ).
tff(c_442,plain,
ib = '#skF_5',
inference(splitLeft,[status(thm)],[c_441]) ).
tff(c_466,plain,
! [X_28] :
( ( ia = X_28 )
| ( X_28 = '#skF_5' )
| ~ cA_and_B(X_28) ),
inference(demodulation,[status(thm),theory(equality)],[c_442,c_28]) ).
tff(c_476,plain,
( ( ia = '#skF_6' )
| ( '#skF_5' = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_465,c_466]) ).
tff(c_481,plain,
'#skF_5' = '#skF_6',
inference(splitLeft,[status(thm)],[c_476]) ).
tff(c_445,plain,
cB('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_442,c_36]) ).
tff(c_484,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_481,c_445]) ).
tff(c_488,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_484]) ).
tff(c_489,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_476]) ).
tff(c_496,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_489,c_26]) ).
tff(c_499,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_496]) ).
tff(c_500,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_464]) ).
tff(c_501,plain,
~ cA_and_B('#skF_6'),
inference(splitRight,[status(thm)],[c_464]) ).
tff(c_518,plain,
( xsd_string('#skF_4')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_437,c_456,c_126]) ).
tff(c_519,plain,
xsd_string('#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_501,c_518]) ).
tff(c_522,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_519,c_20]) ).
tff(c_526,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_500,c_522]) ).
tff(c_527,plain,
( xsd_integer('#skF_4')
| cA_and_B('#skF_6') ),
inference(splitRight,[status(thm)],[c_436]) ).
tff(c_533,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_527]) ).
tff(c_540,plain,
! [X_31] :
( ( ia = X_31 )
| ( X_31 = '#skF_5' )
| ~ cA_and_B(X_31) ),
inference(demodulation,[status(thm),theory(equality)],[c_442,c_28]) ).
tff(c_550,plain,
( ( ia = '#skF_6' )
| ( '#skF_5' = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_533,c_540]) ).
tff(c_557,plain,
'#skF_5' = '#skF_6',
inference(splitLeft,[status(thm)],[c_550]) ).
tff(c_560,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_557,c_445]) ).
tff(c_564,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_560]) ).
tff(c_565,plain,
ia = '#skF_6',
inference(splitRight,[status(thm)],[c_550]) ).
tff(c_570,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_565,c_26]) ).
tff(c_573,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_570]) ).
tff(c_574,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_527]) ).
tff(c_575,plain,
~ cA_and_B('#skF_6'),
inference(splitRight,[status(thm)],[c_527]) ).
tff(c_528,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_436]) ).
tff(c_78,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_105,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_78]) ).
tff(c_118,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_105]) ).
tff(c_608,plain,
( xsd_string('#skF_4')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_437,c_528,c_118]) ).
tff(c_609,plain,
xsd_string('#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_575,c_608]) ).
tff(c_612,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_609,c_20]) ).
tff(c_616,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_574,c_612]) ).
tff(c_617,plain,
ia = '#skF_5',
inference(splitRight,[status(thm)],[c_441]) ).
tff(c_642,plain,
! [X_35] :
( ( X_35 = '#skF_5' )
| ( ib = X_35 )
| ~ cA_and_B(X_35) ),
inference(demodulation,[status(thm),theory(equality)],[c_617,c_28]) ).
tff(c_652,plain,
( ( '#skF_5' = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_635,c_642]) ).
tff(c_663,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_652]) ).
tff(c_667,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_663,c_36]) ).
tff(c_670,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_667]) ).
tff(c_671,plain,
'#skF_5' = '#skF_6',
inference(splitRight,[status(thm)],[c_652]) ).
tff(c_627,plain,
cA('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_617,c_26]) ).
tff(c_677,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_671,c_627]) ).
tff(c_682,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_677]) ).
tff(c_684,plain,
~ cA_and_B('#skF_6'),
inference(splitRight,[status(thm)],[c_634]) ).
tff(c_683,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_634]) ).
tff(c_688,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_683,c_20]) ).
tff(c_716,plain,
( xsd_integer('#skF_4')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_437,c_623,c_152]) ).
tff(c_717,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_684,c_688,c_716]) ).
tff(c_718,plain,
( xsd_integer('#skF_4')
| cA_and_B('#skF_6') ),
inference(splitRight,[status(thm)],[c_436]) ).
tff(c_733,plain,
cA_and_B('#skF_6'),
inference(splitLeft,[status(thm)],[c_718]) ).
tff(c_742,plain,
! [X_39] :
( ( X_39 = '#skF_5' )
| ( ib = X_39 )
| ~ cA_and_B(X_39) ),
inference(demodulation,[status(thm),theory(equality)],[c_617,c_28]) ).
tff(c_752,plain,
( ( '#skF_5' = '#skF_6' )
| ( ib = '#skF_6' ) ),
inference(resolution,[status(thm)],[c_733,c_742]) ).
tff(c_761,plain,
ib = '#skF_6',
inference(splitLeft,[status(thm)],[c_752]) ).
tff(c_765,plain,
cB('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_761,c_36]) ).
tff(c_768,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_765]) ).
tff(c_769,plain,
'#skF_5' = '#skF_6',
inference(splitRight,[status(thm)],[c_752]) ).
tff(c_727,plain,
cA('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_617,c_26]) ).
tff(c_773,plain,
cA('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_769,c_727]) ).
tff(c_778,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_773]) ).
tff(c_779,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_718]) ).
tff(c_780,plain,
~ cA_and_B('#skF_6'),
inference(splitRight,[status(thm)],[c_718]) ).
tff(c_719,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_436]) ).
tff(c_817,plain,
( xsd_string('#skF_4')
| cA_and_B('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_437,c_719,c_118]) ).
tff(c_818,plain,
xsd_string('#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_780,c_817]) ).
tff(c_821,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_818,c_20]) ).
tff(c_825,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_779,c_821]) ).
tff(c_827,plain,
cB('#skF_6'),
inference(splitRight,[status(thm)],[c_124]) ).
tff(c_841,plain,
~ cA_and_B('#skF_5'),
inference(splitLeft,[status(thm)],[c_162]) ).
tff(c_831,plain,
ib = '#skF_6',
inference(resolution,[status(thm)],[c_827,c_34]) ).
tff(c_835,plain,
cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_831,c_32]) ).
tff(c_68,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_100,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_68]) ).
tff(c_138,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_100]) ).
tff(c_871,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_138]) ).
tff(c_872,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_871]) ).
tff(c_70,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_99,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_70]) ).
tff(c_136,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_99]) ).
tff(c_874,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_136]) ).
tff(c_875,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_874]) ).
tff(c_878,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_875]) ).
tff(c_882,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_872,c_878]) ).
tff(c_883,plain,
( cB('#skF_5')
| cA('#skF_5')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_874]) ).
tff(c_891,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_883]) ).
tff(c_895,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_891,c_20]) ).
tff(c_884,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_874]) ).
tff(c_66,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_102,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_66]) ).
tff(c_142,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_102]) ).
tff(c_905,plain,
( xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_884,c_142]) ).
tff(c_906,plain,
( cA('#skF_5')
| cB('#skF_5') ),
inference(negUnitSimplification,[status(thm)],[c_895,c_905]) ).
tff(c_907,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_906]) ).
tff(c_833,plain,
! [X_19] :
( ( X_19 = '#skF_6' )
| ~ cB(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_831,c_34]) ).
tff(c_911,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_907,c_833]) ).
tff(c_913,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_911,c_841]) ).
tff(c_917,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_835,c_913]) ).
tff(c_918,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_906]) ).
tff(c_923,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_918,c_24]) ).
tff(c_926,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_923,c_30]) ).
tff(c_929,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_841,c_926]) ).
tff(c_930,plain,
( cA('#skF_5')
| cB('#skF_5') ),
inference(splitRight,[status(thm)],[c_883]) ).
tff(c_936,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_930]) ).
tff(c_940,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_936,c_833]) ).
tff(c_944,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_940,c_841]) ).
tff(c_948,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_835,c_944]) ).
tff(c_949,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_930]) ).
tff(c_954,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_949,c_24]) ).
tff(c_957,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_954,c_30]) ).
tff(c_960,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_841,c_957]) ).
tff(c_961,plain,
( cB('#skF_5')
| cA('#skF_5')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_871]) ).
tff(c_963,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_961]) ).
tff(c_962,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_871]) ).
tff(c_72,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_90,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_72]) ).
tff(c_148,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_90]) ).
tff(c_970,plain,
( xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_962,c_148]) ).
tff(c_971,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_970]) ).
tff(c_980,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_971,c_833]) ).
tff(c_982,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_980,c_841]) ).
tff(c_986,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_835,c_982]) ).
tff(c_987,plain,
( cA('#skF_5')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_970]) ).
tff(c_994,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_987]) ).
tff(c_997,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_994,c_20]) ).
tff(c_1001,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_963,c_997]) ).
tff(c_1002,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_987]) ).
tff(c_1012,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_1002,c_24]) ).
tff(c_1017,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1012,c_30]) ).
tff(c_1020,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_841,c_1017]) ).
tff(c_1021,plain,
( cA('#skF_5')
| cB('#skF_5') ),
inference(splitRight,[status(thm)],[c_961]) ).
tff(c_1023,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_1021]) ).
tff(c_1027,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1023,c_833]) ).
tff(c_1029,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1027,c_841]) ).
tff(c_1033,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_835,c_1029]) ).
tff(c_1034,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_1021]) ).
tff(c_1039,plain,
ia = '#skF_5',
inference(resolution,[status(thm)],[c_1034,c_24]) ).
tff(c_1042,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1039,c_30]) ).
tff(c_1045,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_841,c_1042]) ).
tff(c_1047,plain,
cA_and_B('#skF_5'),
inference(splitRight,[status(thm)],[c_162]) ).
tff(c_60,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_108,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_60]) ).
tff(c_154,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_108]) ).
tff(c_1049,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_1047,c_154]) ).
tff(c_1050,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_1049]) ).
tff(c_58,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_95,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_58]) ).
tff(c_128,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_95]) ).
tff(c_1061,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_1047,c_128]) ).
tff(c_1062,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1061]) ).
tff(c_1065,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_1062]) ).
tff(c_1069,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1050,c_1065]) ).
tff(c_1070,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1061]) ).
tff(c_1071,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1061]) ).
tff(c_62,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_106,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_62]) ).
tff(c_120,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cB('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_106]) ).
tff(c_1150,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_827,c_1047,c_1071,c_120]) ).
tff(c_1153,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1150,c_20]) ).
tff(c_1157,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1070,c_1153]) ).
tff(c_1158,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1049]) ).
tff(c_1159,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_1049]) ).
tff(c_826,plain,
( ~ cA_and_B('#skF_5')
| ~ xsd_integer('#skF_3')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_124]) ).
tff(c_1170,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1159,c_1047,c_826]) ).
tff(c_1173,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1170,c_20]) ).
tff(c_1177,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1158,c_1173]) ).
tff(c_1179,plain,
cA('#skF_6'),
inference(splitRight,[status(thm)],[c_140]) ).
tff(c_1183,plain,
ia = '#skF_6',
inference(resolution,[status(thm)],[c_1179,c_24]) ).
tff(c_1185,plain,
cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1183,c_30]) ).
tff(c_1178,plain,
( ~ cA_and_B('#skF_5')
| ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_140]) ).
tff(c_1215,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_1178]) ).
tff(c_42,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_103,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_42]) ).
tff(c_144,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_103]) ).
tff(c_1222,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ cA_and_B('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_144]) ).
tff(c_1223,plain,
~ cA_and_B('#skF_5'),
inference(splitLeft,[status(thm)],[c_1222]) ).
tff(c_50,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_98,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_50]) ).
tff(c_134,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_98]) ).
tff(c_1229,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_134]) ).
tff(c_1230,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1229]) ).
tff(c_1233,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_1230]) ).
tff(c_1237,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1215,c_1233]) ).
tff(c_1238,plain,
( cB('#skF_5')
| cA('#skF_5')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_1229]) ).
tff(c_1244,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_1238]) ).
tff(c_1239,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1229]) ).
tff(c_54,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_96,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_54]) ).
tff(c_130,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_96]) ).
tff(c_1258,plain,
( xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_1239,c_130]) ).
tff(c_1259,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_1258]) ).
tff(c_1263,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_1259,c_34]) ).
tff(c_1267,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1263,c_32]) ).
tff(c_1270,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1223,c_1267]) ).
tff(c_1271,plain,
( cA('#skF_5')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_1258]) ).
tff(c_1274,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_1271]) ).
tff(c_1277,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1274,c_20]) ).
tff(c_1281,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1244,c_1277]) ).
tff(c_1282,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_1271]) ).
tff(c_1184,plain,
! [X_17] :
( ( X_17 = '#skF_6' )
| ~ cA(X_17) ),
inference(demodulation,[status(thm),theory(equality)],[c_1183,c_24]) ).
tff(c_1292,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1282,c_1184]) ).
tff(c_1295,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1292,c_1223]) ).
tff(c_1299,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1185,c_1295]) ).
tff(c_1300,plain,
( cA('#skF_5')
| cB('#skF_5') ),
inference(splitRight,[status(thm)],[c_1238]) ).
tff(c_1302,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_1300]) ).
tff(c_1306,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_1302,c_34]) ).
tff(c_1313,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1306,c_32]) ).
tff(c_1316,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1223,c_1313]) ).
tff(c_1317,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_1300]) ).
tff(c_1322,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1317,c_1184]) ).
tff(c_1325,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1322,c_1223]) ).
tff(c_1329,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1185,c_1325]) ).
tff(c_1330,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_1222]) ).
tff(c_1336,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1330]) ).
tff(c_1339,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_22,c_1336]) ).
tff(c_1343,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1215,c_1339]) ).
tff(c_1344,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1330]) ).
tff(c_1331,plain,
cA_and_B('#skF_5'),
inference(splitRight,[status(thm)],[c_1222]) ).
tff(c_1345,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1330]) ).
tff(c_46,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_92,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_46]) ).
tff(c_122,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_92]) ).
tff(c_1380,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_1331,c_1345,c_122]) ).
tff(c_1383,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1380,c_20]) ).
tff(c_1387,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1344,c_1383]) ).
tff(c_1388,plain,
( ~ cA_and_B('#skF_5')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_1178]) ).
tff(c_1390,plain,
~ cA_and_B('#skF_5'),
inference(splitLeft,[status(thm)],[c_1388]) ).
tff(c_1389,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_1178]) ).
tff(c_56,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_111,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_56]) ).
tff(c_160,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_111]) ).
tff(c_1409,plain,
( xsd_string('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_1389,c_160]) ).
tff(c_1410,plain,
cB('#skF_5'),
inference(splitLeft,[status(thm)],[c_1409]) ).
tff(c_1414,plain,
ib = '#skF_5',
inference(resolution,[status(thm)],[c_1410,c_34]) ).
tff(c_1418,plain,
cA_and_B('#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_1414,c_32]) ).
tff(c_1421,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1390,c_1418]) ).
tff(c_1423,plain,
~ cB('#skF_5'),
inference(splitRight,[status(thm)],[c_1409]) ).
tff(c_1422,plain,
( cA('#skF_5')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_1409]) ).
tff(c_1424,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_1422]) ).
tff(c_1428,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1424,c_20]) ).
tff(c_52,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_97,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_52]) ).
tff(c_132,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_97]) ).
tff(c_1438,plain,
( xsd_integer('#skF_4')
| cA('#skF_5')
| cB('#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_1389,c_132]) ).
tff(c_1439,plain,
cA('#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1423,c_1428,c_1438]) ).
tff(c_1443,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1439,c_1184]) ).
tff(c_1446,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1443,c_1390]) ).
tff(c_1450,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1185,c_1446]) ).
tff(c_1451,plain,
cA('#skF_5'),
inference(splitRight,[status(thm)],[c_1422]) ).
tff(c_1456,plain,
'#skF_5' = '#skF_6',
inference(resolution,[status(thm)],[c_1451,c_1184]) ).
tff(c_1463,plain,
~ cA_and_B('#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_1456,c_1390]) ).
tff(c_1467,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1185,c_1463]) ).
tff(c_1468,plain,
xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1388]) ).
tff(c_1469,plain,
cA_and_B('#skF_5'),
inference(splitRight,[status(thm)],[c_1388]) ).
tff(c_48,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_89,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_18,c_48]) ).
tff(c_116,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ cA_and_B('#skF_5')
| ~ cA('#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_89]) ).
tff(c_1516,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1179,c_1469,c_1389,c_116]) ).
tff(c_1519,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1516,c_20]) ).
tff(c_1523,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1468,c_1519]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS174+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.32 % Computer : n003.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Tue Apr 8 03:01:03 EDT 2025
% 0.12/0.32 % CPUTime :
% 4.75/2.11 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.75/2.17
% 4.75/2.17 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------