%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS155+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 : n008.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:48 PM UTC 2025
% Result : Theorem 33.95s 21.00s
% Output : CNFRefutation 34.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 33
% Syntax : Number of formulae : 244 ( 126 unt; 0 typ; 0 def)
% Number of atoms : 926 ( 0 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 1340 ( 658 ~; 638 |; 30 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 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 : 103 ( 102 usr; 1 prp; 0-2 aty)
% Number of functors : 93 ( 93 usr; 14 con; 0-1 aty)
% Number of variables : 65 ( 56 !; 9 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ ra_Px9 > ra_Px8 > ra_Px7 > ra_Px6 > ra_Px5 > ra_Px34 > ra_Px33 > ra_Px32 > ra_Px31 > ra_Px30 > ra_Px3 > ra_Px29 > ra_Px28 > ra_Px25 > ra_Px23 > ra_Px20 > ra_Px2 > ra_Px18 > ra_Px17 > ra_Px14 > ra_Px13 > ra_Px12 > ra_Px10 > ra_Px1 > rR1 > xsd_string > xsd_integer > cowlThing > cowlNothing > cTOP > cTEST > cC94xcomp > cC94 > cC92xcomp > cC92 > cC90 > cC88 > cC86 > cC84xcomp > cC84 > cC82xcomp > cC82 > cC80 > cC8 > cC78xcomp > cC78 > cC76 > cC74xcomp > cC74 > cC72xcomp > cC72 > cC70 > cC6xcomp > cC68 > cC66 > cC64 > cC62xcomp > cC62 > cC60 > cC6 > cC58 > cC56 > cC54xcomp > cC54 > cC52xcomp > cC52 > cC50xcomp > cC50 > cC48xcomp > cC48 > cC46 > cC44xcomp > cC44 > cC42xcomp > cC42 > cC40 > cC4 > cC38 > cC36xcomp > cC36 > cC34xcomp > cC34 > cC32xcomp > cC32 > cC30 > cC2xcomp > cC28xcomp > cC28 > cC26xcomp > cC26 > cC24 > cC22 > cC20xcomp > cC20 > cC2 > cC18 > cC16xcomp > cC16 > cC14xcomp > cC14 > cC12 > cC10 > #nlpp > iV8476 > iV8475 > iV8474 > iV8473 > iV8472 > iV8471 > iV8470 > iV8469 > iV8468 > iV8467 > #skF_53 > #skF_9 > #skF_36 > #skF_25 > #skF_7 > #skF_5 > #skF_44 > #skF_21 > #skF_16 > #skF_61 > #skF_2 > #skF_4 > #skF_18 > #skF_24 > #skF_66 > #skF_35 > #skF_19 > #skF_1 > #skF_31 > #skF_75 > #skF_62 > #skF_73 > #skF_79 > #skF_22 > #skF_37 > #skF_80 > #skF_72 > #skF_40 > #skF_8 > #skF_69 > #skF_68 > #skF_52 > #skF_64 > #skF_34 > #skF_58 > #skF_29 > #skF_15 > #skF_32 > #skF_81 > #skF_56 > #skF_60 > #skF_28 > #skF_71 > #skF_10 > #skF_41 > #skF_38 > #skF_43 > #skF_82 > #skF_57 > #skF_74 > #skF_39 > #skF_23 > #skF_59 > #skF_33 > #skF_26 > #skF_13 > #skF_67 > #skF_78 > #skF_77 > #skF_17 > #skF_3 > #skF_54 > #skF_11 > #skF_14 > #skF_48 > #skF_27 > #skF_83 > #skF_12 > #skF_49 > #skF_46 > #skF_42 > #skF_50 > #skF_45 > #skF_55 > #skF_30 > #skF_6 > #skF_65 > #skF_70 > #skF_63 > #skF_20 > #skF_76 > #skF_51 > #skF_47
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(cC34xcomp,type,
cC34xcomp: $i > $o ).
tff('#skF_53',type,
'#skF_53': $i > $i ).
tff(cC20xcomp,type,
cC20xcomp: $i > $o ).
tff(ra_Px28,type,
ra_Px28: ( $i * $i ) > $o ).
tff(cC94,type,
cC94: $i > $o ).
tff(cC8,type,
cC8: $i > $o ).
tff(cC70,type,
cC70: $i > $o ).
tff(cTOP,type,
cTOP: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff('#skF_36',type,
'#skF_36': $i > $i ).
tff('#skF_25',type,
'#skF_25': $i > $i ).
tff(ra_Px17,type,
ra_Px17: ( $i * $i ) > $o ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(cC82xcomp,type,
cC82xcomp: $i > $o ).
tff(ra_Px5,type,
ra_Px5: ( $i * $i ) > $o ).
tff('#skF_44',type,
'#skF_44': $i > $i ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff(cC14,type,
cC14: $i > $o ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(cC48xcomp,type,
cC48xcomp: $i > $o ).
tff('#skF_61',type,
'#skF_61': $i > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(ra_Px20,type,
ra_Px20: ( $i * $i ) > $o ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff(ra_Px2,type,
ra_Px2: ( $i * $i ) > $o ).
tff(cC88,type,
cC88: $i > $o ).
tff(ra_Px30,type,
ra_Px30: ( $i * $i ) > $o ).
tff(cC28xcomp,type,
cC28xcomp: $i > $o ).
tff(cC22,type,
cC22: $i > $o ).
tff('#skF_24',type,
'#skF_24': $i > $i ).
tff('#skF_66',type,
'#skF_66': $i > $i ).
tff(cowlThing,type,
cowlThing: $i > $o ).
tff(cC34,type,
cC34: $i > $o ).
tff('#skF_35',type,
'#skF_35': $i > $i ).
tff(cC2,type,
cC2: $i > $o ).
tff('#skF_19',type,
'#skF_19': $i > $i ).
tff(cC92xcomp,type,
cC92xcomp: $i > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff('#skF_31',type,
'#skF_31': $i > $i ).
tff('#skF_75',type,
'#skF_75': $i > $i ).
tff(ra_Px8,type,
ra_Px8: ( $i * $i ) > $o ).
tff(cC52,type,
cC52: $i > $o ).
tff('#skF_62',type,
'#skF_62': $i > $i ).
tff('#skF_73',type,
'#skF_73': $i > $i ).
tff('#skF_79',type,
'#skF_79': $i > $i ).
tff('#skF_22',type,
'#skF_22': $i > $i ).
tff(cC16,type,
cC16: $i > $o ).
tff(cC78,type,
cC78: $i > $o ).
tff('#skF_37',type,
'#skF_37': $i > $i ).
tff('#skF_80',type,
'#skF_80': $i ).
tff(cC10,type,
cC10: $i > $o ).
tff('#skF_72',type,
'#skF_72': $i > $i ).
tff(cC62xcomp,type,
cC62xcomp: $i > $o ).
tff(iV8476,type,
iV8476: $i ).
tff('#skF_40',type,
'#skF_40': $i > $i ).
tff(cC42xcomp,type,
cC42xcomp: $i > $o ).
tff(ra_Px6,type,
ra_Px6: ( $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(ra_Px14,type,
ra_Px14: ( $i * $i ) > $o ).
tff(cC74xcomp,type,
cC74xcomp: $i > $o ).
tff(cC82,type,
cC82: $i > $o ).
tff(cC72,type,
cC72: $i > $o ).
tff(cC56,type,
cC56: $i > $o ).
tff(cC50xcomp,type,
cC50xcomp: $i > $o ).
tff(cTEST,type,
cTEST: $i > $o ).
tff('#skF_69',type,
'#skF_69': $i > $i ).
tff('#skF_68',type,
'#skF_68': $i > $i ).
tff(cC58,type,
cC58: $i > $o ).
tff('#skF_52',type,
'#skF_52': $i > $i ).
tff(iV8474,type,
iV8474: $i ).
tff(cC12,type,
cC12: $i > $o ).
tff('#skF_64',type,
'#skF_64': $i > $i ).
tff(ra_Px31,type,
ra_Px31: ( $i * $i ) > $o ).
tff(iV8468,type,
iV8468: $i ).
tff(cC46,type,
cC46: $i > $o ).
tff('#skF_34',type,
'#skF_34': $i > $i ).
tff('#skF_58',type,
'#skF_58': $i > $i ).
tff('#skF_29',type,
'#skF_29': $i > $i ).
tff(cC84,type,
cC84: $i > $o ).
tff('#skF_15',type,
'#skF_15': $i > $i ).
tff(xsd_integer,type,
xsd_integer: $i > $o ).
tff('#skF_32',type,
'#skF_32': $i > $i ).
tff(cC64,type,
cC64: $i > $o ).
tff(cC48,type,
cC48: $i > $o ).
tff('#skF_81',type,
'#skF_81': $i ).
tff('#skF_56',type,
'#skF_56': $i > $i ).
tff(cC38,type,
cC38: $i > $o ).
tff('#skF_60',type,
'#skF_60': $i > $i ).
tff(cC6,type,
cC6: $i > $o ).
tff(cC18,type,
cC18: $i > $o ).
tff('#skF_28',type,
'#skF_28': $i > $i ).
tff('#skF_71',type,
'#skF_71': $i > $i ).
tff(ra_Px23,type,
ra_Px23: ( $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(cC6xcomp,type,
cC6xcomp: $i > $o ).
tff('#skF_41',type,
'#skF_41': $i > $i ).
tff(ra_Px7,type,
ra_Px7: ( $i * $i ) > $o ).
tff(cC36xcomp,type,
cC36xcomp: $i > $o ).
tff('#skF_38',type,
'#skF_38': $i > $i ).
tff('#skF_43',type,
'#skF_43': $i > $i ).
tff(ra_Px9,type,
ra_Px9: ( $i * $i ) > $o ).
tff('#skF_82',type,
'#skF_82': $i ).
tff(cC42,type,
cC42: $i > $o ).
tff(cC78xcomp,type,
cC78xcomp: $i > $o ).
tff(ra_Px34,type,
ra_Px34: ( $i * $i ) > $o ).
tff(cC60,type,
cC60: $i > $o ).
tff(iV8469,type,
iV8469: $i ).
tff(cC92,type,
cC92: $i > $o ).
tff(ra_Px33,type,
ra_Px33: ( $i * $i ) > $o ).
tff('#skF_57',type,
'#skF_57': $i > $i ).
tff(ra_Px1,type,
ra_Px1: ( $i * $i ) > $o ).
tff(ra_Px12,type,
ra_Px12: ( $i * $i ) > $o ).
tff(iV8471,type,
iV8471: $i ).
tff(cC68,type,
cC68: $i > $o ).
tff('#skF_74',type,
'#skF_74': $i > $i ).
tff(ra_Px13,type,
ra_Px13: ( $i * $i ) > $o ).
tff(cC16xcomp,type,
cC16xcomp: $i > $o ).
tff(ra_Px32,type,
ra_Px32: ( $i * $i ) > $o ).
tff('#skF_39',type,
'#skF_39': $i > $i ).
tff(cC62,type,
cC62: $i > $o ).
tff(cC80,type,
cC80: $i > $o ).
tff('#skF_23',type,
'#skF_23': $i > $i ).
tff('#skF_59',type,
'#skF_59': $i > $i ).
tff(cC40,type,
cC40: $i > $o ).
tff(cC14xcomp,type,
cC14xcomp: $i > $o ).
tff(cC72xcomp,type,
cC72xcomp: $i > $o ).
tff('#skF_33',type,
'#skF_33': $i > $i ).
tff(cC54,type,
cC54: $i > $o ).
tff('#skF_26',type,
'#skF_26': $i > $i ).
tff(rR1,type,
rR1: ( $i * $i ) > $o ).
tff(cC76,type,
cC76: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(iV8473,type,
iV8473: $i ).
tff('#skF_67',type,
'#skF_67': $i > $i ).
tff('#skF_78',type,
'#skF_78': $i > $i ).
tff(iV8470,type,
iV8470: $i ).
tff(iV8467,type,
iV8467: $i ).
tff('#skF_77',type,
'#skF_77': $i > $i ).
tff(cC28,type,
cC28: $i > $o ).
tff(cC2xcomp,type,
cC2xcomp: $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_17',type,
'#skF_17': $i > $i ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_54',type,
'#skF_54': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(cC36,type,
cC36: $i > $o ).
tff(cC44xcomp,type,
cC44xcomp: $i > $o ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff(cC44,type,
cC44: $i > $o ).
tff(ra_Px25,type,
ra_Px25: ( $i * $i ) > $o ).
tff(ra_Px29,type,
ra_Px29: ( $i * $i ) > $o ).
tff(cC66,type,
cC66: $i > $o ).
tff('#skF_48',type,
'#skF_48': $i > $i ).
tff(cC4,type,
cC4: $i > $o ).
tff(cC32xcomp,type,
cC32xcomp: $i > $o ).
tff(cC94xcomp,type,
cC94xcomp: $i > $o ).
tff('#skF_27',type,
'#skF_27': $i > $i ).
tff(cC20,type,
cC20: $i > $o ).
tff('#skF_83',type,
'#skF_83': $i ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff(ra_Px10,type,
ra_Px10: ( $i * $i ) > $o ).
tff(iV8475,type,
iV8475: $i ).
tff('#skF_49',type,
'#skF_49': $i > $i ).
tff(ra_Px18,type,
ra_Px18: ( $i * $i ) > $o ).
tff(cC26xcomp,type,
cC26xcomp: $i > $o ).
tff('#skF_46',type,
'#skF_46': $i > $i ).
tff('#skF_42',type,
'#skF_42': $i > $i ).
tff(cC30,type,
cC30: $i > $o ).
tff(ra_Px3,type,
ra_Px3: ( $i * $i ) > $o ).
tff(cC90,type,
cC90: $i > $o ).
tff('#skF_50',type,
'#skF_50': $i > $i ).
tff(cC24,type,
cC24: $i > $o ).
tff('#skF_45',type,
'#skF_45': $i > $i ).
tff('#skF_55',type,
'#skF_55': $i > $i ).
tff(cC26,type,
cC26: $i > $o ).
tff('#skF_30',type,
'#skF_30': $i > $i ).
tff(cC52xcomp,type,
cC52xcomp: $i > $o ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(cowlNothing,type,
cowlNothing: $i > $o ).
tff('#skF_65',type,
'#skF_65': $i > $i ).
tff(cC54xcomp,type,
cC54xcomp: $i > $o ).
tff('#skF_70',type,
'#skF_70': $i > $i ).
tff('#skF_63',type,
'#skF_63': $i > $i ).
tff(iV8472,type,
iV8472: $i ).
tff('#skF_20',type,
'#skF_20': $i > $i ).
tff('#skF_76',type,
'#skF_76': $i > $i ).
tff('#skF_51',type,
'#skF_51': $i > $i ).
tff('#skF_47',type,
'#skF_47': $i > $i ).
tff(cC84xcomp,type,
cC84xcomp: $i > $o ).
tff(f_750,axiom,
cC78xcomp(iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_118) ).
tff(f_752,axiom,
cC2xcomp(iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_119) ).
tff(f_598,axiom,
! [X] :
( cC80(X)
<=> ( cC78xcomp(X)
& cC2xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_80) ).
tff(f_761,axiom,
cC2xcomp(iV8472),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_122) ).
tff(f_462,axiom,
! [X] :
( cC60(X)
<=> ( cC2xcomp(X)
& cC58(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_61) ).
tff(f_33,axiom,
! [X] :
( cowlThing(X)
& ~ cowlNothing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
tff(f_723,axiom,
cowlThing(iV8467),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_102) ).
tff(f_754,axiom,
cowlThing(iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_120) ).
tff(f_763,axiom,
cowlThing(iV8472),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_123) ).
tff(f_844,negated_conjecture,
~ ( ! [X] :
( cowlThing(X)
& ~ cowlNothing(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
tff(f_724,axiom,
rR1(iV8467,iV8471),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_103) ).
tff(f_124,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( rR1(X,Y)
& cC2xcomp(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
tff(f_280,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( rR1(X,Y)
& cC2xcomp(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_35) ).
tff(f_737,axiom,
cC6xcomp(iV8469),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_113) ).
tff(f_726,axiom,
rR1(iV8467,iV8469),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_105) ).
tff(f_591,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( rR1(X,Y)
& cC6xcomp(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_79) ).
tff(f_613,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( rR1(X,Y)
& cC80(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_82) ).
tff(f_39,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
tff(f_783,axiom,
cC2(iV8476),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_132) ).
tff(f_764,axiom,
rR1(iV8472,iV8476),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_124) ).
tff(f_434,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( rR1(X,Y)
& cC2(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_57) ).
tff(f_731,axiom,
rR1(iV8467,iV8472),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_110) ).
tff(f_470,axiom,
! [X] :
( cC62(X)
<=> ? [Y] :
( rR1(X,Y)
& cC60(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_62) ).
tff(f_746,axiom,
cTOP(iV8470),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_116) ).
tff(f_725,axiom,
rR1(iV8467,iV8470),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_104) ).
tff(f_69,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( rR1(X,Y)
& cTOP(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
tff(f_779,axiom,
cC2xcomp(iV8475),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_130) ).
tff(f_730,axiom,
rR1(iV8467,iV8475),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_109) ).
tff(f_344,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( rR1(X,Y)
& cC2xcomp(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
tff(f_770,axiom,
cC32xcomp(iV8474),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_127) ).
tff(f_727,axiom,
rR1(iV8467,iV8474),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_106) ).
tff(f_236,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( rR1(X,Y)
& cC32xcomp(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
tff(f_46,axiom,
! [X] :
( cC10(X)
<=> ( cC4(X)
& cC8(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
tff(c_526,plain,
cC78xcomp(iV8471),
inference(cnfTransformation,[status(thm)],[f_750]) ).
tff(c_528,plain,
cC2xcomp(iV8471),
inference(cnfTransformation,[status(thm)],[f_752]) ).
tff(c_62305,plain,
! [X_5259] :
( cC80(X_5259)
| ~ cC2xcomp(X_5259)
| ~ cC78xcomp(X_5259) ),
inference(cnfTransformation,[status(thm)],[f_598]) ).
tff(c_534,plain,
cC2xcomp(iV8472),
inference(cnfTransformation,[status(thm)],[f_761]) ).
tff(c_48833,plain,
! [X_4118] :
( cC60(X_4118)
| ~ cC58(X_4118)
| ~ cC2xcomp(X_4118) ),
inference(cnfTransformation,[status(thm)],[f_462]) ).
tff(c_38877,plain,
! [X_3153] :
( cC80(X_3153)
| ~ cC2xcomp(X_3153)
| ~ cC78xcomp(X_3153) ),
inference(cnfTransformation,[status(thm)],[f_598]) ).
tff(c_24423,plain,
! [X_2233] :
( cC60(X_2233)
| ~ cC58(X_2233)
| ~ cC2xcomp(X_2233) ),
inference(cnfTransformation,[status(thm)],[f_462]) ).
tff(c_398,plain,
! [X_279] :
( cC80(X_279)
| ~ cC2xcomp(X_279)
| ~ cC78xcomp(X_279) ),
inference(cnfTransformation,[status(thm)],[f_598]) ).
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_494,plain,
cowlThing(iV8467),
inference(cnfTransformation,[status(thm)],[f_723]) ).
tff(c_530,plain,
cowlThing(iV8471),
inference(cnfTransformation,[status(thm)],[f_754]) ).
tff(c_536,plain,
cowlThing(iV8472),
inference(cnfTransformation,[status(thm)],[f_763]) ).
tff(c_564,plain,
( ~ xsd_integer('#skF_82')
| xsd_string('#skF_83')
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_568,plain,
( ~ xsd_integer('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_536,c_564]) ).
tff(c_576,plain,
( ~ xsd_integer('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_530,c_568]) ).
tff(c_586,plain,
( ~ xsd_integer('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_494,c_576]) ).
tff(c_592,plain,
( ~ xsd_integer('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_586]) ).
tff(c_610,plain,
( ~ xsd_integer('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_592]) ).
tff(c_613,plain,
~ cC20(iV8467),
inference(splitLeft,[status(thm)],[c_610]) ).
tff(c_496,plain,
rR1(iV8467,iV8471),
inference(cnfTransformation,[status(thm)],[f_724]) ).
tff(c_6890,plain,
! [X_741,Y_742] :
( cC20(X_741)
| ~ cC2xcomp(Y_742)
| ~ rR1(X_741,Y_742) ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_6995,plain,
( cC20(iV8467)
| ~ cC2xcomp(iV8471) ),
inference(resolution,[status(thm)],[c_496,c_6890]) ).
tff(c_7051,plain,
cC20(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_528,c_6995]) ).
tff(c_7053,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_613,c_7051]) ).
tff(c_7055,plain,
cC20(iV8467),
inference(splitRight,[status(thm)],[c_610]) ).
tff(c_562,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_570,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_536,c_562]) ).
tff(c_578,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_530,c_570]) ).
tff(c_588,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_494,c_578]) ).
tff(c_589,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_588]) ).
tff(c_604,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_589]) ).
tff(c_7057,plain,
( ~ xsd_string('#skF_82')
| xsd_string('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_7055,c_604]) ).
tff(c_7058,plain,
~ cC4(iV8467),
inference(splitLeft,[status(thm)],[c_7057]) ).
tff(c_13230,plain,
! [X_1143,Y_1144] :
( cC4(X_1143)
| ~ cC2xcomp(Y_1144)
| ~ rR1(X_1143,Y_1144) ),
inference(cnfTransformation,[status(thm)],[f_280]) ).
tff(c_13329,plain,
( cC4(iV8467)
| ~ cC2xcomp(iV8471) ),
inference(resolution,[status(thm)],[c_496,c_13230]) ).
tff(c_13387,plain,
cC4(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_528,c_13329]) ).
tff(c_13389,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7058,c_13387]) ).
tff(c_13391,plain,
cC4(iV8467),
inference(splitRight,[status(thm)],[c_7057]) ).
tff(c_560,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_572,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_536,c_560]) ).
tff(c_580,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_530,c_572]) ).
tff(c_582,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_494,c_580]) ).
tff(c_590,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_582]) ).
tff(c_606,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_590]) ).
tff(c_13393,plain,
( ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_7055,c_13391,c_606]) ).
tff(c_13394,plain,
~ cC8(iV8467),
inference(splitLeft,[status(thm)],[c_13393]) ).
tff(c_516,plain,
cC6xcomp(iV8469),
inference(cnfTransformation,[status(thm)],[f_737]) ).
tff(c_500,plain,
rR1(iV8467,iV8469),
inference(cnfTransformation,[status(thm)],[f_726]) ).
tff(c_20257,plain,
! [X_1552,Y_1553] :
( cC8(X_1552)
| ~ cC6xcomp(Y_1553)
| ~ rR1(X_1552,Y_1553) ),
inference(cnfTransformation,[status(thm)],[f_591]) ).
tff(c_20368,plain,
( cC8(iV8467)
| ~ cC6xcomp(iV8469) ),
inference(resolution,[status(thm)],[c_500,c_20257]) ).
tff(c_20424,plain,
cC8(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_516,c_20368]) ).
tff(c_20426,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13394,c_20424]) ).
tff(c_20428,plain,
cC8(iV8467),
inference(splitRight,[status(thm)],[c_13393]) ).
tff(c_558,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(cnfTransformation,[status(thm)],[f_844]) ).
tff(c_566,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_536,c_558]) ).
tff(c_574,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_530,c_566]) ).
tff(c_584,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81')
| cowlNothing('#skF_80') ),
inference(demodulation,[status(thm),theory(equality)],[c_494,c_574]) ).
tff(c_591,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing('#skF_81') ),
inference(negUnitSimplification,[status(thm)],[c_4,c_584]) ).
tff(c_608,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_591]) ).
tff(c_20431,plain,
( ~ xsd_string('#skF_82')
| xsd_integer('#skF_83')
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467) ),
inference(demodulation,[status(thm),theory(equality)],[c_7055,c_13391,c_20428,c_608]) ).
tff(c_20432,plain,
~ cC82(iV8467),
inference(splitLeft,[status(thm)],[c_20431]) ).
tff(c_22675,plain,
! [X_1908,Y_1909] :
( cC82(X_1908)
| ~ cC80(Y_1909)
| ~ rR1(X_1908,Y_1909) ),
inference(cnfTransformation,[status(thm)],[f_613]) ).
tff(c_22783,plain,
( cC82(iV8467)
| ~ cC80(iV8471) ),
inference(resolution,[status(thm)],[c_496,c_22675]) ).
tff(c_22839,plain,
~ cC80(iV8471),
inference(negUnitSimplification,[status(thm)],[c_20432,c_22783]) ).
tff(c_22868,plain,
( ~ cC2xcomp(iV8471)
| ~ cC78xcomp(iV8471) ),
inference(resolution,[status(thm)],[c_398,c_22839]) ).
tff(c_22872,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_526,c_528,c_22868]) ).
tff(c_22874,plain,
cC82(iV8467),
inference(splitRight,[status(thm)],[c_20431]) ).
tff(c_7054,plain,
( ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ xsd_integer('#skF_82')
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_610]) ).
tff(c_22880,plain,
( ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ xsd_integer('#skF_82')
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_22874,c_20428,c_13391,c_7054]) ).
tff(c_22881,plain,
~ xsd_integer('#skF_82'),
inference(splitLeft,[status(thm)],[c_22880]) ).
tff(c_8,plain,
! [X_2] :
( xsd_string(X_2)
| xsd_integer(X_2) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_22873,plain,
( ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ xsd_string('#skF_82')
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_20431]) ).
tff(c_22890,plain,
~ xsd_string('#skF_82'),
inference(splitLeft,[status(thm)],[c_22873]) ).
tff(c_22893,plain,
xsd_integer('#skF_82'),
inference(resolution,[status(thm)],[c_8,c_22890]) ).
tff(c_22897,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22881,c_22893]) ).
tff(c_22899,plain,
xsd_string('#skF_82'),
inference(splitRight,[status(thm)],[c_22873]) ).
tff(c_13390,plain,
( ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ xsd_string('#skF_82')
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_7057]) ).
tff(c_22919,plain,
( ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_22899,c_22874,c_20428,c_13390]) ).
tff(c_22920,plain,
~ cC60(iV8472),
inference(splitLeft,[status(thm)],[c_22919]) ).
tff(c_24426,plain,
( ~ cC58(iV8472)
| ~ cC2xcomp(iV8472) ),
inference(resolution,[status(thm)],[c_24423,c_22920]) ).
tff(c_24435,plain,
~ cC58(iV8472),
inference(demodulation,[status(thm),theory(equality)],[c_534,c_24426]) ).
tff(c_554,plain,
cC2(iV8476),
inference(cnfTransformation,[status(thm)],[f_783]) ).
tff(c_538,plain,
rR1(iV8472,iV8476),
inference(cnfTransformation,[status(thm)],[f_764]) ).
tff(c_26347,plain,
! [X_2277,Y_2278] :
( cC58(X_2277)
| ~ cC2(Y_2278)
| ~ rR1(X_2277,Y_2278) ),
inference(cnfTransformation,[status(thm)],[f_434]) ).
tff(c_26449,plain,
( cC58(iV8472)
| ~ cC2(iV8476) ),
inference(resolution,[status(thm)],[c_538,c_26347]) ).
tff(c_26503,plain,
cC58(iV8472),
inference(demodulation,[status(thm),theory(equality)],[c_554,c_26449]) ).
tff(c_26505,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24435,c_26503]) ).
tff(c_26507,plain,
cC60(iV8472),
inference(splitRight,[status(thm)],[c_22919]) ).
tff(c_302,plain,
! [X_215] :
( cC58(X_215)
| ~ cC60(X_215) ),
inference(cnfTransformation,[status(thm)],[f_462]) ).
tff(c_26514,plain,
cC58(iV8472),
inference(resolution,[status(thm)],[c_26507,c_302]) ).
tff(c_22898,plain,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_22873]) ).
tff(c_26533,plain,
( ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_integer('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_26514,c_26507,c_22898]) ).
tff(c_26534,plain,
~ cC62(iV8467),
inference(splitLeft,[status(thm)],[c_26533]) ).
tff(c_510,plain,
rR1(iV8467,iV8472),
inference(cnfTransformation,[status(thm)],[f_731]) ).
tff(c_33022,plain,
! [X_2653,Y_2654] :
( cC62(X_2653)
| ~ cC60(Y_2654)
| ~ rR1(X_2653,Y_2654) ),
inference(cnfTransformation,[status(thm)],[f_470]) ).
tff(c_33142,plain,
( cC62(iV8467)
| ~ cC60(iV8472) ),
inference(resolution,[status(thm)],[c_510,c_33022]) ).
tff(c_33198,plain,
cC62(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_26507,c_33142]) ).
tff(c_33200,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_26534,c_33198]) ).
tff(c_33202,plain,
cC62(iV8467),
inference(splitRight,[status(thm)],[c_26533]) ).
tff(c_26506,plain,
( ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_22919]) ).
tff(c_33220,plain,
( ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_33202,c_26514,c_26506]) ).
tff(c_33221,plain,
~ cC14(iV8467),
inference(splitLeft,[status(thm)],[c_33220]) ).
tff(c_522,plain,
cTOP(iV8470),
inference(cnfTransformation,[status(thm)],[f_746]) ).
tff(c_498,plain,
rR1(iV8467,iV8470),
inference(cnfTransformation,[status(thm)],[f_725]) ).
tff(c_38495,plain,
! [X_3007,Y_3008] :
( cC14(X_3007)
| ~ cTOP(Y_3008)
| ~ rR1(X_3007,Y_3008) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_38594,plain,
( cC14(iV8467)
| ~ cTOP(iV8470) ),
inference(resolution,[status(thm)],[c_498,c_38495]) ).
tff(c_38652,plain,
cC14(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_522,c_38594]) ).
tff(c_38654,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33221,c_38652]) ).
tff(c_38656,plain,
cC14(iV8467),
inference(splitRight,[status(thm)],[c_33220]) ).
tff(c_33201,plain,
( ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_26533]) ).
tff(c_38674,plain,
( ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| xsd_integer('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_38656,c_33201]) ).
tff(c_38675,plain,
~ cC80(iV8471),
inference(splitLeft,[status(thm)],[c_38674]) ).
tff(c_38880,plain,
( ~ cC2xcomp(iV8471)
| ~ cC78xcomp(iV8471) ),
inference(resolution,[status(thm)],[c_38877,c_38675]) ).
tff(c_38890,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_526,c_528,c_38880]) ).
tff(c_38892,plain,
cC80(iV8471),
inference(splitRight,[status(thm)],[c_38674]) ).
tff(c_38655,plain,
( ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_33220]) ).
tff(c_38906,plain,
( ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_38892,c_38655]) ).
tff(c_38907,plain,
~ cC48(iV8467),
inference(splitLeft,[status(thm)],[c_38906]) ).
tff(c_550,plain,
cC2xcomp(iV8475),
inference(cnfTransformation,[status(thm)],[f_779]) ).
tff(c_508,plain,
rR1(iV8467,iV8475),
inference(cnfTransformation,[status(thm)],[f_730]) ).
tff(c_41936,plain,
! [X_3456,Y_3457] :
( cC48(X_3456)
| ~ cC2xcomp(Y_3457)
| ~ rR1(X_3456,Y_3457) ),
inference(cnfTransformation,[status(thm)],[f_344]) ).
tff(c_42041,plain,
( cC48(iV8467)
| ~ cC2xcomp(iV8475) ),
inference(resolution,[status(thm)],[c_508,c_41936]) ).
tff(c_42097,plain,
cC48(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_550,c_42041]) ).
tff(c_42099,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38907,c_42097]) ).
tff(c_42101,plain,
cC48(iV8467),
inference(splitRight,[status(thm)],[c_38906]) ).
tff(c_38891,plain,
( ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_38674]) ).
tff(c_42105,plain,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_integer('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_42101,c_38891]) ).
tff(c_42106,plain,
~ cC34(iV8467),
inference(splitLeft,[status(thm)],[c_42105]) ).
tff(c_544,plain,
cC32xcomp(iV8474),
inference(cnfTransformation,[status(thm)],[f_770]) ).
tff(c_502,plain,
rR1(iV8467,iV8474),
inference(cnfTransformation,[status(thm)],[f_727]) ).
tff(c_48066,plain,
! [X_3784,Y_3785] :
( cC34(X_3784)
| ~ cC32xcomp(Y_3785)
| ~ rR1(X_3784,Y_3785) ),
inference(cnfTransformation,[status(thm)],[f_236]) ).
tff(c_48162,plain,
( cC34(iV8467)
| ~ cC32xcomp(iV8474) ),
inference(resolution,[status(thm)],[c_502,c_48066]) ).
tff(c_48220,plain,
cC34(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_544,c_48162]) ).
tff(c_48222,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_42106,c_48220]) ).
tff(c_48223,plain,
( ~ cC10(iV8467)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_42105]) ).
tff(c_48225,plain,
~ cC10(iV8467),
inference(splitLeft,[status(thm)],[c_48223]) ).
tff(c_48430,plain,
! [X_3911] :
( cC10(X_3911)
| ~ cC8(X_3911)
| ~ cC4(X_3911) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_48436,plain,
( cC10(iV8467)
| ~ cC4(iV8467) ),
inference(resolution,[status(thm)],[c_20428,c_48430]) ).
tff(c_48440,plain,
cC10(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_13391,c_48436]) ).
tff(c_48442,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48225,c_48440]) ).
tff(c_48443,plain,
xsd_integer('#skF_83'),
inference(splitRight,[status(thm)],[c_48223]) ).
tff(c_48224,plain,
cC34(iV8467),
inference(splitRight,[status(thm)],[c_42105]) ).
tff(c_48444,plain,
cC10(iV8467),
inference(splitRight,[status(thm)],[c_48223]) ).
tff(c_42100,plain,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_38906]) ).
tff(c_48452,plain,
xsd_string('#skF_83'),
inference(demodulation,[status(thm),theory(equality)],[c_48224,c_48444,c_42100]) ).
tff(c_6,plain,
! [X_2] :
( ~ xsd_integer(X_2)
| ~ xsd_string(X_2) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_48455,plain,
~ xsd_integer('#skF_83'),
inference(resolution,[status(thm)],[c_48452,c_6]) ).
tff(c_48459,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_48443,c_48455]) ).
tff(c_48461,plain,
xsd_integer('#skF_82'),
inference(splitRight,[status(thm)],[c_22880]) ).
tff(c_20427,plain,
( ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ xsd_integer('#skF_82')
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_13393]) ).
tff(c_48485,plain,
( ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| xsd_integer('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_48461,c_22874,c_20427]) ).
tff(c_48486,plain,
~ cC60(iV8472),
inference(splitLeft,[status(thm)],[c_48485]) ).
tff(c_48836,plain,
( ~ cC58(iV8472)
| ~ cC2xcomp(iV8472) ),
inference(resolution,[status(thm)],[c_48833,c_48486]) ).
tff(c_48845,plain,
~ cC58(iV8472),
inference(demodulation,[status(thm),theory(equality)],[c_534,c_48836]) ).
tff(c_50355,plain,
! [X_4263,Y_4264] :
( cC58(X_4263)
| ~ cC2(Y_4264)
| ~ rR1(X_4263,Y_4264) ),
inference(cnfTransformation,[status(thm)],[f_434]) ).
tff(c_50457,plain,
( cC58(iV8472)
| ~ cC2(iV8476) ),
inference(resolution,[status(thm)],[c_538,c_50355]) ).
tff(c_50511,plain,
cC58(iV8472),
inference(demodulation,[status(thm),theory(equality)],[c_554,c_50457]) ).
tff(c_50513,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48845,c_50511]) ).
tff(c_50515,plain,
cC60(iV8472),
inference(splitRight,[status(thm)],[c_48485]) ).
tff(c_50522,plain,
cC58(iV8472),
inference(resolution,[status(thm)],[c_50515,c_302]) ).
tff(c_48460,plain,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_22880]) ).
tff(c_50548,plain,
( ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_50522,c_50515,c_48460]) ).
tff(c_50549,plain,
~ cC62(iV8467),
inference(splitLeft,[status(thm)],[c_50548]) ).
tff(c_54494,plain,
! [X_4619,Y_4620] :
( cC62(X_4619)
| ~ cC60(Y_4620)
| ~ rR1(X_4619,Y_4620) ),
inference(cnfTransformation,[status(thm)],[f_470]) ).
tff(c_54614,plain,
( cC62(iV8467)
| ~ cC60(iV8472) ),
inference(resolution,[status(thm)],[c_510,c_54494]) ).
tff(c_54670,plain,
cC62(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_50515,c_54614]) ).
tff(c_54672,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50549,c_54670]) ).
tff(c_54674,plain,
cC62(iV8467),
inference(splitRight,[status(thm)],[c_50548]) ).
tff(c_50514,plain,
( ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_48485]) ).
tff(c_54684,plain,
( ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| xsd_integer('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_54674,c_50522,c_50514]) ).
tff(c_54685,plain,
~ cC14(iV8467),
inference(splitLeft,[status(thm)],[c_54684]) ).
tff(c_60653,plain,
! [X_4979,Y_4980] :
( cC14(X_4979)
| ~ cTOP(Y_4980)
| ~ rR1(X_4979,Y_4980) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_60752,plain,
( cC14(iV8467)
| ~ cTOP(iV8470) ),
inference(resolution,[status(thm)],[c_498,c_60653]) ).
tff(c_60810,plain,
cC14(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_522,c_60752]) ).
tff(c_60812,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_54685,c_60810]) ).
tff(c_60814,plain,
cC14(iV8467),
inference(splitRight,[status(thm)],[c_54684]) ).
tff(c_54673,plain,
( ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_50548]) ).
tff(c_60826,plain,
( ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_60814,c_54673]) ).
tff(c_60827,plain,
~ cC80(iV8471),
inference(splitLeft,[status(thm)],[c_60826]) ).
tff(c_62308,plain,
( ~ cC2xcomp(iV8471)
| ~ cC78xcomp(iV8471) ),
inference(resolution,[status(thm)],[c_62305,c_60827]) ).
tff(c_62318,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_526,c_528,c_62308]) ).
tff(c_62320,plain,
cC80(iV8471),
inference(splitRight,[status(thm)],[c_60826]) ).
tff(c_60813,plain,
( ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| ~ cC80(iV8471)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_54684]) ).
tff(c_62335,plain,
( ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cC48(iV8467)
| xsd_integer('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_62320,c_60813]) ).
tff(c_62336,plain,
~ cC48(iV8467),
inference(splitLeft,[status(thm)],[c_62335]) ).
tff(c_64511,plain,
! [X_5559,Y_5560] :
( cC48(X_5559)
| ~ cC2xcomp(Y_5560)
| ~ rR1(X_5559,Y_5560) ),
inference(cnfTransformation,[status(thm)],[f_344]) ).
tff(c_64616,plain,
( cC48(iV8467)
| ~ cC2xcomp(iV8475) ),
inference(resolution,[status(thm)],[c_508,c_64511]) ).
tff(c_64672,plain,
cC48(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_550,c_64616]) ).
tff(c_64674,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62336,c_64672]) ).
tff(c_64676,plain,
cC48(iV8467),
inference(splitRight,[status(thm)],[c_62335]) ).
tff(c_62319,plain,
( ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_60826]) ).
tff(c_64680,plain,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_string('#skF_83') ),
inference(demodulation,[status(thm),theory(equality)],[c_64676,c_62319]) ).
tff(c_64681,plain,
~ cC34(iV8467),
inference(splitLeft,[status(thm)],[c_64680]) ).
tff(c_71498,plain,
! [X_5909,Y_5910] :
( cC34(X_5909)
| ~ cC32xcomp(Y_5910)
| ~ rR1(X_5909,Y_5910) ),
inference(cnfTransformation,[status(thm)],[f_236]) ).
tff(c_71594,plain,
( cC34(iV8467)
| ~ cC32xcomp(iV8474) ),
inference(resolution,[status(thm)],[c_502,c_71498]) ).
tff(c_71652,plain,
cC34(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_544,c_71594]) ).
tff(c_71654,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64681,c_71652]) ).
tff(c_71655,plain,
( ~ cC10(iV8467)
| xsd_string('#skF_83') ),
inference(splitRight,[status(thm)],[c_64680]) ).
tff(c_71657,plain,
~ cC10(iV8467),
inference(splitLeft,[status(thm)],[c_71655]) ).
tff(c_72050,plain,
! [X_6052] :
( cC10(X_6052)
| ~ cC8(X_6052)
| ~ cC4(X_6052) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_72056,plain,
( cC10(iV8467)
| ~ cC4(iV8467) ),
inference(resolution,[status(thm)],[c_20428,c_72050]) ).
tff(c_72060,plain,
cC10(iV8467),
inference(demodulation,[status(thm),theory(equality)],[c_13391,c_72056]) ).
tff(c_72062,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71657,c_72060]) ).
tff(c_72063,plain,
xsd_string('#skF_83'),
inference(splitRight,[status(thm)],[c_71655]) ).
tff(c_72068,plain,
~ xsd_integer('#skF_83'),
inference(resolution,[status(thm)],[c_72063,c_6]) ).
tff(c_71656,plain,
cC34(iV8467),
inference(splitRight,[status(thm)],[c_64680]) ).
tff(c_72064,plain,
cC10(iV8467),
inference(splitRight,[status(thm)],[c_71655]) ).
tff(c_64675,plain,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_integer('#skF_83') ),
inference(splitRight,[status(thm)],[c_62335]) ).
tff(c_72070,plain,
xsd_integer('#skF_83'),
inference(demodulation,[status(thm),theory(equality)],[c_71656,c_72064,c_64675]) ).
tff(c_72071,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72068,c_72070]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : KRS155+1 : TPTP v9.0.0. Released v3.1.0.
% 0.00/0.10 % 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.09/0.31 % Computer : n008.cluster.edu
% 0.09/0.31 % Model : x86_64 x86_64
% 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.31 % Memory : 8042.1875MB
% 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.31 % CPULimit : 300
% 0.09/0.31 % WCLimit : 300
% 0.09/0.31 % DateTime : Tue Apr 8 03:00:47 EDT 2025
% 0.09/0.31 % CPUTime :
% 33.95/21.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.95/21.04
% 33.95/21.04 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------