%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW577_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 : n001.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:50 PM UTC 2026
% Result : Theorem 19.41s 3.73s
% Output : Refutation 22.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 24
% Syntax : Number of formulae : 146 ( 27 unt; 0 typ; 17 def)
% Number of atoms : 1384 ( 278 equ)
% Maximal formula atoms : 95 ( 9 avg)
% Number of connectives : 1856 ( 618 ~; 574 |; 422 &)
% ( 29 <=>; 213 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 638 ( 340 atm; 140 fun; 100 num; 58 var)
% Number of types : 13 ( 11 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 37 ( 33 usr; 18 prp; 0-3 aty)
% Number of functors : 174 ( 170 usr; 37 con; 0-5 aty)
% Number of variables : 631 ( 481 !; 150 ?; 631 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
vertex: $tType ).
tff(type_def_10,type,
t: $tType ).
tff(type_def_11,type,
map_vertex_t19: $tType ).
tff(type_def_12,type,
list_vertex: $tType ).
tff(type_def_13,type,
set_vertex: $tType ).
tff(type_def_14,type,
set_lpvertexcm_vertexrp: $tType ).
tff(type_def_15,type,
lpvertexcm_vertexrp: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_10,type,
map: ( ty * ty ) > ty ).
tff(func_def_11,type,
vertex1: ty ).
tff(func_def_12,type,
t1: ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
get1: ( map_vertex_t19 * vertex ) > t ).
tff(func_def_15,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
t2tb: vertex > uni ).
tff(func_def_17,type,
tb2t: uni > vertex ).
tff(func_def_18,type,
t2tb1: map_vertex_t19 > uni ).
tff(func_def_19,type,
tb2t1: uni > map_vertex_t19 ).
tff(func_def_20,type,
t2tb2: t > uni ).
tff(func_def_21,type,
tb2t2: uni > t ).
tff(func_def_22,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_25,type,
list: ty > ty ).
tff(func_def_26,type,
nil: ty > uni ).
tff(func_def_27,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_28,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_29,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(func_def_30,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(func_def_31,type,
length: ( ty * uni ) > $int ).
tff(func_def_32,type,
length1: list_vertex > $int ).
tff(func_def_33,type,
t2tb3: list_vertex > uni ).
tff(func_def_34,type,
tb2t3: uni > list_vertex ).
tff(func_def_37,type,
set1: ty > ty ).
tff(func_def_38,type,
tuple2: ( ty * ty ) > ty ).
tff(func_def_39,type,
t2tb4: set_lpvertexcm_vertexrp > uni ).
tff(func_def_40,type,
tb2t4: uni > set_lpvertexcm_vertexrp ).
tff(func_def_41,type,
t2tb5: set_vertex > uni ).
tff(func_def_42,type,
tb2t5: uni > set_vertex ).
tff(func_def_43,type,
empty: ty > uni ).
tff(func_def_44,type,
empty1: set_vertex ).
tff(func_def_45,type,
empty2: set_lpvertexcm_vertexrp ).
tff(func_def_46,type,
add: ( ty * uni * uni ) > uni ).
tff(func_def_47,type,
add1: ( vertex * set_vertex ) > set_vertex ).
tff(func_def_48,type,
add2: ( lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > set_lpvertexcm_vertexrp ).
tff(func_def_49,type,
remove: ( ty * uni * uni ) > uni ).
tff(func_def_50,type,
remove1: ( vertex * set_vertex ) > set_vertex ).
tff(func_def_51,type,
remove2: ( lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > set_lpvertexcm_vertexrp ).
tff(func_def_52,type,
union: ( ty * uni * uni ) > uni ).
tff(func_def_53,type,
inter: ( ty * uni * uni ) > uni ).
tff(func_def_54,type,
diff: ( ty * uni * uni ) > uni ).
tff(func_def_55,type,
diff1: ( set_vertex * set_vertex ) > set_vertex ).
tff(func_def_56,type,
diff2: ( set_lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > set_lpvertexcm_vertexrp ).
tff(func_def_57,type,
choose: ( ty * uni ) > uni ).
tff(func_def_58,type,
t2tb6: lpvertexcm_vertexrp > uni ).
tff(func_def_59,type,
tb2t6: uni > lpvertexcm_vertexrp ).
tff(func_def_60,type,
cardinal: ( ty * uni ) > $int ).
tff(func_def_61,type,
cardinal1: set_vertex > $int ).
tff(func_def_62,type,
cardinal2: set_lpvertexcm_vertexrp > $int ).
tff(func_def_63,type,
vertices: set_vertex ).
tff(func_def_64,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(func_def_65,type,
tuple22: ( vertex * vertex ) > lpvertexcm_vertexrp ).
tff(func_def_66,type,
tuple2_proj_1: ( ty * ty * uni ) > uni ).
tff(func_def_67,type,
tuple2_proj_2: ( ty * ty * uni ) > uni ).
tff(func_def_68,type,
edges: set_lpvertexcm_vertexrp ).
tff(func_def_69,type,
s: vertex ).
tff(func_def_70,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_71,type,
weight: ( vertex * vertex ) > $int ).
tff(func_def_72,type,
path_weight: ( list_vertex * vertex ) > $int ).
tff(func_def_73,type,
finite: $int > t ).
tff(func_def_74,type,
infinite: t ).
tff(func_def_75,type,
match_t: ( ty * t * uni * uni ) > uni ).
tff(func_def_76,type,
finite_proj_1: t > $int ).
tff(func_def_77,type,
add3: ( t * t ) > t ).
tff(func_def_78,type,
ref: ty > ty ).
tff(func_def_79,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_80,type,
contents: ( ty * uni ) > uni ).
tff(func_def_83,type,
sK0: ( set_lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > lpvertexcm_vertexrp ).
tff(func_def_84,type,
sK1: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_85,type,
sK2: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_86,type,
sK3: ( vertex * list_vertex * vertex ) > list_vertex ).
tff(func_def_87,type,
sK4: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_88,type,
sK5: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_89,type,
sK6: ( ty * uni * uni ) > uni ).
tff(func_def_90,type,
sK7: ( vertex * list_vertex ) > list_vertex ).
tff(func_def_91,type,
sK8: ( vertex * list_vertex ) > list_vertex ).
tff(func_def_92,type,
sK9: list_vertex > list_vertex ).
tff(func_def_93,type,
sK10: list_vertex > list_vertex ).
tff(func_def_94,type,
sK11: list_vertex > vertex ).
tff(func_def_95,type,
sK12: list_vertex > list_vertex ).
tff(func_def_96,type,
sK13: vertex > list_vertex ).
tff(func_def_97,type,
sK14: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_98,type,
sK15: ( list_vertex * vertex ) > vertex ).
tff(func_def_99,type,
sK16: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_100,type,
sK17: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_101,type,
sK18: ( list_vertex * vertex ) > vertex ).
tff(func_def_102,type,
sK19: map_vertex_t19 ).
tff(func_def_103,type,
sK20: $int ).
tff(func_def_104,type,
sK21: vertex > $int ).
tff(func_def_105,type,
sK22: vertex > list_vertex ).
tff(func_def_106,type,
sK23: set_lpvertexcm_vertexrp ).
tff(func_def_107,type,
sK24: map_vertex_t19 ).
tff(func_def_108,type,
sK25: set_lpvertexcm_vertexrp ).
tff(func_def_109,type,
sK26: bool ).
tff(func_def_110,type,
sK27: vertex ).
tff(func_def_111,type,
sK28: vertex ).
tff(func_def_112,type,
sK29: set_lpvertexcm_vertexrp ).
tff(func_def_113,type,
sK30: vertex > $int ).
tff(func_def_114,type,
sK31: vertex > list_vertex ).
tff(func_def_115,type,
sK32: map_vertex_t19 ).
tff(func_def_116,type,
sK33: vertex > $int ).
tff(func_def_117,type,
sK34: vertex > list_vertex ).
tff(func_def_118,type,
sK35: vertex ).
tff(func_def_119,type,
sK36: $int ).
tff(func_def_120,type,
sK37: list_vertex ).
tff(func_def_121,type,
sK38: vertex ).
tff(func_def_122,type,
sK39: lpvertexcm_vertexrp ).
tff(func_def_123,type,
sK40: lpvertexcm_vertexrp ).
tff(func_def_124,type,
sK41: vertex > $int ).
tff(func_def_125,type,
sK42: vertex > list_vertex ).
tff(func_def_126,type,
sK43: ( ty * uni * uni ) > uni ).
tff(func_def_127,type,
sK44: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_128,type,
sK45: ( vertex * list_vertex * vertex ) > list_vertex ).
tff(func_def_129,type,
sK46: set_vertex ).
tff(func_def_130,type,
sK47: set_vertex ).
tff(func_def_131,type,
sK48: vertex ).
tff(func_def_132,type,
sK49: ( list_vertex * set_vertex ) > vertex ).
tff(func_def_133,type,
sK50: list_vertex > list_vertex ).
tff(func_def_134,type,
sK51: list_vertex > list_vertex ).
tff(func_def_135,type,
sK52: list_vertex > vertex ).
tff(func_def_136,type,
sK53: list_vertex > list_vertex ).
tff(func_def_137,type,
sK54: set_vertex > vertex ).
tff(func_def_138,type,
sK55: ( set_vertex * set_vertex ) > vertex ).
tff(func_def_139,type,
sK56: ( set_lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > lpvertexcm_vertexrp ).
tff(func_def_140,type,
sK57: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_141,type,
sK58: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp * $int ) > vertex ).
tff(func_def_142,type,
sK59: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp * $int ) > list_vertex ).
tff(func_def_143,type,
sK60: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp * $int ) > list_vertex ).
tff(func_def_144,type,
sK61: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_145,type,
sK62: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > list_vertex ).
tff(func_def_146,type,
sK63: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > list_vertex ).
tff(func_def_147,type,
sK64: ( vertex * $int ) > list_vertex ).
tff(func_def_148,type,
sK65: ( map_vertex_t19 * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_149,type,
sK66: ( map_vertex_t19 * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_150,type,
sK67: ( set_vertex * set_vertex ) > vertex ).
tff(func_def_151,type,
sK68: ( list_vertex * set_vertex ) > vertex ).
tff(func_def_152,type,
sK69: list_vertex > list_vertex ).
tff(func_def_153,type,
sK70: list_vertex > list_vertex ).
tff(func_def_154,type,
sK71: list_vertex > vertex ).
tff(func_def_155,type,
sK72: list_vertex > list_vertex ).
tff(func_def_156,type,
sK73: set_vertex > list_vertex ).
tff(func_def_157,type,
sK74: list_vertex > vertex ).
tff(func_def_158,type,
sK75: list_vertex > list_vertex ).
tff(func_def_159,type,
sK76: list_vertex > list_vertex ).
tff(func_def_160,type,
sK77: list_vertex > list_vertex ).
tff(func_def_161,type,
sK78: ( set_vertex * list_vertex ) > vertex ).
tff(func_def_162,type,
sK79: vertex ).
tff(func_def_163,type,
sK80: ( $int * vertex ) > list_vertex ).
tff(func_def_164,type,
sK81: set_lpvertexcm_vertexrp > lpvertexcm_vertexrp ).
tff(func_def_165,type,
sK82: ( ty * uni * uni ) > uni ).
tff(func_def_166,type,
sK83: ( ty * uni * uni ) > uni ).
tff(func_def_167,type,
sK84: vertex > list_vertex ).
tff(func_def_168,type,
sK85: vertex > list_vertex ).
tff(func_def_169,type,
sK86: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_170,type,
sK87: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_171,type,
sK88: list_vertex > vertex ).
tff(func_def_172,type,
sK89: list_vertex > list_vertex ).
tff(func_def_173,type,
sK90: list_vertex > list_vertex ).
tff(func_def_174,type,
sK91: list_vertex > list_vertex ).
tff(func_def_175,type,
sK92: ( ty * uni ) > uni ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
mem1: ( vertex * set_vertex ) > $o ).
tff(pred_def_5,type,
mem2: ( lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > $o ).
tff(pred_def_6,type,
infix_eqeq: ( ty * uni * uni ) > $o ).
tff(pred_def_7,type,
subset: ( ty * uni * uni ) > $o ).
tff(pred_def_8,type,
is_empty: ( ty * uni ) > $o ).
tff(pred_def_9,type,
edge: ( vertex * vertex ) > $o ).
tff(pred_def_11,type,
mem3: ( ty * uni * uni ) > $o ).
tff(pred_def_12,type,
path: ( vertex * list_vertex * vertex ) > $o ).
tff(pred_def_13,type,
pigeon_set: set_vertex > $o ).
tff(pred_def_14,type,
negative_cycle: vertex > $o ).
tff(pred_def_15,type,
lt: ( t * t ) > $o ).
tff(pred_def_16,type,
le: ( t * t ) > $o ).
tff(pred_def_17,type,
inv1: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > $o ).
tff(pred_def_18,type,
inv2: ( map_vertex_t19 * set_lpvertexcm_vertexrp ) > $o ).
tff(f73,axiom,
! [X1: lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp] :
( ( mem2(X0,X2)
| ( X0 = X1 ) )
<=> mem2(X0,add2(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_def1) ).
tff(f77,axiom,
! [X1: lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp] :
( mem2(X0,remove2(X1,X2))
<=> ( ( X0 != X1 )
& mem2(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',remove_def1) ).
tff(f80,axiom,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X0,X1)
=> ( add2(X0,remove2(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_remove) ).
tff(f98,axiom,
! [X1: set_lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X2: lpvertexcm_vertexrp] :
( mem2(X2,diff2(X0,X1))
<=> ( mem2(X2,X0)
& ~ mem2(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',diff_def1) ).
tff(f180,axiom,
! [X0: $int] : ( finite(X0) != infinite ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_Infinite) ).
tff(f181,axiom,
! [X0: $int] : ( finite_proj_1(finite(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',finite_proj_1_def) ).
tff(f197,conjecture,
( ( $less(1,$difference(cardinal1(vertices),1))
| ( 1 = $difference(cardinal1(vertices),1) ) )
=> ! [X1: $int,X0: map_vertex_t19] :
( ( ( $less(X1,$difference(cardinal1(vertices),1))
| ( X1 = $difference(cardinal1(vertices),1) ) )
& ( $less(1,X1)
| ( 1 = X1 ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ( get1(X0,X2) = infinite )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),empty2)
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) ) )
| ? [X3: $int] :
( ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ! [X4: list_vertex,X5: vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),empty2)
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) )
& ( get1(X0,X2) = finite(X3) ) ) ) )
=> ! [X7: set_lpvertexcm_vertexrp] :
( ( X7 = edges )
=> ! [X9: map_vertex_t19,X8: set_lpvertexcm_vertexrp] :
( ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ( get1(X9,X2) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) ) )
| ? [X3: $int] :
( ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ( get1(X9,X2) = finite(X3) )
& ? [X4: list_vertex] :
( ( path_weight(X4,X2) = X3 )
& path(s,X4,X2) )
& ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X8))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) ) ) ) )
& ! [X3: lpvertexcm_vertexrp] :
( mem2(X3,X8)
=> mem2(X3,edges) ) )
=> ! [X10: bool] :
( ( ( X10 = true )
<=> ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8) )
=> ( ( X10 != true )
=> ( ~ ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8)
=> ! [X12: vertex,X11: set_lpvertexcm_vertexrp,X13: vertex] :
( ( ( X11 = remove2(tuple22(X12,X13),X8) )
& mem2(tuple22(X12,X13),X8) )
=> ( ( ( ( 1 = X1 )
| $less(1,X1) )
& mem2(tuple22(X12,X13),edges)
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X8))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) )
& ( get1(X9,X2) = finite(X3) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) ) )
| ( ! [X5: vertex] :
( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ( get1(X9,X2) = infinite ) ) ) )
& ~ mem2(tuple22(X12,X13),diff2(edges,X8)) )
=> ! [X14: map_vertex_t19] :
( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
& ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),add2(tuple22(X12,X13),diff2(edges,X8)))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ? [X4: list_vertex] :
( ( path_weight(X4,X2) = X3 )
& path(s,X4,X2) ) )
| ( ( get1(X14,X2) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),add2(tuple22(X12,X13),diff2(edges,X8)))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) ) ) ) )
=> ! [X2: vertex] :
( mem1(X2,vertices)
=> ! [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
=> ! [X4: list_vertex,X5: vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X11))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_bellman_ford) ).
tff(f198,negated_conjecture,
~ ( ( $less(1,$difference(cardinal1(vertices),1))
| ( 1 = $difference(cardinal1(vertices),1) ) )
=> ! [X1: $int,X0: map_vertex_t19] :
( ( ( $less(X1,$difference(cardinal1(vertices),1))
| ( X1 = $difference(cardinal1(vertices),1) ) )
& ( $less(1,X1)
| ( 1 = X1 ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ( get1(X0,X2) = infinite )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),empty2)
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) ) )
| ? [X3: $int] :
( ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ! [X4: list_vertex,X5: vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),empty2)
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) )
& ( get1(X0,X2) = finite(X3) ) ) ) )
=> ! [X7: set_lpvertexcm_vertexrp] :
( ( X7 = edges )
=> ! [X9: map_vertex_t19,X8: set_lpvertexcm_vertexrp] :
( ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ( get1(X9,X2) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) ) )
| ? [X3: $int] :
( ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ( get1(X9,X2) = finite(X3) )
& ? [X4: list_vertex] :
( ( path_weight(X4,X2) = X3 )
& path(s,X4,X2) )
& ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X8))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) ) ) ) )
& ! [X3: lpvertexcm_vertexrp] :
( mem2(X3,X8)
=> mem2(X3,edges) ) )
=> ! [X10: bool] :
( ( ( X10 = true )
<=> ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8) )
=> ( ( X10 != true )
=> ( ~ ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8)
=> ! [X12: vertex,X11: set_lpvertexcm_vertexrp,X13: vertex] :
( ( ( X11 = remove2(tuple22(X12,X13),X8) )
& mem2(tuple22(X12,X13),X8) )
=> ( ( ( ( 1 = X1 )
| $less(1,X1) )
& mem2(tuple22(X12,X13),edges)
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X8))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) )
& ( get1(X9,X2) = finite(X3) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) ) )
| ( ! [X5: vertex] :
( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ( get1(X9,X2) = infinite ) ) ) )
& ~ mem2(tuple22(X12,X13),diff2(edges,X8)) )
=> ! [X14: map_vertex_t19] :
( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
& ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),add2(tuple22(X12,X13),diff2(edges,X8)))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> $lesseq(X3,path_weight(X4,X2)) ) )
& ? [X4: list_vertex] :
( ( path_weight(X4,X2) = X3 )
& path(s,X4,X2) ) )
| ( ( get1(X14,X2) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),add2(tuple22(X12,X13),diff2(edges,X8)))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) ) ) ) )
=> ! [X2: vertex] :
( mem1(X2,vertices)
=> ! [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
=> ! [X4: list_vertex,X5: vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X11))
=> $lesseq(X3,$sum(path_weight(X4,X5),weight(X5,X2))) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f197]) ).
tff(f209,plain,
~ ( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
=> ! [X1: $int,X0: map_vertex_t19] :
( ( ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) )
& ( $less(1,X1)
| ( 1 = X1 ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ( get1(X0,X2) = infinite )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),empty2)
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> ~ $less(length1(X6),X1) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ~ $less(length1(X4),X1) ) )
| ? [X3: $int] :
( ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> ~ $less(path_weight(X4,X2),X3) ) )
& ! [X4: list_vertex,X5: vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),empty2)
=> ~ $less($sum(path_weight(X4,X5),weight(X5,X2)),X3) ) ) )
& ( get1(X0,X2) = finite(X3) ) ) ) )
=> ! [X7: set_lpvertexcm_vertexrp] :
( ( X7 = edges )
=> ! [X9: map_vertex_t19,X8: set_lpvertexcm_vertexrp] :
( ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ( get1(X9,X2) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ~ $less(length1(X4),X1) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> ~ $less(length1(X6),X1) ) ) )
| ? [X3: $int] :
( ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> ~ $less(path_weight(X4,X2),X3) ) )
& ( get1(X9,X2) = finite(X3) )
& ? [X4: list_vertex] :
( ( path_weight(X4,X2) = X3 )
& path(s,X4,X2) )
& ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ~ $less($sum(path_weight(X4,X5),weight(X5,X2)),X3) ) ) ) ) ) )
& ! [X3: lpvertexcm_vertexrp] :
( mem2(X3,X8)
=> mem2(X3,edges) ) )
=> ! [X10: bool] :
( ( ( X10 = true )
<=> ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8) )
=> ( ( X10 != true )
=> ( ~ ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8)
=> ! [X12: vertex,X11: set_lpvertexcm_vertexrp,X13: vertex] :
( ( ( X11 = remove2(tuple22(X12,X13),X8) )
& mem2(tuple22(X12,X13),X8) )
=> ( ( ( ( 1 = X1 )
| $less(1,X1) )
& mem2(tuple22(X12,X13),edges)
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ~ $less($sum(path_weight(X4,X5),weight(X5,X2)),X3) ) ) )
& ( get1(X9,X2) = finite(X3) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> ~ $less(path_weight(X4,X2),X3) ) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) ) )
| ( ! [X5: vertex] :
( mem2(tuple22(X5,X2),diff2(edges,X8))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> ~ $less(length1(X6),X1) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ~ $less(length1(X4),X1) )
& ( get1(X9,X2) = infinite ) ) ) )
& ~ mem2(tuple22(X12,X13),diff2(edges,X8)) )
=> ! [X14: map_vertex_t19] :
( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
& ! [X5: vertex,X4: list_vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),add2(tuple22(X12,X13),diff2(edges,X8)))
=> ~ $less($sum(path_weight(X4,X5),weight(X5,X2)),X3) ) ) )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ( $less(length1(X4),X1)
=> ~ $less(path_weight(X4,X2),X3) ) )
& ? [X4: list_vertex] :
( ( path_weight(X4,X2) = X3 )
& path(s,X4,X2) ) )
| ( ( get1(X14,X2) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ~ $less(length1(X4),X1) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),add2(tuple22(X12,X13),diff2(edges,X8)))
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> ~ $less(length1(X6),X1) ) ) ) ) )
=> ! [X2: vertex] :
( mem1(X2,vertices)
=> ! [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
=> ! [X4: list_vertex,X5: vertex] :
( path(s,X4,X5)
=> ( $less(length1(X4),X1)
=> ( mem2(tuple22(X5,X2),diff2(edges,X11))
=> ~ $less($sum(path_weight(X4,X5),weight(X5,X2)),X3) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f198]) ).
tff(f245,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X2,diff2(X1,X0))
<=> ( ~ mem2(X2,X0)
& mem2(X2,X1) ) ),
inference(rectify,[],[f98]) ).
tff(f298,plain,
~ ( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
=> ! [X0: $int,X1: map_vertex_t19] :
( ( ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(X0,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X0 ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ( ! [X3: vertex] :
( mem2(tuple22(X3,X2),empty2)
=> ! [X4: list_vertex] :
( path(s,X4,X3)
=> ~ $less(length1(X4),X0) ) )
& ( infinite = get1(X1,X2) )
& ! [X5: list_vertex] :
( path(s,X5,X2)
=> ~ $less(length1(X5),X0) ) )
| ? [X6: $int] :
( ? [X7: list_vertex] :
( ( path_weight(X7,X2) = X6 )
& path(s,X7,X2) )
& ! [X8: list_vertex] :
( path(s,X8,X2)
=> ( $less(length1(X8),X0)
=> ~ $less(path_weight(X8,X2),X6) ) )
& ( finite(X6) = get1(X1,X2) )
& ! [X10: vertex,X9: list_vertex] :
( path(s,X9,X10)
=> ( $less(length1(X9),X0)
=> ( mem2(tuple22(X10,X2),empty2)
=> ~ $less($sum(path_weight(X9,X10),weight(X10,X2)),X6) ) ) ) ) ) )
=> ! [X11: set_lpvertexcm_vertexrp] :
( ( edges = X11 )
=> ! [X12: map_vertex_t19,X13: set_lpvertexcm_vertexrp] :
( ( ! [X23: lpvertexcm_vertexrp] :
( mem2(X23,X13)
=> mem2(X23,edges) )
& ! [X14: vertex] :
( mem1(X14,vertices)
=> ( ( ! [X16: vertex] :
( mem2(tuple22(X16,X14),diff2(edges,X13))
=> ! [X17: list_vertex] :
( path(s,X17,X16)
=> ~ $less(length1(X17),X0) ) )
& ( infinite = get1(X12,X14) )
& ! [X15: list_vertex] :
( path(s,X15,X14)
=> ~ $less(length1(X15),X0) ) )
| ? [X18: $int] :
( ! [X22: list_vertex,X21: vertex] :
( path(s,X22,X21)
=> ( $less(length1(X22),X0)
=> ( mem2(tuple22(X21,X14),diff2(edges,X13))
=> ~ $less($sum(path_weight(X22,X21),weight(X21,X14)),X18) ) ) )
& ! [X19: list_vertex] :
( path(s,X19,X14)
=> ( $less(length1(X19),X0)
=> ~ $less(path_weight(X19,X14),X18) ) )
& ( get1(X12,X14) = finite(X18) )
& ? [X20: list_vertex] :
( ( path_weight(X20,X14) = X18 )
& path(s,X20,X14) ) ) ) ) )
=> ! [X24: bool] :
( ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X13) )
=> ( ( true != X24 )
=> ( ~ ! [X26: lpvertexcm_vertexrp] : ~ mem2(X26,X13)
=> ! [X29: vertex,X27: vertex,X28: set_lpvertexcm_vertexrp] :
( ( mem2(tuple22(X27,X29),X13)
& ( remove2(tuple22(X27,X29),X13) = X28 ) )
=> ( ( ( $less(1,X0)
| ( 1 = X0 ) )
& ~ mem2(tuple22(X27,X29),diff2(edges,X13))
& ! [X30: vertex] :
( mem1(X30,vertices)
=> ( ? [X31: $int] :
( ! [X34: list_vertex] :
( path(s,X34,X30)
=> ( $less(length1(X34),X0)
=> ~ $less(path_weight(X34,X30),X31) ) )
& ! [X32: vertex,X33: list_vertex] :
( path(s,X33,X32)
=> ( $less(length1(X33),X0)
=> ( mem2(tuple22(X32,X30),diff2(edges,X13))
=> ~ $less($sum(path_weight(X33,X32),weight(X32,X30)),X31) ) ) )
& ( finite(X31) = get1(X12,X30) )
& ? [X35: list_vertex] :
( path(s,X35,X30)
& ( path_weight(X35,X30) = X31 ) ) )
| ( ! [X38: list_vertex] :
( path(s,X38,X30)
=> ~ $less(length1(X38),X0) )
& ( infinite = get1(X12,X30) )
& ! [X36: vertex] :
( mem2(tuple22(X36,X30),diff2(edges,X13))
=> ! [X37: list_vertex] :
( path(s,X37,X36)
=> ~ $less(length1(X37),X0) ) ) ) ) )
& mem2(tuple22(X27,X29),edges) )
=> ! [X39: map_vertex_t19] :
( ! [X40: vertex] :
( mem1(X40,vertices)
=> ( ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( path(s,X46,X40)
=> ~ $less(length1(X46),X0) )
& ! [X47: vertex] :
( mem2(tuple22(X47,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
=> ! [X48: list_vertex] :
( path(s,X48,X47)
=> ~ $less(length1(X48),X0) ) ) )
| ? [X41: $int] :
( ? [X45: list_vertex] :
( path(s,X45,X40)
& ( path_weight(X45,X40) = X41 ) )
& ! [X44: list_vertex] :
( path(s,X44,X40)
=> ( $less(length1(X44),X0)
=> ~ $less(path_weight(X44,X40),X41) ) )
& ! [X42: vertex,X43: list_vertex] :
( path(s,X43,X42)
=> ( $less(length1(X43),X0)
=> ( mem2(tuple22(X42,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
=> ~ $less($sum(path_weight(X43,X42),weight(X42,X40)),X41) ) ) )
& ( finite(X41) = get1(X39,X40) ) ) ) )
=> ! [X49: vertex] :
( mem1(X49,vertices)
=> ! [X50: $int] :
( ( get1(X39,X49) = finite(X50) )
=> ! [X52: vertex,X51: list_vertex] :
( path(s,X51,X52)
=> ( $less(length1(X51),X0)
=> ( mem2(tuple22(X52,X49),diff2(edges,X28))
=> ~ $less($sum(path_weight(X51,X52),weight(X52,X49)),X50) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f209]) ).
tff(f317,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( mem2(X1,remove2(X0,X2))
<=> ( ( X0 != X1 )
& mem2(X1,X2) ) ),
inference(rectify,[],[f77]) ).
tff(f321,plain,
! [X0: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ( mem2(X1,X2)
| ( X0 = X1 ) )
<=> mem2(X1,add2(X0,X2)) ),
inference(rectify,[],[f73]) ).
tff(f378,plain,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X0,X1)
| ( add2(X0,remove2(X0,X1)) = X1 ) ),
inference(ennf_transformation,[],[f80]) ).
tff(f387,plain,
( ? [X0: $int,X1: map_vertex_t19] :
( ? [X11: set_lpvertexcm_vertexrp] :
( ? [X12: map_vertex_t19,X13: set_lpvertexcm_vertexrp] :
( ? [X24: bool] :
( ? [X29: vertex,X27: vertex,X28: set_lpvertexcm_vertexrp] :
( ? [X39: map_vertex_t19] :
( ? [X49: vertex] :
( ? [X50: $int] :
( ? [X52: vertex,X51: list_vertex] :
( $less($sum(path_weight(X51,X52),weight(X52,X49)),X50)
& mem2(tuple22(X52,X49),diff2(edges,X28))
& $less(length1(X51),X0)
& path(s,X51,X52) )
& ( get1(X39,X49) = finite(X50) ) )
& mem1(X49,vertices) )
& ! [X40: vertex] :
( ( ! [X46: list_vertex] :
( ~ path(s,X46,X40)
| ~ $less(length1(X46),X0) )
& ( infinite = get1(X39,X40) )
& ! [X47: vertex] :
( ~ mem2(tuple22(X47,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
| ! [X48: list_vertex] :
( ~ path(s,X48,X47)
| ~ $less(length1(X48),X0) ) ) )
| ? [X41: $int] :
( ? [X45: list_vertex] :
( path(s,X45,X40)
& ( path_weight(X45,X40) = X41 ) )
& ! [X44: list_vertex] :
( ~ $less(path_weight(X44,X40),X41)
| ~ $less(length1(X44),X0)
| ~ path(s,X44,X40) )
& ! [X42: vertex,X43: list_vertex] :
( ~ $less($sum(path_weight(X43,X42),weight(X42,X40)),X41)
| ~ mem2(tuple22(X42,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
| ~ $less(length1(X43),X0)
| ~ path(s,X43,X42) )
& ( finite(X41) = get1(X39,X40) ) )
| ~ mem1(X40,vertices) ) )
& ( $less(1,X0)
| ( 1 = X0 ) )
& ~ mem2(tuple22(X27,X29),diff2(edges,X13))
& ! [X30: vertex] :
( ? [X31: $int] :
( ! [X34: list_vertex] :
( ~ $less(path_weight(X34,X30),X31)
| ~ $less(length1(X34),X0)
| ~ path(s,X34,X30) )
& ! [X32: vertex,X33: list_vertex] :
( ~ $less($sum(path_weight(X33,X32),weight(X32,X30)),X31)
| ~ mem2(tuple22(X32,X30),diff2(edges,X13))
| ~ $less(length1(X33),X0)
| ~ path(s,X33,X32) )
& ( finite(X31) = get1(X12,X30) )
& ? [X35: list_vertex] :
( path(s,X35,X30)
& ( path_weight(X35,X30) = X31 ) ) )
| ( ! [X38: list_vertex] :
( ~ path(s,X38,X30)
| ~ $less(length1(X38),X0) )
& ( infinite = get1(X12,X30) )
& ! [X36: vertex] :
( ! [X37: list_vertex] :
( ~ $less(length1(X37),X0)
| ~ path(s,X37,X36) )
| ~ mem2(tuple22(X36,X30),diff2(edges,X13)) ) )
| ~ mem1(X30,vertices) )
& mem2(tuple22(X27,X29),edges)
& mem2(tuple22(X27,X29),X13)
& ( remove2(tuple22(X27,X29),X13) = X28 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X13)
& ( true != X24 )
& ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X13) ) )
& ! [X23: lpvertexcm_vertexrp] :
( mem2(X23,edges)
| ~ mem2(X23,X13) )
& ! [X14: vertex] :
( ( ( infinite = get1(X12,X14) )
& ! [X16: vertex] :
( ~ mem2(tuple22(X16,X14),diff2(edges,X13))
| ! [X17: list_vertex] :
( ~ path(s,X17,X16)
| ~ $less(length1(X17),X0) ) )
& ! [X15: list_vertex] :
( ~ $less(length1(X15),X0)
| ~ path(s,X15,X14) ) )
| ? [X18: $int] :
( ! [X22: list_vertex,X21: vertex] :
( ~ $less($sum(path_weight(X22,X21),weight(X21,X14)),X18)
| ~ mem2(tuple22(X21,X14),diff2(edges,X13))
| ~ $less(length1(X22),X0)
| ~ path(s,X22,X21) )
& ! [X19: list_vertex] :
( ~ $less(path_weight(X19,X14),X18)
| ~ $less(length1(X19),X0)
| ~ path(s,X19,X14) )
& ( get1(X12,X14) = finite(X18) )
& ? [X20: list_vertex] :
( ( path_weight(X20,X14) = X18 )
& path(s,X20,X14) ) )
| ~ mem1(X14,vertices) ) )
& ( edges = X11 ) )
& ! [X2: vertex] :
( ( ! [X5: list_vertex] :
( ~ path(s,X5,X2)
| ~ $less(length1(X5),X0) )
& ! [X3: vertex] :
( ! [X4: list_vertex] :
( ~ path(s,X4,X3)
| ~ $less(length1(X4),X0) )
| ~ mem2(tuple22(X3,X2),empty2) )
& ( infinite = get1(X1,X2) ) )
| ? [X6: $int] :
( ? [X7: list_vertex] :
( ( path_weight(X7,X2) = X6 )
& path(s,X7,X2) )
& ! [X8: list_vertex] :
( ~ $less(path_weight(X8,X2),X6)
| ~ $less(length1(X8),X0)
| ~ path(s,X8,X2) )
& ( finite(X6) = get1(X1,X2) )
& ! [X10: vertex,X9: list_vertex] :
( ~ $less($sum(path_weight(X9,X10),weight(X10,X2)),X6)
| ~ mem2(tuple22(X10,X2),empty2)
| ~ $less(length1(X9),X0)
| ~ path(s,X9,X10) ) )
| ~ mem1(X2,vertices) )
& ( ( 1 = X0 )
| $less(1,X0) )
& ( $less(X0,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X0 ) ) )
& ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) ) ),
inference(ennf_transformation,[],[f298]) ).
tff(f388,plain,
( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
& ? [X1: map_vertex_t19,X0: $int] :
( ! [X2: vertex] :
( ( ! [X5: list_vertex] :
( ~ path(s,X5,X2)
| ~ $less(length1(X5),X0) )
& ! [X3: vertex] :
( ! [X4: list_vertex] :
( ~ path(s,X4,X3)
| ~ $less(length1(X4),X0) )
| ~ mem2(tuple22(X3,X2),empty2) )
& ( infinite = get1(X1,X2) ) )
| ~ mem1(X2,vertices)
| ? [X6: $int] :
( ( finite(X6) = get1(X1,X2) )
& ? [X7: list_vertex] :
( ( path_weight(X7,X2) = X6 )
& path(s,X7,X2) )
& ! [X10: vertex,X9: list_vertex] :
( ~ $less(length1(X9),X0)
| ~ $less($sum(path_weight(X9,X10),weight(X10,X2)),X6)
| ~ path(s,X9,X10)
| ~ mem2(tuple22(X10,X2),empty2) )
& ! [X8: list_vertex] :
( ~ $less(path_weight(X8,X2),X6)
| ~ path(s,X8,X2)
| ~ $less(length1(X8),X0) ) ) )
& ( $less(X0,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X0 ) )
& ( ( 1 = X0 )
| $less(1,X0) )
& ? [X11: set_lpvertexcm_vertexrp] :
( ( edges = X11 )
& ? [X12: map_vertex_t19,X13: set_lpvertexcm_vertexrp] :
( ? [X24: bool] :
( ( true != X24 )
& ? [X27: vertex,X29: vertex,X28: set_lpvertexcm_vertexrp] :
( ! [X30: vertex] :
( ? [X31: $int] :
( ! [X34: list_vertex] :
( ~ path(s,X34,X30)
| ~ $less(path_weight(X34,X30),X31)
| ~ $less(length1(X34),X0) )
& ( finite(X31) = get1(X12,X30) )
& ! [X33: list_vertex,X32: vertex] :
( ~ $less(length1(X33),X0)
| ~ mem2(tuple22(X32,X30),diff2(edges,X13))
| ~ path(s,X33,X32)
| ~ $less($sum(path_weight(X33,X32),weight(X32,X30)),X31) )
& ? [X35: list_vertex] :
( path(s,X35,X30)
& ( path_weight(X35,X30) = X31 ) ) )
| ~ mem1(X30,vertices)
| ( ! [X38: list_vertex] :
( ~ path(s,X38,X30)
| ~ $less(length1(X38),X0) )
& ( infinite = get1(X12,X30) )
& ! [X36: vertex] :
( ! [X37: list_vertex] :
( ~ $less(length1(X37),X0)
| ~ path(s,X37,X36) )
| ~ mem2(tuple22(X36,X30),diff2(edges,X13)) ) ) )
& mem2(tuple22(X27,X29),edges)
& ( $less(1,X0)
| ( 1 = X0 ) )
& mem2(tuple22(X27,X29),X13)
& ( remove2(tuple22(X27,X29),X13) = X28 )
& ? [X39: map_vertex_t19] :
( ! [X40: vertex] :
( ~ mem1(X40,vertices)
| ( ! [X46: list_vertex] :
( ~ path(s,X46,X40)
| ~ $less(length1(X46),X0) )
& ( infinite = get1(X39,X40) )
& ! [X47: vertex] :
( ~ mem2(tuple22(X47,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
| ! [X48: list_vertex] :
( ~ path(s,X48,X47)
| ~ $less(length1(X48),X0) ) ) )
| ? [X41: $int] :
( ! [X44: list_vertex] :
( ~ $less(path_weight(X44,X40),X41)
| ~ $less(length1(X44),X0)
| ~ path(s,X44,X40) )
& ( finite(X41) = get1(X39,X40) )
& ? [X45: list_vertex] :
( path(s,X45,X40)
& ( path_weight(X45,X40) = X41 ) )
& ! [X42: vertex,X43: list_vertex] :
( ~ $less($sum(path_weight(X43,X42),weight(X42,X40)),X41)
| ~ path(s,X43,X42)
| ~ $less(length1(X43),X0)
| ~ mem2(tuple22(X42,X40),add2(tuple22(X27,X29),diff2(edges,X13))) ) ) )
& ? [X49: vertex] :
( mem1(X49,vertices)
& ? [X50: $int] :
( ( get1(X39,X49) = finite(X50) )
& ? [X51: list_vertex,X52: vertex] :
( path(s,X51,X52)
& $less($sum(path_weight(X51,X52),weight(X52,X49)),X50)
& $less(length1(X51),X0)
& mem2(tuple22(X52,X49),diff2(edges,X28)) ) ) ) )
& ~ mem2(tuple22(X27,X29),diff2(edges,X13)) )
& ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X13) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X13) )
& ! [X23: lpvertexcm_vertexrp] :
( mem2(X23,edges)
| ~ mem2(X23,X13) )
& ! [X14: vertex] :
( ~ mem1(X14,vertices)
| ( ( infinite = get1(X12,X14) )
& ! [X16: vertex] :
( ~ mem2(tuple22(X16,X14),diff2(edges,X13))
| ! [X17: list_vertex] :
( ~ path(s,X17,X16)
| ~ $less(length1(X17),X0) ) )
& ! [X15: list_vertex] :
( ~ $less(length1(X15),X0)
| ~ path(s,X15,X14) ) )
| ? [X18: $int] :
( ( get1(X12,X14) = finite(X18) )
& ! [X19: list_vertex] :
( ~ $less(path_weight(X19,X14),X18)
| ~ path(s,X19,X14)
| ~ $less(length1(X19),X0) )
& ! [X21: vertex,X22: list_vertex] :
( ~ path(s,X22,X21)
| ~ $less($sum(path_weight(X22,X21),weight(X21,X14)),X18)
| ~ mem2(tuple22(X21,X14),diff2(edges,X13))
| ~ $less(length1(X22),X0) )
& ? [X20: list_vertex] :
( ( path_weight(X20,X14) = X18 )
& path(s,X20,X14) ) ) ) ) ) ) ),
inference(flattening,[],[f387]) ).
tff(f476,plain,
( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
& ? [X1: map_vertex_t19,X0: $int] :
( ! [X2: vertex] :
( ( ! [X5: list_vertex] :
( ~ path(s,X5,X2)
| ~ $less(length1(X5),X0) )
& ! [X3: vertex] :
( ! [X4: list_vertex] :
( ~ path(s,X4,X3)
| ~ $less(length1(X4),X0) )
| ~ mem2(tuple22(X3,X2),empty2) )
& ( infinite = get1(X1,X2) ) )
| ~ mem1(X2,vertices)
| ? [X6: $int] :
( ( finite(X6) = get1(X1,X2) )
& ? [X7: list_vertex] :
( ( path_weight(X7,X2) = X6 )
& path(s,X7,X2) )
& ! [X10: vertex,X9: list_vertex] :
( ~ $less(length1(X9),X0)
| ~ $less($sum(path_weight(X9,X10),weight(X10,X2)),X6)
| ~ path(s,X9,X10)
| ~ mem2(tuple22(X10,X2),empty2) )
& ! [X8: list_vertex] :
( ~ $less(path_weight(X8,X2),X6)
| ~ path(s,X8,X2)
| ~ $less(length1(X8),X0) ) ) )
& ( $less(X0,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X0 ) )
& ( ( 1 = X0 )
| $less(1,X0) )
& ? [X11: set_lpvertexcm_vertexrp] :
( ( edges = X11 )
& ? [X12: map_vertex_t19,X13: set_lpvertexcm_vertexrp] :
( ? [X24: bool] :
( ( true != X24 )
& ? [X27: vertex,X29: vertex,X28: set_lpvertexcm_vertexrp] :
( ! [X30: vertex] :
( ? [X31: $int] :
( ! [X34: list_vertex] :
( ~ path(s,X34,X30)
| ~ $less(path_weight(X34,X30),X31)
| ~ $less(length1(X34),X0) )
& ( finite(X31) = get1(X12,X30) )
& ! [X33: list_vertex,X32: vertex] :
( ~ $less(length1(X33),X0)
| ~ mem2(tuple22(X32,X30),diff2(edges,X13))
| ~ path(s,X33,X32)
| ~ $less($sum(path_weight(X33,X32),weight(X32,X30)),X31) )
& ? [X35: list_vertex] :
( path(s,X35,X30)
& ( path_weight(X35,X30) = X31 ) ) )
| ~ mem1(X30,vertices)
| ( ! [X38: list_vertex] :
( ~ path(s,X38,X30)
| ~ $less(length1(X38),X0) )
& ( infinite = get1(X12,X30) )
& ! [X36: vertex] :
( ! [X37: list_vertex] :
( ~ $less(length1(X37),X0)
| ~ path(s,X37,X36) )
| ~ mem2(tuple22(X36,X30),diff2(edges,X13)) ) ) )
& mem2(tuple22(X27,X29),edges)
& ( $less(1,X0)
| ( 1 = X0 ) )
& mem2(tuple22(X27,X29),X13)
& ( remove2(tuple22(X27,X29),X13) = X28 )
& ? [X39: map_vertex_t19] :
( ! [X40: vertex] :
( ~ mem1(X40,vertices)
| ( ! [X46: list_vertex] :
( ~ path(s,X46,X40)
| ~ $less(length1(X46),X0) )
& ( infinite = get1(X39,X40) )
& ! [X47: vertex] :
( ~ mem2(tuple22(X47,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
| ! [X48: list_vertex] :
( ~ path(s,X48,X47)
| ~ $less(length1(X48),X0) ) ) )
| ? [X41: $int] :
( ! [X44: list_vertex] :
( ~ $less(path_weight(X44,X40),X41)
| ~ $less(length1(X44),X0)
| ~ path(s,X44,X40) )
& ( finite(X41) = get1(X39,X40) )
& ? [X45: list_vertex] :
( path(s,X45,X40)
& ( path_weight(X45,X40) = X41 ) )
& ! [X42: vertex,X43: list_vertex] :
( ~ $less($sum(path_weight(X43,X42),weight(X42,X40)),X41)
| ~ path(s,X43,X42)
| ~ $less(length1(X43),X0)
| ~ mem2(tuple22(X42,X40),add2(tuple22(X27,X29),diff2(edges,X13))) ) ) )
& ? [X49: vertex] :
( mem1(X49,vertices)
& ? [X50: $int] :
( ( get1(X39,X49) = finite(X50) )
& ? [X51: list_vertex,X52: vertex] :
( path(s,X51,X52)
& $less($sum(path_weight(X51,X52),weight(X52,X49)),X50)
& $less(length1(X51),X0)
& mem2(tuple22(X52,X49),diff2(edges,X28)) ) ) ) )
& ~ mem2(tuple22(X27,X29),diff2(edges,X13)) )
& ( ( true = X24 )
| ? [X25: lpvertexcm_vertexrp] : mem2(X25,X13) )
& ( ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X13)
| ( true != X24 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X13) )
& ! [X23: lpvertexcm_vertexrp] :
( mem2(X23,edges)
| ~ mem2(X23,X13) )
& ! [X14: vertex] :
( ~ mem1(X14,vertices)
| ( ( infinite = get1(X12,X14) )
& ! [X16: vertex] :
( ~ mem2(tuple22(X16,X14),diff2(edges,X13))
| ! [X17: list_vertex] :
( ~ path(s,X17,X16)
| ~ $less(length1(X17),X0) ) )
& ! [X15: list_vertex] :
( ~ $less(length1(X15),X0)
| ~ path(s,X15,X14) ) )
| ? [X18: $int] :
( ( get1(X12,X14) = finite(X18) )
& ! [X19: list_vertex] :
( ~ $less(path_weight(X19,X14),X18)
| ~ path(s,X19,X14)
| ~ $less(length1(X19),X0) )
& ! [X21: vertex,X22: list_vertex] :
( ~ path(s,X22,X21)
| ~ $less($sum(path_weight(X22,X21),weight(X21,X14)),X18)
| ~ mem2(tuple22(X21,X14),diff2(edges,X13))
| ~ $less(length1(X22),X0) )
& ? [X20: list_vertex] :
( ( path_weight(X20,X14) = X18 )
& path(s,X20,X14) ) ) ) ) ) ) ),
inference(nnf_transformation,[],[f388]) ).
tff(f477,plain,
( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
& ? [X1: map_vertex_t19,X0: $int] :
( ! [X2: vertex] :
( ( ! [X5: list_vertex] :
( ~ path(s,X5,X2)
| ~ $less(length1(X5),X0) )
& ! [X3: vertex] :
( ! [X4: list_vertex] :
( ~ path(s,X4,X3)
| ~ $less(length1(X4),X0) )
| ~ mem2(tuple22(X3,X2),empty2) )
& ( infinite = get1(X1,X2) ) )
| ~ mem1(X2,vertices)
| ? [X6: $int] :
( ( finite(X6) = get1(X1,X2) )
& ? [X7: list_vertex] :
( ( path_weight(X7,X2) = X6 )
& path(s,X7,X2) )
& ! [X10: vertex,X9: list_vertex] :
( ~ $less(length1(X9),X0)
| ~ $less($sum(path_weight(X9,X10),weight(X10,X2)),X6)
| ~ path(s,X9,X10)
| ~ mem2(tuple22(X10,X2),empty2) )
& ! [X8: list_vertex] :
( ~ $less(path_weight(X8,X2),X6)
| ~ path(s,X8,X2)
| ~ $less(length1(X8),X0) ) ) )
& ( $less(X0,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X0 ) )
& ( ( 1 = X0 )
| $less(1,X0) )
& ? [X11: set_lpvertexcm_vertexrp] :
( ( edges = X11 )
& ? [X12: map_vertex_t19,X13: set_lpvertexcm_vertexrp] :
( ? [X24: bool] :
( ( true != X24 )
& ? [X27: vertex,X29: vertex,X28: set_lpvertexcm_vertexrp] :
( ! [X30: vertex] :
( ? [X31: $int] :
( ! [X34: list_vertex] :
( ~ path(s,X34,X30)
| ~ $less(path_weight(X34,X30),X31)
| ~ $less(length1(X34),X0) )
& ( finite(X31) = get1(X12,X30) )
& ! [X33: list_vertex,X32: vertex] :
( ~ $less(length1(X33),X0)
| ~ mem2(tuple22(X32,X30),diff2(edges,X13))
| ~ path(s,X33,X32)
| ~ $less($sum(path_weight(X33,X32),weight(X32,X30)),X31) )
& ? [X35: list_vertex] :
( path(s,X35,X30)
& ( path_weight(X35,X30) = X31 ) ) )
| ~ mem1(X30,vertices)
| ( ! [X38: list_vertex] :
( ~ path(s,X38,X30)
| ~ $less(length1(X38),X0) )
& ( infinite = get1(X12,X30) )
& ! [X36: vertex] :
( ! [X37: list_vertex] :
( ~ $less(length1(X37),X0)
| ~ path(s,X37,X36) )
| ~ mem2(tuple22(X36,X30),diff2(edges,X13)) ) ) )
& mem2(tuple22(X27,X29),edges)
& ( $less(1,X0)
| ( 1 = X0 ) )
& mem2(tuple22(X27,X29),X13)
& ( remove2(tuple22(X27,X29),X13) = X28 )
& ? [X39: map_vertex_t19] :
( ! [X40: vertex] :
( ~ mem1(X40,vertices)
| ( ! [X46: list_vertex] :
( ~ path(s,X46,X40)
| ~ $less(length1(X46),X0) )
& ( infinite = get1(X39,X40) )
& ! [X47: vertex] :
( ~ mem2(tuple22(X47,X40),add2(tuple22(X27,X29),diff2(edges,X13)))
| ! [X48: list_vertex] :
( ~ path(s,X48,X47)
| ~ $less(length1(X48),X0) ) ) )
| ? [X41: $int] :
( ! [X44: list_vertex] :
( ~ $less(path_weight(X44,X40),X41)
| ~ $less(length1(X44),X0)
| ~ path(s,X44,X40) )
& ( finite(X41) = get1(X39,X40) )
& ? [X45: list_vertex] :
( path(s,X45,X40)
& ( path_weight(X45,X40) = X41 ) )
& ! [X42: vertex,X43: list_vertex] :
( ~ $less($sum(path_weight(X43,X42),weight(X42,X40)),X41)
| ~ path(s,X43,X42)
| ~ $less(length1(X43),X0)
| ~ mem2(tuple22(X42,X40),add2(tuple22(X27,X29),diff2(edges,X13))) ) ) )
& ? [X49: vertex] :
( mem1(X49,vertices)
& ? [X50: $int] :
( ( get1(X39,X49) = finite(X50) )
& ? [X51: list_vertex,X52: vertex] :
( path(s,X51,X52)
& $less($sum(path_weight(X51,X52),weight(X52,X49)),X50)
& $less(length1(X51),X0)
& mem2(tuple22(X52,X49),diff2(edges,X28)) ) ) ) )
& ~ mem2(tuple22(X27,X29),diff2(edges,X13)) )
& ( ( true = X24 )
| ? [X25: lpvertexcm_vertexrp] : mem2(X25,X13) )
& ( ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X13)
| ( true != X24 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X13) )
& ! [X23: lpvertexcm_vertexrp] :
( mem2(X23,edges)
| ~ mem2(X23,X13) )
& ! [X14: vertex] :
( ~ mem1(X14,vertices)
| ( ( infinite = get1(X12,X14) )
& ! [X16: vertex] :
( ~ mem2(tuple22(X16,X14),diff2(edges,X13))
| ! [X17: list_vertex] :
( ~ path(s,X17,X16)
| ~ $less(length1(X17),X0) ) )
& ! [X15: list_vertex] :
( ~ $less(length1(X15),X0)
| ~ path(s,X15,X14) ) )
| ? [X18: $int] :
( ( get1(X12,X14) = finite(X18) )
& ! [X19: list_vertex] :
( ~ $less(path_weight(X19,X14),X18)
| ~ path(s,X19,X14)
| ~ $less(length1(X19),X0) )
& ! [X21: vertex,X22: list_vertex] :
( ~ path(s,X22,X21)
| ~ $less($sum(path_weight(X22,X21),weight(X21,X14)),X18)
| ~ mem2(tuple22(X21,X14),diff2(edges,X13))
| ~ $less(length1(X22),X0) )
& ? [X20: list_vertex] :
( ( path_weight(X20,X14) = X18 )
& path(s,X20,X14) ) ) ) ) ) ) ),
inference(flattening,[],[f476]) ).
tff(f478,plain,
( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
& ? [X0: map_vertex_t19,X1: $int] :
( ! [X2: vertex] :
( ( ! [X3: list_vertex] :
( ~ path(s,X3,X2)
| ~ $less(length1(X3),X1) )
& ! [X4: vertex] :
( ! [X5: list_vertex] :
( ~ path(s,X5,X4)
| ~ $less(length1(X5),X1) )
| ~ mem2(tuple22(X4,X2),empty2) )
& ( get1(X0,X2) = infinite ) )
| ~ mem1(X2,vertices)
| ? [X6: $int] :
( ( get1(X0,X2) = finite(X6) )
& ? [X7: list_vertex] :
( ( path_weight(X7,X2) = X6 )
& path(s,X7,X2) )
& ! [X8: vertex,X9: list_vertex] :
( ~ $less(length1(X9),X1)
| ~ $less($sum(path_weight(X9,X8),weight(X8,X2)),X6)
| ~ path(s,X9,X8)
| ~ mem2(tuple22(X8,X2),empty2) )
& ! [X10: list_vertex] :
( ~ $less(path_weight(X10,X2),X6)
| ~ path(s,X10,X2)
| ~ $less(length1(X10),X1) ) ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) )
& ( ( 1 = X1 )
| $less(1,X1) )
& ? [X11: set_lpvertexcm_vertexrp] :
( ( edges = X11 )
& ? [X12: map_vertex_t19,X13: set_lpvertexcm_vertexrp] :
( ? [X14: bool] :
( ( true != X14 )
& ? [X15: vertex,X16: vertex,X17: set_lpvertexcm_vertexrp] :
( ! [X18: vertex] :
( ? [X19: $int] :
( ! [X20: list_vertex] :
( ~ path(s,X20,X18)
| ~ $less(path_weight(X20,X18),X19)
| ~ $less(length1(X20),X1) )
& ( finite(X19) = get1(X12,X18) )
& ! [X21: list_vertex,X22: vertex] :
( ~ $less(length1(X21),X1)
| ~ mem2(tuple22(X22,X18),diff2(edges,X13))
| ~ path(s,X21,X22)
| ~ $less($sum(path_weight(X21,X22),weight(X22,X18)),X19) )
& ? [X23: list_vertex] :
( path(s,X23,X18)
& ( path_weight(X23,X18) = X19 ) ) )
| ~ mem1(X18,vertices)
| ( ! [X24: list_vertex] :
( ~ path(s,X24,X18)
| ~ $less(length1(X24),X1) )
& ( infinite = get1(X12,X18) )
& ! [X25: vertex] :
( ! [X26: list_vertex] :
( ~ $less(length1(X26),X1)
| ~ path(s,X26,X25) )
| ~ mem2(tuple22(X25,X18),diff2(edges,X13)) ) ) )
& mem2(tuple22(X15,X16),edges)
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X15,X16),X13)
& ( remove2(tuple22(X15,X16),X13) = X17 )
& ? [X27: map_vertex_t19] :
( ! [X28: vertex] :
( ~ mem1(X28,vertices)
| ( ! [X29: list_vertex] :
( ~ path(s,X29,X28)
| ~ $less(length1(X29),X1) )
& ( infinite = get1(X27,X28) )
& ! [X30: vertex] :
( ~ mem2(tuple22(X30,X28),add2(tuple22(X15,X16),diff2(edges,X13)))
| ! [X31: list_vertex] :
( ~ path(s,X31,X30)
| ~ $less(length1(X31),X1) ) ) )
| ? [X32: $int] :
( ! [X33: list_vertex] :
( ~ $less(path_weight(X33,X28),X32)
| ~ $less(length1(X33),X1)
| ~ path(s,X33,X28) )
& ( get1(X27,X28) = finite(X32) )
& ? [X34: list_vertex] :
( path(s,X34,X28)
& ( path_weight(X34,X28) = X32 ) )
& ! [X35: vertex,X36: list_vertex] :
( ~ $less($sum(path_weight(X36,X35),weight(X35,X28)),X32)
| ~ path(s,X36,X35)
| ~ $less(length1(X36),X1)
| ~ mem2(tuple22(X35,X28),add2(tuple22(X15,X16),diff2(edges,X13))) ) ) )
& ? [X37: vertex] :
( mem1(X37,vertices)
& ? [X38: $int] :
( ( finite(X38) = get1(X27,X37) )
& ? [X39: list_vertex,X40: vertex] :
( path(s,X39,X40)
& $less($sum(path_weight(X39,X40),weight(X40,X37)),X38)
& $less(length1(X39),X1)
& mem2(tuple22(X40,X37),diff2(edges,X17)) ) ) ) )
& ~ mem2(tuple22(X15,X16),diff2(edges,X13)) )
& ( ( true = X14 )
| ? [X41: lpvertexcm_vertexrp] : mem2(X41,X13) )
& ( ! [X42: lpvertexcm_vertexrp] : ~ mem2(X42,X13)
| ( true != X14 ) )
& ? [X43: lpvertexcm_vertexrp] : mem2(X43,X13) )
& ! [X44: lpvertexcm_vertexrp] :
( mem2(X44,edges)
| ~ mem2(X44,X13) )
& ! [X45: vertex] :
( ~ mem1(X45,vertices)
| ( ( infinite = get1(X12,X45) )
& ! [X46: vertex] :
( ~ mem2(tuple22(X46,X45),diff2(edges,X13))
| ! [X47: list_vertex] :
( ~ path(s,X47,X46)
| ~ $less(length1(X47),X1) ) )
& ! [X48: list_vertex] :
( ~ $less(length1(X48),X1)
| ~ path(s,X48,X45) ) )
| ? [X49: $int] :
( ( finite(X49) = get1(X12,X45) )
& ! [X50: list_vertex] :
( ~ $less(path_weight(X50,X45),X49)
| ~ path(s,X50,X45)
| ~ $less(length1(X50),X1) )
& ! [X51: vertex,X52: list_vertex] :
( ~ path(s,X52,X51)
| ~ $less($sum(path_weight(X52,X51),weight(X51,X45)),X49)
| ~ mem2(tuple22(X51,X45),diff2(edges,X13))
| ~ $less(length1(X52),X1) )
& ? [X53: list_vertex] :
( ( path_weight(X53,X45) = X49 )
& path(s,X53,X45) ) ) ) ) ) ) ),
inference(rectify,[],[f477]) ).
tff(f479,plain,
( ( ( 1 = $sum(cardinal1(vertices),$uminus(1)) )
| $less(1,$sum(cardinal1(vertices),$uminus(1))) )
& ! [X2: vertex] :
( ( ! [X3: list_vertex] :
( ~ path(s,X3,X2)
| ~ $less(length1(X3),sK20) )
& ! [X4: vertex] :
( ! [X5: list_vertex] :
( ~ path(s,X5,X4)
| ~ $less(length1(X5),sK20) )
| ~ mem2(tuple22(X4,X2),empty2) )
& ( infinite = get1(sK19,X2) ) )
| ~ mem1(X2,vertices)
| ( ( finite(sK21(X2)) = get1(sK19,X2) )
& ( sK21(X2) = path_weight(sK22(X2),X2) )
& path(s,sK22(X2),X2)
& ! [X8: vertex,X9: list_vertex] :
( ~ $less(length1(X9),sK20)
| ~ $less($sum(path_weight(X9,X8),weight(X8,X2)),sK21(X2))
| ~ path(s,X9,X8)
| ~ mem2(tuple22(X8,X2),empty2) )
& ! [X10: list_vertex] :
( ~ $less(path_weight(X10,X2),sK21(X2))
| ~ path(s,X10,X2)
| ~ $less(length1(X10),sK20) ) ) )
& ( $less(sK20,$sum(cardinal1(vertices),$uminus(1)))
| ( sK20 = $sum(cardinal1(vertices),$uminus(1)) ) )
& ( ( 1 = sK20 )
| $less(1,sK20) )
& ( edges = sK23 )
& ( true != sK26 )
& ! [X18: vertex] :
( ( ! [X20: list_vertex] :
( ~ path(s,X20,X18)
| ~ $less(path_weight(X20,X18),sK30(X18))
| ~ $less(length1(X20),sK20) )
& ( get1(sK24,X18) = finite(sK30(X18)) )
& ! [X21: list_vertex,X22: vertex] :
( ~ $less(length1(X21),sK20)
| ~ mem2(tuple22(X22,X18),diff2(edges,sK25))
| ~ path(s,X21,X22)
| ~ $less($sum(path_weight(X21,X22),weight(X22,X18)),sK30(X18)) )
& path(s,sK31(X18),X18)
& ( sK30(X18) = path_weight(sK31(X18),X18) ) )
| ~ mem1(X18,vertices)
| ( ! [X24: list_vertex] :
( ~ path(s,X24,X18)
| ~ $less(length1(X24),sK20) )
& ( infinite = get1(sK24,X18) )
& ! [X25: vertex] :
( ! [X26: list_vertex] :
( ~ $less(length1(X26),sK20)
| ~ path(s,X26,X25) )
| ~ mem2(tuple22(X25,X18),diff2(edges,sK25)) ) ) )
& mem2(tuple22(sK27,sK28),edges)
& ( $less(1,sK20)
| ( 1 = sK20 ) )
& mem2(tuple22(sK27,sK28),sK25)
& ( sK29 = remove2(tuple22(sK27,sK28),sK25) )
& ! [X28: vertex] :
( ~ mem1(X28,vertices)
| ( ! [X29: list_vertex] :
( ~ path(s,X29,X28)
| ~ $less(length1(X29),sK20) )
& ( infinite = get1(sK32,X28) )
& ! [X30: vertex] :
( ~ mem2(tuple22(X30,X28),add2(tuple22(sK27,sK28),diff2(edges,sK25)))
| ! [X31: list_vertex] :
( ~ path(s,X31,X30)
| ~ $less(length1(X31),sK20) ) ) )
| ( ! [X33: list_vertex] :
( ~ $less(path_weight(X33,X28),sK33(X28))
| ~ $less(length1(X33),sK20)
| ~ path(s,X33,X28) )
& ( get1(sK32,X28) = finite(sK33(X28)) )
& path(s,sK34(X28),X28)
& ( sK33(X28) = path_weight(sK34(X28),X28) )
& ! [X35: vertex,X36: list_vertex] :
( ~ $less($sum(path_weight(X36,X35),weight(X35,X28)),sK33(X28))
| ~ path(s,X36,X35)
| ~ $less(length1(X36),sK20)
| ~ mem2(tuple22(X35,X28),add2(tuple22(sK27,sK28),diff2(edges,sK25))) ) ) )
& mem1(sK35,vertices)
& ( finite(sK36) = get1(sK32,sK35) )
& path(s,sK37,sK38)
& $less($sum(path_weight(sK37,sK38),weight(sK38,sK35)),sK36)
& $less(length1(sK37),sK20)
& mem2(tuple22(sK38,sK35),diff2(edges,sK29))
& ~ mem2(tuple22(sK27,sK28),diff2(edges,sK25))
& ( ( true = sK26 )
| mem2(sK39,sK25) )
& ( ! [X42: lpvertexcm_vertexrp] : ~ mem2(X42,sK25)
| ( true != sK26 ) )
& mem2(sK40,sK25)
& ! [X44: lpvertexcm_vertexrp] :
( mem2(X44,edges)
| ~ mem2(X44,sK25) )
& ! [X45: vertex] :
( ~ mem1(X45,vertices)
| ( ( infinite = get1(sK24,X45) )
& ! [X46: vertex] :
( ~ mem2(tuple22(X46,X45),diff2(edges,sK25))
| ! [X47: list_vertex] :
( ~ path(s,X47,X46)
| ~ $less(length1(X47),sK20) ) )
& ! [X48: list_vertex] :
( ~ $less(length1(X48),sK20)
| ~ path(s,X48,X45) ) )
| ( ( finite(sK41(X45)) = get1(sK24,X45) )
& ! [X50: list_vertex] :
( ~ $less(path_weight(X50,X45),sK41(X45))
| ~ path(s,X50,X45)
| ~ $less(length1(X50),sK20) )
& ! [X51: vertex,X52: list_vertex] :
( ~ path(s,X52,X51)
| ~ $less($sum(path_weight(X52,X51),weight(X51,X45)),sK41(X45))
| ~ mem2(tuple22(X51,X45),diff2(edges,sK25))
| ~ $less(length1(X52),sK20) )
& ( sK41(X45) = path_weight(sK42(X45),X45) )
& path(s,sK42(X45),X45) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42]),skolemize(X0,sK19),skolemize(X1,sK20),skolemize(X6,sK21(X2)),skolemize(X7,sK22(X2)),skolemize(X11,sK23),skolemize(X12,sK24),skolemize(X13,sK25),skolemize(X14,sK26),skolemize(X15,sK27),skolemize(X16,sK28),skolemize(X17,sK29),skolemize(X19,sK30(X18)),skolemize(X23,sK31(X18)),skolemize(X27,sK32),skolemize(X32,sK33(X28)),skolemize(X34,sK34(X28)),skolemize(X37,sK35),skolemize(X38,sK36),skolemize(X39,sK37),skolemize(X40,sK38),skolemize(X41,sK39),skolemize(X43,sK40),skolemize(X49,sK41(X45)),skolemize(X53,sK42(X45))],[f478]) ).
tff(f528,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ( mem2(X2,diff2(X1,X0))
| mem2(X2,X0)
| ~ mem2(X2,X1) )
& ( ( ~ mem2(X2,X0)
& mem2(X2,X1) )
| ~ mem2(X2,diff2(X1,X0)) ) ),
inference(nnf_transformation,[],[f245]) ).
tff(f529,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ( mem2(X2,diff2(X1,X0))
| mem2(X2,X0)
| ~ mem2(X2,X1) )
& ( ( ~ mem2(X2,X0)
& mem2(X2,X1) )
| ~ mem2(X2,diff2(X1,X0)) ) ),
inference(flattening,[],[f528]) ).
tff(f530,plain,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp] :
( ( mem2(X0,diff2(X2,X1))
| mem2(X0,X1)
| ~ mem2(X0,X2) )
& ( ( ~ mem2(X0,X1)
& mem2(X0,X2) )
| ~ mem2(X0,diff2(X2,X1)) ) ),
inference(rectify,[],[f529]) ).
tff(f566,plain,
! [X0: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ( mem2(X1,X2)
| ( X0 = X1 )
| ~ mem2(X1,add2(X0,X2)) )
& ( mem2(X1,add2(X0,X2))
| ( ~ mem2(X1,X2)
& ( X0 != X1 ) ) ) ),
inference(nnf_transformation,[],[f321]) ).
tff(f567,plain,
! [X0: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ( mem2(X1,X2)
| ( X0 = X1 )
| ~ mem2(X1,add2(X0,X2)) )
& ( mem2(X1,add2(X0,X2))
| ( ~ mem2(X1,X2)
& ( X0 != X1 ) ) ) ),
inference(flattening,[],[f566]) ).
tff(f568,plain,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp,X2: lpvertexcm_vertexrp] :
( ( mem2(X2,X1)
| ( X0 = X2 )
| ~ mem2(X2,add2(X0,X1)) )
& ( mem2(X2,add2(X0,X1))
| ( ~ mem2(X2,X1)
& ( X0 != X2 ) ) ) ),
inference(rectify,[],[f567]) ).
tff(f591,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ( mem2(X1,remove2(X0,X2))
| ( X0 = X1 )
| ~ mem2(X1,X2) )
& ( ( ( X0 != X1 )
& mem2(X1,X2) )
| ~ mem2(X1,remove2(X0,X2)) ) ),
inference(nnf_transformation,[],[f317]) ).
tff(f592,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ( mem2(X1,remove2(X0,X2))
| ( X0 = X1 )
| ~ mem2(X1,X2) )
& ( ( ( X0 != X1 )
& mem2(X1,X2) )
| ~ mem2(X1,remove2(X0,X2)) ) ),
inference(flattening,[],[f591]) ).
tff(f593,plain,
! [X0: set_lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp,X2: lpvertexcm_vertexrp] :
( ( mem2(X2,remove2(X1,X0))
| ( X1 = X2 )
| ~ mem2(X2,X0) )
& ( ( ( X1 != X2 )
& mem2(X2,X0) )
| ~ mem2(X2,remove2(X1,X0)) ) ),
inference(rectify,[],[f592]) ).
tff(f701,plain,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ( add2(X0,remove2(X0,X1)) = X1 )
| ~ mem2(X0,X1) ),
inference(cnf_transformation,[],[f378]) ).
tff(f734,plain,
mem2(tuple22(sK38,sK35),diff2(edges,sK29)),
inference(cnf_transformation,[],[f479]) ).
tff(f735,plain,
$less(length1(sK37),sK20),
inference(cnf_transformation,[],[f479]) ).
tff(f736,plain,
$less($sum(path_weight(sK37,sK38),weight(sK38,sK35)),sK36),
inference(cnf_transformation,[],[f479]) ).
tff(f737,plain,
path(s,sK37,sK38),
inference(cnf_transformation,[],[f479]) ).
tff(f738,plain,
finite(sK36) = get1(sK32,sK35),
inference(cnf_transformation,[],[f479]) ).
tff(f739,plain,
mem1(sK35,vertices),
inference(cnf_transformation,[],[f479]) ).
tff(f745,plain,
! [X28: vertex,X36: list_vertex,X35: vertex] :
( ~ mem1(X28,vertices)
| ( infinite = get1(sK32,X28) )
| ~ $less($sum(path_weight(X36,X35),weight(X35,X28)),sK33(X28))
| ~ path(s,X36,X35)
| ~ $less(length1(X36),sK20)
| ~ mem2(tuple22(X35,X28),add2(tuple22(sK27,sK28),diff2(edges,sK25))) ),
inference(cnf_transformation,[],[f479]) ).
tff(f748,plain,
! [X28: vertex] :
( ( get1(sK32,X28) = finite(sK33(X28)) )
| ~ mem1(X28,vertices)
| ( infinite = get1(sK32,X28) ) ),
inference(cnf_transformation,[],[f479]) ).
tff(f755,plain,
sK29 = remove2(tuple22(sK27,sK28),sK25),
inference(cnf_transformation,[],[f479]) ).
tff(f756,plain,
mem2(tuple22(sK27,sK28),sK25),
inference(cnf_transformation,[],[f479]) ).
tff(f775,plain,
edges = sK23,
inference(cnf_transformation,[],[f479]) ).
tff(f874,plain,
! [X0: $int] : ( infinite != finite(X0) ),
inference(cnf_transformation,[],[f180]) ).
tff(f875,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X0,diff2(X2,X1))
| mem2(X0,X2) ),
inference(cnf_transformation,[],[f530]) ).
tff(f876,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X0,diff2(X2,X1))
| ~ mem2(X0,X1) ),
inference(cnf_transformation,[],[f530]) ).
tff(f877,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X0,diff2(X2,X1))
| ~ mem2(X0,X2)
| mem2(X0,X1) ),
inference(cnf_transformation,[],[f530]) ).
tff(f951,plain,
! [X2: lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X2,add2(X0,X1))
| ( X0 != X2 ) ),
inference(cnf_transformation,[],[f568]) ).
tff(f952,plain,
! [X2: lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X2,add2(X0,X1))
| ~ mem2(X2,X1) ),
inference(cnf_transformation,[],[f568]) ).
tff(f953,plain,
! [X2: lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X2,add2(X0,X1))
| ( X0 = X2 )
| mem2(X2,X1) ),
inference(cnf_transformation,[],[f568]) ).
tff(f999,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ( X1 != X2 )
| ~ mem2(X2,remove2(X1,X0)) ),
inference(cnf_transformation,[],[f593]) ).
tff(f1018,plain,
! [X0: $int] : ( finite_proj_1(finite(X0)) = X0 ),
inference(cnf_transformation,[],[f181]) ).
tff(f1045,plain,
! [X28: vertex,X36: list_vertex,X35: vertex] :
( ~ $less(length1(X36),sK20)
| ( infinite = get1(sK32,X28) )
| ~ path(s,X36,X35)
| ~ mem2(tuple22(X35,X28),add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| ~ $less($sum(path_weight(X36,X35),weight(X35,X28)),sK33(X28))
| ~ mem1(X28,vertices) ),
inference(definition_unfolding,[],[f745,f775]) ).
tff(f1051,plain,
mem2(tuple22(sK38,sK35),diff2(sK23,sK29)),
inference(definition_unfolding,[],[f734,f775]) ).
tff(f1085,plain,
! [X2: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] : mem2(X2,add2(X2,X1)),
inference(equality_resolution,[],[f951]) ).
tff(f1089,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp] : ~ mem2(X2,remove2(X2,X0)),
inference(equality_resolution,[],[f999]) ).
tff(f1133,plain,
! [X28: vertex,X36: list_vertex,X35: vertex] :
( ~ mem2(tuple22(X35,X28),add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| ( infinite = get1(sK32,X28) )
| mem1(X28,vertices)
| ~ $less(length1(X36),sK20)
| ~ $less($sum(path_weight(X36,X35),weight(X35,X28)),sK33(X28))
| path(s,X36,X35) ),
inference(consistent_polarity_flipping,[],[f1045]) ).
tff(f1141,plain,
! [X28: vertex] :
( ( get1(sK32,X28) = finite(sK33(X28)) )
| ( infinite = get1(sK32,X28) )
| mem1(X28,vertices) ),
inference(consistent_polarity_flipping,[],[f748]) ).
tff(f1144,plain,
~ path(s,sK37,sK38),
inference(consistent_polarity_flipping,[],[f737]) ).
tff(f1223,plain,
~ mem1(sK35,vertices),
inference(consistent_polarity_flipping,[],[f739]) ).
tff(f1434,definition,
( spl93_15
<=> mem2(tuple22(sK27,sK28),sK25) ),
introduced(definition,[new_symbols(definition,[spl93_15])],[avatar_definition]) ).
tff(f1436,plain,
( mem2(tuple22(sK27,sK28),sK25)
| ~ spl93_15 ),
inference(avatar_component_clause,[],[f1434]) ).
tff(f1437,plain,
spl93_15,
inference(avatar_split_clause,[],[f756,f1434]) ).
tff(f1439,definition,
( spl93_16
<=> ( sK29 = remove2(tuple22(sK27,sK28),sK25) ) ),
introduced(definition,[new_symbols(definition,[spl93_16])],[avatar_definition]) ).
tff(f1441,plain,
( ( sK29 = remove2(tuple22(sK27,sK28),sK25) )
| ~ spl93_16 ),
inference(avatar_component_clause,[],[f1439]) ).
tff(f1442,plain,
spl93_16,
inference(avatar_split_clause,[],[f755,f1439]) ).
tff(f1453,definition,
( spl93_19
<=> $less(length1(sK37),sK20) ),
introduced(definition,[new_symbols(definition,[spl93_19])],[avatar_definition]) ).
tff(f1455,plain,
( $less(length1(sK37),sK20)
| ~ spl93_19 ),
inference(avatar_component_clause,[],[f1453]) ).
tff(f1456,plain,
spl93_19,
inference(avatar_split_clause,[],[f735,f1453]) ).
tff(f1475,definition,
( spl93_24
<=> mem2(tuple22(sK38,sK35),diff2(sK23,sK29)) ),
introduced(definition,[new_symbols(definition,[spl93_24])],[avatar_definition]) ).
tff(f1477,plain,
( mem2(tuple22(sK38,sK35),diff2(sK23,sK29))
| ~ spl93_24 ),
inference(avatar_component_clause,[],[f1475]) ).
tff(f1478,plain,
spl93_24,
inference(avatar_split_clause,[],[f1051,f1475]) ).
tff(f1497,definition,
( spl93_28
<=> path(s,sK37,sK38) ),
introduced(definition,[new_symbols(definition,[spl93_28])],[avatar_definition]) ).
tff(f1499,plain,
( ~ path(s,sK37,sK38)
| spl93_28 ),
inference(avatar_component_clause,[],[f1497]) ).
tff(f1500,plain,
~ spl93_28,
inference(avatar_split_clause,[],[f1144,f1497]) ).
tff(f1504,definition,
( spl93_29
<=> ( finite(sK36) = get1(sK32,sK35) ) ),
introduced(definition,[new_symbols(definition,[spl93_29])],[avatar_definition]) ).
tff(f1506,plain,
( ( finite(sK36) = get1(sK32,sK35) )
| ~ spl93_29 ),
inference(avatar_component_clause,[],[f1504]) ).
tff(f1507,plain,
spl93_29,
inference(avatar_split_clause,[],[f738,f1504]) ).
tff(f1537,definition,
( spl93_36
<=> mem1(sK35,vertices) ),
introduced(definition,[new_symbols(definition,[spl93_36])],[avatar_definition]) ).
tff(f1539,plain,
( ~ mem1(sK35,vertices)
| spl93_36 ),
inference(avatar_component_clause,[],[f1537]) ).
tff(f1540,plain,
~ spl93_36,
inference(avatar_split_clause,[],[f1223,f1537]) ).
tff(f1551,definition,
( spl93_39
<=> $less($sum(path_weight(sK37,sK38),weight(sK38,sK35)),sK36) ),
introduced(definition,[new_symbols(definition,[spl93_39])],[avatar_definition]) ).
tff(f1553,plain,
( $less($sum(path_weight(sK37,sK38),weight(sK38,sK35)),sK36)
| ~ spl93_39 ),
inference(avatar_component_clause,[],[f1551]) ).
tff(f1554,plain,
spl93_39,
inference(avatar_split_clause,[],[f736,f1551]) ).
tff(f2021,plain,
( ~ mem2(tuple22(sK27,sK28),sK29)
| ~ spl93_16 ),
inference(superposition,[],[f1089,f1441]) ).
tff(f2023,definition,
( spl93_64
<=> mem2(tuple22(sK27,sK28),sK29) ),
introduced(definition,[new_symbols(definition,[spl93_64])],[avatar_definition]) ).
tff(f2025,plain,
( ~ mem2(tuple22(sK27,sK28),sK29)
| spl93_64 ),
inference(avatar_component_clause,[],[f2023]) ).
tff(f2026,plain,
( ~ spl93_64
| ~ spl93_16 ),
inference(avatar_split_clause,[],[f2021,f1439,f2023]) ).
tff(f2034,plain,
! [X0: vertex] :
( ( sK33(X0) = finite_proj_1(get1(sK32,X0)) )
| ( infinite = get1(sK32,X0) )
| mem1(X0,vertices) ),
inference(superposition,[],[f1018,f1141]) ).
tff(f2037,plain,
( ( finite_proj_1(finite(sK36)) = sK33(sK35) )
| ( infinite = finite(sK36) )
| mem1(sK35,vertices)
| ~ spl93_29 ),
inference(superposition,[],[f2034,f1506]) ).
tff(f2038,plain,
( ( finite_proj_1(finite(sK36)) = sK33(sK35) )
| mem1(sK35,vertices)
| ~ spl93_29 ),
inference(forward_subsumption_resolution,[],[f2037,f874]) ).
tff(f2039,plain,
( ( finite_proj_1(finite(sK36)) = sK33(sK35) )
| ~ spl93_29
| spl93_36 ),
inference(forward_subsumption_resolution,[],[f2038,f1539]) ).
tff(f2040,plain,
( ( sK33(sK35) = sK36 )
| ~ spl93_29
| spl93_36 ),
inference(forward_demodulation,[],[f2039,f1018]) ).
tff(f2042,definition,
( spl93_65
<=> ( sK33(sK35) = sK36 ) ),
introduced(definition,[new_symbols(definition,[spl93_65])],[avatar_definition]) ).
tff(f2044,plain,
( ( sK33(sK35) = sK36 )
| ~ spl93_65 ),
inference(avatar_component_clause,[],[f2042]) ).
tff(f2045,plain,
( spl93_65
| ~ spl93_29
| spl93_36 ),
inference(avatar_split_clause,[],[f2040,f1537,f1504,f2042]) ).
tff(f2589,plain,
( mem2(tuple22(sK38,sK35),sK23)
| ~ spl93_24 ),
inference(resolution,[],[f875,f1477]) ).
tff(f2591,definition,
( spl93_110
<=> mem2(tuple22(sK38,sK35),sK23) ),
introduced(definition,[new_symbols(definition,[spl93_110])],[avatar_definition]) ).
tff(f2593,plain,
( mem2(tuple22(sK38,sK35),sK23)
| ~ spl93_110 ),
inference(avatar_component_clause,[],[f2591]) ).
tff(f2594,plain,
( spl93_110
| ~ spl93_24 ),
inference(avatar_split_clause,[],[f2589,f1475,f2591]) ).
tff(f2770,plain,
( ~ mem2(tuple22(sK38,sK35),sK29)
| ~ spl93_24 ),
inference(resolution,[],[f876,f1477]) ).
tff(f2772,definition,
( spl93_114
<=> mem2(tuple22(sK38,sK35),sK29) ),
introduced(definition,[new_symbols(definition,[spl93_114])],[avatar_definition]) ).
tff(f2774,plain,
( ~ mem2(tuple22(sK38,sK35),sK29)
| spl93_114 ),
inference(avatar_component_clause,[],[f2772]) ).
tff(f2775,plain,
( ~ spl93_114
| ~ spl93_24 ),
inference(avatar_split_clause,[],[f2770,f1475,f2772]) ).
tff(f2793,plain,
! [X2: list_vertex,X0: vertex,X1: vertex] :
( ~ $less($sum(path_weight(X2,X0),weight(X0,X1)),sK33(X1))
| ( infinite = get1(sK32,X1) )
| ~ mem2(tuple22(X0,X1),diff2(sK23,sK25))
| ~ $less(length1(X2),sK20)
| path(s,X2,X0)
| mem1(X1,vertices) ),
inference(resolution,[],[f952,f1133]) ).
tff(f2817,plain,
( ! [X0: list_vertex,X1: vertex] :
( path(s,X0,X1)
| mem1(sK35,vertices)
| ~ mem2(tuple22(X1,sK35),diff2(sK23,sK25))
| ~ $less(length1(X0),sK20)
| ~ $less($sum(path_weight(X0,X1),weight(X1,sK35)),sK36)
| ( infinite = get1(sK32,sK35) ) )
| ~ spl93_65 ),
inference(superposition,[],[f2793,f2044]) ).
tff(f2827,plain,
( ! [X0: list_vertex,X1: vertex] :
( ( infinite = get1(sK32,sK35) )
| ~ $less($sum(path_weight(X0,X1),weight(X1,sK35)),sK36)
| ~ $less(length1(X0),sK20)
| ~ mem2(tuple22(X1,sK35),diff2(sK23,sK25))
| path(s,X0,X1) )
| spl93_36
| ~ spl93_65 ),
inference(forward_subsumption_resolution,[],[f2817,f1539]) ).
tff(f2832,plain,
( ! [X0: list_vertex,X1: vertex] :
( ~ mem2(tuple22(X1,sK35),diff2(sK23,sK25))
| ~ $less($sum(path_weight(X0,X1),weight(X1,sK35)),sK36)
| path(s,X0,X1)
| ~ $less(length1(X0),sK20)
| ( infinite = finite(sK36) ) )
| ~ spl93_29
| spl93_36
| ~ spl93_65 ),
inference(forward_demodulation,[],[f2827,f1506]) ).
tff(f2833,plain,
( ! [X0: list_vertex,X1: vertex] :
( ~ $less($sum(path_weight(X0,X1),weight(X1,sK35)),sK36)
| path(s,X0,X1)
| ~ $less(length1(X0),sK20)
| ~ mem2(tuple22(X1,sK35),diff2(sK23,sK25)) )
| ~ spl93_29
| spl93_36
| ~ spl93_65 ),
inference(forward_subsumption_resolution,[],[f2832,f874]) ).
tff(f2834,plain,
( path(s,sK37,sK38)
| ~ $less(length1(sK37),sK20)
| ~ mem2(tuple22(sK38,sK35),diff2(sK23,sK25))
| ~ spl93_29
| spl93_36
| ~ spl93_39
| ~ spl93_65 ),
inference(resolution,[],[f2833,f1553]) ).
tff(f2852,plain,
( ~ mem2(tuple22(sK38,sK35),diff2(sK23,sK25))
| ~ $less(length1(sK37),sK20)
| spl93_28
| ~ spl93_29
| spl93_36
| ~ spl93_39
| ~ spl93_65 ),
inference(forward_subsumption_resolution,[],[f2834,f1499]) ).
tff(f2858,plain,
( ~ mem2(tuple22(sK38,sK35),diff2(sK23,sK25))
| ~ spl93_19
| spl93_28
| ~ spl93_29
| spl93_36
| ~ spl93_39
| ~ spl93_65 ),
inference(forward_subsumption_resolution,[],[f2852,f1455]) ).
tff(f2860,definition,
( spl93_117
<=> mem2(tuple22(sK38,sK35),diff2(sK23,sK25)) ),
introduced(definition,[new_symbols(definition,[spl93_117])],[avatar_definition]) ).
tff(f2862,plain,
( ~ mem2(tuple22(sK38,sK35),diff2(sK23,sK25))
| spl93_117 ),
inference(avatar_component_clause,[],[f2860]) ).
tff(f2863,plain,
( ~ spl93_117
| ~ spl93_19
| spl93_28
| ~ spl93_29
| spl93_36
| ~ spl93_39
| ~ spl93_65 ),
inference(avatar_split_clause,[],[f2858,f2042,f1551,f1537,f1504,f1497,f1453,f2860]) ).
tff(f3095,plain,
( ~ mem2(tuple22(sK27,sK28),sK25)
| ( add2(tuple22(sK27,sK28),sK29) = sK25 )
| ~ spl93_16 ),
inference(superposition,[],[f701,f1441]) ).
tff(f3101,plain,
( ( add2(tuple22(sK27,sK28),sK29) = sK25 )
| ~ spl93_15
| ~ spl93_16 ),
inference(forward_subsumption_resolution,[],[f3095,f1436]) ).
tff(f3103,definition,
( spl93_124
<=> ( add2(tuple22(sK27,sK28),sK29) = sK25 ) ),
introduced(definition,[new_symbols(definition,[spl93_124])],[avatar_definition]) ).
tff(f3105,plain,
( ( add2(tuple22(sK27,sK28),sK29) = sK25 )
| ~ spl93_124 ),
inference(avatar_component_clause,[],[f3103]) ).
tff(f3106,plain,
( spl93_124
| ~ spl93_15
| ~ spl93_16 ),
inference(avatar_split_clause,[],[f3101,f1439,f1434,f3103]) ).
tff(f3247,plain,
( ~ mem2(tuple22(sK38,sK35),sK23)
| mem2(tuple22(sK38,sK35),sK25)
| spl93_117 ),
inference(resolution,[],[f877,f2862]) ).
tff(f3261,plain,
( mem2(tuple22(sK38,sK35),sK25)
| ~ spl93_110
| spl93_117 ),
inference(forward_subsumption_resolution,[],[f3247,f2593]) ).
tff(f3272,definition,
( spl93_128
<=> mem2(tuple22(sK38,sK35),sK25) ),
introduced(definition,[new_symbols(definition,[spl93_128])],[avatar_definition]) ).
tff(f3274,plain,
( mem2(tuple22(sK38,sK35),sK25)
| ~ spl93_128 ),
inference(avatar_component_clause,[],[f3272]) ).
tff(f3275,plain,
( spl93_128
| ~ spl93_110
| spl93_117 ),
inference(avatar_split_clause,[],[f3261,f2860,f2591,f3272]) ).
tff(f3334,plain,
( ! [X0: lpvertexcm_vertexrp] :
( ( tuple22(sK27,sK28) = X0 )
| ~ mem2(X0,sK25)
| mem2(X0,sK29) )
| ~ spl93_124 ),
inference(superposition,[],[f953,f3105]) ).
tff(f3335,plain,
( ! [X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( mem2(X1,sK29)
| mem2(X0,sK29)
| ~ mem2(X1,sK25)
| ~ mem2(X0,sK25)
| ( X0 = X1 ) )
| ~ spl93_124 ),
inference(superposition,[],[f3334,f3334]) ).
tff(f3422,plain,
( ! [X0: lpvertexcm_vertexrp] :
( ~ mem2(tuple22(sK38,sK35),sK25)
| ~ mem2(X0,sK25)
| ( tuple22(sK38,sK35) = X0 )
| mem2(X0,sK29) )
| spl93_114
| ~ spl93_124 ),
inference(resolution,[],[f3335,f2774]) ).
tff(f3425,plain,
( ! [X0: lpvertexcm_vertexrp] :
( ( tuple22(sK38,sK35) = X0 )
| ~ mem2(X0,sK25)
| mem2(X0,sK29) )
| spl93_114
| ~ spl93_124
| ~ spl93_128 ),
inference(forward_subsumption_resolution,[],[f3422,f3274]) ).
tff(f3438,plain,
( ! [X0: lpvertexcm_vertexrp,X1: list_vertex] :
( mem2(X0,sK29)
| ( infinite = get1(sK32,sK35) )
| ~ mem2(X0,sK25)
| ~ $less($sum(path_weight(X1,sK38),weight(sK38,sK35)),sK33(sK35))
| ~ mem2(X0,add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| ~ $less(length1(X1),sK20)
| mem1(sK35,vertices)
| path(s,X1,sK38) )
| spl93_114
| ~ spl93_124
| ~ spl93_128 ),
inference(superposition,[],[f1133,f3425]) ).
tff(f3475,plain,
( ! [X0: lpvertexcm_vertexrp,X1: list_vertex] :
( ( infinite = get1(sK32,sK35) )
| ~ mem2(X0,add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| mem2(X0,sK29)
| ~ $less(length1(X1),sK20)
| ~ $less($sum(path_weight(X1,sK38),weight(sK38,sK35)),sK33(sK35))
| ~ mem2(X0,sK25)
| path(s,X1,sK38) )
| spl93_36
| spl93_114
| ~ spl93_124
| ~ spl93_128 ),
inference(forward_subsumption_resolution,[],[f3438,f1539]) ).
tff(f3481,definition,
( spl93_134
<=> ! [X0: lpvertexcm_vertexrp] :
( mem2(X0,sK29)
| ~ mem2(X0,sK25)
| ~ mem2(X0,add2(tuple22(sK27,sK28),diff2(sK23,sK25))) ) ),
introduced(definition,[new_symbols(definition,[spl93_134])],[avatar_definition]) ).
tff(f3482,plain,
( ! [X0: lpvertexcm_vertexrp] :
( ~ mem2(X0,add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| ~ mem2(X0,sK25)
| mem2(X0,sK29) )
| ~ spl93_134 ),
inference(avatar_component_clause,[],[f3481]) ).
tff(f3491,definition,
( spl93_137
<=> ! [X2: list_vertex] :
( ~ $less(length1(X2),sK20)
| path(s,X2,sK38)
| ~ $less($sum(path_weight(X2,sK38),weight(sK38,sK35)),sK33(sK35)) ) ),
introduced(definition,[new_symbols(definition,[spl93_137])],[avatar_definition]) ).
tff(f3492,plain,
( ! [X2: list_vertex] :
( ~ $less($sum(path_weight(X2,sK38),weight(sK38,sK35)),sK33(sK35))
| ~ $less(length1(X2),sK20)
| path(s,X2,sK38) )
| ~ spl93_137 ),
inference(avatar_component_clause,[],[f3491]) ).
tff(f3494,plain,
( ! [X0: lpvertexcm_vertexrp,X1: list_vertex] :
( ~ $less($sum(path_weight(X1,sK38),weight(sK38,sK35)),sK33(sK35))
| ~ mem2(X0,sK25)
| ( infinite = finite(sK36) )
| mem2(X0,sK29)
| ~ mem2(X0,add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| ~ $less(length1(X1),sK20)
| path(s,X1,sK38) )
| ~ spl93_29
| spl93_36
| spl93_114
| ~ spl93_124
| ~ spl93_128 ),
inference(forward_demodulation,[],[f3475,f1506]) ).
tff(f3506,plain,
( ! [X0: lpvertexcm_vertexrp,X1: list_vertex] :
( mem2(X0,sK29)
| ~ $less(length1(X1),sK20)
| ~ mem2(X0,add2(tuple22(sK27,sK28),diff2(sK23,sK25)))
| ~ mem2(X0,sK25)
| ~ $less($sum(path_weight(X1,sK38),weight(sK38,sK35)),sK33(sK35))
| path(s,X1,sK38) )
| ~ spl93_29
| spl93_36
| spl93_114
| ~ spl93_124
| ~ spl93_128 ),
inference(forward_subsumption_resolution,[],[f3494,f874]) ).
tff(f3512,plain,
( spl93_137
| spl93_134
| ~ spl93_29
| spl93_36
| spl93_114
| ~ spl93_124
| ~ spl93_128 ),
inference(avatar_split_clause,[],[f3506,f3272,f3103,f2772,f1537,f1504,f3481,f3491]) ).
tff(f3524,plain,
( ~ mem2(tuple22(sK27,sK28),sK25)
| mem2(tuple22(sK27,sK28),sK29)
| ~ spl93_134 ),
inference(resolution,[],[f3482,f1085]) ).
tff(f3527,plain,
( mem2(tuple22(sK27,sK28),sK29)
| ~ spl93_15
| ~ spl93_134 ),
inference(forward_subsumption_resolution,[],[f3524,f1436]) ).
tff(f3528,plain,
( $false
| ~ spl93_15
| spl93_64
| ~ spl93_134 ),
inference(forward_subsumption_resolution,[],[f3527,f2025]) ).
tff(f3529,plain,
( ~ spl93_15
| spl93_64
| ~ spl93_134 ),
inference(avatar_contradiction_clause,[],[f3528]) ).
tff(f3710,plain,
( ! [X0: list_vertex] :
( ~ $less($sum(path_weight(X0,sK38),weight(sK38,sK35)),sK36)
| path(s,X0,sK38)
| ~ $less(length1(X0),sK20) )
| ~ spl93_65
| ~ spl93_137 ),
inference(superposition,[],[f3492,f2044]) ).
tff(f3814,plain,
( path(s,sK37,sK38)
| ~ $less(length1(sK37),sK20)
| ~ spl93_39
| ~ spl93_65
| ~ spl93_137 ),
inference(resolution,[],[f3710,f1553]) ).
tff(f3825,plain,
( ~ $less(length1(sK37),sK20)
| spl93_28
| ~ spl93_39
| ~ spl93_65
| ~ spl93_137 ),
inference(forward_subsumption_resolution,[],[f3814,f1499]) ).
tff(f3828,plain,
( $false
| ~ spl93_19
| spl93_28
| ~ spl93_39
| ~ spl93_65
| ~ spl93_137 ),
inference(forward_subsumption_resolution,[],[f3825,f1455]) ).
tff(f3829,plain,
( ~ spl93_19
| spl93_28
| ~ spl93_39
| ~ spl93_65
| ~ spl93_137 ),
inference(avatar_contradiction_clause,[],[f3828]) ).
tff(f3830,plain,
$false,
inference(avatar_smt_refutation,[],[f3829,f3529,f3512,f3275,f3106,f2863,f2775,f2594,f2045,f2026,f1554,f1540,f1507,f1500,f1478,f1456,f1442,f1437]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW577_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n001.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 14:25:48 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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
% 4.62/1.37 % (378462)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.62/1.37 % (378495)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3923316402:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.62/1.37 % (378495)Instruction limit reached!
% 4.62/1.37 % (378495)------------------------------
% 4.62/1.37 % (378495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.62/1.37 % (378495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.62/1.37 % (378495)CaDiCaL version: 2.1.3
% 4.62/1.37 % (378495)Termination reason: Instruction limit
% 4.62/1.37 % (378495)Termination phase: Saturation
% 4.62/1.37 % (378495)Time elapsed: 0.044 s
% 4.62/1.37 % (378495)Peak memory usage: 113 MB
% 4.62/1.37 % (378495)Instructions burned: 33 (million)
% 4.62/1.37 % (378489)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2766696310:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.62/1.37 % (378494)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3790523181:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.62/1.37 % (378493)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1271041862:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.62/1.37 % (378492)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=109264489:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.62/1.37 % (378490)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=329670913:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.62/1.37 % (378491)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2987845084:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.62/1.37 % (378493)Instruction limit reached!
% 4.62/1.37 % (378493)------------------------------
% 4.62/1.37 % (378493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.62/1.37 % (378493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.62/1.37 % (378493)CaDiCaL version: 2.1.3
% 4.62/1.37 % (378493)Termination reason: Instruction limit
% 4.62/1.37 % (378493)Termination phase: Property scanning
% 4.62/1.37 % (378493)Time elapsed: 0.004 s
% 4.62/1.37 % (378493)Peak memory usage: 85 MB
% 4.62/1.37 % (378493)Instructions burned: 4 (million)
% 4.62/1.37 % (378492)Instruction limit reached!
% 4.62/1.37 % (378492)------------------------------
% 4.62/1.37 % (378492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.62/1.37 % (378492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.62/1.37 % (378492)CaDiCaL version: 2.1.3
% 4.62/1.37 % (378492)Termination reason: Instruction limit
% 4.62/1.37 % (378492)Termination phase: Preprocessing 1
% 4.62/1.37 % (378492)Time elapsed: 0.008 s
% 4.62/1.37 % (378492)Peak memory usage: 86 MB
% 4.62/1.37 % (378492)Instructions burned: 7 (million)
% 4.62/1.37 % (378489)Instruction limit reached!
% 4.62/1.37 % (378489)------------------------------
% 4.62/1.37 % (378489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.62/1.37 % (378489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.62/1.37 % (378489)CaDiCaL version: 2.1.3
% 4.62/1.37 % (378489)Termination reason: Instruction limit
% 4.62/1.37 % (378489)Termination phase: Preprocessing 3
% 4.62/1.37 % (378489)Time elapsed: 0.012 s
% 4.62/1.37 % (378489)Peak memory usage: 86 MB
% 4.62/1.37 % (378489)Instructions burned: 12 (million)
% 4.62/1.37 % (378494)Instruction limit reached!
% 4.62/1.37 % (378494)------------------------------
% 4.62/1.37 % (378494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.62/1.37 % (378494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.62/1.37 % (378494)CaDiCaL version: 2.1.3
% 4.62/1.37 % (378494)Termination reason: Instruction limit
% 4.62/1.37 % (378494)Termination phase: Saturation
% 4.62/1.37 % (378494)Time elapsed: 0.079 s
% 4.62/1.37 % (378494)Peak memory usage: 116 MB
% 4.62/1.37 % (378494)Instructions burned: 46 (million)
% 4.62/1.37 % (378506)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=4116148805:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.62/1.37 % (378504)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=3421214315:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 5.88/1.58 % (378497)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1200396635:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.88/1.58 % (378506)Instruction limit reached!
% 5.88/1.58 % (378506)------------------------------
% 5.88/1.58 % (378506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.58 % (378506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.58 % (378506)CaDiCaL version: 2.1.3
% 5.88/1.58 % (378506)Termination reason: Instruction limit
% 5.88/1.58 % (378506)Termination phase: Saturation
% 5.88/1.58 % (378506)Time elapsed: 0.013 s
% 5.88/1.58 % (378506)Peak memory usage: 89 MB
% 5.88/1.58 % (378506)Instructions burned: 24 (million)
% 5.88/1.58 % (378497)Instruction limit reached!
% 5.88/1.58 % (378497)------------------------------
% 5.88/1.58 % (378497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.58 % (378497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.58 % (378497)CaDiCaL version: 2.1.3
% 5.88/1.58 % (378497)Termination reason: Instruction limit
% 5.88/1.58 % (378497)Termination phase: Property scanning
% 5.88/1.58 % (378497)Time elapsed: 0.015 s
% 5.88/1.58 % (378497)Peak memory usage: 86 MB
% 5.88/1.58 % (378497)Instructions burned: 14 (million)
% 5.88/1.58 % (378504)Instruction limit reached!
% 5.88/1.58 % (378504)------------------------------
% 5.88/1.58 % (378504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.58 % (378504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.58 % (378504)CaDiCaL version: 2.1.3
% 5.88/1.58 % (378504)Termination reason: Instruction limit
% 5.88/1.58 % (378504)Termination phase: Saturation
% 5.88/1.58 % (378504)Time elapsed: 0.017 s
% 5.88/1.58 % (378504)Peak memory usage: 89 MB
% 5.88/1.58 % (378504)Instructions burned: 29 (million)
% 5.88/1.58 % (378505)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1734015803:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.88/1.58 % (378505)Instruction limit reached!
% 5.88/1.58 % (378505)------------------------------
% 5.88/1.58 % (378505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.58 % (378505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.58 % (378505)CaDiCaL version: 2.1.3
% 5.88/1.58 % (378505)Termination reason: Instruction limit
% 5.88/1.58 % (378505)Termination phase: Property scanning
% 5.88/1.58 % (378505)Time elapsed: 0.017 s
% 5.88/1.58 % (378505)Peak memory usage: 87 MB
% 5.88/1.58 % (378505)Instructions burned: 16 (million)
% 5.88/1.58 % (378491)Instruction limit reached!
% 5.88/1.58 % (378491)------------------------------
% 5.88/1.58 % (378491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.58 % (378491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.58 % (378491)CaDiCaL version: 2.1.3
% 5.88/1.58 % (378491)Termination reason: Instruction limit
% 5.88/1.58 % (378491)Termination phase: Saturation
% 5.88/1.58 % (378491)Time elapsed: 0.252 s
% 5.88/1.58 % (378491)Peak memory usage: 119 MB
% 5.88/1.58 % (378491)Instructions burned: 201 (million)
% 5.88/1.58 % (378511)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=2529689337:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 5.88/1.58 % (378522)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=818100129:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.88/1.58 % (378522)Instruction limit reached!
% 5.88/1.58 % (378522)------------------------------
% 5.88/1.58 % (378522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.88/1.58 % (378522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.88/1.58 % (378522)CaDiCaL version: 2.1.3
% 5.88/1.58 % (378522)Termination reason: Instruction limit
% 5.88/1.58 % (378522)Termination phase: Property scanning
% 5.88/1.58 % (378522)Time elapsed: 0.002 s
% 5.88/1.58 % (378522)Peak memory usage: 85 MB
% 5.88/1.58 % (378522)Instructions burned: 3 (million)
% 5.88/1.58 % (378511)Instruction limit reached!
% 5.88/1.58 % (378511)------------------------------
% 5.88/1.58 % (378511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.81 % (378511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.81 % (378511)CaDiCaL version: 2.1.3
% 7.60/1.81 % (378511)Termination reason: Instruction limit
% 7.60/1.81 % (378511)Termination phase: Saturation
% 7.60/1.81 % (378511)Time elapsed: 0.028 s
% 7.60/1.81 % (378511)Peak memory usage: 89 MB
% 7.60/1.81 % (378511)Instructions burned: 27 (million)
% 7.60/1.81 % (378490)Instruction limit reached!
% 7.60/1.81 % (378490)------------------------------
% 7.60/1.81 % (378490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.81 % (378490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.81 % (378490)CaDiCaL version: 2.1.3
% 7.60/1.81 % (378490)Termination reason: Instruction limit
% 7.60/1.81 % (378490)Termination phase: Saturation
% 7.60/1.81 % (378490)Time elapsed: 0.349 s
% 7.60/1.81 % (378490)Peak memory usage: 118 MB
% 7.60/1.81 % (378490)Instructions burned: 307 (million)
% 7.60/1.81 % (378521)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3647341111:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 7.60/1.81 % (378524)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1532926376:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 7.60/1.81 % (378527)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3965337235:i=4:ep=RST:ins=2:rtra=on_2995 on theBenchmark for (2995ds/4Mi)
% 7.60/1.81 % (378527)Instruction limit reached!
% 7.60/1.81 % (378527)------------------------------
% 7.60/1.81 % (378527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.81 % (378527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.81 % (378527)CaDiCaL version: 2.1.3
% 7.60/1.81 % (378527)Termination reason: Instruction limit
% 7.60/1.81 % (378527)Termination phase: Property scanning
% 7.60/1.81 % (378527)Time elapsed: 0.004 s
% 7.60/1.81 % (378527)Peak memory usage: 85 MB
% 7.60/1.81 % (378527)Instructions burned: 4 (million)
% 7.60/1.81 % (378521)Instruction limit reached!
% 7.60/1.81 % (378521)------------------------------
% 7.60/1.81 % (378521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.81 % (378521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.81 % (378521)CaDiCaL version: 2.1.3
% 7.60/1.81 % (378521)Termination reason: Instruction limit
% 7.60/1.81 % (378521)Termination phase: Saturation
% 7.60/1.81 % (378521)Time elapsed: 0.087 s
% 7.60/1.81 % (378521)Peak memory usage: 90 MB
% 7.60/1.81 % (378521)Instructions burned: 86 (million)
% 7.60/1.81 % (378528)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1509857154:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 7.60/1.81 % (378531)lrs+10_1_thi=all:si=on:fd=off:random_seed=419834311:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 7.60/1.81 % (378531)Instruction limit reached!
% 7.60/1.81 % (378531)------------------------------
% 7.60/1.81 % (378531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.81 % (378531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.81 % (378531)CaDiCaL version: 2.1.3
% 7.60/1.81 % (378531)Termination reason: Instruction limit
% 7.60/1.81 % (378531)Termination phase: Saturation
% 7.60/1.81 % (378531)Time elapsed: 0.044 s
% 7.60/1.81 % (378531)Peak memory usage: 116 MB
% 7.60/1.81 % (378531)Instructions burned: 53 (million)
% 7.60/1.81 % (378532)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=1906682013:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 7.60/1.81 % (378533)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1199107198:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 7.60/1.81 % (378533)Instruction limit reached!
% 7.60/1.81 % (378533)------------------------------
% 7.60/1.81 % (378533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.60/1.81 % (378533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.60/1.81 % (378533)CaDiCaL version: 2.1.3
% 7.60/1.81 % (378533)Termination reason: Instruction limit
% 7.60/1.81 % (378533)Termination phase: Property scanning
% 7.60/1.81 % (378533)Time elapsed: 0.003 s
% 7.60/1.81 % (378533)Peak memory usage: 85 MB
% 7.60/1.81 % (378533)Instructions burned: 3 (million)
% 7.60/1.81 % (378532)Instruction limit reached!
% 10.97/2.14 % (378532)------------------------------
% 10.97/2.14 % (378532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/2.14 % (378532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/2.14 % (378532)CaDiCaL version: 2.1.3
% 10.97/2.14 % (378532)Termination reason: Instruction limit
% 10.97/2.14 % (378532)Termination phase: Preprocessing 1
% 10.97/2.14 % (378532)Time elapsed: 0.008 s
% 10.97/2.14 % (378532)Peak memory usage: 86 MB
% 10.97/2.14 % (378532)Instructions burned: 9 (million)
% 10.97/2.14 % (378537)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1059335449:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 10.97/2.14 % (378537)Instruction limit reached!
% 10.97/2.14 % (378537)------------------------------
% 10.97/2.14 % (378537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/2.14 % (378537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/2.14 % (378537)CaDiCaL version: 2.1.3
% 10.97/2.14 % (378537)Termination reason: Instruction limit
% 10.97/2.14 % (378537)Termination phase: Preprocessing 1
% 10.97/2.14 % (378537)Time elapsed: 0.006 s
% 10.97/2.14 % (378537)Peak memory usage: 86 MB
% 10.97/2.14 % (378537)Instructions burned: 6 (million)
% 10.97/2.14 % (378528)Instruction limit reached!
% 10.97/2.14 % (378528)------------------------------
% 10.97/2.14 % (378528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/2.14 % (378528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/2.14 % (378528)CaDiCaL version: 2.1.3
% 10.97/2.14 % (378528)Termination reason: Instruction limit
% 10.97/2.14 % (378528)Termination phase: Saturation
% 10.97/2.14 % (378528)Time elapsed: 0.126 s
% 10.97/2.14 % (378528)Peak memory usage: 135 MB
% 10.97/2.14 % (378528)Instructions burned: 66 (million)
% 10.97/2.14 % (378524)Instruction limit reached!
% 10.97/2.14 % (378524)------------------------------
% 10.97/2.14 % (378524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/2.14 % (378524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/2.14 % (378524)CaDiCaL version: 2.1.3
% 10.97/2.14 % (378524)Termination reason: Instruction limit
% 10.97/2.14 % (378524)Termination phase: Saturation
% 10.97/2.14 % (378524)Time elapsed: 0.209 s
% 10.97/2.14 % (378524)Peak memory usage: 92 MB
% 10.97/2.14 % (378524)Instructions burned: 182 (million)
% 10.97/2.14 % (378540)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1935656608:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 10.97/2.14 % (378543)dis+10_1_si=on:random_seed=1712625098:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.97/2.14 % (378543)Instruction limit reached!
% 10.97/2.14 % (378543)------------------------------
% 10.97/2.14 % (378543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/2.14 % (378543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/2.14 % (378543)CaDiCaL version: 2.1.3
% 10.97/2.14 % (378543)Termination reason: Instruction limit
% 10.97/2.14 % (378543)Termination phase: Preprocessing 3
% 10.97/2.14 % (378543)Time elapsed: 0.011 s
% 10.97/2.14 % (378543)Peak memory usage: 86 MB
% 10.97/2.14 % (378543)Instructions burned: 10 (million)
% 10.97/2.14 % (378548)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1800905389: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_2992 on theBenchmark for (2992ds/35Mi)
% 10.97/2.14 % (378548)Instruction limit reached!
% 10.97/2.14 % (378548)------------------------------
% 10.97/2.14 % (378548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.97/2.14 % (378548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.97/2.14 % (378548)CaDiCaL version: 2.1.3
% 10.97/2.14 % (378548)Termination reason: Instruction limit
% 10.97/2.14 % (378548)Termination phase: Saturation
% 10.97/2.14 % (378548)Time elapsed: 0.020 s
% 10.97/2.14 % (378548)Peak memory usage: 90 MB
% 10.97/2.14 % (378548)Instructions burned: 35 (million)
% 10.97/2.14 % (378547)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=1659330649:i=26:canc=cautious:av=off:rtra=on_2992 on theBenchmark for (2992ds/26Mi)
% 10.97/2.14 % (378550)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1118635624:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2991 on theBenchmark for (2991ds/8Mi)
% 10.97/2.14 % (378550)Instruction limit reached!
% 12.20/2.54 % (378550)------------------------------
% 12.20/2.54 % (378550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.20/2.54 % (378550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.20/2.54 % (378550)CaDiCaL version: 2.1.3
% 12.20/2.54 % (378550)Termination reason: Instruction limit
% 12.20/2.54 % (378550)Termination phase: Preprocessing 1
% 12.20/2.54 % (378550)Time elapsed: 0.008 s
% 12.20/2.54 % (378550)Peak memory usage: 86 MB
% 12.20/2.54 % (378550)Instructions burned: 8 (million)
% 12.20/2.54 % (378549)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=154416926:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 12.20/2.54 % (378549)Instruction limit reached!
% 12.20/2.54 % (378549)------------------------------
% 12.20/2.54 % (378549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.20/2.54 % (378549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.20/2.54 % (378549)CaDiCaL version: 2.1.3
% 12.20/2.54 % (378549)Termination reason: Instruction limit
% 12.20/2.54 % (378549)Termination phase: Property scanning
% 12.20/2.54 % (378549)Time elapsed: 0.003 s
% 12.20/2.54 % (378549)Peak memory usage: 85 MB
% 12.20/2.54 % (378549)Instructions burned: 2 (million)
% 12.20/2.54 % (378547)Instruction limit reached!
% 12.20/2.54 % (378547)------------------------------
% 12.20/2.54 % (378547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.20/2.54 % (378547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.20/2.54 % (378547)CaDiCaL version: 2.1.3
% 12.20/2.54 % (378547)Termination reason: Instruction limit
% 12.20/2.54 % (378547)Termination phase: Saturation
% 12.20/2.54 % (378547)Time elapsed: 0.026 s
% 12.20/2.54 % (378547)Peak memory usage: 89 MB
% 12.20/2.54 % (378547)Instructions burned: 26 (million)
% 12.20/2.54 % (378551)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1379704914:i=370:ep=RS:fsr=off:rtra=on_2991 on theBenchmark for (2991ds/370Mi)
% 12.20/2.54 % (378540)Instruction limit reached!
% 12.20/2.54 % (378540)------------------------------
% 12.20/2.54 % (378540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.20/2.54 % (378540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.20/2.54 % (378540)CaDiCaL version: 2.1.3
% 12.20/2.54 % (378540)Termination reason: Instruction limit
% 12.20/2.54 % (378540)Termination phase: Saturation
% 12.20/2.54 % (378540)Time elapsed: 0.173 s
% 12.20/2.54 % (378540)Peak memory usage: 118 MB
% 12.20/2.54 % (378540)Instructions burned: 127 (million)
% 12.20/2.54 % (378556)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3316146725:i=226:rtra=on:gtg=position:ss=axioms_2990 on theBenchmark for (2990ds/226Mi)
% 12.20/2.54 % (378560)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4076402280:i=10:rtra=on_2990 on theBenchmark for (2990ds/10Mi)
% 12.20/2.54 % (378555)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3056380907:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/13Mi)
% 12.20/2.54 % (378560)Instruction limit reached!
% 12.20/2.54 % (378560)------------------------------
% 12.20/2.54 % (378560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.20/2.54 % (378560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.20/2.54 % (378560)CaDiCaL version: 2.1.3
% 12.20/2.54 % (378560)Termination reason: Instruction limit
% 12.20/2.54 % (378560)Termination phase: Preprocessing 3
% 12.20/2.54 % (378560)Time elapsed: 0.008 s
% 12.20/2.54 % (378560)Peak memory usage: 86 MB
% 12.20/2.54 % (378560)Instructions burned: 11 (million)
% 12.20/2.54 % (378555)Instruction limit reached!
% 12.20/2.54 % (378555)------------------------------
% 12.20/2.54 % (378555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.20/2.54 % (378555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.20/2.54 % (378555)CaDiCaL version: 2.1.3
% 12.20/2.54 % (378555)Termination reason: Instruction limit
% 12.20/2.54 % (378555)Termination phase: Naming
% 12.20/2.54 % (378555)Time elapsed: 0.013 s
% 12.20/2.54 % (378555)Peak memory usage: 86 MB
% 12.20/2.54 % (378555)Instructions burned: 13 (million)
% 12.20/2.54 % (378561)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2752099451:i=71:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/71Mi)
% 12.20/2.54 % (378562)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=501246377:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2989 on theBenchmark for (2989ds/75Mi)
% 14.00/2.86 % (378556)Instruction limit reached!
% 14.00/2.86 % (378556)------------------------------
% 14.00/2.86 % (378556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.86 % (378556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.86 % (378556)CaDiCaL version: 2.1.3
% 14.00/2.86 % (378556)Termination reason: Instruction limit
% 14.00/2.86 % (378556)Termination phase: Saturation
% 14.00/2.86 % (378556)Time elapsed: 0.148 s
% 14.00/2.86 % (378556)Peak memory usage: 118 MB
% 14.00/2.86 % (378556)Instructions burned: 227 (million)
% 14.00/2.86 % (378568)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1834057060:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/130Mi)
% 14.00/2.86 % (378564)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=4209413832:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2989 on theBenchmark for (2989ds/294Mi)
% 14.00/2.86 % (378562)Instruction limit reached!
% 14.00/2.86 % (378562)------------------------------
% 14.00/2.86 % (378562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.86 % (378562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.86 % (378562)CaDiCaL version: 2.1.3
% 14.00/2.86 % (378562)Termination reason: Instruction limit
% 14.00/2.86 % (378562)Termination phase: Saturation
% 14.00/2.86 % (378562)Time elapsed: 0.083 s
% 14.00/2.86 % (378562)Peak memory usage: 91 MB
% 14.00/2.86 % (378562)Instructions burned: 75 (million)
% 14.00/2.86 % (378561)Instruction limit reached!
% 14.00/2.86 % (378561)------------------------------
% 14.00/2.86 % (378561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.86 % (378561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.86 % (378561)CaDiCaL version: 2.1.3
% 14.00/2.86 % (378561)Termination reason: Instruction limit
% 14.00/2.86 % (378561)Termination phase: Saturation
% 14.00/2.86 % (378561)Time elapsed: 0.129 s
% 14.00/2.86 % (378561)Peak memory usage: 134 MB
% 14.00/2.86 % (378561)Instructions burned: 71 (million)
% 14.00/2.86 % (378569)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=241883009:i=131:rtra=on_2988 on theBenchmark for (2988ds/131Mi)
% 14.00/2.86 % (378568)Instruction limit reached!
% 14.00/2.86 % (378568)------------------------------
% 14.00/2.86 % (378568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.86 % (378568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.86 % (378568)CaDiCaL version: 2.1.3
% 14.00/2.86 % (378568)Termination reason: Instruction limit
% 14.00/2.86 % (378568)Termination phase: Saturation
% 14.00/2.86 % (378568)Time elapsed: 0.132 s
% 14.00/2.86 % (378568)Peak memory usage: 117 MB
% 14.00/2.86 % (378568)Instructions burned: 131 (million)
% 14.00/2.86 % (378551)Instruction limit reached!
% 14.00/2.86 % (378551)------------------------------
% 14.00/2.86 % (378551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.86 % (378551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.00/2.86 % (378551)CaDiCaL version: 2.1.3
% 14.00/2.86 % (378551)Termination reason: Instruction limit
% 14.00/2.86 % (378551)Termination phase: Saturation
% 14.00/2.86 % (378551)Time elapsed: 0.385 s
% 14.00/2.86 % (378551)Peak memory usage: 93 MB
% 14.00/2.86 % (378551)Instructions burned: 370 (million)
% 14.00/2.86 % (378572)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=108166876:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2987 on theBenchmark for (2987ds/40Mi)
% 14.00/2.86 % (378578)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=670216257:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2986 on theBenchmark for (2986ds/598Mi)
% 14.00/2.86 % (378577)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3759862139:i=307:rtra=on:gtg=exists_top_2986 on theBenchmark for (2986ds/307Mi)
% 14.00/2.86 % (378572)Instruction limit reached!
% 14.00/2.86 % (378572)------------------------------
% 14.00/2.86 % (378572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.00/2.86 % (378572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378572)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378572)Termination reason: Instruction limit
% 19.17/3.36 % (378572)Termination phase: Saturation
% 19.17/3.36 % (378572)Time elapsed: 0.093 s
% 19.17/3.36 % (378572)Peak memory usage: 130 MB
% 19.17/3.36 % (378572)Instructions burned: 40 (million)
% 19.17/3.36 % (378569)Instruction limit reached!
% 19.17/3.36 % (378569)------------------------------
% 19.17/3.36 % (378569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.17/3.36 % (378569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378569)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378569)Termination reason: Instruction limit
% 19.17/3.36 % (378569)Termination phase: Saturation
% 19.17/3.36 % (378569)Time elapsed: 0.201 s
% 19.17/3.36 % (378569)Peak memory usage: 134 MB
% 19.17/3.36 % (378569)Instructions burned: 131 (million)
% 19.17/3.36 % (378564)Instruction limit reached!
% 19.17/3.36 % (378564)------------------------------
% 19.17/3.36 % (378564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.17/3.36 % (378564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378564)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378564)Termination reason: Instruction limit
% 19.17/3.36 % (378564)Termination phase: Saturation
% 19.17/3.36 % (378564)Time elapsed: 0.342 s
% 19.17/3.36 % (378564)Peak memory usage: 92 MB
% 19.17/3.36 % (378564)Instructions burned: 294 (million)
% 19.17/3.36 % (378580)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3435960656:i=131:canc=cautious:fsr=off:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 19.17/3.36 % (378581)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=2428476817:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2985 on theBenchmark for (2985ds/259Mi)
% 19.17/3.36 % (378585)dis+10_1_si=on:random_seed=3427405349:s2a=on:i=1000:rtra=on:gtg=exists_all_2984 on theBenchmark for (2984ds/1000Mi)
% 19.17/3.36 % (378586)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2337994042:i=383:fsr=off:rtra=on:ev=force_2984 on theBenchmark for (2984ds/383Mi)
% 19.17/3.36 % (378580)Instruction limit reached!
% 19.17/3.36 % (378580)------------------------------
% 19.17/3.36 % (378580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.17/3.36 % (378580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378580)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378580)Termination reason: Instruction limit
% 19.17/3.36 % (378580)Termination phase: Saturation
% 19.17/3.36 % (378580)Time elapsed: 0.165 s
% 19.17/3.36 % (378580)Peak memory usage: 118 MB
% 19.17/3.36 % (378580)Instructions burned: 132 (million)
% 19.17/3.36 % (378587)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4201077563:i=141:doe=on:rtra=on_2983 on theBenchmark for (2983ds/141Mi)
% 19.17/3.36 % (378578)Instruction limit reached!
% 19.17/3.36 % (378578)------------------------------
% 19.17/3.36 % (378578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.17/3.36 % (378578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378578)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378578)Termination reason: Instruction limit
% 19.17/3.36 % (378578)Termination phase: Saturation
% 19.17/3.36 % (378578)Time elapsed: 0.364 s
% 19.17/3.36 % (378578)Peak memory usage: 138 MB
% 19.17/3.36 % (378578)Instructions burned: 599 (million)
% 19.17/3.36 % (378577)Instruction limit reached!
% 19.17/3.36 % (378577)------------------------------
% 19.17/3.36 % (378577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.17/3.36 % (378577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378577)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378577)Termination reason: Instruction limit
% 19.17/3.36 % (378577)Termination phase: Saturation
% 19.17/3.36 % (378577)Time elapsed: 0.332 s
% 19.17/3.36 % (378577)Peak memory usage: 93 MB
% 19.17/3.36 % (378577)Instructions burned: 307 (million)
% 19.17/3.36 % (378581)Instruction limit reached!
% 19.17/3.36 % (378581)------------------------------
% 19.17/3.36 % (378581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.17/3.36 % (378581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.17/3.36 % (378581)CaDiCaL version: 2.1.3
% 19.17/3.36 % (378581)Termination reason: Instruction limit
% 19.17/3.36 % (378581)Termination phase: Saturation
% 19.17/3.36 % (378581)Time elapsed: 0.303 s
% 19.41/3.73 % (378581)Peak memory usage: 118 MB
% 19.41/3.73 % (378581)Instructions burned: 260 (million)
% 19.41/3.73 % (378587)Instruction limit reached!
% 19.41/3.73 % (378587)------------------------------
% 19.41/3.73 % (378587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378587)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378587)Termination reason: Instruction limit
% 19.41/3.73 % (378587)Termination phase: Saturation
% 19.41/3.73 % (378587)Time elapsed: 0.165 s
% 19.41/3.73 % (378587)Peak memory usage: 91 MB
% 19.41/3.73 % (378587)Instructions burned: 141 (million)
% 19.41/3.73 % (378595)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=693278432:s2a=on:i=128:s2at=5:ins=3:rtra=on_2981 on theBenchmark for (2981ds/128Mi)
% 19.41/3.73 % (378593)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2909478705:i=65:nm=16:rtra=on_2981 on theBenchmark for (2981ds/65Mi)
% 19.41/3.73 % (378594)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=636256655:i=121:nm=16:rtra=on_2981 on theBenchmark for (2981ds/121Mi)
% 19.41/3.73 % (378595)Instruction limit reached!
% 19.41/3.73 % (378595)------------------------------
% 19.41/3.73 % (378595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378595)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378595)Termination reason: Instruction limit
% 19.41/3.73 % (378595)Termination phase: Saturation
% 19.41/3.73 % (378595)Time elapsed: 0.092 s
% 19.41/3.73 % (378595)Peak memory usage: 118 MB
% 19.41/3.73 % (378595)Instructions burned: 129 (million)
% 19.41/3.73 % (378593)Instruction limit reached!
% 19.41/3.73 % (378593)------------------------------
% 19.41/3.73 % (378593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378593)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378593)Termination reason: Instruction limit
% 19.41/3.73 % (378593)Termination phase: Saturation
% 19.41/3.73 % (378593)Time elapsed: 0.098 s
% 19.41/3.73 % (378593)Peak memory usage: 117 MB
% 19.41/3.73 % (378593)Instructions burned: 65 (million)
% 19.41/3.73 % (378597)dis+1010_1_to=kbo:si=on:random_seed=3094056547:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2980 on theBenchmark for (2980ds/175Mi)
% 19.41/3.73 % (378596)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2199848832:i=39:ins=3:rtra=on_2980 on theBenchmark for (2980ds/39Mi)
% 19.41/3.73 % (378594)Instruction limit reached!
% 19.41/3.73 % (378594)------------------------------
% 19.41/3.73 % (378594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378594)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378594)Termination reason: Instruction limit
% 19.41/3.73 % (378594)Termination phase: Saturation
% 19.41/3.73 % (378594)Time elapsed: 0.125 s
% 19.41/3.73 % (378594)Peak memory usage: 90 MB
% 19.41/3.73 % (378594)Instructions burned: 121 (million)
% 19.41/3.73 % (378586)Instruction limit reached!
% 19.41/3.73 % (378586)------------------------------
% 19.41/3.73 % (378586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378586)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378586)Termination reason: Instruction limit
% 19.41/3.73 % (378586)Termination phase: Saturation
% 19.41/3.73 % (378586)Time elapsed: 0.441 s
% 19.41/3.73 % (378586)Peak memory usage: 96 MB
% 19.41/3.73 % (378586)Instructions burned: 383 (million)
% 19.41/3.73 % (378596)Instruction limit reached!
% 19.41/3.73 % (378596)------------------------------
% 19.41/3.73 % (378596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378596)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378596)Termination reason: Instruction limit
% 19.41/3.73 % (378596)Termination phase: Saturation
% 19.41/3.73 % (378596)Time elapsed: 0.070 s
% 19.41/3.73 % (378596)Peak memory usage: 113 MB
% 19.41/3.73 % (378596)Instructions burned: 39 (million)
% 19.41/3.73 % (378603)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3355929434:s2a=on:i=483:doe=on:nm=32:rtra=on_2978 on theBenchmark for (2978ds/483Mi)
% 19.41/3.73 % (378601)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1964402701:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/329Mi)
% 19.41/3.73 % (378597)Instruction limit reached!
% 19.41/3.73 % (378597)------------------------------
% 19.41/3.73 % (378597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378597)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378597)Termination reason: Instruction limit
% 19.41/3.73 % (378597)Termination phase: Saturation
% 19.41/3.73 % (378597)Time elapsed: 0.208 s
% 19.41/3.73 % (378597)Peak memory usage: 92 MB
% 19.41/3.73 % (378597)Instructions burned: 175 (million)
% 19.41/3.73 % (378605)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3983384311:thitd=on:i=215:nm=0:rtra=on:ev=force_2977 on theBenchmark for (2977ds/215Mi)
% 19.41/3.73 % (378606)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1811659626:i=349:rtra=on_2977 on theBenchmark for (2977ds/349Mi)
% 19.41/3.73 % (378607)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1646434409:st=2:i=295:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/295Mi)
% 19.41/3.73 % (378605)Instruction limit reached!
% 19.41/3.73 % (378605)------------------------------
% 19.41/3.73 % (378605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378605)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378605)Termination reason: Instruction limit
% 19.41/3.73 % (378605)Termination phase: Saturation
% 19.41/3.73 % (378605)Time elapsed: 0.128 s
% 19.41/3.73 % (378605)Peak memory usage: 137 MB
% 19.41/3.73 % (378605)Instructions burned: 219 (million)
% 19.41/3.73 % (378610)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=4016900236:i=328:kws=inv_frequency:nm=20:rtra=on_2976 on theBenchmark for (2976ds/328Mi)
% 19.41/3.73 % (378617)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2845679835:i=281:gtgl=2:rtra=on:gtg=all_2975 on theBenchmark for (2975ds/281Mi)
% 19.41/3.73 % (378601)Instruction limit reached!
% 19.41/3.73 % (378601)------------------------------
% 19.41/3.73 % (378601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378601)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378601)Termination reason: Instruction limit
% 19.41/3.73 % (378601)Termination phase: Saturation
% 19.41/3.73 % (378601)Time elapsed: 0.385 s
% 19.41/3.73 % (378601)Peak memory usage: 120 MB
% 19.41/3.73 % (378601)Instructions burned: 330 (million)
% 19.41/3.73 % (378603)First to succeed.
% 19.41/3.73 % (378603)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-378462"
% 19.41/3.73 % (378585)Instruction limit reached!
% 19.41/3.73 % (378585)------------------------------
% 19.41/3.73 % (378585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378585)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378585)Termination reason: Instruction limit
% 19.41/3.73 % (378585)Termination phase: Saturation
% 19.41/3.73 % (378585)Time elapsed: 0.988 s
% 19.41/3.73 % (378585)Peak memory usage: 97 MB
% 19.41/3.73 % (378585)Instructions burned: 1000 (million)
% 19.41/3.73 % (378607)Instruction limit reached!
% 19.41/3.73 % (378607)------------------------------
% 19.41/3.73 % (378607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378607)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378607)Termination reason: Instruction limit
% 19.41/3.73 % (378607)Termination phase: Saturation
% 19.41/3.73 % (378607)Time elapsed: 0.292 s
% 19.41/3.73 % (378607)Peak memory usage: 92 MB
% 19.41/3.73 % (378607)Instructions burned: 295 (million)
% 19.41/3.73 % (378606)Instruction limit reached!
% 19.41/3.73 % (378606)------------------------------
% 19.41/3.73 % (378606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378606)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378606)Termination reason: Instruction limit
% 19.41/3.73 % (378606)Termination phase: Saturation
% 19.41/3.73 % (378606)Time elapsed: 0.339 s
% 19.41/3.73 % (378606)Peak memory usage: 118 MB
% 19.41/3.73 % (378606)Instructions burned: 352 (million)
% 19.41/3.73 % (378617)Instruction limit reached!
% 19.41/3.73 % (378617)------------------------------
% 19.41/3.73 % (378617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378617)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378617)Termination reason: Instruction limit
% 19.41/3.73 % (378617)Termination phase: Saturation
% 19.41/3.73 % (378617)Time elapsed: 0.176 s
% 19.41/3.73 % (378617)Peak memory usage: 118 MB
% 19.41/3.73 % (378617)Instructions burned: 283 (million)
% 19.41/3.73 % (378621)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2111167933:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi)
% 19.41/3.73 % (378610)Instruction limit reached!
% 19.41/3.73 % (378610)------------------------------
% 19.41/3.73 % (378610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.41/3.73 % (378610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.41/3.73 % (378610)CaDiCaL version: 2.1.3
% 19.41/3.73 % (378610)Termination reason: Instruction limit
% 19.41/3.73 % (378610)Termination phase: Saturation
% 19.41/3.73 % (378610)Time elapsed: 0.371 s
% 19.41/3.73 % (378610)Peak memory usage: 118 MB
% 19.41/3.73 % (378610)Instructions burned: 328 (million)
% 19.41/3.73 % (378625)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=3100439215:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi)
% 19.41/3.73 % (378623)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=829002005:i=416:rtra=on:gtg=position:ss=axioms_2972 on theBenchmark for (2972ds/416Mi)
% 19.41/3.73 % (378622)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1519739125:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2972 on theBenchmark for (2972ds/321Mi)
% 19.41/3.73 % (378624)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3424718610:i=471:thf=on:kws=precedence:rtra=on_2972 on theBenchmark for (2972ds/471Mi)
% 19.41/3.73 % (378603)Refutation found. Thanks to Tanya!
% 19.41/3.73 % SZS status Theorem for theBenchmark
% 19.41/3.73 % SZS output start Proof for theBenchmark
% See solution above
% 22.63/4.02 % (378603)------------------------------
% 22.63/4.02 % (378603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.63/4.02 % (378603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.63/4.02 % (378603)CaDiCaL version: 2.1.3
% 22.63/4.02 % (378603)Termination reason: Refutation
% 22.63/4.02 % (378603)Time elapsed: 0.441 s
% 22.63/4.02 % (378603)Peak memory usage: 137 MB
% 22.63/4.02 % (378603)Instructions burned: 396 (million)
% 22.63/4.02 % (378603)------------------------------
% 22.63/4.02 % (378603)------------------------------
% 22.63/4.02 % (378462)Success in time 3.137 s
% 22.63/4.02 % Vampire exiting
%------------------------------------------------------------------------------