%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW661_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 : n015.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:05 PM UTC 2026
% Result : Theorem 9.73s 2.40s
% Output : Refutation 11.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 37 ( 24 unt; 0 typ; 0 def)
% Number of atoms : 50 ( 49 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 13 ~; 0 |; 10 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 14 ( 12 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 82 ( 82 usr; 18 con; 0-5 aty)
% Number of variables : 124 ( 112 !; 12 ?; 124 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
loc1: $tType ).
tff(type_def_10,type,
node2: $tType ).
tff(type_def_11,type,
tree_loc: $tType ).
tff(type_def_12,type,
map_loc_node: $tType ).
tff(type_def_13,type,
a1: $tType ).
tff(type_def_14,type,
zipper_a: $tType ).
tff(type_def_15,type,
list_a: $tType ).
tff(type_def_16,type,
tree_a: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_10,type,
map: ( ty * ty ) > ty ).
tff(func_def_11,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_12,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_13,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_14,type,
ref: ty > ty ).
tff(func_def_15,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_16,type,
contents: ( ty * uni ) > uni ).
tff(func_def_17,type,
loc: ty ).
tff(func_def_18,type,
null1: loc1 ).
tff(func_def_19,type,
node: ty ).
tff(func_def_20,type,
mk_node1: ( loc1 * loc1 * $int ) > node2 ).
tff(func_def_21,type,
left2: node2 > loc1 ).
tff(func_def_22,type,
right1: node2 > loc1 ).
tff(func_def_23,type,
data1: node2 > $int ).
tff(func_def_24,type,
tree: ty > ty ).
tff(func_def_25,type,
empty: ty > uni ).
tff(func_def_26,type,
node1: ( ty * uni * uni * uni ) > uni ).
tff(func_def_27,type,
match_tree: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_28,type,
node_proj_1: ( ty * uni ) > uni ).
tff(func_def_29,type,
node_proj_2: ( ty * uni ) > uni ).
tff(func_def_30,type,
node_proj_3: ( ty * uni ) > uni ).
tff(func_def_31,type,
list: ty > ty ).
tff(func_def_32,type,
nil: ty > uni ).
tff(func_def_33,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_34,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_35,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_36,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_37,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_40,type,
length1: ( ty * uni ) > $int ).
tff(func_def_43,type,
inorder: ( ty * uni ) > uni ).
tff(func_def_44,type,
t2tb: tree_loc > uni ).
tff(func_def_45,type,
tb2t: uni > tree_loc ).
tff(func_def_46,type,
t2tb1: map_loc_node > uni ).
tff(func_def_47,type,
tb2t1: uni > map_loc_node ).
tff(func_def_48,type,
t2tb2: node2 > uni ).
tff(func_def_49,type,
tb2t2: uni > node2 ).
tff(func_def_50,type,
t2tb3: loc1 > uni ).
tff(func_def_51,type,
tb2t3: uni > loc1 ).
tff(func_def_52,type,
zipper: ty > ty ).
tff(func_def_53,type,
top: ty > uni ).
tff(func_def_54,type,
left1: ( ty * uni * uni * uni ) > uni ).
tff(func_def_55,type,
match_zipper1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_56,type,
left_proj_11: ( ty * uni ) > uni ).
tff(func_def_57,type,
left_proj_21: ( ty * uni ) > uni ).
tff(func_def_58,type,
left_proj_31: ( ty * uni ) > uni ).
tff(func_def_59,type,
zip: ( ty * uni * uni ) > uni ).
tff(func_def_60,type,
a: ty ).
tff(func_def_61,type,
t2tb4: zipper_a > uni ).
tff(func_def_62,type,
tb2t4: uni > zipper_a ).
tff(func_def_63,type,
t2tb5: a1 > uni ).
tff(func_def_64,type,
tb2t5: uni > a1 ).
tff(func_def_65,type,
t2tb6: list_a > uni ).
tff(func_def_66,type,
tb2t6: uni > list_a ).
tff(func_def_67,type,
t2tb7: tree_a > uni ).
tff(func_def_68,type,
tb2t7: uni > tree_a ).
tff(func_def_70,type,
sK2: ( ty * uni * uni ) > uni ).
tff(func_def_71,type,
sK3: ( ty * uni * uni ) > uni ).
tff(func_def_72,type,
sK4: ( ty * uni ) > uni ).
tff(func_def_73,type,
sK5: ( ty * uni ) > uni ).
tff(func_def_74,type,
sK6: ( ty * uni ) > uni ).
tff(func_def_75,type,
sK7: ( uni * uni * ty ) > uni ).
tff(func_def_76,type,
sK8: tree_a ).
tff(func_def_77,type,
sK9: a1 ).
tff(func_def_78,type,
sK10: zipper_a ).
tff(func_def_79,type,
sK11: a1 ).
tff(func_def_80,type,
sK12: tree_a ).
tff(func_def_81,type,
sK13: tree_a ).
tff(func_def_82,type,
sK14: ( tree_loc * loc1 * map_loc_node ) > loc1 ).
tff(func_def_83,type,
sK15: ( tree_loc * loc1 * map_loc_node ) > tree_loc ).
tff(func_def_84,type,
sK16: ( tree_loc * loc1 * map_loc_node ) > map_loc_node ).
tff(func_def_85,type,
sK17: ( tree_loc * loc1 * map_loc_node ) > tree_loc ).
tff(func_def_86,type,
sK18: ( loc1 * tree_loc * map_loc_node ) > map_loc_node ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
distinct: ( ty * uni ) > $o ).
tff(pred_def_5,type,
istree1: ( map_loc_node * loc1 * tree_loc ) > $o ).
tff(pred_def_7,type,
sP0: ( ty * uni ) > $o ).
tff(pred_def_8,type,
sP1: ( tree_loc * loc1 * map_loc_node ) > $o ).
tff(f47,axiom,
! [X1: uni,X0: ty] :
( ! [X3: uni,X2: uni] : ( infix_plpl(X0,cons(X0,X2,X3),X1) = cons(X0,X2,infix_plpl(X0,X3,X1)) )
& ( infix_plpl(X0,nil(X0),X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infix_plpl_def) ).
tff(f48,axiom,
! [X0: ty,X1: uni,X3: uni,X2: uni] : ( infix_plpl(X0,X1,infix_plpl(X0,X2,X3)) = infix_plpl(X0,infix_plpl(X0,X1,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',append_assoc) ).
tff(f59,axiom,
! [X0: ty] :
( ( inorder(X0,empty(X0)) = nil(X0) )
& ! [X3: uni,X2: uni,X1: uni] : ( inorder(X0,node1(X0,X1,X2,X3)) = infix_plpl(X0,inorder(X0,X1),cons(X0,X2,inorder(X0,X3))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inorder_def) ).
tff(f94,axiom,
! [X0: ty,X1: uni] :
( ! [X2: uni,X4: uni,X3: uni] : ( zip(X0,X1,left1(X0,X2,X3,X4)) = zip(X0,node1(X0,X1,X3,X4),X2) )
& ( zip(X0,X1,top(X0)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zip_def) ).
tff(f103,axiom,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR6) ).
tff(f106,axiom,
! [X0: uni] : ( t2tb7(tb2t7(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR7) ).
tff(f107,conjecture,
! [X2: tree_a,X1: a1,X0: zipper_a] :
( ! [X5: tree_a,X4: tree_a,X3: a1] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X4),t2tb5(X3),t2tb7(X5)),t2tb4(X0)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X4)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X5),t2tb4(X0)))))) )
=> ! [X5: tree_a,X3: a1,X4: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X4),t2tb5(X3),t2tb7(X5)),left1(a,t2tb4(X0),t2tb5(X1),t2tb7(X2))))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X4)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X5),left1(a,t2tb4(X0),t2tb5(X1),t2tb7(X2))))))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inorder_zip) ).
tff(f108,negated_conjecture,
~ ! [X2: tree_a,X1: a1,X0: zipper_a] :
( ! [X5: tree_a,X4: tree_a,X3: a1] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X4),t2tb5(X3),t2tb7(X5)),t2tb4(X0)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X4)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X5),t2tb4(X0)))))) )
=> ! [X5: tree_a,X3: a1,X4: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X4),t2tb5(X3),t2tb7(X5)),left1(a,t2tb4(X0),t2tb5(X1),t2tb7(X2))))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X4)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X5),left1(a,t2tb4(X0),t2tb5(X1),t2tb7(X2))))))) ) ),
inference(negated_conjecture,[status(cth)],[f107]) ).
tff(f153,plain,
! [X3: uni,X2: uni,X0: ty,X1: uni] : ( infix_plpl(X0,X1,infix_plpl(X0,X3,X2)) = infix_plpl(X0,infix_plpl(X0,X1,X3),X2) ),
inference(rectify,[],[f48]) ).
tff(f177,plain,
~ ! [X2: zipper_a,X0: tree_a,X1: a1] :
( ! [X5: a1,X3: tree_a,X4: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X4),t2tb5(X5),t2tb7(X3)),t2tb4(X2)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X4)),cons(a,t2tb5(X5),inorder(a,zip(a,t2tb7(X3),t2tb4(X2)))))) )
=> ! [X8: tree_a,X6: tree_a,X7: a1] : ( tb2t6(infix_plpl(a,inorder(a,t2tb7(X8)),cons(a,t2tb5(X7),inorder(a,zip(a,t2tb7(X6),left1(a,t2tb4(X2),t2tb5(X1),t2tb7(X0))))))) = tb2t6(inorder(a,zip(a,node1(a,t2tb7(X8),t2tb5(X7),t2tb7(X6)),left1(a,t2tb4(X2),t2tb5(X1),t2tb7(X0))))) ) ),
inference(rectify,[],[f108]) ).
tff(f178,plain,
! [X1: uni,X0: ty] :
( ( zip(X0,X1,top(X0)) = X1 )
& ! [X3: uni,X4: uni,X2: uni] : ( zip(X0,node1(X0,X1,X4,X3),X2) = zip(X0,X1,left1(X0,X2,X4,X3)) ) ),
inference(rectify,[],[f94]) ).
tff(f204,plain,
? [X0: tree_a,X1: a1,X2: zipper_a] :
( ! [X5: a1,X3: tree_a,X4: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X4),t2tb5(X5),t2tb7(X3)),t2tb4(X2)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X4)),cons(a,t2tb5(X5),inorder(a,zip(a,t2tb7(X3),t2tb4(X2)))))) )
& ? [X7: a1,X8: tree_a,X6: tree_a] : ( tb2t6(infix_plpl(a,inorder(a,t2tb7(X8)),cons(a,t2tb5(X7),inorder(a,zip(a,t2tb7(X6),left1(a,t2tb4(X2),t2tb5(X1),t2tb7(X0))))))) != tb2t6(inorder(a,zip(a,node1(a,t2tb7(X8),t2tb5(X7),t2tb7(X6)),left1(a,t2tb4(X2),t2tb5(X1),t2tb7(X0))))) ) ),
inference(ennf_transformation,[],[f177]) ).
tff(f244,plain,
! [X0: uni,X1: ty] :
( ( zip(X1,X0,top(X1)) = X0 )
& ! [X2: uni,X3: uni,X4: uni] : ( zip(X1,node1(X1,X0,X3,X2),X4) = zip(X1,X0,left1(X1,X4,X3,X2)) ) ),
inference(rectify,[],[f178]) ).
tff(f254,plain,
! [X0: uni,X1: ty] :
( ! [X2: uni,X3: uni] : ( cons(X1,X3,infix_plpl(X1,X2,X0)) = infix_plpl(X1,cons(X1,X3,X2),X0) )
& ( infix_plpl(X1,nil(X1),X0) = X0 ) ),
inference(rectify,[],[f47]) ).
tff(f261,plain,
? [X0: tree_a,X1: a1,X2: zipper_a] :
( ! [X3: a1,X4: tree_a,X5: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X5),t2tb5(X3),t2tb7(X4)),t2tb4(X2)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X5)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X4),t2tb4(X2)))))) )
& ? [X6: a1,X7: tree_a,X8: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X7),t2tb5(X6),t2tb7(X8)),left1(a,t2tb4(X2),t2tb5(X1),t2tb7(X0))))) != tb2t6(infix_plpl(a,inorder(a,t2tb7(X7)),cons(a,t2tb5(X6),inorder(a,zip(a,t2tb7(X8),left1(a,t2tb4(X2),t2tb5(X1),t2tb7(X0))))))) ) ),
inference(rectify,[],[f204]) ).
tff(f262,plain,
( ! [X3: a1,X4: tree_a,X5: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X5),t2tb5(X3),t2tb7(X4)),t2tb4(sK10)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X5)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X4),t2tb4(sK10)))))) )
& ( tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,zip(a,t2tb7(sK13),left1(a,t2tb4(sK10),t2tb5(sK9),t2tb7(sK8))))))) != tb2t6(inorder(a,zip(a,node1(a,t2tb7(sK12),t2tb5(sK11),t2tb7(sK13)),left1(a,t2tb4(sK10),t2tb5(sK9),t2tb7(sK8))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12,sK13]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X6,sK11),skolemize(X7,sK12),skolemize(X8,sK13)],[f261]) ).
tff(f265,plain,
! [X0: uni,X1: uni,X2: ty,X3: uni] : ( infix_plpl(X2,X3,infix_plpl(X2,X0,X1)) = infix_plpl(X2,infix_plpl(X2,X3,X0),X1) ),
inference(rectify,[],[f153]) ).
tff(f270,plain,
! [X0: ty] :
( ( inorder(X0,empty(X0)) = nil(X0) )
& ! [X1: uni,X2: uni,X3: uni] : ( infix_plpl(X0,inorder(X0,X3),cons(X0,X2,inorder(X0,X1))) = inorder(X0,node1(X0,X3,X2,X1)) ) ),
inference(rectify,[],[f59]) ).
tff(f327,plain,
! [X0: uni] : ( t2tb6(tb2t6(X0)) = X0 ),
inference(cnf_transformation,[],[f103]) ).
tff(f340,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty,X4: uni] : ( zip(X1,node1(X1,X0,X3,X2),X4) = zip(X1,X0,left1(X1,X4,X3,X2)) ),
inference(cnf_transformation,[],[f244]) ).
tff(f355,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] : ( cons(X1,X3,infix_plpl(X1,X2,X0)) = infix_plpl(X1,cons(X1,X3,X2),X0) ),
inference(cnf_transformation,[],[f254]) ).
tff(f365,plain,
tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,zip(a,t2tb7(sK13),left1(a,t2tb4(sK10),t2tb5(sK9),t2tb7(sK8))))))) != tb2t6(inorder(a,zip(a,node1(a,t2tb7(sK12),t2tb5(sK11),t2tb7(sK13)),left1(a,t2tb4(sK10),t2tb5(sK9),t2tb7(sK8))))),
inference(cnf_transformation,[],[f262]) ).
tff(f366,plain,
! [X3: a1,X4: tree_a,X5: tree_a] : ( tb2t6(inorder(a,zip(a,node1(a,t2tb7(X5),t2tb5(X3),t2tb7(X4)),t2tb4(sK10)))) = tb2t6(infix_plpl(a,inorder(a,t2tb7(X5)),cons(a,t2tb5(X3),inorder(a,zip(a,t2tb7(X4),t2tb4(sK10)))))) ),
inference(cnf_transformation,[],[f262]) ).
tff(f375,plain,
! [X2: ty,X3: uni,X0: uni,X1: uni] : ( infix_plpl(X2,X3,infix_plpl(X2,X0,X1)) = infix_plpl(X2,infix_plpl(X2,X3,X0),X1) ),
inference(cnf_transformation,[],[f265]) ).
tff(f386,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] : ( infix_plpl(X0,inorder(X0,X3),cons(X0,X2,inorder(X0,X1))) = inorder(X0,node1(X0,X3,X2,X1)) ),
inference(cnf_transformation,[],[f270]) ).
tff(f403,plain,
! [X0: uni] : ( t2tb7(tb2t7(X0)) = X0 ),
inference(cnf_transformation,[],[f106]) ).
tff(f447,plain,
tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,zip(a,t2tb7(sK13),left1(a,t2tb4(sK10),t2tb5(sK9),t2tb7(sK8))))))) != tb2t6(inorder(a,zip(a,node1(a,node1(a,t2tb7(sK12),t2tb5(sK11),t2tb7(sK13)),t2tb5(sK9),t2tb7(sK8)),t2tb4(sK10)))),
inference(forward_demodulation,[],[f365,f340]) ).
tff(f448,plain,
tb2t6(inorder(a,zip(a,node1(a,node1(a,t2tb7(sK12),t2tb5(sK11),t2tb7(sK13)),t2tb5(sK9),t2tb7(sK8)),t2tb4(sK10)))) != tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,zip(a,node1(a,t2tb7(sK13),t2tb5(sK9),t2tb7(sK8)),t2tb4(sK10)))))),
inference(forward_demodulation,[],[f447,f340]) ).
tff(f449,plain,
! [X2: tree_a,X0: uni,X1: a1] : ( tb2t6(inorder(a,zip(a,node1(a,X0,t2tb5(X1),t2tb7(X2)),t2tb4(sK10)))) = tb2t6(infix_plpl(a,inorder(a,X0),cons(a,t2tb5(X1),inorder(a,zip(a,t2tb7(X2),t2tb4(sK10)))))) ),
inference(superposition,[],[f366,f403]) ).
tff(f452,plain,
! [X2: tree_a,X0: tree_a,X1: a1] : ( t2tb6(tb2t6(infix_plpl(a,inorder(a,t2tb7(X0)),cons(a,t2tb5(X1),inorder(a,zip(a,t2tb7(X2),t2tb4(sK10))))))) = inorder(a,zip(a,node1(a,t2tb7(X0),t2tb5(X1),t2tb7(X2)),t2tb4(sK10))) ),
inference(superposition,[],[f327,f366]) ).
tff(f453,plain,
! [X2: tree_a,X0: tree_a,X1: a1] : ( infix_plpl(a,inorder(a,t2tb7(X0)),cons(a,t2tb5(X1),inorder(a,zip(a,t2tb7(X2),t2tb4(sK10))))) = inorder(a,zip(a,node1(a,t2tb7(X0),t2tb5(X1),t2tb7(X2)),t2tb4(sK10))) ),
inference(forward_demodulation,[],[f452,f327]) ).
tff(f456,plain,
tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,zip(a,node1(a,t2tb7(sK13),t2tb5(sK9),t2tb7(sK8)),t2tb4(sK10)))))) != tb2t6(infix_plpl(a,inorder(a,node1(a,t2tb7(sK12),t2tb5(sK11),t2tb7(sK13))),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))),
inference(superposition,[],[f448,f449]) ).
tff(f458,plain,
tb2t6(infix_plpl(a,infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,t2tb7(sK13)))),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))) != tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,zip(a,node1(a,t2tb7(sK13),t2tb5(sK9),t2tb7(sK8)),t2tb4(sK10)))))),
inference(forward_demodulation,[],[f456,f386]) ).
tff(f460,plain,
tb2t6(infix_plpl(a,infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),inorder(a,t2tb7(sK13)))),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))) != tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),infix_plpl(a,inorder(a,t2tb7(sK13)),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))))),
inference(forward_demodulation,[],[f458,f453]) ).
tff(f461,plain,
tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),infix_plpl(a,cons(a,t2tb5(sK11),inorder(a,t2tb7(sK13))),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10))))))) != tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),infix_plpl(a,inorder(a,t2tb7(sK13)),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))))),
inference(forward_demodulation,[],[f460,f375]) ).
tff(f462,plain,
tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),infix_plpl(a,inorder(a,t2tb7(sK13)),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))))) != tb2t6(infix_plpl(a,inorder(a,t2tb7(sK12)),cons(a,t2tb5(sK11),infix_plpl(a,inorder(a,t2tb7(sK13)),cons(a,t2tb5(sK9),inorder(a,zip(a,t2tb7(sK8),t2tb4(sK10)))))))),
inference(forward_demodulation,[],[f461,f355]) ).
tff(f463,plain,
$false,
inference(trivial_inequality_removal,[],[f462]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW661_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.22 % Computer : n015.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 14:27:32 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.28 Running first-order theorem proving
% 0.26/0.28 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
% 5.23/1.71 % (2665961)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.23/1.71 % (2665971)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=4032015155:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.23/1.71 % (2665972)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1866009367:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.23/1.71 % (2665971)Instruction limit reached!
% 5.23/1.71 % (2665971)------------------------------
% 5.23/1.71 % (2665971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.71 % (2665971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.71 % (2665971)CaDiCaL version: 2.1.3
% 5.23/1.71 % (2665971)Termination reason: Instruction limit
% 5.23/1.71 % (2665971)Termination phase: Saturation
% 5.23/1.71 % (2665971)Time elapsed: 0.042 s
% 5.23/1.71 % (2665971)Peak memory usage: 116 MB
% 5.23/1.71 % (2665971)Instructions burned: 46 (million)
% 5.23/1.71 % (2665972)Instruction limit reached!
% 5.23/1.71 % (2665972)------------------------------
% 5.23/1.71 % (2665972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.71 % (2665972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.71 % (2665972)CaDiCaL version: 2.1.3
% 5.23/1.71 % (2665972)Termination reason: Instruction limit
% 5.23/1.71 % (2665972)Termination phase: Saturation
% 5.23/1.71 % (2665972)Time elapsed: 0.066 s
% 5.23/1.71 % (2665972)Peak memory usage: 116 MB
% 5.23/1.71 % (2665972)Instructions burned: 33 (million)
% 5.23/1.71 % (2665966)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1657458316:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.23/1.71 % (2665968)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1807853531:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.23/1.71 % (2665970)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=243579571:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.23/1.71 % (2665967)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=266961724:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.23/1.71 % (2665970)Instruction limit reached!
% 5.23/1.71 % (2665970)------------------------------
% 5.23/1.71 % (2665970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.71 % (2665970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.71 % (2665970)CaDiCaL version: 2.1.3
% 5.23/1.71 % (2665970)Termination reason: Instruction limit
% 5.23/1.71 % (2665970)Termination phase: Preprocessing 3
% 5.23/1.71 % (2665970)Time elapsed: 0.005 s
% 5.23/1.71 % (2665970)Peak memory usage: 86 MB
% 5.23/1.71 % (2665970)Instructions burned: 4 (million)
% 5.23/1.71 % (2665969)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1649619422:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.23/1.71 % (2665969)Instruction limit reached!
% 5.23/1.71 % (2665969)------------------------------
% 5.23/1.71 % (2665969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.71 % (2665969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.71 % (2665969)CaDiCaL version: 2.1.3
% 5.23/1.71 % (2665969)Termination reason: Instruction limit
% 5.23/1.71 % (2665969)Termination phase: Property scanning
% 5.23/1.71 % (2665969)Time elapsed: 0.008 s
% 5.23/1.71 % (2665969)Peak memory usage: 86 MB
% 5.23/1.71 % (2665969)Instructions burned: 7 (million)
% 5.23/1.71 % (2665966)Instruction limit reached!
% 5.23/1.71 % (2665966)------------------------------
% 5.23/1.71 % (2665966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.23/1.71 % (2665966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.23/1.71 % (2665966)CaDiCaL version: 2.1.3
% 5.23/1.71 % (2665966)Termination reason: Instruction limit
% 5.23/1.71 % (2665966)Termination phase: Saturation
% 5.23/1.71 % (2665966)Time elapsed: 0.041 s
% 5.23/1.71 % (2665966)Peak memory usage: 115 MB
% 5.23/1.71 % (2665966)Instructions burned: 12 (million)
% 5.23/1.71 % (2665982)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1310362373:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.23/1.71 % (2665975)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3463551164:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 7.16/1.98 % (2665982)Instruction limit reached!
% 7.16/1.98 % (2665982)------------------------------
% 7.16/1.98 % (2665982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.98 % (2665982)CaDiCaL version: 2.1.3
% 7.16/1.98 % (2665982)Termination reason: Instruction limit
% 7.16/1.98 % (2665982)Termination phase: Saturation
% 7.16/1.98 % (2665982)Time elapsed: 0.010 s
% 7.16/1.98 % (2665982)Peak memory usage: 89 MB
% 7.16/1.98 % (2665982)Instructions burned: 18 (million)
% 7.16/1.98 % (2665975)Instruction limit reached!
% 7.16/1.98 % (2665975)------------------------------
% 7.16/1.98 % (2665975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.98 % (2665975)CaDiCaL version: 2.1.3
% 7.16/1.98 % (2665975)Termination reason: Instruction limit
% 7.16/1.98 % (2665975)Termination phase: Saturation
% 7.16/1.98 % (2665975)Time elapsed: 0.016 s
% 7.16/1.98 % (2665975)Peak memory usage: 88 MB
% 7.16/1.98 % (2665975)Instructions burned: 14 (million)
% 7.16/1.98 % (2665984)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3420340227:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.16/1.98 % (2665968)Instruction limit reached!
% 7.16/1.98 % (2665968)------------------------------
% 7.16/1.98 % (2665968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.98 % (2665968)CaDiCaL version: 2.1.3
% 7.16/1.98 % (2665968)Termination reason: Instruction limit
% 7.16/1.98 % (2665968)Termination phase: Saturation
% 7.16/1.98 % (2665968)Time elapsed: 0.235 s
% 7.16/1.98 % (2665968)Peak memory usage: 118 MB
% 7.16/1.98 % (2665968)Instructions burned: 201 (million)
% 7.16/1.98 % (2665984)Instruction limit reached!
% 7.16/1.98 % (2665984)------------------------------
% 7.16/1.98 % (2665984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.98 % (2665984)CaDiCaL version: 2.1.3
% 7.16/1.98 % (2665984)Termination reason: Instruction limit
% 7.16/1.98 % (2665984)Termination phase: Saturation
% 7.16/1.98 % (2665984)Time elapsed: 0.020 s
% 7.16/1.98 % (2665984)Peak memory usage: 89 MB
% 7.16/1.98 % (2665984)Instructions burned: 28 (million)
% 7.16/1.98 % (2665983)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=640120922:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 7.16/1.98 % (2665981)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=657424733:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 7.16/1.98 % (2665983)Instruction limit reached!
% 7.16/1.98 % (2665983)------------------------------
% 7.16/1.98 % (2665983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.98 % (2665983)CaDiCaL version: 2.1.3
% 7.16/1.98 % (2665983)Termination reason: Instruction limit
% 7.16/1.98 % (2665983)Termination phase: Saturation
% 7.16/1.98 % (2665983)Time elapsed: 0.028 s
% 7.16/1.98 % (2665983)Peak memory usage: 89 MB
% 7.16/1.98 % (2665983)Instructions burned: 24 (million)
% 7.16/1.98 % (2665981)Instruction limit reached!
% 7.16/1.98 % (2665981)------------------------------
% 7.16/1.98 % (2665981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.16/1.98 % (2665981)CaDiCaL version: 2.1.3
% 7.16/1.98 % (2665981)Termination reason: Instruction limit
% 7.16/1.98 % (2665981)Termination phase: Saturation
% 7.16/1.98 % (2665981)Time elapsed: 0.031 s
% 7.16/1.98 % (2665981)Peak memory usage: 89 MB
% 7.16/1.98 % (2665981)Instructions burned: 29 (million)
% 7.16/1.98 % (2665967)Instruction limit reached!
% 7.16/1.98 % (2665967)------------------------------
% 7.16/1.98 % (2665967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.16/1.98 % (2665967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.31 % (2665967)CaDiCaL version: 2.1.3
% 9.73/2.31 % (2665967)Termination reason: Instruction limit
% 9.73/2.31 % (2665967)Termination phase: Saturation
% 9.73/2.31 % (2665967)Time elapsed: 0.332 s
% 9.73/2.31 % (2665967)Peak memory usage: 118 MB
% 9.73/2.31 % (2665967)Instructions burned: 307 (million)
% 9.73/2.31 % (2665989)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1473936536:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.73/2.31 % (2665989)Instruction limit reached!
% 9.73/2.31 % (2665989)------------------------------
% 9.73/2.31 % (2665989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.31 % (2665989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.31 % (2665989)CaDiCaL version: 2.1.3
% 9.73/2.31 % (2665989)Termination reason: Instruction limit
% 9.73/2.31 % (2665989)Termination phase: Property scanning
% 9.73/2.31 % (2665989)Time elapsed: 0.003 s
% 9.73/2.31 % (2665989)Peak memory usage: 86 MB
% 9.73/2.31 % (2665989)Instructions burned: 5 (million)
% 9.73/2.31 % (2665987)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2284268656:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 9.73/2.31 % (2665992)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4140533266:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.73/2.31 % (2665995)lrs+10_1_thi=all:si=on:fd=off:random_seed=2343615663:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 9.73/2.31 % (2665993)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=4072547788:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.73/2.31 % (2665993)Instruction limit reached!
% 9.73/2.31 % (2665993)------------------------------
% 9.73/2.31 % (2665993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.31 % (2665993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.31 % (2665993)CaDiCaL version: 2.1.3
% 9.73/2.31 % (2665993)Termination reason: Instruction limit
% 9.73/2.31 % (2665993)Termination phase: Preprocessing 3
% 9.73/2.31 % (2665993)Time elapsed: 0.005 s
% 9.73/2.31 % (2665993)Peak memory usage: 86 MB
% 9.73/2.31 % (2665993)Instructions burned: 4 (million)
% 9.73/2.31 % (2665987)Instruction limit reached!
% 9.73/2.31 % (2665987)------------------------------
% 9.73/2.31 % (2665987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.31 % (2665987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.31 % (2665987)CaDiCaL version: 2.1.3
% 9.73/2.31 % (2665987)Termination reason: Instruction limit
% 9.73/2.31 % (2665987)Termination phase: Saturation
% 9.73/2.31 % (2665987)Time elapsed: 0.073 s
% 9.73/2.31 % (2665987)Peak memory usage: 89 MB
% 9.73/2.31 % (2665987)Instructions burned: 85 (million)
% 9.73/2.31 % (2665994)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=290042003:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.73/2.31 % (2665996)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=3106769459:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 9.73/2.31 % (2665996)Instruction limit reached!
% 9.73/2.31 % (2665996)------------------------------
% 9.73/2.31 % (2665996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.31 % (2665996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.31 % (2665996)CaDiCaL version: 2.1.3
% 9.73/2.31 % (2665996)Termination reason: Instruction limit
% 9.73/2.31 % (2665996)Termination phase: Function definition elimination
% 9.73/2.31 % (2665996)Time elapsed: 0.004 s
% 9.73/2.31 % (2665996)Peak memory usage: 86 MB
% 9.73/2.31 % (2665996)Instructions burned: 8 (million)
% 9.73/2.31 % (2665995)Instruction limit reached!
% 9.73/2.31 % (2665995)------------------------------
% 9.73/2.31 % (2665995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.31 % (2665995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.31 % (2665995)CaDiCaL version: 2.1.3
% 9.73/2.31 % (2665995)Termination reason: Instruction limit
% 9.73/2.31 % (2665995)Termination phase: Saturation
% 9.73/2.31 % (2665995)Time elapsed: 0.079 s
% 9.73/2.31 % (2665995)Peak memory usage: 115 MB
% 9.73/2.31 % (2665995)Instructions burned: 53 (million)
% 9.73/2.40 % (2665998)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4242479019:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 9.73/2.40 % (2665998)Instruction limit reached!
% 9.73/2.40 % (2665998)------------------------------
% 9.73/2.40 % (2665998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2665998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2665998)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2665998)Termination reason: Instruction limit
% 9.73/2.40 % (2665998)Termination phase: shuffling
% 9.73/2.40 % (2665998)Time elapsed: 0.003 s
% 9.73/2.40 % (2665998)Peak memory usage: 85 MB
% 9.73/2.40 % (2665998)Instructions burned: 2 (million)
% 9.73/2.40 % (2665992)Instruction limit reached!
% 9.73/2.40 % (2665992)------------------------------
% 9.73/2.40 % (2665992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2665992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2665992)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2665992)Termination reason: Instruction limit
% 9.73/2.40 % (2665992)Termination phase: Saturation
% 9.73/2.40 % (2665992)Time elapsed: 0.181 s
% 9.73/2.40 % (2665992)Peak memory usage: 91 MB
% 9.73/2.40 % (2665992)Instructions burned: 182 (million)
% 9.73/2.40 % (2665994)Instruction limit reached!
% 9.73/2.40 % (2665994)------------------------------
% 9.73/2.40 % (2665994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2665994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2665994)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2665994)Termination reason: Instruction limit
% 9.73/2.40 % (2665994)Termination phase: Saturation
% 9.73/2.40 % (2665994)Time elapsed: 0.136 s
% 9.73/2.40 % (2665994)Peak memory usage: 134 MB
% 9.73/2.40 % (2665994)Instructions burned: 66 (million)
% 9.73/2.40 % (2666005)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=40892227:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi)
% 9.73/2.40 % (2666003)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=97142171:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 9.73/2.40 % (2666003)Instruction limit reached!
% 9.73/2.40 % (2666003)------------------------------
% 9.73/2.40 % (2666003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666003)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666003)Termination reason: Instruction limit
% 9.73/2.40 % (2666003)Termination phase: Preprocessing 1
% 9.73/2.40 % (2666003)Time elapsed: 0.003 s
% 9.73/2.40 % (2666003)Peak memory usage: 85 MB
% 9.73/2.40 % (2666003)Instructions burned: 2 (million)
% 9.73/2.40 % (2666007)dis+10_1_si=on:random_seed=1632192165:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 9.73/2.40 % (2666007)Instruction limit reached!
% 9.73/2.40 % (2666007)------------------------------
% 9.73/2.40 % (2666007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666007)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666007)Termination reason: Instruction limit
% 9.73/2.40 % (2666007)Termination phase: Saturation
% 9.73/2.40 % (2666007)Time elapsed: 0.006 s
% 9.73/2.40 % (2666007)Peak memory usage: 88 MB
% 9.73/2.40 % (2666007)Instructions burned: 11 (million)
% 9.73/2.40 % (2666010)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=737408622:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2991 on theBenchmark for (2991ds/35Mi)
% 9.73/2.40 % (2666008)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=719417584:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 9.73/2.40 % (2666008)First to succeed.
% 9.73/2.40 % (2666010)Instruction limit reached!
% 9.73/2.40 % (2666010)------------------------------
% 9.73/2.40 % (2666010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666010)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666010)Termination reason: Instruction limit
% 9.73/2.40 % (2666010)Termination phase: Saturation
% 9.73/2.40 % (2666010)Time elapsed: 0.041 s
% 9.73/2.40 % (2666010)Peak memory usage: 89 MB
% 9.73/2.40 % (2666010)Instructions burned: 35 (million)
% 9.73/2.40 % (2666008)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2665961"
% 9.73/2.40 % (2666005)Instruction limit reached!
% 9.73/2.40 % (2666005)------------------------------
% 9.73/2.40 % (2666005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666005)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666005)Termination reason: Instruction limit
% 9.73/2.40 % (2666005)Termination phase: Saturation
% 9.73/2.40 % (2666005)Time elapsed: 0.151 s
% 9.73/2.40 % (2666005)Peak memory usage: 117 MB
% 9.73/2.40 % (2666005)Instructions burned: 129 (million)
% 9.73/2.40 % (2666011)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=642995298:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 9.73/2.40 % (2666011)Instruction limit reached!
% 9.73/2.40 % (2666011)------------------------------
% 9.73/2.40 % (2666011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666011)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666011)Termination reason: Instruction limit
% 9.73/2.40 % (2666011)Termination phase: shuffling
% 9.73/2.40 % (2666011)Time elapsed: 0.003 s
% 9.73/2.40 % (2666011)Peak memory usage: 86 MB
% 9.73/2.40 % (2666011)Instructions burned: 3 (million)
% 9.73/2.40 % (2666017)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1786729893:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 9.73/2.40 % (2666012)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2284524546:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 9.73/2.40 % (2666012)Instruction limit reached!
% 9.73/2.40 % (2666012)------------------------------
% 9.73/2.40 % (2666012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666012)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666012)Termination reason: Instruction limit
% 9.73/2.40 % (2666012)Termination phase: Saturation
% 9.73/2.40 % (2666012)Time elapsed: 0.008 s
% 9.73/2.40 % (2666012)Peak memory usage: 87 MB
% 9.73/2.40 % (2666012)Instructions burned: 8 (million)
% 9.73/2.40 % (2666017)Instruction limit reached!
% 9.73/2.40 % (2666017)------------------------------
% 9.73/2.40 % (2666017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666017)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666017)Termination reason: Instruction limit
% 9.73/2.40 % (2666017)Termination phase: Saturation
% 9.73/2.40 % (2666017)Time elapsed: 0.025 s
% 9.73/2.40 % (2666017)Peak memory usage: 112 MB
% 9.73/2.40 % (2666017)Instructions burned: 15 (million)
% 9.73/2.40 % (2666016)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1739225269:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 9.73/2.40 % (2666020)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3337893484:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 9.73/2.40 % (2666023)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2284736431:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 9.73/2.40 % (2666022)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=563764796:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 9.73/2.40 % (2666022)Instruction limit reached!
% 9.73/2.40 % (2666022)------------------------------
% 9.73/2.40 % (2666022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666022)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666022)Termination reason: Instruction limit
% 9.73/2.40 % (2666022)Termination phase: Saturation
% 9.73/2.40 % (2666022)Time elapsed: 0.012 s
% 9.73/2.40 % (2666022)Peak memory usage: 88 MB
% 9.73/2.40 % (2666022)Instructions burned: 10 (million)
% 9.73/2.40 % (2666026)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=2673362204:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 9.73/2.40 % (2666026)Instruction limit reached!
% 9.73/2.40 % (2666026)------------------------------
% 9.73/2.40 % (2666026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666026)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666026)Termination reason: Instruction limit
% 9.73/2.40 % (2666026)Termination phase: Saturation
% 9.73/2.40 % (2666026)Time elapsed: 0.039 s
% 9.73/2.40 % (2666026)Peak memory usage: 90 MB
% 9.73/2.40 % (2666026)Instructions burned: 76 (million)
% 9.73/2.40 % (2666023)Instruction limit reached!
% 9.73/2.40 % (2666023)------------------------------
% 9.73/2.40 % (2666023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.73/2.40 % (2666023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.73/2.40 % (2666023)CaDiCaL version: 2.1.3
% 9.73/2.40 % (2666023)Termination reason: Instruction limit
% 9.73/2.40 % (2666023)Termination phase: Saturation
% 9.73/2.40 % (2666023)Time elapsed: 0.117 s
% 9.73/2.40 % (2666023)Peak memory usage: 132 MB
% 9.73/2.40 % (2666023)Instructions burned: 71 (million)
% 9.73/2.40 % (2666008)Refutation found. Thanks to Tanya!
% 9.73/2.40 % SZS status Theorem for theBenchmark
% 9.73/2.40 % SZS output start Proof for theBenchmark
% See solution above
% 11.48/2.64 % (2666008)------------------------------
% 11.48/2.64 % (2666008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.48/2.64 % (2666008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.48/2.64 % (2666008)CaDiCaL version: 2.1.3
% 11.48/2.64 % (2666008)Termination reason: Refutation
% 11.48/2.64 % (2666008)Time elapsed: 0.020 s
% 11.48/2.64 % (2666008)Peak memory usage: 89 MB
% 11.48/2.64 % (2666008)Instructions burned: 18 (million)
% 11.48/2.64 % (2666008)------------------------------
% 11.48/2.64 % (2666008)------------------------------
% 11.48/2.64 % (2665961)Success in time 1.521 s
% 11.48/2.64 % Vampire exiting
%------------------------------------------------------------------------------