%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW643_2 : TPTP v9.0.0. Released v6.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 : n026.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 09:53:07 PM UTC 2025
% Result : Theorem 29.80s 10.70s
% Output : CNFRefutation 30.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 18
% Syntax : Number of formulae : 378 ( 243 unt; 0 typ; 0 def)
% Number of atoms : 697 ( 392 equ)
% Maximal formula atoms : 18 ( 1 avg)
% Number of connectives : 540 ( 221 ~; 287 |; 11 &)
% ( 5 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 125 ( 44 atm; 20 fun; 32 num; 29 var)
% Number of types : 7 ( 5 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 53 ( 49 usr; 28 con; 0-5 aty)
% Number of variables : 155 ( 151 !; 4 ?; 155 :)
% Comments :
%------------------------------------------------------------------------------
%$ mem > sort1 > sorted1 > match_list1 > match_bool1 > infix_plpl > cons > length1 > cons_proj_21 > cons_proj_11 > #nlpp > witness1 > tb2t1 > tb2t > t2tb1 > t2tb > nil > list > tuple03 > tuple0 > true1 > real > qtmark > int > false1 > bool > #skF_8 > #skF_7 > #skF_9 > #skF_1 > #skF_3 > #skF_2 > #skF_11 > #skF_6 > #skF_4 > #skF_16 > #skF_5 > #skF_15 > #skF_13
%Foreground sorts:
tff(tuple02,type,
tuple02: $tType ).
tff(list_int,type,
list_int: $tType ).
tff(bool1,type,
bool1: $tType ).
tff(ty,type,
ty: $tType ).
tff(uni,type,
uni: $tType ).
%Background operators:
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skF_14',type,
'#skF_14': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skF_10',type,
'#skF_10': $int ).
tff('#skF_12',type,
'#skF_12': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
%Foreground operators:
tff('#skF_8',type,
'#skF_8': ( list_int * list_int ) > $int ).
tff(list,type,
list: ty > ty ).
tff(length1,type,
length1: ( ty * uni ) > $int ).
tff(cons,type,
cons: ( ty * uni * uni ) > uni ).
tff(t2tb1,type,
t2tb1: $int > uni ).
tff(nil,type,
nil: ty > uni ).
tff(true1,type,
true1: bool1 ).
tff(match_list1,type,
match_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff('#skF_7',type,
'#skF_7': ( ty * uni * uni ) > uni ).
tff('#skF_9',type,
'#skF_9': ( list_int * list_int ) > $int ).
tff(int,type,
int: ty ).
tff(false1,type,
false1: bool1 ).
tff(sort1,type,
sort1: ( ty * uni ) > $o ).
tff(tb2t1,type,
tb2t1: uni > $int ).
tff(sorted1,type,
sorted1: list_int > $o ).
tff(witness1,type,
witness1: ty > uni ).
tff(t2tb,type,
t2tb: list_int > uni ).
tff(real,type,
real: ty ).
tff('#skF_1',type,
'#skF_1': list_int > $int ).
tff('#skF_3',type,
'#skF_3': list_int > $int ).
tff('#skF_2',type,
'#skF_2': list_int > $int ).
tff(match_bool1,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(tuple0,type,
tuple0: ty ).
tff(qtmark,type,
qtmark: ty ).
tff('#skF_11',type,
'#skF_11': list_int ).
tff(bool,type,
bool: ty ).
tff('#skF_6',type,
'#skF_6': ( ty * uni * uni ) > uni ).
tff('#skF_4',type,
'#skF_4': list_int > list_int ).
tff('#skF_16',type,
'#skF_16': bool1 ).
tff(tuple03,type,
tuple03: tuple02 ).
tff(cons_proj_11,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(tb2t,type,
tb2t: uni > list_int ).
tff('#skF_5',type,
'#skF_5': ( $int * list_int ) > $int ).
tff('#skF_15',type,
'#skF_15': list_int ).
tff(mem,type,
mem: ( ty * uni * uni ) > $o ).
tff('#skF_13',type,
'#skF_13': list_int ).
tff(cons_proj_21,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(infix_plpl,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(f_108,axiom,
! [Xa: $int] : sort1(int,t2tb1(Xa)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f_71,axiom,
! [A: ty,V: uni,V1: uni] : ( nil(A) != cons(A,V,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nil_Cons1) ).
tff(f_247,negated_conjecture,
~ ! [Xa: $int,L: list_int] :
( sorted1(L)
=> ( ( ( L = tb2t(nil(int)) )
=> ~ mem(int,t2tb1(Xa),t2tb(L)) )
& ! [X1a: $int,X2: list_int] :
( ( L = tb2t(cons(int,t2tb1(X1a),t2tb(X2))) )
=> ( ( ( Xa = X1a )
=> mem(int,t2tb1(Xa),t2tb(L)) )
& ( ( Xa != X1a )
=> ( ( $less(X1a,Xa)
=> ( ( L != tb2t(nil(int)) )
& ! [X3a: $int,X4: list_int] :
( ( L = tb2t(cons(int,t2tb1(X3a),t2tb(X4))) )
=> ( X4 = X2 ) )
& sorted1(X2)
& ! [Result: bool1] :
( ( ( Result = true1 )
<=> mem(int,t2tb1(Xa),t2tb(X2)) )
=> ( ( Result = true1 )
<=> mem(int,t2tb1(Xa),t2tb(L)) ) ) ) )
& ( ~ $less(X1a,Xa)
=> ~ mem(int,t2tb1(Xa),t2tb(L)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_find) ).
tff(f_105,axiom,
! [J: uni] : ( t2tb(tb2t(J)) = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f_99,axiom,
! [A: ty,X: uni] :
( sort1(A,X)
=> ( ~ mem(A,X,nil(A))
& ! [X1: uni,X2: uni] :
( sort1(A,X1)
=> ( mem(A,X,cons(A,X1,X2))
<=> ( ( X = X1 )
| mem(A,X,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_def) ).
tff(f_46,axiom,
! [U: bool1] :
( ( U = true1 )
| ( U = false1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bool_inversion) ).
tff(f_42,axiom,
true1 != false1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',true_False) ).
tff(f_143,axiom,
! [Xa: $int,L: list_int] :
( ( ! [Ya: $int] :
( mem(int,t2tb1(Ya),t2tb(L))
=> $lesseq(Xa,Ya) )
& sorted1(L) )
<=> sorted1(tb2t(cons(int,t2tb1(Xa),t2tb(L)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_mem) ).
tff(f_103,axiom,
! [I: list_int] : ( tb2t(t2tb(I)) = I ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(f_81,axiom,
! [A: ty,U: uni,U1: uni] : ( cons_proj_21(A,cons(A,U,U1)) = U1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cons_proj_2_def1) ).
tff(f_159,axiom,
! [A: ty] :
( ( length1(A,nil(A)) = 0 )
& ! [X: uni,X1: uni] : ( length1(A,cons(A,X,X1)) = $sum(1,length1(A,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_def) ).
tff(f_165,axiom,
! [A: ty,L: uni] :
( ( length1(A,L) = 0 )
<=> ( L = nil(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',length_nil) ).
tff(f_134,axiom,
! [Z: list_int] :
( sorted1(Z)
=> ( ( Z = tb2t(nil(int)) )
| ? [Xa: $int] : ( Z = tb2t(cons(int,t2tb1(Xa),nil(int))) )
| ? [Xa: $int,Ya: $int,L: list_int] :
( $lesseq(Xa,Ya)
& sorted1(tb2t(cons(int,t2tb1(Ya),t2tb(L))))
& ( Z = tb2t(cons(int,t2tb1(Xa),cons(int,t2tb1(Ya),t2tb(L)))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_inversion) ).
tff(f_77,axiom,
! [A: ty,U: uni,U1: uni] :
( sort1(A,U)
=> ( cons_proj_11(A,cons(A,U,U1)) = U ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cons_proj_1_def1) ).
tff(f_110,axiom,
! [Ia: $int] : ( tb2t1(t2tb1(Ia)) = Ia ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL1) ).
tff(f_202,axiom,
! [Xa: $int,Ya: $int,L: list_int] :
( $less(Xa,Ya)
=> ( sorted1(tb2t(cons(int,t2tb1(Ya),t2tb(L))))
=> ~ mem(int,t2tb1(Xa),cons(int,t2tb1(Ya),t2tb(L))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sorted_not_mem) ).
tff(f_73,axiom,
! [A: ty,X: uni] : sort1(A,cons_proj_11(A,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cons_proj_1_sort1) ).
tff(f_85,axiom,
! [A: ty,U: uni] :
( ( U = nil(A) )
| ( U = cons(A,cons_proj_11(A,U),cons_proj_21(A,U)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',list_inversion1) ).
tff(c_674,plain,
! [X_60a: $int] : sort1(int,t2tb1(X_60a)),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_28,plain,
! [A_36: ty,V_37: uni,V1_38: uni] : ( cons(A_36,V_37,V1_38) != nil(A_36) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_489,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| $less('#skF_12','#skF_10')
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_826,plain,
'#skF_12' = '#skF_10',
inference(splitLeft,[status(thm)],[c_489]) ).
tff(c_294,plain,
( ( tb2t(nil(int)) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_868,plain,
( ( tb2t(nil(int)) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skF_10'),t2tb('#skF_13'))) = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_826,c_294]) ).
tff(c_870,plain,
tb2t(nil(int)) = '#skF_11',
inference(splitLeft,[status(thm)],[c_868]) ).
tff(c_52,plain,
! [J_59: uni] : ( t2tb(tb2t(J_59)) = J_59 ),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_876,plain,
t2tb('#skF_11') = nil(int),
inference(superposition,[status(thm),theory(equality)],[c_870,c_52]) ).
tff(c_298,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_986,plain,
( mem(int,t2tb1('#skF_10'),nil(int))
| ( tb2t(cons(int,t2tb1('#skF_10'),t2tb('#skF_13'))) = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_826,c_876,c_298]) ).
tff(c_1381,plain,
tb2t(cons(int,t2tb1('#skF_10'),t2tb('#skF_13'))) = '#skF_11',
inference(splitLeft,[status(thm)],[c_986]) ).
tff(c_1393,plain,
cons(int,t2tb1('#skF_10'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_1381,c_52]) ).
tff(c_1408,plain,
cons(int,t2tb1('#skF_10'),t2tb('#skF_13')) = nil(int),
inference(demodulation,[status(thm),theory(equality)],[c_876,c_1393]) ).
tff(c_1412,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_1408]) ).
tff(c_1421,plain,
mem(int,t2tb1('#skF_10'),nil(int)),
inference(splitRight,[status(thm)],[c_986]) ).
tff(c_40,plain,
! [A_51: ty,X_52: uni] :
( ~ mem(A_51,X_52,nil(A_51))
| ~ sort1(A_51,X_52) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_1424,plain,
~ sort1(int,t2tb1('#skF_10')),
inference(resolution,[status(thm)],[c_1421,c_40]) ).
tff(c_1428,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_674,c_1424]) ).
tff(c_1856,plain,
tb2t(cons(int,t2tb1('#skF_10'),t2tb('#skF_13'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_868]) ).
tff(c_1957,plain,
cons(int,t2tb1('#skF_10'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_1856,c_52]) ).
tff(c_46,plain,
! [A_51: ty,X_52: uni,X2_56: uni] :
( mem(A_51,X_52,cons(A_51,X_52,X2_56))
| ~ sort1(A_51,X_52) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_1966,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(superposition,[status(thm),theory(equality)],[c_1957,c_46]) ).
tff(c_2013,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_1966]) ).
tff(c_1430,plain,
tb2t(nil(int)) != '#skF_11',
inference(splitRight,[status(thm)],[c_868]) ).
tff(c_306,plain,
( ( tb2t(nil(int)) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( '#skF_12' != '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_1447,plain,
( ( tb2t(nil(int)) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(demodulation,[status(thm),theory(equality)],[c_826,c_306]) ).
tff(c_1451,plain,
~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(negUnitSimplification,[status(thm)],[c_1430,c_1447]) ).
tff(c_2016,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2013,c_1451]) ).
tff(c_2022,plain,
'#skF_12' != '#skF_10',
inference(splitRight,[status(thm)],[c_489]) ).
tff(c_2043,plain,
tb2t(nil(int)) = '#skF_11',
inference(splitLeft,[status(thm)],[c_294]) ).
tff(c_2049,plain,
t2tb('#skF_11') = nil(int),
inference(superposition,[status(thm),theory(equality)],[c_2043,c_52]) ).
tff(c_2165,plain,
( mem(int,t2tb1('#skF_10'),nil(int))
| ( tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2049,c_298]) ).
tff(c_2567,plain,
tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11',
inference(splitLeft,[status(thm)],[c_2165]) ).
tff(c_2579,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_2567,c_52]) ).
tff(c_2594,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = nil(int),
inference(demodulation,[status(thm),theory(equality)],[c_2049,c_2579]) ).
tff(c_2598,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_2594]) ).
tff(c_2625,plain,
mem(int,t2tb1('#skF_10'),nil(int)),
inference(splitRight,[status(thm)],[c_2165]) ).
tff(c_2628,plain,
~ sort1(int,t2tb1('#skF_10')),
inference(resolution,[status(thm)],[c_2625,c_40]) ).
tff(c_2632,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_674,c_2628]) ).
tff(c_2634,plain,
tb2t(nil(int)) != '#skF_11',
inference(splitRight,[status(thm)],[c_294]) ).
tff(c_774,plain,
( ( false1 = '#skF_16' )
| ( true1 = '#skF_16' ) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_12,plain,
! [U_12: bool1] :
( ( false1 = U_12 )
| ( true1 = U_12 ) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_775,plain,
! [U_12: bool1] :
( ( false1 = U_12 )
| ( U_12 = '#skF_16' )
| ( false1 = '#skF_16' ) ),
inference(superposition,[status(thm),theory(equality)],[c_774,c_12]) ).
tff(c_2686,plain,
false1 = '#skF_16',
inference(splitLeft,[status(thm)],[c_775]) ).
tff(c_10,plain,
true1 != false1,
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_2695,plain,
true1 != '#skF_16',
inference(demodulation,[status(thm),theory(equality)],[c_2686,c_10]) ).
tff(c_569,plain,
( ( '#skF_15' != '#skF_13' )
| ( true1 = '#skF_16' )
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_2754,plain,
( ( '#skF_15' != '#skF_13' )
| ~ sorted1('#skF_13')
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_2695,c_569]) ).
tff(c_2756,plain,
~ sorted1('#skF_13'),
inference(splitLeft,[status(thm)],[c_2754]) ).
tff(c_131,plain,
sorted1('#skF_11'),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_3003,plain,
tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_294]) ).
tff(c_664,plain,
! [L_73: list_int,X_72a: $int] :
( sorted1(L_73)
| ~ sorted1(tb2t(cons(int,t2tb1(X_72a),t2tb(L_73)))) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_3009,plain,
( sorted1('#skF_13')
| ~ sorted1('#skF_11') ),
inference(superposition,[status(thm),theory(equality)],[c_3003,c_664]) ).
tff(c_3021,plain,
sorted1('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_131,c_3009]) ).
tff(c_3023,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2756,c_3021]) ).
tff(c_3028,plain,
( ( '#skF_15' != '#skF_13' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(splitRight,[status(thm)],[c_2754]) ).
tff(c_11685,plain,
'#skF_15' != '#skF_13',
inference(splitLeft,[status(thm)],[c_3028]) ).
tff(c_50,plain,
! [I_58: list_int] : ( tb2t(t2tb(I_58)) = I_58 ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_3206,plain,
tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_294]) ).
tff(c_11693,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_3206,c_52]) ).
tff(c_36,plain,
! [A_46: ty,U_47: uni,U1_48: uni] : ( cons_proj_21(A_46,cons(A_46,U_47,U1_48)) = U1_48 ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_11732,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_13'),
inference(superposition,[status(thm),theory(equality)],[c_11693,c_36]) ).
tff(c_3227,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_3206,c_52]) ).
tff(c_11895,plain,
! [A_2118: ty,X_2119: uni,X1_2120: uni] : ( length1(A_2118,cons(A_2118,X_2119,X1_2120)) = $sum(1,length1(A_2118,X1_2120)) ),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_11920,plain,
length1(int,t2tb('#skF_11')) = $sum(1,length1(int,t2tb('#skF_13'))),
inference(superposition,[status(thm),theory(equality)],[c_3227,c_11895]) ).
tff(c_11926,plain,
length1(int,t2tb('#skF_13')) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_11920]) ).
tff(c_11925,plain,
length1(int,t2tb('#skF_11')) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_11920]) ).
tff(c_11928,plain,
$sum(1,'#skE_2') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_11926,c_11925,c_11920]) ).
tff(c_11932,plain,
'#skE_2' = $sum($uminus(1),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11928]) ).
tff(c_11930,plain,
length1(int,t2tb('#skF_13')) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_11920]) ).
tff(c_659,plain,
! [A_99: ty,L_100: uni] :
( ( nil(A_99) = L_100 )
| ( length1(A_99,L_100) != 0 ) ),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_11956,plain,
( ( t2tb('#skF_13') = nil(int) )
| ( '#skE_2' != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11930,c_659]) ).
tff(c_11971,plain,
( ( t2tb('#skF_13') = nil(int) )
| ( $sum($uminus(1),'#skE_1') != 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11932,c_11956]) ).
tff(c_11973,plain,
( ( t2tb('#skF_13') = nil(int) )
| ( '#skE_1' != 1 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11971]) ).
tff(c_11975,plain,
'#skE_1' != 1,
inference(splitLeft,[status(thm)],[c_11973]) ).
tff(c_658,plain,
! [A_99: ty] : ( length1(A_99,nil(A_99)) = 0 ),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_11929,plain,
length1(int,t2tb('#skF_11')) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_11920]) ).
tff(c_70,plain,
! [Z_67: list_int] :
( $lesseq('#skF_2'(Z_67),'#skF_3'(Z_67))
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_67)),nil(int))) = Z_67 )
| ( tb2t(nil(int)) = Z_67 )
| ~ sorted1(Z_67) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_14936,plain,
! [Z_2467: list_int] :
( ~ $less('#skF_3'(Z_2467),'#skF_2'(Z_2467))
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_2467)),nil(int))) = Z_2467 )
| ( tb2t(nil(int)) = Z_2467 )
| ~ sorted1(Z_2467) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_70]) ).
tff(c_14957,plain,
( ~ $less('#skF_3'('#skF_11'),'#skF_2'('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' )
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(resolution,[status(thm)],[c_131,c_14936]) ).
tff(c_14974,plain,
( ~ $less('#skF_3'('#skF_11'),'#skF_2'('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_2634,c_14957]) ).
tff(c_14983,plain,
'#skF_1'('#skF_11') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_14974]) ).
tff(c_14981,plain,
'#skF_3'('#skF_11') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_14974]) ).
tff(c_14982,plain,
'#skF_2'('#skF_11') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_14974]) ).
tff(c_15785,plain,
! [Z_2540: list_int] :
( ( tb2t(cons(int,t2tb1('#skF_2'(Z_2540)),cons(int,t2tb1('#skF_3'(Z_2540)),t2tb('#skF_4'(Z_2540))))) = Z_2540 )
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_2540)),nil(int))) = Z_2540 )
| ( tb2t(nil(int)) = Z_2540 )
| ~ sorted1(Z_2540) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_15818,plain,
( ( tb2t(cons(int,t2tb1('#skF_2'('#skF_11')),cons(int,t2tb1('#skF_3'('#skF_11')),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' )
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(resolution,[status(thm)],[c_131,c_15785]) ).
tff(c_15846,plain,
( ( tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11' )
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14983,c_14981,c_14982,c_15818]) ).
tff(c_15850,plain,
( ( tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_2634,c_15846]) ).
tff(c_16117,plain,
tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11',
inference(splitLeft,[status(thm)],[c_15850]) ).
tff(c_16588,plain,
cons(int,t2tb1('#skE_5'),nil(int)) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_16117,c_52]) ).
tff(c_661,plain,
! [A_92: ty,X_95: uni,X1_96: uni] : ( length1(A_92,cons(A_92,X_95,X1_96)) = $sum(1,length1(A_92,X1_96)) ),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_16618,plain,
length1(int,t2tb('#skF_11')) = $sum(1,length1(int,nil(int))),
inference(superposition,[status(thm),theory(equality)],[c_16588,c_661]) ).
tff(c_16668,plain,
'#skE_1' = $sum(1,0),
inference(demodulation,[status(thm),theory(equality)],[c_658,c_11929,c_16618]) ).
tff(c_16670,plain,
'#skE_1' = 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_16668]) ).
tff(c_16689,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11975,c_16670]) ).
tff(c_16862,plain,
tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11',
inference(splitRight,[status(thm)],[c_15850]) ).
tff(c_17859,plain,
cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11')))) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_16862,c_52]) ).
tff(c_11615,plain,
! [A_2074: ty,U_2075: uni,U1_2076: uni] :
( ( cons_proj_11(A_2074,cons(A_2074,U_2075,U1_2076)) = U_2075 )
| ~ sort1(A_2074,U_2075) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_11633,plain,
! [X_60a: $int,U1_2076: uni] : ( cons_proj_11(int,cons(int,t2tb1(X_60a),U1_2076)) = t2tb1(X_60a) ),
inference(resolution,[status(thm)],[c_674,c_11615]) ).
tff(c_18024,plain,
cons_proj_11(int,t2tb('#skF_11')) = t2tb1('#skE_4'),
inference(superposition,[status(thm),theory(equality)],[c_17859,c_11633]) ).
tff(c_11720,plain,
cons_proj_11(int,t2tb('#skF_11')) = t2tb1('#skF_12'),
inference(superposition,[status(thm),theory(equality)],[c_11693,c_11633]) ).
tff(c_18172,plain,
t2tb1('#skF_12') = t2tb1('#skE_4'),
inference(superposition,[status(thm),theory(equality)],[c_18024,c_11720]) ).
tff(c_673,plain,
! [I_61a: $int] : ( tb2t1(t2tb1(I_61a)) = I_61a ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_18624,plain,
tb2t1(t2tb1('#skE_4')) = '#skF_12',
inference(superposition,[status(thm),theory(equality)],[c_18172,c_673]) ).
tff(c_18651,plain,
'#skF_12' = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_18624,c_673]) ).
tff(c_18702,plain,
'#skF_10' != '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_18651,c_2022]) ).
tff(c_3025,plain,
sorted1('#skF_13'),
inference(splitRight,[status(thm)],[c_2754]) ).
tff(c_555,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ( true1 = '#skF_16' )
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_11825,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ( true1 = '#skF_16' )
| ( tb2t(nil(int)) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3025,c_555]) ).
tff(c_11829,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_2695,c_11825]) ).
tff(c_11834,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(splitLeft,[status(thm)],[c_11829]) ).
tff(c_14275,plain,
! [A_2395: ty,X_2396: uni,X2_2397: uni,X1_2398: uni] :
( mem(A_2395,X_2396,X2_2397)
| ( X_2396 = X1_2398 )
| ~ mem(A_2395,X_2396,cons(A_2395,X1_2398,X2_2397))
| ~ sort1(A_2395,X1_2398)
| ~ sort1(A_2395,X_2396) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_14306,plain,
! [X_2396: uni] :
( mem(int,X_2396,t2tb('#skF_13'))
| ( t2tb1('#skF_12') = X_2396 )
| ~ mem(int,X_2396,t2tb('#skF_11'))
| ~ sort1(int,t2tb1('#skF_12'))
| ~ sort1(int,X_2396) ),
inference(superposition,[status(thm),theory(equality)],[c_3227,c_14275]) ).
tff(c_14636,plain,
! [X_2419: uni] :
( mem(int,X_2419,t2tb('#skF_13'))
| ( t2tb1('#skF_12') = X_2419 )
| ~ mem(int,X_2419,t2tb('#skF_11'))
| ~ sort1(int,X_2419) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_14306]) ).
tff(c_14650,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( t2tb1('#skF_12') = t2tb1('#skF_10') )
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(resolution,[status(thm)],[c_11834,c_14636]) ).
tff(c_14676,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( t2tb1('#skF_12') = t2tb1('#skF_10') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_14650]) ).
tff(c_26050,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( t2tb1('#skF_10') = t2tb1('#skE_4') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18651,c_14676]) ).
tff(c_26097,plain,
t2tb1('#skF_10') = t2tb1('#skE_4'),
inference(splitLeft,[status(thm)],[c_26050]) ).
tff(c_26630,plain,
tb2t1(t2tb1('#skE_4')) = '#skF_10',
inference(superposition,[status(thm),theory(equality)],[c_26097,c_673]) ).
tff(c_26657,plain,
'#skF_10' = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_26630,c_673]) ).
tff(c_26671,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18702,c_26657]) ).
tff(c_26677,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_13')),
inference(splitRight,[status(thm)],[c_26050]) ).
tff(c_3369,plain,
'#skF_15' != '#skF_13',
inference(splitLeft,[status(thm)],[c_3028]) ).
tff(c_3374,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_3206,c_52]) ).
tff(c_3413,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_13'),
inference(superposition,[status(thm),theory(equality)],[c_3374,c_36]) ).
tff(c_3425,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ( true1 = '#skF_16' )
| ( tb2t(nil(int)) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3025,c_555]) ).
tff(c_3429,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_2695,c_3425]) ).
tff(c_3434,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(splitLeft,[status(thm)],[c_3429]) ).
tff(c_3371,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_3206,c_52]) ).
tff(c_7231,plain,
! [X_1564a: $int,Y_1565a: $int,L_1566: list_int] :
( ~ mem(int,t2tb1(X_1564a),cons(int,t2tb1(Y_1565a),t2tb(L_1566)))
| ~ sorted1(tb2t(cons(int,t2tb1(Y_1565a),t2tb(L_1566))))
| ~ $less(X_1564a,Y_1565a) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_7241,plain,
! [X_1564a: $int] :
( ~ mem(int,t2tb1(X_1564a),t2tb('#skF_11'))
| ~ sorted1(tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))))
| ~ $less(X_1564a,'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_3227,c_7231]) ).
tff(c_7451,plain,
! [X_1631a: $int] :
( ~ mem(int,t2tb1(X_1631a),t2tb('#skF_11'))
| ~ $less(X_1631a,'#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_131,c_50,c_3371,c_7241]) ).
tff(c_7469,plain,
~ $less('#skF_10','#skF_12'),
inference(resolution,[status(thm)],[c_3434,c_7451]) ).
tff(c_368,plain,
( ( '#skF_15' != '#skF_13' )
| ( true1 = '#skF_16' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10')
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_3233,plain,
( ( '#skF_15' != '#skF_13' )
| ( true1 = '#skF_16' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10')
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3025,c_368]) ).
tff(c_3237,plain,
( ( '#skF_15' != '#skF_13' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ~ $less('#skF_12','#skF_10') ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_2695,c_3233]) ).
tff(c_3240,plain,
~ $less('#skF_12','#skF_10'),
inference(splitLeft,[status(thm)],[c_3237]) ).
tff(c_7470,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_7469,c_3240,c_2022]) ).
tff(c_7490,plain,
tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_3429]) ).
tff(c_7596,plain,
cons(int,t2tb1('#skF_14'),t2tb('#skF_15')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_7490,c_52]) ).
tff(c_7614,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_7596,c_36]) ).
tff(c_7641,plain,
t2tb('#skF_15') = t2tb('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_3413,c_7614]) ).
tff(c_7666,plain,
tb2t(t2tb('#skF_13')) = '#skF_15',
inference(superposition,[status(thm),theory(equality)],[c_7641,c_50]) ).
tff(c_7673,plain,
'#skF_15' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_50,c_7666]) ).
tff(c_7675,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3369,c_7673]) ).
tff(c_7680,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(splitRight,[status(thm)],[c_3028]) ).
tff(c_11395,plain,
! [X_2043a: $int,Y_2044a: $int,L_2045: list_int] :
( ~ mem(int,t2tb1(X_2043a),cons(int,t2tb1(Y_2044a),t2tb(L_2045)))
| ~ sorted1(tb2t(cons(int,t2tb1(Y_2044a),t2tb(L_2045))))
| ~ $less(X_2043a,Y_2044a) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_11405,plain,
! [X_2043a: $int] :
( ~ mem(int,t2tb1(X_2043a),t2tb('#skF_11'))
| ~ sorted1(tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))))
| ~ $less(X_2043a,'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_3227,c_11395]) ).
tff(c_11534,plain,
! [X_2056a: $int] :
( ~ mem(int,t2tb1(X_2056a),t2tb('#skF_11'))
| ~ $less(X_2056a,'#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_131,c_50,c_3371,c_11405]) ).
tff(c_11552,plain,
~ $less('#skF_10','#skF_12'),
inference(resolution,[status(thm)],[c_7680,c_11534]) ).
tff(c_11553,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_11552,c_3240,c_2022]) ).
tff(c_11559,plain,
$less('#skF_12','#skF_10'),
inference(splitRight,[status(thm)],[c_3237]) ).
tff(c_353,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ( true1 = '#skF_16' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10')
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_12329,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ( true1 = '#skF_16' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( tb2t(nil(int)) = '#skF_11' )
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11559,c_3025,c_353]) ).
tff(c_12333,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13')) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_2695,c_12329]) ).
tff(c_12338,plain,
~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13')),
inference(splitLeft,[status(thm)],[c_12333]) ).
tff(c_26680,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26677,c_12338]) ).
tff(c_26700,plain,
tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_12333]) ).
tff(c_26736,plain,
cons(int,t2tb1('#skF_14'),t2tb('#skF_15')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_26700,c_52]) ).
tff(c_26763,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_26736,c_36]) ).
tff(c_26799,plain,
t2tb('#skF_15') = t2tb('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_11732,c_26763]) ).
tff(c_26828,plain,
tb2t(t2tb('#skF_13')) = '#skF_15',
inference(superposition,[status(thm),theory(equality)],[c_26799,c_50]) ).
tff(c_26835,plain,
'#skF_15' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_50,c_26828]) ).
tff(c_26837,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11685,c_26835]) ).
tff(c_26838,plain,
t2tb('#skF_13') = nil(int),
inference(splitRight,[status(thm)],[c_11973]) ).
tff(c_26872,plain,
tb2t(nil(int)) = '#skF_13',
inference(superposition,[status(thm),theory(equality)],[c_26838,c_50]) ).
tff(c_26851,plain,
cons_proj_21(int,t2tb('#skF_11')) = nil(int),
inference(demodulation,[status(thm),theory(equality)],[c_26838,c_11732]) ).
tff(c_26880,plain,
'#skF_11' != '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_26872,c_2634]) ).
tff(c_667,plain,
! [Z_67: list_int] :
( ~ $less('#skF_3'(Z_67),'#skF_2'(Z_67))
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_67)),nil(int))) = Z_67 )
| ( tb2t(nil(int)) = Z_67 )
| ~ sorted1(Z_67) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_70]) ).
tff(c_31145,plain,
! [Z_4058: list_int] :
( ~ $less('#skF_3'(Z_4058),'#skF_2'(Z_4058))
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_4058)),nil(int))) = Z_4058 )
| ( Z_4058 = '#skF_13' )
| ~ sorted1(Z_4058) ),
inference(demodulation,[status(thm),theory(equality)],[c_26872,c_667]) ).
tff(c_31205,plain,
( ~ $less('#skF_3'('#skF_11'),'#skF_2'('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' )
| ( '#skF_11' = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_131,c_31145]) ).
tff(c_31249,plain,
( ~ $less('#skF_3'('#skF_11'),'#skF_2'('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_26880,c_31205]) ).
tff(c_31459,plain,
'#skF_1'('#skF_11') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_31249]) ).
tff(c_31457,plain,
'#skF_3'('#skF_11') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_31249]) ).
tff(c_31458,plain,
'#skF_2'('#skF_11') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_31249]) ).
tff(c_669,plain,
! [Z_67: list_int] :
( ( tb2t(cons(int,t2tb1('#skF_2'(Z_67)),cons(int,t2tb1('#skF_3'(Z_67)),t2tb('#skF_4'(Z_67))))) = Z_67 )
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_67)),nil(int))) = Z_67 )
| ( tb2t(nil(int)) = Z_67 )
| ~ sorted1(Z_67) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_46413,plain,
! [Z_5068: list_int] :
( ( tb2t(cons(int,t2tb1('#skF_2'(Z_5068)),cons(int,t2tb1('#skF_3'(Z_5068)),t2tb('#skF_4'(Z_5068))))) = Z_5068 )
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_5068)),nil(int))) = Z_5068 )
| ( Z_5068 = '#skF_13' )
| ~ sorted1(Z_5068) ),
inference(demodulation,[status(thm),theory(equality)],[c_26872,c_669]) ).
tff(c_46500,plain,
( ( tb2t(cons(int,t2tb1('#skF_2'('#skF_11')),cons(int,t2tb1('#skF_3'('#skF_11')),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' )
| ( '#skF_11' = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_131,c_46413]) ).
tff(c_46561,plain,
( ( tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11' )
| ( '#skF_11' = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_31459,c_31457,c_31458,c_46500]) ).
tff(c_46565,plain,
( ( tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_26880,c_46561]) ).
tff(c_46574,plain,
tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11',
inference(splitLeft,[status(thm)],[c_46565]) ).
tff(c_46683,plain,
cons(int,t2tb1('#skE_5'),nil(int)) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_46574,c_52]) ).
tff(c_46831,plain,
cons_proj_11(int,t2tb('#skF_11')) = t2tb1('#skE_5'),
inference(superposition,[status(thm),theory(equality)],[c_46683,c_11633]) ).
tff(c_47068,plain,
t2tb1('#skF_12') = t2tb1('#skE_5'),
inference(superposition,[status(thm),theory(equality)],[c_46831,c_11720]) ).
tff(c_47553,plain,
tb2t1(t2tb1('#skE_5')) = '#skF_12',
inference(superposition,[status(thm),theory(equality)],[c_47068,c_673]) ).
tff(c_47580,plain,
'#skF_12' = '#skE_5',
inference(superposition,[status(thm),theory(equality)],[c_47553,c_673]) ).
tff(c_47607,plain,
'#skF_10' != '#skE_5',
inference(demodulation,[status(thm),theory(equality)],[c_47580,c_2022]) ).
tff(c_11734,plain,
t2tb('#skF_11') != nil(int),
inference(superposition,[status(thm),theory(equality)],[c_11693,c_28]) ).
tff(c_46830,plain,
cons_proj_11(int,t2tb('#skF_11')) = t2tb1('#skE_5'),
inference(superposition,[status(thm),theory(equality)],[c_46683,c_11633]) ).
tff(c_30,plain,
! [A_39: ty,X_40: uni] : sort1(A_39,cons_proj_11(A_39,X_40)),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_38,plain,
! [A_49: ty,U_50: uni] :
( ( cons(A_49,cons_proj_11(A_49,U_50),cons_proj_21(A_49,U_50)) = U_50 )
| ( nil(A_49) = U_50 ) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_30308,plain,
! [A_4031: ty,X_4032: uni,X2_4033: uni,X1_4034: uni] :
( mem(A_4031,X_4032,X2_4033)
| ( X_4032 = X1_4034 )
| ~ mem(A_4031,X_4032,cons(A_4031,X1_4034,X2_4033))
| ~ sort1(A_4031,X1_4034)
| ~ sort1(A_4031,X_4032) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_30336,plain,
! [A_49: ty,X_4032: uni,U_50: uni] :
( mem(A_49,X_4032,cons_proj_21(A_49,U_50))
| ( cons_proj_11(A_49,U_50) = X_4032 )
| ~ mem(A_49,X_4032,U_50)
| ~ sort1(A_49,cons_proj_11(A_49,U_50))
| ~ sort1(A_49,X_4032)
| ( nil(A_49) = U_50 ) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_30308]) ).
tff(c_56517,plain,
! [A_5772: ty,X_5773: uni,U_5774: uni] :
( mem(A_5772,X_5773,cons_proj_21(A_5772,U_5774))
| ( cons_proj_11(A_5772,U_5774) = X_5773 )
| ~ mem(A_5772,X_5773,U_5774)
| ~ sort1(A_5772,X_5773)
| ( nil(A_5772) = U_5774 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_30,c_30336]) ).
tff(c_56530,plain,
! [X_5773: uni] :
( mem(int,X_5773,nil(int))
| ( cons_proj_11(int,t2tb('#skF_11')) = X_5773 )
| ~ mem(int,X_5773,t2tb('#skF_11'))
| ~ sort1(int,X_5773)
| ( t2tb('#skF_11') = nil(int) ) ),
inference(superposition,[status(thm),theory(equality)],[c_26851,c_56517]) ).
tff(c_56541,plain,
! [X_5773: uni] :
( mem(int,X_5773,nil(int))
| ( t2tb1('#skE_5') = X_5773 )
| ~ mem(int,X_5773,t2tb('#skF_11'))
| ~ sort1(int,X_5773)
| ( t2tb('#skF_11') = nil(int) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_46830,c_56530]) ).
tff(c_56733,plain,
! [X_5779: uni] :
( mem(int,X_5779,nil(int))
| ( t2tb1('#skE_5') = X_5779 )
| ~ mem(int,X_5779,t2tb('#skF_11'))
| ~ sort1(int,X_5779) ),
inference(negUnitSimplification,[status(thm)],[c_11734,c_56541]) ).
tff(c_56759,plain,
( mem(int,t2tb1('#skF_10'),nil(int))
| ( t2tb1('#skF_10') = t2tb1('#skE_5') )
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(resolution,[status(thm)],[c_11834,c_56733]) ).
tff(c_56809,plain,
( mem(int,t2tb1('#skF_10'),nil(int))
| ( t2tb1('#skF_10') = t2tb1('#skE_5') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_56759]) ).
tff(c_57283,plain,
t2tb1('#skF_10') = t2tb1('#skE_5'),
inference(splitLeft,[status(thm)],[c_56809]) ).
tff(c_57789,plain,
tb2t1(t2tb1('#skE_5')) = '#skF_10',
inference(superposition,[status(thm),theory(equality)],[c_57283,c_673]) ).
tff(c_57816,plain,
'#skF_10' = '#skE_5',
inference(superposition,[status(thm),theory(equality)],[c_57789,c_673]) ).
tff(c_57830,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_47607,c_57816]) ).
tff(c_57836,plain,
mem(int,t2tb1('#skF_10'),nil(int)),
inference(splitRight,[status(thm)],[c_56809]) ).
tff(c_26933,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ( true1 = '#skF_16' )
| ~ mem(int,t2tb1('#skF_10'),nil(int))
| ( '#skF_11' = '#skF_13' )
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11559,c_26872,c_3025,c_26838,c_353]) ).
tff(c_26937,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),nil(int)) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_26880,c_2695,c_26933]) ).
tff(c_26942,plain,
~ mem(int,t2tb1('#skF_10'),nil(int)),
inference(splitLeft,[status(thm)],[c_26937]) ).
tff(c_57839,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_57836,c_26942]) ).
tff(c_58042,plain,
tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11',
inference(splitRight,[status(thm)],[c_46565]) ).
tff(c_58750,plain,
cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11')))) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_58042,c_52]) ).
tff(c_58810,plain,
cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))) = cons_proj_21(int,t2tb('#skF_11')),
inference(superposition,[status(thm),theory(equality)],[c_58750,c_36]) ).
tff(c_58894,plain,
cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))) = nil(int),
inference(demodulation,[status(thm),theory(equality)],[c_26851,c_58810]) ).
tff(c_58898,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_58894]) ).
tff(c_59119,plain,
tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_26937]) ).
tff(c_59155,plain,
cons(int,t2tb1('#skF_14'),t2tb('#skF_15')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_59119,c_52]) ).
tff(c_59179,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_59155,c_36]) ).
tff(c_59213,plain,
t2tb('#skF_15') = nil(int),
inference(demodulation,[status(thm),theory(equality)],[c_26851,c_59179]) ).
tff(c_59270,plain,
tb2t(nil(int)) = '#skF_15',
inference(superposition,[status(thm),theory(equality)],[c_59213,c_50]) ).
tff(c_59277,plain,
'#skF_15' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_26872,c_59270]) ).
tff(c_59279,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11685,c_59277]) ).
tff(c_59286,plain,
tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_11829]) ).
tff(c_59326,plain,
cons(int,t2tb1('#skF_14'),t2tb('#skF_15')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_59286,c_52]) ).
tff(c_59344,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_59326,c_36]) ).
tff(c_59371,plain,
t2tb('#skF_15') = t2tb('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_11732,c_59344]) ).
tff(c_59396,plain,
tb2t(t2tb('#skF_13')) = '#skF_15',
inference(superposition,[status(thm),theory(equality)],[c_59371,c_50]) ).
tff(c_59403,plain,
'#skF_15' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_50,c_59396]) ).
tff(c_59405,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11685,c_59403]) ).
tff(c_59410,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(splitRight,[status(thm)],[c_3028]) ).
tff(c_59441,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_3206,c_52]) ).
tff(c_59474,plain,
cons_proj_11(int,t2tb('#skF_11')) = t2tb1('#skF_12'),
inference(superposition,[status(thm),theory(equality)],[c_59441,c_11633]) ).
tff(c_59698,plain,
! [A_6098: ty,X_6099: uni,X1_6100: uni] : ( length1(A_6098,cons(A_6098,X_6099,X1_6100)) = $sum(1,length1(A_6098,X1_6100)) ),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_59723,plain,
length1(int,t2tb('#skF_11')) = $sum(1,length1(int,t2tb('#skF_13'))),
inference(superposition,[status(thm),theory(equality)],[c_3227,c_59698]) ).
tff(c_59729,plain,
length1(int,t2tb('#skF_13')) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_59723]) ).
tff(c_59728,plain,
length1(int,t2tb('#skF_11')) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_59723]) ).
tff(c_59731,plain,
$sum(1,'#skE_2') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_59729,c_59728,c_59723]) ).
tff(c_59735,plain,
'#skE_2' = $sum($uminus(1),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_59731]) ).
tff(c_59733,plain,
length1(int,t2tb('#skF_13')) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_59723]) ).
tff(c_59759,plain,
( ( t2tb('#skF_13') = nil(int) )
| ( '#skE_2' != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_59733,c_659]) ).
tff(c_59774,plain,
( ( t2tb('#skF_13') = nil(int) )
| ( $sum($uminus(1),'#skE_1') != 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_59735,c_59759]) ).
tff(c_59776,plain,
( ( t2tb('#skF_13') = nil(int) )
| ( '#skE_1' != 1 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_59774]) ).
tff(c_59778,plain,
'#skE_1' != 1,
inference(splitLeft,[status(thm)],[c_59776]) ).
tff(c_59732,plain,
length1(int,t2tb('#skF_11')) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_59723]) ).
tff(c_62629,plain,
! [Z_6403: list_int] :
( ~ $less('#skF_3'(Z_6403),'#skF_2'(Z_6403))
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_6403)),nil(int))) = Z_6403 )
| ( tb2t(nil(int)) = Z_6403 )
| ~ sorted1(Z_6403) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_70]) ).
tff(c_62650,plain,
( ~ $less('#skF_3'('#skF_11'),'#skF_2'('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' )
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(resolution,[status(thm)],[c_131,c_62629]) ).
tff(c_62667,plain,
( ~ $less('#skF_3'('#skF_11'),'#skF_2'('#skF_11'))
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_2634,c_62650]) ).
tff(c_62915,plain,
'#skF_1'('#skF_11') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_62667]) ).
tff(c_62913,plain,
'#skF_3'('#skF_11') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_62667]) ).
tff(c_62914,plain,
'#skF_2'('#skF_11') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_62667]) ).
tff(c_63827,plain,
! [Z_6520: list_int] :
( ( tb2t(cons(int,t2tb1('#skF_2'(Z_6520)),cons(int,t2tb1('#skF_3'(Z_6520)),t2tb('#skF_4'(Z_6520))))) = Z_6520 )
| ( tb2t(cons(int,t2tb1('#skF_1'(Z_6520)),nil(int))) = Z_6520 )
| ( tb2t(nil(int)) = Z_6520 )
| ~ sorted1(Z_6520) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_63857,plain,
( ( tb2t(cons(int,t2tb1('#skF_2'('#skF_11')),cons(int,t2tb1('#skF_3'('#skF_11')),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skF_1'('#skF_11')),nil(int))) = '#skF_11' )
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(resolution,[status(thm)],[c_131,c_63827]) ).
tff(c_63883,plain,
( ( tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11' )
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_62915,c_62913,c_62914,c_63857]) ).
tff(c_63887,plain,
( ( tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11' )
| ( tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11' ) ),
inference(negUnitSimplification,[status(thm)],[c_2634,c_63883]) ).
tff(c_63946,plain,
tb2t(cons(int,t2tb1('#skE_5'),nil(int))) = '#skF_11',
inference(splitLeft,[status(thm)],[c_63887]) ).
tff(c_64071,plain,
cons(int,t2tb1('#skE_5'),nil(int)) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_63946,c_52]) ).
tff(c_64110,plain,
length1(int,t2tb('#skF_11')) = $sum(1,length1(int,nil(int))),
inference(superposition,[status(thm),theory(equality)],[c_64071,c_661]) ).
tff(c_64174,plain,
'#skE_1' = $sum(1,0),
inference(demodulation,[status(thm),theory(equality)],[c_658,c_59732,c_64110]) ).
tff(c_64176,plain,
'#skE_1' = 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_64174]) ).
tff(c_64195,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_59778,c_64176]) ).
tff(c_64236,plain,
tb2t(cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11'))))) = '#skF_11',
inference(splitRight,[status(thm)],[c_63887]) ).
tff(c_64600,plain,
cons(int,t2tb1('#skE_4'),cons(int,t2tb1('#skE_3'),t2tb('#skF_4'('#skF_11')))) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_64236,c_52]) ).
tff(c_64781,plain,
cons_proj_11(int,t2tb('#skF_11')) = t2tb1('#skE_4'),
inference(superposition,[status(thm),theory(equality)],[c_64600,c_11633]) ).
tff(c_65166,plain,
t2tb1('#skF_12') = t2tb1('#skE_4'),
inference(superposition,[status(thm),theory(equality)],[c_59474,c_64781]) ).
tff(c_65618,plain,
tb2t1(t2tb1('#skE_4')) = '#skF_12',
inference(superposition,[status(thm),theory(equality)],[c_65166,c_673]) ).
tff(c_65645,plain,
'#skF_12' = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_65618,c_673]) ).
tff(c_65696,plain,
'#skF_10' != '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_65645,c_2022]) ).
tff(c_61849,plain,
! [A_6341: ty,X_6342: uni,X2_6343: uni,X1_6344: uni] :
( mem(A_6341,X_6342,X2_6343)
| ( X_6342 = X1_6344 )
| ~ mem(A_6341,X_6342,cons(A_6341,X1_6344,X2_6343))
| ~ sort1(A_6341,X1_6344)
| ~ sort1(A_6341,X_6342) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_61877,plain,
! [X_6342: uni] :
( mem(int,X_6342,t2tb('#skF_13'))
| ( t2tb1('#skF_12') = X_6342 )
| ~ mem(int,X_6342,t2tb('#skF_11'))
| ~ sort1(int,t2tb1('#skF_12'))
| ~ sort1(int,X_6342) ),
inference(superposition,[status(thm),theory(equality)],[c_3227,c_61849]) ).
tff(c_61994,plain,
! [X_6352: uni] :
( mem(int,X_6352,t2tb('#skF_13'))
| ( t2tb1('#skF_12') = X_6352 )
| ~ mem(int,X_6352,t2tb('#skF_11'))
| ~ sort1(int,X_6352) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_61877]) ).
tff(c_62011,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( t2tb1('#skF_12') = t2tb1('#skF_10') )
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(resolution,[status(thm)],[c_59410,c_61994]) ).
tff(c_62040,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( t2tb1('#skF_12') = t2tb1('#skF_10') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_62011]) ).
tff(c_73899,plain,
( mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( t2tb1('#skF_10') = t2tb1('#skE_4') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_65645,c_62040]) ).
tff(c_73946,plain,
t2tb1('#skF_10') = t2tb1('#skE_4'),
inference(splitLeft,[status(thm)],[c_73899]) ).
tff(c_74479,plain,
tb2t1(t2tb1('#skE_4')) = '#skF_10',
inference(superposition,[status(thm),theory(equality)],[c_73946,c_673]) ).
tff(c_74506,plain,
'#skF_10' = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_74479,c_673]) ).
tff(c_74520,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65696,c_74506]) ).
tff(c_74526,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_13')),
inference(splitRight,[status(thm)],[c_73899]) ).
tff(c_59407,plain,
'#skF_15' = '#skF_13',
inference(splitRight,[status(thm)],[c_3028]) ).
tff(c_11558,plain,
( ( '#skF_15' != '#skF_13' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13')) ),
inference(splitRight,[status(thm)],[c_3237]) ).
tff(c_59423,plain,
~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13')),
inference(demodulation,[status(thm),theory(equality)],[c_59407,c_11558]) ).
tff(c_74529,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_74526,c_59423]) ).
tff(c_74530,plain,
t2tb('#skF_13') = nil(int),
inference(splitRight,[status(thm)],[c_59776]) ).
tff(c_74618,plain,
cons(int,t2tb1('#skF_12'),nil(int)) = t2tb('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_74530,c_3227]) ).
tff(c_78106,plain,
! [A_7951: ty,X_7952: uni,X2_7953: uni,X1_7954: uni] :
( mem(A_7951,X_7952,X2_7953)
| ( X_7952 = X1_7954 )
| ~ mem(A_7951,X_7952,cons(A_7951,X1_7954,X2_7953))
| ~ sort1(A_7951,X1_7954)
| ~ sort1(A_7951,X_7952) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_78124,plain,
! [X_7952: uni] :
( mem(int,X_7952,nil(int))
| ( t2tb1('#skF_12') = X_7952 )
| ~ mem(int,X_7952,t2tb('#skF_11'))
| ~ sort1(int,t2tb1('#skF_12'))
| ~ sort1(int,X_7952) ),
inference(superposition,[status(thm),theory(equality)],[c_74618,c_78106]) ).
tff(c_78295,plain,
! [X_7959: uni] :
( mem(int,X_7959,nil(int))
| ( t2tb1('#skF_12') = X_7959 )
| ~ mem(int,X_7959,t2tb('#skF_11'))
| ~ sort1(int,X_7959) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_78124]) ).
tff(c_78309,plain,
( mem(int,t2tb1('#skF_10'),nil(int))
| ( t2tb1('#skF_12') = t2tb1('#skF_10') )
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(resolution,[status(thm)],[c_59410,c_78295]) ).
tff(c_78336,plain,
( mem(int,t2tb1('#skF_10'),nil(int))
| ( t2tb1('#skF_12') = t2tb1('#skF_10') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_78309]) ).
tff(c_79429,plain,
t2tb1('#skF_12') = t2tb1('#skF_10'),
inference(splitLeft,[status(thm)],[c_78336]) ).
tff(c_79771,plain,
tb2t1(t2tb1('#skF_10')) = '#skF_12',
inference(superposition,[status(thm),theory(equality)],[c_79429,c_673]) ).
tff(c_79798,plain,
'#skF_12' = '#skF_10',
inference(superposition,[status(thm),theory(equality)],[c_79771,c_673]) ).
tff(c_79812,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2022,c_79798]) ).
tff(c_79818,plain,
mem(int,t2tb1('#skF_10'),nil(int)),
inference(splitRight,[status(thm)],[c_78336]) ).
tff(c_74621,plain,
~ mem(int,t2tb1('#skF_10'),nil(int)),
inference(demodulation,[status(thm),theory(equality)],[c_74530,c_59423]) ).
tff(c_79821,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_79818,c_74621]) ).
tff(c_79831,plain,
! [U_8065: bool1] :
( ( false1 = U_8065 )
| ( U_8065 = '#skF_16' ) ),
inference(splitRight,[status(thm)],[c_775]) ).
tff(c_79847,plain,
true1 = '#skF_16',
inference(superposition,[status(thm),theory(equality)],[c_79831,c_10]) ).
tff(c_478,plain,
( ( '#skF_15' != '#skF_13' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( true1 != '#skF_16' )
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_80061,plain,
( ( '#skF_15' != '#skF_13' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10') ),
inference(demodulation,[status(thm),theory(equality)],[c_79847,c_478]) ).
tff(c_80065,plain,
( ( '#skF_15' != '#skF_13' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ~ sorted1('#skF_13')
| ~ $less('#skF_12','#skF_10') ),
inference(negUnitSimplification,[status(thm)],[c_2634,c_80061]) ).
tff(c_80068,plain,
~ $less('#skF_12','#skF_10'),
inference(splitLeft,[status(thm)],[c_80065]) ).
tff(c_2021,plain,
( $less('#skF_12','#skF_10')
| mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(splitRight,[status(thm)],[c_489]) ).
tff(c_80411,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(negUnitSimplification,[status(thm)],[c_80068,c_2021]) ).
tff(c_80139,plain,
tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_294]) ).
tff(c_80225,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_80139,c_52]) ).
tff(c_80154,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_80139,c_52]) ).
tff(c_84144,plain,
! [X_8601a: $int,Y_8602a: $int,L_8603: list_int] :
( ~ mem(int,t2tb1(X_8601a),cons(int,t2tb1(Y_8602a),t2tb(L_8603)))
| ~ sorted1(tb2t(cons(int,t2tb1(Y_8602a),t2tb(L_8603))))
| ~ $less(X_8601a,Y_8602a) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_84154,plain,
! [X_8601a: $int] :
( ~ mem(int,t2tb1(X_8601a),t2tb('#skF_11'))
| ~ sorted1(tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))))
| ~ $less(X_8601a,'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_80154,c_84144]) ).
tff(c_84179,plain,
! [X_8604a: $int] :
( ~ mem(int,t2tb1(X_8604a),t2tb('#skF_11'))
| ~ $less(X_8604a,'#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_131,c_50,c_80225,c_84154]) ).
tff(c_84194,plain,
~ $less('#skF_10','#skF_12'),
inference(resolution,[status(thm)],[c_80411,c_84179]) ).
tff(c_84198,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_84194,c_80068,c_2022]) ).
tff(c_84204,plain,
$less('#skF_12','#skF_10'),
inference(splitRight,[status(thm)],[c_80065]) ).
tff(c_2637,plain,
tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_294]) ).
tff(c_84350,plain,
! [L_8634: list_int,X_8635a: $int] :
( sorted1(L_8634)
| ~ sorted1(tb2t(cons(int,t2tb1(X_8635a),t2tb(L_8634)))) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_84353,plain,
( sorted1('#skF_13')
| ~ sorted1('#skF_11') ),
inference(superposition,[status(thm),theory(equality)],[c_2637,c_84350]) ).
tff(c_84359,plain,
sorted1('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_131,c_84353]) ).
tff(c_338,plain,
( ( '#skF_15' != '#skF_13' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( true1 != '#skF_16' )
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10')
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_84413,plain,
( ( '#skF_15' != '#skF_13' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( tb2t(nil(int)) = '#skF_11' )
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_84204,c_84359,c_79847,c_338]) ).
tff(c_84417,plain,
( ( '#skF_15' != '#skF_13' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_13')) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_84413]) ).
tff(c_84419,plain,
'#skF_15' != '#skF_13',
inference(splitLeft,[status(thm)],[c_84417]) ).
tff(c_84275,plain,
tb2t(cons(int,t2tb1('#skF_12'),t2tb('#skF_13'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_294]) ).
tff(c_84366,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_84275,c_52]) ).
tff(c_84405,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_13'),
inference(superposition,[status(thm),theory(equality)],[c_84366,c_36]) ).
tff(c_323,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( true1 != '#skF_16' )
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10')
| ( '#skF_12' = '#skF_10' ) ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_85253,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ( tb2t(nil(int)) = '#skF_11' )
| ( '#skF_12' = '#skF_10' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_84204,c_84359,c_79847,c_323]) ).
tff(c_85257,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| mem(int,t2tb1('#skF_10'),t2tb('#skF_13')) ),
inference(negUnitSimplification,[status(thm)],[c_2022,c_2634,c_85253]) ).
tff(c_85264,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_13')),
inference(splitLeft,[status(thm)],[c_85257]) ).
tff(c_84290,plain,
cons(int,t2tb1('#skF_12'),t2tb('#skF_13')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_84275,c_52]) ).
tff(c_85996,plain,
! [A_8844: ty,X_8845: uni,X2_8846: uni,X1_8847: uni] :
( ~ mem(A_8844,X_8845,X2_8846)
| mem(A_8844,X_8845,cons(A_8844,X1_8847,X2_8846))
| ~ sort1(A_8844,X1_8847)
| ~ sort1(A_8844,X_8845) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_86002,plain,
! [X_8845: uni] :
( ~ mem(int,X_8845,t2tb('#skF_13'))
| mem(int,X_8845,t2tb('#skF_11'))
| ~ sort1(int,t2tb1('#skF_12'))
| ~ sort1(int,X_8845) ),
inference(superposition,[status(thm),theory(equality)],[c_84290,c_85996]) ).
tff(c_86086,plain,
! [X_8857: uni] :
( ~ mem(int,X_8857,t2tb('#skF_13'))
| mem(int,X_8857,t2tb('#skF_11'))
| ~ sort1(int,X_8857) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_86002]) ).
tff(c_464,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( true1 != '#skF_16' )
| ~ sorted1('#skF_13')
| ( tb2t(nil(int)) = '#skF_11' )
| ~ $less('#skF_12','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_84638,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11'))
| ( tb2t(nil(int)) = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_84204,c_84359,c_79847,c_464]) ).
tff(c_84642,plain,
( ( tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(negUnitSimplification,[status(thm)],[c_2634,c_84638]) ).
tff(c_84647,plain,
~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(splitLeft,[status(thm)],[c_84642]) ).
tff(c_86093,plain,
( ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(resolution,[status(thm)],[c_86086,c_84647]) ).
tff(c_86101,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_674,c_85264,c_86093]) ).
tff(c_86267,plain,
tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_85257]) ).
tff(c_86404,plain,
cons(int,t2tb1('#skF_14'),t2tb('#skF_15')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_86267,c_52]) ).
tff(c_86431,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_86404,c_36]) ).
tff(c_86468,plain,
t2tb('#skF_15') = t2tb('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_84405,c_86431]) ).
tff(c_86493,plain,
tb2t(t2tb('#skF_13')) = '#skF_15',
inference(superposition,[status(thm),theory(equality)],[c_86468,c_50]) ).
tff(c_86500,plain,
'#skF_15' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_50,c_86493]) ).
tff(c_86502,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_84419,c_86500]) ).
tff(c_86617,plain,
tb2t(cons(int,t2tb1('#skF_14'),t2tb('#skF_15'))) = '#skF_11',
inference(splitRight,[status(thm)],[c_84642]) ).
tff(c_86653,plain,
cons(int,t2tb1('#skF_14'),t2tb('#skF_15')) = t2tb('#skF_11'),
inference(superposition,[status(thm),theory(equality)],[c_86617,c_52]) ).
tff(c_86674,plain,
cons_proj_21(int,t2tb('#skF_11')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_86653,c_36]) ).
tff(c_86705,plain,
t2tb('#skF_15') = t2tb('#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_84405,c_86674]) ).
tff(c_86792,plain,
tb2t(t2tb('#skF_13')) = '#skF_15',
inference(superposition,[status(thm),theory(equality)],[c_86705,c_50]) ).
tff(c_86799,plain,
'#skF_15' = '#skF_13',
inference(demodulation,[status(thm),theory(equality)],[c_50,c_86792]) ).
tff(c_86801,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_84419,c_86799]) ).
tff(c_86828,plain,
mem(int,t2tb1('#skF_10'),t2tb('#skF_13')),
inference(splitRight,[status(thm)],[c_84417]) ).
tff(c_91523,plain,
! [A_9492: ty,X_9493: uni,X2_9494: uni,X1_9495: uni] :
( ~ mem(A_9492,X_9493,X2_9494)
| mem(A_9492,X_9493,cons(A_9492,X1_9495,X2_9494))
| ~ sort1(A_9492,X1_9495)
| ~ sort1(A_9492,X_9493) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_91529,plain,
! [X_9493: uni] :
( ~ mem(int,X_9493,t2tb('#skF_13'))
| mem(int,X_9493,t2tb('#skF_11'))
| ~ sort1(int,t2tb1('#skF_12'))
| ~ sort1(int,X_9493) ),
inference(superposition,[status(thm),theory(equality)],[c_84290,c_91523]) ).
tff(c_91637,plain,
! [X_9504: uni] :
( ~ mem(int,X_9504,t2tb('#skF_13'))
| mem(int,X_9504,t2tb('#skF_11'))
| ~ sort1(int,X_9504) ),
inference(demodulation,[status(thm),theory(equality)],[c_674,c_91529]) ).
tff(c_86803,plain,
'#skF_15' = '#skF_13',
inference(splitRight,[status(thm)],[c_84417]) ).
tff(c_84203,plain,
( ~ sorted1('#skF_13')
| ( '#skF_15' != '#skF_13' )
| ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11')) ),
inference(splitRight,[status(thm)],[c_80065]) ).
tff(c_90712,plain,
~ mem(int,t2tb1('#skF_10'),t2tb('#skF_11')),
inference(demodulation,[status(thm),theory(equality)],[c_86803,c_84359,c_84203]) ).
tff(c_91644,plain,
( ~ mem(int,t2tb1('#skF_10'),t2tb('#skF_13'))
| ~ sort1(int,t2tb1('#skF_10')) ),
inference(resolution,[status(thm)],[c_91637,c_90712]) ).
tff(c_91652,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_674,c_86828,c_91644]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW643_2 : TPTP v9.0.0. Released v6.1.0.
% 0.11/0.13 % 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.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Apr 9 06:20:23 EDT 2025
% 0.12/0.33 % CPUTime :
% 29.80/10.70 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.80/10.75
% 29.80/10.75 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------