%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS172+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n016.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:09 PM UTC 2025
% Result : Theorem 6.13s 2.97s
% Output : CNFRefutation 6.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 9
% Syntax : Number of formulae : 284 ( 144 unt; 0 typ; 0 def)
% Number of atoms : 591 ( 55 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 555 ( 248 ~; 292 |; 6 &)
% ( 5 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 79 ( 79 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rq > rp > xsd_string > xsd_integer > cowlThing > cowlNothing > cd > #nlpp > iv > #skF_7 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_8 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(rq,type,
rq: ( $i * $i ) > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(iv,type,
iv: $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(rp,type,
rp: ( $i * $i ) > $o ).
tff(cd,type,
cd: $i > $o ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(f_94,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
tff(f_88,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
tff(f_149,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X,Y] :
( rq(X,Y)
<=> rp(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
tff(f_128,axiom,
! [X,Y] :
( rq(X,Y)
=> cd(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
tff(f_99,axiom,
! [X] :
( cd(X)
<=> rq(X,iv) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
tff(f_123,axiom,
! [X,Y,Z] :
( ( rq(X,Y)
& rq(X,Z) )
=> ( Y = Z ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
tff(f_104,axiom,
! [X] :
( cd(X)
<=> rp(X,iv) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
tff(f_116,axiom,
! [X,Y] :
( rp(X,Y)
=> cd(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
tff(f_111,axiom,
! [X,Y,Z] :
( ( rp(X,Y)
& rp(X,Z) )
=> ( Y = Z ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
tff(c_26,plain,
! [X_24] :
( xsd_string(X_24)
| xsd_integer(X_24) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_20,plain,
! [X_23] : cowlThing(X_23),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_22,plain,
! [X_23] : ~ cowlNothing(X_23),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_74,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_87,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_74]) ).
tff(c_115,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_87]) ).
tff(c_168,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_115]) ).
tff(c_172,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_26,c_168]) ).
tff(c_72,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_80,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_72]) ).
tff(c_101,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_80]) ).
tff(c_178,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_172,c_101]) ).
tff(c_179,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_178]) ).
tff(c_42,plain,
! [X_35,Y_36] :
( cd(X_35)
| ~ rq(X_35,Y_36) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_190,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_179,c_42]) ).
tff(c_28,plain,
! [X_25] :
( rq(X_25,iv)
| ~ cd(X_25) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_146,plain,
! [Z_47,Y_48,X_49] :
( ( Z_47 = Y_48 )
| ~ rq(X_49,Z_47)
| ~ rq(X_49,Y_48) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_149,plain,
! [Y_48,X_25] :
( ( iv = Y_48 )
| ~ rq(X_25,Y_48)
| ~ cd(X_25) ),
inference(resolution,[status(thm)],[c_28,c_146]) ).
tff(c_188,plain,
( ( iv = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_179,c_149]) ).
tff(c_194,plain,
iv = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_190,c_188]) ).
tff(c_32,plain,
! [X_26] :
( rp(X_26,iv)
| ~ cd(X_26) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_227,plain,
! [X_59] :
( rp(X_59,'#skF_8')
| ~ cd(X_59) ),
inference(demodulation,[status(thm),theory(equality)],[c_194,c_32]) ).
tff(c_58,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_88,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_58]) ).
tff(c_117,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_88]) ).
tff(c_167,plain,
~ rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_117]) ).
tff(c_230,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_227,c_167]) ).
tff(c_239,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_190,c_230]) ).
tff(c_240,plain,
( rp('#skF_5','#skF_6')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_178]) ).
tff(c_242,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_240]) ).
tff(c_241,plain,
~ rq('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_178]) ).
tff(c_76,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_79,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_76]) ).
tff(c_99,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_79]) ).
tff(c_256,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_172,c_99]) ).
tff(c_257,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(negUnitSimplification,[status(thm)],[c_241,c_256]) ).
tff(c_258,plain,
rp('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_257]) ).
tff(c_38,plain,
! [X_30,Y_31] :
( cd(X_30)
| ~ rp(X_30,Y_31) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_269,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_258,c_38]) ).
tff(c_157,plain,
! [Z_52,Y_53,X_54] :
( ( Z_52 = Y_53 )
| ~ rp(X_54,Z_52)
| ~ rp(X_54,Y_53) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_160,plain,
! [Y_53,X_26] :
( ( iv = Y_53 )
| ~ rp(X_26,Y_53)
| ~ cd(X_26) ),
inference(resolution,[status(thm)],[c_32,c_157]) ).
tff(c_267,plain,
( ( iv = '#skF_6' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_258,c_160]) ).
tff(c_271,plain,
iv = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_269,c_267]) ).
tff(c_303,plain,
! [X_62] :
( rq(X_62,'#skF_6')
| ~ cd(X_62) ),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_28]) ).
tff(c_68,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_89,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_68]) ).
tff(c_119,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_89]) ).
tff(c_150,plain,
~ rq('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_119]) ).
tff(c_306,plain,
~ cd('#skF_5'),
inference(resolution,[status(thm)],[c_303,c_150]) ).
tff(c_315,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_269,c_306]) ).
tff(c_316,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_257]) ).
tff(c_24,plain,
! [X_24] :
( ~ xsd_integer(X_24)
| ~ xsd_string(X_24) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_321,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_316,c_24]) ).
tff(c_325,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_242,c_321]) ).
tff(c_326,plain,
rp('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_240]) ).
tff(c_338,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_326,c_38]) ).
tff(c_336,plain,
( ( iv = '#skF_6' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_326,c_160]) ).
tff(c_340,plain,
iv = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_338,c_336]) ).
tff(c_357,plain,
! [X_64] :
( rq(X_64,'#skF_6')
| ~ cd(X_64) ),
inference(demodulation,[status(thm),theory(equality)],[c_340,c_28]) ).
tff(c_360,plain,
~ cd('#skF_5'),
inference(resolution,[status(thm)],[c_357,c_150]) ).
tff(c_369,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_338,c_360]) ).
tff(c_370,plain,
( rq('#skF_7','#skF_8')
| rp('#skF_5','#skF_6')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_115]) ).
tff(c_376,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_370]) ).
tff(c_380,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_376,c_24]) ).
tff(c_371,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_115]) ).
tff(c_70,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_78,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_70]) ).
tff(c_97,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_78]) ).
tff(c_392,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_371,c_97]) ).
tff(c_393,plain,
( rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(negUnitSimplification,[status(thm)],[c_380,c_392]) ).
tff(c_394,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_393]) ).
tff(c_405,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_394,c_42]) ).
tff(c_403,plain,
( ( iv = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_394,c_149]) ).
tff(c_407,plain,
iv = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_405,c_403]) ).
tff(c_425,plain,
! [X_66] :
( rp(X_66,'#skF_8')
| ~ cd(X_66) ),
inference(demodulation,[status(thm),theory(equality)],[c_407,c_32]) ).
tff(c_428,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_425,c_167]) ).
tff(c_437,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_405,c_428]) ).
tff(c_438,plain,
rp('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_393]) ).
tff(c_451,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_438,c_38]) ).
tff(c_449,plain,
( ( iv = '#skF_6' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_438,c_160]) ).
tff(c_453,plain,
iv = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_451,c_449]) ).
tff(c_468,plain,
! [X_68] :
( rq(X_68,'#skF_6')
| ~ cd(X_68) ),
inference(demodulation,[status(thm),theory(equality)],[c_453,c_28]) ).
tff(c_471,plain,
~ cd('#skF_5'),
inference(resolution,[status(thm)],[c_468,c_150]) ).
tff(c_480,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_451,c_471]) ).
tff(c_481,plain,
( rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(splitRight,[status(thm)],[c_370]) ).
tff(c_487,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_481]) ).
tff(c_498,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_487,c_42]) ).
tff(c_496,plain,
( ( iv = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_487,c_149]) ).
tff(c_502,plain,
iv = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_498,c_496]) ).
tff(c_533,plain,
! [X_71] :
( rp(X_71,'#skF_8')
| ~ cd(X_71) ),
inference(demodulation,[status(thm),theory(equality)],[c_502,c_32]) ).
tff(c_536,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_533,c_167]) ).
tff(c_545,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_498,c_536]) ).
tff(c_546,plain,
rp('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_481]) ).
tff(c_558,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_546,c_38]) ).
tff(c_556,plain,
( ( iv = '#skF_6' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_546,c_160]) ).
tff(c_560,plain,
iv = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_558,c_556]) ).
tff(c_593,plain,
! [X_74] :
( rq(X_74,'#skF_6')
| ~ cd(X_74) ),
inference(demodulation,[status(thm),theory(equality)],[c_560,c_28]) ).
tff(c_596,plain,
~ cd('#skF_5'),
inference(resolution,[status(thm)],[c_593,c_150]) ).
tff(c_605,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_558,c_596]) ).
tff(c_607,plain,
rp('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_117]) ).
tff(c_606,plain,
( ~ xsd_string('#skF_3')
| rp('#skF_5','#skF_6')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_117]) ).
tff(c_619,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_606]) ).
tff(c_623,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_26,c_619]) ).
tff(c_60,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_86,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_60]) ).
tff(c_113,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_86]) ).
tff(c_635,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_607,c_623,c_113]) ).
tff(c_636,plain,
rp('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_635]) ).
tff(c_643,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_636,c_38]) ).
tff(c_618,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_607,c_38]) ).
tff(c_616,plain,
( ( iv = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_607,c_160]) ).
tff(c_625,plain,
iv = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_618,c_616]) ).
tff(c_697,plain,
! [X_78] :
( rq(X_78,'#skF_8')
| ~ cd(X_78) ),
inference(demodulation,[status(thm),theory(equality)],[c_625,c_28]) ).
tff(c_628,plain,
! [X_26] :
( rp(X_26,'#skF_8')
| ~ cd(X_26) ),
inference(demodulation,[status(thm),theory(equality)],[c_625,c_32]) ).
tff(c_36,plain,
! [Z_29,Y_28,X_27] :
( ( Z_29 = Y_28 )
| ~ rp(X_27,Z_29)
| ~ rp(X_27,Y_28) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_666,plain,
! [Y_77] :
( ( Y_77 = '#skF_6' )
| ~ rp('#skF_5',Y_77) ),
inference(resolution,[status(thm)],[c_636,c_36]) ).
tff(c_670,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_628,c_666]) ).
tff(c_676,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_643,c_670]) ).
tff(c_683,plain,
~ rq('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_676,c_150]) ).
tff(c_700,plain,
~ cd('#skF_5'),
inference(resolution,[status(thm)],[c_697,c_683]) ).
tff(c_709,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_643,c_700]) ).
tff(c_711,plain,
~ rp('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_635]) ).
tff(c_710,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_635]) ).
tff(c_715,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_710,c_24]) ).
tff(c_56,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_90,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_56]) ).
tff(c_121,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_90]) ).
tff(c_818,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_607,c_623,c_121]) ).
tff(c_819,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_711,c_715,c_818]) ).
tff(c_820,plain,
( xsd_string('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(splitRight,[status(thm)],[c_606]) ).
tff(c_826,plain,
rp('#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_820]) ).
tff(c_837,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_826,c_38]) ).
tff(c_839,plain,
iv = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_618,c_616]) ).
tff(c_881,plain,
! [X_89] :
( rq(X_89,'#skF_8')
| ~ cd(X_89) ),
inference(demodulation,[status(thm),theory(equality)],[c_839,c_28]) ).
tff(c_835,plain,
( ( iv = '#skF_6' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_826,c_160]) ).
tff(c_851,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_837,c_839,c_835]) ).
tff(c_853,plain,
~ rq('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_851,c_150]) ).
tff(c_884,plain,
~ cd('#skF_5'),
inference(resolution,[status(thm)],[c_881,c_853]) ).
tff(c_893,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_837,c_884]) ).
tff(c_895,plain,
~ rp('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_820]) ).
tff(c_894,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_820]) ).
tff(c_899,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_894,c_24]) ).
tff(c_821,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_606]) ).
tff(c_54,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_91,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_54]) ).
tff(c_123,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| rp('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_91]) ).
tff(c_1018,plain,
( xsd_integer('#skF_4')
| rp('#skF_5','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_607,c_821,c_123]) ).
tff(c_1019,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_895,c_899,c_1018]) ).
tff(c_1020,plain,
( ~ xsd_integer('#skF_3')
| rq('#skF_7','#skF_8')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_119]) ).
tff(c_1042,plain,
~ xsd_integer('#skF_3'),
inference(splitLeft,[status(thm)],[c_1020]) ).
tff(c_1021,plain,
rq('#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_119]) ).
tff(c_66,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_92,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_66]) ).
tff(c_125,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_92]) ).
tff(c_1338,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1021,c_125]) ).
tff(c_1339,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_1338]) ).
tff(c_1342,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_26,c_1339]) ).
tff(c_1346,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1042,c_1342]) ).
tff(c_1347,plain,
( rq('#skF_7','#skF_8')
| xsd_string('#skF_4') ),
inference(splitRight,[status(thm)],[c_1338]) ).
tff(c_1357,plain,
xsd_string('#skF_4'),
inference(splitLeft,[status(thm)],[c_1347]) ).
tff(c_1361,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1357,c_24]) ).
tff(c_1089,plain,
~ xsd_string('#skF_3'),
inference(splitLeft,[status(thm)],[c_97]) ).
tff(c_1092,plain,
xsd_integer('#skF_3'),
inference(resolution,[status(thm)],[c_26,c_1089]) ).
tff(c_1096,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1042,c_1092]) ).
tff(c_1097,plain,
( rq('#skF_7','#skF_8')
| rp('#skF_5','#skF_6')
| xsd_integer('#skF_4') ),
inference(splitRight,[status(thm)],[c_97]) ).
tff(c_1109,plain,
xsd_integer('#skF_4'),
inference(splitLeft,[status(thm)],[c_1097]) ).
tff(c_1098,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_97]) ).
tff(c_1111,plain,
( xsd_string('#skF_4')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1021,c_1098,c_125]) ).
tff(c_1112,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1111]) ).
tff(c_1123,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_1112,c_42]) ).
tff(c_1028,plain,
cd('#skF_5'),
inference(resolution,[status(thm)],[c_1021,c_42]) ).
tff(c_40,plain,
! [Z_34,Y_33,X_32] :
( ( Z_34 = Y_33 )
| ~ rq(X_32,Z_34)
| ~ rq(X_32,Y_33) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_1029,plain,
! [Y_98] :
( ( Y_98 = '#skF_6' )
| ~ rq('#skF_5',Y_98) ),
inference(resolution,[status(thm)],[c_1021,c_40]) ).
tff(c_1036,plain,
( ( iv = '#skF_6' )
| ~ cd('#skF_5') ),
inference(resolution,[status(thm)],[c_28,c_1029]) ).
tff(c_1041,plain,
iv = '#skF_6',
inference(demodulation,[status(thm),theory(equality)],[c_1028,c_1036]) ).
tff(c_1071,plain,
! [Y_48,X_25] :
( ( Y_48 = '#skF_6' )
| ~ rq(X_25,Y_48)
| ~ cd(X_25) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_149]) ).
tff(c_1121,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1112,c_1071]) ).
tff(c_1125,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1123,c_1121]) ).
tff(c_1043,plain,
! [X_26] :
( rp(X_26,'#skF_6')
| ~ cd(X_26) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_32]) ).
tff(c_1163,plain,
! [X_110] :
( rp(X_110,'#skF_8')
| ~ cd(X_110) ),
inference(demodulation,[status(thm),theory(equality)],[c_1125,c_1043]) ).
tff(c_1054,plain,
~ rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_123]) ).
tff(c_1168,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_1163,c_1054]) ).
tff(c_1176,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1123,c_1168]) ).
tff(c_1177,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1111]) ).
tff(c_1181,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1177,c_24]) ).
tff(c_1185,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1109,c_1181]) ).
tff(c_1186,plain,
( rp('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(splitRight,[status(thm)],[c_1097]) ).
tff(c_1188,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1186]) ).
tff(c_1199,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_1188,c_42]) ).
tff(c_1197,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1188,c_1071]) ).
tff(c_1201,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1199,c_1197]) ).
tff(c_1265,plain,
! [X_114] :
( rp(X_114,'#skF_8')
| ~ cd(X_114) ),
inference(demodulation,[status(thm),theory(equality)],[c_1201,c_1043]) ).
tff(c_1270,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_1265,c_1054]) ).
tff(c_1278,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1199,c_1270]) ).
tff(c_1280,plain,
~ rq('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1186]) ).
tff(c_1187,plain,
~ xsd_integer('#skF_4'),
inference(splitRight,[status(thm)],[c_1097]) ).
tff(c_62,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_85,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_62]) ).
tff(c_111,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_85]) ).
tff(c_1333,plain,
( xsd_integer('#skF_4')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1021,c_1098,c_111]) ).
tff(c_1334,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1280,c_1187,c_1333]) ).
tff(c_1336,plain,
rp('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_123]) ).
tff(c_1356,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_1336,c_38]) ).
tff(c_1403,plain,
! [Z_119,Y_120,X_121] :
( ( Z_119 = Y_120 )
| ~ rp(X_121,Z_119)
| ~ rp(X_121,Y_120) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_1413,plain,
! [Y_122] :
( ( Y_122 = '#skF_8' )
| ~ rp('#skF_7',Y_122) ),
inference(resolution,[status(thm)],[c_1336,c_1403]) ).
tff(c_1420,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1043,c_1413]) ).
tff(c_1425,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1356,c_1420]) ).
tff(c_1348,plain,
xsd_string('#skF_3'),
inference(splitRight,[status(thm)],[c_1338]) ).
tff(c_46,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_84,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_46]) ).
tff(c_109,plain,
( ~ xsd_string('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_84]) ).
tff(c_1438,plain,
( xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1336,c_1425,c_1348,c_109]) ).
tff(c_1439,plain,
~ rq('#skF_5','#skF_8'),
inference(negUnitSimplification,[status(thm)],[c_1361,c_1438]) ).
tff(c_1432,plain,
rq('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1425,c_1021]) ).
tff(c_1444,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1439,c_1432]) ).
tff(c_1446,plain,
~ xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1347]) ).
tff(c_1468,plain,
! [X_124] :
( rq(X_124,'#skF_6')
| ~ cd(X_124) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_28]) ).
tff(c_1445,plain,
rq('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1347]) ).
tff(c_1459,plain,
! [Y_33] :
( ( Y_33 = '#skF_8' )
| ~ rq('#skF_7',Y_33) ),
inference(resolution,[status(thm)],[c_1445,c_40]) ).
tff(c_1472,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1468,c_1459]) ).
tff(c_1484,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1356,c_1472]) ).
tff(c_1495,plain,
rq('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1484,c_1021]) ).
tff(c_50,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_82,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_50]) ).
tff(c_105,plain,
( ~ xsd_string('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_82]) ).
tff(c_1652,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1336,c_1495,c_1484,c_1348,c_105]) ).
tff(c_1653,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1446,c_1652]) ).
tff(c_1654,plain,
( xsd_string('#skF_4')
| rq('#skF_7','#skF_8') ),
inference(splitRight,[status(thm)],[c_1020]) ).
tff(c_1663,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1654]) ).
tff(c_1670,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_1663,c_42]) ).
tff(c_1678,plain,
! [X_141] :
( rq(X_141,'#skF_6')
| ~ cd(X_141) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_28]) ).
tff(c_1669,plain,
! [Y_33] :
( ( Y_33 = '#skF_8' )
| ~ rq('#skF_7',Y_33) ),
inference(resolution,[status(thm)],[c_1663,c_40]) ).
tff(c_1682,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1678,c_1669]) ).
tff(c_1694,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1670,c_1682]) ).
tff(c_1656,plain,
! [X_26] :
( rp(X_26,'#skF_6')
| ~ cd(X_26) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_32]) ).
tff(c_1724,plain,
! [X_142] :
( rp(X_142,'#skF_8')
| ~ cd(X_142) ),
inference(demodulation,[status(thm),theory(equality)],[c_1694,c_1656]) ).
tff(c_1662,plain,
~ rp('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_123]) ).
tff(c_1729,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_1724,c_1662]) ).
tff(c_1737,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1670,c_1729]) ).
tff(c_1739,plain,
~ rq('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1654]) ).
tff(c_1738,plain,
xsd_string('#skF_4'),
inference(splitRight,[status(thm)],[c_1654]) ).
tff(c_1743,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1738,c_24]) ).
tff(c_1655,plain,
xsd_integer('#skF_3'),
inference(splitRight,[status(thm)],[c_1020]) ).
tff(c_64,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_77,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_64]) ).
tff(c_95,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_77]) ).
tff(c_1803,plain,
( xsd_integer('#skF_4')
| rq('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_1021,c_1655,c_95]) ).
tff(c_1804,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1739,c_1743,c_1803]) ).
tff(c_1806,plain,
rp('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_123]) ).
tff(c_1810,plain,
cd('#skF_7'),
inference(resolution,[status(thm)],[c_1806,c_38]) ).
tff(c_2050,plain,
! [Z_170,Y_171,X_172] :
( ( Z_170 = Y_171 )
| ~ rp(X_172,Z_170)
| ~ rp(X_172,Y_171) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_2057,plain,
! [Y_173] :
( ( Y_173 = '#skF_8' )
| ~ rp('#skF_7',Y_173) ),
inference(resolution,[status(thm)],[c_1806,c_2050]) ).
tff(c_2061,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1656,c_2057]) ).
tff(c_2067,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1810,c_2061]) ).
tff(c_1657,plain,
! [X_25] :
( rq(X_25,'#skF_6')
| ~ cd(X_25) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_28]) ).
tff(c_2094,plain,
! [X_174] :
( rq(X_174,'#skF_8')
| ~ cd(X_174) ),
inference(demodulation,[status(thm),theory(equality)],[c_2067,c_1657]) ).
tff(c_1839,plain,
! [X_154] :
( rq(X_154,'#skF_6')
| ~ cd(X_154) ),
inference(demodulation,[status(thm),theory(equality)],[c_1041,c_28]) ).
tff(c_1819,plain,
rq('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1654]) ).
tff(c_1825,plain,
! [Y_33] :
( ( Y_33 = '#skF_8' )
| ~ rq('#skF_7',Y_33) ),
inference(resolution,[status(thm)],[c_1819,c_40]) ).
tff(c_1843,plain,
( ( '#skF_6' = '#skF_8' )
| ~ cd('#skF_7') ),
inference(resolution,[status(thm)],[c_1839,c_1825]) ).
tff(c_1855,plain,
'#skF_6' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_1810,c_1843]) ).
tff(c_1866,plain,
rq('#skF_5','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_1855,c_1021]) ).
tff(c_52,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_81,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_52]) ).
tff(c_103,plain,
( ~ xsd_integer('#skF_3')
| xsd_string('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_81]) ).
tff(c_1979,plain,
xsd_string('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1806,c_1866,c_1855,c_1655,c_103]) ).
tff(c_1983,plain,
~ xsd_integer('#skF_4'),
inference(resolution,[status(thm)],[c_1979,c_24]) ).
tff(c_48,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2')
| cowlNothing('#skF_1') ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_83,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8')
| ~ cowlThing('#skF_2') ),
inference(negUnitSimplification,[status(thm)],[c_22,c_48]) ).
tff(c_107,plain,
( ~ xsd_integer('#skF_3')
| xsd_integer('#skF_4')
| ~ rq('#skF_5','#skF_6')
| ~ rp('#skF_7','#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_20,c_83]) ).
tff(c_1993,plain,
xsd_integer('#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1806,c_1866,c_1855,c_1655,c_107]) ).
tff(c_1994,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1983,c_1993]) ).
tff(c_1996,plain,
~ rq('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1654]) ).
tff(c_2097,plain,
~ cd('#skF_7'),
inference(resolution,[status(thm)],[c_2094,c_1996]) ).
tff(c_2106,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1810,c_2097]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.08 % Problem : KRS172+1 : TPTP v9.0.0. Released v3.1.0.
% 0.03/0.08 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.08/0.28 % Computer : n016.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Tue Apr 8 03:01:08 EDT 2025
% 0.08/0.28 % CPUTime :
% 6.13/2.97 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.36/3.04
% 6.36/3.04 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------