%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW587_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 : n012.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:30:52 PM UTC 2026
% Result : Theorem 7.20s 1.62s
% Output : Refutation 8.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 45
% Syntax : Number of formulae : 257 ( 84 unt; 0 typ; 35 def)
% Number of atoms : 1694 ( 427 equ)
% Maximal formula atoms : 92 ( 6 avg)
% Number of connectives : 2036 ( 599 ~; 544 |; 612 &)
% ( 38 <=>; 243 =>; 0 <=; 0 <~>)
% Maximal formula depth : 69 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 264 ( 108 atm; 96 fun; 36 num; 24 var)
% Number of types : 9 ( 7 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 30 ( 26 usr; 15 prp; 0-6 aty)
% Number of functors : 155 ( 153 usr; 99 con; 0-5 aty)
% Number of variables : 670 ( 0 sgn 532 !; 138 ?; 670 :)
% 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,
vertex1: $tType ).
tff(type_def_10,type,
set_vertex: $tType ).
tff(type_def_11,type,
map_vertex_int: $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_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
set: ty > ty ).
tff(func_def_16,type,
empty: ty > uni ).
tff(func_def_17,type,
add: ( ty * uni * uni ) > uni ).
tff(func_def_18,type,
remove: ( ty * uni * uni ) > uni ).
tff(func_def_19,type,
union: ( ty * uni * uni ) > uni ).
tff(func_def_20,type,
inter: ( ty * uni * uni ) > uni ).
tff(func_def_21,type,
diff: ( ty * uni * uni ) > uni ).
tff(func_def_22,type,
choose: ( ty * uni ) > uni ).
tff(func_def_23,type,
cardinal1: ( ty * uni ) > $int ).
tff(func_def_26,type,
map: ( ty * ty ) > ty ).
tff(func_def_27,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_28,type,
set1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_29,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_30,type,
vertex: ty ).
tff(func_def_31,type,
v1: set_vertex ).
tff(func_def_32,type,
g_succ1: vertex1 > set_vertex ).
tff(func_def_33,type,
t2tb: set_vertex > uni ).
tff(func_def_34,type,
tb2t: uni > set_vertex ).
tff(func_def_35,type,
weight1: ( vertex1 * vertex1 ) > $int ).
tff(func_def_36,type,
t2tb1: map_vertex_int > uni ).
tff(func_def_37,type,
tb2t1: uni > map_vertex_int ).
tff(func_def_38,type,
t2tb2: vertex1 > uni ).
tff(func_def_39,type,
tb2t2: uni > vertex1 ).
tff(func_def_40,type,
t2tb3: $int > uni ).
tff(func_def_41,type,
tb2t3: uni > $int ).
tff(func_def_44,type,
sK0: ( vertex1 * $int * vertex1 ) > $int ).
tff(func_def_45,type,
sK1: ( uni * uni * ty ) > uni ).
tff(func_def_46,type,
sK2: vertex1 ).
tff(func_def_47,type,
sK3: vertex1 ).
tff(func_def_48,type,
sK4: map_vertex_int ).
tff(func_def_49,type,
sK5: set_vertex ).
tff(func_def_50,type,
sK6: set_vertex ).
tff(func_def_51,type,
sK7: map_vertex_int ).
tff(func_def_52,type,
sK8: set_vertex ).
tff(func_def_53,type,
sK9: map_vertex_int ).
tff(func_def_54,type,
sK10: set_vertex ).
tff(func_def_55,type,
sK11: vertex1 > vertex1 ).
tff(func_def_56,type,
sK12: bool1 ).
tff(func_def_57,type,
sK13: vertex1 ).
tff(func_def_58,type,
sK14: vertex1 ).
tff(func_def_59,type,
sK15: vertex1 ).
tff(func_def_60,type,
sK16: set_vertex ).
tff(func_def_61,type,
sK17: set_vertex ).
tff(func_def_62,type,
sK18: set_vertex ).
tff(func_def_63,type,
sK19: set_vertex ).
tff(func_def_64,type,
sK20: map_vertex_int ).
tff(func_def_65,type,
sK21: bool1 ).
tff(func_def_66,type,
sK22: vertex1 ).
tff(func_def_67,type,
sK23: set_vertex ).
tff(func_def_68,type,
sK24: map_vertex_int ).
tff(func_def_69,type,
sK25: set_vertex ).
tff(func_def_70,type,
sK26: vertex1 ).
tff(func_def_71,type,
sK27: vertex1 ).
tff(func_def_72,type,
sK28: vertex1 ).
tff(func_def_73,type,
sK29: vertex1 ).
tff(func_def_74,type,
sK30: ( vertex1 * $int * vertex1 ) > vertex1 ).
tff(func_def_75,type,
sK31: ( vertex1 * $int * vertex1 ) > $int ).
tff(func_def_76,type,
sK32: ( vertex1 * $int * vertex1 ) > vertex1 ).
tff(func_def_77,type,
sK33: ( ty * uni ) > uni ).
tff(func_def_78,type,
sK34: set_vertex > vertex1 ).
tff(func_def_79,type,
sK35: set_vertex > vertex1 ).
tff(func_def_80,type,
sK36: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_81,type,
sK37: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_82,type,
sK38: ( vertex1 * vertex1 * $int ) > $int ).
tff(func_def_83,type,
sK39: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_84,type,
sK40: ( vertex1 * vertex1 * $int ) > vertex1 ).
tff(func_def_85,type,
sK41: ( uni * ty * uni ) > uni ).
tff(func_def_86,type,
sF42: uni ).
tff(func_def_87,type,
sF43: uni ).
tff(func_def_88,type,
sF44: uni ).
tff(func_def_89,type,
sF45: vertex1 > uni ).
tff(func_def_90,type,
sF46: vertex1 > uni ).
tff(func_def_91,type,
sF47: vertex1 > $int ).
tff(func_def_92,type,
sF48: vertex1 > uni ).
tff(func_def_93,type,
sF49: vertex1 > $int ).
tff(func_def_94,type,
sF50: uni ).
tff(func_def_95,type,
sF51: uni ).
tff(func_def_96,type,
sF52: uni ).
tff(func_def_97,type,
sF53: $int ).
tff(func_def_98,type,
sF54: uni ).
tff(func_def_99,type,
sF55: uni ).
tff(func_def_100,type,
sF56: uni ).
tff(func_def_101,type,
sF57: uni ).
tff(func_def_102,type,
sF58: set_vertex ).
tff(func_def_103,type,
sF59: uni ).
tff(func_def_104,type,
sF60: $int ).
tff(func_def_105,type,
sF61: uni ).
tff(func_def_106,type,
sF62: set_vertex ).
tff(func_def_107,type,
sF63: uni ).
tff(func_def_108,type,
sF64: uni ).
tff(func_def_109,type,
sF65: uni ).
tff(func_def_110,type,
sF66: vertex1 > uni ).
tff(func_def_111,type,
sF67: vertex1 > $int ).
tff(func_def_112,type,
sF68: uni ).
tff(func_def_113,type,
sF69: $int ).
tff(func_def_114,type,
sF70: vertex1 > uni ).
tff(func_def_115,type,
sF71: ( vertex1 * vertex1 ) > $int ).
tff(func_def_116,type,
sF72: set_vertex ).
tff(func_def_117,type,
sF73: uni ).
tff(func_def_118,type,
sF74: uni ).
tff(func_def_119,type,
sF75: uni ).
tff(func_def_120,type,
sF76: $int ).
tff(func_def_121,type,
sF77: vertex1 > $int ).
tff(func_def_122,type,
sF78: vertex1 > $int ).
tff(func_def_123,type,
sF79: uni ).
tff(func_def_124,type,
sF80: uni ).
tff(func_def_125,type,
sF81: set_vertex ).
tff(func_def_126,type,
sF82: $int ).
tff(func_def_127,type,
sF83: $int ).
tff(func_def_128,type,
sF84: uni ).
tff(func_def_129,type,
sF85: uni ).
tff(func_def_130,type,
sF86: map_vertex_int ).
tff(func_def_131,type,
sF87: uni ).
tff(func_def_132,type,
sF88: uni ).
tff(func_def_133,type,
sF89: $int ).
tff(func_def_134,type,
sF90: uni ).
tff(func_def_135,type,
sF91: uni ).
tff(func_def_136,type,
sF92: $int ).
tff(func_def_137,type,
sF93: $int ).
tff(func_def_138,type,
sF94: uni ).
tff(func_def_139,type,
sF95: $int ).
tff(func_def_140,type,
sF96: uni ).
tff(func_def_141,type,
sF97: set_vertex ).
tff(func_def_142,type,
sF98: uni ).
tff(func_def_143,type,
sF99: uni ).
tff(func_def_144,type,
sF100: set_vertex ).
tff(func_def_145,type,
sF101: uni ).
tff(func_def_146,type,
sF102: uni ).
tff(func_def_147,type,
sF103: uni ).
tff(func_def_148,type,
sF104: uni ).
tff(func_def_149,type,
sF105: ( vertex1 * vertex1 ) > $int ).
tff(func_def_150,type,
sF106: uni ).
tff(func_def_151,type,
sF107: uni ).
tff(func_def_152,type,
sF108: uni ).
tff(func_def_153,type,
sF109: set_vertex ).
tff(func_def_154,type,
sF110: uni ).
tff(func_def_155,type,
sF111: uni ).
tff(func_def_156,type,
sF112: uni ).
tff(func_def_157,type,
sF113: map_vertex_int ).
tff(func_def_158,type,
sF114: uni ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
infix_eqeq: ( ty * uni * uni ) > $o ).
tff(pred_def_5,type,
subset: ( ty * uni * uni ) > $o ).
tff(pred_def_6,type,
is_empty: ( ty * uni ) > $o ).
tff(pred_def_7,type,
min1: ( vertex1 * set_vertex * map_vertex_int ) > $o ).
tff(pred_def_8,type,
path1: ( vertex1 * vertex1 * $int ) > $o ).
tff(pred_def_9,type,
shortest_path1: ( vertex1 * vertex1 * $int ) > $o ).
tff(pred_def_11,type,
inv_src1: ( vertex1 * set_vertex * set_vertex ) > $o ).
tff(pred_def_12,type,
inv1: ( vertex1 * set_vertex * set_vertex * map_vertex_int ) > $o ).
tff(pred_def_13,type,
inv_succ1: ( vertex1 * set_vertex * set_vertex * map_vertex_int ) > $o ).
tff(pred_def_14,type,
inv_succ21: ( vertex1 * set_vertex * set_vertex * map_vertex_int * vertex1 * set_vertex ) > $o ).
tff(f22,axiom,
! [X1: uni,X0: ty,X2: uni] : sort1(set(X0),add(X0,X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_sort1) ).
tff(f23,axiom,
! [X2: uni,X1: uni,X0: ty] :
( sort1(X0,X1)
=> ( sort1(X0,X2)
=> ! [X3: uni] :
( mem(X0,X1,add(X0,X2,X3))
<=> ( mem(X0,X1,X3)
| ( X1 = X2 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_def1) ).
tff(f24,axiom,
! [X1: uni,X0: ty,X2: uni] : sort1(set(X0),remove(X0,X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',remove_sort1) ).
tff(f25,axiom,
! [X2: uni,X1: uni,X3: uni,X0: ty] :
( sort1(X0,X1)
=> ( sort1(X0,X2)
=> ( mem(X0,X1,remove(X0,X2,X3))
<=> ( ( X1 != X2 )
& mem(X0,X1,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',remove_def1) ).
tff(f26,axiom,
! [X1: uni,X2: uni,X0: ty] :
( sort1(set(X0),X2)
=> ( mem(X0,X1,X2)
=> ( add(X0,X1,remove(X0,X1,X2)) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_remove) ).
tff(f27,axiom,
! [X2: uni,X0: ty,X1: uni] : ( remove(X0,X1,add(X0,X1,X2)) = remove(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',remove_add) ).
tff(f50,axiom,
! [X0: set_vertex] : sort1(set(vertex),t2tb(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort) ).
tff(f52,axiom,
! [X0: uni] :
( sort1(set(vertex),X0)
=> ( t2tb(tb2t(X0)) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f58,axiom,
! [X0: vertex1] : sort1(vertex,t2tb2(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f78,conjecture,
! [X1: vertex1,X0: vertex1,X2: map_vertex_int] :
( ( mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) )
=> ! [X3: set_vertex,X4: map_vertex_int,X5: set_vertex] :
( ( ( X4 = tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X0),t2tb3(0))) )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5))
& ( X3 = tb2t(add(vertex,t2tb2(X0),empty(vertex))) ) )
=> ! [X8: map_vertex_int,X7: set_vertex,X9: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X7))
=> path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X10)))) )
& ( tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X0))) = 0 )
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X9))
=> shortest_path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X10)))) )
& inv_src1(X0,X9,X7)
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X7))
=> ( mem(vertex,t2tb2(X10),t2tb(X9))
=> $false ) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X9))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X11))),$sum(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6))),weight1(X6,X11)))
& ( mem(vertex,t2tb2(X11),t2tb(X9))
| mem(vertex,t2tb2(X11),t2tb(X7)) ) ) ) )
& subset(vertex,t2tb(X7),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X12: vertex1] :
( ( ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X7))
=> $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X12))),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6)))) )
& mem(vertex,t2tb2(X12),t2tb(X7)) )
=> ! [X6: vertex1,X13: $int] :
( path1(X0,X6,X13)
=> ( $less(X13,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X12))))
=> mem(vertex,t2tb2(X6),t2tb(X9)) ) ) ) )
=> ! [X14: bool1] :
( ( ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X7))
<=> ( X14 = true1 ) )
=> ( ( X14 != true1 )
=> ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X7))
=> ! [X15: set_vertex,X16: vertex1] :
( ( mem(vertex,t2tb2(X16),t2tb(X7))
& ( X15 = tb2t(remove(vertex,t2tb2(X16),t2tb(X7))) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X7))
=> $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6)))) ) )
=> ( ( ! [X17: $int] :
( path1(X0,X16,X17)
=> $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16))),X17) )
& path1(X0,X16,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16)))) )
=> ! [X18: set_vertex] :
( ( X18 = tb2t(add(vertex,t2tb2(X16),t2tb(X9))) )
=> ! [X21: map_vertex_int,X19: set_vertex,X20: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X20))
=> ( mem(vertex,t2tb2(X10),t2tb(X18))
=> $false ) )
& subset(vertex,t2tb(X18),t2tb(v1))
& ( tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X0))) = 0 )
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X20))
=> path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10)))) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X18))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ( ( ~ mem(vertex,t2tb2(X11),t2tb(X19))
& ( X6 = X16 ) )
| ( X6 != X16 ) )
=> ( $lesseq(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X11))),$sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X6))),weight1(X6,X11)))
& ( mem(vertex,t2tb2(X11),t2tb(X20))
| mem(vertex,t2tb2(X11),t2tb(X18)) ) ) ) ) )
& subset(vertex,t2tb(X20),t2tb(v1))
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X19))
=> mem(vertex,t2tb2(X6),t2tb(g_succ1(X16))) )
& inv_src1(X0,X18,X20)
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X18))
=> shortest_path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10)))) ) )
=> ! [X22: bool1] :
( ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X19))
<=> ( X22 = true1 ) )
=> ( ( X22 = true1 )
=> ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X19))
=> ! [X10: vertex1,X23: set_vertex] :
( ( mem(vertex,t2tb2(X10),t2tb(X19))
& ( X23 = tb2t(remove(vertex,t2tb2(X10),t2tb(X19))) ) )
=> ! [X24: set_vertex,X25: map_vertex_int] :
( ( ( ( X25 = X21 )
& ( X24 = X20 )
& mem(vertex,t2tb2(X10),t2tb(X24))
& $lesseq(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))),$sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10))) )
| ( ( X24 = X20 )
& mem(vertex,t2tb2(X10),t2tb(X18))
& ( X25 = X21 ) )
| ( ( X24 = tb2t(add(vertex,t2tb2(X10),t2tb(X20))) )
& ( X25 = tb2t1(set1(int,vertex,t2tb1(X21),t2tb2(X10),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10))))) )
& ~ mem(vertex,t2tb2(X10),t2tb(X20))
& ~ mem(vertex,t2tb2(X10),t2tb(X18)) )
| ( ( X25 = tb2t1(set1(int,vertex,t2tb1(X21),t2tb2(X10),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10))))) )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10)),tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10))))
& mem(vertex,t2tb2(X10),t2tb(X24))
& ( X24 = X20 ) ) )
=> ( ( $less(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))),$sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)))
| ( tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))) = $sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)) ) )
=> ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X18))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ( ( ( X6 = X16 )
& ~ mem(vertex,t2tb2(X11),t2tb(X23)) )
| ( X6 != X16 ) )
=> ( mem(vertex,t2tb2(X11),t2tb(X18))
| mem(vertex,t2tb2(X11),t2tb(X24)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_shortest_path_code) ).
tff(f79,negated_conjecture,
~ ! [X1: vertex1,X0: vertex1,X2: map_vertex_int] :
( ( mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) )
=> ! [X3: set_vertex,X4: map_vertex_int,X5: set_vertex] :
( ( ( X4 = tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X0),t2tb3(0))) )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5))
& ( X3 = tb2t(add(vertex,t2tb2(X0),empty(vertex))) ) )
=> ! [X8: map_vertex_int,X7: set_vertex,X9: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X7))
=> path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X10)))) )
& ( tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X0))) = 0 )
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X9))
=> shortest_path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X10)))) )
& inv_src1(X0,X9,X7)
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X7))
=> ( mem(vertex,t2tb2(X10),t2tb(X9))
=> $false ) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X9))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X11))),$sum(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6))),weight1(X6,X11)))
& ( mem(vertex,t2tb2(X11),t2tb(X9))
| mem(vertex,t2tb2(X11),t2tb(X7)) ) ) ) )
& subset(vertex,t2tb(X7),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X12: vertex1] :
( ( ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X7))
=> $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X12))),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6)))) )
& mem(vertex,t2tb2(X12),t2tb(X7)) )
=> ! [X6: vertex1,X13: $int] :
( path1(X0,X6,X13)
=> ( $less(X13,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X12))))
=> mem(vertex,t2tb2(X6),t2tb(X9)) ) ) ) )
=> ! [X14: bool1] :
( ( ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X7))
<=> ( X14 = true1 ) )
=> ( ( X14 != true1 )
=> ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X7))
=> ! [X15: set_vertex,X16: vertex1] :
( ( mem(vertex,t2tb2(X16),t2tb(X7))
& ( X15 = tb2t(remove(vertex,t2tb2(X16),t2tb(X7))) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X7))
=> $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6)))) ) )
=> ( ( ! [X17: $int] :
( path1(X0,X16,X17)
=> $lesseq(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16))),X17) )
& path1(X0,X16,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16)))) )
=> ! [X18: set_vertex] :
( ( X18 = tb2t(add(vertex,t2tb2(X16),t2tb(X9))) )
=> ! [X21: map_vertex_int,X19: set_vertex,X20: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X20))
=> ( mem(vertex,t2tb2(X10),t2tb(X18))
=> $false ) )
& subset(vertex,t2tb(X18),t2tb(v1))
& ( tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X0))) = 0 )
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X20))
=> path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10)))) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X18))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ( ( ~ mem(vertex,t2tb2(X11),t2tb(X19))
& ( X6 = X16 ) )
| ( X6 != X16 ) )
=> ( $lesseq(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X11))),$sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X6))),weight1(X6,X11)))
& ( mem(vertex,t2tb2(X11),t2tb(X20))
| mem(vertex,t2tb2(X11),t2tb(X18)) ) ) ) ) )
& subset(vertex,t2tb(X20),t2tb(v1))
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X19))
=> mem(vertex,t2tb2(X6),t2tb(g_succ1(X16))) )
& inv_src1(X0,X18,X20)
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X18))
=> shortest_path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10)))) ) )
=> ! [X22: bool1] :
( ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X19))
<=> ( X22 = true1 ) )
=> ( ( X22 = true1 )
=> ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X19))
=> ! [X10: vertex1,X23: set_vertex] :
( ( mem(vertex,t2tb2(X10),t2tb(X19))
& ( X23 = tb2t(remove(vertex,t2tb2(X10),t2tb(X19))) ) )
=> ! [X24: set_vertex,X25: map_vertex_int] :
( ( ( ( X25 = X21 )
& ( X24 = X20 )
& mem(vertex,t2tb2(X10),t2tb(X24))
& $lesseq(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))),$sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10))) )
| ( ( X24 = X20 )
& mem(vertex,t2tb2(X10),t2tb(X18))
& ( X25 = X21 ) )
| ( ( X24 = tb2t(add(vertex,t2tb2(X10),t2tb(X20))) )
& ( X25 = tb2t1(set1(int,vertex,t2tb1(X21),t2tb2(X10),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10))))) )
& ~ mem(vertex,t2tb2(X10),t2tb(X20))
& ~ mem(vertex,t2tb2(X10),t2tb(X18)) )
| ( ( X25 = tb2t1(set1(int,vertex,t2tb1(X21),t2tb2(X10),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10))))) )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10)),tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10))))
& mem(vertex,t2tb2(X10),t2tb(X24))
& ( X24 = X20 ) ) )
=> ( ( $less(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))),$sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)))
| ( tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))) = $sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)) ) )
=> ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X18))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ( ( ( X6 = X16 )
& ~ mem(vertex,t2tb2(X11),t2tb(X23)) )
| ( X6 != X16 ) )
=> ( mem(vertex,t2tb2(X11),t2tb(X18))
| mem(vertex,t2tb2(X11),t2tb(X24)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f78]) ).
tff(f89,plain,
~ ! [X1: vertex1,X0: vertex1,X2: map_vertex_int] :
( ( mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) )
=> ! [X3: set_vertex,X4: map_vertex_int,X5: set_vertex] :
( ( ( X4 = tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X0),t2tb3(0))) )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5))
& ( X3 = tb2t(add(vertex,t2tb2(X0),empty(vertex))) ) )
=> ! [X8: map_vertex_int,X7: set_vertex,X9: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X7))
=> path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X10)))) )
& ( tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X0))) = 0 )
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X9))
=> shortest_path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X10)))) )
& inv_src1(X0,X9,X7)
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X7))
=> ( mem(vertex,t2tb2(X10),t2tb(X9))
=> $false ) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X9))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6))),weight1(X6,X11)),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X11))))
& ( mem(vertex,t2tb2(X11),t2tb(X9))
| mem(vertex,t2tb2(X11),t2tb(X7)) ) ) ) )
& subset(vertex,t2tb(X7),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X12: vertex1] :
( ( ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X7))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6))),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X12)))) )
& mem(vertex,t2tb2(X12),t2tb(X7)) )
=> ! [X6: vertex1,X13: $int] :
( path1(X0,X6,X13)
=> ( $less(X13,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X12))))
=> mem(vertex,t2tb2(X6),t2tb(X9)) ) ) ) )
=> ! [X14: bool1] :
( ( ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X7))
<=> ( X14 = true1 ) )
=> ( ( X14 != true1 )
=> ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X7))
=> ! [X15: set_vertex,X16: vertex1] :
( ( mem(vertex,t2tb2(X16),t2tb(X7))
& ( X15 = tb2t(remove(vertex,t2tb2(X16),t2tb(X7))) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X7))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X6))),tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16)))) ) )
=> ( ( ! [X17: $int] :
( path1(X0,X16,X17)
=> ~ $less(X17,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16)))) )
& path1(X0,X16,tb2t3(get(int,vertex,t2tb1(X8),t2tb2(X16)))) )
=> ! [X18: set_vertex] :
( ( X18 = tb2t(add(vertex,t2tb2(X16),t2tb(X9))) )
=> ! [X21: map_vertex_int,X19: set_vertex,X20: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X20))
=> ( mem(vertex,t2tb2(X10),t2tb(X18))
=> $false ) )
& subset(vertex,t2tb(X18),t2tb(v1))
& ( tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X0))) = 0 )
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X20))
=> path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10)))) )
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X18))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ( ( ~ mem(vertex,t2tb2(X11),t2tb(X19))
& ( X6 = X16 ) )
| ( X6 != X16 ) )
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X6))),weight1(X6,X11)),tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X11))))
& ( mem(vertex,t2tb2(X11),t2tb(X20))
| mem(vertex,t2tb2(X11),t2tb(X18)) ) ) ) ) )
& subset(vertex,t2tb(X20),t2tb(v1))
& ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X19))
=> mem(vertex,t2tb2(X6),t2tb(g_succ1(X16))) )
& inv_src1(X0,X18,X20)
& ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X18))
=> shortest_path1(X0,X10,tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10)))) ) )
=> ! [X22: bool1] :
( ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X19))
<=> ( X22 = true1 ) )
=> ( ( X22 = true1 )
=> ( ~ ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X19))
=> ! [X10: vertex1,X23: set_vertex] :
( ( mem(vertex,t2tb2(X10),t2tb(X19))
& ( X23 = tb2t(remove(vertex,t2tb2(X10),t2tb(X19))) ) )
=> ! [X24: set_vertex,X25: map_vertex_int] :
( ( ( ( X25 = X21 )
& ( X24 = X20 )
& mem(vertex,t2tb2(X10),t2tb(X24))
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)),tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10)))) )
| ( ( X24 = X20 )
& mem(vertex,t2tb2(X10),t2tb(X18))
& ( X25 = X21 ) )
| ( ( X24 = tb2t(add(vertex,t2tb2(X10),t2tb(X20))) )
& ( X25 = tb2t1(set1(int,vertex,t2tb1(X21),t2tb2(X10),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10))))) )
& ~ mem(vertex,t2tb2(X10),t2tb(X20))
& ~ mem(vertex,t2tb2(X10),t2tb(X18)) )
| ( ( X25 = tb2t1(set1(int,vertex,t2tb1(X21),t2tb2(X10),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10))))) )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X16))),weight1(X16,X10)),tb2t3(get(int,vertex,t2tb1(X21),t2tb2(X10))))
& mem(vertex,t2tb2(X10),t2tb(X24))
& ( X24 = X20 ) ) )
=> ( ( $less(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))),$sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)))
| ( tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X10))) = $sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X16))),weight1(X16,X10)) ) )
=> ! [X6: vertex1] :
( mem(vertex,t2tb2(X6),t2tb(X18))
=> ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(g_succ1(X6)))
=> ( ( ( ( X6 = X16 )
& ~ mem(vertex,t2tb2(X11),t2tb(X23)) )
| ( X6 != X16 ) )
=> ( mem(vertex,t2tb2(X11),t2tb(X18))
| mem(vertex,t2tb2(X11),t2tb(X24)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f79]) ).
tff(f126,plain,
~ ! [X0: vertex1,X1: vertex1,X2: map_vertex_int] :
( ( mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) )
=> ! [X3: set_vertex,X4: map_vertex_int,X5: set_vertex] :
( ( ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 )
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5)) )
=> ! [X7: map_vertex_int,X8: set_vertex,X9: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X8))
=> path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(X9))
=> shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11)))) )
& inv_src1(X1,X9,X8)
& ! [X12: vertex1] :
( mem(vertex,t2tb2(X12),t2tb(X8))
=> ( mem(vertex,t2tb2(X12),t2tb(X9))
=> $false ) )
& ! [X13: vertex1] :
( mem(vertex,t2tb2(X13),t2tb(X9))
=> ! [X14: vertex1] :
( mem(vertex,t2tb2(X14),t2tb(g_succ1(X13)))
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) ) ) )
& subset(vertex,t2tb(X8),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X15: vertex1] :
( ( ! [X16: vertex1] :
( mem(vertex,t2tb2(X16),t2tb(X8))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
& mem(vertex,t2tb2(X15),t2tb(X8)) )
=> ! [X18: $int,X17: vertex1] :
( path1(X1,X17,X18)
=> ( $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
=> mem(vertex,t2tb2(X17),t2tb(X9)) ) ) ) )
=> ! [X19: bool1] :
( ( ( true1 = X19 )
<=> ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8)) )
=> ( ( true1 != X19 )
=> ( ~ ! [X21: vertex1] : ~ mem(vertex,t2tb2(X21),t2tb(X8))
=> ! [X22: set_vertex,X23: vertex1] :
( ( mem(vertex,t2tb2(X23),t2tb(X8))
& ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& ! [X24: vertex1] :
( mem(vertex,t2tb2(X24),t2tb(X8))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
=> ( ( path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ! [X25: $int] :
( path1(X1,X23,X25)
=> ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
=> ! [X26: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 )
=> ! [X27: map_vertex_int,X28: set_vertex,X29: set_vertex] :
( ( ! [X30: vertex1] :
( mem(vertex,t2tb2(X30),t2tb(X29))
=> ( mem(vertex,t2tb2(X30),t2tb(X26))
=> $false ) )
& subset(vertex,t2tb(X26),t2tb(v1))
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) )
& ! [X31: vertex1] :
( mem(vertex,t2tb2(X31),t2tb(X29))
=> path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& ! [X32: vertex1] :
( mem(vertex,t2tb2(X32),t2tb(X26))
=> ! [X33: vertex1] :
( mem(vertex,t2tb2(X33),t2tb(g_succ1(X32)))
=> ( ( ( X23 != X32 )
| ( ~ mem(vertex,t2tb2(X33),t2tb(X28))
& ( X23 = X32 ) ) )
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) ) ) ) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(X28))
=> mem(vertex,t2tb2(X34),t2tb(g_succ1(X23))) )
& inv_src1(X1,X26,X29)
& ! [X35: vertex1] :
( mem(vertex,t2tb2(X35),t2tb(X26))
=> shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35)))) ) )
=> ! [X36: bool1] :
( ( ~ ! [X37: vertex1] : ~ mem(vertex,t2tb2(X37),t2tb(X28))
<=> ( true1 = X36 ) )
=> ( ( true1 = X36 )
=> ( ~ ! [X38: vertex1] : ~ mem(vertex,t2tb2(X38),t2tb(X28))
=> ! [X40: set_vertex,X39: vertex1] :
( ( mem(vertex,t2tb2(X39),t2tb(X28))
& ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 ) )
=> ! [X41: set_vertex,X42: map_vertex_int] :
( ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) )
=> ( ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) )
=> ! [X43: vertex1] :
( mem(vertex,t2tb2(X43),t2tb(X26))
=> ! [X44: vertex1] :
( mem(vertex,t2tb2(X44),t2tb(g_succ1(X43)))
=> ( ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
=> ( mem(vertex,t2tb2(X44),t2tb(X26))
| mem(vertex,t2tb2(X44),t2tb(X41)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f89]) ).
tff(f127,plain,
~ ! [X0: vertex1,X1: vertex1,X2: map_vertex_int] :
( ( mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) )
=> ! [X3: set_vertex,X4: map_vertex_int,X5: set_vertex] :
( ( ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 )
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5)) )
=> ! [X7: map_vertex_int,X8: set_vertex,X9: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X8))
=> path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(X9))
=> shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11)))) )
& inv_src1(X1,X9,X8)
& ! [X12: vertex1] :
( mem(vertex,t2tb2(X12),t2tb(X8))
=> ~ mem(vertex,t2tb2(X12),t2tb(X9)) )
& ! [X13: vertex1] :
( mem(vertex,t2tb2(X13),t2tb(X9))
=> ! [X14: vertex1] :
( mem(vertex,t2tb2(X14),t2tb(g_succ1(X13)))
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) ) ) )
& subset(vertex,t2tb(X8),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X15: vertex1] :
( ( ! [X16: vertex1] :
( mem(vertex,t2tb2(X16),t2tb(X8))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
& mem(vertex,t2tb2(X15),t2tb(X8)) )
=> ! [X18: $int,X17: vertex1] :
( path1(X1,X17,X18)
=> ( $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
=> mem(vertex,t2tb2(X17),t2tb(X9)) ) ) ) )
=> ! [X19: bool1] :
( ( ( true1 = X19 )
<=> ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8)) )
=> ( ( true1 != X19 )
=> ( ~ ! [X21: vertex1] : ~ mem(vertex,t2tb2(X21),t2tb(X8))
=> ! [X22: set_vertex,X23: vertex1] :
( ( mem(vertex,t2tb2(X23),t2tb(X8))
& ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& ! [X24: vertex1] :
( mem(vertex,t2tb2(X24),t2tb(X8))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
=> ( ( path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ! [X25: $int] :
( path1(X1,X23,X25)
=> ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
=> ! [X26: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 )
=> ! [X27: map_vertex_int,X28: set_vertex,X29: set_vertex] :
( ( ! [X30: vertex1] :
( mem(vertex,t2tb2(X30),t2tb(X29))
=> ~ mem(vertex,t2tb2(X30),t2tb(X26)) )
& subset(vertex,t2tb(X26),t2tb(v1))
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) )
& ! [X31: vertex1] :
( mem(vertex,t2tb2(X31),t2tb(X29))
=> path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& ! [X32: vertex1] :
( mem(vertex,t2tb2(X32),t2tb(X26))
=> ! [X33: vertex1] :
( mem(vertex,t2tb2(X33),t2tb(g_succ1(X32)))
=> ( ( ( X23 != X32 )
| ( ~ mem(vertex,t2tb2(X33),t2tb(X28))
& ( X23 = X32 ) ) )
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) ) ) ) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(X28))
=> mem(vertex,t2tb2(X34),t2tb(g_succ1(X23))) )
& inv_src1(X1,X26,X29)
& ! [X35: vertex1] :
( mem(vertex,t2tb2(X35),t2tb(X26))
=> shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35)))) ) )
=> ! [X36: bool1] :
( ( ~ ! [X37: vertex1] : ~ mem(vertex,t2tb2(X37),t2tb(X28))
<=> ( true1 = X36 ) )
=> ( ( true1 = X36 )
=> ( ~ ! [X38: vertex1] : ~ mem(vertex,t2tb2(X38),t2tb(X28))
=> ! [X40: set_vertex,X39: vertex1] :
( ( mem(vertex,t2tb2(X39),t2tb(X28))
& ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 ) )
=> ! [X41: set_vertex,X42: map_vertex_int] :
( ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) )
=> ( ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) )
=> ! [X43: vertex1] :
( mem(vertex,t2tb2(X43),t2tb(X26))
=> ! [X44: vertex1] :
( mem(vertex,t2tb2(X44),t2tb(g_succ1(X43)))
=> ( ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
=> ( mem(vertex,t2tb2(X44),t2tb(X26))
| mem(vertex,t2tb2(X44),t2tb(X41)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(true_and_false_elimination,[],[f126]) ).
tff(f128,plain,
~ ! [X2: map_vertex_int,X0: vertex1,X1: vertex1] :
( ( mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) )
=> ! [X5: set_vertex,X4: map_vertex_int,X3: set_vertex] :
( ( ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 )
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5)) )
=> ! [X8: set_vertex,X7: map_vertex_int,X9: set_vertex] :
( ( ! [X10: vertex1] :
( mem(vertex,t2tb2(X10),t2tb(X8))
=> path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ! [X11: vertex1] :
( mem(vertex,t2tb2(X11),t2tb(X9))
=> shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11)))) )
& subset(vertex,t2tb(X8),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X12: vertex1] :
( mem(vertex,t2tb2(X12),t2tb(X8))
=> ~ mem(vertex,t2tb2(X12),t2tb(X9)) )
& ! [X15: vertex1] :
( ( ! [X16: vertex1] :
( mem(vertex,t2tb2(X16),t2tb(X8))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
& mem(vertex,t2tb2(X15),t2tb(X8)) )
=> ! [X18: $int,X17: vertex1] :
( path1(X1,X17,X18)
=> ( $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
=> mem(vertex,t2tb2(X17),t2tb(X9)) ) ) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& inv_src1(X1,X9,X8)
& ! [X13: vertex1] :
( mem(vertex,t2tb2(X13),t2tb(X9))
=> ! [X14: vertex1] :
( mem(vertex,t2tb2(X14),t2tb(g_succ1(X13)))
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) ) ) ) )
=> ! [X19: bool1] :
( ( ( true1 = X19 )
<=> ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8)) )
=> ( ( true1 != X19 )
=> ( ~ ! [X21: vertex1] : ~ mem(vertex,t2tb2(X21),t2tb(X8))
=> ! [X23: vertex1,X22: set_vertex] :
( ( mem(vertex,t2tb2(X23),t2tb(X8))
& ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& ! [X24: vertex1] :
( mem(vertex,t2tb2(X24),t2tb(X8))
=> ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
=> ( ( path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ! [X25: $int] :
( path1(X1,X23,X25)
=> ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
=> ! [X26: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 )
=> ! [X27: map_vertex_int,X28: set_vertex,X29: set_vertex] :
( ( ! [X31: vertex1] :
( mem(vertex,t2tb2(X31),t2tb(X29))
=> path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X35: vertex1] :
( mem(vertex,t2tb2(X35),t2tb(X26))
=> shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35)))) )
& ! [X30: vertex1] :
( mem(vertex,t2tb2(X30),t2tb(X29))
=> ~ mem(vertex,t2tb2(X30),t2tb(X26)) )
& subset(vertex,t2tb(X26),t2tb(v1))
& ! [X32: vertex1] :
( mem(vertex,t2tb2(X32),t2tb(X26))
=> ! [X33: vertex1] :
( mem(vertex,t2tb2(X33),t2tb(g_succ1(X32)))
=> ( ( ( X23 != X32 )
| ( ~ mem(vertex,t2tb2(X33),t2tb(X28))
& ( X23 = X32 ) ) )
=> ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) ) ) ) )
& inv_src1(X1,X26,X29)
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(X28))
=> mem(vertex,t2tb2(X34),t2tb(g_succ1(X23))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) ) )
=> ! [X36: bool1] :
( ( ~ ! [X37: vertex1] : ~ mem(vertex,t2tb2(X37),t2tb(X28))
<=> ( true1 = X36 ) )
=> ( ( true1 = X36 )
=> ( ~ ! [X38: vertex1] : ~ mem(vertex,t2tb2(X38),t2tb(X28))
=> ! [X40: set_vertex,X39: vertex1] :
( ( mem(vertex,t2tb2(X39),t2tb(X28))
& ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 ) )
=> ! [X41: set_vertex,X42: map_vertex_int] :
( ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) )
=> ( ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) )
=> ! [X43: vertex1] :
( mem(vertex,t2tb2(X43),t2tb(X26))
=> ! [X44: vertex1] :
( mem(vertex,t2tb2(X44),t2tb(g_succ1(X43)))
=> ( ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
=> ( mem(vertex,t2tb2(X44),t2tb(X26))
| mem(vertex,t2tb2(X44),t2tb(X41)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(flattening,[],[f127]) ).
tff(f140,plain,
! [X2: uni,X0: uni,X1: ty] : ( remove(X1,X2,X0) = remove(X1,X2,add(X1,X2,X0)) ),
inference(rectify,[],[f27]) ).
tff(f141,plain,
! [X2: uni,X1: uni,X0: uni,X3: ty] :
( sort1(X3,X1)
=> ( sort1(X3,X0)
=> ( ( mem(X3,X1,X2)
& ( X0 != X1 ) )
<=> mem(X3,X1,remove(X3,X0,X2)) ) ) ),
inference(rectify,[],[f25]) ).
tff(f146,plain,
! [X1: uni,X2: ty,X0: uni] :
( sort1(X2,X1)
=> ( sort1(X2,X0)
=> ! [X3: uni] :
( ( mem(X2,X1,X3)
| ( X0 = X1 ) )
<=> mem(X2,X1,add(X2,X0,X3)) ) ) ),
inference(rectify,[],[f23]) ).
tff(f153,plain,
! [X0: uni,X1: ty,X2: uni] : sort1(set(X1),add(X1,X0,X2)),
inference(rectify,[],[f22]) ).
tff(f155,plain,
! [X2: uni,X0: uni,X1: ty] : sort1(set(X1),remove(X1,X0,X2)),
inference(rectify,[],[f24]) ).
tff(f156,plain,
! [X2: ty,X1: uni,X0: uni] :
( sort1(set(X2),X1)
=> ( mem(X2,X0,X1)
=> ( add(X2,X0,remove(X2,X0,X1)) = X1 ) ) ),
inference(rectify,[],[f26]) ).
tff(f182,plain,
! [X2: uni,X1: uni,X0: uni,X3: ty] :
( ( ( mem(X3,X1,X2)
& ( X0 != X1 ) )
<=> mem(X3,X1,remove(X3,X0,X2)) )
| ~ sort1(X3,X0)
| ~ sort1(X3,X1) ),
inference(ennf_transformation,[],[f141]) ).
tff(f183,plain,
! [X3: ty,X2: uni,X0: uni,X1: uni] :
( ~ sort1(X3,X0)
| ( ( mem(X3,X1,X2)
& ( X0 != X1 ) )
<=> mem(X3,X1,remove(X3,X0,X2)) )
| ~ sort1(X3,X1) ),
inference(flattening,[],[f182]) ).
tff(f190,plain,
! [X0: uni] :
( ~ sort1(set(vertex),X0)
| ( t2tb(tb2t(X0)) = X0 ) ),
inference(ennf_transformation,[],[f52]) ).
tff(f199,plain,
! [X2: ty,X1: uni,X0: uni] :
( ( add(X2,X0,remove(X2,X0,X1)) = X1 )
| ~ mem(X2,X0,X1)
| ~ sort1(set(X2),X1) ),
inference(ennf_transformation,[],[f156]) ).
tff(f200,plain,
! [X0: uni,X1: uni,X2: ty] :
( ( add(X2,X0,remove(X2,X0,X1)) = X1 )
| ~ sort1(set(X2),X1)
| ~ mem(X2,X0,X1) ),
inference(flattening,[],[f199]) ).
tff(f202,plain,
? [X2: map_vertex_int,X0: vertex1,X1: vertex1] :
( ? [X5: set_vertex,X4: map_vertex_int,X3: set_vertex] :
( ? [X8: set_vertex,X7: map_vertex_int,X9: set_vertex] :
( ? [X19: bool1] :
( ? [X23: vertex1,X22: set_vertex] :
( ? [X26: set_vertex] :
( ? [X27: map_vertex_int,X28: set_vertex,X29: set_vertex] :
( ? [X36: bool1] :
( ? [X40: set_vertex,X39: vertex1] :
( ? [X41: set_vertex,X42: map_vertex_int] :
( ? [X43: vertex1] :
( ? [X44: vertex1] :
( ~ mem(vertex,t2tb2(X44),t2tb(X26))
& ~ mem(vertex,t2tb2(X44),t2tb(X41))
& ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
& mem(vertex,t2tb2(X44),t2tb(g_succ1(X43))) )
& mem(vertex,t2tb2(X43),t2tb(X26)) )
& ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) )
& ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) ) )
& mem(vertex,t2tb2(X39),t2tb(X28))
& ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 ) )
& ? [X38: vertex1] : mem(vertex,t2tb2(X38),t2tb(X28))
& ( true1 = X36 )
& ( ? [X37: vertex1] : mem(vertex,t2tb2(X37),t2tb(X28))
<=> ( true1 = X36 ) ) )
& ! [X31: vertex1] :
( ~ mem(vertex,t2tb2(X31),t2tb(X29))
| path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X35: vertex1] :
( shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35))))
| ~ mem(vertex,t2tb2(X35),t2tb(X26)) )
& ! [X30: vertex1] :
( ~ mem(vertex,t2tb2(X30),t2tb(X29))
| ~ mem(vertex,t2tb2(X30),t2tb(X26)) )
& subset(vertex,t2tb(X26),t2tb(v1))
& ! [X32: vertex1] :
( ! [X33: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) )
| ( ( X23 = X32 )
& ( mem(vertex,t2tb2(X33),t2tb(X28))
| ( X23 != X32 ) ) )
| ~ mem(vertex,t2tb2(X33),t2tb(g_succ1(X32))) )
| ~ mem(vertex,t2tb2(X32),t2tb(X26)) )
& inv_src1(X1,X26,X29)
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(g_succ1(X23)))
| ~ mem(vertex,t2tb2(X34),t2tb(X28)) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) ) )
& ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 ) )
& path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ! [X25: $int] :
( ~ path1(X1,X23,X25)
| ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) )
& mem(vertex,t2tb2(X23),t2tb(X8))
& ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& ! [X24: vertex1] :
( ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
| ~ mem(vertex,t2tb2(X24),t2tb(X8)) ) )
& ? [X21: vertex1] : mem(vertex,t2tb2(X21),t2tb(X8))
& ( true1 != X19 )
& ( ( true1 = X19 )
<=> ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8)) ) )
& ! [X10: vertex1] :
( ~ mem(vertex,t2tb2(X10),t2tb(X8))
| path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ! [X11: vertex1] :
( shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11))))
| ~ mem(vertex,t2tb2(X11),t2tb(X9)) )
& subset(vertex,t2tb(X8),t2tb(v1))
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X12: vertex1] :
( ~ mem(vertex,t2tb2(X12),t2tb(X9))
| ~ mem(vertex,t2tb2(X12),t2tb(X8)) )
& ! [X15: vertex1] :
( ! [X18: $int,X17: vertex1] :
( mem(vertex,t2tb2(X17),t2tb(X9))
| ~ $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
| ~ path1(X1,X17,X18) )
| ? [X16: vertex1] :
( $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
& mem(vertex,t2tb2(X16),t2tb(X8)) )
| ~ mem(vertex,t2tb2(X15),t2tb(X8)) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& inv_src1(X1,X9,X8)
& ! [X13: vertex1] :
( ~ mem(vertex,t2tb2(X13),t2tb(X9))
| ! [X14: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) )
| ~ mem(vertex,t2tb2(X14),t2tb(g_succ1(X13))) ) ) )
& ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 )
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5)) )
& mem(vertex,t2tb2(X1),t2tb(v1))
& mem(vertex,t2tb2(X0),t2tb(v1)) ),
inference(ennf_transformation,[],[f128]) ).
tff(f203,plain,
? [X0: vertex1,X1: vertex1,X2: map_vertex_int] :
( mem(vertex,t2tb2(X1),t2tb(v1))
& ? [X5: set_vertex,X3: set_vertex,X4: map_vertex_int] :
( ? [X9: set_vertex,X7: map_vertex_int,X8: set_vertex] :
( ! [X15: vertex1] :
( ? [X16: vertex1] :
( $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
& mem(vertex,t2tb2(X16),t2tb(X8)) )
| ! [X17: vertex1,X18: $int] :
( ~ path1(X1,X17,X18)
| mem(vertex,t2tb2(X17),t2tb(X9))
| ~ $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
| ~ mem(vertex,t2tb2(X15),t2tb(X8)) )
& inv_src1(X1,X9,X8)
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X11: vertex1] :
( shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11))))
| ~ mem(vertex,t2tb2(X11),t2tb(X9)) )
& ! [X12: vertex1] :
( ~ mem(vertex,t2tb2(X12),t2tb(X9))
| ~ mem(vertex,t2tb2(X12),t2tb(X8)) )
& ! [X10: vertex1] :
( ~ mem(vertex,t2tb2(X10),t2tb(X8))
| path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& subset(vertex,t2tb(X8),t2tb(v1))
& ? [X19: bool1] :
( ? [X21: vertex1] : mem(vertex,t2tb2(X21),t2tb(X8))
& ( ( true1 = X19 )
<=> ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8)) )
& ? [X23: vertex1,X22: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& mem(vertex,t2tb2(X23),t2tb(X8))
& path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ? [X26: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 )
& ? [X29: set_vertex,X28: set_vertex,X27: map_vertex_int] :
( subset(vertex,t2tb(X26),t2tb(v1))
& ! [X31: vertex1] :
( ~ mem(vertex,t2tb2(X31),t2tb(X29))
| path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X32: vertex1] :
( ~ mem(vertex,t2tb2(X32),t2tb(X26))
| ! [X33: vertex1] :
( ~ mem(vertex,t2tb2(X33),t2tb(g_succ1(X32)))
| ( ( X23 = X32 )
& ( mem(vertex,t2tb2(X33),t2tb(X28))
| ( X23 != X32 ) ) )
| ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) ) ) )
& inv_src1(X1,X26,X29)
& ! [X30: vertex1] :
( ~ mem(vertex,t2tb2(X30),t2tb(X29))
| ~ mem(vertex,t2tb2(X30),t2tb(X26)) )
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(g_succ1(X23)))
| ~ mem(vertex,t2tb2(X34),t2tb(X28)) )
& ? [X36: bool1] :
( ? [X39: vertex1,X40: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 )
& ? [X42: map_vertex_int,X41: set_vertex] :
( ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) )
& ? [X43: vertex1] :
( mem(vertex,t2tb2(X43),t2tb(X26))
& ? [X44: vertex1] :
( mem(vertex,t2tb2(X44),t2tb(g_succ1(X43)))
& ~ mem(vertex,t2tb2(X44),t2tb(X41))
& ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
& ~ mem(vertex,t2tb2(X44),t2tb(X26)) ) )
& ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) ) )
& mem(vertex,t2tb2(X39),t2tb(X28)) )
& ( true1 = X36 )
& ( ? [X37: vertex1] : mem(vertex,t2tb2(X37),t2tb(X28))
<=> ( true1 = X36 ) )
& ? [X38: vertex1] : mem(vertex,t2tb2(X38),t2tb(X28)) )
& ! [X35: vertex1] :
( shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35))))
| ~ mem(vertex,t2tb2(X35),t2tb(X26)) ) ) )
& ! [X24: vertex1] :
( ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
| ~ mem(vertex,t2tb2(X24),t2tb(X8)) )
& ! [X25: $int] :
( ~ path1(X1,X23,X25)
| ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
& ( true1 != X19 ) )
& ! [X13: vertex1] :
( ~ mem(vertex,t2tb2(X13),t2tb(X9))
| ! [X14: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) )
| ~ mem(vertex,t2tb2(X14),t2tb(g_succ1(X13))) ) ) )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5))
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 ) )
& mem(vertex,t2tb2(X0),t2tb(v1)) ),
inference(flattening,[],[f202]) ).
tff(f208,plain,
! [X1: uni,X2: ty,X0: uni] :
( ! [X3: uni] :
( ( mem(X2,X1,X3)
| ( X0 = X1 ) )
<=> mem(X2,X1,add(X2,X0,X3)) )
| ~ sort1(X2,X0)
| ~ sort1(X2,X1) ),
inference(ennf_transformation,[],[f146]) ).
tff(f209,plain,
! [X0: uni,X2: ty,X1: uni] :
( ~ sort1(X2,X1)
| ~ sort1(X2,X0)
| ! [X3: uni] :
( ( mem(X2,X1,X3)
| ( X0 = X1 ) )
<=> mem(X2,X1,add(X2,X0,X3)) ) ),
inference(flattening,[],[f208]) ).
tff(f227,plain,
! [X0: uni,X2: ty,X1: uni] :
( ~ sort1(X2,X1)
| ~ sort1(X2,X0)
| ! [X3: uni] :
( ( mem(X2,X1,X3)
| ( X0 = X1 )
| ~ mem(X2,X1,add(X2,X0,X3)) )
& ( mem(X2,X1,add(X2,X0,X3))
| ( ~ mem(X2,X1,X3)
& ( X0 != X1 ) ) ) ) ),
inference(nnf_transformation,[],[f209]) ).
tff(f228,plain,
! [X0: uni,X2: ty,X1: uni] :
( ~ sort1(X2,X1)
| ~ sort1(X2,X0)
| ! [X3: uni] :
( ( mem(X2,X1,X3)
| ( X0 = X1 )
| ~ mem(X2,X1,add(X2,X0,X3)) )
& ( mem(X2,X1,add(X2,X0,X3))
| ( ~ mem(X2,X1,X3)
& ( X0 != X1 ) ) ) ) ),
inference(flattening,[],[f227]) ).
tff(f229,plain,
! [X0: uni,X1: ty,X2: uni] :
( ~ sort1(X1,X2)
| ~ sort1(X1,X0)
| ! [X3: uni] :
( ( mem(X1,X2,X3)
| ( X0 = X2 )
| ~ mem(X1,X2,add(X1,X0,X3)) )
& ( mem(X1,X2,add(X1,X0,X3))
| ( ~ mem(X1,X2,X3)
& ( X0 != X2 ) ) ) ) ),
inference(rectify,[],[f228]) ).
tff(f233,plain,
? [X0: vertex1,X1: vertex1,X2: map_vertex_int] :
( mem(vertex,t2tb2(X1),t2tb(v1))
& ? [X5: set_vertex,X3: set_vertex,X4: map_vertex_int] :
( ? [X9: set_vertex,X7: map_vertex_int,X8: set_vertex] :
( ! [X15: vertex1] :
( ? [X16: vertex1] :
( $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
& mem(vertex,t2tb2(X16),t2tb(X8)) )
| ! [X17: vertex1,X18: $int] :
( ~ path1(X1,X17,X18)
| mem(vertex,t2tb2(X17),t2tb(X9))
| ~ $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
| ~ mem(vertex,t2tb2(X15),t2tb(X8)) )
& inv_src1(X1,X9,X8)
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X11: vertex1] :
( shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11))))
| ~ mem(vertex,t2tb2(X11),t2tb(X9)) )
& ! [X12: vertex1] :
( ~ mem(vertex,t2tb2(X12),t2tb(X9))
| ~ mem(vertex,t2tb2(X12),t2tb(X8)) )
& ! [X10: vertex1] :
( ~ mem(vertex,t2tb2(X10),t2tb(X8))
| path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& subset(vertex,t2tb(X8),t2tb(v1))
& ? [X19: bool1] :
( ? [X21: vertex1] : mem(vertex,t2tb2(X21),t2tb(X8))
& ( ( true1 = X19 )
| ? [X20: vertex1] : mem(vertex,t2tb2(X20),t2tb(X8)) )
& ( ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8))
| ( true1 != X19 ) )
& ? [X23: vertex1,X22: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& mem(vertex,t2tb2(X23),t2tb(X8))
& path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ? [X26: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 )
& ? [X29: set_vertex,X28: set_vertex,X27: map_vertex_int] :
( subset(vertex,t2tb(X26),t2tb(v1))
& ! [X31: vertex1] :
( ~ mem(vertex,t2tb2(X31),t2tb(X29))
| path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X32: vertex1] :
( ~ mem(vertex,t2tb2(X32),t2tb(X26))
| ! [X33: vertex1] :
( ~ mem(vertex,t2tb2(X33),t2tb(g_succ1(X32)))
| ( ( X23 = X32 )
& ( mem(vertex,t2tb2(X33),t2tb(X28))
| ( X23 != X32 ) ) )
| ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) ) ) )
& inv_src1(X1,X26,X29)
& ! [X30: vertex1] :
( ~ mem(vertex,t2tb2(X30),t2tb(X29))
| ~ mem(vertex,t2tb2(X30),t2tb(X26)) )
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(g_succ1(X23)))
| ~ mem(vertex,t2tb2(X34),t2tb(X28)) )
& ? [X36: bool1] :
( ? [X39: vertex1,X40: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 )
& ? [X42: map_vertex_int,X41: set_vertex] :
( ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) )
& ? [X43: vertex1] :
( mem(vertex,t2tb2(X43),t2tb(X26))
& ? [X44: vertex1] :
( mem(vertex,t2tb2(X44),t2tb(g_succ1(X43)))
& ~ mem(vertex,t2tb2(X44),t2tb(X41))
& ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
& ~ mem(vertex,t2tb2(X44),t2tb(X26)) ) )
& ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) ) )
& mem(vertex,t2tb2(X39),t2tb(X28)) )
& ( true1 = X36 )
& ( ? [X37: vertex1] : mem(vertex,t2tb2(X37),t2tb(X28))
| ( true1 != X36 ) )
& ( ( true1 = X36 )
| ! [X37: vertex1] : ~ mem(vertex,t2tb2(X37),t2tb(X28)) )
& ? [X38: vertex1] : mem(vertex,t2tb2(X38),t2tb(X28)) )
& ! [X35: vertex1] :
( shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35))))
| ~ mem(vertex,t2tb2(X35),t2tb(X26)) ) ) )
& ! [X24: vertex1] :
( ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
| ~ mem(vertex,t2tb2(X24),t2tb(X8)) )
& ! [X25: $int] :
( ~ path1(X1,X23,X25)
| ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
& ( true1 != X19 ) )
& ! [X13: vertex1] :
( ~ mem(vertex,t2tb2(X13),t2tb(X9))
| ! [X14: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) )
| ~ mem(vertex,t2tb2(X14),t2tb(g_succ1(X13))) ) ) )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5))
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 ) )
& mem(vertex,t2tb2(X0),t2tb(v1)) ),
inference(nnf_transformation,[],[f203]) ).
tff(f234,plain,
? [X0: vertex1,X1: vertex1,X2: map_vertex_int] :
( mem(vertex,t2tb2(X1),t2tb(v1))
& ? [X5: set_vertex,X3: set_vertex,X4: map_vertex_int] :
( ? [X9: set_vertex,X7: map_vertex_int,X8: set_vertex] :
( ! [X15: vertex1] :
( ? [X16: vertex1] :
( $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X16))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15))))
& mem(vertex,t2tb2(X16),t2tb(X8)) )
| ! [X17: vertex1,X18: $int] :
( ~ path1(X1,X17,X18)
| mem(vertex,t2tb2(X17),t2tb(X9))
| ~ $less(X18,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
| ~ mem(vertex,t2tb2(X15),t2tb(X8)) )
& inv_src1(X1,X9,X8)
& subset(vertex,t2tb(X9),t2tb(v1))
& ! [X11: vertex1] :
( shortest_path1(X1,X11,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X11))))
| ~ mem(vertex,t2tb2(X11),t2tb(X9)) )
& ! [X12: vertex1] :
( ~ mem(vertex,t2tb2(X12),t2tb(X9))
| ~ mem(vertex,t2tb2(X12),t2tb(X8)) )
& ! [X10: vertex1] :
( ~ mem(vertex,t2tb2(X10),t2tb(X8))
| path1(X1,X10,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& subset(vertex,t2tb(X8),t2tb(v1))
& ? [X19: bool1] :
( ? [X21: vertex1] : mem(vertex,t2tb2(X21),t2tb(X8))
& ( ( true1 = X19 )
| ? [X20: vertex1] : mem(vertex,t2tb2(X20),t2tb(X8)) )
& ( ! [X20: vertex1] : ~ mem(vertex,t2tb2(X20),t2tb(X8))
| ( true1 != X19 ) )
& ? [X23: vertex1,X22: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X23),t2tb(X8))) = X22 )
& mem(vertex,t2tb2(X23),t2tb(X8))
& path1(X1,X23,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
& ? [X26: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X23),t2tb(X9))) = X26 )
& ? [X29: set_vertex,X28: set_vertex,X27: map_vertex_int] :
( subset(vertex,t2tb(X26),t2tb(v1))
& ! [X31: vertex1] :
( ~ mem(vertex,t2tb2(X31),t2tb(X29))
| path1(X1,X31,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X31)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X1))) )
& subset(vertex,t2tb(X29),t2tb(v1))
& ! [X32: vertex1] :
( ~ mem(vertex,t2tb2(X32),t2tb(X26))
| ! [X33: vertex1] :
( ~ mem(vertex,t2tb2(X33),t2tb(g_succ1(X32)))
| ( ( X23 = X32 )
& ( mem(vertex,t2tb2(X33),t2tb(X28))
| ( X23 != X32 ) ) )
| ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X32))),weight1(X32,X33)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X33))))
& ( mem(vertex,t2tb2(X33),t2tb(X26))
| mem(vertex,t2tb2(X33),t2tb(X29)) ) ) ) )
& inv_src1(X1,X26,X29)
& ! [X30: vertex1] :
( ~ mem(vertex,t2tb2(X30),t2tb(X29))
| ~ mem(vertex,t2tb2(X30),t2tb(X26)) )
& ! [X34: vertex1] :
( mem(vertex,t2tb2(X34),t2tb(g_succ1(X23)))
| ~ mem(vertex,t2tb2(X34),t2tb(X28)) )
& ? [X36: bool1] :
( ? [X39: vertex1,X40: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X39),t2tb(X28))) = X40 )
& ? [X42: map_vertex_int,X41: set_vertex] :
( ( ( ~ mem(vertex,t2tb2(X39),t2tb(X26))
& ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& ( tb2t(add(vertex,t2tb2(X39),t2tb(X29))) = X41 )
& ~ mem(vertex,t2tb2(X39),t2tb(X29)) )
| ( mem(vertex,t2tb2(X39),t2tb(X26))
& ( X27 = X42 )
& ( X29 = X41 ) )
| ( ( X27 = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X27),t2tb2(X39),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39))))) = X42 )
& mem(vertex,t2tb2(X39),t2tb(X41))
& ( X29 = X41 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X23))),weight1(X23,X39)),tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X39)))) ) )
& ? [X43: vertex1] :
( mem(vertex,t2tb2(X43),t2tb(X26))
& ? [X44: vertex1] :
( mem(vertex,t2tb2(X44),t2tb(g_succ1(X43)))
& ~ mem(vertex,t2tb2(X44),t2tb(X41))
& ( ( X23 != X43 )
| ( ( X23 = X43 )
& ~ mem(vertex,t2tb2(X44),t2tb(X40)) ) )
& ~ mem(vertex,t2tb2(X44),t2tb(X26)) ) )
& ( ( $sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39)) = tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))) )
| $less(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X39))),$sum(tb2t3(get(int,vertex,t2tb1(X42),t2tb2(X23))),weight1(X23,X39))) ) )
& mem(vertex,t2tb2(X39),t2tb(X28)) )
& ( true1 = X36 )
& ( ? [X37: vertex1] : mem(vertex,t2tb2(X37),t2tb(X28))
| ( true1 != X36 ) )
& ( ( true1 = X36 )
| ! [X37: vertex1] : ~ mem(vertex,t2tb2(X37),t2tb(X28)) )
& ? [X38: vertex1] : mem(vertex,t2tb2(X38),t2tb(X28)) )
& ! [X35: vertex1] :
( shortest_path1(X1,X35,tb2t3(get(int,vertex,t2tb1(X27),t2tb2(X35))))
| ~ mem(vertex,t2tb2(X35),t2tb(X26)) ) ) )
& ! [X24: vertex1] :
( ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X24))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23))))
| ~ mem(vertex,t2tb2(X24),t2tb(X8)) )
& ! [X25: $int] :
( ~ path1(X1,X23,X25)
| ~ $less(X25,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X23)))) ) )
& ( true1 != X19 ) )
& ! [X13: vertex1] :
( ~ mem(vertex,t2tb2(X13),t2tb(X9))
| ! [X14: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))),weight1(X13,X14)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X14))))
& ( mem(vertex,t2tb2(X14),t2tb(X9))
| mem(vertex,t2tb2(X14),t2tb(X8)) ) )
| ~ mem(vertex,t2tb2(X14),t2tb(g_succ1(X13))) ) ) )
& ! [X6: vertex1] : ~ mem(vertex,t2tb2(X6),t2tb(X5))
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X3 )
& ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X4 ) )
& mem(vertex,t2tb2(X0),t2tb(v1)) ),
inference(flattening,[],[f233]) ).
tff(f235,plain,
? [X0: vertex1,X1: vertex1,X2: map_vertex_int] :
( mem(vertex,t2tb2(X1),t2tb(v1))
& ? [X3: set_vertex,X4: set_vertex,X5: map_vertex_int] :
( ? [X6: set_vertex,X7: map_vertex_int,X8: set_vertex] :
( ! [X9: vertex1] :
( ? [X10: vertex1] :
( $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X10))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X9))))
& mem(vertex,t2tb2(X10),t2tb(X8)) )
| ! [X11: vertex1,X12: $int] :
( ~ path1(X1,X11,X12)
| mem(vertex,t2tb2(X11),t2tb(X6))
| ~ $less(X12,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X9)))) )
| ~ mem(vertex,t2tb2(X9),t2tb(X8)) )
& inv_src1(X1,X6,X8)
& subset(vertex,t2tb(X6),t2tb(v1))
& ! [X13: vertex1] :
( shortest_path1(X1,X13,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X13))))
| ~ mem(vertex,t2tb2(X13),t2tb(X6)) )
& ! [X14: vertex1] :
( ~ mem(vertex,t2tb2(X14),t2tb(X6))
| ~ mem(vertex,t2tb2(X14),t2tb(X8)) )
& ! [X15: vertex1] :
( ~ mem(vertex,t2tb2(X15),t2tb(X8))
| path1(X1,X15,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X15)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X1))) )
& subset(vertex,t2tb(X8),t2tb(v1))
& ? [X16: bool1] :
( ? [X17: vertex1] : mem(vertex,t2tb2(X17),t2tb(X8))
& ( ( true1 = X16 )
| ? [X18: vertex1] : mem(vertex,t2tb2(X18),t2tb(X8)) )
& ( ! [X19: vertex1] : ~ mem(vertex,t2tb2(X19),t2tb(X8))
| ( true1 != X16 ) )
& ? [X20: vertex1,X21: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X20),t2tb(X8))) = X21 )
& mem(vertex,t2tb2(X20),t2tb(X8))
& path1(X1,X20,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X20))))
& ? [X22: set_vertex] :
( ( tb2t(add(vertex,t2tb2(X20),t2tb(X6))) = X22 )
& ? [X23: set_vertex,X24: set_vertex,X25: map_vertex_int] :
( subset(vertex,t2tb(X22),t2tb(v1))
& ! [X26: vertex1] :
( ~ mem(vertex,t2tb2(X26),t2tb(X23))
| path1(X1,X26,tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X26)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X1))) )
& subset(vertex,t2tb(X23),t2tb(v1))
& ! [X27: vertex1] :
( ~ mem(vertex,t2tb2(X27),t2tb(X22))
| ! [X28: vertex1] :
( ~ mem(vertex,t2tb2(X28),t2tb(g_succ1(X27)))
| ( ( X20 = X27 )
& ( mem(vertex,t2tb2(X28),t2tb(X24))
| ( X20 != X27 ) ) )
| ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X27))),weight1(X27,X28)),tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X28))))
& ( mem(vertex,t2tb2(X28),t2tb(X22))
| mem(vertex,t2tb2(X28),t2tb(X23)) ) ) ) )
& inv_src1(X1,X22,X23)
& ! [X29: vertex1] :
( ~ mem(vertex,t2tb2(X29),t2tb(X23))
| ~ mem(vertex,t2tb2(X29),t2tb(X22)) )
& ! [X30: vertex1] :
( mem(vertex,t2tb2(X30),t2tb(g_succ1(X20)))
| ~ mem(vertex,t2tb2(X30),t2tb(X24)) )
& ? [X31: bool1] :
( ? [X32: vertex1,X33: set_vertex] :
( ( tb2t(remove(vertex,t2tb2(X32),t2tb(X24))) = X33 )
& ? [X34: map_vertex_int,X35: set_vertex] :
( ( ( ~ mem(vertex,t2tb2(X32),t2tb(X22))
& ( tb2t1(set1(int,vertex,t2tb1(X25),t2tb2(X32),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X20))),weight1(X20,X32))))) = X34 )
& ( tb2t(add(vertex,t2tb2(X32),t2tb(X23))) = X35 )
& ~ mem(vertex,t2tb2(X32),t2tb(X23)) )
| ( mem(vertex,t2tb2(X32),t2tb(X22))
& ( X25 = X34 )
& ( X23 = X35 ) )
| ( ( X25 = X34 )
& mem(vertex,t2tb2(X32),t2tb(X35))
& ( X23 = X35 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X34),t2tb2(X20))),weight1(X20,X32)),tb2t3(get(int,vertex,t2tb1(X34),t2tb2(X32)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(X25),t2tb2(X32),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X20))),weight1(X20,X32))))) = X34 )
& mem(vertex,t2tb2(X32),t2tb(X35))
& ( X23 = X35 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X20))),weight1(X20,X32)),tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X32)))) ) )
& ? [X36: vertex1] :
( mem(vertex,t2tb2(X36),t2tb(X22))
& ? [X37: vertex1] :
( mem(vertex,t2tb2(X37),t2tb(g_succ1(X36)))
& ~ mem(vertex,t2tb2(X37),t2tb(X35))
& ( ( X20 != X36 )
| ( ( X20 = X36 )
& ~ mem(vertex,t2tb2(X37),t2tb(X33)) ) )
& ~ mem(vertex,t2tb2(X37),t2tb(X22)) ) )
& ( ( tb2t3(get(int,vertex,t2tb1(X34),t2tb2(X32))) = $sum(tb2t3(get(int,vertex,t2tb1(X34),t2tb2(X20))),weight1(X20,X32)) )
| $less(tb2t3(get(int,vertex,t2tb1(X34),t2tb2(X32))),$sum(tb2t3(get(int,vertex,t2tb1(X34),t2tb2(X20))),weight1(X20,X32))) ) )
& mem(vertex,t2tb2(X32),t2tb(X24)) )
& ( true1 = X31 )
& ( ? [X38: vertex1] : mem(vertex,t2tb2(X38),t2tb(X24))
| ( true1 != X31 ) )
& ( ( true1 = X31 )
| ! [X39: vertex1] : ~ mem(vertex,t2tb2(X39),t2tb(X24)) )
& ? [X40: vertex1] : mem(vertex,t2tb2(X40),t2tb(X24)) )
& ! [X41: vertex1] :
( shortest_path1(X1,X41,tb2t3(get(int,vertex,t2tb1(X25),t2tb2(X41))))
| ~ mem(vertex,t2tb2(X41),t2tb(X22)) ) ) )
& ! [X42: vertex1] :
( ~ $less(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X42))),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X20))))
| ~ mem(vertex,t2tb2(X42),t2tb(X8)) )
& ! [X43: $int] :
( ~ path1(X1,X20,X43)
| ~ $less(X43,tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X20)))) ) )
& ( true1 != X16 ) )
& ! [X44: vertex1] :
( ~ mem(vertex,t2tb2(X44),t2tb(X6))
| ! [X45: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X44))),weight1(X44,X45)),tb2t3(get(int,vertex,t2tb1(X7),t2tb2(X45))))
& ( mem(vertex,t2tb2(X45),t2tb(X6))
| mem(vertex,t2tb2(X45),t2tb(X8)) ) )
| ~ mem(vertex,t2tb2(X45),t2tb(g_succ1(X44))) ) ) )
& ! [X46: vertex1] : ~ mem(vertex,t2tb2(X46),t2tb(X3))
& ( tb2t(add(vertex,t2tb2(X1),empty(vertex))) = X4 )
& ( tb2t1(set1(int,vertex,t2tb1(X2),t2tb2(X1),t2tb3(0))) = X5 ) )
& mem(vertex,t2tb2(X0),t2tb(v1)) ),
inference(rectify,[],[f234]) ).
tff(f236,plain,
( mem(vertex,t2tb2(sK3),t2tb(v1))
& ! [X9: vertex1] :
( ( $less(tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(sK11(X9)))),tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X9))))
& mem(vertex,t2tb2(sK11(X9)),t2tb(sK10)) )
| ! [X11: vertex1,X12: $int] :
( ~ path1(sK3,X11,X12)
| mem(vertex,t2tb2(X11),t2tb(sK8))
| ~ $less(X12,tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X9)))) )
| ~ mem(vertex,t2tb2(X9),t2tb(sK10)) )
& inv_src1(sK3,sK8,sK10)
& subset(vertex,t2tb(sK8),t2tb(v1))
& ! [X13: vertex1] :
( shortest_path1(sK3,X13,tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X13))))
| ~ mem(vertex,t2tb2(X13),t2tb(sK8)) )
& ! [X14: vertex1] :
( ~ mem(vertex,t2tb2(X14),t2tb(sK8))
| ~ mem(vertex,t2tb2(X14),t2tb(sK10)) )
& ! [X15: vertex1] :
( ~ mem(vertex,t2tb2(X15),t2tb(sK10))
| path1(sK3,X15,tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X15)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(sK3))) )
& subset(vertex,t2tb(sK10),t2tb(v1))
& mem(vertex,t2tb2(sK13),t2tb(sK10))
& ( ( true1 = sK12 )
| mem(vertex,t2tb2(sK14),t2tb(sK10)) )
& ( ! [X19: vertex1] : ~ mem(vertex,t2tb2(X19),t2tb(sK10))
| ( true1 != sK12 ) )
& ( tb2t(remove(vertex,t2tb2(sK15),t2tb(sK10))) = sK16 )
& mem(vertex,t2tb2(sK15),t2tb(sK10))
& path1(sK3,sK15,tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(sK15))))
& ( sK17 = tb2t(add(vertex,t2tb2(sK15),t2tb(sK8))) )
& subset(vertex,t2tb(sK17),t2tb(v1))
& ! [X26: vertex1] :
( ~ mem(vertex,t2tb2(X26),t2tb(sK18))
| path1(sK3,X26,tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(X26)))) )
& ( 0 = tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(sK3))) )
& subset(vertex,t2tb(sK18),t2tb(v1))
& ! [X27: vertex1] :
( ~ mem(vertex,t2tb2(X27),t2tb(sK17))
| ! [X28: vertex1] :
( ~ mem(vertex,t2tb2(X28),t2tb(g_succ1(X27)))
| ( ( sK15 = X27 )
& ( mem(vertex,t2tb2(X28),t2tb(sK19))
| ( sK15 != X27 ) ) )
| ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(X27))),weight1(X27,X28)),tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(X28))))
& ( mem(vertex,t2tb2(X28),t2tb(sK17))
| mem(vertex,t2tb2(X28),t2tb(sK18)) ) ) ) )
& inv_src1(sK3,sK17,sK18)
& ! [X29: vertex1] :
( ~ mem(vertex,t2tb2(X29),t2tb(sK18))
| ~ mem(vertex,t2tb2(X29),t2tb(sK17)) )
& ! [X30: vertex1] :
( mem(vertex,t2tb2(X30),t2tb(g_succ1(sK15)))
| ~ mem(vertex,t2tb2(X30),t2tb(sK19)) )
& ( sK23 = tb2t(remove(vertex,t2tb2(sK22),t2tb(sK19))) )
& ( ( ~ mem(vertex,t2tb2(sK22),t2tb(sK17))
& ( tb2t1(set1(int,vertex,t2tb1(sK20),t2tb2(sK22),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(sK15))),weight1(sK15,sK22))))) = sK24 )
& ( sK25 = tb2t(add(vertex,t2tb2(sK22),t2tb(sK18))) )
& ~ mem(vertex,t2tb2(sK22),t2tb(sK18)) )
| ( mem(vertex,t2tb2(sK22),t2tb(sK17))
& ( sK24 = sK20 )
& ( sK25 = sK18 ) )
| ( ( sK24 = sK20 )
& mem(vertex,t2tb2(sK22),t2tb(sK25))
& ( sK25 = sK18 )
& ~ $less($sum(tb2t3(get(int,vertex,t2tb1(sK24),t2tb2(sK15))),weight1(sK15,sK22)),tb2t3(get(int,vertex,t2tb1(sK24),t2tb2(sK22)))) )
| ( ( tb2t1(set1(int,vertex,t2tb1(sK20),t2tb2(sK22),t2tb3($sum(tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(sK15))),weight1(sK15,sK22))))) = sK24 )
& mem(vertex,t2tb2(sK22),t2tb(sK25))
& ( sK25 = sK18 )
& $less($sum(tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(sK15))),weight1(sK15,sK22)),tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(sK22)))) ) )
& mem(vertex,t2tb2(sK26),t2tb(sK17))
& mem(vertex,t2tb2(sK27),t2tb(g_succ1(sK26)))
& ~ mem(vertex,t2tb2(sK27),t2tb(sK25))
& ( ( sK15 != sK26 )
| ( ( sK15 = sK26 )
& ~ mem(vertex,t2tb2(sK27),t2tb(sK23)) ) )
& ~ mem(vertex,t2tb2(sK27),t2tb(sK17))
& ( ( tb2t3(get(int,vertex,t2tb1(sK24),t2tb2(sK22))) = $sum(tb2t3(get(int,vertex,t2tb1(sK24),t2tb2(sK15))),weight1(sK15,sK22)) )
| $less(tb2t3(get(int,vertex,t2tb1(sK24),t2tb2(sK22))),$sum(tb2t3(get(int,vertex,t2tb1(sK24),t2tb2(sK15))),weight1(sK15,sK22))) )
& mem(vertex,t2tb2(sK22),t2tb(sK19))
& ( true1 = sK21 )
& ( mem(vertex,t2tb2(sK28),t2tb(sK19))
| ( true1 != sK21 ) )
& ( ( true1 = sK21 )
| ! [X39: vertex1] : ~ mem(vertex,t2tb2(X39),t2tb(sK19)) )
& mem(vertex,t2tb2(sK29),t2tb(sK19))
& ! [X41: vertex1] :
( shortest_path1(sK3,X41,tb2t3(get(int,vertex,t2tb1(sK20),t2tb2(X41))))
| ~ mem(vertex,t2tb2(X41),t2tb(sK17)) )
& ! [X42: vertex1] :
( ~ $less(tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X42))),tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(sK15))))
| ~ mem(vertex,t2tb2(X42),t2tb(sK10)) )
& ! [X43: $int] :
( ~ path1(sK3,sK15,X43)
| ~ $less(X43,tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(sK15)))) )
& ( true1 != sK12 )
& ! [X44: vertex1] :
( ~ mem(vertex,t2tb2(X44),t2tb(sK8))
| ! [X45: vertex1] :
( ( ~ $less($sum(tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X44))),weight1(X44,X45)),tb2t3(get(int,vertex,t2tb1(sK9),t2tb2(X45))))
& ( mem(vertex,t2tb2(X45),t2tb(sK8))
| mem(vertex,t2tb2(X45),t2tb(sK10)) ) )
| ~ mem(vertex,t2tb2(X45),t2tb(g_succ1(X44))) ) )
& ! [X46: vertex1] : ~ mem(vertex,t2tb2(X46),t2tb(sK5))
& ( sK6 = tb2t(add(vertex,t2tb2(sK3),empty(vertex))) )
& ( sK7 = tb2t1(set1(int,vertex,t2tb1(sK4),t2tb2(sK3),t2tb3(0))) )
& mem(vertex,t2tb2(sK2),t2tb(v1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10),skolemize(X10,sK11(X9)),skolemize(X16,sK12),skolemize(X17,sK13),skolemize(X18,sK14),skolemize(X20,sK15),skolemize(X21,sK16),skolemize(X22,sK17),skolemize(X23,sK18),skolemize(X24,sK19),skolemize(X25,sK20),skolemize(X31,sK21),skolemize(X32,sK22),skolemize(X33,sK23),skolemize(X34,sK24),skolemize(X35,sK25),skolemize(X36,sK26),skolemize(X37,sK27),skolemize(X38,sK28),skolemize(X40,sK29)],[f235]) ).
tff(f240,plain,
! [X0: uni,X1: uni,X2: ty] : ( remove(X2,X0,add(X2,X0,X1)) = remove(X2,X0,X1) ),
inference(rectify,[],[f140]) ).
tff(f244,plain,
! [X0: uni,X1: uni,X2: ty] : sort1(set(X2),remove(X2,X1,X0)),
inference(rectify,[],[f155]) ).
tff(f258,plain,
! [X3: ty,X2: uni,X0: uni,X1: uni] :
( ~ sort1(X3,X0)
| ( ( ( mem(X3,X1,X2)
& ( X0 != X1 ) )
| ~ mem(X3,X1,remove(X3,X0,X2)) )
& ( mem(X3,X1,remove(X3,X0,X2))
| ~ mem(X3,X1,X2)
| ( X0 = X1 ) ) )
| ~ sort1(X3,X1) ),
inference(nnf_transformation,[],[f183]) ).
tff(f259,plain,
! [X3: ty,X2: uni,X0: uni,X1: uni] :
( ~ sort1(X3,X0)
| ( ( ( mem(X3,X1,X2)
& ( X0 != X1 ) )
| ~ mem(X3,X1,remove(X3,X0,X2)) )
& ( mem(X3,X1,remove(X3,X0,X2))
| ~ mem(X3,X1,X2)
| ( X0 = X1 ) ) )
| ~ sort1(X3,X1) ),
inference(flattening,[],[f258]) ).
tff(f260,plain,
! [X0: ty,X1: uni,X2: uni,X3: uni] :
( ~ sort1(X0,X2)
| ( ( ( mem(X0,X3,X1)
& ( X2 != X3 ) )
| ~ mem(X0,X3,remove(X0,X2,X1)) )
& ( mem(X0,X3,remove(X0,X2,X1))
| ~ mem(X0,X3,X1)
| ( X2 = X3 ) ) )
| ~ sort1(X0,X3) ),
inference(rectify,[],[f259]) ).
tff(f288,plain,
! [X2: ty,X0: uni,X1: uni] :
( ( add(X2,X0,remove(X2,X0,X1)) = X1 )
| ~ sort1(set(X2),X1)
| ~ mem(X2,X0,X1) ),
inference(cnf_transformation,[],[f200]) ).
tff(f296,plain,
! [X0: uni] :
( ( t2tb(tb2t(X0)) = X0 )
| ~ sort1(set(vertex),X0) ),
inference(cnf_transformation,[],[f190]) ).
tff(f306,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] :
( ~ sort1(X1,X2)
| ~ sort1(X1,X0)
| mem(X1,X2,add(X1,X0,X3))
| ( X0 != X2 ) ),
inference(cnf_transformation,[],[f229]) ).
tff(f307,plain,
! [X2: uni,X3: uni,X0: uni,X1: ty] :
( mem(X1,X2,add(X1,X0,X3))
| ~ sort1(X1,X0)
| ~ sort1(X1,X2)
| ~ mem(X1,X2,X3) ),
inference(cnf_transformation,[],[f229]) ).
tff(f309,plain,
! [X0: set_vertex] : sort1(set(vertex),t2tb(X0)),
inference(cnf_transformation,[],[f50]) ).
tff(f329,plain,
mem(vertex,t2tb2(sK22),t2tb(sK19)),
inference(cnf_transformation,[],[f236]) ).
tff(f331,plain,
~ mem(vertex,t2tb2(sK27),t2tb(sK17)),
inference(cnf_transformation,[],[f236]) ).
tff(f332,plain,
( ( sK15 != sK26 )
| ~ mem(vertex,t2tb2(sK27),t2tb(sK23)) ),
inference(cnf_transformation,[],[f236]) ).
tff(f334,plain,
~ mem(vertex,t2tb2(sK27),t2tb(sK25)),
inference(cnf_transformation,[],[f236]) ).
tff(f335,plain,
mem(vertex,t2tb2(sK27),t2tb(g_succ1(sK26))),
inference(cnf_transformation,[],[f236]) ).
tff(f336,plain,
mem(vertex,t2tb2(sK26),t2tb(sK17)),
inference(cnf_transformation,[],[f236]) ).
tff(f390,plain,
( ( sK25 = tb2t(add(vertex,t2tb2(sK22),t2tb(sK18))) )
| ( sK25 = sK18 )
| ( sK25 = sK18 )
| ( sK25 = sK18 ) ),
inference(cnf_transformation,[],[f236]) ).
tff(f427,plain,
( ( sK25 = tb2t(add(vertex,t2tb2(sK22),t2tb(sK18))) )
| mem(vertex,t2tb2(sK22),t2tb(sK17))
| mem(vertex,t2tb2(sK22),t2tb(sK25))
| mem(vertex,t2tb2(sK22),t2tb(sK25)) ),
inference(cnf_transformation,[],[f236]) ).
tff(f529,plain,
sK23 = tb2t(remove(vertex,t2tb2(sK22),t2tb(sK19))),
inference(cnf_transformation,[],[f236]) ).
tff(f533,plain,
! [X28: vertex1,X27: vertex1] :
( ~ mem(vertex,t2tb2(X27),t2tb(sK17))
| ~ mem(vertex,t2tb2(X28),t2tb(g_succ1(X27)))
| mem(vertex,t2tb2(X28),t2tb(sK19))
| ( sK15 != X27 )
| mem(vertex,t2tb2(X28),t2tb(sK17))
| mem(vertex,t2tb2(X28),t2tb(sK18)) ),
inference(cnf_transformation,[],[f236]) ).
tff(f535,plain,
! [X28: vertex1,X27: vertex1] :
( ~ mem(vertex,t2tb2(X27),t2tb(sK17))
| ~ mem(vertex,t2tb2(X28),t2tb(g_succ1(X27)))
| ( sK15 = X27 )
| mem(vertex,t2tb2(X28),t2tb(sK17))
| mem(vertex,t2tb2(X28),t2tb(sK18)) ),
inference(cnf_transformation,[],[f236]) ).
tff(f541,plain,
sK17 = tb2t(add(vertex,t2tb2(sK15),t2tb(sK8))),
inference(cnf_transformation,[],[f236]) ).
tff(f564,plain,
! [X2: ty,X0: uni,X1: uni] : ( remove(X2,X0,add(X2,X0,X1)) = remove(X2,X0,X1) ),
inference(cnf_transformation,[],[f240]) ).
tff(f572,plain,
! [X2: ty,X0: uni,X1: uni] : sort1(set(X2),remove(X2,X1,X0)),
inference(cnf_transformation,[],[f244]) ).
tff(f593,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( mem(X0,X3,remove(X0,X2,X1))
| ~ sort1(X0,X3)
| ~ sort1(X0,X2)
| ~ mem(X0,X3,X1)
| ( X2 = X3 ) ),
inference(cnf_transformation,[],[f260]) ).
tff(f628,plain,
! [X0: vertex1] : sort1(vertex,t2tb2(X0)),
inference(cnf_transformation,[],[f58]) ).
tff(f630,plain,
! [X2: uni,X0: uni,X1: ty] : sort1(set(X1),add(X1,X0,X2)),
inference(cnf_transformation,[],[f153]) ).
tff(f640,plain,
! [X2: uni,X3: uni,X1: ty] :
( ~ sort1(X1,X2)
| ~ sort1(X1,X2)
| mem(X1,X2,add(X1,X2,X3)) ),
inference(equality_resolution,[],[f306]) ).
tff(f642,plain,
! [X28: vertex1] :
( ~ mem(vertex,t2tb2(sK15),t2tb(sK17))
| ~ mem(vertex,t2tb2(X28),t2tb(g_succ1(sK15)))
| mem(vertex,t2tb2(X28),t2tb(sK19))
| mem(vertex,t2tb2(X28),t2tb(sK17))
| mem(vertex,t2tb2(X28),t2tb(sK18)) ),
inference(equality_resolution,[],[f533]) ).
tff(f660,definition,
sF50 = t2tb(sK8),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
tff(f661,plain,
t2tb(sK8) = sF50,
inference(reorient_equations,[],[f660]) ).
tff(f680,definition,
sF56 = t2tb2(sK15),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
tff(f691,definition,
sF61 = add(vertex,sF56,sF50),
introduced(definition,[new_symbols(definition,[sF61])],[function_definition]) ).
tff(f692,definition,
sF62 = tb2t(sF61),
introduced(definition,[new_symbols(definition,[sF62])],[function_definition]) ).
tff(f693,plain,
sF62 = sK17,
inference(definition_folding,[],[f541,f692,f691,f661,f680]) ).
tff(f694,definition,
sF63 = t2tb(sK17),
introduced(definition,[new_symbols(definition,[sF63])],[function_definition]) ).
tff(f696,definition,
sF64 = t2tb(sK18),
introduced(definition,[new_symbols(definition,[sF64])],[function_definition]) ).
tff(f708,definition,
! [X27: vertex1] : ( sF70(X27) = t2tb(g_succ1(X27)) ),
introduced(definition,[new_symbols(definition,[sF70])],[function_definition]) ).
tff(f712,plain,
! [X28: vertex1,X27: vertex1] :
( mem(vertex,t2tb2(X28),sF63)
| ~ mem(vertex,t2tb2(X27),sF63)
| mem(vertex,t2tb2(X28),sF64)
| ~ mem(vertex,t2tb2(X28),sF70(X27))
| ( sK15 = X27 ) ),
inference(definition_folding,[],[f535,f696,f694,f708,f694]) ).
tff(f713,definition,
sF72 = g_succ1(sK15),
introduced(definition,[new_symbols(definition,[sF72])],[function_definition]) ).
tff(f714,definition,
sF73 = t2tb(sF72),
introduced(definition,[new_symbols(definition,[sF73])],[function_definition]) ).
tff(f715,definition,
sF74 = t2tb(sK19),
introduced(definition,[new_symbols(definition,[sF74])],[function_definition]) ).
tff(f723,plain,
! [X28: vertex1] :
( ~ mem(vertex,sF56,sF63)
| mem(vertex,t2tb2(X28),sF63)
| mem(vertex,t2tb2(X28),sF64)
| ~ mem(vertex,t2tb2(X28),sF73)
| mem(vertex,t2tb2(X28),sF74) ),
inference(definition_folding,[],[f642,f696,f694,f715,f714,f713,f694,f680]) ).
tff(f726,definition,
sF79 = t2tb2(sK22),
introduced(definition,[new_symbols(definition,[sF79])],[function_definition]) ).
tff(f727,definition,
sF80 = remove(vertex,sF79,sF74),
introduced(definition,[new_symbols(definition,[sF80])],[function_definition]) ).
tff(f728,definition,
sF81 = tb2t(sF80),
introduced(definition,[new_symbols(definition,[sF81])],[function_definition]) ).
tff(f729,plain,
sF81 = sK23,
inference(definition_folding,[],[f529,f728,f727,f715,f726]) ).
tff(f737,definition,
sF87 = t2tb(sK25),
introduced(definition,[new_symbols(definition,[sF87])],[function_definition]) ).
tff(f845,definition,
sF96 = add(vertex,sF79,sF64),
introduced(definition,[new_symbols(definition,[sF96])],[function_definition]) ).
tff(f846,definition,
sF97 = tb2t(sF96),
introduced(definition,[new_symbols(definition,[sF97])],[function_definition]) ).
tff(f852,plain,
( ( sK25 = sF97 )
| mem(vertex,sF79,sF87)
| mem(vertex,sF79,sF63)
| mem(vertex,sF79,sF87) ),
inference(definition_folding,[],[f427,f737,f726,f737,f726,f694,f726,f846,f845,f696,f726]) ).
tff(f889,plain,
( ( sK25 = sK18 )
| ( sK25 = sK18 )
| ( sK25 = sK18 )
| ( sK25 = sF97 ) ),
inference(definition_folding,[],[f390,f846,f845,f696,f726]) ).
tff(f943,definition,
sF98 = t2tb2(sK26),
introduced(definition,[new_symbols(definition,[sF98])],[function_definition]) ).
tff(f944,plain,
t2tb2(sK26) = sF98,
inference(reorient_equations,[],[f943]) ).
tff(f945,plain,
mem(vertex,sF98,sF63),
inference(definition_folding,[],[f336,f694,f944]) ).
tff(f946,definition,
sF99 = t2tb2(sK27),
introduced(definition,[new_symbols(definition,[sF99])],[function_definition]) ).
tff(f947,plain,
t2tb2(sK27) = sF99,
inference(reorient_equations,[],[f946]) ).
tff(f948,definition,
sF100 = g_succ1(sK26),
introduced(definition,[new_symbols(definition,[sF100])],[function_definition]) ).
tff(f949,plain,
g_succ1(sK26) = sF100,
inference(reorient_equations,[],[f948]) ).
tff(f950,definition,
sF101 = t2tb(sF100),
introduced(definition,[new_symbols(definition,[sF101])],[function_definition]) ).
tff(f951,plain,
mem(vertex,sF99,sF101),
inference(definition_folding,[],[f335,f950,f949,f947]) ).
tff(f952,plain,
~ mem(vertex,sF99,sF87),
inference(definition_folding,[],[f334,f737,f947]) ).
tff(f953,definition,
sF102 = t2tb(sK23),
introduced(definition,[new_symbols(definition,[sF102])],[function_definition]) ).
tff(f954,plain,
( ( sK15 != sK26 )
| ~ mem(vertex,sF99,sF102) ),
inference(definition_folding,[],[f332,f953,f947]) ).
tff(f955,plain,
~ mem(vertex,sF99,sF63),
inference(definition_folding,[],[f331,f694,f947]) ).
tff(f957,plain,
mem(vertex,sF79,sF74),
inference(definition_folding,[],[f329,f715,f726]) ).
tff(f1009,plain,
( mem(vertex,sF79,sF87)
| mem(vertex,sF79,sF63)
| ( sK25 = sF97 ) ),
inference(duplicate_literal_removal,[],[f852]) ).
tff(f1013,plain,
( ( sK25 = sK18 )
| ( sK25 = sF97 ) ),
inference(duplicate_literal_removal,[],[f889]) ).
tff(f1016,plain,
! [X2: uni,X3: uni,X1: ty] :
( mem(X1,X2,add(X1,X2,X3))
| ~ sort1(X1,X2) ),
inference(duplicate_literal_removal,[],[f640]) ).
tff(f1083,definition,
( spl115_4
<=> ( sK25 = sK18 ) ),
introduced(definition,[new_symbols(definition,[spl115_4])],[avatar_definition]) ).
tff(f1085,plain,
( ( sK25 = sK18 )
| ~ spl115_4 ),
inference(avatar_component_clause,[],[f1083]) ).
tff(f1088,definition,
( spl115_5
<=> ( sK25 = sF97 ) ),
introduced(definition,[new_symbols(definition,[spl115_5])],[avatar_definition]) ).
tff(f1089,plain,
( ( sK25 != sF97 )
| spl115_5 ),
inference(avatar_component_clause,[],[f1088]) ).
tff(f1090,plain,
( ( sK25 = sF97 )
| ~ spl115_5 ),
inference(avatar_component_clause,[],[f1088]) ).
tff(f1091,plain,
( spl115_5
| spl115_4 ),
inference(avatar_split_clause,[],[f1013,f1083,f1088]) ).
tff(f1098,definition,
( spl115_6
<=> mem(vertex,sF99,sF102) ),
introduced(definition,[new_symbols(definition,[spl115_6])],[avatar_definition]) ).
tff(f1100,plain,
( ~ mem(vertex,sF99,sF102)
| spl115_6 ),
inference(avatar_component_clause,[],[f1098]) ).
tff(f1102,definition,
( spl115_7
<=> ( sK15 = sK26 ) ),
introduced(definition,[new_symbols(definition,[spl115_7])],[avatar_definition]) ).
tff(f1103,plain,
( ( sK15 = sK26 )
| ~ spl115_7 ),
inference(avatar_component_clause,[],[f1102]) ).
tff(f1105,plain,
( ~ spl115_6
| ~ spl115_7 ),
inference(avatar_split_clause,[],[f954,f1102,f1098]) ).
tff(f1114,plain,
sort1(vertex,sF56),
inference(superposition,[],[f628,f680]) ).
tff(f1116,plain,
sK17 = tb2t(sF61),
inference(forward_demodulation,[],[f692,f693]) ).
tff(f1117,plain,
( ( sF64 = t2tb(sK25) )
| ~ spl115_4 ),
inference(forward_demodulation,[],[f696,f1085]) ).
tff(f1119,plain,
sort1(vertex,sF79),
inference(superposition,[],[f628,f726]) ).
tff(f1123,plain,
( ( sF64 = sF87 )
| ~ spl115_4 ),
inference(superposition,[],[f737,f1117]) ).
tff(f1128,plain,
sort1(vertex,sF99),
inference(superposition,[],[f628,f947]) ).
tff(f1130,plain,
t2tb(sF81) = sF102,
inference(forward_demodulation,[],[f953,f729]) ).
tff(f1223,definition,
( spl115_20
<=> mem(vertex,sF79,sF63) ),
introduced(definition,[new_symbols(definition,[spl115_20])],[avatar_definition]) ).
tff(f1224,plain,
( mem(vertex,sF79,sF63)
| ~ spl115_20 ),
inference(avatar_component_clause,[],[f1223]) ).
tff(f1225,plain,
( ~ mem(vertex,sF79,sF63)
| spl115_20 ),
inference(avatar_component_clause,[],[f1223]) ).
tff(f1257,definition,
( spl115_25
<=> mem(vertex,sF79,sF87) ),
introduced(definition,[new_symbols(definition,[spl115_25])],[avatar_definition]) ).
tff(f1258,plain,
( mem(vertex,sF79,sF87)
| ~ spl115_25 ),
inference(avatar_component_clause,[],[f1257]) ).
tff(f1259,plain,
( ~ mem(vertex,sF79,sF87)
| spl115_25 ),
inference(avatar_component_clause,[],[f1257]) ).
tff(f1289,plain,
sort1(set(vertex),sF74),
inference(superposition,[],[f309,f715]) ).
tff(f1393,definition,
( spl115_38
<=> mem(vertex,sF99,sF73) ),
introduced(definition,[new_symbols(definition,[spl115_38])],[avatar_definition]) ).
tff(f1394,plain,
( ~ mem(vertex,sF99,sF73)
| spl115_38 ),
inference(avatar_component_clause,[],[f1393]) ).
tff(f1397,definition,
( spl115_39
<=> mem(vertex,sF99,sF74) ),
introduced(definition,[new_symbols(definition,[spl115_39])],[avatar_definition]) ).
tff(f1398,plain,
( mem(vertex,sF99,sF74)
| ~ spl115_39 ),
inference(avatar_component_clause,[],[f1397]) ).
tff(f1399,plain,
( ~ mem(vertex,sF99,sF74)
| spl115_39 ),
inference(avatar_component_clause,[],[f1397]) ).
tff(f1410,plain,
sF70(sK15) = t2tb(sF72),
inference(superposition,[],[f708,f713]) ).
tff(f1411,plain,
t2tb(sF100) = sF70(sK26),
inference(superposition,[],[f708,f949]) ).
tff(f1414,plain,
sF73 = sF70(sK15),
inference(forward_demodulation,[],[f1410,f714]) ).
tff(f1415,plain,
sF101 = sF70(sK26),
inference(forward_demodulation,[],[f1411,f950]) ).
tff(f1514,plain,
sort1(set(vertex),sF61),
inference(superposition,[],[f630,f691]) ).
tff(f1563,plain,
( ( sF61 = t2tb(sK17) )
| ~ sort1(set(vertex),sF61) ),
inference(superposition,[],[f296,f1116]) ).
tff(f1567,plain,
( ( t2tb(sF81) = sF80 )
| ~ sort1(set(vertex),sF80) ),
inference(superposition,[],[f296,f728]) ).
tff(f1569,plain,
( ( t2tb(sF97) = sF96 )
| ~ sort1(set(vertex),sF96) ),
inference(superposition,[],[f296,f846]) ).
tff(f1575,plain,
( ( sF102 = sF80 )
| ~ sort1(set(vertex),sF80) ),
inference(forward_demodulation,[],[f1567,f1130]) ).
tff(f1576,plain,
( ( sF61 = sF63 )
| ~ sort1(set(vertex),sF61) ),
inference(forward_demodulation,[],[f1563,f694]) ).
tff(f1679,plain,
( mem(vertex,sF56,sF61)
| ~ sort1(vertex,sF56) ),
inference(superposition,[],[f1016,f691]) ).
tff(f1683,plain,
mem(vertex,sF56,sF61),
inference(forward_subsumption_resolution,[],[f1679,f1114]) ).
tff(f1712,plain,
( ( sK25 = sF97 )
| mem(vertex,sF79,sF63)
| spl115_25 ),
inference(forward_subsumption_resolution,[],[f1009,f1259]) ).
tff(f1722,plain,
( ( sK25 = sF97 )
| spl115_20
| spl115_25 ),
inference(forward_subsumption_resolution,[],[f1712,f1225]) ).
tff(f1727,plain,
( $false
| spl115_5
| spl115_20
| spl115_25 ),
inference(forward_subsumption_resolution,[],[f1722,f1089]) ).
tff(f1728,plain,
( spl115_5
| spl115_20
| spl115_25 ),
inference(avatar_contradiction_clause,[],[f1727]) ).
tff(f1801,definition,
( spl115_54
<=> sort1(set(vertex),sF80) ),
introduced(definition,[new_symbols(definition,[spl115_54])],[avatar_definition]) ).
tff(f1803,plain,
( ~ sort1(set(vertex),sF80)
| spl115_54 ),
inference(avatar_component_clause,[],[f1801]) ).
tff(f1805,definition,
( spl115_55
<=> ( sF102 = sF80 ) ),
introduced(definition,[new_symbols(definition,[spl115_55])],[avatar_definition]) ).
tff(f1807,plain,
( ( sF102 = sF80 )
| ~ spl115_55 ),
inference(avatar_component_clause,[],[f1805]) ).
tff(f1808,plain,
( ~ spl115_54
| spl115_55 ),
inference(avatar_split_clause,[],[f1575,f1805,f1801]) ).
tff(f1812,definition,
( spl115_56
<=> sort1(set(vertex),sF61) ),
introduced(definition,[new_symbols(definition,[spl115_56])],[avatar_definition]) ).
tff(f1814,plain,
( ~ sort1(set(vertex),sF61)
| spl115_56 ),
inference(avatar_component_clause,[],[f1812]) ).
tff(f1816,definition,
( spl115_57
<=> ( sF61 = sF63 ) ),
introduced(definition,[new_symbols(definition,[spl115_57])],[avatar_definition]) ).
tff(f1818,plain,
( ( sF61 = sF63 )
| ~ spl115_57 ),
inference(avatar_component_clause,[],[f1816]) ).
tff(f1819,plain,
( ~ spl115_56
| spl115_57 ),
inference(avatar_split_clause,[],[f1576,f1816,f1812]) ).
tff(f1892,plain,
( ( add(vertex,sF79,sF80) = sF74 )
| ~ sort1(set(vertex),sF74)
| ~ mem(vertex,sF79,sF74) ),
inference(superposition,[],[f288,f727]) ).
tff(f1899,plain,
( ~ mem(vertex,sF79,sF74)
| ( add(vertex,sF79,sF80) = sF74 ) ),
inference(forward_subsumption_resolution,[],[f1892,f1289]) ).
tff(f1902,plain,
add(vertex,sF79,sF80) = sF74,
inference(forward_subsumption_resolution,[],[f1899,f957]) ).
tff(f2014,plain,
remove(vertex,sF79,sF80) = remove(vertex,sF79,sF74),
inference(superposition,[],[f564,f1902]) ).
tff(f2017,plain,
remove(vertex,sF79,sF80) = sF80,
inference(forward_demodulation,[],[f2014,f727]) ).
tff(f2030,plain,
sort1(set(vertex),sF80),
inference(superposition,[],[f572,f2017]) ).
tff(f2032,plain,
( $false
| spl115_54 ),
inference(forward_subsumption_resolution,[],[f2030,f1803]) ).
tff(f2033,plain,
spl115_54,
inference(avatar_contradiction_clause,[],[f2032]) ).
tff(f2037,plain,
( ~ mem(vertex,sF99,sF80)
| spl115_6
| ~ spl115_55 ),
inference(superposition,[],[f1100,f1807]) ).
tff(f2055,plain,
! [X0: uni] :
( ~ sort1(vertex,sF79)
| mem(vertex,X0,sF96)
| ~ mem(vertex,X0,sF64)
| ~ sort1(vertex,X0) ),
inference(superposition,[],[f307,f845]) ).
tff(f2058,plain,
( ~ sort1(vertex,sF79)
| mem(vertex,sF79,sF96) ),
inference(superposition,[],[f1016,f845]) ).
tff(f2059,plain,
sort1(set(vertex),sF96),
inference(superposition,[],[f630,f845]) ).
tff(f2060,plain,
! [X0: uni] :
( ~ mem(vertex,X0,sF64)
| mem(vertex,X0,sF96)
| ~ sort1(vertex,X0) ),
inference(forward_subsumption_resolution,[],[f2055,f1119]) ).
tff(f2061,plain,
mem(vertex,sF79,sF96),
inference(forward_subsumption_resolution,[],[f2058,f1119]) ).
tff(f2073,plain,
! [X0: vertex1] :
( mem(vertex,sF99,sF63)
| ( sK15 = X0 )
| ~ mem(vertex,t2tb2(X0),sF63)
| mem(vertex,sF99,sF64)
| ~ mem(vertex,sF99,sF70(X0)) ),
inference(superposition,[],[f712,f947]) ).
tff(f2080,plain,
! [X0: vertex1] :
( ( sK15 = X0 )
| ~ mem(vertex,sF99,sF70(X0))
| ~ mem(vertex,t2tb2(X0),sF63)
| mem(vertex,sF99,sF64) ),
inference(forward_subsumption_resolution,[],[f2073,f955]) ).
tff(f2141,plain,
! [X0: uni] :
( mem(vertex,X0,sF80)
| ~ sort1(vertex,X0)
| ~ sort1(vertex,sF79)
| ~ mem(vertex,X0,sF74)
| ( sF79 = X0 ) ),
inference(superposition,[],[f593,f727]) ).
tff(f2146,plain,
! [X0: uni] :
( mem(vertex,X0,sF80)
| ~ sort1(vertex,X0)
| ~ mem(vertex,X0,sF74)
| ( sF79 = X0 ) ),
inference(forward_subsumption_resolution,[],[f2141,f1119]) ).
tff(f2278,plain,
( $false
| spl115_56 ),
inference(forward_subsumption_resolution,[],[f1514,f1814]) ).
tff(f2279,plain,
spl115_56,
inference(avatar_contradiction_clause,[],[f2278]) ).
tff(f2282,plain,
( mem(vertex,sF98,sF61)
| ~ spl115_57 ),
inference(superposition,[],[f945,f1818]) ).
tff(f2283,plain,
( ~ mem(vertex,sF99,sF61)
| ~ spl115_57 ),
inference(superposition,[],[f955,f1818]) ).
tff(f2318,plain,
( ! [X28: vertex1] :
( mem(vertex,t2tb2(X28),sF74)
| mem(vertex,t2tb2(X28),sF63)
| mem(vertex,t2tb2(X28),sF64)
| ~ mem(vertex,sF56,sF61)
| ~ mem(vertex,t2tb2(X28),sF73) )
| ~ spl115_57 ),
inference(forward_demodulation,[],[f723,f1818]) ).
tff(f2322,plain,
( ! [X28: vertex1] :
( mem(vertex,t2tb2(X28),sF63)
| ~ mem(vertex,t2tb2(X28),sF73)
| mem(vertex,t2tb2(X28),sF64)
| mem(vertex,t2tb2(X28),sF74) )
| ~ spl115_57 ),
inference(forward_subsumption_resolution,[],[f2318,f1683]) ).
tff(f2323,plain,
( ! [X28: vertex1] :
( mem(vertex,t2tb2(X28),sF74)
| mem(vertex,t2tb2(X28),sF61)
| ~ mem(vertex,t2tb2(X28),sF73)
| mem(vertex,t2tb2(X28),sF64) )
| ~ spl115_57 ),
inference(forward_demodulation,[],[f2322,f1818]) ).
tff(f2338,plain,
( ~ mem(vertex,sF99,sF73)
| mem(vertex,sF99,sF64)
| mem(vertex,sF99,sF74)
| mem(vertex,sF99,sF61)
| ~ spl115_57 ),
inference(superposition,[],[f2323,f947]) ).
tff(f2343,plain,
( mem(vertex,sF99,sF64)
| mem(vertex,sF99,sF61)
| ~ mem(vertex,sF99,sF73)
| spl115_39
| ~ spl115_57 ),
inference(forward_subsumption_resolution,[],[f2338,f1399]) ).
tff(f2347,plain,
( mem(vertex,sF99,sF64)
| ~ mem(vertex,sF99,sF73)
| spl115_39
| ~ spl115_57 ),
inference(forward_subsumption_resolution,[],[f2343,f2283]) ).
tff(f2356,definition,
( spl115_65
<=> mem(vertex,sF99,sF64) ),
introduced(definition,[new_symbols(definition,[spl115_65])],[avatar_definition]) ).
tff(f2358,plain,
( mem(vertex,sF99,sF64)
| ~ spl115_65 ),
inference(avatar_component_clause,[],[f2356]) ).
tff(f2359,plain,
( ~ spl115_38
| spl115_65
| spl115_39
| ~ spl115_57 ),
inference(avatar_split_clause,[],[f2347,f1816,f1397,f2356,f1393]) ).
tff(f2572,plain,
t2tb(sF97) = sF96,
inference(forward_subsumption_resolution,[],[f1569,f2059]) ).
tff(f2573,plain,
( ( sF96 = t2tb(sK25) )
| ~ spl115_5 ),
inference(forward_demodulation,[],[f2572,f1090]) ).
tff(f2574,plain,
( ( sF87 = sF96 )
| ~ spl115_5 ),
inference(superposition,[],[f2573,f737]) ).
tff(f2578,plain,
( ~ mem(vertex,sF99,sF96)
| ~ spl115_5 ),
inference(superposition,[],[f952,f2574]) ).
tff(f2748,plain,
( ! [X0: vertex1] :
( ~ mem(vertex,sF99,sF70(X0))
| mem(vertex,sF99,sF64)
| ~ mem(vertex,t2tb2(X0),sF61)
| ( sK15 = X0 ) )
| ~ spl115_57 ),
inference(forward_demodulation,[],[f2080,f1818]) ).
tff(f2791,definition,
( spl115_80
<=> ! [X0: vertex1] :
( ~ mem(vertex,sF99,sF70(X0))
| ( sK15 = X0 )
| ~ mem(vertex,t2tb2(X0),sF61) ) ),
introduced(definition,[new_symbols(definition,[spl115_80])],[avatar_definition]) ).
tff(f2792,plain,
( ! [X0: vertex1] :
( ~ mem(vertex,sF99,sF70(X0))
| ~ mem(vertex,t2tb2(X0),sF61)
| ( sK15 = X0 ) )
| ~ spl115_80 ),
inference(avatar_component_clause,[],[f2791]) ).
tff(f2793,plain,
( spl115_65
| spl115_80
| ~ spl115_57 ),
inference(avatar_split_clause,[],[f2748,f1816,f2791,f2356]) ).
tff(f3074,plain,
( ( sK15 = sK26 )
| ~ mem(vertex,t2tb2(sK26),sF61)
| ~ mem(vertex,sF99,sF101)
| ~ spl115_80 ),
inference(superposition,[],[f2792,f1415]) ).
tff(f3075,plain,
( ~ mem(vertex,t2tb2(sK26),sF61)
| ( sK15 = sK26 )
| ~ spl115_80 ),
inference(forward_subsumption_resolution,[],[f3074,f951]) ).
tff(f3076,plain,
( ( sK15 = sK26 )
| ~ mem(vertex,sF98,sF61)
| ~ spl115_80 ),
inference(forward_demodulation,[],[f3075,f944]) ).
tff(f3077,plain,
( ( sK15 = sK26 )
| ~ spl115_57
| ~ spl115_80 ),
inference(forward_subsumption_resolution,[],[f3076,f2282]) ).
tff(f3079,plain,
( spl115_7
| ~ spl115_57
| ~ spl115_80 ),
inference(avatar_split_clause,[],[f3077,f2791,f1816,f1102]) ).
tff(f3080,plain,
( ( sF101 = sF70(sK15) )
| ~ spl115_7 ),
inference(superposition,[],[f1415,f1103]) ).
tff(f3083,plain,
( ( sF101 = sF73 )
| ~ spl115_7 ),
inference(forward_demodulation,[],[f3080,f1414]) ).
tff(f3161,plain,
( mem(vertex,sF99,sF73)
| ~ spl115_7 ),
inference(superposition,[],[f951,f3083]) ).
tff(f3163,plain,
( $false
| ~ spl115_7
| spl115_38 ),
inference(forward_subsumption_resolution,[],[f3161,f1394]) ).
tff(f3164,plain,
( ~ spl115_7
| spl115_38 ),
inference(avatar_contradiction_clause,[],[f3163]) ).
tff(f3901,plain,
( ~ sort1(vertex,sF99)
| ( sF79 = sF99 )
| ~ mem(vertex,sF99,sF74)
| spl115_6
| ~ spl115_55 ),
inference(resolution,[],[f2146,f2037]) ).
tff(f3903,plain,
( ( sF79 = sF99 )
| ~ sort1(vertex,sF99)
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(forward_subsumption_resolution,[],[f3901,f1398]) ).
tff(f3904,plain,
( ( sF79 = sF99 )
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(forward_subsumption_resolution,[],[f3903,f1128]) ).
tff(f4004,plain,
( ~ mem(vertex,sF79,sF87)
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(superposition,[],[f952,f3904]) ).
tff(f4005,plain,
( ~ mem(vertex,sF79,sF63)
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(superposition,[],[f955,f3904]) ).
tff(f4023,plain,
( ~ mem(vertex,sF79,sF96)
| ~ spl115_5
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(forward_demodulation,[],[f4004,f2574]) ).
tff(f4028,plain,
( $false
| ~ spl115_5
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(forward_subsumption_resolution,[],[f4023,f2061]) ).
tff(f4029,plain,
( ~ spl115_5
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(avatar_contradiction_clause,[],[f4028]) ).
tff(f4213,plain,
( mem(vertex,sF99,sF96)
| ~ sort1(vertex,sF99)
| ~ spl115_65 ),
inference(resolution,[],[f2060,f2358]) ).
tff(f4218,plain,
( ~ sort1(vertex,sF99)
| ~ spl115_5
| ~ spl115_65 ),
inference(forward_subsumption_resolution,[],[f4213,f2578]) ).
tff(f4219,plain,
( $false
| ~ spl115_5
| ~ spl115_65 ),
inference(forward_subsumption_resolution,[],[f4218,f1128]) ).
tff(f4220,plain,
( ~ spl115_5
| ~ spl115_65 ),
inference(avatar_contradiction_clause,[],[f4219]) ).
tff(f4287,plain,
( ~ mem(vertex,sF79,sF87)
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(superposition,[],[f952,f3904]) ).
tff(f4306,plain,
( $false
| spl115_6
| ~ spl115_25
| ~ spl115_39
| ~ spl115_55 ),
inference(forward_subsumption_resolution,[],[f4287,f1258]) ).
tff(f4307,plain,
( spl115_6
| ~ spl115_25
| ~ spl115_39
| ~ spl115_55 ),
inference(avatar_contradiction_clause,[],[f4306]) ).
tff(f4313,plain,
( mem(vertex,sF79,sF61)
| ~ spl115_20
| ~ spl115_57 ),
inference(forward_demodulation,[],[f1224,f1818]) ).
tff(f4605,plain,
( mem(vertex,sF99,sF87)
| ~ spl115_4
| ~ spl115_65 ),
inference(forward_demodulation,[],[f2358,f1123]) ).
tff(f4640,plain,
( $false
| ~ spl115_4
| ~ spl115_65 ),
inference(forward_subsumption_resolution,[],[f4605,f952]) ).
tff(f4641,plain,
( ~ spl115_4
| ~ spl115_65 ),
inference(avatar_contradiction_clause,[],[f4640]) ).
tff(f4681,plain,
( ~ mem(vertex,sF79,sF61)
| spl115_6
| ~ spl115_39
| ~ spl115_55
| ~ spl115_57 ),
inference(forward_demodulation,[],[f4005,f1818]) ).
tff(f4694,plain,
( $false
| spl115_6
| ~ spl115_20
| ~ spl115_39
| ~ spl115_55
| ~ spl115_57 ),
inference(forward_subsumption_resolution,[],[f4681,f4313]) ).
tff(f4695,plain,
( spl115_6
| ~ spl115_20
| ~ spl115_39
| ~ spl115_55
| ~ spl115_57 ),
inference(avatar_contradiction_clause,[],[f4694]) ).
cnf(s3,plain,
( spl115_4
| spl115_5 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s4,plain,
( ~ spl115_6
| ~ spl115_7 ),
inference(sat_conversion,[],[f1105]) ).
cnf(s30,plain,
( spl115_5
| spl115_20
| spl115_25 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s31,plain,
( ~ spl115_54
| spl115_55 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s32,plain,
( ~ spl115_56
| spl115_57 ),
inference(sat_conversion,[],[f1819]) ).
cnf(s36,plain,
spl115_54,
inference(sat_conversion,[],[f2033]) ).
cnf(s43,plain,
spl115_56,
inference(sat_conversion,[],[f2279]) ).
cnf(s48,plain,
( ~ spl115_38
| spl115_39
| ~ spl115_57
| spl115_65 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s67,plain,
( ~ spl115_57
| spl115_65
| spl115_80 ),
inference(sat_conversion,[],[f2793]) ).
cnf(s74,plain,
( spl115_7
| ~ spl115_57
| ~ spl115_80 ),
inference(sat_conversion,[],[f3079]) ).
cnf(s77,plain,
( ~ spl115_7
| spl115_38 ),
inference(sat_conversion,[],[f3164]) ).
cnf(s85,plain,
( ~ spl115_5
| spl115_6
| ~ spl115_39
| ~ spl115_55 ),
inference(sat_conversion,[],[f4029]) ).
cnf(s91,plain,
( ~ spl115_5
| ~ spl115_65 ),
inference(sat_conversion,[],[f4220]) ).
cnf(s92,plain,
( spl115_6
| ~ spl115_25
| ~ spl115_39
| ~ spl115_55 ),
inference(sat_conversion,[],[f4307]) ).
cnf(s110,plain,
( ~ spl115_4
| ~ spl115_65 ),
inference(sat_conversion,[],[f4641]) ).
cnf(s120,plain,
( spl115_6
| ~ spl115_20
| ~ spl115_39
| ~ spl115_55
| ~ spl115_57 ),
inference(sat_conversion,[],[f4695]) ).
cnf(s121,plain,
spl115_57,
inference(rat,[],[s32,s43]) ).
cnf(s124,plain,
spl115_55,
inference(rat,[],[s31,s36]) ).
cnf(s126,plain,
( ~ spl115_39
| spl115_6 ),
inference(rat,[],[s30,s85,s92,s120,s121,s124]) ).
cnf(s127,plain,
spl115_65,
inference(rat,[],[s126,s48,s4,s77,s74,s67,s121]) ).
cnf(s128,plain,
~ spl115_4,
inference(rat,[],[s110,s127]) ).
cnf(s129,plain,
~ spl115_5,
inference(rat,[],[s91,s127]) ).
cnf(s132,plain,
$false,
inference(rat,[],[s3,s129,s128]) ).
tff(f4697,plain,
$false,
inference(avatar_sat_refutation,[],[s132]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW587_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.12 % Computer : n012.cluster.edu
% 0.00/0.12 % Model : x86_64 x86_64
% 0.00/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.12 % Memory : 8046.5625MB
% 0.00/0.12 % OS : Linux 6.8.0-71-generic
% 0.00/0.12 % CPULimit : 300
% 0.00/0.12 % WCLimit : 300
% 0.00/0.12 % DateTime : Mon Sep 28 14:19:49 UTC 2026
% 0.00/0.12 % CPUTime :
% 0.00/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.15 Running first-order theorem proving
% 0.09/0.15 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
% 2.94/0.92 % (3404392)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.94/0.92 % (3404418)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3852662052:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.94/0.92 % (3404419)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=444911695:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.94/0.92 % (3404419)Instruction limit reached!
% 2.94/0.92 % (3404419)------------------------------
% 2.94/0.92 % (3404419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/0.92 % (3404419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/0.92 % (3404419)CaDiCaL version: 2.1.3
% 2.94/0.92 % (3404419)Termination reason: Instruction limit
% 2.94/0.92 % (3404419)Termination phase: Preprocessing 3
% 2.94/0.92 % (3404419)Time elapsed: 0.003 s
% 2.94/0.92 % (3404419)Peak memory usage: 86 MB
% 2.94/0.92 % (3404419)Instructions burned: 8 (million)
% 2.94/0.92 % (3404416)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1632682897:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.94/0.92 % (3404417)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2858563025:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.94/0.92 % (3404421)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2369964362:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.94/0.92 % (3404422)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1969653941:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.94/0.92 % (3404421)Instruction limit reached!
% 2.94/0.92 % (3404421)------------------------------
% 2.94/0.92 % (3404421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/0.92 % (3404421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/0.92 % (3404421)CaDiCaL version: 2.1.3
% 2.94/0.92 % (3404421)Termination reason: Instruction limit
% 2.94/0.92 % (3404421)Termination phase: Naming
% 2.94/0.92 % (3404421)Time elapsed: 0.003 s
% 2.94/0.92 % (3404421)Peak memory usage: 86 MB
% 2.94/0.92 % (3404421)Instructions burned: 5 (million)
% 2.94/0.92 % (3404416)Instruction limit reached!
% 2.94/0.92 % (3404416)------------------------------
% 2.94/0.92 % (3404416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/0.92 % (3404416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/0.92 % (3404416)CaDiCaL version: 2.1.3
% 2.94/0.92 % (3404416)Termination reason: Instruction limit
% 2.94/0.92 % (3404416)Termination phase: Property scanning
% 2.94/0.92 % (3404416)Time elapsed: 0.007 s
% 2.94/0.92 % (3404416)Peak memory usage: 87 MB
% 2.94/0.92 % (3404416)Instructions burned: 13 (million)
% 2.94/0.92 % (3404423)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1406919962:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.94/0.92 % (3404422)Instruction limit reached!
% 2.94/0.92 % (3404422)------------------------------
% 2.94/0.92 % (3404422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/0.92 % (3404422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/0.92 % (3404422)CaDiCaL version: 2.1.3
% 2.94/0.92 % (3404422)Termination reason: Instruction limit
% 2.94/0.92 % (3404422)Termination phase: Saturation
% 2.94/0.92 % (3404422)Time elapsed: 0.043 s
% 2.94/0.92 % (3404422)Peak memory usage: 116 MB
% 2.94/0.92 % (3404422)Instructions burned: 46 (million)
% 2.94/0.92 % (3404423)Instruction limit reached!
% 2.94/0.92 % (3404423)------------------------------
% 2.94/0.92 % (3404423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/0.92 % (3404423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/0.92 % (3404423)CaDiCaL version: 2.1.3
% 2.94/0.92 % (3404423)Termination reason: Instruction limit
% 2.94/0.92 % (3404423)Termination phase: Saturation
% 2.94/0.92 % (3404423)Time elapsed: 0.035 s
% 2.94/0.92 % (3404423)Peak memory usage: 116 MB
% 2.94/0.92 % (3404423)Instructions burned: 33 (million)
% 2.94/0.92 % (3404418)Instruction limit reached!
% 2.94/0.92 % (3404418)------------------------------
% 2.94/0.92 % (3404418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/0.92 % (3404418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404418)CaDiCaL version: 2.1.3
% 4.44/1.06 % (3404418)Termination reason: Instruction limit
% 4.44/1.06 % (3404418)Termination phase: Saturation
% 4.44/1.06 % (3404418)Time elapsed: 0.117 s
% 4.44/1.06 % (3404418)Peak memory usage: 114 MB
% 4.44/1.06 % (3404418)Instructions burned: 201 (million)
% 4.44/1.06 % (3404433)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1922859561:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.44/1.06 % (3404433)Instruction limit reached!
% 4.44/1.06 % (3404433)------------------------------
% 4.44/1.06 % (3404433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.06 % (3404433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404433)CaDiCaL version: 2.1.3
% 4.44/1.06 % (3404433)Termination reason: Instruction limit
% 4.44/1.06 % (3404433)Termination phase: Saturation
% 4.44/1.06 % (3404433)Time elapsed: 0.007 s
% 4.44/1.06 % (3404433)Peak memory usage: 89 MB
% 4.44/1.06 % (3404433)Instructions burned: 16 (million)
% 4.44/1.06 % (3404439)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3387768808:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.44/1.06 % (3404438)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=1922189182:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.44/1.06 % (3404439)Instruction limit reached!
% 4.44/1.06 % (3404439)------------------------------
% 4.44/1.06 % (3404439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.06 % (3404439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404439)CaDiCaL version: 2.1.3
% 4.44/1.06 % (3404439)Termination reason: Instruction limit
% 4.44/1.06 % (3404439)Termination phase: Saturation
% 4.44/1.06 % (3404439)Time elapsed: 0.010 s
% 4.44/1.06 % (3404439)Peak memory usage: 88 MB
% 4.44/1.06 % (3404439)Instructions burned: 16 (million)
% 4.44/1.06 % (3404438)Instruction limit reached!
% 4.44/1.06 % (3404438)------------------------------
% 4.44/1.06 % (3404438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.06 % (3404438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404438)CaDiCaL version: 2.1.3
% 4.44/1.06 % (3404438)Termination reason: Instruction limit
% 4.44/1.06 % (3404438)Termination phase: Saturation
% 4.44/1.06 % (3404438)Time elapsed: 0.014 s
% 4.44/1.06 % (3404438)Peak memory usage: 88 MB
% 4.44/1.06 % (3404438)Instructions burned: 30 (million)
% 4.44/1.06 % (3404441)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=27796062:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 4.44/1.06 % (3404417)Instruction limit reached!
% 4.44/1.06 % (3404417)------------------------------
% 4.44/1.06 % (3404417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.06 % (3404417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404417)CaDiCaL version: 2.1.3
% 4.44/1.06 % (3404417)Termination reason: Instruction limit
% 4.44/1.06 % (3404417)Termination phase: Saturation
% 4.44/1.06 % (3404417)Time elapsed: 0.185 s
% 4.44/1.06 % (3404417)Peak memory usage: 118 MB
% 4.44/1.06 % (3404417)Instructions burned: 309 (million)
% 4.44/1.06 % (3404441)Instruction limit reached!
% 4.44/1.06 % (3404441)------------------------------
% 4.44/1.06 % (3404441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.06 % (3404441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404441)CaDiCaL version: 2.1.3
% 4.44/1.06 % (3404441)Termination reason: Instruction limit
% 4.44/1.06 % (3404441)Termination phase: Saturation
% 4.44/1.06 % (3404441)Time elapsed: 0.013 s
% 4.44/1.06 % (3404441)Peak memory usage: 89 MB
% 4.44/1.06 % (3404441)Instructions burned: 24 (million)
% 4.44/1.06 % (3404448)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1719949419:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 4.44/1.06 % (3404448)Instruction limit reached!
% 4.44/1.06 % (3404448)------------------------------
% 4.44/1.06 % (3404448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.44/1.06 % (3404448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.06 % (3404448)CaDiCaL version: 2.1.3
% 5.15/1.20 % (3404448)Termination reason: Instruction limit
% 5.15/1.20 % (3404448)Termination phase: Property scanning
% 5.15/1.20 % (3404448)Time elapsed: 0.002 s
% 5.15/1.20 % (3404448)Peak memory usage: 85 MB
% 5.15/1.20 % (3404448)Instructions burned: 3 (million)
% 5.15/1.20 % (3404443)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=3431924683:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 5.15/1.20 % (3404444)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3296654526:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 5.15/1.20 % (3404443)Instruction limit reached!
% 5.15/1.20 % (3404443)------------------------------
% 5.15/1.20 % (3404443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.20 % (3404443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.20 % (3404443)CaDiCaL version: 2.1.3
% 5.15/1.20 % (3404443)Termination reason: Instruction limit
% 5.15/1.20 % (3404443)Termination phase: Saturation
% 5.15/1.20 % (3404443)Time elapsed: 0.016 s
% 5.15/1.20 % (3404443)Peak memory usage: 90 MB
% 5.15/1.20 % (3404443)Instructions burned: 27 (million)
% 5.15/1.20 % (3404444)Instruction limit reached!
% 5.15/1.20 % (3404444)------------------------------
% 5.15/1.20 % (3404444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.20 % (3404444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.20 % (3404444)CaDiCaL version: 2.1.3
% 5.15/1.20 % (3404444)Termination reason: Instruction limit
% 5.15/1.20 % (3404444)Termination phase: Saturation
% 5.15/1.20 % (3404444)Time elapsed: 0.042 s
% 5.15/1.20 % (3404444)Peak memory usage: 89 MB
% 5.15/1.20 % (3404444)Instructions burned: 87 (million)
% 5.15/1.20 % (3404456)lrs+10_1_thi=all:si=on:fd=off:random_seed=2533085077:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.15/1.20 % (3404452)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1970340035:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 5.15/1.20 % (3404453)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=346228279:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.15/1.20 % (3404453)Instruction limit reached!
% 5.15/1.20 % (3404453)------------------------------
% 5.15/1.20 % (3404453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.20 % (3404453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.20 % (3404453)CaDiCaL version: 2.1.3
% 5.15/1.20 % (3404453)Termination reason: Instruction limit
% 5.15/1.20 % (3404453)Termination phase: Preprocessing 2
% 5.15/1.20 % (3404453)Time elapsed: 0.003 s
% 5.15/1.20 % (3404453)Peak memory usage: 86 MB
% 5.15/1.20 % (3404453)Instructions burned: 5 (million)
% 5.15/1.20 % (3404455)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3231930256:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.15/1.20 % (3404456)Instruction limit reached!
% 5.15/1.20 % (3404456)------------------------------
% 5.15/1.20 % (3404456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.20 % (3404456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.20 % (3404456)CaDiCaL version: 2.1.3
% 5.15/1.20 % (3404456)Termination reason: Instruction limit
% 5.15/1.20 % (3404456)Termination phase: Saturation
% 5.15/1.20 % (3404456)Time elapsed: 0.031 s
% 5.15/1.20 % (3404456)Peak memory usage: 116 MB
% 5.15/1.20 % (3404456)Instructions burned: 57 (million)
% 5.15/1.20 % (3404459)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=3356869141:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.15/1.20 % (3404459)Instruction limit reached!
% 5.15/1.20 % (3404459)------------------------------
% 5.15/1.20 % (3404459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.20 % (3404459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.20 % (3404459)CaDiCaL version: 2.1.3
% 5.15/1.20 % (3404459)Termination reason: Instruction limit
% 5.15/1.20 % (3404459)Termination phase: Preprocessing 3
% 5.15/1.20 % (3404459)Time elapsed: 0.005 s
% 5.15/1.20 % (3404459)Peak memory usage: 86 MB
% 5.15/1.20 % (3404459)Instructions burned: 9 (million)
% 5.15/1.20 % (3404462)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=282917137:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 6.28/1.40 % (3404462)Instruction limit reached!
% 6.28/1.40 % (3404462)------------------------------
% 6.28/1.40 % (3404462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/1.40 % (3404462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/1.40 % (3404462)CaDiCaL version: 2.1.3
% 6.28/1.40 % (3404462)Termination reason: Instruction limit
% 6.28/1.40 % (3404462)Termination phase: SInE selection
% 6.28/1.40 % (3404462)Time elapsed: 0.001 s
% 6.28/1.40 % (3404462)Peak memory usage: 85 MB
% 6.28/1.40 % (3404462)Instructions burned: 2 (million)
% 6.28/1.40 % (3404455)Instruction limit reached!
% 6.28/1.40 % (3404455)------------------------------
% 6.28/1.40 % (3404455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/1.40 % (3404455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/1.40 % (3404455)CaDiCaL version: 2.1.3
% 6.28/1.40 % (3404455)Termination reason: Instruction limit
% 6.28/1.40 % (3404455)Termination phase: Saturation
% 6.28/1.40 % (3404455)Time elapsed: 0.068 s
% 6.28/1.40 % (3404455)Peak memory usage: 134 MB
% 6.28/1.40 % (3404455)Instructions burned: 67 (million)
% 6.28/1.40 % (3404464)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1714390110:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.28/1.40 % (3404464)Instruction limit reached!
% 6.28/1.40 % (3404464)------------------------------
% 6.28/1.40 % (3404464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/1.40 % (3404464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/1.40 % (3404464)CaDiCaL version: 2.1.3
% 6.28/1.40 % (3404464)Termination reason: Instruction limit
% 6.28/1.40 % (3404464)Termination phase: Preprocessing 1
% 6.28/1.40 % (3404464)Time elapsed: 0.002 s
% 6.28/1.40 % (3404464)Peak memory usage: 86 MB
% 6.28/1.40 % (3404464)Instructions burned: 4 (million)
% 6.28/1.40 % (3404452)Instruction limit reached!
% 6.28/1.40 % (3404452)------------------------------
% 6.28/1.40 % (3404452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/1.40 % (3404452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/1.40 % (3404452)CaDiCaL version: 2.1.3
% 6.28/1.40 % (3404452)Termination reason: Instruction limit
% 6.28/1.40 % (3404452)Termination phase: Saturation
% 6.28/1.40 % (3404452)Time elapsed: 0.115 s
% 6.28/1.40 % (3404452)Peak memory usage: 92 MB
% 6.28/1.40 % (3404452)Instructions burned: 181 (million)
% 6.28/1.40 % (3404468)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3263254935:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 6.28/1.40 % (3404470)dis+10_1_si=on:random_seed=1094532500:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 6.28/1.40 % (3404470)Instruction limit reached!
% 6.28/1.40 % (3404470)------------------------------
% 6.28/1.40 % (3404470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/1.40 % (3404470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/1.40 % (3404470)CaDiCaL version: 2.1.3
% 6.28/1.40 % (3404470)Termination reason: Instruction limit
% 6.28/1.40 % (3404470)Termination phase: Property scanning
% 6.28/1.40 % (3404470)Time elapsed: 0.006 s
% 6.28/1.40 % (3404470)Peak memory usage: 86 MB
% 6.28/1.40 % (3404470)Instructions burned: 12 (million)
% 6.28/1.40 % (3404472)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2924601765:i=26:canc=cautious:av=off:rtra=on_2995 on theBenchmark for (2995ds/26Mi)
% 6.28/1.40 % (3404472)Instruction limit reached!
% 6.28/1.40 % (3404472)------------------------------
% 6.28/1.40 % (3404472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.28/1.40 % (3404472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.28/1.40 % (3404472)CaDiCaL version: 2.1.3
% 6.28/1.40 % (3404472)Termination reason: Instruction limit
% 6.28/1.40 % (3404472)Termination phase: Saturation
% 6.28/1.40 % (3404472)Time elapsed: 0.015 s
% 6.28/1.40 % (3404472)Peak memory usage: 89 MB
% 6.28/1.40 % (3404472)Instructions burned: 27 (million)
% 6.28/1.40 % (3404474)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2889857972: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_2994 on theBenchmark for (2994ds/35Mi)
% 7.20/1.62 % (3404475)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=881112540:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 7.20/1.62 % (3404475)Instruction limit reached!
% 7.20/1.62 % (3404475)------------------------------
% 7.20/1.62 % (3404475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404475)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404475)Termination reason: Instruction limit
% 7.20/1.62 % (3404475)Termination phase: Preprocessing 1
% 7.20/1.62 % (3404475)Time elapsed: 0.002 s
% 7.20/1.62 % (3404475)Peak memory usage: 85 MB
% 7.20/1.62 % (3404475)Instructions burned: 4 (million)
% 7.20/1.62 % (3404468)Instruction limit reached!
% 7.20/1.62 % (3404468)------------------------------
% 7.20/1.62 % (3404468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404468)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404468)Termination reason: Instruction limit
% 7.20/1.62 % (3404468)Termination phase: Saturation
% 7.20/1.62 % (3404468)Time elapsed: 0.092 s
% 7.20/1.62 % (3404468)Peak memory usage: 117 MB
% 7.20/1.62 % (3404468)Instructions burned: 128 (million)
% 7.20/1.62 % (3404474)Instruction limit reached!
% 7.20/1.62 % (3404474)------------------------------
% 7.20/1.62 % (3404474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404474)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404474)Termination reason: Instruction limit
% 7.20/1.62 % (3404474)Termination phase: Saturation
% 7.20/1.62 % (3404474)Time elapsed: 0.020 s
% 7.20/1.62 % (3404474)Peak memory usage: 89 MB
% 7.20/1.62 % (3404474)Instructions burned: 37 (million)
% 7.20/1.62 % (3404477)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=320580686:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 7.20/1.62 % (3404477)Instruction limit reached!
% 7.20/1.62 % (3404477)------------------------------
% 7.20/1.62 % (3404477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404477)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404477)Termination reason: Instruction limit
% 7.20/1.62 % (3404477)Termination phase: Property scanning
% 7.20/1.62 % (3404477)Time elapsed: 0.005 s
% 7.20/1.62 % (3404477)Peak memory usage: 86 MB
% 7.20/1.62 % (3404477)Instructions burned: 9 (million)
% 7.20/1.62 % (3404478)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3814855378:i=370:ep=RS:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/370Mi)
% 7.20/1.62 % (3404481)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4213754648:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2994 on theBenchmark for (2994ds/13Mi)
% 7.20/1.62 % (3404481)Instruction limit reached!
% 7.20/1.62 % (3404481)------------------------------
% 7.20/1.62 % (3404481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404481)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404481)Termination reason: Instruction limit
% 7.20/1.62 % (3404481)Termination phase: Property scanning
% 7.20/1.62 % (3404481)Time elapsed: 0.007 s
% 7.20/1.62 % (3404481)Peak memory usage: 87 MB
% 7.20/1.62 % (3404481)Instructions burned: 14 (million)
% 7.20/1.62 % (3404485)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3869342432:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 7.20/1.62 % (3404486)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4168713482:i=10:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 7.20/1.62 % (3404487)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2896697193:i=71:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/71Mi)
% 7.20/1.62 % (3404486)Instruction limit reached!
% 7.20/1.62 % (3404486)------------------------------
% 7.20/1.62 % (3404486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404486)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404486)Termination reason: Instruction limit
% 7.20/1.62 % (3404486)Termination phase: Saturation
% 7.20/1.62 % (3404486)Time elapsed: 0.006 s
% 7.20/1.62 % (3404486)Peak memory usage: 87 MB
% 7.20/1.62 % (3404486)Instructions burned: 11 (million)
% 7.20/1.62 % (3404488)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=1934708557:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2993 on theBenchmark for (2993ds/75Mi)
% 7.20/1.62 % (3404491)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=3484250047:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2993 on theBenchmark for (2993ds/294Mi)
% 7.20/1.62 % (3404487)Instruction limit reached!
% 7.20/1.62 % (3404487)------------------------------
% 7.20/1.62 % (3404487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404487)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404487)Termination reason: Instruction limit
% 7.20/1.62 % (3404487)Termination phase: Saturation
% 7.20/1.62 % (3404487)Time elapsed: 0.063 s
% 7.20/1.62 % (3404487)Peak memory usage: 133 MB
% 7.20/1.62 % (3404487)Instructions burned: 73 (million)
% 7.20/1.62 % (3404488)Instruction limit reached!
% 7.20/1.62 % (3404488)------------------------------
% 7.20/1.62 % (3404488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404488)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404488)Termination reason: Instruction limit
% 7.20/1.62 % (3404488)Termination phase: Saturation
% 7.20/1.62 % (3404488)Time elapsed: 0.034 s
% 7.20/1.62 % (3404488)Peak memory usage: 90 MB
% 7.20/1.62 % (3404488)Instructions burned: 75 (million)
% 7.20/1.62 % (3404495)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=209727409:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2992 on theBenchmark for (2992ds/130Mi)
% 7.20/1.62 % (3404478)Instruction limit reached!
% 7.20/1.62 % (3404478)------------------------------
% 7.20/1.62 % (3404478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404478)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404478)Termination reason: Instruction limit
% 7.20/1.62 % (3404478)Termination phase: Saturation
% 7.20/1.62 % (3404478)Time elapsed: 0.194 s
% 7.20/1.62 % (3404478)Peak memory usage: 93 MB
% 7.20/1.62 % (3404478)Instructions burned: 372 (million)
% 7.20/1.62 % (3404485)Instruction limit reached!
% 7.20/1.62 % (3404485)------------------------------
% 7.20/1.62 % (3404485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404485)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404485)Termination reason: Instruction limit
% 7.20/1.62 % (3404485)Termination phase: Saturation
% 7.20/1.62 % (3404485)Time elapsed: 0.140 s
% 7.20/1.62 % (3404485)Peak memory usage: 117 MB
% 7.20/1.62 % (3404485)Instructions burned: 228 (million)
% 7.20/1.62 % (3404499)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=314552683:i=131:rtra=on_2992 on theBenchmark for (2992ds/131Mi)
% 7.20/1.62 % (3404503)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1532329928:i=307:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/307Mi)
% 7.20/1.62 % (3404491)First to succeed.
% 7.20/1.62 % (3404491)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3404392"
% 7.20/1.62 % (3404495)Instruction limit reached!
% 7.20/1.62 % (3404495)------------------------------
% 7.20/1.62 % (3404495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404495)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404495)Termination reason: Instruction limit
% 7.20/1.62 % (3404495)Termination phase: Saturation
% 7.20/1.62 % (3404495)Time elapsed: 0.080 s
% 7.20/1.62 % (3404495)Peak memory usage: 117 MB
% 7.20/1.62 % (3404495)Instructions burned: 130 (million)
% 7.20/1.62 % (3404502)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1540873474:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2991 on theBenchmark for (2991ds/40Mi)
% 7.20/1.62 % (3404505)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2844824294:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/598Mi)
% 7.20/1.62 % (3404499)Instruction limit reached!
% 7.20/1.62 % (3404499)------------------------------
% 7.20/1.62 % (3404499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404499)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404499)Termination reason: Instruction limit
% 7.20/1.62 % (3404499)Termination phase: Saturation
% 7.20/1.62 % (3404499)Time elapsed: 0.108 s
% 7.20/1.62 % (3404499)Peak memory usage: 134 MB
% 7.20/1.62 % (3404499)Instructions burned: 131 (million)
% 7.20/1.62 % (3404502)Instruction limit reached!
% 7.20/1.62 % (3404502)------------------------------
% 7.20/1.62 % (3404502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404502)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404502)Termination reason: Instruction limit
% 7.20/1.62 % (3404502)Termination phase: Saturation
% 7.20/1.62 % (3404502)Time elapsed: 0.055 s
% 7.20/1.62 % (3404502)Peak memory usage: 134 MB
% 7.20/1.62 % (3404502)Instructions burned: 41 (million)
% 7.20/1.62 % (3404503)Instruction limit reached!
% 7.20/1.62 % (3404503)------------------------------
% 7.20/1.62 % (3404503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404503)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404503)Termination reason: Instruction limit
% 7.20/1.62 % (3404503)Termination phase: Saturation
% 7.20/1.62 % (3404503)Time elapsed: 0.111 s
% 7.20/1.62 % (3404503)Peak memory usage: 93 MB
% 7.20/1.62 % (3404503)Instructions burned: 309 (million)
% 7.20/1.62 % (3404506)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1263974643:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 7.20/1.62 % (3404509)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3368396563:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2990 on theBenchmark for (2990ds/259Mi)
% 7.20/1.62 % (3404514)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1059677503:i=141:doe=on:rtra=on_2989 on theBenchmark for (2989ds/141Mi)
% 7.20/1.62 % (3404506)Instruction limit reached!
% 7.20/1.62 % (3404506)------------------------------
% 7.20/1.62 % (3404506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404506)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404506)Termination reason: Instruction limit
% 7.20/1.62 % (3404506)Termination phase: Saturation
% 7.20/1.62 % (3404506)Time elapsed: 0.083 s
% 7.20/1.62 % (3404506)Peak memory usage: 117 MB
% 7.20/1.62 % (3404506)Instructions burned: 133 (million)
% 7.20/1.62 % (3404514)Instruction limit reached!
% 7.20/1.62 % (3404514)------------------------------
% 7.20/1.62 % (3404514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.62 % (3404514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.62 % (3404514)CaDiCaL version: 2.1.3
% 7.20/1.62 % (3404514)Termination reason: Instruction limit
% 7.20/1.62 % (3404514)Termination phase: Saturation
% 7.20/1.62 % (3404514)Time elapsed: 0.040 s
% 7.20/1.62 % (3404514)Peak memory usage: 89 MB
% 7.20/1.62 % (3404514)Instructions burned: 143 (million)
% 7.20/1.62 % (3404491)Refutation found. Thanks to Tanya!
% 7.20/1.62 % SZS status Theorem for theBenchmark
% 7.20/1.62 % SZS output start Proof for theBenchmark
% See solution above
% 8.79/1.75 % (3404491)------------------------------
% 8.79/1.75 % (3404491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/1.75 % (3404491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/1.75 % (3404491)CaDiCaL version: 2.1.3
% 8.79/1.75 % (3404491)Termination reason: Refutation
% 8.79/1.75 % (3404491)Time elapsed: 0.134 s
% 8.79/1.75 % (3404491)Peak memory usage: 92 MB
% 8.79/1.75 % (3404491)Instructions burned: 232 (million)
% 8.79/1.75 % (3404491)------------------------------
% 8.79/1.75 % (3404491)------------------------------
% 8.79/1.75 % (3404392)Success in time 1.211 s
% 8.79/1.75 % Vampire exiting
%------------------------------------------------------------------------------