%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS132+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 : n021.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:24 PM UTC 2025
% Result : Theorem 4.73s 1.97s
% Output : CNFRefutation 5.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 12
% Syntax : Number of formulae : 310 ( 124 unt; 0 typ; 0 def)
% Number of atoms : 794 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 833 ( 349 ~; 461 |; 8 &)
% ( 10 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 15 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-1 aty)
% Number of variables : 110 ( 105 !; 5 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rs > rr > rq > rp > xsd_string > xsd_integer > cowlThing > cowlNothing > cnotB > cnotAorB > cnotA > cNothing > cB > cAorB > cA > #nlpp > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_11 > #skF_1 > #skF_10 > #skF_13 > #skF_9 > #skF_8 > #skF_3 > #skF_6 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(cnotAorB,type,
cnotAorB: $i > $o ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(rr,type,
rr: ( $i * $i ) > $o ).
tff(cA,type,
cA: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff(rq,type,
rq: ( $i * $i ) > $o ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(cAorB,type,
cAorB: $i > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(cnotA,type,
cnotA: $i > $o ).
tff(cB,type,
cB: $i > $o ).
tff(rs,type,
rs: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(cnotB,type,
cnotB: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(cNothing,type,
cNothing: $i > $o ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i ).
tff('#skF_9',type,
'#skF_9': $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff(rp,type,
rp: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(f_34,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
tff(f_130,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( cAorB(X)
<=> ( cB(X)
| cA(X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
tff(f_85,axiom,
! [X] :
( cnotA(X)
<=> ! [Y] :
( rq(X,Y)
=> cNothing(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
tff(f_48,axiom,
! [X] :
( cA(X)
<=> ? [Y] :
( rq(X,Y)
& cowlThing(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
tff(f_108,axiom,
! [X] :
( cnotB(X)
<=> ! [Y] :
( rr(X,Y)
=> cNothing(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_10) ).
tff(f_64,axiom,
! [X] :
( cB(X)
<=> ? [Y] :
( rr(X,Y)
& cowlThing(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
tff(f_100,axiom,
! [X] :
( cnotAorB(X)
<=> ( cnotB(X)
& cnotA(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
tff(f_56,axiom,
! [X] :
( cAorB(X)
<=> ? [Y] :
( rs(X,Y)
& cowlThing(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
tff(f_70,axiom,
! [X] :
( cNothing(X)
=> ? [Y0] : rp(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
tff(f_77,axiom,
! [X] :
( cNothing(X)
=> ~ ? [Y] : rp(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
tff(f_93,axiom,
! [X] :
( cnotAorB(X)
<=> ! [Y] :
( rs(X,Y)
=> cNothing(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
tff(f_40,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
tff(c_2,plain,
! [X_1] : cowlThing(X_1),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_4,plain,
! [X_1] : ~ cowlNothing(X_1),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_60,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_123,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_60]) ).
tff(c_177,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_123]) ).
tff(c_255,plain,
~ cA('#skF_13'),
inference(splitLeft,[status(thm)],[c_177]) ).
tff(c_240,plain,
! [X_60] :
( rq(X_60,'#skF_5'(X_60))
| cnotA(X_60) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_10,plain,
! [X_3,Y_6] :
( cA(X_3)
| ~ cowlThing(Y_6)
| ~ rq(X_3,Y_6) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_135,plain,
! [X_3,Y_6] :
( cA(X_3)
| ~ rq(X_3,Y_6) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10]) ).
tff(c_244,plain,
! [X_60] :
( cA(X_60)
| cnotA(X_60) ),
inference(resolution,[status(thm)],[c_240,c_135]) ).
tff(c_229,plain,
! [X_57] :
( rr(X_57,'#skF_7'(X_57))
| cnotB(X_57) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_22,plain,
! [X_11,Y_14] :
( cB(X_11)
| ~ cowlThing(Y_14)
| ~ rr(X_11,Y_14) ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_133,plain,
! [X_11,Y_14] :
( cB(X_11)
| ~ rr(X_11,Y_14) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22]) ).
tff(c_233,plain,
! [X_57] :
( cB(X_57)
| cnotB(X_57) ),
inference(resolution,[status(thm)],[c_229,c_133]) ).
tff(c_246,plain,
! [X_62] :
( cnotAorB(X_62)
| ~ cnotA(X_62)
| ~ cnotB(X_62) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_253,plain,
! [X_57] :
( cnotAorB(X_57)
| ~ cnotA(X_57)
| cB(X_57) ),
inference(resolution,[status(thm)],[c_233,c_246]) ).
tff(c_20,plain,
! [X_7] :
( rs(X_7,'#skF_2'(X_7))
| ~ cAorB(X_7) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_223,plain,
! [X_55] :
( rp(X_55,'#skF_4'(X_55))
| ~ cNothing(X_55) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_30,plain,
! [X_17,Y_19] :
( ~ rp(X_17,Y_19)
| ~ cNothing(X_17) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_227,plain,
! [X_55] : ~ cNothing(X_55),
inference(resolution,[status(thm)],[c_223,c_30]) ).
tff(c_38,plain,
! [Y_27,X_24] :
( cNothing(Y_27)
| ~ rs(X_24,Y_27)
| ~ cnotAorB(X_24) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_311,plain,
! [X_73,Y_74] :
( ~ rs(X_73,Y_74)
| ~ cnotAorB(X_73) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_38]) ).
tff(c_320,plain,
! [X_75] :
( ~ cnotAorB(X_75)
| ~ cAorB(X_75) ),
inference(resolution,[status(thm)],[c_20,c_311]) ).
tff(c_329,plain,
! [X_76] :
( ~ cAorB(X_76)
| ~ cnotA(X_76)
| cB(X_76) ),
inference(resolution,[status(thm)],[c_253,c_320]) ).
tff(c_338,plain,
! [X_77] :
( ~ cAorB(X_77)
| cB(X_77)
| cA(X_77) ),
inference(resolution,[status(thm)],[c_244,c_329]) ).
tff(c_72,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_104,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_72]) ).
tff(c_139,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_104]) ).
tff(c_197,plain,
~ cB('#skF_13'),
inference(splitLeft,[status(thm)],[c_139]) ).
tff(c_344,plain,
( ~ cAorB('#skF_13')
| cA('#skF_13') ),
inference(resolution,[status(thm)],[c_338,c_197]) ).
tff(c_348,plain,
~ cAorB('#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_255,c_344]) ).
tff(c_94,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_103,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_94]) ).
tff(c_137,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_103]) ).
tff(c_353,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_348,c_137]) ).
tff(c_354,plain,
~ cAorB('#skF_12'),
inference(splitLeft,[status(thm)],[c_353]) ).
tff(c_212,plain,
! [X_52] :
( rs(X_52,'#skF_6'(X_52))
| cnotAorB(X_52) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_16,plain,
! [X_7,Y_10] :
( cAorB(X_7)
| ~ cowlThing(Y_10)
| ~ rs(X_7,Y_10) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_131,plain,
! [X_7,Y_10] :
( cAorB(X_7)
| ~ rs(X_7,Y_10) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16]) ).
tff(c_217,plain,
! [X_53] :
( cAorB(X_53)
| cnotAorB(X_53) ),
inference(resolution,[status(thm)],[c_212,c_131]) ).
tff(c_46,plain,
! [X_28] :
( cnotA(X_28)
| ~ cnotAorB(X_28) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_221,plain,
! [X_53] :
( cnotA(X_53)
| cAorB(X_53) ),
inference(resolution,[status(thm)],[c_217,c_46]) ).
tff(c_14,plain,
! [X_3] :
( rq(X_3,'#skF_1'(X_3))
| ~ cA(X_3) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_32,plain,
! [Y_23,X_20] :
( cNothing(Y_23)
| ~ rq(X_20,Y_23)
| ~ cnotA(X_20) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_262,plain,
! [X_64,Y_65] :
( ~ rq(X_64,Y_65)
| ~ cnotA(X_64) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_32]) ).
tff(c_271,plain,
! [X_66] :
( ~ cnotA(X_66)
| ~ cA(X_66) ),
inference(resolution,[status(thm)],[c_14,c_262]) ).
tff(c_279,plain,
! [X_53] :
( ~ cA(X_53)
| cAorB(X_53) ),
inference(resolution,[status(thm)],[c_221,c_271]) ).
tff(c_358,plain,
~ cA('#skF_12'),
inference(resolution,[status(thm)],[c_279,c_354]) ).
tff(c_8,plain,
! [X_2] :
( xsd_string(X_2)
| xsd_integer(X_2) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_96,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_112,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_96]) ).
tff(c_155,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_112]) ).
tff(c_362,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_348,c_358,c_155]) ).
tff(c_363,plain,
~ xsd_string('#skF_10'),
inference(splitLeft,[status(thm)],[c_362]) ).
tff(c_367,plain,
xsd_integer('#skF_10'),
inference(resolution,[status(thm)],[c_8,c_363]) ).
tff(c_102,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_113,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_102]) ).
tff(c_157,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_113]) ).
tff(c_386,plain,
( xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_367,c_157]) ).
tff(c_387,plain,
( xsd_string('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_348,c_358,c_386]) ).
tff(c_388,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_387]) ).
tff(c_216,plain,
! [X_52] :
( cAorB(X_52)
| cnotAorB(X_52) ),
inference(resolution,[status(thm)],[c_212,c_131]) ).
tff(c_48,plain,
! [X_28] :
( cnotB(X_28)
| ~ cnotAorB(X_28) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_26,plain,
! [X_11] :
( rr(X_11,'#skF_3'(X_11))
| ~ cB(X_11) ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_50,plain,
! [Y_32,X_29] :
( cNothing(Y_32)
| ~ rr(X_29,Y_32)
| ~ cnotB(X_29) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_282,plain,
! [X_68,Y_69] :
( ~ rr(X_68,Y_69)
| ~ cnotB(X_68) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_50]) ).
tff(c_291,plain,
! [X_70] :
( ~ cnotB(X_70)
| ~ cB(X_70) ),
inference(resolution,[status(thm)],[c_26,c_282]) ).
tff(c_300,plain,
! [X_71] :
( ~ cB(X_71)
| ~ cnotAorB(X_71) ),
inference(resolution,[status(thm)],[c_48,c_291]) ).
tff(c_308,plain,
! [X_52] :
( ~ cB(X_52)
| cAorB(X_52) ),
inference(resolution,[status(thm)],[c_216,c_300]) ).
tff(c_391,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_388,c_308]) ).
tff(c_395,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_391]) ).
tff(c_397,plain,
~ cB('#skF_12'),
inference(splitRight,[status(thm)],[c_387]) ).
tff(c_98,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_107,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_98]) ).
tff(c_145,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_107]) ).
tff(c_399,plain,
( xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_367,c_145]) ).
tff(c_400,plain,
( xsd_integer('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_348,c_358,c_399]) ).
tff(c_401,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_400]) ).
tff(c_407,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_397,c_401]) ).
tff(c_408,plain,
xsd_integer('#skF_11'),
inference(splitRight,[status(thm)],[c_400]) ).
tff(c_396,plain,
xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_387]) ).
tff(c_6,plain,
! [X_2] :
( ~ xsd_integer(X_2)
| ~ xsd_string(X_2) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_417,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_396,c_6]) ).
tff(c_421,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_408,c_417]) ).
tff(c_422,plain,
( cB('#skF_12')
| xsd_integer('#skF_11') ),
inference(splitRight,[status(thm)],[c_362]) ).
tff(c_428,plain,
xsd_integer('#skF_11'),
inference(splitLeft,[status(thm)],[c_422]) ).
tff(c_423,plain,
xsd_string('#skF_10'),
inference(splitRight,[status(thm)],[c_362]) ).
tff(c_100,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_120,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_100]) ).
tff(c_171,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_120]) ).
tff(c_445,plain,
( xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_423,c_171]) ).
tff(c_446,plain,
( xsd_string('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_348,c_358,c_445]) ).
tff(c_447,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_446]) ).
tff(c_450,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_447,c_308]) ).
tff(c_454,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_450]) ).
tff(c_455,plain,
xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_446]) ).
tff(c_466,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_455,c_6]) ).
tff(c_470,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_428,c_466]) ).
tff(c_471,plain,
cB('#skF_12'),
inference(splitRight,[status(thm)],[c_422]) ).
tff(c_475,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_471,c_308]) ).
tff(c_479,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_475]) ).
tff(c_480,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11') ),
inference(splitRight,[status(thm)],[c_353]) ).
tff(c_482,plain,
~ xsd_integer('#skF_10'),
inference(splitLeft,[status(thm)],[c_480]) ).
tff(c_481,plain,
cAorB('#skF_12'),
inference(splitRight,[status(thm)],[c_353]) ).
tff(c_88,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_115,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_88]) ).
tff(c_161,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_115]) ).
tff(c_493,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_481,c_161]) ).
tff(c_494,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11') ),
inference(negUnitSimplification,[status(thm)],[c_348,c_493]) ).
tff(c_495,plain,
~ xsd_string('#skF_10'),
inference(splitLeft,[status(thm)],[c_494]) ).
tff(c_498,plain,
xsd_integer('#skF_10'),
inference(resolution,[status(thm)],[c_8,c_495]) ).
tff(c_502,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_482,c_498]) ).
tff(c_503,plain,
xsd_integer('#skF_11'),
inference(splitRight,[status(thm)],[c_494]) ).
tff(c_504,plain,
xsd_string('#skF_10'),
inference(splitRight,[status(thm)],[c_494]) ).
tff(c_92,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_108,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_92]) ).
tff(c_147,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_108]) ).
tff(c_510,plain,
( xsd_string('#skF_11')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_481,c_504,c_147]) ).
tff(c_511,plain,
xsd_string('#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_348,c_510]) ).
tff(c_514,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_511,c_6]) ).
tff(c_518,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_503,c_514]) ).
tff(c_519,plain,
xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_480]) ).
tff(c_524,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_519,c_6]) ).
tff(c_520,plain,
xsd_integer('#skF_10'),
inference(splitRight,[status(thm)],[c_480]) ).
tff(c_90,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_110,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_90]) ).
tff(c_151,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_110]) ).
tff(c_526,plain,
( xsd_integer('#skF_11')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_481,c_520,c_151]) ).
tff(c_527,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_348,c_524,c_526]) ).
tff(c_529,plain,
cA('#skF_13'),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_528,plain,
( ~ cAorB('#skF_12')
| ~ xsd_string('#skF_10')
| xsd_string('#skF_11') ),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_530,plain,
~ xsd_string('#skF_10'),
inference(splitLeft,[status(thm)],[c_528]) ).
tff(c_534,plain,
xsd_integer('#skF_10'),
inference(resolution,[status(thm)],[c_8,c_530]) ).
tff(c_575,plain,
( xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| cAorB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_534,c_137]) ).
tff(c_576,plain,
~ cAorB('#skF_12'),
inference(splitLeft,[status(thm)],[c_575]) ).
tff(c_578,plain,
! [X_84,Y_85] :
( ~ rq(X_84,Y_85)
| ~ cnotA(X_84) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_32]) ).
tff(c_587,plain,
! [X_86] :
( ~ cnotA(X_86)
| ~ cA(X_86) ),
inference(resolution,[status(thm)],[c_14,c_578]) ).
tff(c_596,plain,
! [X_87] :
( ~ cA(X_87)
| cAorB(X_87) ),
inference(resolution,[status(thm)],[c_221,c_587]) ).
tff(c_600,plain,
~ cA('#skF_12'),
inference(resolution,[status(thm)],[c_596,c_576]) ).
tff(c_66,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_118,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_66]) ).
tff(c_167,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_118]) ).
tff(c_655,plain,
( xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_534,c_167]) ).
tff(c_656,plain,
( xsd_integer('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_600,c_655]) ).
tff(c_657,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_656]) ).
tff(c_602,plain,
! [X_88,Y_89] :
( ~ rr(X_88,Y_89)
| ~ cnotB(X_88) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_50]) ).
tff(c_611,plain,
! [X_90] :
( ~ cnotB(X_90)
| ~ cB(X_90) ),
inference(resolution,[status(thm)],[c_26,c_602]) ).
tff(c_620,plain,
! [X_91] :
( ~ cB(X_91)
| ~ cnotAorB(X_91) ),
inference(resolution,[status(thm)],[c_48,c_611]) ).
tff(c_628,plain,
! [X_52] :
( ~ cB(X_52)
| cAorB(X_52) ),
inference(resolution,[status(thm)],[c_216,c_620]) ).
tff(c_660,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_657,c_628]) ).
tff(c_664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_576,c_660]) ).
tff(c_665,plain,
xsd_integer('#skF_11'),
inference(splitRight,[status(thm)],[c_656]) ).
tff(c_666,plain,
~ cB('#skF_12'),
inference(splitRight,[status(thm)],[c_656]) ).
tff(c_70,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_114,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_70]) ).
tff(c_159,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_114]) ).
tff(c_675,plain,
( xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_534,c_159]) ).
tff(c_676,plain,
xsd_string('#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_666,c_600,c_675]) ).
tff(c_679,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_676,c_6]) ).
tff(c_683,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_665,c_679]) ).
tff(c_685,plain,
cAorB('#skF_12'),
inference(splitRight,[status(thm)],[c_575]) ).
tff(c_62,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_105,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_62]) ).
tff(c_141,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_105]) ).
tff(c_752,plain,
xsd_string('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_685,c_534,c_141]) ).
tff(c_684,plain,
( cAorB('#skF_13')
| xsd_string('#skF_11') ),
inference(splitRight,[status(thm)],[c_575]) ).
tff(c_686,plain,
xsd_string('#skF_11'),
inference(splitLeft,[status(thm)],[c_684]) ).
tff(c_690,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_686,c_6]) ).
tff(c_58,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_124,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_58]) ).
tff(c_179,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_124]) ).
tff(c_747,plain,
xsd_integer('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_685,c_534,c_179]) ).
tff(c_748,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_690,c_747]) ).
tff(c_750,plain,
~ xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_684]) ).
tff(c_758,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_752,c_750]) ).
tff(c_759,plain,
( ~ cAorB('#skF_12')
| xsd_string('#skF_11') ),
inference(splitRight,[status(thm)],[c_528]) ).
tff(c_765,plain,
~ cAorB('#skF_12'),
inference(splitLeft,[status(thm)],[c_759]) ).
tff(c_772,plain,
! [X_103,Y_104] :
( ~ rq(X_103,Y_104)
| ~ cnotA(X_103) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_32]) ).
tff(c_781,plain,
! [X_105] :
( ~ cnotA(X_105)
| ~ cA(X_105) ),
inference(resolution,[status(thm)],[c_14,c_772]) ).
tff(c_790,plain,
! [X_106] :
( ~ cA(X_106)
| cAorB(X_106) ),
inference(resolution,[status(thm)],[c_221,c_781]) ).
tff(c_794,plain,
~ cA('#skF_12'),
inference(resolution,[status(thm)],[c_790,c_765]) ).
tff(c_760,plain,
xsd_string('#skF_10'),
inference(splitRight,[status(thm)],[c_528]) ).
tff(c_64,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_119,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_64]) ).
tff(c_169,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_119]) ).
tff(c_883,plain,
( xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_760,c_169]) ).
tff(c_884,plain,
( xsd_integer('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_794,c_883]) ).
tff(c_885,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_884]) ).
tff(c_796,plain,
! [X_107,Y_108] :
( ~ rr(X_107,Y_108)
| ~ cnotB(X_107) ),
inference(negUnitSimplification,[status(thm)],[c_227,c_50]) ).
tff(c_805,plain,
! [X_109] :
( ~ cnotB(X_109)
| ~ cB(X_109) ),
inference(resolution,[status(thm)],[c_26,c_796]) ).
tff(c_814,plain,
! [X_110] :
( ~ cB(X_110)
| ~ cnotAorB(X_110) ),
inference(resolution,[status(thm)],[c_48,c_805]) ).
tff(c_822,plain,
! [X_52] :
( ~ cB(X_52)
| cAorB(X_52) ),
inference(resolution,[status(thm)],[c_216,c_814]) ).
tff(c_888,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_885,c_822]) ).
tff(c_892,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_765,c_888]) ).
tff(c_893,plain,
xsd_integer('#skF_11'),
inference(splitRight,[status(thm)],[c_884]) ).
tff(c_894,plain,
~ cB('#skF_12'),
inference(splitRight,[status(thm)],[c_884]) ).
tff(c_68,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_116,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_68]) ).
tff(c_163,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_116]) ).
tff(c_917,plain,
( xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_760,c_163]) ).
tff(c_918,plain,
xsd_string('#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_894,c_794,c_917]) ).
tff(c_921,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_918,c_6]) ).
tff(c_925,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_893,c_921]) ).
tff(c_926,plain,
xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_759]) ).
tff(c_931,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_926,c_6]) ).
tff(c_927,plain,
cAorB('#skF_12'),
inference(splitRight,[status(thm)],[c_759]) ).
tff(c_56,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_106,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_56]) ).
tff(c_143,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cA('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_106]) ).
tff(c_1043,plain,
xsd_integer('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_529,c_927,c_760,c_143]) ).
tff(c_1044,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_931,c_1043]) ).
tff(c_1046,plain,
cB('#skF_13'),
inference(splitRight,[status(thm)],[c_139]) ).
tff(c_1074,plain,
~ cAorB('#skF_12'),
inference(splitLeft,[status(thm)],[c_151]) ).
tff(c_1058,plain,
! [X_140] :
( rs(X_140,'#skF_6'(X_140))
| cnotAorB(X_140) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_1063,plain,
! [X_141] :
( cAorB(X_141)
| cnotAorB(X_141) ),
inference(resolution,[status(thm)],[c_1058,c_131]) ).
tff(c_1067,plain,
! [X_141] :
( cnotA(X_141)
| cAorB(X_141) ),
inference(resolution,[status(thm)],[c_1063,c_46]) ).
tff(c_1080,plain,
! [X_145] :
( rp(X_145,'#skF_4'(X_145))
| ~ cNothing(X_145) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_1084,plain,
! [X_145] : ~ cNothing(X_145),
inference(resolution,[status(thm)],[c_1080,c_30]) ).
tff(c_1143,plain,
! [X_157,Y_158] :
( ~ rq(X_157,Y_158)
| ~ cnotA(X_157) ),
inference(negUnitSimplification,[status(thm)],[c_1084,c_32]) ).
tff(c_1152,plain,
! [X_159] :
( ~ cnotA(X_159)
| ~ cA(X_159) ),
inference(resolution,[status(thm)],[c_14,c_1143]) ).
tff(c_1161,plain,
! [X_160] :
( ~ cA(X_160)
| cAorB(X_160) ),
inference(resolution,[status(thm)],[c_1067,c_1152]) ).
tff(c_1165,plain,
~ cA('#skF_12'),
inference(resolution,[status(thm)],[c_1161,c_1074]) ).
tff(c_82,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_122,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_82]) ).
tff(c_175,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_122]) ).
tff(c_1220,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_175]) ).
tff(c_1221,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_1165,c_1220]) ).
tff(c_1222,plain,
~ xsd_integer('#skF_10'),
inference(splitLeft,[status(thm)],[c_1221]) ).
tff(c_80,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_125,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_80]) ).
tff(c_181,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_125]) ).
tff(c_1212,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_181]) ).
tff(c_1213,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_1165,c_1212]) ).
tff(c_1214,plain,
~ xsd_string('#skF_10'),
inference(splitLeft,[status(thm)],[c_1213]) ).
tff(c_1218,plain,
xsd_integer('#skF_10'),
inference(resolution,[status(thm)],[c_8,c_1214]) ).
tff(c_1223,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1222,c_1218]) ).
tff(c_1224,plain,
( cB('#skF_12')
| xsd_integer('#skF_11') ),
inference(splitRight,[status(thm)],[c_1221]) ).
tff(c_1230,plain,
xsd_integer('#skF_11'),
inference(splitLeft,[status(thm)],[c_1224]) ).
tff(c_1225,plain,
xsd_integer('#skF_10'),
inference(splitRight,[status(thm)],[c_1221]) ).
tff(c_86,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_117,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_86]) ).
tff(c_165,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_117]) ).
tff(c_1245,plain,
( xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_1225,c_165]) ).
tff(c_1246,plain,
( xsd_string('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_1165,c_1245]) ).
tff(c_1247,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_1246]) ).
tff(c_1062,plain,
! [X_140] :
( cAorB(X_140)
| cnotAorB(X_140) ),
inference(resolution,[status(thm)],[c_1058,c_131]) ).
tff(c_1167,plain,
! [X_161,Y_162] :
( ~ rr(X_161,Y_162)
| ~ cnotB(X_161) ),
inference(negUnitSimplification,[status(thm)],[c_1084,c_50]) ).
tff(c_1176,plain,
! [X_163] :
( ~ cnotB(X_163)
| ~ cB(X_163) ),
inference(resolution,[status(thm)],[c_26,c_1167]) ).
tff(c_1185,plain,
! [X_164] :
( ~ cB(X_164)
| ~ cnotAorB(X_164) ),
inference(resolution,[status(thm)],[c_48,c_1176]) ).
tff(c_1193,plain,
! [X_140] :
( ~ cB(X_140)
| cAorB(X_140) ),
inference(resolution,[status(thm)],[c_1062,c_1185]) ).
tff(c_1250,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_1247,c_1193]) ).
tff(c_1254,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1074,c_1250]) ).
tff(c_1255,plain,
xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_1246]) ).
tff(c_1264,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_1255,c_6]) ).
tff(c_1268,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1230,c_1264]) ).
tff(c_1269,plain,
cB('#skF_12'),
inference(splitRight,[status(thm)],[c_1224]) ).
tff(c_1273,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_1269,c_1193]) ).
tff(c_1277,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1074,c_1273]) ).
tff(c_1278,plain,
( cB('#skF_12')
| xsd_integer('#skF_11') ),
inference(splitRight,[status(thm)],[c_1213]) ).
tff(c_1284,plain,
xsd_integer('#skF_11'),
inference(splitLeft,[status(thm)],[c_1278]) ).
tff(c_1279,plain,
xsd_string('#skF_10'),
inference(splitRight,[status(thm)],[c_1213]) ).
tff(c_84,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_121,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_84]) ).
tff(c_173,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_121]) ).
tff(c_1286,plain,
( xsd_string('#skF_11')
| cA('#skF_12')
| cB('#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_1279,c_173]) ).
tff(c_1287,plain,
( xsd_string('#skF_11')
| cB('#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_1165,c_1286]) ).
tff(c_1288,plain,
cB('#skF_12'),
inference(splitLeft,[status(thm)],[c_1287]) ).
tff(c_1294,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_1288,c_1193]) ).
tff(c_1298,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1074,c_1294]) ).
tff(c_1299,plain,
xsd_string('#skF_11'),
inference(splitRight,[status(thm)],[c_1287]) ).
tff(c_1303,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_1299,c_6]) ).
tff(c_1307,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1284,c_1303]) ).
tff(c_1308,plain,
cB('#skF_12'),
inference(splitRight,[status(thm)],[c_1278]) ).
tff(c_1312,plain,
cAorB('#skF_12'),
inference(resolution,[status(thm)],[c_1308,c_1193]) ).
tff(c_1316,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1074,c_1312]) ).
tff(c_1318,plain,
cAorB('#skF_12'),
inference(splitRight,[status(thm)],[c_151]) ).
tff(c_1045,plain,
( ~ cAorB('#skF_12')
| ~ xsd_string('#skF_10')
| xsd_integer('#skF_11') ),
inference(splitRight,[status(thm)],[c_139]) ).
tff(c_1320,plain,
( ~ xsd_string('#skF_10')
| xsd_integer('#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_1318,c_1045]) ).
tff(c_1321,plain,
~ xsd_string('#skF_10'),
inference(splitLeft,[status(thm)],[c_1320]) ).
tff(c_1325,plain,
xsd_integer('#skF_10'),
inference(resolution,[status(thm)],[c_8,c_1321]) ).
tff(c_74,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_111,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_74]) ).
tff(c_153,plain,
( ~ xsd_integer('#skF_10')
| xsd_integer('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_111]) ).
tff(c_1337,plain,
xsd_integer('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_1318,c_1325,c_153]) ).
tff(c_78,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_126,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_78]) ).
tff(c_183,plain,
( ~ xsd_integer('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_126]) ).
tff(c_1455,plain,
xsd_string('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_1318,c_1325,c_183]) ).
tff(c_1458,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_1455,c_6]) ).
tff(c_1462,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1337,c_1458]) ).
tff(c_1463,plain,
xsd_integer('#skF_11'),
inference(splitRight,[status(thm)],[c_1320]) ).
tff(c_1464,plain,
xsd_string('#skF_10'),
inference(splitRight,[status(thm)],[c_1320]) ).
tff(c_76,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9')
| cowlNothing('#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_109,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13')
| ~ cowlThing('#skF_9') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_76]) ).
tff(c_149,plain,
( ~ xsd_string('#skF_10')
| xsd_string('#skF_11')
| ~ cAorB('#skF_12')
| ~ cB('#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_109]) ).
tff(c_1609,plain,
xsd_string('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_1318,c_1464,c_149]) ).
tff(c_1612,plain,
~ xsd_integer('#skF_11'),
inference(resolution,[status(thm)],[c_1609,c_6]) ).
tff(c_1616,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1463,c_1612]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : KRS132+1 : TPTP v9.0.0. Released v3.1.0.
% 0.06/0.07 % 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.06/0.25 % Computer : n021.cluster.edu
% 0.06/0.25 % Model : x86_64 x86_64
% 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.25 % Memory : 8042.1875MB
% 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.25 % CPULimit : 300
% 0.06/0.25 % WCLimit : 300
% 0.06/0.25 % DateTime : Tue Apr 8 03:00:13 EDT 2025
% 0.06/0.25 % CPUTime :
% 4.73/1.97 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/2.01
% 5.00/2.01 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------