%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS146+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 : n002.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:27 PM UTC 2025
% Result : Theorem 12.79s 4.37s
% Output : CNFRefutation 12.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 22
% Syntax : Number of formulae : 181 ( 91 unt; 0 typ; 0 def)
% Number of atoms : 562 ( 0 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 757 ( 376 ~; 351 |; 20 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 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 : 77 ( 76 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-1 aty)
% Number of variables : 34 ( 34 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rR1 > xsd_string > xsd_integer > cowlThing > cowlNothing > cTEST > cC98 > cC96 > cC94 > cC92 > cC90 > cC88 > cC86 > cC84 > cC82 > cC80 > cC8 > cC78 > cC76 > cC74 > cC72 > cC70 > cC68 > cC66 > cC64 > cC62 > cC60 > cC6 > cC58 > cC56 > cC54 > cC52 > cC50 > cC48 > cC46 > cC44 > cC42 > cC40 > cC4 > cC38 > cC36 > cC34 > cC32 > cC30 > cC28 > cC26 > cC24 > cC22 > cC20 > cC2 > cC18 > cC16 > cC140 > cC14 > cC138 > cC136 > cC134 > cC132 > cC130 > cC128 > cC126 > cC124 > cC122 > cC120 > cC12 > cC118 > cC116 > cC114 > cC112 > cC110 > cC108 > cC106 > cC104 > cC102 > cC100 > cC10 > #nlpp > iV822576 > #skF_9 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_17 > #skF_15 > #skF_1 > #skF_8 > #skF_16 > #skF_14 > #skF_10 > #skF_13 > #skF_3 > #skF_11 > #skF_12 > #skF_6
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(cC104,type,
cC104: $i > $o ).
tff(cC94,type,
cC94: $i > $o ).
tff(cC8,type,
cC8: $i > $o ).
tff(cC70,type,
cC70: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(cC14,type,
cC14: $i > $o ).
tff(cC100,type,
cC100: $i > $o ).
tff(cC130,type,
cC130: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(cC88,type,
cC88: $i > $o ).
tff('#skF_17',type,
'#skF_17': $i ).
tff(cC22,type,
cC22: $i > $o ).
tff(cC112,type,
cC112: $i > $o ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(cC34,type,
cC34: $i > $o ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(cC2,type,
cC2: $i > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(cC52,type,
cC52: $i > $o ).
tff(iV822576,type,
iV822576: $i ).
tff(cC118,type,
cC118: $i > $o ).
tff(cC16,type,
cC16: $i > $o ).
tff(cC78,type,
cC78: $i > $o ).
tff(cC10,type,
cC10: $i > $o ).
tff(cC108,type,
cC108: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(cC128,type,
cC128: $i > $o ).
tff(cC82,type,
cC82: $i > $o ).
tff(cC72,type,
cC72: $i > $o ).
tff(cC56,type,
cC56: $i > $o ).
tff(cC136,type,
cC136: $i > $o ).
tff(cTEST,type,
cTEST: $i > $o ).
tff(cC58,type,
cC58: $i > $o ).
tff(cC12,type,
cC12: $i > $o ).
tff('#skF_16',type,
'#skF_16': $i ).
tff(cC114,type,
cC114: $i > $o ).
tff(cC96,type,
cC96: $i > $o ).
tff(cC46,type,
cC46: $i > $o ).
tff(cC84,type,
cC84: $i > $o ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff(cC64,type,
cC64: $i > $o ).
tff(cC48,type,
cC48: $i > $o ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(cC38,type,
cC38: $i > $o ).
tff(cC124,type,
cC124: $i > $o ).
tff(cC6,type,
cC6: $i > $o ).
tff(cC106,type,
cC106: $i > $o ).
tff(cC18,type,
cC18: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(cC42,type,
cC42: $i > $o ).
tff(cC60,type,
cC60: $i > $o ).
tff(cC92,type,
cC92: $i > $o ).
tff(cC68,type,
cC68: $i > $o ).
tff(cC62,type,
cC62: $i > $o ).
tff(cC80,type,
cC80: $i > $o ).
tff(cC98,type,
cC98: $i > $o ).
tff(cC40,type,
cC40: $i > $o ).
tff(cC54,type,
cC54: $i > $o ).
tff(rR1,type,
rR1: ( $i * $i ) > $o ).
tff(cC76,type,
cC76: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(cC28,type,
cC28: $i > $o ).
tff(xsd_string,type,
xsd_string: $i > $o ).
tff(cC74,type,
cC74: $i > $o ).
tff(cC86,type,
cC86: $i > $o ).
tff(cC50,type,
cC50: $i > $o ).
tff(cC32,type,
cC32: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(cC116,type,
cC116: $i > $o ).
tff(cC36,type,
cC36: $i > $o ).
tff(cC110,type,
cC110: $i > $o ).
tff(cC120,type,
cC120: $i > $o ).
tff(cC44,type,
cC44: $i > $o ).
tff(cC126,type,
cC126: $i > $o ).
tff(cC66,type,
cC66: $i > $o ).
tff(cC4,type,
cC4: $i > $o ).
tff(cC134,type,
cC134: $i > $o ).
tff(cC20,type,
cC20: $i > $o ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff(cC122,type,
cC122: $i > $o ).
tff(cC138,type,
cC138: $i > $o ).
tff(cC132,type,
cC132: $i > $o ).
tff(cC30,type,
cC30: $i > $o ).
tff(cC90,type,
cC90: $i > $o ).
tff(cC140,type,
cC140: $i > $o ).
tff(cC24,type,
cC24: $i > $o ).
tff(cC26,type,
cC26: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff(cC102,type,
cC102: $i > $o ).
tff(f_573,axiom,
~ cC134(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_71) ).
tff(f_623,axiom,
~ cC112(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_87) ).
tff(f_626,axiom,
~ cC78(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_88) ).
tff(f_620,axiom,
~ cC76(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_86) ).
tff(f_483,axiom,
! [X] :
( cC80(X)
<=> ( ~ cC78(X)
& ~ cC76(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
tff(f_614,axiom,
~ cC10(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_84) ).
tff(f_585,axiom,
cC4(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_75) ).
tff(f_372,axiom,
! [X] :
( cC56(X)
<=> ( cC4(X)
& ~ cC10(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
tff(f_583,axiom,
cC34(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_74) ).
tff(f_379,axiom,
! [X] :
( cC58(X)
<=> ( cC34(X)
& cC56(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_44) ).
tff(f_591,axiom,
~ cC86(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_77) ).
tff(f_594,axiom,
~ cC92(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_78) ).
tff(f_538,axiom,
! [X] :
( cC94(X)
<=> ( ~ cC86(X)
& ~ cC92(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
tff(f_33,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
tff(f_599,axiom,
cowlThing(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_80) ).
tff(f_675,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC94(iV822576)
& cowlThing(iV822576)
& cC58(iV822576)
& cC116(iV822576)
& cC56(iV822576)
& cC110(iV822576)
& cC114(iV822576)
& cC136(iV822576)
& cC80(iV822576) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
tff(f_39,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
tff(f_110,axiom,
! [X] :
( cC116(X)
<=> ( cC114(X)
& cC80(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_10) ).
tff(f_103,axiom,
! [X] :
( cC114(X)
<=> ( ~ cC96(X)
& ~ cC112(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
tff(f_588,axiom,
~ cC96(iV822576),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_76) ).
tff(f_196,axiom,
! [X] :
( cC136(X)
<=> ( cC116(X)
& ~ cC134(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
tff(f_94,axiom,
! [X] :
( cC112(X)
<=> ( ~ cC110(X)
& cC4(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
tff(c_412,plain,
~ cC134(iV822576),
inference(cnfTransformation,[status(thm)],[f_573]) ).
tff(c_444,plain,
~ cC112(iV822576),
inference(cnfTransformation,[status(thm)],[f_623]) ).
tff(c_446,plain,
~ cC78(iV822576),
inference(cnfTransformation,[status(thm)],[f_626]) ).
tff(c_442,plain,
~ cC76(iV822576),
inference(cnfTransformation,[status(thm)],[f_620]) ).
tff(c_9413,plain,
! [X_1905] :
( cC80(X_1905)
| cC76(X_1905)
| cC78(X_1905) ),
inference(cnfTransformation,[status(thm)],[f_483]) ).
tff(c_4462,plain,
! [X_939] :
( cC80(X_939)
| cC76(X_939)
| cC78(X_939) ),
inference(cnfTransformation,[status(thm)],[f_483]) ).
tff(c_438,plain,
~ cC10(iV822576),
inference(cnfTransformation,[status(thm)],[f_614]) ).
tff(c_420,plain,
cC4(iV822576),
inference(cnfTransformation,[status(thm)],[f_585]) ).
tff(c_256,plain,
! [X_71] :
( cC56(X_71)
| cC10(X_71)
| ~ cC4(X_71) ),
inference(cnfTransformation,[status(thm)],[f_372]) ).
tff(c_418,plain,
cC34(iV822576),
inference(cnfTransformation,[status(thm)],[f_583]) ).
tff(c_2656,plain,
! [X_582] :
( cC58(X_582)
| ~ cC56(X_582)
| ~ cC34(X_582) ),
inference(cnfTransformation,[status(thm)],[f_379]) ).
tff(c_424,plain,
~ cC86(iV822576),
inference(cnfTransformation,[status(thm)],[f_591]) ).
tff(c_426,plain,
~ cC92(iV822576),
inference(cnfTransformation,[status(thm)],[f_594]) ).
tff(c_1649,plain,
! [X_352] :
( cC94(X_352)
| cC92(X_352)
| cC86(X_352) ),
inference(cnfTransformation,[status(thm)],[f_538]) ).
tff(c_2,plain,
! [X_1] : cowlThing(X_1),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_4,plain,
! [X_1] : ~ cowlNothing(X_1),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_430,plain,
cowlThing(iV822576),
inference(cnfTransformation,[status(thm)],[f_599]) ).
tff(c_452,plain,
( ~ xsd_string('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(cnfTransformation,[status(thm)],[f_675]) ).
tff(c_460,plain,
( ~ xsd_string('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(demodulation,[status(thm),theory(equality)],[c_430,c_452]) ).
tff(c_468,plain,
( ~ xsd_string('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_460]) ).
tff(c_475,plain,
( ~ xsd_string('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_468]) ).
tff(c_482,plain,
~ cC94(iV822576),
inference(splitLeft,[status(thm)],[c_475]) ).
tff(c_1658,plain,
( cC92(iV822576)
| cC86(iV822576) ),
inference(resolution,[status(thm)],[c_1649,c_482]) ).
tff(c_1664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_424,c_426,c_1658]) ).
tff(c_1666,plain,
cC94(iV822576),
inference(splitRight,[status(thm)],[c_475]) ).
tff(c_456,plain,
( ~ xsd_string('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(cnfTransformation,[status(thm)],[f_675]) ).
tff(c_464,plain,
( ~ xsd_string('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(demodulation,[status(thm),theory(equality)],[c_430,c_456]) ).
tff(c_470,plain,
( ~ xsd_string('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_464]) ).
tff(c_479,plain,
( ~ xsd_string('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_470]) ).
tff(c_1677,plain,
( ~ xsd_string('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576) ),
inference(demodulation,[status(thm),theory(equality)],[c_1666,c_479]) ).
tff(c_1678,plain,
~ cC58(iV822576),
inference(splitLeft,[status(thm)],[c_1677]) ).
tff(c_2665,plain,
( ~ cC56(iV822576)
| ~ cC34(iV822576) ),
inference(resolution,[status(thm)],[c_2656,c_1678]) ).
tff(c_2670,plain,
~ cC56(iV822576),
inference(demodulation,[status(thm),theory(equality)],[c_418,c_2665]) ).
tff(c_2673,plain,
( cC10(iV822576)
| ~ cC4(iV822576) ),
inference(resolution,[status(thm)],[c_256,c_2670]) ).
tff(c_2676,plain,
cC10(iV822576),
inference(demodulation,[status(thm),theory(equality)],[c_420,c_2673]) ).
tff(c_2678,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_438,c_2676]) ).
tff(c_2680,plain,
cC58(iV822576),
inference(splitRight,[status(thm)],[c_1677]) ).
tff(c_454,plain,
( ~ xsd_integer('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(cnfTransformation,[status(thm)],[f_675]) ).
tff(c_466,plain,
( ~ xsd_integer('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(demodulation,[status(thm),theory(equality)],[c_430,c_454]) ).
tff(c_467,plain,
( ~ xsd_integer('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_466]) ).
tff(c_473,plain,
( ~ xsd_integer('#skF_16')
| xsd_integer('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_467]) ).
tff(c_1667,plain,
~ cC94(iV822576),
inference(splitLeft,[status(thm)],[c_473]) ).
tff(c_1672,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1666,c_1667]) ).
tff(c_1673,plain,
( ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ xsd_integer('#skF_16')
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_473]) ).
tff(c_2694,plain,
( ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ xsd_integer('#skF_16')
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_2680,c_1673]) ).
tff(c_2695,plain,
~ xsd_integer('#skF_16'),
inference(splitLeft,[status(thm)],[c_2694]) ).
tff(c_2917,plain,
! [X_683] :
( xsd_string(X_683)
| xsd_integer(X_683) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_1665,plain,
( ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ xsd_string('#skF_16')
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_475]) ).
tff(c_2689,plain,
( ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ xsd_string('#skF_16')
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_2680,c_1665]) ).
tff(c_2690,plain,
~ xsd_string('#skF_16'),
inference(splitLeft,[status(thm)],[c_2689]) ).
tff(c_2923,plain,
xsd_integer('#skF_16'),
inference(resolution,[status(thm)],[c_2917,c_2690]) ).
tff(c_2928,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2695,c_2923]) ).
tff(c_2930,plain,
xsd_integer('#skF_16'),
inference(splitRight,[status(thm)],[c_2694]) ).
tff(c_458,plain,
( ~ xsd_integer('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(cnfTransformation,[status(thm)],[f_675]) ).
tff(c_462,plain,
( ~ xsd_integer('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15')
| cowlNothing('#skF_14') ),
inference(demodulation,[status(thm),theory(equality)],[c_430,c_458]) ).
tff(c_469,plain,
( ~ xsd_integer('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing('#skF_15') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_462]) ).
tff(c_477,plain,
( ~ xsd_integer('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cC94(iV822576) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_469]) ).
tff(c_2682,plain,
( ~ xsd_integer('#skF_16')
| xsd_string('#skF_17')
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576) ),
inference(demodulation,[status(thm),theory(equality)],[c_1666,c_477]) ).
tff(c_2683,plain,
~ cC58(iV822576),
inference(splitLeft,[status(thm)],[c_2682]) ).
tff(c_2685,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2680,c_2683]) ).
tff(c_2686,plain,
( ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ xsd_integer('#skF_16')
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_2682]) ).
tff(c_2934,plain,
( ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| xsd_string('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_2930,c_2686]) ).
tff(c_2935,plain,
~ cC80(iV822576),
inference(splitLeft,[status(thm)],[c_2934]) ).
tff(c_4474,plain,
( cC76(iV822576)
| cC78(iV822576) ),
inference(resolution,[status(thm)],[c_4462,c_2935]) ).
tff(c_4481,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_446,c_442,c_4474]) ).
tff(c_4483,plain,
cC80(iV822576),
inference(splitRight,[status(thm)],[c_2934]) ).
tff(c_2929,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_2694]) ).
tff(c_4493,plain,
( ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_4483,c_2929]) ).
tff(c_4494,plain,
~ cC116(iV822576),
inference(splitLeft,[status(thm)],[c_4493]) ).
tff(c_5251,plain,
! [X_1137] :
( cC116(X_1137)
| ~ cC80(X_1137)
| ~ cC114(X_1137) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_5257,plain,
( cC116(iV822576)
| ~ cC114(iV822576) ),
inference(resolution,[status(thm)],[c_4483,c_5251]) ).
tff(c_5261,plain,
~ cC114(iV822576),
inference(negUnitSimplification,[status(thm)],[c_4494,c_5257]) ).
tff(c_5604,plain,
! [X_1172] :
( cC114(X_1172)
| cC112(X_1172)
| cC96(X_1172) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_422,plain,
~ cC96(iV822576),
inference(cnfTransformation,[status(thm)],[f_588]) ).
tff(c_5616,plain,
( cC114(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[c_5604,c_422]) ).
tff(c_5623,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_444,c_5261,c_5616]) ).
tff(c_5625,plain,
cC116(iV822576),
inference(splitRight,[status(thm)],[c_4493]) ).
tff(c_6866,plain,
! [X_1410] :
( cC136(X_1410)
| cC134(X_1410)
| ~ cC116(X_1410) ),
inference(cnfTransformation,[status(thm)],[f_196]) ).
tff(c_4482,plain,
( ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_2934]) ).
tff(c_5629,plain,
( ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| xsd_string('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_5625,c_4482]) ).
tff(c_5630,plain,
~ cC56(iV822576),
inference(splitLeft,[status(thm)],[c_5629]) ).
tff(c_5650,plain,
! [X_1188] :
( cC56(X_1188)
| ~ cC58(X_1188) ),
inference(cnfTransformation,[status(thm)],[f_379]) ).
tff(c_5653,plain,
cC56(iV822576),
inference(resolution,[status(thm)],[c_2680,c_5650]) ).
tff(c_5657,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5630,c_5653]) ).
tff(c_5659,plain,
cC56(iV822576),
inference(splitRight,[status(thm)],[c_5629]) ).
tff(c_5624,plain,
( ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_4493]) ).
tff(c_5666,plain,
( ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_5659,c_5624]) ).
tff(c_5667,plain,
~ cC136(iV822576),
inference(splitLeft,[status(thm)],[c_5666]) ).
tff(c_6878,plain,
( cC134(iV822576)
| ~ cC116(iV822576) ),
inference(resolution,[status(thm)],[c_6866,c_5667]) ).
tff(c_6884,plain,
cC134(iV822576),
inference(demodulation,[status(thm),theory(equality)],[c_5625,c_6878]) ).
tff(c_6886,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_412,c_6884]) ).
tff(c_6888,plain,
cC136(iV822576),
inference(splitRight,[status(thm)],[c_5666]) ).
tff(c_5658,plain,
( ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_5629]) ).
tff(c_6891,plain,
( ~ cC110(iV822576)
| ~ cC114(iV822576)
| xsd_string('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_6888,c_5658]) ).
tff(c_6892,plain,
~ cC114(iV822576),
inference(splitLeft,[status(thm)],[c_6891]) ).
tff(c_6899,plain,
! [X_1418] :
( cC114(X_1418)
| ~ cC116(X_1418) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_6902,plain,
cC114(iV822576),
inference(resolution,[status(thm)],[c_5625,c_6899]) ).
tff(c_6906,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6892,c_6902]) ).
tff(c_6908,plain,
cC114(iV822576),
inference(splitRight,[status(thm)],[c_6891]) ).
tff(c_6887,plain,
( ~ cC114(iV822576)
| ~ cC110(iV822576)
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_5666]) ).
tff(c_6910,plain,
( ~ cC110(iV822576)
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_6908,c_6887]) ).
tff(c_6911,plain,
~ cC110(iV822576),
inference(splitLeft,[status(thm)],[c_6910]) ).
tff(c_8122,plain,
! [X_1646] :
( cC112(X_1646)
| ~ cC4(X_1646)
| cC110(X_1646) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_8152,plain,
( cC112(iV822576)
| cC110(iV822576) ),
inference(resolution,[status(thm)],[c_420,c_8122]) ).
tff(c_8165,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6911,c_444,c_8152]) ).
tff(c_8166,plain,
xsd_integer('#skF_17'),
inference(splitRight,[status(thm)],[c_6910]) ).
tff(c_8167,plain,
cC110(iV822576),
inference(splitRight,[status(thm)],[c_6910]) ).
tff(c_6907,plain,
( ~ cC110(iV822576)
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_6891]) ).
tff(c_8173,plain,
xsd_string('#skF_17'),
inference(demodulation,[status(thm),theory(equality)],[c_8167,c_6907]) ).
tff(c_8195,plain,
! [X_1658] :
( ~ xsd_integer(X_1658)
| ~ xsd_string(X_1658) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_8198,plain,
~ xsd_integer('#skF_17'),
inference(resolution,[status(thm)],[c_8173,c_8195]) ).
tff(c_8202,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8166,c_8198]) ).
tff(c_8204,plain,
xsd_string('#skF_16'),
inference(splitRight,[status(thm)],[c_2689]) ).
tff(c_2679,plain,
( ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ xsd_string('#skF_16')
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_1677]) ).
tff(c_8221,plain,
( ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| xsd_string('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_8204,c_2679]) ).
tff(c_8222,plain,
~ cC80(iV822576),
inference(splitLeft,[status(thm)],[c_8221]) ).
tff(c_9425,plain,
( cC76(iV822576)
| cC78(iV822576) ),
inference(resolution,[status(thm)],[c_9413,c_8222]) ).
tff(c_9432,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_446,c_442,c_9425]) ).
tff(c_9434,plain,
cC80(iV822576),
inference(splitRight,[status(thm)],[c_8221]) ).
tff(c_8203,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_2689]) ).
tff(c_9452,plain,
( ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_9434,c_8203]) ).
tff(c_9453,plain,
~ cC116(iV822576),
inference(splitLeft,[status(thm)],[c_9452]) ).
tff(c_9885,plain,
! [X_2054] :
( cC116(X_2054)
| ~ cC80(X_2054)
| ~ cC114(X_2054) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_9891,plain,
( cC116(iV822576)
| ~ cC114(iV822576) ),
inference(resolution,[status(thm)],[c_9434,c_9885]) ).
tff(c_9895,plain,
~ cC114(iV822576),
inference(negUnitSimplification,[status(thm)],[c_9453,c_9891]) ).
tff(c_10417,plain,
! [X_2126] :
( cC114(X_2126)
| cC112(X_2126)
| cC96(X_2126) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_10429,plain,
( cC114(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[c_10417,c_422]) ).
tff(c_10436,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_444,c_9895,c_10429]) ).
tff(c_10438,plain,
cC116(iV822576),
inference(splitRight,[status(thm)],[c_9452]) ).
tff(c_11305,plain,
! [X_2327] :
( cC136(X_2327)
| cC134(X_2327)
| ~ cC116(X_2327) ),
inference(cnfTransformation,[status(thm)],[f_196]) ).
tff(c_62,plain,
! [X_17] :
( cC114(X_17)
| ~ cC116(X_17) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_10442,plain,
cC114(iV822576),
inference(resolution,[status(thm)],[c_10438,c_62]) ).
tff(c_9433,plain,
( ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_8221]) ).
tff(c_10463,plain,
( ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| xsd_string('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_10438,c_10442,c_9433]) ).
tff(c_10464,plain,
~ cC56(iV822576),
inference(splitLeft,[status(thm)],[c_10463]) ).
tff(c_10468,plain,
! [X_2137] :
( cC56(X_2137)
| ~ cC58(X_2137) ),
inference(cnfTransformation,[status(thm)],[f_379]) ).
tff(c_10471,plain,
cC56(iV822576),
inference(resolution,[status(thm)],[c_2680,c_10468]) ).
tff(c_10475,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10464,c_10471]) ).
tff(c_10477,plain,
cC56(iV822576),
inference(splitRight,[status(thm)],[c_10463]) ).
tff(c_10437,plain,
( ~ cC56(iV822576)
| ~ cC110(iV822576)
| ~ cC114(iV822576)
| ~ cC136(iV822576)
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_9452]) ).
tff(c_10489,plain,
( ~ cC110(iV822576)
| ~ cC136(iV822576)
| xsd_integer('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_10442,c_10477,c_10437]) ).
tff(c_10490,plain,
~ cC136(iV822576),
inference(splitLeft,[status(thm)],[c_10489]) ).
tff(c_11317,plain,
( cC134(iV822576)
| ~ cC116(iV822576) ),
inference(resolution,[status(thm)],[c_11305,c_10490]) ).
tff(c_11323,plain,
cC134(iV822576),
inference(demodulation,[status(thm),theory(equality)],[c_10438,c_11317]) ).
tff(c_11325,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_412,c_11323]) ).
tff(c_11327,plain,
cC136(iV822576),
inference(splitRight,[status(thm)],[c_10489]) ).
tff(c_10476,plain,
( ~ cC110(iV822576)
| ~ cC136(iV822576)
| xsd_string('#skF_17') ),
inference(splitRight,[status(thm)],[c_10463]) ).
tff(c_11339,plain,
( ~ cC110(iV822576)
| xsd_string('#skF_17') ),
inference(demodulation,[status(thm),theory(equality)],[c_11327,c_10476]) ).
tff(c_11340,plain,
~ cC110(iV822576),
inference(splitLeft,[status(thm)],[c_11339]) ).
tff(c_12198,plain,
! [X_2520] :
( cC112(X_2520)
| ~ cC4(X_2520)
| cC110(X_2520) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_12234,plain,
( cC112(iV822576)
| cC110(iV822576) ),
inference(resolution,[status(thm)],[c_420,c_12198]) ).
tff(c_12249,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11340,c_444,c_12234]) ).
tff(c_12251,plain,
cC110(iV822576),
inference(splitRight,[status(thm)],[c_11339]) ).
tff(c_11326,plain,
( ~ cC110(iV822576)
| xsd_integer('#skF_17') ),
inference(splitRight,[status(thm)],[c_10489]) ).
tff(c_12286,plain,
xsd_integer('#skF_17'),
inference(demodulation,[status(thm),theory(equality)],[c_12251,c_11326]) ).
tff(c_12250,plain,
xsd_string('#skF_17'),
inference(splitRight,[status(thm)],[c_11339]) ).
tff(c_12370,plain,
! [X_2563] :
( ~ xsd_integer(X_2563)
| ~ xsd_string(X_2563) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_12373,plain,
~ xsd_integer('#skF_17'),
inference(resolution,[status(thm)],[c_12250,c_12370]) ).
tff(c_12380,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12286,c_12373]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS146+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n002.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 03:01:02 EDT 2025
% 0.14/0.34 % CPUTime :
% 12.79/4.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.79/4.38
% 12.79/4.38 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------