%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW637_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 : n014.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 : Timeout 290.11s 217.49s
% Output : None
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 116 ( 61 unt; 0 typ; 0 def)
% Number of atoms : 241 ( 11 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 215 ( 90 ~; 99 |; 13 &)
% ( 1 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 89 ( 75 atm; 0 fun; 0 num; 14 var)
% Number of types : 10 ( 8 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 73 ( 73 usr; 32 con; 0-5 aty)
% Number of variables : 84 ( 84 !; 0 ?; 84 :)
% Comments :
%------------------------------------------------------------------------------
%$ same_shape > mem > sort > distinct > match_tree > match_list > match_bool > node > infix_plpl > cons > node_proj_2 > node_proj_1 > mk_ref > length > leaf_proj_1 > leaf > labels > contents > cons_proj_2 > cons_proj_1 > #nlpp > witness > tree > tb2t3 > tb2t2 > tb2t1 > tb2t > t2tb3 > t2tb2 > t2tb1 > t2tb > ref > nil > list > tuple02 > tuple01 > true > real > qtmark > int > false > bool1 > a1 > #skF_14 > #skF_11 > #skF_8 > #skF_9 > #skF_12 > #skF_10 > #skF_7 > #skF_4 > #skF_6 > #skF_19 > #skF_1 > #skF_5 > #skF_3 > #skF_17 > #skF_15 > #skF_2
%Foreground sorts:
tff(tree_int,type,
tree_int: $tType ).
tff(tree_a1,type,
tree_a1: $tType ).
tff(list_int,type,
list_int: $tType ).
tff(bool,type,
bool: $tType ).
tff(tuple0,type,
tuple0: $tType ).
tff(a,type,
a: $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('#skE_12',type,
'#skE_12': $int ).
tff('#skF_13',type,
'#skF_13': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skF_16',type,
'#skF_16': $int ).
tff('#skF_20',type,
'#skF_20': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skF_18',type,
'#skF_18': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
%Foreground operators:
tff(list,type,
list: ty > ty ).
tff(t2tb,type,
t2tb: tree_int > uni ).
tff(tb2t1,type,
tb2t1: uni > list_int ).
tff(leaf_proj_1,type,
leaf_proj_1: ( ty * uni ) > uni ).
tff(cons_proj_1,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(cons,type,
cons: ( ty * uni * uni ) > uni ).
tff(nil,type,
nil: ty > uni ).
tff(labels,type,
labels: ( ty * uni ) > uni ).
tff(tuple02,type,
tuple02: tuple0 ).
tff(same_shape,type,
same_shape: ( ty * ty * uni * uni ) > $o ).
tff(t2tb2,type,
t2tb2: tree_a1 > uni ).
tff(t2tb3,type,
t2tb3: $int > uni ).
tff('#skF_14',type,
'#skF_14': tree_a1 ).
tff(tuple01,type,
tuple01: ty ).
tff(a1,type,
a1: ty ).
tff(int,type,
int: ty ).
tff('#skF_11',type,
'#skF_11': ( ty * ty * uni * uni ) > uni ).
tff('#skF_8',type,
'#skF_8': ( ty * ty * uni * uni ) > uni ).
tff(contents,type,
contents: ( ty * uni ) > uni ).
tff(node_proj_1,type,
node_proj_1: ( ty * uni ) > uni ).
tff('#skF_9',type,
'#skF_9': ( ty * ty * uni * uni ) > uni ).
tff('#skF_12',type,
'#skF_12': ( ty * ty * uni * uni ) > uni ).
tff(node,type,
node: ( ty * uni * uni ) > uni ).
tff(real,type,
real: ty ).
tff(match_bool,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(false,type,
false: bool ).
tff(tb2t2,type,
tb2t2: uni > tree_a1 ).
tff(match_tree,type,
match_tree: ( ty * ty * uni * uni * uni ) > uni ).
tff(node_proj_2,type,
node_proj_2: ( ty * uni ) > uni ).
tff(tb2t,type,
tb2t: uni > tree_int ).
tff(tree,type,
tree: ty > ty ).
tff(distinct,type,
distinct: ( ty * uni ) > $o ).
tff(length,type,
length: ( ty * uni ) > $int ).
tff(qtmark,type,
qtmark: ty ).
tff('#skF_10',type,
'#skF_10': ( ty * ty * uni * uni ) > uni ).
tff('#skF_7',type,
'#skF_7': ( ty * ty * uni * uni ) > uni ).
tff('#skF_4',type,
'#skF_4': ( ty * uni ) > uni ).
tff(bool1,type,
bool1: ty ).
tff('#skF_6',type,
'#skF_6': ( ty * uni * uni ) > uni ).
tff(t2tb1,type,
t2tb1: list_int > uni ).
tff(leaf,type,
leaf: ( ty * uni ) > uni ).
tff('#skF_19',type,
'#skF_19': tree_int ).
tff('#skF_1',type,
'#skF_1': ( ty * uni * uni ) > uni ).
tff('#skF_5',type,
'#skF_5': ( ty * uni ) > uni ).
tff(match_list,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(sort,type,
sort: ( ty * uni ) > $o ).
tff(true,type,
true: bool ).
tff(ref,type,
ref: ty > ty ).
tff(cons_proj_2,type,
cons_proj_2: ( ty * uni ) > uni ).
tff('#skF_3',type,
'#skF_3': ( ty * uni ) > uni ).
tff(mem,type,
mem: ( ty * uni * uni ) > $o ).
tff('#skF_17',type,
'#skF_17': tree_int ).
tff(tb2t3,type,
tb2t3: uni > $int ).
tff('#skF_15',type,
'#skF_15': tree_a1 ).
tff(witness,type,
witness: ty > uni ).
tff(infix_plpl,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff('#skF_2',type,
'#skF_2': ( ty * uni * uni ) > uni ).
tff(mk_ref,type,
mk_ref: ( ty * uni ) > uni ).
tff(f_311,axiom,
! [Ia: $int] : ( tb2t3(t2tb3(Ia)) = Ia ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL3) ).
tff(f_354,negated_conjecture,
~ ! [Ra: $int,X: tree_a1,X1: tree_a1,R1a: $int,O: tree_int] :
( ( same_shape(int,a1,t2tb2(X1),t2tb(O))
& distinct(int,labels(int,t2tb(O)))
& $lesseq(Ra,R1a)
& ! [X2a: $int] :
( mem(int,t2tb3(X2a),labels(int,t2tb(O)))
=> ( $less(Ra,X2a)
& $lesseq(X2a,R1a) ) ) )
=> ! [R2a: $int,O1: tree_int] :
( ( same_shape(int,a1,t2tb2(X),t2tb(O1))
& distinct(int,labels(int,t2tb(O1)))
& $lesseq(R1a,R2a)
& ! [X2a: $int] :
( mem(int,t2tb3(X2a),labels(int,t2tb(O1)))
=> ( $less(R1a,X2a)
& $lesseq(X2a,R2a) ) ) )
=> ( same_shape(int,a1,node(a1,t2tb2(X),t2tb2(X1)),node(int,t2tb(O1),t2tb(O)))
& distinct(int,labels(int,node(int,t2tb(O1),t2tb(O))))
& $lesseq(Ra,R2a)
& ! [X2a: $int] :
( mem(int,t2tb3(X2a),labels(int,node(int,t2tb(O1),t2tb(O))))
=> ( $less(Ra,X2a)
& $lesseq(X2a,R2a) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_relabel) ).
tff(f_184,axiom,
! [A: ty,L1: uni,L2: uni] :
( distinct(A,L1)
=> ( distinct(A,L2)
=> ( ! [X: uni] :
( sort(A,X)
=> ( mem(A,X,L1)
=> ~ mem(A,X,L2) ) )
=> distinct(A,infix_plpl(A,L1,L2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distinct_append) ).
tff(f_313,axiom,
! [J: uni] : ( t2tb3(tb2t3(J)) = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR3) ).
tff(f_249,axiom,
! [A: ty,B: ty,L1: uni,R1: uni,L2: uni,R2: uni] :
( same_shape(B,A,L1,L2)
=> ( same_shape(B,A,R1,R2)
=> same_shape(B,A,node(A,L1,R1),node(B,L2,R2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_shape_Node) ).
tff(f_227,axiom,
! [A: ty] :
( ! [X: uni] : ( labels(A,leaf(A,X)) = cons(A,X,nil(A)) )
& ! [X: uni,X1: uni] : ( labels(A,node(A,X,X1)) = infix_plpl(A,labels(A,X),labels(A,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',labels_def) ).
tff(f_129,axiom,
! [A: ty,X: uni,L1: uni,L2: uni] :
( mem(A,X,infix_plpl(A,L1,L2))
<=> ( mem(A,X,L1)
| mem(A,X,L2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_append) ).
tff(c_551790,plain,
! [I_14205: $int] : ( tb2t3(t2tb3(I_14205)) = I_14205 ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_262,plain,
distinct(int,labels(int,t2tb('#skF_19'))),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_271,plain,
distinct(int,labels(int,t2tb('#skF_17'))),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_642437,plain,
! [A_20948: ty,L1_20949: uni,L2_20950: uni] :
( mem(A_20948,'#skF_6'(A_20948,L1_20949,L2_20950),L2_20950)
| distinct(A_20948,infix_plpl(A_20948,L1_20949,L2_20950))
| ~ distinct(A_20948,L2_20950)
| ~ distinct(A_20948,L1_20949) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_551789,plain,
! [J_14204: uni] : ( t2tb3(tb2t3(J_14204)) = J_14204 ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_552253,plain,
! [X2_14673: $int] :
( ~ mem(int,t2tb3(X2_14673),labels(int,t2tb('#skF_17')))
| $less('#skF_13',X2_14673) ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_552260,plain,
! [J_14204: uni] :
( ~ mem(int,J_14204,labels(int,t2tb('#skF_17')))
| $less('#skF_13',tb2t3(J_14204)) ),
inference(superposition,[status(thm),theory(equality)],[c_551789,c_552253]) ).
tff(c_642463,plain,
! [L1_20949: uni] :
( $less('#skF_13',tb2t3('#skF_6'(int,L1_20949,labels(int,t2tb('#skF_17')))))
| distinct(int,infix_plpl(int,L1_20949,labels(int,t2tb('#skF_17'))))
| ~ distinct(int,labels(int,t2tb('#skF_17')))
| ~ distinct(int,L1_20949) ),
inference(resolution,[status(thm)],[c_642437,c_552260]) ).
tff(c_642930,plain,
! [L1_20986: uni] :
( $less('#skF_13',tb2t3('#skF_6'(int,L1_20986,labels(int,t2tb('#skF_17')))))
| distinct(int,infix_plpl(int,L1_20986,labels(int,t2tb('#skF_17'))))
| ~ distinct(int,L1_20986) ),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_642463]) ).
tff(c_264,plain,
same_shape(int,a1,t2tb2('#skF_14'),t2tb('#skF_19')),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_273,plain,
same_shape(int,a1,t2tb2('#skF_15'),t2tb('#skF_17')),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_628786,plain,
! [L1_19970: uni,A_19971: ty,R2_19969: uni,L2_19972: uni,B_19967: ty,R1_19968: uni] :
( same_shape(B_19967,A_19971,node(A_19971,L1_19970,R1_19968),node(B_19967,L2_19972,R2_19969))
| ~ same_shape(B_19967,A_19971,R1_19968,R2_19969)
| ~ same_shape(B_19967,A_19971,L1_19970,L2_19972) ),
inference(cnfTransformation,[status(thm)],[f_249]) ).
tff(c_551844,plain,
! [A_14379: ty,X_14380: uni,X1_14381: uni] : ( labels(A_14379,node(A_14379,X_14380,X1_14381)) = infix_plpl(A_14379,labels(A_14379,X_14380),labels(A_14379,X1_14381)) ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_276,plain,
( mem(int,t2tb3('#skF_20'),labels(int,node(int,t2tb('#skF_19'),t2tb('#skF_17'))))
| ~ distinct(int,labels(int,node(int,t2tb('#skF_19'),t2tb('#skF_17'))))
| ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| ~ $lesseq('#skF_13','#skF_18') ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_551784,plain,
( mem(int,t2tb3('#skF_20'),labels(int,node(int,t2tb('#skF_19'),t2tb('#skF_17'))))
| ~ distinct(int,labels(int,node(int,t2tb('#skF_19'),t2tb('#skF_17'))))
| ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| $less('#skF_18','#skF_13') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_276]) ).
tff(c_551929,plain,
( mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| ~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| $less('#skF_18','#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_551844,c_551844,c_551784]) ).
tff(c_622146,plain,
~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17'))),
inference(splitLeft,[status(thm)],[c_551929]) ).
tff(c_628789,plain,
( ~ same_shape(int,a1,t2tb2('#skF_15'),t2tb('#skF_17'))
| ~ same_shape(int,a1,t2tb2('#skF_14'),t2tb('#skF_19')) ),
inference(resolution,[status(thm)],[c_628786,c_622146]) ).
tff(c_628799,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_264,c_273,c_628789]) ).
tff(c_628804,plain,
( ~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| $less('#skF_18','#skF_13')
| mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) ),
inference(splitRight,[status(thm)],[c_551929]) ).
tff(c_642000,plain,
~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))),
inference(splitLeft,[status(thm)],[c_628804]) ).
tff(c_642933,plain,
( $less('#skF_13',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))))
| ~ distinct(int,labels(int,t2tb('#skF_19'))) ),
inference(resolution,[status(thm)],[c_642930,c_642000]) ).
tff(c_642960,plain,
$less('#skF_13',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))),
inference(demodulation,[status(thm),theory(equality)],[c_262,c_642933]) ).
tff(c_644890,plain,
tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) = '#skE_15',
inference(define,[status(thm),theory(equality)],[c_642960]) ).
tff(c_643646,plain,
! [A_21034: ty,L1_21035: uni,L2_21036: uni] :
( mem(A_21034,'#skF_6'(A_21034,L1_21035,L2_21036),L1_21035)
| distinct(A_21034,infix_plpl(A_21034,L1_21035,L2_21036))
| ~ distinct(A_21034,L2_21036)
| ~ distinct(A_21034,L1_21035) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_552178,plain,
! [X2_14649: $int] :
( ~ mem(int,t2tb3(X2_14649),labels(int,t2tb('#skF_19')))
| $less('#skF_16',X2_14649) ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_552185,plain,
! [J_14204: uni] :
( ~ mem(int,J_14204,labels(int,t2tb('#skF_19')))
| $less('#skF_16',tb2t3(J_14204)) ),
inference(superposition,[status(thm),theory(equality)],[c_551789,c_552178]) ).
tff(c_643680,plain,
! [L2_21036: uni] :
( $less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),L2_21036)))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),L2_21036))
| ~ distinct(int,L2_21036)
| ~ distinct(int,labels(int,t2tb('#skF_19'))) ),
inference(resolution,[status(thm)],[c_643646,c_552185]) ).
tff(c_643871,plain,
! [L2_21059: uni] :
( $less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),L2_21059)))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),L2_21059))
| ~ distinct(int,L2_21059) ),
inference(demodulation,[status(thm),theory(equality)],[c_262,c_643680]) ).
tff(c_643874,plain,
( $less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))))
| ~ distinct(int,labels(int,t2tb('#skF_17'))) ),
inference(resolution,[status(thm)],[c_643871,c_642000]) ).
tff(c_643889,plain,
$less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_643874]) ).
tff(c_644939,plain,
$less('#skF_16','#skE_15'),
inference(demodulation,[status(thm),theory(equality)],[c_644890,c_643889]) ).
tff(c_654207,plain,
'#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))) = t2tb3('#skE_15'),
inference(superposition,[status(thm),theory(equality)],[c_644890,c_551789]) ).
tff(c_551862,plain,
! [A_14433: ty,L1_14434: uni,L2_14435: uni] :
( mem(A_14433,'#skF_6'(A_14433,L1_14434,L2_14435),L2_14435)
| distinct(A_14433,infix_plpl(A_14433,L1_14434,L2_14435))
| ~ distinct(A_14433,L2_14435)
| ~ distinct(A_14433,L1_14434) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_654214,plain,
( mem(int,t2tb3('#skE_15'),labels(int,t2tb('#skF_17')))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| ~ distinct(int,labels(int,t2tb('#skF_17')))
| ~ distinct(int,labels(int,t2tb('#skF_19'))) ),
inference(superposition,[status(thm),theory(equality)],[c_654207,c_551862]) ).
tff(c_654232,plain,
( mem(int,t2tb3('#skE_15'),labels(int,t2tb('#skF_17')))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) ),
inference(demodulation,[status(thm),theory(equality)],[c_262,c_271,c_654214]) ).
tff(c_654308,plain,
mem(int,t2tb3('#skE_15'),labels(int,t2tb('#skF_17'))),
inference(negUnitSimplification,[status(thm)],[c_642000,c_654232]) ).
tff(c_265,plain,
! [X2_212a: $int] :
( ~ mem(int,t2tb3(X2_212a),labels(int,t2tb('#skF_17')))
| $lesseq(X2_212a,'#skF_16') ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_552638,plain,
! [X2_14719: $int] :
( ~ mem(int,t2tb3(X2_14719),labels(int,t2tb('#skF_17')))
| ~ $less('#skF_16',X2_14719) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_265]) ).
tff(c_552645,plain,
! [J_14204: uni] :
( ~ mem(int,J_14204,labels(int,t2tb('#skF_17')))
| ~ $less('#skF_16',tb2t3(J_14204)) ),
inference(superposition,[status(thm),theory(equality)],[c_551789,c_552638]) ).
tff(c_654314,plain,
~ $less('#skF_16',tb2t3(t2tb3('#skE_15'))),
inference(resolution,[status(thm)],[c_654308,c_552645]) ).
tff(c_654330,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_644939,c_551790,c_654314]) ).
tff(c_654332,plain,
distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))),
inference(splitRight,[status(thm)],[c_628804]) ).
tff(c_628801,plain,
same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17'))),
inference(splitRight,[status(thm)],[c_551929]) ).
tff(c_274,plain,
( ~ distinct(int,labels(int,node(int,t2tb('#skF_19'),t2tb('#skF_17'))))
| ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| ~ $lesseq('#skF_13','#skF_18')
| ~ $less('#skF_13','#skF_20')
| ~ $lesseq('#skF_20','#skF_18') ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_305,plain,
( ~ distinct(int,labels(int,node(int,t2tb('#skF_19'),t2tb('#skF_17'))))
| ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| $less('#skF_18','#skF_13')
| ~ $less('#skF_13','#skF_20')
| $less('#skF_18','#skF_20') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_274]) ).
tff(c_551923,plain,
( ~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| $less('#skF_18','#skF_13')
| ~ $less('#skF_13','#skF_20')
| $less('#skF_18','#skF_20') ),
inference(demodulation,[status(thm),theory(equality)],[c_551844,c_305]) ).
tff(c_554128,plain,
~ $less('#skF_13','#skF_20'),
inference(splitLeft,[status(thm)],[c_551923]) ).
tff(c_577914,plain,
! [A_16716: ty,L1_16717: uni,L2_16718: uni] :
( mem(A_16716,'#skF_6'(A_16716,L1_16717,L2_16718),L2_16718)
| distinct(A_16716,infix_plpl(A_16716,L1_16717,L2_16718))
| ~ distinct(A_16716,L2_16718)
| ~ distinct(A_16716,L1_16717) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_577944,plain,
! [L1_16717: uni] :
( $less('#skF_13',tb2t3('#skF_6'(int,L1_16717,labels(int,t2tb('#skF_17')))))
| distinct(int,infix_plpl(int,L1_16717,labels(int,t2tb('#skF_17'))))
| ~ distinct(int,labels(int,t2tb('#skF_17')))
| ~ distinct(int,L1_16717) ),
inference(resolution,[status(thm)],[c_577914,c_552260]) ).
tff(c_578130,plain,
! [L1_16744: uni] :
( $less('#skF_13',tb2t3('#skF_6'(int,L1_16744,labels(int,t2tb('#skF_17')))))
| distinct(int,infix_plpl(int,L1_16744,labels(int,t2tb('#skF_17'))))
| ~ distinct(int,L1_16744) ),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_577944]) ).
tff(c_560569,plain,
! [L2_15520: uni,B_15515: ty,L1_15518: uni,R2_15517: uni,R1_15516: uni,A_15519: ty] :
( same_shape(B_15515,A_15519,node(A_15519,L1_15518,R1_15516),node(B_15515,L2_15520,R2_15517))
| ~ same_shape(B_15515,A_15519,R1_15516,R2_15517)
| ~ same_shape(B_15515,A_15519,L1_15518,L2_15520) ),
inference(cnfTransformation,[status(thm)],[f_249]) ).
tff(c_554339,plain,
~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17'))),
inference(splitLeft,[status(thm)],[c_551929]) ).
tff(c_560572,plain,
( ~ same_shape(int,a1,t2tb2('#skF_15'),t2tb('#skF_17'))
| ~ same_shape(int,a1,t2tb2('#skF_14'),t2tb('#skF_19')) ),
inference(resolution,[status(thm)],[c_560569,c_554339]) ).
tff(c_560582,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_264,c_273,c_560572]) ).
tff(c_560587,plain,
( ~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| $less('#skF_18','#skF_13')
| mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) ),
inference(splitRight,[status(thm)],[c_551929]) ).
tff(c_576313,plain,
~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))),
inference(splitLeft,[status(thm)],[c_560587]) ).
tff(c_578133,plain,
( $less('#skF_13',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))))
| ~ distinct(int,labels(int,t2tb('#skF_19'))) ),
inference(resolution,[status(thm)],[c_578130,c_576313]) ).
tff(c_578160,plain,
$less('#skF_13',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))),
inference(demodulation,[status(thm),theory(equality)],[c_262,c_578133]) ).
tff(c_580058,plain,
tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) = '#skE_15',
inference(define,[status(thm),theory(equality)],[c_578160]) ).
tff(c_577566,plain,
! [A_16680: ty,L1_16681: uni,L2_16682: uni] :
( mem(A_16680,'#skF_6'(A_16680,L1_16681,L2_16682),L1_16681)
| distinct(A_16680,infix_plpl(A_16680,L1_16681,L2_16682))
| ~ distinct(A_16680,L2_16682)
| ~ distinct(A_16680,L1_16681) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_577596,plain,
! [L2_16682: uni] :
( $less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),L2_16682)))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),L2_16682))
| ~ distinct(int,L2_16682)
| ~ distinct(int,labels(int,t2tb('#skF_19'))) ),
inference(resolution,[status(thm)],[c_577566,c_552185]) ).
tff(c_577843,plain,
! [L2_16708: uni] :
( $less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),L2_16708)))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),L2_16708))
| ~ distinct(int,L2_16708) ),
inference(demodulation,[status(thm),theory(equality)],[c_262,c_577596]) ).
tff(c_577846,plain,
( $less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))))
| ~ distinct(int,labels(int,t2tb('#skF_17'))) ),
inference(resolution,[status(thm)],[c_577843,c_576313]) ).
tff(c_577861,plain,
$less('#skF_16',tb2t3('#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_577846]) ).
tff(c_580075,plain,
$less('#skF_16','#skE_15'),
inference(demodulation,[status(thm),theory(equality)],[c_580058,c_577861]) ).
tff(c_588593,plain,
'#skF_6'(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))) = t2tb3('#skE_15'),
inference(superposition,[status(thm),theory(equality)],[c_580058,c_551789]) ).
tff(c_588597,plain,
( mem(int,t2tb3('#skE_15'),labels(int,t2tb('#skF_17')))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| ~ distinct(int,labels(int,t2tb('#skF_17')))
| ~ distinct(int,labels(int,t2tb('#skF_19'))) ),
inference(superposition,[status(thm),theory(equality)],[c_588593,c_551862]) ).
tff(c_588610,plain,
( mem(int,t2tb3('#skE_15'),labels(int,t2tb('#skF_17')))
| distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) ),
inference(demodulation,[status(thm),theory(equality)],[c_262,c_271,c_588597]) ).
tff(c_590187,plain,
mem(int,t2tb3('#skE_15'),labels(int,t2tb('#skF_17'))),
inference(negUnitSimplification,[status(thm)],[c_576313,c_588610]) ).
tff(c_590193,plain,
~ $less('#skF_16',tb2t3(t2tb3('#skE_15'))),
inference(resolution,[status(thm)],[c_590187,c_552645]) ).
tff(c_590209,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_580075,c_551790,c_590193]) ).
tff(c_590214,plain,
( $less('#skF_18','#skF_13')
| mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) ),
inference(splitRight,[status(thm)],[c_560587]) ).
tff(c_590720,plain,
$less('#skF_18','#skF_13'),
inference(splitLeft,[status(thm)],[c_590214]) ).
tff(c_259,plain,
$lesseq('#skF_16','#skF_18'),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_309,plain,
~ $less('#skF_18','#skF_16'),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_259]) ).
tff(c_268,plain,
$lesseq('#skF_13','#skF_16'),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_306,plain,
~ $less('#skF_16','#skF_13'),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_268]) ).
tff(c_590721,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_590720,c_309,c_306]) ).
tff(c_590730,plain,
mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))),
inference(splitRight,[status(thm)],[c_590214]) ).
tff(c_551881,plain,
! [A_14479: ty,X_14480: uni,L2_14481: uni,L1_14482: uni] :
( mem(A_14479,X_14480,L2_14481)
| mem(A_14479,X_14480,L1_14482)
| ~ mem(A_14479,X_14480,infix_plpl(A_14479,L1_14482,L2_14481)) ),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_590745,plain,
( mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_17')))
| mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_19'))) ),
inference(resolution,[status(thm)],[c_590730,c_551881]) ).
tff(c_621918,plain,
mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_19'))),
inference(splitLeft,[status(thm)],[c_590745]) ).
tff(c_621927,plain,
$less('#skF_16',tb2t3(t2tb3('#skF_20'))),
inference(resolution,[status(thm)],[c_621918,c_552185]) ).
tff(c_621942,plain,
$less('#skF_16','#skF_20'),
inference(demodulation,[status(thm),theory(equality)],[c_551790,c_621927]) ).
tff(c_621947,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_621942,c_554128,c_306]) ).
tff(c_622095,plain,
mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_17'))),
inference(splitRight,[status(thm)],[c_590745]) ).
tff(c_622104,plain,
$less('#skF_13',tb2t3(t2tb3('#skF_20'))),
inference(resolution,[status(thm)],[c_622095,c_552260]) ).
tff(c_622118,plain,
$less('#skF_13','#skF_20'),
inference(demodulation,[status(thm),theory(equality)],[c_551790,c_622104]) ).
tff(c_622120,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_554128,c_622118]) ).
tff(c_622123,plain,
( ~ same_shape(int,a1,node(a1,t2tb2('#skF_14'),t2tb2('#skF_15')),node(int,t2tb('#skF_19'),t2tb('#skF_17')))
| ~ distinct(int,infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17'))))
| $less('#skF_18','#skF_20')
| $less('#skF_18','#skF_13') ),
inference(splitRight,[status(thm)],[c_551923]) ).
tff(c_654343,plain,
( $less('#skF_18','#skF_20')
| $less('#skF_18','#skF_13') ),
inference(demodulation,[status(thm),theory(equality)],[c_654332,c_628801,c_622123]) ).
tff(c_654345,plain,
$less('#skF_18','#skF_13'),
inference(splitLeft,[status(thm)],[c_654343]) ).
tff(c_654346,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_654345,c_309,c_306]) ).
tff(c_654349,plain,
$less('#skF_18','#skF_20'),
inference(splitRight,[status(thm)],[c_654343]) ).
tff(c_654350,plain,
~ $less('#skF_18','#skF_13'),
inference(splitRight,[status(thm)],[c_654343]) ).
tff(c_654335,plain,
( $less('#skF_18','#skF_13')
| mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))) ),
inference(splitRight,[status(thm)],[c_628804]) ).
tff(c_654900,plain,
mem(int,t2tb3('#skF_20'),infix_plpl(int,labels(int,t2tb('#skF_19')),labels(int,t2tb('#skF_17')))),
inference(negUnitSimplification,[status(thm)],[c_654350,c_654335]) ).
tff(c_654915,plain,
( mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_17')))
| mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_19'))) ),
inference(resolution,[status(thm)],[c_654900,c_551881]) ).
tff(c_681831,plain,
mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_19'))),
inference(splitLeft,[status(thm)],[c_654915]) ).
tff(c_256,plain,
! [X2_215a: $int] :
( ~ mem(int,t2tb3(X2_215a),labels(int,t2tb('#skF_19')))
| $lesseq(X2_215a,'#skF_18') ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_552448,plain,
! [X2_14692: $int] :
( ~ mem(int,t2tb3(X2_14692),labels(int,t2tb('#skF_19')))
| ~ $less('#skF_18',X2_14692) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_256]) ).
tff(c_552455,plain,
! [J_14204: uni] :
( ~ mem(int,J_14204,labels(int,t2tb('#skF_19')))
| ~ $less('#skF_18',tb2t3(J_14204)) ),
inference(superposition,[status(thm),theory(equality)],[c_551789,c_552448]) ).
tff(c_681837,plain,
~ $less('#skF_18',tb2t3(t2tb3('#skF_20'))),
inference(resolution,[status(thm)],[c_681831,c_552455]) ).
tff(c_681853,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_654349,c_551790,c_681837]) ).
tff(c_681860,plain,
mem(int,t2tb3('#skF_20'),labels(int,t2tb('#skF_17'))),
inference(splitRight,[status(thm)],[c_654915]) ).
tff(c_681866,plain,
~ $less('#skF_16',tb2t3(t2tb3('#skF_20'))),
inference(resolution,[status(thm)],[c_681860,c_552645]) ).
tff(c_681881,plain,
~ $less('#skF_16','#skF_20'),
inference(demodulation,[status(thm),theory(equality)],[c_551790,c_681866]) ).
tff(c_681888,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_681881,c_654349,c_309]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW637_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.14/0.34 % Computer : n014.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 06:19:34 EDT 2025
% 0.14/0.34 % CPUTime :
% 143.59/101.65 ***********************************************************************
% 143.59/101.65 After 99.7 sec it's time to try something different, got 99.7 sec left
% 143.59/101.65 ***********************************************************************
% 270.91/201.34 ***********************************************************************
% 270.91/201.34 After 199.4 sec it's time to try something different, got 99.7 sec left
% 270.91/201.34 ***********************************************************************
% 290.11/217.49 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 290.13/217.50
% 290.13/217.50 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------