%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW637_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:00 PM UTC 2026
% Result : Theorem 3.79s 1.43s
% Output : Refutation 4.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 39
% Syntax : Number of formulae : 160 ( 39 unt; 0 typ; 33 def)
% Number of atoms : 552 ( 40 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 635 ( 243 ~; 224 |; 109 &)
% ( 25 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 154 ( 102 atm; 0 fun; 0 num; 52 var)
% Number of types : 10 ( 8 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 31 ( 27 usr; 24 prp; 0-4 aty)
% Number of functors : 68 ( 68 usr; 27 con; 0-5 aty)
% Number of variables : 199 ( 172 !; 27 ?; 199 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
a: $tType ).
tff(type_def_10,type,
tree_int: $tType ).
tff(type_def_11,type,
list_int: $tType ).
tff(type_def_12,type,
tree_a1: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_10,type,
list: ty > ty ).
tff(func_def_11,type,
nil: ty > uni ).
tff(func_def_12,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_13,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_14,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_15,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_16,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_19,type,
length: ( ty * uni ) > $int ).
tff(func_def_22,type,
tree: ty > ty ).
tff(func_def_23,type,
leaf: ( ty * uni ) > uni ).
tff(func_def_24,type,
node: ( ty * uni * uni ) > uni ).
tff(func_def_25,type,
match_tree: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_26,type,
leaf_proj_1: ( ty * uni ) > uni ).
tff(func_def_27,type,
node_proj_1: ( ty * uni ) > uni ).
tff(func_def_28,type,
node_proj_2: ( ty * uni ) > uni ).
tff(func_def_29,type,
labels: ( ty * uni ) > uni ).
tff(func_def_30,type,
ref: ty > ty ).
tff(func_def_31,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_32,type,
contents: ( ty * uni ) > uni ).
tff(func_def_33,type,
a1: ty ).
tff(func_def_34,type,
t2tb: tree_int > uni ).
tff(func_def_35,type,
tb2t: uni > tree_int ).
tff(func_def_36,type,
t2tb1: list_int > uni ).
tff(func_def_37,type,
tb2t1: uni > list_int ).
tff(func_def_38,type,
t2tb2: tree_a1 > uni ).
tff(func_def_39,type,
tb2t2: uni > tree_a1 ).
tff(func_def_40,type,
t2tb3: $int > uni ).
tff(func_def_41,type,
tb2t3: uni > $int ).
tff(func_def_42,type,
sK0: ( uni * ty ) > uni ).
tff(func_def_43,type,
sK1: ( uni * ty ) > uni ).
tff(func_def_44,type,
sK2: ( uni * ty ) > uni ).
tff(func_def_45,type,
sK3: tree_int ).
tff(func_def_46,type,
sK4: $int ).
tff(func_def_47,type,
sK5: $int ).
tff(func_def_48,type,
sK6: tree_a1 ).
tff(func_def_49,type,
sK7: tree_a1 ).
tff(func_def_50,type,
sK8: tree_int ).
tff(func_def_51,type,
sK9: $int ).
tff(func_def_52,type,
sK10: $int ).
tff(func_def_53,type,
sK11: ( uni * uni * ty ) > uni ).
tff(func_def_54,type,
sK12: ( ty * ty * uni * uni ) > uni ).
tff(func_def_55,type,
sK13: ( ty * ty * uni * uni ) > uni ).
tff(func_def_56,type,
sK14: ( ty * ty * uni * uni ) > uni ).
tff(func_def_57,type,
sK15: ( ty * ty * uni * uni ) > uni ).
tff(func_def_58,type,
sK16: ( ty * ty * uni * uni ) > uni ).
tff(func_def_59,type,
sK17: ( ty * ty * uni * uni ) > uni ).
tff(func_def_60,type,
sK18: ( uni * ty * uni ) > uni ).
tff(func_def_61,type,
sK19: ( uni * ty * uni ) > uni ).
tff(func_def_62,type,
sF20: uni ).
tff(func_def_63,type,
sF21: uni ).
tff(func_def_64,type,
sF22: uni ).
tff(func_def_65,type,
sF23: uni ).
tff(func_def_66,type,
sF24: uni ).
tff(func_def_67,type,
sF25: uni ).
tff(func_def_68,type,
sF26: uni ).
tff(func_def_69,type,
sF27: uni ).
tff(func_def_70,type,
sF28: uni ).
tff(func_def_71,type,
sF29: uni ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_2,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
distinct: ( ty * uni ) > $o ).
tff(pred_def_5,type,
same_shape: ( ty * ty * uni * uni ) > $o ).
tff(f35,axiom,
! [X1: uni,X0: ty,X2: uni] :
( distinct(X0,X1)
=> ( distinct(X0,X2)
=> ( ! [X3: uni] :
( sort(X0,X3)
=> ( mem(X0,X3,X1)
=> ~ mem(X0,X3,X2) ) )
=> distinct(X0,infix_plpl(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distinct_append) ).
tff(f50,axiom,
! [X0: ty] :
( ! [X2: uni,X1: uni] : ( labels(X0,node(X0,X1,X2)) = infix_plpl(X0,labels(X0,X1),labels(X0,X2)) )
& ! [X1: uni] : ( labels(X0,leaf(X0,X1)) = cons(X0,X1,nil(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',labels_def) ).
tff(f52,axiom,
! [X3: uni,X0: ty,X2: uni,X1: uni] :
( ( mem(X0,X1,labels(X0,X3))
| mem(X0,X1,labels(X0,X2)) )
<=> mem(X0,X1,labels(X0,node(X0,X2,X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',labels_Node) ).
tff(f54,axiom,
! [X5: uni,X3: uni,X1: ty,X2: uni,X0: ty,X4: uni] :
( same_shape(X1,X0,X2,X4)
=> ( same_shape(X1,X0,X3,X5)
=> same_shape(X1,X0,node(X0,X2,X3),node(X1,X4,X5)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',same_shape_Node) ).
tff(f71,axiom,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f72,conjecture,
! [X0: $int,X3: $int,X4: tree_int,X1: tree_a1,X2: tree_a1] :
( ( ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X4)))
=> ( $less(X0,X5)
& $lesseq(X5,X3) ) )
& same_shape(int,a1,t2tb2(X2),t2tb(X4))
& distinct(int,labels(int,t2tb(X4)))
& $lesseq(X0,X3) )
=> ! [X7: tree_int,X6: $int] :
( ( $lesseq(X3,X6)
& ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X7)))
=> ( $less(X3,X5)
& $lesseq(X5,X6) ) )
& distinct(int,labels(int,t2tb(X7)))
& same_shape(int,a1,t2tb2(X1),t2tb(X7)) )
=> ( ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,node(int,t2tb(X7),t2tb(X4))))
=> ( $lesseq(X5,X6)
& $less(X0,X5) ) )
& distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4))))
& same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4)))
& $lesseq(X0,X6) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_relabel) ).
tff(f73,negated_conjecture,
~ ! [X0: $int,X3: $int,X4: tree_int,X1: tree_a1,X2: tree_a1] :
( ( ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X4)))
=> ( $less(X0,X5)
& $lesseq(X5,X3) ) )
& same_shape(int,a1,t2tb2(X2),t2tb(X4))
& distinct(int,labels(int,t2tb(X4)))
& $lesseq(X0,X3) )
=> ! [X7: tree_int,X6: $int] :
( ( $lesseq(X3,X6)
& ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X7)))
=> ( $less(X3,X5)
& $lesseq(X5,X6) ) )
& distinct(int,labels(int,t2tb(X7)))
& same_shape(int,a1,t2tb2(X1),t2tb(X7)) )
=> ( ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,node(int,t2tb(X7),t2tb(X4))))
=> ( $lesseq(X5,X6)
& $less(X0,X5) ) )
& distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4))))
& same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4)))
& $lesseq(X0,X6) ) ) ),
inference(negated_conjecture,[status(cth)],[f72]) ).
tff(f75,plain,
~ ! [X0: $int,X3: $int,X4: tree_int,X1: tree_a1,X2: tree_a1] :
( ( ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X4)))
=> ( $less(X0,X5)
& ~ $less(X3,X5) ) )
& same_shape(int,a1,t2tb2(X2),t2tb(X4))
& distinct(int,labels(int,t2tb(X4)))
& ~ $less(X3,X0) )
=> ! [X7: tree_int,X6: $int] :
( ( ~ $less(X6,X3)
& ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X7)))
=> ( $less(X3,X5)
& ~ $less(X6,X5) ) )
& distinct(int,labels(int,t2tb(X7)))
& same_shape(int,a1,t2tb2(X1),t2tb(X7)) )
=> ( ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,node(int,t2tb(X7),t2tb(X4))))
=> ( ~ $less(X6,X5)
& $less(X0,X5) ) )
& distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4))))
& same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4)))
& ~ $less(X6,X0) ) ) ),
inference(theory_normalization,[],[f73]) ).
tff(f80,plain,
! [X2: uni,X3: uni,X1: ty,X0: uni] :
( ( mem(X1,X3,labels(X1,X2))
| mem(X1,X3,labels(X1,X0)) )
<=> mem(X1,X3,labels(X1,node(X1,X2,X0))) ),
inference(rectify,[],[f52]) ).
tff(f101,plain,
~ ! [X2: tree_int,X0: $int,X4: tree_a1,X1: $int,X3: tree_a1] :
( ( distinct(int,labels(int,t2tb(X2)))
& ! [X5: $int] :
( mem(int,t2tb3(X5),labels(int,t2tb(X2)))
=> ( $less(X0,X5)
& ~ $less(X1,X5) ) )
& ~ $less(X1,X0)
& same_shape(int,a1,t2tb2(X4),t2tb(X2)) )
=> ! [X6: tree_int,X7: $int] :
( ( ! [X8: $int] :
( mem(int,t2tb3(X8),labels(int,t2tb(X6)))
=> ( $less(X1,X8)
& ~ $less(X7,X8) ) )
& distinct(int,labels(int,t2tb(X6)))
& ~ $less(X7,X1)
& same_shape(int,a1,t2tb2(X3),t2tb(X6)) )
=> ( ! [X9: $int] :
( mem(int,t2tb3(X9),labels(int,node(int,t2tb(X6),t2tb(X2))))
=> ( $less(X0,X9)
& ~ $less(X7,X9) ) )
& distinct(int,labels(int,node(int,t2tb(X6),t2tb(X2))))
& ~ $less(X7,X0)
& same_shape(int,a1,node(a1,t2tb2(X3),t2tb2(X4)),node(int,t2tb(X6),t2tb(X2))) ) ) ),
inference(rectify,[],[f75]) ).
tff(f106,plain,
! [X0: uni,X1: ty,X2: uni] :
( distinct(X1,X0)
=> ( distinct(X1,X2)
=> ( ! [X3: uni] :
( sort(X1,X3)
=> ( mem(X1,X3,X0)
=> ~ mem(X1,X3,X2) ) )
=> distinct(X1,infix_plpl(X1,X0,X2)) ) ) ),
inference(rectify,[],[f35]) ).
tff(f116,plain,
! [X0: ty] :
( ! [X3: uni] : ( labels(X0,leaf(X0,X3)) = cons(X0,X3,nil(X0)) )
& ! [X1: uni,X2: uni] : ( labels(X0,node(X0,X2,X1)) = infix_plpl(X0,labels(X0,X2),labels(X0,X1)) ) ),
inference(rectify,[],[f50]) ).
tff(f117,plain,
! [X4: ty,X5: uni,X1: uni,X0: uni,X3: uni,X2: ty] :
( same_shape(X2,X4,X3,X5)
=> ( same_shape(X2,X4,X1,X0)
=> same_shape(X2,X4,node(X4,X3,X1),node(X2,X5,X0)) ) ),
inference(rectify,[],[f54]) ).
tff(f136,plain,
! [X4: ty,X5: uni,X1: uni,X0: uni,X3: uni,X2: ty] :
( same_shape(X2,X4,node(X4,X3,X1),node(X2,X5,X0))
| ~ same_shape(X2,X4,X1,X0)
| ~ same_shape(X2,X4,X3,X5) ),
inference(ennf_transformation,[],[f117]) ).
tff(f137,plain,
! [X0: uni,X4: ty,X3: uni,X1: uni,X5: uni,X2: ty] :
( ~ same_shape(X2,X4,X3,X5)
| ~ same_shape(X2,X4,X1,X0)
| same_shape(X2,X4,node(X4,X3,X1),node(X2,X5,X0)) ),
inference(flattening,[],[f136]) ).
tff(f139,plain,
? [X2: tree_int,X0: $int,X4: tree_a1,X1: $int,X3: tree_a1] :
( ? [X6: tree_int,X7: $int] :
( ( $less(X7,X0)
| ~ distinct(int,labels(int,node(int,t2tb(X6),t2tb(X2))))
| ? [X9: $int] :
( ( ~ $less(X0,X9)
| $less(X7,X9) )
& mem(int,t2tb3(X9),labels(int,node(int,t2tb(X6),t2tb(X2)))) )
| ~ same_shape(int,a1,node(a1,t2tb2(X3),t2tb2(X4)),node(int,t2tb(X6),t2tb(X2))) )
& ! [X8: $int] :
( ( $less(X1,X8)
& ~ $less(X7,X8) )
| ~ mem(int,t2tb3(X8),labels(int,t2tb(X6))) )
& distinct(int,labels(int,t2tb(X6)))
& ~ $less(X7,X1)
& same_shape(int,a1,t2tb2(X3),t2tb(X6)) )
& distinct(int,labels(int,t2tb(X2)))
& ! [X5: $int] :
( ( $less(X0,X5)
& ~ $less(X1,X5) )
| ~ mem(int,t2tb3(X5),labels(int,t2tb(X2))) )
& ~ $less(X1,X0)
& same_shape(int,a1,t2tb2(X4),t2tb(X2)) ),
inference(ennf_transformation,[],[f101]) ).
tff(f140,plain,
? [X2: tree_int,X1: $int,X0: $int,X3: tree_a1,X4: tree_a1] :
( distinct(int,labels(int,t2tb(X2)))
& ! [X5: $int] :
( ( $less(X0,X5)
& ~ $less(X1,X5) )
| ~ mem(int,t2tb3(X5),labels(int,t2tb(X2))) )
& same_shape(int,a1,t2tb2(X4),t2tb(X2))
& ~ $less(X1,X0)
& ? [X6: tree_int,X7: $int] :
( same_shape(int,a1,t2tb2(X3),t2tb(X6))
& ~ $less(X7,X1)
& distinct(int,labels(int,t2tb(X6)))
& ( $less(X7,X0)
| ~ distinct(int,labels(int,node(int,t2tb(X6),t2tb(X2))))
| ? [X9: $int] :
( ( ~ $less(X0,X9)
| $less(X7,X9) )
& mem(int,t2tb3(X9),labels(int,node(int,t2tb(X6),t2tb(X2)))) )
| ~ same_shape(int,a1,node(a1,t2tb2(X3),t2tb2(X4)),node(int,t2tb(X6),t2tb(X2))) )
& ! [X8: $int] :
( ( $less(X1,X8)
& ~ $less(X7,X8) )
| ~ mem(int,t2tb3(X8),labels(int,t2tb(X6))) ) ) ),
inference(flattening,[],[f139]) ).
tff(f143,plain,
! [X0: uni,X1: ty,X2: uni] :
( distinct(X1,infix_plpl(X1,X0,X2))
| ? [X3: uni] :
( mem(X1,X3,X2)
& mem(X1,X3,X0)
& sort(X1,X3) )
| ~ distinct(X1,X2)
| ~ distinct(X1,X0) ),
inference(ennf_transformation,[],[f106]) ).
tff(f144,plain,
! [X0: uni,X2: uni,X1: ty] :
( ~ distinct(X1,X0)
| ~ distinct(X1,X2)
| distinct(X1,infix_plpl(X1,X0,X2))
| ? [X3: uni] :
( mem(X1,X3,X2)
& mem(X1,X3,X0)
& sort(X1,X3) ) ),
inference(flattening,[],[f143]) ).
tff(f167,plain,
? [X0: tree_int,X1: $int,X2: $int,X3: tree_a1,X4: tree_a1] :
( distinct(int,labels(int,t2tb(X0)))
& ! [X5: $int] :
( ( $less(X2,X5)
& ~ $less(X1,X5) )
| ~ mem(int,t2tb3(X5),labels(int,t2tb(X0))) )
& same_shape(int,a1,t2tb2(X4),t2tb(X0))
& ~ $less(X1,X2)
& ? [X6: tree_int,X7: $int] :
( same_shape(int,a1,t2tb2(X3),t2tb(X6))
& ~ $less(X7,X1)
& distinct(int,labels(int,t2tb(X6)))
& ( $less(X7,X2)
| ~ distinct(int,labels(int,node(int,t2tb(X6),t2tb(X0))))
| ? [X8: $int] :
( ( ~ $less(X2,X8)
| $less(X7,X8) )
& mem(int,t2tb3(X8),labels(int,node(int,t2tb(X6),t2tb(X0)))) )
| ~ same_shape(int,a1,node(a1,t2tb2(X3),t2tb2(X4)),node(int,t2tb(X6),t2tb(X0))) )
& ! [X9: $int] :
( ( $less(X1,X9)
& ~ $less(X7,X9) )
| ~ mem(int,t2tb3(X9),labels(int,t2tb(X6))) ) ) ),
inference(rectify,[],[f140]) ).
tff(f168,plain,
( distinct(int,labels(int,t2tb(sK3)))
& ! [X5: $int] :
( ( $less(sK5,X5)
& ~ $less(sK4,X5) )
| ~ mem(int,t2tb3(X5),labels(int,t2tb(sK3))) )
& same_shape(int,a1,t2tb2(sK7),t2tb(sK3))
& ~ $less(sK4,sK5)
& same_shape(int,a1,t2tb2(sK6),t2tb(sK8))
& ~ $less(sK9,sK4)
& distinct(int,labels(int,t2tb(sK8)))
& ( $less(sK9,sK5)
| ~ distinct(int,labels(int,node(int,t2tb(sK8),t2tb(sK3))))
| ( ( ~ $less(sK5,sK10)
| $less(sK9,sK10) )
& mem(int,t2tb3(sK10),labels(int,node(int,t2tb(sK8),t2tb(sK3)))) )
| ~ same_shape(int,a1,node(a1,t2tb2(sK6),t2tb2(sK7)),node(int,t2tb(sK8),t2tb(sK3))) )
& ! [X9: $int] :
( ( $less(sK4,X9)
& ~ $less(sK9,X9) )
| ~ mem(int,t2tb3(X9),labels(int,t2tb(sK8))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10)],[f167]) ).
tff(f170,plain,
! [X0: uni,X1: uni,X2: ty] :
( ~ distinct(X2,X0)
| ~ distinct(X2,X1)
| distinct(X2,infix_plpl(X2,X0,X1))
| ? [X3: uni] :
( mem(X2,X3,X1)
& mem(X2,X3,X0)
& sort(X2,X3) ) ),
inference(rectify,[],[f144]) ).
tff(f171,plain,
! [X0: uni,X1: uni,X2: ty] :
( ~ distinct(X2,X0)
| ~ distinct(X2,X1)
| distinct(X2,infix_plpl(X2,X0,X1))
| ( mem(X2,sK11(X0,X1,X2),X1)
& mem(X2,sK11(X0,X1,X2),X0)
& sort(X2,sK11(X0,X1,X2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X0,X1,X2))],[f170]) ).
tff(f173,plain,
! [X0: ty] :
( ! [X1: uni] : ( cons(X0,X1,nil(X0)) = labels(X0,leaf(X0,X1)) )
& ! [X2: uni,X3: uni] : ( labels(X0,node(X0,X3,X2)) = infix_plpl(X0,labels(X0,X3),labels(X0,X2)) ) ),
inference(rectify,[],[f116]) ).
tff(f183,plain,
! [X2: uni,X3: uni,X1: ty,X0: uni] :
( ( mem(X1,X3,labels(X1,X2))
| mem(X1,X3,labels(X1,X0))
| ~ mem(X1,X3,labels(X1,node(X1,X2,X0))) )
& ( mem(X1,X3,labels(X1,node(X1,X2,X0)))
| ( ~ mem(X1,X3,labels(X1,X2))
& ~ mem(X1,X3,labels(X1,X0)) ) ) ),
inference(nnf_transformation,[],[f80]) ).
tff(f184,plain,
! [X2: uni,X3: uni,X1: ty,X0: uni] :
( ( mem(X1,X3,labels(X1,X2))
| mem(X1,X3,labels(X1,X0))
| ~ mem(X1,X3,labels(X1,node(X1,X2,X0))) )
& ( mem(X1,X3,labels(X1,node(X1,X2,X0)))
| ( ~ mem(X1,X3,labels(X1,X2))
& ~ mem(X1,X3,labels(X1,X0)) ) ) ),
inference(flattening,[],[f183]) ).
tff(f185,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni] :
( ( mem(X2,X1,labels(X2,X0))
| mem(X2,X1,labels(X2,X3))
| ~ mem(X2,X1,labels(X2,node(X2,X0,X3))) )
& ( mem(X2,X1,labels(X2,node(X2,X0,X3)))
| ( ~ mem(X2,X1,labels(X2,X0))
& ~ mem(X2,X1,labels(X2,X3)) ) ) ),
inference(rectify,[],[f184]) ).
tff(f201,plain,
! [X0: uni,X1: ty,X2: uni,X3: uni,X4: uni,X5: ty] :
( ~ same_shape(X5,X1,X2,X4)
| ~ same_shape(X5,X1,X3,X0)
| same_shape(X5,X1,node(X1,X2,X3),node(X5,X4,X0)) ),
inference(rectify,[],[f137]) ).
tff(f244,plain,
! [X9: $int] :
( ~ $less(sK9,X9)
| ~ mem(int,t2tb3(X9),labels(int,t2tb(sK8))) ),
inference(cnf_transformation,[],[f168]) ).
tff(f245,plain,
! [X9: $int] :
( $less(sK4,X9)
| ~ mem(int,t2tb3(X9),labels(int,t2tb(sK8))) ),
inference(cnf_transformation,[],[f168]) ).
tff(f246,plain,
( $less(sK9,sK5)
| ~ distinct(int,labels(int,node(int,t2tb(sK8),t2tb(sK3))))
| mem(int,t2tb3(sK10),labels(int,node(int,t2tb(sK8),t2tb(sK3))))
| ~ same_shape(int,a1,node(a1,t2tb2(sK6),t2tb2(sK7)),node(int,t2tb(sK8),t2tb(sK3))) ),
inference(cnf_transformation,[],[f168]) ).
tff(f247,plain,
( $less(sK9,sK5)
| ~ distinct(int,labels(int,node(int,t2tb(sK8),t2tb(sK3))))
| ~ $less(sK5,sK10)
| $less(sK9,sK10)
| ~ same_shape(int,a1,node(a1,t2tb2(sK6),t2tb2(sK7)),node(int,t2tb(sK8),t2tb(sK3))) ),
inference(cnf_transformation,[],[f168]) ).
tff(f248,plain,
distinct(int,labels(int,t2tb(sK8))),
inference(cnf_transformation,[],[f168]) ).
tff(f249,plain,
~ $less(sK9,sK4),
inference(cnf_transformation,[],[f168]) ).
tff(f250,plain,
same_shape(int,a1,t2tb2(sK6),t2tb(sK8)),
inference(cnf_transformation,[],[f168]) ).
tff(f251,plain,
~ $less(sK4,sK5),
inference(cnf_transformation,[],[f168]) ).
tff(f252,plain,
same_shape(int,a1,t2tb2(sK7),t2tb(sK3)),
inference(cnf_transformation,[],[f168]) ).
tff(f253,plain,
! [X5: $int] :
( ~ $less(sK4,X5)
| ~ mem(int,t2tb3(X5),labels(int,t2tb(sK3))) ),
inference(cnf_transformation,[],[f168]) ).
tff(f254,plain,
! [X5: $int] :
( $less(sK5,X5)
| ~ mem(int,t2tb3(X5),labels(int,t2tb(sK3))) ),
inference(cnf_transformation,[],[f168]) ).
tff(f255,plain,
distinct(int,labels(int,t2tb(sK3))),
inference(cnf_transformation,[],[f168]) ).
tff(f258,plain,
! [X2: ty,X0: uni,X1: uni] :
( mem(X2,sK11(X0,X1,X2),X0)
| ~ distinct(X2,X1)
| distinct(X2,infix_plpl(X2,X0,X1))
| ~ distinct(X2,X0) ),
inference(cnf_transformation,[],[f171]) ).
tff(f259,plain,
! [X2: ty,X0: uni,X1: uni] :
( mem(X2,sK11(X0,X1,X2),X1)
| ~ distinct(X2,X1)
| distinct(X2,infix_plpl(X2,X0,X1))
| ~ distinct(X2,X0) ),
inference(cnf_transformation,[],[f171]) ).
tff(f261,plain,
! [X2: uni,X3: uni,X0: ty] : ( labels(X0,node(X0,X3,X2)) = infix_plpl(X0,labels(X0,X3),labels(X0,X2)) ),
inference(cnf_transformation,[],[f173]) ).
tff(f277,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] :
( ~ mem(X2,X1,labels(X2,node(X2,X0,X3)))
| mem(X2,X1,labels(X2,X3))
| mem(X2,X1,labels(X2,X0)) ),
inference(cnf_transformation,[],[f185]) ).
tff(f321,plain,
! [X0: uni] : ( t2tb3(tb2t3(X0)) = X0 ),
inference(cnf_transformation,[],[f71]) ).
tff(f335,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty,X4: uni,X5: ty] :
( same_shape(X5,X1,node(X1,X2,X3),node(X5,X4,X0))
| ~ same_shape(X5,X1,X2,X4)
| ~ same_shape(X5,X1,X3,X0) ),
inference(cnf_transformation,[],[f201]) ).
tff(f347,definition,
sF20 = t2tb(sK3),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f348,definition,
sF21 = labels(int,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f349,plain,
labels(int,sF20) = sF21,
inference(reorient_equations,[],[f348]) ).
tff(f350,plain,
distinct(int,sF21),
inference(definition_folding,[],[f255,f349,f347]) ).
tff(f351,plain,
! [X5: $int] :
( ~ mem(int,t2tb3(X5),sF21)
| $less(sK5,X5) ),
inference(definition_folding,[],[f254,f349,f347]) ).
tff(f352,plain,
! [X5: $int] :
( ~ mem(int,t2tb3(X5),sF21)
| ~ $less(sK4,X5) ),
inference(definition_folding,[],[f253,f349,f347]) ).
tff(f353,definition,
sF22 = t2tb2(sK7),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f354,plain,
t2tb2(sK7) = sF22,
inference(reorient_equations,[],[f353]) ).
tff(f355,plain,
same_shape(int,a1,sF22,sF20),
inference(definition_folding,[],[f252,f347,f354]) ).
tff(f356,definition,
sF23 = t2tb2(sK6),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f357,definition,
sF24 = t2tb(sK8),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f358,plain,
same_shape(int,a1,sF23,sF24),
inference(definition_folding,[],[f250,f357,f356]) ).
tff(f359,definition,
sF25 = labels(int,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f360,plain,
distinct(int,sF25),
inference(definition_folding,[],[f248,f359,f357]) ).
tff(f361,definition,
sF26 = node(int,sF24,sF20),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f362,definition,
sF27 = labels(int,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f363,plain,
labels(int,sF26) = sF27,
inference(reorient_equations,[],[f362]) ).
tff(f364,definition,
sF28 = node(a1,sF23,sF22),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f365,plain,
( ~ $less(sK5,sK10)
| ~ distinct(int,sF27)
| $less(sK9,sK10)
| ~ same_shape(int,a1,sF28,sF26)
| $less(sK9,sK5) ),
inference(definition_folding,[],[f247,f361,f347,f357,f364,f354,f356,f363,f361,f347,f357]) ).
tff(f366,definition,
sF29 = t2tb3(sK10),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f367,plain,
( ~ same_shape(int,a1,sF28,sF26)
| $less(sK9,sK5)
| mem(int,sF29,sF27)
| ~ distinct(int,sF27) ),
inference(definition_folding,[],[f246,f361,f347,f357,f364,f354,f356,f363,f361,f347,f357,f366,f363,f361,f347,f357]) ).
tff(f368,plain,
! [X9: $int] :
( ~ mem(int,t2tb3(X9),sF25)
| $less(sK4,X9) ),
inference(definition_folding,[],[f245,f359,f357]) ).
tff(f369,plain,
! [X9: $int] :
( ~ mem(int,t2tb3(X9),sF25)
| ~ $less(sK9,X9) ),
inference(definition_folding,[],[f244,f359,f357]) ).
tff(f373,definition,
( spl30_1
<=> ( labels(int,sF20) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
tff(f375,plain,
( ( labels(int,sF20) = sF21 )
| ~ spl30_1 ),
inference(avatar_component_clause,[],[f373]) ).
tff(f376,plain,
spl30_1,
inference(avatar_split_clause,[],[f349,f373]) ).
tff(f383,definition,
( spl30_3
<=> $less(sK9,sK5) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
tff(f387,definition,
( spl30_4
<=> $less(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
tff(f391,definition,
( spl30_5
<=> $less(sK5,sK10) ),
introduced(definition,[new_symbols(definition,[spl30_5])],[avatar_definition]) ).
tff(f395,definition,
( spl30_6
<=> same_shape(int,a1,sF28,sF26) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
tff(f397,plain,
( ~ same_shape(int,a1,sF28,sF26)
| spl30_6 ),
inference(avatar_component_clause,[],[f395]) ).
tff(f399,definition,
( spl30_7
<=> distinct(int,sF27) ),
introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition]) ).
tff(f402,plain,
( spl30_3
| spl30_4
| ~ spl30_5
| ~ spl30_6
| ~ spl30_7 ),
inference(avatar_split_clause,[],[f365,f399,f395,f391,f387,f383]) ).
tff(f404,definition,
( spl30_8
<=> ( sF26 = node(int,sF24,sF20) ) ),
introduced(definition,[new_symbols(definition,[spl30_8])],[avatar_definition]) ).
tff(f406,plain,
( ( sF26 = node(int,sF24,sF20) )
| ~ spl30_8 ),
inference(avatar_component_clause,[],[f404]) ).
tff(f407,plain,
spl30_8,
inference(avatar_split_clause,[],[f361,f404]) ).
tff(f409,definition,
( spl30_9
<=> ( sF25 = labels(int,sF24) ) ),
introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition]) ).
tff(f411,plain,
( ( sF25 = labels(int,sF24) )
| ~ spl30_9 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
spl30_9,
inference(avatar_split_clause,[],[f359,f409]) ).
tff(f414,definition,
( spl30_10
<=> distinct(int,sF21) ),
introduced(definition,[new_symbols(definition,[spl30_10])],[avatar_definition]) ).
tff(f416,plain,
( distinct(int,sF21)
| ~ spl30_10 ),
inference(avatar_component_clause,[],[f414]) ).
tff(f417,plain,
spl30_10,
inference(avatar_split_clause,[],[f350,f414]) ).
tff(f419,definition,
( spl30_11
<=> ( sF28 = node(a1,sF23,sF22) ) ),
introduced(definition,[new_symbols(definition,[spl30_11])],[avatar_definition]) ).
tff(f421,plain,
( ( sF28 = node(a1,sF23,sF22) )
| ~ spl30_11 ),
inference(avatar_component_clause,[],[f419]) ).
tff(f422,plain,
spl30_11,
inference(avatar_split_clause,[],[f364,f419]) ).
tff(f424,definition,
( spl30_12
<=> $less(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl30_12])],[avatar_definition]) ).
tff(f427,plain,
~ spl30_12,
inference(avatar_split_clause,[],[f251,f424]) ).
tff(f434,definition,
( spl30_14
<=> $less(sK9,sK4) ),
introduced(definition,[new_symbols(definition,[spl30_14])],[avatar_definition]) ).
tff(f437,plain,
~ spl30_14,
inference(avatar_split_clause,[],[f249,f434]) ).
tff(f439,definition,
( spl30_15
<=> ( labels(int,sF26) = sF27 ) ),
introduced(definition,[new_symbols(definition,[spl30_15])],[avatar_definition]) ).
tff(f441,plain,
( ( labels(int,sF26) = sF27 )
| ~ spl30_15 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,plain,
spl30_15,
inference(avatar_split_clause,[],[f363,f439]) ).
tff(f444,definition,
( spl30_16
<=> same_shape(int,a1,sF23,sF24) ),
introduced(definition,[new_symbols(definition,[spl30_16])],[avatar_definition]) ).
tff(f446,plain,
( same_shape(int,a1,sF23,sF24)
| ~ spl30_16 ),
inference(avatar_component_clause,[],[f444]) ).
tff(f447,plain,
spl30_16,
inference(avatar_split_clause,[],[f358,f444]) ).
tff(f459,definition,
( spl30_19
<=> ( sF29 = t2tb3(sK10) ) ),
introduced(definition,[new_symbols(definition,[spl30_19])],[avatar_definition]) ).
tff(f461,plain,
( ( sF29 = t2tb3(sK10) )
| ~ spl30_19 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f462,plain,
spl30_19,
inference(avatar_split_clause,[],[f366,f459]) ).
tff(f464,definition,
( spl30_20
<=> distinct(int,sF25) ),
introduced(definition,[new_symbols(definition,[spl30_20])],[avatar_definition]) ).
tff(f466,plain,
( distinct(int,sF25)
| ~ spl30_20 ),
inference(avatar_component_clause,[],[f464]) ).
tff(f467,plain,
spl30_20,
inference(avatar_split_clause,[],[f360,f464]) ).
tff(f469,definition,
( spl30_21
<=> same_shape(int,a1,sF22,sF20) ),
introduced(definition,[new_symbols(definition,[spl30_21])],[avatar_definition]) ).
tff(f471,plain,
( same_shape(int,a1,sF22,sF20)
| ~ spl30_21 ),
inference(avatar_component_clause,[],[f469]) ).
tff(f472,plain,
spl30_21,
inference(avatar_split_clause,[],[f355,f469]) ).
tff(f479,definition,
( spl30_23
<=> mem(int,sF29,sF27) ),
introduced(definition,[new_symbols(definition,[spl30_23])],[avatar_definition]) ).
tff(f482,plain,
( ~ spl30_7
| ~ spl30_6
| spl30_23
| spl30_3 ),
inference(avatar_split_clause,[],[f367,f383,f479,f395,f399]) ).
tff(f487,plain,
( ~ mem(int,sF29,sF25)
| ~ $less(sK9,sK10)
| ~ spl30_19 ),
inference(superposition,[],[f369,f461]) ).
tff(f488,plain,
( ~ mem(int,sF29,sF25)
| $less(sK4,sK10)
| ~ spl30_19 ),
inference(superposition,[],[f368,f461]) ).
tff(f489,plain,
( ~ $less(sK4,sK10)
| ~ mem(int,sF29,sF21)
| ~ spl30_19 ),
inference(superposition,[],[f352,f461]) ).
tff(f490,plain,
( ~ mem(int,sF29,sF21)
| $less(sK5,sK10)
| ~ spl30_19 ),
inference(superposition,[],[f351,f461]) ).
tff(f492,definition,
( spl30_24
<=> mem(int,sF29,sF21) ),
introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition]) ).
tff(f494,plain,
( ~ mem(int,sF29,sF21)
| spl30_24 ),
inference(avatar_component_clause,[],[f492]) ).
tff(f495,plain,
( spl30_5
| ~ spl30_24
| ~ spl30_19 ),
inference(avatar_split_clause,[],[f490,f459,f492,f391]) ).
tff(f497,definition,
( spl30_25
<=> $less(sK4,sK10) ),
introduced(definition,[new_symbols(definition,[spl30_25])],[avatar_definition]) ).
tff(f500,plain,
( ~ spl30_25
| ~ spl30_24
| ~ spl30_19 ),
inference(avatar_split_clause,[],[f489,f459,f492,f497]) ).
tff(f507,definition,
( spl30_27
<=> mem(int,sF29,sF25) ),
introduced(definition,[new_symbols(definition,[spl30_27])],[avatar_definition]) ).
tff(f509,plain,
( ~ mem(int,sF29,sF25)
| spl30_27 ),
inference(avatar_component_clause,[],[f507]) ).
tff(f510,plain,
( ~ spl30_4
| ~ spl30_27
| ~ spl30_19 ),
inference(avatar_split_clause,[],[f487,f459,f507,f387]) ).
tff(f511,plain,
( ~ spl30_27
| spl30_25
| ~ spl30_19 ),
inference(avatar_split_clause,[],[f488,f459,f497,f507]) ).
tff(f548,plain,
! [X0: uni] :
( $less(sK4,tb2t3(X0))
| ~ mem(int,X0,sF25) ),
inference(superposition,[],[f368,f321]) ).
tff(f549,plain,
! [X0: uni] :
( ~ $less(sK4,tb2t3(X0))
| ~ mem(int,X0,sF21) ),
inference(superposition,[],[f352,f321]) ).
tff(f567,plain,
! [X0: uni] :
( ~ mem(int,X0,sF25)
| ~ mem(int,X0,sF21) ),
inference(resolution,[],[f549,f548]) ).
tff(f729,plain,
( ! [X0: uni] : ( labels(int,node(int,sF24,X0)) = infix_plpl(int,sF25,labels(int,X0)) )
| ~ spl30_9 ),
inference(superposition,[],[f261,f411]) ).
tff(f856,plain,
! [X0: uni] :
( ~ distinct(int,sF25)
| ~ distinct(int,X0)
| ~ mem(int,sK11(sF25,X0,int),sF21)
| distinct(int,infix_plpl(int,sF25,X0)) ),
inference(resolution,[],[f258,f567]) ).
tff(f865,plain,
( ! [X0: uni] :
( ~ mem(int,sK11(sF25,X0,int),sF21)
| distinct(int,infix_plpl(int,sF25,X0))
| ~ distinct(int,X0) )
| ~ spl30_20 ),
inference(forward_subsumption_resolution,[],[f856,f466]) ).
tff(f871,plain,
( ~ distinct(int,sF21)
| ~ distinct(int,sF25)
| distinct(int,infix_plpl(int,sF25,sF21))
| distinct(int,infix_plpl(int,sF25,sF21))
| ~ distinct(int,sF21)
| ~ spl30_20 ),
inference(resolution,[],[f259,f865]) ).
tff(f877,plain,
( distinct(int,infix_plpl(int,sF25,sF21))
| ~ distinct(int,sF25)
| ~ distinct(int,sF21)
| ~ spl30_20 ),
inference(duplicate_literal_removal,[],[f871]) ).
tff(f882,plain,
( distinct(int,infix_plpl(int,sF25,sF21))
| ~ distinct(int,sF21)
| ~ spl30_20 ),
inference(forward_subsumption_resolution,[],[f877,f466]) ).
tff(f885,plain,
( distinct(int,infix_plpl(int,sF25,sF21))
| ~ spl30_10
| ~ spl30_20 ),
inference(forward_subsumption_resolution,[],[f882,f416]) ).
tff(f888,definition,
( spl30_43
<=> distinct(int,infix_plpl(int,sF25,sF21)) ),
introduced(definition,[new_symbols(definition,[spl30_43])],[avatar_definition]) ).
tff(f890,plain,
( distinct(int,infix_plpl(int,sF25,sF21))
| ~ spl30_43 ),
inference(avatar_component_clause,[],[f888]) ).
tff(f891,plain,
( spl30_43
| ~ spl30_10
| ~ spl30_20 ),
inference(avatar_split_clause,[],[f885,f464,f414,f888]) ).
tff(f1073,plain,
( ( labels(int,sF26) = infix_plpl(int,sF25,labels(int,sF20)) )
| ~ spl30_8
| ~ spl30_9 ),
inference(superposition,[],[f729,f406]) ).
tff(f1080,plain,
( ( labels(int,sF26) = infix_plpl(int,sF25,sF21) )
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9 ),
inference(forward_demodulation,[],[f1073,f375]) ).
tff(f1083,plain,
( ( sF27 = infix_plpl(int,sF25,sF21) )
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9
| ~ spl30_15 ),
inference(forward_demodulation,[],[f1080,f441]) ).
tff(f1086,definition,
( spl30_51
<=> ( sF27 = infix_plpl(int,sF25,sF21) ) ),
introduced(definition,[new_symbols(definition,[spl30_51])],[avatar_definition]) ).
tff(f1088,plain,
( ( sF27 = infix_plpl(int,sF25,sF21) )
| ~ spl30_51 ),
inference(avatar_component_clause,[],[f1086]) ).
tff(f1089,plain,
( spl30_51
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9
| ~ spl30_15 ),
inference(avatar_split_clause,[],[f1083,f439,f409,f404,f373,f1086]) ).
tff(f1118,plain,
( distinct(int,sF27)
| ~ spl30_43
| ~ spl30_51 ),
inference(superposition,[],[f890,f1088]) ).
tff(f1125,plain,
( spl30_7
| ~ spl30_43
| ~ spl30_51 ),
inference(avatar_split_clause,[],[f1118,f1086,f888,f399]) ).
tff(f1142,plain,
( ! [X0: uni] :
( mem(int,X0,labels(int,sF20))
| ~ mem(int,X0,labels(int,sF26))
| mem(int,X0,labels(int,sF24)) )
| ~ spl30_8 ),
inference(superposition,[],[f277,f406]) ).
tff(f1150,plain,
( ! [X0: uni] :
( mem(int,X0,labels(int,sF24))
| mem(int,X0,sF21)
| ~ mem(int,X0,labels(int,sF26)) )
| ~ spl30_1
| ~ spl30_8 ),
inference(forward_demodulation,[],[f1142,f375]) ).
tff(f1155,plain,
( ! [X0: uni] :
( ~ mem(int,X0,labels(int,sF26))
| mem(int,X0,sF21)
| mem(int,X0,sF25) )
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9 ),
inference(forward_demodulation,[],[f1150,f411]) ).
tff(f1158,plain,
( ! [X0: uni] :
( mem(int,X0,sF25)
| ~ mem(int,X0,sF27)
| mem(int,X0,sF21) )
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9
| ~ spl30_15 ),
inference(forward_demodulation,[],[f1155,f441]) ).
tff(f1187,plain,
( ! [X2: uni,X0: ty,X1: uni] :
( same_shape(X0,a1,sF28,node(X0,X1,X2))
| ~ same_shape(X0,a1,sF23,X1)
| ~ same_shape(X0,a1,sF22,X2) )
| ~ spl30_11 ),
inference(superposition,[],[f335,f421]) ).
tff(f1217,plain,
( mem(int,sF29,sF21)
| ~ mem(int,sF29,sF27)
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9
| ~ spl30_15
| spl30_27 ),
inference(resolution,[],[f1158,f509]) ).
tff(f1218,plain,
( ~ mem(int,sF29,sF27)
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9
| ~ spl30_15
| spl30_24
| spl30_27 ),
inference(forward_subsumption_resolution,[],[f1217,f494]) ).
tff(f1219,plain,
( ~ spl30_23
| ~ spl30_1
| ~ spl30_8
| ~ spl30_9
| ~ spl30_15
| spl30_24
| spl30_27 ),
inference(avatar_split_clause,[],[f1218,f507,f492,f439,f409,f404,f373,f479]) ).
tff(f2094,plain,
( same_shape(int,a1,sF28,sF26)
| ~ same_shape(int,a1,sF22,sF20)
| ~ same_shape(int,a1,sF23,sF24)
| ~ spl30_8
| ~ spl30_11 ),
inference(superposition,[],[f1187,f406]) ).
tff(f2118,plain,
( ~ same_shape(int,a1,sF22,sF20)
| ~ same_shape(int,a1,sF23,sF24)
| spl30_6
| ~ spl30_8
| ~ spl30_11 ),
inference(forward_subsumption_resolution,[],[f2094,f397]) ).
tff(f2119,plain,
( ~ same_shape(int,a1,sF23,sF24)
| spl30_6
| ~ spl30_8
| ~ spl30_11
| ~ spl30_21 ),
inference(forward_subsumption_resolution,[],[f2118,f471]) ).
tff(f2120,plain,
( $false
| spl30_6
| ~ spl30_8
| ~ spl30_11
| ~ spl30_16
| ~ spl30_21 ),
inference(forward_subsumption_resolution,[],[f2119,f446]) ).
tff(f2121,plain,
( spl30_6
| ~ spl30_8
| ~ spl30_11
| ~ spl30_16
| ~ spl30_21 ),
inference(avatar_contradiction_clause,[],[f2120]) ).
tff(f2122,plain,
$false,
inference(avatar_smt_refutation,[],[f2121,f1219,f1125,f1089,f891,f511,f510,f500,f495,f482,f472,f467,f462,f447,f442,f437,f427,f422,f417,f412,f407,f402,f376]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW637_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 % Computer : n020.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 14:24:04 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.27 Running first-order theorem proving
% 0.09/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.79/1.43 % (198278)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.79/1.43 % (198284)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2887028549:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.79/1.43 % (198283)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=166562929:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.79/1.43 % (198289)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=69464327:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.79/1.43 % (198283)Instruction limit reached!
% 3.79/1.43 % (198283)------------------------------
% 3.79/1.43 % (198283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198283)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198283)Termination reason: Instruction limit
% 3.79/1.43 % (198283)Termination phase: Saturation
% 3.79/1.43 % (198283)Time elapsed: 0.041 s
% 3.79/1.43 % (198283)Peak memory usage: 112 MB
% 3.79/1.43 % (198283)Instructions burned: 12 (million)
% 3.79/1.43 % (198288)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2714608121:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.79/1.43 % (198286)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=495297513:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.79/1.43 % (198287)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1978525604:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.79/1.43 % (198285)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1541594920:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.79/1.43 % (198287)Instruction limit reached!
% 3.79/1.43 % (198287)------------------------------
% 3.79/1.43 % (198287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198287)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198287)Termination reason: Instruction limit
% 3.79/1.43 % (198287)Termination phase: Property scanning
% 3.79/1.43 % (198287)Time elapsed: 0.005 s
% 3.79/1.43 % (198287)Peak memory usage: 86 MB
% 3.79/1.43 % (198287)Instructions burned: 4 (million)
% 3.79/1.43 % (198286)Instruction limit reached!
% 3.79/1.43 % (198286)------------------------------
% 3.79/1.43 % (198286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198286)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198286)Termination reason: Instruction limit
% 3.79/1.43 % (198286)Termination phase: Saturation
% 3.79/1.43 % (198286)Time elapsed: 0.008 s
% 3.79/1.43 % (198286)Peak memory usage: 88 MB
% 3.79/1.43 % (198286)Instructions burned: 7 (million)
% 3.79/1.43 % (198289)Instruction limit reached!
% 3.79/1.43 % (198289)------------------------------
% 3.79/1.43 % (198289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198289)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198289)Termination reason: Instruction limit
% 3.79/1.43 % (198289)Termination phase: Saturation
% 3.79/1.43 % (198289)Time elapsed: 0.067 s
% 3.79/1.43 % (198289)Peak memory usage: 116 MB
% 3.79/1.43 % (198289)Instructions burned: 33 (million)
% 3.79/1.43 % (198284)First to succeed.
% 3.79/1.43 % (198284)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-198278"
% 3.79/1.43 % (198288)Instruction limit reached!
% 3.79/1.43 % (198288)------------------------------
% 3.79/1.43 % (198288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198288)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198288)Termination reason: Instruction limit
% 3.79/1.43 % (198288)Termination phase: Saturation
% 3.79/1.43 % (198288)Time elapsed: 0.080 s
% 3.79/1.43 % (198288)Peak memory usage: 116 MB
% 3.79/1.43 % (198288)Instructions burned: 46 (million)
% 3.79/1.43 % (198285)Instruction limit reached!
% 3.79/1.43 % (198285)------------------------------
% 3.79/1.43 % (198285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198285)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198285)Termination reason: Instruction limit
% 3.79/1.43 % (198285)Termination phase: Saturation
% 3.79/1.43 % (198285)Time elapsed: 0.224 s
% 3.79/1.43 % (198285)Peak memory usage: 118 MB
% 3.79/1.43 % (198285)Instructions burned: 201 (million)
% 3.79/1.43 % (198295)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1797928917:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 3.79/1.43 % (198301)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2289960412:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 3.79/1.43 % (198295)Instruction limit reached!
% 3.79/1.43 % (198295)------------------------------
% 3.79/1.43 % (198295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198295)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198295)Termination reason: Instruction limit
% 3.79/1.43 % (198295)Termination phase: Saturation
% 3.79/1.43 % (198295)Time elapsed: 0.017 s
% 3.79/1.43 % (198295)Peak memory usage: 88 MB
% 3.79/1.43 % (198295)Instructions burned: 14 (million)
% 3.79/1.43 % (198301)Instruction limit reached!
% 3.79/1.43 % (198301)------------------------------
% 3.79/1.43 % (198301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.43 % (198301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.43 % (198301)CaDiCaL version: 2.1.3
% 3.79/1.43 % (198301)Termination reason: Instruction limit
% 3.79/1.43 % (198301)Termination phase: Saturation
% 3.79/1.43 % (198301)Time elapsed: 0.017 s
% 3.79/1.43 % (198301)Peak memory usage: 88 MB
% 3.79/1.43 % (198301)Instructions burned: 16 (million)
% 3.79/1.43 % (198300)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2445042746:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 3.79/1.43 % (198284)Refutation found. Thanks to Tanya!
% 3.79/1.43 % SZS status Theorem for theBenchmark
% 3.79/1.43 % SZS output start Proof for theBenchmark
% See solution above
% 4.85/1.63 % (198284)------------------------------
% 4.85/1.63 % (198284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.63 % (198284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.63 % (198284)CaDiCaL version: 2.1.3
% 4.85/1.63 % (198284)Termination reason: Refutation
% 4.85/1.63 % (198284)Time elapsed: 0.119 s
% 4.85/1.63 % (198284)Peak memory usage: 118 MB
% 4.85/1.63 % (198284)Instructions burned: 168 (million)
% 4.85/1.63 % (198284)------------------------------
% 4.85/1.63 % (198284)------------------------------
% 4.85/1.63 % (198278)Success in time 0.566 s
% 4.85/1.63 % Vampire exiting
%------------------------------------------------------------------------------