%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : DAT052_1 : TPTP v9.0.0. Released v5.0.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 : n005.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 06:08:00 PM UTC 2025
% Result : Theorem 19.44s 6.63s
% Output : CNFRefutation 19.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 10
% Syntax : Number of formulae : 242 ( 161 unt; 0 typ; 0 def)
% Number of atoms : 351 ( 177 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 245 ( 136 ~; 92 |; 7 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 353 ( 42 atm; 155 fun; 156 num; 0 var)
% Number of types : 3 ( 1 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 137 ( 131 usr; 130 con; 0-2 aty)
% Number of variables : 38 ( 38 !; 0 ?; 38 :)
% Comments :
%------------------------------------------------------------------------------
%$ isrecord > #nlpp > split2 > split1 > next > length > data > #skF_1 > #skF_2
%Foreground sorts:
tff(record,type,
record: $tType ).
%Background operators:
tff('#skE_46',type,
'#skE_46': $int ).
tff('#skE_120',type,
'#skE_120': $int ).
tff('#skE_74',type,
'#skE_74': $int ).
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_90',type,
'#skE_90': $int ).
tff('#skE_105',type,
'#skE_105': $int ).
tff('#skE_88',type,
'#skE_88': $int ).
tff('#skE_121',type,
'#skE_121': $int ).
tff('#skE_95',type,
'#skE_95': $int ).
tff('#skE_21',type,
'#skE_21': $int ).
tff('#skE_62',type,
'#skE_62': $int ).
tff('#skE_30',type,
'#skE_30': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_25',type,
'#skE_25': $int ).
tff('#skE_52',type,
'#skE_52': $int ).
tff('#skE_28',type,
'#skE_28': $int ).
tff('#skE_109',type,
'#skE_109': $int ).
tff('#skE_48',type,
'#skE_48': $int ).
tff('#skE_23',type,
'#skE_23': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skE_41',type,
'#skE_41': $int ).
tff('#skE_43',type,
'#skE_43': $int ).
tff('#skE_37',type,
'#skE_37': $int ).
tff('#skE_73',type,
'#skE_73': $int ).
tff('#skE_80',type,
'#skE_80': $int ).
tff('#skE_85',type,
'#skE_85': $int ).
tff('#skE_101',type,
'#skE_101': $int ).
tff('#skE_84',type,
'#skE_84': $int ).
tff('#skE_42',type,
'#skE_42': $int ).
tff('#skE_57',type,
'#skE_57': $int ).
tff('#skE_86',type,
'#skE_86': $int ).
tff('#skE_111',type,
'#skE_111': $int ).
tff('#skE_63',type,
'#skE_63': $int ).
tff('#skE_102',type,
'#skE_102': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_33',type,
'#skE_33': $int ).
tff('#skE_97',type,
'#skE_97': $int ).
tff('#skE_20',type,
'#skE_20': $int ).
tff('#skE_78',type,
'#skE_78': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_116',type,
'#skE_116': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_118',type,
'#skE_118': $int ).
tff('#skE_26',type,
'#skE_26': $int ).
tff('#skE_32',type,
'#skE_32': $int ).
tff('#skE_92',type,
'#skE_92': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_24',type,
'#skE_24': $int ).
tff('#skE_114',type,
'#skE_114': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_110',type,
'#skE_110': $int ).
tff('#skE_38',type,
'#skE_38': $int ).
tff('#skE_31',type,
'#skE_31': $int ).
tff('#skE_122',type,
'#skE_122': $int ).
tff('#skE_51',type,
'#skE_51': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_36',type,
'#skE_36': $int ).
tff('#skE_69',type,
'#skE_69': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_54',type,
'#skE_54': $int ).
tff('#skE_76',type,
'#skE_76': $int ).
tff('#skE_70',type,
'#skE_70': $int ).
tff('#skE_64',type,
'#skE_64': $int ).
tff('#skE_82',type,
'#skE_82': $int ).
tff('#skE_103',type,
'#skE_103': $int ).
tff('#skE_60',type,
'#skE_60': $int ).
tff('#skE_50',type,
'#skE_50': $int ).
tff('#skE_104',type,
'#skE_104': $int ).
tff('#skE_113',type,
'#skE_113': $int ).
tff('#skE_22',type,
'#skE_22': $int ).
tff('#skE_16',type,
'#skE_16': $int ).
tff('#skE_17',type,
'#skE_17': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_55',type,
'#skE_55': $int ).
tff('#skE_123',type,
'#skE_123': $int ).
tff('#skE_77',type,
'#skE_77': $int ).
tff('#skE_79',type,
'#skE_79': $int ).
tff('#skE_124',type,
'#skE_124': $int ).
tff('#skE_71',type,
'#skE_71': $int ).
tff('#skE_91',type,
'#skE_91': $int ).
tff('#skE_67',type,
'#skE_67': $int ).
tff('#skE_58',type,
'#skE_58': $int ).
tff('#skE_87',type,
'#skE_87': $int ).
tff('#skE_47',type,
'#skE_47': $int ).
tff('#skE_68',type,
'#skE_68': $int ).
tff('#skE_40',type,
'#skE_40': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_75',type,
'#skE_75': $int ).
tff('#skE_117',type,
'#skE_117': $int ).
tff('#skE_29',type,
'#skE_29': $int ).
tff('#skE_44',type,
'#skE_44': $int ).
tff('#skE_49',type,
'#skE_49': $int ).
tff('#skE_34',type,
'#skE_34': $int ).
tff('#skE_45',type,
'#skE_45': $int ).
tff('#skE_96',type,
'#skE_96': $int ).
tff('#skE_27',type,
'#skE_27': $int ).
tff('#skE_115',type,
'#skE_115': $int ).
tff('#skE_100',type,
'#skE_100': $int ).
tff('#skE_59',type,
'#skE_59': $int ).
tff('#skE_18',type,
'#skE_18': $int ).
tff('#skE_83',type,
'#skE_83': $int ).
tff('#skE_93',type,
'#skE_93': $int ).
tff('#skE_107',type,
'#skE_107': $int ).
tff('#skE_119',type,
'#skE_119': $int ).
tff('#skE_94',type,
'#skE_94': $int ).
tff('#skE_106',type,
'#skE_106': $int ).
tff('#skE_81',type,
'#skE_81': $int ).
tff('#skE_112',type,
'#skE_112': $int ).
tff('#skE_35',type,
'#skE_35': $int ).
tff('#skE_108',type,
'#skE_108': $int ).
tff('#skE_61',type,
'#skE_61': $int ).
tff('#skE_99',type,
'#skE_99': $int ).
tff('#skE_98',type,
'#skE_98': $int ).
tff('#skE_39',type,
'#skE_39': $int ).
tff('#skE_66',type,
'#skE_66': $int ).
tff('#skE_89',type,
'#skE_89': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_53',type,
'#skE_53': $int ).
tff('#skE_65',type,
'#skE_65': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
tff('#skE_72',type,
'#skE_72': $int ).
tff('#skE_56',type,
'#skE_56': $int ).
%Foreground operators:
tff(split2,type,
split2: record > record ).
tff('#skF_1',type,
'#skF_1': record ).
tff(next,type,
next: record > record ).
tff('#skF_2',type,
'#skF_2': record ).
tff(isrecord,type,
isrecord: record > $o ).
tff(split1,type,
split1: record > record ).
tff(data,type,
data: record > $int ).
tff(length,type,
length: record > $int ).
tff(f_141,negated_conjecture,
~ ! [U: record,V: record] :
( ( isrecord(U)
& isrecord(next(U))
& ( V = next(next(U)) )
& ( $sum(length(split1(V)),length(split2(V))) = length(V) ) )
=> ( $sum(length(split1(U)),length(split2(U))) = length(U) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
tff(f_66,axiom,
! [U: record] :
( isrecord(U)
=> $greatereq(length(U),1) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax2) ).
tff(f_80,axiom,
! [U: record] :
( isrecord(U)
=> isrecord(split1(U)) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax5) ).
tff(f_62,axiom,
! [U: record] :
( ~ isrecord(U)
=> ( length(U) = 0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax1) ).
tff(f_122,axiom,
! [U: record] :
( ( isrecord(U)
& isrecord(next(U)) )
=> ( data(split2(U)) = data(next(U)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax12) ).
tff(f_70,axiom,
! [U: record] :
( isrecord(U)
=> ( length(U) = $sum(length(next(U)),1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax3) ).
tff(f_110,axiom,
! [U: record] :
( ~ isrecord(next(U))
=> ~ isrecord(split2(U)) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax10) ).
tff(f_116,axiom,
! [U: record] :
( ( isrecord(U)
& isrecord(next(U)) )
=> isrecord(split2(U)) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax11) ).
tff(f_98,axiom,
! [U: record] :
( ( isrecord(U)
& isrecord(next(U)) )
=> ( next(split1(U)) = split1(next(next(U))) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax8) ).
tff(f_128,axiom,
! [U: record] :
( ( isrecord(U)
& isrecord(next(U)) )
=> ( next(split2(U)) = split2(next(next(U))) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/DAT003_0.ax',ax13) ).
tff(c_40,plain,
isrecord('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_4,plain,
! [U_2: record] :
( $greatereq(length(U_2),1)
| ~ isrecord(U_2) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_76,plain,
! [U_19: record] :
( ~ $less(length(U_19),1)
| ~ isrecord(U_19) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_4]) ).
tff(c_96,plain,
~ $less(length('#skF_1'),1),
inference(resolution,[status(thm)],[c_40,c_76]) ).
tff(c_100,plain,
length('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_96]) ).
tff(c_12,plain,
! [U_5: record] :
( isrecord(split1(U_5))
| ~ isrecord(U_5) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_268,plain,
! [U_25: record] :
( ~ $less(length(split1(U_25)),1)
| ~ isrecord(U_25) ),
inference(resolution,[status(thm)],[c_12,c_76]) ).
tff(c_308,plain,
~ $less(length(split1('#skF_1')),1),
inference(resolution,[status(thm)],[c_40,c_268]) ).
tff(c_312,plain,
length(split1('#skF_1')) = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_308]) ).
tff(c_30,plain,
$sum(length(split1('#skF_1')),length(split2('#skF_1'))) != length('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_42,plain,
length(split2('#skF_1')) != $sum(length('#skF_1'),$uminus(length(split1('#skF_1')))),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_30]) ).
tff(c_5333,plain,
length(split2('#skF_1')) != $sum('#skE_1',$uminus('#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_100,c_312,c_42]) ).
tff(c_5335,plain,
length(split2('#skF_1')) != $sum($uminus('#skE_7'),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5333]) ).
tff(c_5336,plain,
length(split2('#skF_1')) = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_5335]) ).
tff(c_5338,plain,
$sum($uminus('#skE_7'),'#skE_1') != '#skE_10',
inference(demodulation,[status(thm),theory(equality)],[c_5336,c_5335]) ).
tff(c_5341,plain,
'#skE_7' != $sum('#skE_1',$uminus('#skE_10')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5338]) ).
tff(c_38,plain,
isrecord(next('#skF_1')),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_47,plain,
! [U_1: record] :
( ( length(U_1) = 0 )
| isrecord(U_1) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_36,plain,
next(next('#skF_1')) = '#skF_2',
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_1217,plain,
! [U_42: record] :
( ( data(split2(U_42)) = data(next(U_42)) )
| ~ isrecord(next(U_42))
| ~ isrecord(U_42) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_1256,plain,
( ( data(split2(next('#skF_1'))) = data(next(next('#skF_1'))) )
| ~ isrecord('#skF_2')
| ~ isrecord(next('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_36,c_1217]) ).
tff(c_1286,plain,
( ( data(split2(next('#skF_1'))) = data('#skF_2') )
| ~ isrecord('#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_36,c_1256]) ).
tff(c_1298,plain,
data('#skF_2') = '#skE_19',
inference(define,[status(thm),theory(equality)],[c_1286]) ).
tff(c_1297,plain,
data(split2(next('#skF_1'))) = '#skE_18',
inference(define,[status(thm),theory(equality)],[c_1286]) ).
tff(c_1303,plain,
( ( '#skE_19' = '#skE_18' )
| ~ isrecord('#skF_2') ),
inference(demodulation,[status(thm),theory(equality)],[c_1298,c_1297,c_1286]) ).
tff(c_1316,plain,
~ isrecord('#skF_2'),
inference(splitLeft,[status(thm)],[c_1303]) ).
tff(c_1361,plain,
length('#skF_2') = 0,
inference(resolution,[status(thm)],[c_47,c_1316]) ).
tff(c_94,plain,
~ $less(length(next('#skF_1')),1),
inference(resolution,[status(thm)],[c_38,c_76]) ).
tff(c_111,plain,
length(next('#skF_1')) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_94]) ).
tff(c_7,plain,
! [U_3: record] :
( ( $sum(length(next(U_3)),1) = length(U_3) )
| ~ isrecord(U_3) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_923,plain,
! [U_39: record] :
( ( length(next(U_39)) = $sum($uminus(1),length(U_39)) )
| ~ isrecord(U_39) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_7]) ).
tff(c_965,plain,
length(next('#skF_1')) = $sum($uminus(1),length('#skF_1')),
inference(resolution,[status(thm)],[c_40,c_923]) ).
tff(c_996,plain,
'#skE_2' = $sum($uminus(1),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_111,c_100,c_965]) ).
tff(c_33,plain,
$sum(length(split1('#skF_2')),length(split2('#skF_2'))) = length('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_41,plain,
length(split2('#skF_2')) = $sum(length('#skF_2'),$uminus(length(split1('#skF_2')))),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_33]) ).
tff(c_562,plain,
length('#skF_2') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_41]) ).
tff(c_962,plain,
length(next(next('#skF_1'))) = $sum($uminus(1),length(next('#skF_1'))),
inference(resolution,[status(thm)],[c_38,c_923]) ).
tff(c_991,plain,
$sum($uminus(1),'#skE_2') = '#skE_12',
inference(demodulation,[status(thm),theory(equality)],[c_562,c_111,c_36,c_962]) ).
tff(c_993,plain,
'#skE_2' = $sum(1,'#skE_12'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_991]) ).
tff(c_1003,plain,
$sum(1,'#skE_12') = $sum($uminus(1),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_996,c_993]) ).
tff(c_1006,plain,
'#skE_12' = $sum($uminus(2),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1003]) ).
tff(c_1025,plain,
length('#skF_2') = $sum($uminus(2),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_1006,c_562]) ).
tff(c_1362,plain,
$sum($uminus(2),'#skE_1') = 0,
inference(demodulation,[status(thm),theory(equality)],[c_1361,c_1025]) ).
tff(c_1365,plain,
'#skE_1' = 2,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1362]) ).
tff(c_92,plain,
! [U_1: record] :
( ~ $less(length(U_1),1)
| ( length(U_1) = 0 ) ),
inference(resolution,[status(thm)],[c_47,c_76]) ).
tff(c_569,plain,
( ~ $less('#skE_12',1)
| ( length('#skF_2') = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_562,c_92]) ).
tff(c_574,plain,
( ~ $less('#skE_12',1)
| ( '#skE_12' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_562,c_569]) ).
tff(c_600,plain,
~ $less('#skE_12',1),
inference(splitLeft,[status(thm)],[c_574]) ).
tff(c_1013,plain,
~ $less($sum($uminus(2),'#skE_1'),1),
inference(demodulation,[status(thm),theory(equality)],[c_1006,c_600]) ).
tff(c_1023,plain,
~ $less('#skE_1',3),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1013]) ).
tff(c_1384,plain,
~ $less(2,3),
inference(demodulation,[status(thm),theory(equality)],[c_1365,c_1023]) ).
tff(c_1399,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1384]) ).
tff(c_1401,plain,
isrecord('#skF_2'),
inference(splitRight,[status(thm)],[c_1303]) ).
tff(c_70,plain,
! [U_18: record] :
( ~ isrecord(split2(U_18))
| isrecord(next(U_18)) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_253,plain,
! [U_24: record] :
( isrecord(next(U_24))
| ( length(split2(U_24)) = 0 ) ),
inference(resolution,[status(thm)],[c_47,c_70]) ).
tff(c_267,plain,
( isrecord('#skF_2')
| ( length(split2(next('#skF_1'))) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_36,c_253]) ).
tff(c_441,plain,
length(split2(next('#skF_1'))) = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_267]) ).
tff(c_445,plain,
( isrecord('#skF_2')
| ( '#skE_9' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_441,c_267]) ).
tff(c_447,plain,
'#skE_9' = 0,
inference(splitLeft,[status(thm)],[c_445]) ).
tff(c_444,plain,
length(split2(next('#skF_1'))) = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_267]) ).
tff(c_449,plain,
length(split2(next('#skF_1'))) = 0,
inference(demodulation,[status(thm),theory(equality)],[c_447,c_444]) ).
tff(c_208,plain,
! [U_22: record] :
( isrecord(split2(U_22))
| ~ isrecord(next(U_22))
| ~ isrecord(U_22) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_46,plain,
! [U_2: record] :
( ~ $less(length(U_2),1)
| ~ isrecord(U_2) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_4]) ).
tff(c_1989,plain,
! [U_46: record] :
( ~ $less(length(split2(U_46)),1)
| ~ isrecord(next(U_46))
| ~ isrecord(U_46) ),
inference(resolution,[status(thm)],[c_208,c_46]) ).
tff(c_2040,plain,
( ~ $less(length(split2(next('#skF_1'))),1)
| ~ isrecord('#skF_2')
| ~ isrecord(next('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_36,c_1989]) ).
tff(c_2074,plain,
~ $less(0,1),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_1401,c_449,c_2040]) ).
tff(c_2077,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2074]) ).
tff(c_2080,plain,
'#skE_12' = 0,
inference(splitRight,[status(thm)],[c_574]) ).
tff(c_558,plain,
length(split1('#skF_2')) = '#skE_13',
inference(define,[status(thm),theory(equality)],[c_41]) ).
tff(c_557,plain,
length('#skF_2') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_41]) ).
tff(c_556,plain,
length(split2('#skF_2')) = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_41]) ).
tff(c_560,plain,
$sum('#skE_12',$uminus('#skE_13')) = '#skE_11',
inference(demodulation,[status(thm),theory(equality)],[c_558,c_557,c_556,c_41]) ).
tff(c_565,plain,
'#skE_13' = $sum('#skE_12',$uminus('#skE_11')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_560]) ).
tff(c_2100,plain,
'#skE_13' = $sum(0,$uminus('#skE_11')),
inference(demodulation,[status(thm),theory(equality)],[c_2080,c_565]) ).
tff(c_2102,plain,
'#skE_13' = $uminus('#skE_11'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2100]) ).
tff(c_563,plain,
length(split1('#skF_2')) = '#skE_13',
inference(define,[status(thm),theory(equality)],[c_41]) ).
tff(c_591,plain,
( ~ $less('#skE_13',1)
| ( length(split1('#skF_2')) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_563,c_92]) ).
tff(c_596,plain,
( ~ $less('#skE_13',1)
| ( '#skE_13' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_563,c_591]) ).
tff(c_2120,plain,
( ~ $less($uminus('#skE_11'),1)
| ( $uminus('#skE_11') = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2102,c_2102,c_596]) ).
tff(c_2122,plain,
( ~ $less($uminus(1),'#skE_11')
| ( '#skE_11' = 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2120]) ).
tff(c_2124,plain,
~ $less($uminus(1),'#skE_11'),
inference(splitLeft,[status(thm)],[c_2122]) ).
tff(c_561,plain,
length(split2('#skF_2')) = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_41]) ).
tff(c_580,plain,
( ~ $less('#skE_11',1)
| ( length(split2('#skF_2')) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_561,c_92]) ).
tff(c_585,plain,
( ~ $less('#skE_11',1)
| ( '#skE_11' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_561,c_580]) ).
tff(c_2119,plain,
~ $less('#skE_11',1),
inference(splitLeft,[status(thm)],[c_585]) ).
tff(c_2125,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_2124,c_2119]) ).
tff(c_2128,plain,
'#skE_11' = 0,
inference(splitRight,[status(thm)],[c_2122]) ).
tff(c_2199,plain,
~ $less(0,1),
inference(demodulation,[status(thm),theory(equality)],[c_2128,c_2119]) ).
tff(c_2210,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2199]) ).
tff(c_2213,plain,
'#skE_11' = 0,
inference(splitRight,[status(thm)],[c_585]) ).
tff(c_2105,plain,
length(split1('#skF_2')) = $uminus('#skE_11'),
inference(demodulation,[status(thm),theory(equality)],[c_2102,c_563]) ).
tff(c_2215,plain,
length(split1('#skF_2')) = $uminus(0),
inference(demodulation,[status(thm),theory(equality)],[c_2213,c_2105]) ).
tff(c_2223,plain,
length(split1('#skF_2')) = 0,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2215]) ).
tff(c_3615,plain,
! [U_63: record] :
( ( split1(next(next(U_63))) = next(split1(U_63)) )
| ~ isrecord(next(U_63))
| ~ isrecord(U_63) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_3669,plain,
( ( split1(next(next('#skF_1'))) = next(split1('#skF_1')) )
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_38,c_3615]) ).
tff(c_3705,plain,
next(split1('#skF_1')) = split1('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_36,c_3669]) ).
tff(c_75,plain,
! [U_18: record] :
( isrecord(next(U_18))
| ( length(split2(U_18)) = 0 ) ),
inference(resolution,[status(thm)],[c_47,c_70]) ).
tff(c_3738,plain,
( isrecord(split1('#skF_2'))
| ( length(split2(split1('#skF_1'))) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_3705,c_75]) ).
tff(c_3764,plain,
length(split2(split1('#skF_1'))) = '#skE_21',
inference(define,[status(thm),theory(equality)],[c_3738]) ).
tff(c_3768,plain,
( isrecord(split1('#skF_2'))
| ( '#skE_21' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3764,c_3738]) ).
tff(c_3794,plain,
'#skE_21' = 0,
inference(splitLeft,[status(thm)],[c_3768]) ).
tff(c_3767,plain,
length(split2(split1('#skF_1'))) = '#skE_21',
inference(define,[status(thm),theory(equality)],[c_3738]) ).
tff(c_3797,plain,
length(split2(split1('#skF_1'))) = 0,
inference(demodulation,[status(thm),theory(equality)],[c_3794,c_3767]) ).
tff(c_4640,plain,
! [U_70: record] :
( ~ $less(length(split2(U_70)),1)
| ~ isrecord(next(U_70))
| ~ isrecord(U_70) ),
inference(resolution,[status(thm)],[c_208,c_46]) ).
tff(c_4655,plain,
( ~ $less(length(split2(split1('#skF_1'))),1)
| ~ isrecord(split1('#skF_2'))
| ~ isrecord(split1('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_3705,c_4640]) ).
tff(c_4718,plain,
( ~ $less(0,1)
| ~ isrecord(split1('#skF_2'))
| ~ isrecord(split1('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_3797,c_4655]) ).
tff(c_4720,plain,
( ~ isrecord(split1('#skF_2'))
| ~ isrecord(split1('#skF_1')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4718]) ).
tff(c_4756,plain,
~ isrecord(split1('#skF_1')),
inference(splitLeft,[status(thm)],[c_4720]) ).
tff(c_4801,plain,
~ isrecord('#skF_1'),
inference(resolution,[status(thm)],[c_12,c_4756]) ).
tff(c_4836,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_4801]) ).
tff(c_4838,plain,
isrecord(split1('#skF_1')),
inference(splitRight,[status(thm)],[c_4720]) ).
tff(c_45,plain,
! [U_3: record] :
( ( length(next(U_3)) = $sum($uminus(1),length(U_3)) )
| ~ isrecord(U_3) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_7]) ).
tff(c_4847,plain,
length(next(split1('#skF_1'))) = $sum($uminus(1),length(split1('#skF_1'))),
inference(resolution,[status(thm)],[c_4838,c_45]) ).
tff(c_4866,plain,
$sum($uminus(1),'#skE_7') = 0,
inference(demodulation,[status(thm),theory(equality)],[c_312,c_2223,c_3705,c_4847]) ).
tff(c_4868,plain,
'#skE_7' = 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4866]) ).
tff(c_2084,plain,
length('#skF_2') = 0,
inference(demodulation,[status(thm),theory(equality)],[c_2080,c_562]) ).
tff(c_2287,plain,
! [U_49: record] :
( ( length(next(U_49)) = $sum($uminus(1),length(U_49)) )
| ~ isrecord(U_49) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_7]) ).
tff(c_2320,plain,
length(next(next('#skF_1'))) = $sum($uminus(1),length(next('#skF_1'))),
inference(resolution,[status(thm)],[c_38,c_2287]) ).
tff(c_2345,plain,
$sum($uminus(1),'#skE_2') = 0,
inference(demodulation,[status(thm),theory(equality)],[c_2084,c_36,c_111,c_2320]) ).
tff(c_2347,plain,
'#skE_2' = 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2345]) ).
tff(c_2323,plain,
length(next('#skF_1')) = $sum($uminus(1),length('#skF_1')),
inference(resolution,[status(thm)],[c_40,c_2287]) ).
tff(c_2350,plain,
'#skE_2' = $sum($uminus(1),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_100,c_111,c_2323]) ).
tff(c_2369,plain,
$sum($uminus(1),'#skE_1') = 1,
inference(demodulation,[status(thm),theory(equality)],[c_2347,c_2350]) ).
tff(c_2371,plain,
'#skE_1' = 2,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2369]) ).
tff(c_534,plain,
length(split2('#skF_1')) != $sum('#skE_1',$uminus('#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_312,c_100,c_42]) ).
tff(c_536,plain,
length(split2('#skF_1')) != $sum($uminus('#skE_7'),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_534]) ).
tff(c_537,plain,
length(split2('#skF_1')) = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_536]) ).
tff(c_539,plain,
$sum($uminus('#skE_7'),'#skE_1') != '#skE_10',
inference(demodulation,[status(thm),theory(equality)],[c_537,c_536]) ).
tff(c_542,plain,
'#skE_7' != $sum('#skE_1',$uminus('#skE_10')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_539]) ).
tff(c_2379,plain,
'#skE_7' != $sum(2,$uminus('#skE_10')),
inference(demodulation,[status(thm),theory(equality)],[c_2371,c_542]) ).
tff(c_4885,plain,
$sum(2,$uminus('#skE_10')) != 1,
inference(demodulation,[status(thm),theory(equality)],[c_4868,c_2379]) ).
tff(c_4893,plain,
'#skE_10' != 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4885]) ).
tff(c_540,plain,
length(split2('#skF_1')) = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_536]) ).
tff(c_2225,plain,
length(split2('#skF_2')) = 0,
inference(demodulation,[status(thm),theory(equality)],[c_2213,c_561]) ).
tff(c_3154,plain,
! [U_59: record] :
( ( split2(next(next(U_59))) = next(split2(U_59)) )
| ~ isrecord(next(U_59))
| ~ isrecord(U_59) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_3196,plain,
( ( split2(next(next('#skF_1'))) = next(split2('#skF_1')) )
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_38,c_3154]) ).
tff(c_3225,plain,
next(split2('#skF_1')) = split2('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_36,c_3196]) ).
tff(c_24,plain,
! [U_11: record] :
( isrecord(split2(U_11))
| ~ isrecord(next(U_11))
| ~ isrecord(U_11) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_3249,plain,
( isrecord(split2('#skF_2'))
| ( length(split2(split2('#skF_1'))) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_3225,c_75]) ).
tff(c_3251,plain,
length(split2(split2('#skF_1'))) = '#skE_22',
inference(define,[status(thm),theory(equality)],[c_3249]) ).
tff(c_3255,plain,
( isrecord(split2('#skF_2'))
| ( '#skE_22' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3251,c_3249]) ).
tff(c_3281,plain,
'#skE_22' = 0,
inference(splitLeft,[status(thm)],[c_3255]) ).
tff(c_3254,plain,
length(split2(split2('#skF_1'))) = '#skE_22',
inference(define,[status(thm),theory(equality)],[c_3249]) ).
tff(c_3284,plain,
length(split2(split2('#skF_1'))) = 0,
inference(demodulation,[status(thm),theory(equality)],[c_3281,c_3254]) ).
tff(c_4667,plain,
( ~ $less(length(split2(split2('#skF_1'))),1)
| ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_3225,c_4640]) ).
tff(c_4727,plain,
( ~ $less(0,1)
| ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_3284,c_4667]) ).
tff(c_4729,plain,
( ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4727]) ).
tff(c_5004,plain,
~ isrecord(split2('#skF_1')),
inference(splitLeft,[status(thm)],[c_4729]) ).
tff(c_5057,plain,
( ~ isrecord(next('#skF_1'))
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_24,c_5004]) ).
tff(c_5093,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_5057]) ).
tff(c_5095,plain,
isrecord(split2('#skF_1')),
inference(splitRight,[status(thm)],[c_4729]) ).
tff(c_5104,plain,
length(next(split2('#skF_1'))) = $sum($uminus(1),length(split2('#skF_1'))),
inference(resolution,[status(thm)],[c_5095,c_45]) ).
tff(c_5125,plain,
$sum($uminus(1),'#skE_10') = 0,
inference(demodulation,[status(thm),theory(equality)],[c_540,c_2225,c_3225,c_5104]) ).
tff(c_5127,plain,
'#skE_10' = 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5125]) ).
tff(c_5225,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4893,c_5127]) ).
tff(c_5226,plain,
isrecord('#skF_2'),
inference(splitRight,[status(thm)],[c_445]) ).
tff(c_5243,plain,
~ $less(length('#skF_2'),1),
inference(resolution,[status(thm)],[c_5226,c_46]) ).
tff(c_5247,plain,
length('#skF_2') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_5243]) ).
tff(c_5283,plain,
length(split2('#skF_2')) = $sum('#skE_12',$uminus(length(split1('#skF_2')))),
inference(demodulation,[status(thm),theory(equality)],[c_5247,c_41]) ).
tff(c_5289,plain,
length(split2('#skF_2')) = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_5283]) ).
tff(c_5339,plain,
length(split2('#skF_1')) = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_5335]) ).
tff(c_5983,plain,
! [U_83: record] :
( ( split2(next(next(U_83))) = next(split2(U_83)) )
| ~ isrecord(next(U_83))
| ~ isrecord(U_83) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_6019,plain,
( ( split2(next(next('#skF_1'))) = next(split2('#skF_1')) )
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_38,c_5983]) ).
tff(c_6044,plain,
next(split2('#skF_1')) = split2('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_36,c_6019]) ).
tff(c_6068,plain,
( isrecord(split2('#skF_2'))
| ( length(split2(split2('#skF_1'))) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6044,c_75]) ).
tff(c_6095,plain,
length(split2(split2('#skF_1'))) = '#skE_22',
inference(define,[status(thm),theory(equality)],[c_6068]) ).
tff(c_6099,plain,
( isrecord(split2('#skF_2'))
| ( '#skE_22' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_6095,c_6068]) ).
tff(c_6120,plain,
'#skE_22' = 0,
inference(splitLeft,[status(thm)],[c_6099]) ).
tff(c_6098,plain,
length(split2(split2('#skF_1'))) = '#skE_22',
inference(define,[status(thm),theory(equality)],[c_6068]) ).
tff(c_6123,plain,
length(split2(split2('#skF_1'))) = 0,
inference(demodulation,[status(thm),theory(equality)],[c_6120,c_6098]) ).
tff(c_8518,plain,
! [U_106: record] :
( ~ $less(length(split2(U_106)),1)
| ~ isrecord(next(U_106))
| ~ isrecord(U_106) ),
inference(resolution,[status(thm)],[c_208,c_46]) ).
tff(c_8554,plain,
( ~ $less(length(split2(split2('#skF_1'))),1)
| ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_6044,c_8518]) ).
tff(c_8612,plain,
( ~ $less(0,1)
| ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_6123,c_8554]) ).
tff(c_8614,plain,
( ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_8612]) ).
tff(c_8638,plain,
~ isrecord(split2('#skF_1')),
inference(splitLeft,[status(thm)],[c_8614]) ).
tff(c_8685,plain,
( ~ isrecord(next('#skF_1'))
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_24,c_8638]) ).
tff(c_8721,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_8685]) ).
tff(c_8722,plain,
~ isrecord(split2('#skF_2')),
inference(splitRight,[status(thm)],[c_8614]) ).
tff(c_8846,plain,
length(split2('#skF_2')) = 0,
inference(resolution,[status(thm)],[c_47,c_8722]) ).
tff(c_8939,plain,
'#skE_11' = 0,
inference(demodulation,[status(thm),theory(equality)],[c_8846,c_5289]) ).
tff(c_5302,plain,
( ~ $less('#skE_11',1)
| ( length(split2('#skF_2')) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_5289,c_92]) ).
tff(c_5307,plain,
( ~ $less('#skE_11',1)
| ( '#skE_11' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5289,c_5302]) ).
tff(c_5332,plain,
~ $less('#skE_11',1),
inference(splitLeft,[status(thm)],[c_5307]) ).
tff(c_9071,plain,
~ $less(0,1),
inference(demodulation,[status(thm),theory(equality)],[c_8939,c_5332]) ).
tff(c_9075,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_9071]) ).
tff(c_9076,plain,
isrecord(split2('#skF_2')),
inference(splitRight,[status(thm)],[c_6099]) ).
tff(c_28,plain,
! [U_13: record] :
( ( split2(next(next(U_13))) = next(split2(U_13)) )
| ~ isrecord(next(U_13))
| ~ isrecord(U_13) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_6048,plain,
( ( split2(next(next(split2('#skF_1')))) = next(split2(split2('#skF_1'))) )
| ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(superposition,[status(thm),theory(equality)],[c_6044,c_28]) ).
tff(c_6063,plain,
( ( next(split2(split2('#skF_1'))) = split2(next(split2('#skF_2'))) )
| ~ isrecord(split2('#skF_2'))
| ~ isrecord(split2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_6044,c_6048]) ).
tff(c_10037,plain,
( ( next(split2(split2('#skF_1'))) = split2(next(split2('#skF_2'))) )
| ~ isrecord(split2('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_9076,c_6063]) ).
tff(c_10038,plain,
~ isrecord(split2('#skF_1')),
inference(splitLeft,[status(thm)],[c_10037]) ).
tff(c_10080,plain,
( ~ isrecord(next('#skF_1'))
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_24,c_10038]) ).
tff(c_10116,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_10080]) ).
tff(c_10118,plain,
isrecord(split2('#skF_1')),
inference(splitRight,[status(thm)],[c_10037]) ).
tff(c_10121,plain,
length(next(split2('#skF_1'))) = $sum($uminus(1),length(split2('#skF_1'))),
inference(resolution,[status(thm)],[c_10118,c_45]) ).
tff(c_10142,plain,
'#skE_11' = $sum($uminus(1),'#skE_10'),
inference(demodulation,[status(thm),theory(equality)],[c_5289,c_5339,c_6044,c_10121]) ).
tff(c_5569,plain,
! [U_77: record] :
( ( length(next(U_77)) = $sum($uminus(1),length(U_77)) )
| ~ isrecord(U_77) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_7]) ).
tff(c_5608,plain,
length(next('#skF_1')) = $sum($uminus(1),length('#skF_1')),
inference(resolution,[status(thm)],[c_40,c_5569]) ).
tff(c_5638,plain,
'#skE_2' = $sum($uminus(1),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_100,c_111,c_5608]) ).
tff(c_5605,plain,
length(next(next('#skF_1'))) = $sum($uminus(1),length(next('#skF_1'))),
inference(resolution,[status(thm)],[c_38,c_5569]) ).
tff(c_5633,plain,
$sum($uminus(1),'#skE_2') = '#skE_12',
inference(demodulation,[status(thm),theory(equality)],[c_5247,c_36,c_111,c_5605]) ).
tff(c_5635,plain,
'#skE_2' = $sum(1,'#skE_12'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5633]) ).
tff(c_5645,plain,
$sum(1,'#skE_12') = $sum($uminus(1),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_5638,c_5635]) ).
tff(c_5648,plain,
'#skE_12' = $sum($uminus(2),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5645]) ).
tff(c_5286,plain,
length(split1('#skF_2')) = '#skE_13',
inference(define,[status(thm),theory(equality)],[c_5283]) ).
tff(c_5285,plain,
length(split2('#skF_2')) = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_5283]) ).
tff(c_5284,plain,
length(split2('#skF_2')) = $sum('#skE_12',$uminus(length(split1('#skF_2')))),
inference(demodulation,[status(thm),theory(equality)],[c_5247,c_41]) ).
tff(c_5288,plain,
$sum('#skE_12',$uminus('#skE_13')) = '#skE_11',
inference(demodulation,[status(thm),theory(equality)],[c_5286,c_5285,c_5284]) ).
tff(c_5292,plain,
'#skE_13' = $sum('#skE_12',$uminus('#skE_11')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5288]) ).
tff(c_5290,plain,
length(split1('#skF_2')) = '#skE_13',
inference(define,[status(thm),theory(equality)],[c_5283]) ).
tff(c_5428,plain,
length(split1('#skF_2')) = $sum('#skE_12',$uminus('#skE_11')),
inference(demodulation,[status(thm),theory(equality)],[c_5292,c_5290]) ).
tff(c_5430,plain,
length(split1('#skF_2')) = $sum($uminus('#skE_11'),'#skE_12'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5428]) ).
tff(c_5433,plain,
length(split1('#skF_2')) = $sum('#skE_12',$uminus('#skE_11')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5430]) ).
tff(c_5649,plain,
length(split1('#skF_2')) = $sum($sum($uminus(2),'#skE_1'),$uminus('#skE_11')),
inference(demodulation,[status(thm),theory(equality)],[c_5648,c_5433]) ).
tff(c_5663,plain,
length(split1('#skF_2')) = $sum($uminus(2),$sum($uminus('#skE_11'),'#skE_1')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5649]) ).
tff(c_37637,plain,
length(split1('#skF_2')) = $sum($uminus(2),$sum($uminus($sum($uminus(1),'#skE_10')),'#skE_1')),
inference(demodulation,[status(thm),theory(equality)],[c_10142,c_5663]) ).
tff(c_37639,plain,
length(split1('#skF_2')) = $sum($uminus(1),$sum($uminus('#skE_10'),'#skE_1')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_37637]) ).
tff(c_15910,plain,
! [U_159: record] :
( ( split1(next(next(U_159))) = next(split1(U_159)) )
| ~ isrecord(next(U_159))
| ~ isrecord(U_159) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_16060,plain,
( ( split1(next(next('#skF_1'))) = next(split1('#skF_1')) )
| ~ isrecord('#skF_1') ),
inference(resolution,[status(thm)],[c_38,c_15910]) ).
tff(c_16163,plain,
next(split1('#skF_1')) = split1('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_36,c_16060]) ).
tff(c_37692,plain,
! [U_268: record] :
( ( length(next(U_268)) = $sum($uminus(1),length(U_268)) )
| ( length(U_268) = 0 ) ),
inference(resolution,[status(thm)],[c_47,c_5569]) ).
tff(c_37746,plain,
( ( $sum($uminus(1),length(split1('#skF_1'))) = length(split1('#skF_2')) )
| ( length(split1('#skF_1')) = 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16163,c_37692]) ).
tff(c_37816,plain,
( ( $sum($uminus(1),'#skE_7') = $sum($uminus(1),$sum($uminus('#skE_10'),'#skE_1')) )
| ( '#skE_7' = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_312,c_37639,c_312,c_37746]) ).
tff(c_37818,plain,
( ( '#skE_7' = $sum($uminus('#skE_10'),'#skE_1') )
| ( '#skE_7' = 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_37816]) ).
tff(c_37840,plain,
'#skE_7' = 0,
inference(splitLeft,[status(thm)],[c_37818]) ).
tff(c_309,plain,
length(split1('#skF_1')) = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_308]) ).
tff(c_313,plain,
~ $less('#skE_7',1),
inference(demodulation,[status(thm),theory(equality)],[c_309,c_308]) ).
tff(c_37917,plain,
~ $less(0,1),
inference(demodulation,[status(thm),theory(equality)],[c_37840,c_313]) ).
tff(c_37922,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_37917]) ).
tff(c_37923,plain,
'#skE_7' = $sum($uminus('#skE_10'),'#skE_1'),
inference(splitRight,[status(thm)],[c_37818]) ).
tff(c_37926,plain,
'#skE_7' = $sum('#skE_1',$uminus('#skE_10')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_37923]) ).
tff(c_37927,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5341,c_37926]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : DAT052_1 : TPTP v9.0.0. Released v5.0.0.
% 0.13/0.14 % 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.15/0.35 % Computer : n005.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Mon Apr 7 18:16:27 EDT 2025
% 0.15/0.35 % CPUTime :
% 19.44/6.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.44/6.65
% 19.44/6.65 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------