%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW577_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:40:28 PM UTC 2026
% Result : Theorem 10.68s 2.03s
% Output : Refutation 10.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 22
% Syntax : Number of formulae : 131 ( 63 unt; 0 typ; 16 def)
% Number of atoms : 1153 ( 273 equ)
% Maximal formula atoms : 93 ( 8 avg)
% Number of connectives : 1502 ( 480 ~; 397 |; 403 &)
% ( 9 <=>; 213 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 619 ( 308 atm; 131 fun; 110 num; 70 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 : 27 ( 23 usr; 1 prp; 0-6 aty)
% Number of functors : 189 ( 185 usr; 52 con; 0-6 aty)
% Number of variables : 660 ( 507 !; 153 ?; 660 :)
% 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,
sK7: ( set_lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > lpvertexcm_vertexrp ).
tff(func_def_84,type,
sK8: ( set_vertex * set_vertex ) > vertex ).
tff(func_def_85,type,
sK9: ( ty * uni * uni ) > uni ).
tff(func_def_86,type,
sK10: ( set_lpvertexcm_vertexrp * set_lpvertexcm_vertexrp ) > lpvertexcm_vertexrp ).
tff(func_def_87,type,
sK11: ( set_vertex * set_vertex ) > vertex ).
tff(func_def_88,type,
sK12: ( ty * uni * uni ) > uni ).
tff(func_def_89,type,
sK13: set_lpvertexcm_vertexrp > lpvertexcm_vertexrp ).
tff(func_def_90,type,
sK14: set_vertex > vertex ).
tff(func_def_91,type,
sK15: ( ty * uni ) > uni ).
tff(func_def_92,type,
sK16: ( ty * uni * uni ) > uni ).
tff(func_def_93,type,
sK17: ( ty * uni * uni ) > uni ).
tff(func_def_94,type,
sK18: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_95,type,
sK19: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_96,type,
sK20: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_97,type,
sK21: ( vertex * list_vertex * vertex ) > list_vertex ).
tff(func_def_98,type,
sK22: ( vertex * list_vertex * vertex ) > vertex ).
tff(func_def_99,type,
sK23: ( vertex * vertex * list_vertex ) > vertex ).
tff(func_def_100,type,
sK24: ( vertex * vertex * list_vertex ) > list_vertex ).
tff(func_def_101,type,
sK25: set_vertex > list_vertex ).
tff(func_def_102,type,
sK26: list_vertex > vertex ).
tff(func_def_103,type,
sK27: list_vertex > list_vertex ).
tff(func_def_104,type,
sK28: list_vertex > list_vertex ).
tff(func_def_105,type,
sK29: list_vertex > list_vertex ).
tff(func_def_106,type,
sK30: ( set_vertex * list_vertex ) > vertex ).
tff(func_def_107,type,
sK31: set_vertex ).
tff(func_def_108,type,
sK32: vertex ).
tff(func_def_109,type,
sK33: set_vertex ).
tff(func_def_110,type,
sK34: list_vertex > vertex ).
tff(func_def_111,type,
sK35: list_vertex > list_vertex ).
tff(func_def_112,type,
sK36: list_vertex > list_vertex ).
tff(func_def_113,type,
sK37: list_vertex > list_vertex ).
tff(func_def_114,type,
sK38: ( set_vertex * list_vertex ) > vertex ).
tff(func_def_115,type,
sK39: list_vertex > vertex ).
tff(func_def_116,type,
sK40: list_vertex > list_vertex ).
tff(func_def_117,type,
sK41: list_vertex > list_vertex ).
tff(func_def_118,type,
sK42: list_vertex > list_vertex ).
tff(func_def_119,type,
sK43: ( set_vertex * list_vertex ) > vertex ).
tff(func_def_120,type,
sK44: ( list_vertex * vertex ) > vertex ).
tff(func_def_121,type,
sK45: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_122,type,
sK46: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_123,type,
sK47: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_124,type,
sK48: ( list_vertex * vertex ) > vertex ).
tff(func_def_125,type,
sK49: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_126,type,
sK50: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_127,type,
sK51: list_vertex > vertex ).
tff(func_def_128,type,
sK52: list_vertex > list_vertex ).
tff(func_def_129,type,
sK53: list_vertex > list_vertex ).
tff(func_def_130,type,
sK54: list_vertex > list_vertex ).
tff(func_def_131,type,
sK55: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_132,type,
sK56: ( list_vertex * vertex ) > list_vertex ).
tff(func_def_133,type,
sK57: list_vertex > vertex ).
tff(func_def_134,type,
sK58: list_vertex > list_vertex ).
tff(func_def_135,type,
sK59: list_vertex > list_vertex ).
tff(func_def_136,type,
sK60: list_vertex > list_vertex ).
tff(func_def_137,type,
sK61: vertex > list_vertex ).
tff(func_def_138,type,
sK62: vertex > list_vertex ).
tff(func_def_139,type,
sK63: vertex > list_vertex ).
tff(func_def_140,type,
sK64: vertex ).
tff(func_def_141,type,
sK65: ( vertex * $int ) > list_vertex ).
tff(func_def_142,type,
sK66: ( vertex * $int ) > list_vertex ).
tff(func_def_143,type,
sK67: ( vertex * $int * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_144,type,
sK68: ( vertex * $int * set_lpvertexcm_vertexrp ) > list_vertex ).
tff(func_def_145,type,
sK69: ( $int * vertex * set_lpvertexcm_vertexrp * $int ) > vertex ).
tff(func_def_146,type,
sK70: ( $int * vertex * set_lpvertexcm_vertexrp * $int ) > list_vertex ).
tff(func_def_147,type,
sK71: ( vertex * $int ) > list_vertex ).
tff(func_def_148,type,
sK72: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_149,type,
sK73: ( map_vertex_t19 * $int * set_lpvertexcm_vertexrp * $int ) > list_vertex ).
tff(func_def_150,type,
sK74: ( map_vertex_t19 * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_151,type,
sK75: ( map_vertex_t19 * set_lpvertexcm_vertexrp ) > vertex ).
tff(func_def_152,type,
sK76: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp * vertex * vertex ) > $int ).
tff(func_def_153,type,
sK77: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp * vertex * vertex ) > list_vertex ).
tff(func_def_154,type,
sK78: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > $int ).
tff(func_def_155,type,
sK79: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > list_vertex ).
tff(func_def_156,type,
sK80: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > $int ).
tff(func_def_157,type,
sK81: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > list_vertex ).
tff(func_def_158,type,
sK82: ( vertex * map_vertex_t19 * $int ) > $int ).
tff(func_def_159,type,
sK83: ( vertex * map_vertex_t19 * $int ) > list_vertex ).
tff(func_def_160,type,
sK84: map_vertex_t19 ).
tff(func_def_161,type,
sK85: $int ).
tff(func_def_162,type,
sK86: set_lpvertexcm_vertexrp ).
tff(func_def_163,type,
sK87: set_lpvertexcm_vertexrp ).
tff(func_def_164,type,
sK88: map_vertex_t19 ).
tff(func_def_165,type,
sK89: bool ).
tff(func_def_166,type,
sK90: set_lpvertexcm_vertexrp ).
tff(func_def_167,type,
sK91: vertex ).
tff(func_def_168,type,
sK92: vertex ).
tff(func_def_169,type,
sK93: map_vertex_t19 ).
tff(func_def_170,type,
sK94: vertex ).
tff(func_def_171,type,
sK95: $int ).
tff(func_def_172,type,
sK96: vertex ).
tff(func_def_173,type,
sK97: list_vertex ).
tff(func_def_174,type,
sK98: lpvertexcm_vertexrp ).
tff(func_def_175,type,
sK99: lpvertexcm_vertexrp ).
tff(func_def_176,type,
sF100: $int ).
tff(func_def_177,type,
sF101: $int ).
tff(func_def_178,type,
sF102: $int ).
tff(func_def_179,type,
sF103: $int ).
tff(func_def_180,type,
sF104: lpvertexcm_vertexrp ).
tff(func_def_181,type,
sF105: set_lpvertexcm_vertexrp ).
tff(func_def_182,type,
sF106: $int ).
tff(func_def_183,type,
sF107: t ).
tff(func_def_184,type,
sF108: t ).
tff(func_def_185,type,
sF109: lpvertexcm_vertexrp ).
tff(func_def_186,type,
sF110: set_lpvertexcm_vertexrp ).
tff(func_def_187,type,
sF111: set_lpvertexcm_vertexrp ).
tff(func_def_188,type,
sF112: set_lpvertexcm_vertexrp ).
tff(func_def_189,type,
sF113: $int ).
tff(func_def_190,type,
sF114: $int ).
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(pred_def_19,type,
sP0: ( vertex * list_vertex * vertex ) > $o ).
tff(pred_def_20,type,
sP1: ( $int * vertex * set_lpvertexcm_vertexrp * $int ) > $o ).
tff(pred_def_21,type,
sP2: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > $o ).
tff(pred_def_22,type,
sP3: ( vertex * map_vertex_t19 * $int ) > $o ).
tff(pred_def_23,type,
sP4: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > $o ).
tff(pred_def_24,type,
sP5: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp ) > $o ).
tff(pred_def_25,type,
sP6: ( vertex * map_vertex_t19 * $int * set_lpvertexcm_vertexrp * vertex * vertex ) > $o ).
tff(f73,axiom,
! [X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp] :
( mem2(X0,add2(X1,X2))
<=> ( ( X0 = X1 )
| mem2(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',add_def1) ).
tff(f80,axiom,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X0,X1)
=> ( add2(X0,remove2(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',add_remove) ).
tff(f98,axiom,
! [X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp,X2: lpvertexcm_vertexrp] :
( mem2(X2,diff2(X0,X1))
<=> ( mem2(X2,X0)
& ~ mem2(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',diff_def1) ).
tff(f180,axiom,
! [X0: $int] : ( finite(X0) != infinite ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_Infinite) ).
tff(f181,axiom,
! [X0: $int] : ( finite_proj_1(finite(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_proj_1_def) ).
tff(f197,conjecture,
( ( $less(1,$difference(cardinal1(vertices),1))
| ( 1 = $difference(cardinal1(vertices),1) ) )
=> ! [X0: map_vertex_t19,X1: $int] :
( ( ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$difference(cardinal1(vertices),1))
| ( X1 = $difference(cardinal1(vertices),1) ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [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)) ) )
& ! [X5: vertex,X4: list_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) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),empty2)
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) ) ) ) )
=> ! [X7: set_lpvertexcm_vertexrp] :
( ( X7 = edges )
=> ! [X8: set_lpvertexcm_vertexrp,X9: map_vertex_t19] :
( ( ! [X3: lpvertexcm_vertexrp] :
( mem2(X3,X8)
=> mem2(X3,edges) )
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X9,X2) = finite(X3) )
& ? [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)) ) )
& ! [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) = 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)) ) ) ) ) ) )
=> ! [X10: bool] :
( ( ( X10 = true )
<=> ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8) )
=> ( ( X10 != true )
=> ( ~ ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8)
=> ! [X11: set_lpvertexcm_vertexrp,X12: vertex,X13: vertex] :
( ( mem2(tuple22(X12,X13),X8)
& ( X11 = remove2(tuple22(X12,X13),X8) ) )
=> ( ( ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X12,X13),edges)
& ~ mem2(tuple22(X12,X13),diff2(edges,X8))
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X9,X2) = finite(X3) )
& ? [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)) ) )
& ! [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) = 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)) ) ) ) ) ) )
=> ! [X14: map_vertex_t19] :
( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
& ? [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)) ) )
& ! [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))) ) ) ) )
| ( ( 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) )
=> ! [X5: vertex,X4: list_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/sandbox/benchmark/theBenchmark.p',wP_parameter_bellman_ford) ).
tff(f198,negated_conjecture,
~ ( ( $less(1,$difference(cardinal1(vertices),1))
| ( 1 = $difference(cardinal1(vertices),1) ) )
=> ! [X0: map_vertex_t19,X1: $int] :
( ( ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$difference(cardinal1(vertices),1))
| ( X1 = $difference(cardinal1(vertices),1) ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [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)) ) )
& ! [X5: vertex,X4: list_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) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> $lesseq(X1,length1(X4)) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),empty2)
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> $lesseq(X1,length1(X6)) ) ) ) ) )
=> ! [X7: set_lpvertexcm_vertexrp] :
( ( X7 = edges )
=> ! [X8: set_lpvertexcm_vertexrp,X9: map_vertex_t19] :
( ( ! [X3: lpvertexcm_vertexrp] :
( mem2(X3,X8)
=> mem2(X3,edges) )
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X9,X2) = finite(X3) )
& ? [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)) ) )
& ! [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) = 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)) ) ) ) ) ) )
=> ! [X10: bool] :
( ( ( X10 = true )
<=> ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8) )
=> ( ( X10 != true )
=> ( ~ ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8)
=> ! [X11: set_lpvertexcm_vertexrp,X12: vertex,X13: vertex] :
( ( mem2(tuple22(X12,X13),X8)
& ( X11 = remove2(tuple22(X12,X13),X8) ) )
=> ( ( ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X12,X13),edges)
& ~ mem2(tuple22(X12,X13),diff2(edges,X8))
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X9,X2) = finite(X3) )
& ? [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)) ) )
& ! [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) = 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)) ) ) ) ) ) )
=> ! [X14: map_vertex_t19] :
( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
& ? [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)) ) )
& ! [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))) ) ) ) )
| ( ( 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) )
=> ! [X5: vertex,X4: list_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(f211,plain,
~ ( ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) )
=> ! [X0: map_vertex_t19,X1: $int] :
( ( ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [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) ) )
& ! [X5: vertex,X4: list_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) = infinite )
& ! [X4: list_vertex] :
( path(s,X4,X2)
=> ~ $less(length1(X4),X1) )
& ! [X5: vertex] :
( mem2(tuple22(X5,X2),empty2)
=> ! [X6: list_vertex] :
( path(s,X6,X5)
=> ~ $less(length1(X6),X1) ) ) ) ) )
=> ! [X7: set_lpvertexcm_vertexrp] :
( ( X7 = edges )
=> ! [X8: set_lpvertexcm_vertexrp,X9: map_vertex_t19] :
( ( ! [X3: lpvertexcm_vertexrp] :
( mem2(X3,X8)
=> mem2(X3,edges) )
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X9,X2) = finite(X3) )
& ? [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) ) )
& ! [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) = 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) ) ) ) ) ) )
=> ! [X10: bool] :
( ( ( X10 = true )
<=> ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8) )
=> ( ( X10 != true )
=> ( ~ ! [X3: lpvertexcm_vertexrp] : ~ mem2(X3,X8)
=> ! [X11: set_lpvertexcm_vertexrp,X12: vertex,X13: vertex] :
( ( mem2(tuple22(X12,X13),X8)
& ( X11 = remove2(tuple22(X12,X13),X8) ) )
=> ( ( ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X12,X13),edges)
& ~ mem2(tuple22(X12,X13),diff2(edges,X8))
& ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X9,X2) = finite(X3) )
& ? [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) ) )
& ! [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) = 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) ) ) ) ) ) )
=> ! [X14: map_vertex_t19] :
( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X14,X2) = finite(X3) )
& ? [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) ) )
& ! [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) ) ) ) )
| ( ( 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) )
=> ! [X5: vertex,X4: list_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(f248,plain,
~ ( ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) )
=> ! [X0: map_vertex_t19,X1: $int] :
( ( ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
=> ( ! [X2: vertex] :
( mem1(X2,vertices)
=> ( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X5: list_vertex] :
( path(s,X5,X2)
=> ( $less(length1(X5),X1)
=> ~ $less(path_weight(X5,X2),X3) ) )
& ! [X6: vertex,X7: list_vertex] :
( path(s,X7,X6)
=> ( $less(length1(X7),X1)
=> ( mem2(tuple22(X6,X2),empty2)
=> ~ $less($sum(path_weight(X7,X6),weight(X6,X2)),X3) ) ) ) )
| ( ( get1(X0,X2) = infinite )
& ! [X8: list_vertex] :
( path(s,X8,X2)
=> ~ $less(length1(X8),X1) )
& ! [X9: vertex] :
( mem2(tuple22(X9,X2),empty2)
=> ! [X10: list_vertex] :
( path(s,X10,X9)
=> ~ $less(length1(X10),X1) ) ) ) ) )
=> ! [X11: set_lpvertexcm_vertexrp] :
( ( edges = X11 )
=> ! [X12: set_lpvertexcm_vertexrp,X13: map_vertex_t19] :
( ( ! [X14: lpvertexcm_vertexrp] :
( mem2(X14,X12)
=> mem2(X14,edges) )
& ! [X15: vertex] :
( mem1(X15,vertices)
=> ( ? [X16: $int] :
( ( finite(X16) = get1(X13,X15) )
& ? [X17: list_vertex] :
( path(s,X17,X15)
& ( path_weight(X17,X15) = X16 ) )
& ! [X18: list_vertex] :
( path(s,X18,X15)
=> ( $less(length1(X18),X1)
=> ~ $less(path_weight(X18,X15),X16) ) )
& ! [X19: vertex,X20: list_vertex] :
( path(s,X20,X19)
=> ( $less(length1(X20),X1)
=> ( mem2(tuple22(X19,X15),diff2(edges,X12))
=> ~ $less($sum(path_weight(X20,X19),weight(X19,X15)),X16) ) ) ) )
| ( ( infinite = get1(X13,X15) )
& ! [X21: list_vertex] :
( path(s,X21,X15)
=> ~ $less(length1(X21),X1) )
& ! [X22: vertex] :
( mem2(tuple22(X22,X15),diff2(edges,X12))
=> ! [X23: list_vertex] :
( path(s,X23,X22)
=> ~ $less(length1(X23),X1) ) ) ) ) ) )
=> ! [X24: bool] :
( ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X12) )
=> ( ( true != X24 )
=> ( ~ ! [X26: lpvertexcm_vertexrp] : ~ mem2(X26,X12)
=> ! [X27: set_lpvertexcm_vertexrp,X28: vertex,X29: vertex] :
( ( mem2(tuple22(X28,X29),X12)
& ( remove2(tuple22(X28,X29),X12) = X27 ) )
=> ( ( ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X28,X29),edges)
& ~ mem2(tuple22(X28,X29),diff2(edges,X12))
& ! [X30: vertex] :
( mem1(X30,vertices)
=> ( ? [X31: $int] :
( ( finite(X31) = get1(X13,X30) )
& ? [X32: list_vertex] :
( path(s,X32,X30)
& ( path_weight(X32,X30) = X31 ) )
& ! [X33: list_vertex] :
( path(s,X33,X30)
=> ( $less(length1(X33),X1)
=> ~ $less(path_weight(X33,X30),X31) ) )
& ! [X34: vertex,X35: list_vertex] :
( path(s,X35,X34)
=> ( $less(length1(X35),X1)
=> ( mem2(tuple22(X34,X30),diff2(edges,X12))
=> ~ $less($sum(path_weight(X35,X34),weight(X34,X30)),X31) ) ) ) )
| ( ( infinite = get1(X13,X30) )
& ! [X36: list_vertex] :
( path(s,X36,X30)
=> ~ $less(length1(X36),X1) )
& ! [X37: vertex] :
( mem2(tuple22(X37,X30),diff2(edges,X12))
=> ! [X38: list_vertex] :
( path(s,X38,X37)
=> ~ $less(length1(X38),X1) ) ) ) ) ) )
=> ! [X39: map_vertex_t19] :
( ! [X40: vertex] :
( mem1(X40,vertices)
=> ( ? [X41: $int] :
( ( finite(X41) = get1(X39,X40) )
& ? [X42: list_vertex] :
( path(s,X42,X40)
& ( path_weight(X42,X40) = X41 ) )
& ! [X43: list_vertex] :
( path(s,X43,X40)
=> ( $less(length1(X43),X1)
=> ~ $less(path_weight(X43,X40),X41) ) )
& ! [X44: vertex,X45: list_vertex] :
( path(s,X45,X44)
=> ( $less(length1(X45),X1)
=> ( mem2(tuple22(X44,X40),add2(tuple22(X28,X29),diff2(edges,X12)))
=> ~ $less($sum(path_weight(X45,X44),weight(X44,X40)),X41) ) ) ) )
| ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( path(s,X46,X40)
=> ~ $less(length1(X46),X1) )
& ! [X47: vertex] :
( mem2(tuple22(X47,X40),add2(tuple22(X28,X29),diff2(edges,X12)))
=> ! [X48: list_vertex] :
( path(s,X48,X47)
=> ~ $less(length1(X48),X1) ) ) ) ) )
=> ! [X49: vertex] :
( mem1(X49,vertices)
=> ! [X50: $int] :
( ( finite(X50) = get1(X39,X49) )
=> ! [X51: vertex,X52: list_vertex] :
( path(s,X52,X51)
=> ( $less(length1(X52),X1)
=> ( mem2(tuple22(X51,X49),diff2(edges,X27))
=> ~ $less($sum(path_weight(X52,X51),weight(X51,X49)),X50) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f211]) ).
tff(f281,plain,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ( add2(X0,remove2(X0,X1)) = X1 )
| ~ mem2(X0,X1) ),
inference(ennf_transformation,[],[f80]) ).
tff(f356,plain,
( ? [X0: map_vertex_t19,X1: $int] :
( ? [X11: set_lpvertexcm_vertexrp] :
( ? [X12: set_lpvertexcm_vertexrp,X13: map_vertex_t19] :
( ? [X24: bool] :
( ? [X27: set_lpvertexcm_vertexrp,X28: vertex,X29: vertex] :
( ? [X39: map_vertex_t19] :
( ? [X49: vertex] :
( ? [X50: $int] :
( ? [X51: vertex,X52: list_vertex] :
( $less($sum(path_weight(X52,X51),weight(X51,X49)),X50)
& mem2(tuple22(X51,X49),diff2(edges,X27))
& $less(length1(X52),X1)
& path(s,X52,X51) )
& ( finite(X50) = get1(X39,X49) ) )
& mem1(X49,vertices) )
& ! [X40: vertex] :
( ? [X41: $int] :
( ( finite(X41) = get1(X39,X40) )
& ? [X42: list_vertex] :
( path(s,X42,X40)
& ( path_weight(X42,X40) = X41 ) )
& ! [X43: list_vertex] :
( ~ $less(path_weight(X43,X40),X41)
| ~ $less(length1(X43),X1)
| ~ path(s,X43,X40) )
& ! [X44: vertex,X45: list_vertex] :
( ~ $less($sum(path_weight(X45,X44),weight(X44,X40)),X41)
| ~ mem2(tuple22(X44,X40),add2(tuple22(X28,X29),diff2(edges,X12)))
| ~ $less(length1(X45),X1)
| ~ path(s,X45,X44) ) )
| ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( ~ $less(length1(X46),X1)
| ~ path(s,X46,X40) )
& ! [X47: vertex] :
( ! [X48: list_vertex] :
( ~ $less(length1(X48),X1)
| ~ path(s,X48,X47) )
| ~ mem2(tuple22(X47,X40),add2(tuple22(X28,X29),diff2(edges,X12))) ) )
| ~ mem1(X40,vertices) ) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X28,X29),edges)
& ~ mem2(tuple22(X28,X29),diff2(edges,X12))
& ! [X30: vertex] :
( ? [X31: $int] :
( ( finite(X31) = get1(X13,X30) )
& ? [X32: list_vertex] :
( path(s,X32,X30)
& ( path_weight(X32,X30) = X31 ) )
& ! [X33: list_vertex] :
( ~ $less(path_weight(X33,X30),X31)
| ~ $less(length1(X33),X1)
| ~ path(s,X33,X30) )
& ! [X34: vertex,X35: list_vertex] :
( ~ $less($sum(path_weight(X35,X34),weight(X34,X30)),X31)
| ~ mem2(tuple22(X34,X30),diff2(edges,X12))
| ~ $less(length1(X35),X1)
| ~ path(s,X35,X34) ) )
| ( ( infinite = get1(X13,X30) )
& ! [X36: list_vertex] :
( ~ $less(length1(X36),X1)
| ~ path(s,X36,X30) )
& ! [X37: vertex] :
( ! [X38: list_vertex] :
( ~ $less(length1(X38),X1)
| ~ path(s,X38,X37) )
| ~ mem2(tuple22(X37,X30),diff2(edges,X12)) ) )
| ~ mem1(X30,vertices) )
& mem2(tuple22(X28,X29),X12)
& ( remove2(tuple22(X28,X29),X12) = X27 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X12)
& ( true != X24 )
& ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X12) ) )
& ! [X14: lpvertexcm_vertexrp] :
( mem2(X14,edges)
| ~ mem2(X14,X12) )
& ! [X15: vertex] :
( ? [X16: $int] :
( ( finite(X16) = get1(X13,X15) )
& ? [X17: list_vertex] :
( path(s,X17,X15)
& ( path_weight(X17,X15) = X16 ) )
& ! [X18: list_vertex] :
( ~ $less(path_weight(X18,X15),X16)
| ~ $less(length1(X18),X1)
| ~ path(s,X18,X15) )
& ! [X19: vertex,X20: list_vertex] :
( ~ $less($sum(path_weight(X20,X19),weight(X19,X15)),X16)
| ~ mem2(tuple22(X19,X15),diff2(edges,X12))
| ~ $less(length1(X20),X1)
| ~ path(s,X20,X19) ) )
| ( ( infinite = get1(X13,X15) )
& ! [X21: list_vertex] :
( ~ $less(length1(X21),X1)
| ~ path(s,X21,X15) )
& ! [X22: vertex] :
( ! [X23: list_vertex] :
( ~ $less(length1(X23),X1)
| ~ path(s,X23,X22) )
| ~ mem2(tuple22(X22,X15),diff2(edges,X12)) ) )
| ~ mem1(X15,vertices) ) )
& ( edges = X11 ) )
& ! [X2: vertex] :
( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X5: list_vertex] :
( ~ $less(path_weight(X5,X2),X3)
| ~ $less(length1(X5),X1)
| ~ path(s,X5,X2) )
& ! [X6: vertex,X7: list_vertex] :
( ~ $less($sum(path_weight(X7,X6),weight(X6,X2)),X3)
| ~ mem2(tuple22(X6,X2),empty2)
| ~ $less(length1(X7),X1)
| ~ path(s,X7,X6) ) )
| ( ( get1(X0,X2) = infinite )
& ! [X8: list_vertex] :
( ~ $less(length1(X8),X1)
| ~ path(s,X8,X2) )
& ! [X9: vertex] :
( ! [X10: list_vertex] :
( ~ $less(length1(X10),X1)
| ~ path(s,X10,X9) )
| ~ mem2(tuple22(X9,X2),empty2) ) )
| ~ mem1(X2,vertices) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(ennf_transformation,[],[f248]) ).
tff(f357,plain,
( ? [X0: map_vertex_t19,X1: $int] :
( ? [X11: set_lpvertexcm_vertexrp] :
( ? [X12: set_lpvertexcm_vertexrp,X13: map_vertex_t19] :
( ? [X24: bool] :
( ? [X27: set_lpvertexcm_vertexrp,X28: vertex,X29: vertex] :
( ? [X39: map_vertex_t19] :
( ? [X49: vertex] :
( ? [X50: $int] :
( ? [X51: vertex,X52: list_vertex] :
( $less($sum(path_weight(X52,X51),weight(X51,X49)),X50)
& mem2(tuple22(X51,X49),diff2(edges,X27))
& $less(length1(X52),X1)
& path(s,X52,X51) )
& ( finite(X50) = get1(X39,X49) ) )
& mem1(X49,vertices) )
& ! [X40: vertex] :
( ? [X41: $int] :
( ( finite(X41) = get1(X39,X40) )
& ? [X42: list_vertex] :
( path(s,X42,X40)
& ( path_weight(X42,X40) = X41 ) )
& ! [X43: list_vertex] :
( ~ $less(path_weight(X43,X40),X41)
| ~ $less(length1(X43),X1)
| ~ path(s,X43,X40) )
& ! [X44: vertex,X45: list_vertex] :
( ~ $less($sum(path_weight(X45,X44),weight(X44,X40)),X41)
| ~ mem2(tuple22(X44,X40),add2(tuple22(X28,X29),diff2(edges,X12)))
| ~ $less(length1(X45),X1)
| ~ path(s,X45,X44) ) )
| ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( ~ $less(length1(X46),X1)
| ~ path(s,X46,X40) )
& ! [X47: vertex] :
( ! [X48: list_vertex] :
( ~ $less(length1(X48),X1)
| ~ path(s,X48,X47) )
| ~ mem2(tuple22(X47,X40),add2(tuple22(X28,X29),diff2(edges,X12))) ) )
| ~ mem1(X40,vertices) ) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X28,X29),edges)
& ~ mem2(tuple22(X28,X29),diff2(edges,X12))
& ! [X30: vertex] :
( ? [X31: $int] :
( ( finite(X31) = get1(X13,X30) )
& ? [X32: list_vertex] :
( path(s,X32,X30)
& ( path_weight(X32,X30) = X31 ) )
& ! [X33: list_vertex] :
( ~ $less(path_weight(X33,X30),X31)
| ~ $less(length1(X33),X1)
| ~ path(s,X33,X30) )
& ! [X34: vertex,X35: list_vertex] :
( ~ $less($sum(path_weight(X35,X34),weight(X34,X30)),X31)
| ~ mem2(tuple22(X34,X30),diff2(edges,X12))
| ~ $less(length1(X35),X1)
| ~ path(s,X35,X34) ) )
| ( ( infinite = get1(X13,X30) )
& ! [X36: list_vertex] :
( ~ $less(length1(X36),X1)
| ~ path(s,X36,X30) )
& ! [X37: vertex] :
( ! [X38: list_vertex] :
( ~ $less(length1(X38),X1)
| ~ path(s,X38,X37) )
| ~ mem2(tuple22(X37,X30),diff2(edges,X12)) ) )
| ~ mem1(X30,vertices) )
& mem2(tuple22(X28,X29),X12)
& ( remove2(tuple22(X28,X29),X12) = X27 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X12)
& ( true != X24 )
& ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X12) ) )
& ! [X14: lpvertexcm_vertexrp] :
( mem2(X14,edges)
| ~ mem2(X14,X12) )
& ! [X15: vertex] :
( ? [X16: $int] :
( ( finite(X16) = get1(X13,X15) )
& ? [X17: list_vertex] :
( path(s,X17,X15)
& ( path_weight(X17,X15) = X16 ) )
& ! [X18: list_vertex] :
( ~ $less(path_weight(X18,X15),X16)
| ~ $less(length1(X18),X1)
| ~ path(s,X18,X15) )
& ! [X19: vertex,X20: list_vertex] :
( ~ $less($sum(path_weight(X20,X19),weight(X19,X15)),X16)
| ~ mem2(tuple22(X19,X15),diff2(edges,X12))
| ~ $less(length1(X20),X1)
| ~ path(s,X20,X19) ) )
| ( ( infinite = get1(X13,X15) )
& ! [X21: list_vertex] :
( ~ $less(length1(X21),X1)
| ~ path(s,X21,X15) )
& ! [X22: vertex] :
( ! [X23: list_vertex] :
( ~ $less(length1(X23),X1)
| ~ path(s,X23,X22) )
| ~ mem2(tuple22(X22,X15),diff2(edges,X12)) ) )
| ~ mem1(X15,vertices) ) )
& ( edges = X11 ) )
& ! [X2: vertex] :
( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X5: list_vertex] :
( ~ $less(path_weight(X5,X2),X3)
| ~ $less(length1(X5),X1)
| ~ path(s,X5,X2) )
& ! [X6: vertex,X7: list_vertex] :
( ~ $less($sum(path_weight(X7,X6),weight(X6,X2)),X3)
| ~ mem2(tuple22(X6,X2),empty2)
| ~ $less(length1(X7),X1)
| ~ path(s,X7,X6) ) )
| ( ( get1(X0,X2) = infinite )
& ! [X8: list_vertex] :
( ~ $less(length1(X8),X1)
| ~ path(s,X8,X2) )
& ! [X9: vertex] :
( ! [X10: list_vertex] :
( ~ $less(length1(X10),X1)
| ~ path(s,X10,X9) )
| ~ mem2(tuple22(X9,X2),empty2) ) )
| ~ mem1(X2,vertices) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(flattening,[],[f356]) ).
tff(f363,definition,
! [X2: vertex,X0: map_vertex_t19,X1: $int] :
( ? [X3: $int] :
( ( get1(X0,X2) = finite(X3) )
& ? [X4: list_vertex] :
( path(s,X4,X2)
& ( path_weight(X4,X2) = X3 ) )
& ! [X5: list_vertex] :
( ~ $less(path_weight(X5,X2),X3)
| ~ $less(length1(X5),X1)
| ~ path(s,X5,X2) )
& ! [X6: vertex,X7: list_vertex] :
( ~ $less($sum(path_weight(X7,X6),weight(X6,X2)),X3)
| ~ mem2(tuple22(X6,X2),empty2)
| ~ $less(length1(X7),X1)
| ~ path(s,X7,X6) ) )
| ~ sP3(X2,X0,X1) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
tff(f364,definition,
! [X15: vertex,X13: map_vertex_t19,X1: $int,X12: set_lpvertexcm_vertexrp] :
( ? [X16: $int] :
( ( finite(X16) = get1(X13,X15) )
& ? [X17: list_vertex] :
( path(s,X17,X15)
& ( path_weight(X17,X15) = X16 ) )
& ! [X18: list_vertex] :
( ~ $less(path_weight(X18,X15),X16)
| ~ $less(length1(X18),X1)
| ~ path(s,X18,X15) )
& ! [X19: vertex,X20: list_vertex] :
( ~ $less($sum(path_weight(X20,X19),weight(X19,X15)),X16)
| ~ mem2(tuple22(X19,X15),diff2(edges,X12))
| ~ $less(length1(X20),X1)
| ~ path(s,X20,X19) ) )
| ~ sP4(X15,X13,X1,X12) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
tff(f365,definition,
! [X30: vertex,X13: map_vertex_t19,X1: $int,X12: set_lpvertexcm_vertexrp] :
( ? [X31: $int] :
( ( finite(X31) = get1(X13,X30) )
& ? [X32: list_vertex] :
( path(s,X32,X30)
& ( path_weight(X32,X30) = X31 ) )
& ! [X33: list_vertex] :
( ~ $less(path_weight(X33,X30),X31)
| ~ $less(length1(X33),X1)
| ~ path(s,X33,X30) )
& ! [X34: vertex,X35: list_vertex] :
( ~ $less($sum(path_weight(X35,X34),weight(X34,X30)),X31)
| ~ mem2(tuple22(X34,X30),diff2(edges,X12))
| ~ $less(length1(X35),X1)
| ~ path(s,X35,X34) ) )
| ~ sP5(X30,X13,X1,X12) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
tff(f366,definition,
! [X40: vertex,X39: map_vertex_t19,X1: $int,X12: set_lpvertexcm_vertexrp,X29: vertex,X28: vertex] :
( ? [X41: $int] :
( ( finite(X41) = get1(X39,X40) )
& ? [X42: list_vertex] :
( path(s,X42,X40)
& ( path_weight(X42,X40) = X41 ) )
& ! [X43: list_vertex] :
( ~ $less(path_weight(X43,X40),X41)
| ~ $less(length1(X43),X1)
| ~ path(s,X43,X40) )
& ! [X44: vertex,X45: list_vertex] :
( ~ $less($sum(path_weight(X45,X44),weight(X44,X40)),X41)
| ~ mem2(tuple22(X44,X40),add2(tuple22(X28,X29),diff2(edges,X12)))
| ~ $less(length1(X45),X1)
| ~ path(s,X45,X44) ) )
| ~ sP6(X40,X39,X1,X12,X29,X28) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
tff(f367,plain,
( ? [X0: map_vertex_t19,X1: $int] :
( ? [X11: set_lpvertexcm_vertexrp] :
( ? [X12: set_lpvertexcm_vertexrp,X13: map_vertex_t19] :
( ? [X24: bool] :
( ? [X27: set_lpvertexcm_vertexrp,X28: vertex,X29: vertex] :
( ? [X39: map_vertex_t19] :
( ? [X49: vertex] :
( ? [X50: $int] :
( ? [X51: vertex,X52: list_vertex] :
( $less($sum(path_weight(X52,X51),weight(X51,X49)),X50)
& mem2(tuple22(X51,X49),diff2(edges,X27))
& $less(length1(X52),X1)
& path(s,X52,X51) )
& ( finite(X50) = get1(X39,X49) ) )
& mem1(X49,vertices) )
& ! [X40: vertex] :
( sP6(X40,X39,X1,X12,X29,X28)
| ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( ~ $less(length1(X46),X1)
| ~ path(s,X46,X40) )
& ! [X47: vertex] :
( ! [X48: list_vertex] :
( ~ $less(length1(X48),X1)
| ~ path(s,X48,X47) )
| ~ mem2(tuple22(X47,X40),add2(tuple22(X28,X29),diff2(edges,X12))) ) )
| ~ mem1(X40,vertices) ) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X28,X29),edges)
& ~ mem2(tuple22(X28,X29),diff2(edges,X12))
& ! [X30: vertex] :
( sP5(X30,X13,X1,X12)
| ( ( infinite = get1(X13,X30) )
& ! [X36: list_vertex] :
( ~ $less(length1(X36),X1)
| ~ path(s,X36,X30) )
& ! [X37: vertex] :
( ! [X38: list_vertex] :
( ~ $less(length1(X38),X1)
| ~ path(s,X38,X37) )
| ~ mem2(tuple22(X37,X30),diff2(edges,X12)) ) )
| ~ mem1(X30,vertices) )
& mem2(tuple22(X28,X29),X12)
& ( remove2(tuple22(X28,X29),X12) = X27 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X12)
& ( true != X24 )
& ( ( true = X24 )
<=> ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X12) ) )
& ! [X14: lpvertexcm_vertexrp] :
( mem2(X14,edges)
| ~ mem2(X14,X12) )
& ! [X15: vertex] :
( sP4(X15,X13,X1,X12)
| ( ( infinite = get1(X13,X15) )
& ! [X21: list_vertex] :
( ~ $less(length1(X21),X1)
| ~ path(s,X21,X15) )
& ! [X22: vertex] :
( ! [X23: list_vertex] :
( ~ $less(length1(X23),X1)
| ~ path(s,X23,X22) )
| ~ mem2(tuple22(X22,X15),diff2(edges,X12)) ) )
| ~ mem1(X15,vertices) ) )
& ( edges = X11 ) )
& ! [X2: vertex] :
( sP3(X2,X0,X1)
| ( ( get1(X0,X2) = infinite )
& ! [X8: list_vertex] :
( ~ $less(length1(X8),X1)
| ~ path(s,X8,X2) )
& ! [X9: vertex] :
( ! [X10: list_vertex] :
( ~ $less(length1(X10),X1)
| ~ path(s,X10,X9) )
| ~ mem2(tuple22(X9,X2),empty2) ) )
| ~ mem1(X2,vertices) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(definition_folding,[],[f357,f366,f365,f364,f363]) ).
tff(f393,plain,
! [X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp] :
( ( mem2(X0,add2(X1,X2))
| ( ( X0 != X1 )
& ~ mem2(X0,X2) ) )
& ( ( X0 = X1 )
| mem2(X0,X2)
| ~ mem2(X0,add2(X1,X2)) ) ),
inference(nnf_transformation,[],[f73]) ).
tff(f394,plain,
! [X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp,X2: set_lpvertexcm_vertexrp] :
( ( mem2(X0,add2(X1,X2))
| ( ( X0 != X1 )
& ~ mem2(X0,X2) ) )
& ( ( X0 = X1 )
| mem2(X0,X2)
| ~ mem2(X0,add2(X1,X2)) ) ),
inference(flattening,[],[f393]) ).
tff(f417,plain,
! [X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp,X2: lpvertexcm_vertexrp] :
( ( mem2(X2,diff2(X0,X1))
| ~ mem2(X2,X0)
| mem2(X2,X1) )
& ( ( mem2(X2,X0)
& ~ mem2(X2,X1) )
| ~ mem2(X2,diff2(X0,X1)) ) ),
inference(nnf_transformation,[],[f98]) ).
tff(f418,plain,
! [X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp,X2: lpvertexcm_vertexrp] :
( ( mem2(X2,diff2(X0,X1))
| ~ mem2(X2,X0)
| mem2(X2,X1) )
& ( ( mem2(X2,X0)
& ~ mem2(X2,X1) )
| ~ mem2(X2,diff2(X0,X1)) ) ),
inference(flattening,[],[f417]) ).
tff(f469,plain,
! [X40: vertex,X39: map_vertex_t19,X1: $int,X12: set_lpvertexcm_vertexrp,X29: vertex,X28: vertex] :
( ? [X41: $int] :
( ( finite(X41) = get1(X39,X40) )
& ? [X42: list_vertex] :
( path(s,X42,X40)
& ( path_weight(X42,X40) = X41 ) )
& ! [X43: list_vertex] :
( ~ $less(path_weight(X43,X40),X41)
| ~ $less(length1(X43),X1)
| ~ path(s,X43,X40) )
& ! [X44: vertex,X45: list_vertex] :
( ~ $less($sum(path_weight(X45,X44),weight(X44,X40)),X41)
| ~ mem2(tuple22(X44,X40),add2(tuple22(X28,X29),diff2(edges,X12)))
| ~ $less(length1(X45),X1)
| ~ path(s,X45,X44) ) )
| ~ sP6(X40,X39,X1,X12,X29,X28) ),
inference(nnf_transformation,[],[f366]) ).
tff(f470,plain,
! [X0: vertex,X1: map_vertex_t19,X2: $int,X3: set_lpvertexcm_vertexrp,X4: vertex,X5: vertex] :
( ? [X6: $int] :
( ( get1(X1,X0) = finite(X6) )
& ? [X7: list_vertex] :
( path(s,X7,X0)
& ( path_weight(X7,X0) = X6 ) )
& ! [X8: list_vertex] :
( ~ $less(path_weight(X8,X0),X6)
| ~ $less(length1(X8),X2)
| ~ path(s,X8,X0) )
& ! [X9: vertex,X10: list_vertex] :
( ~ $less($sum(path_weight(X10,X9),weight(X9,X0)),X6)
| ~ mem2(tuple22(X9,X0),add2(tuple22(X5,X4),diff2(edges,X3)))
| ~ $less(length1(X10),X2)
| ~ path(s,X10,X9) ) )
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(rectify,[],[f469]) ).
tff(f471,plain,
! [X0: vertex,X1: map_vertex_t19,X2: $int,X3: set_lpvertexcm_vertexrp,X4: vertex,X5: vertex] :
( ( ( get1(X1,X0) = finite(sK76(X0,X1,X2,X3,X4,X5)) )
& path(s,sK77(X0,X1,X2,X3,X4,X5),X0)
& ( sK76(X0,X1,X2,X3,X4,X5) = path_weight(sK77(X0,X1,X2,X3,X4,X5),X0) )
& ! [X8: list_vertex] :
( ~ $less(path_weight(X8,X0),sK76(X0,X1,X2,X3,X4,X5))
| ~ $less(length1(X8),X2)
| ~ path(s,X8,X0) )
& ! [X9: vertex,X10: list_vertex] :
( ~ $less($sum(path_weight(X10,X9),weight(X9,X0)),sK76(X0,X1,X2,X3,X4,X5))
| ~ mem2(tuple22(X9,X0),add2(tuple22(X5,X4),diff2(edges,X3)))
| ~ $less(length1(X10),X2)
| ~ path(s,X10,X9) ) )
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76,sK77]),skolemize(X6,sK76(X0,X1,X2,X3,X4,X5)),skolemize(X7,sK77(X0,X1,X2,X3,X4,X5))],[f470]) ).
tff(f481,plain,
( ? [X0: map_vertex_t19,X1: $int] :
( ? [X11: set_lpvertexcm_vertexrp] :
( ? [X12: set_lpvertexcm_vertexrp,X13: map_vertex_t19] :
( ? [X24: bool] :
( ? [X27: set_lpvertexcm_vertexrp,X28: vertex,X29: vertex] :
( ? [X39: map_vertex_t19] :
( ? [X49: vertex] :
( ? [X50: $int] :
( ? [X51: vertex,X52: list_vertex] :
( $less($sum(path_weight(X52,X51),weight(X51,X49)),X50)
& mem2(tuple22(X51,X49),diff2(edges,X27))
& $less(length1(X52),X1)
& path(s,X52,X51) )
& ( finite(X50) = get1(X39,X49) ) )
& mem1(X49,vertices) )
& ! [X40: vertex] :
( sP6(X40,X39,X1,X12,X29,X28)
| ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( ~ $less(length1(X46),X1)
| ~ path(s,X46,X40) )
& ! [X47: vertex] :
( ! [X48: list_vertex] :
( ~ $less(length1(X48),X1)
| ~ path(s,X48,X47) )
| ~ mem2(tuple22(X47,X40),add2(tuple22(X28,X29),diff2(edges,X12))) ) )
| ~ mem1(X40,vertices) ) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X28,X29),edges)
& ~ mem2(tuple22(X28,X29),diff2(edges,X12))
& ! [X30: vertex] :
( sP5(X30,X13,X1,X12)
| ( ( infinite = get1(X13,X30) )
& ! [X36: list_vertex] :
( ~ $less(length1(X36),X1)
| ~ path(s,X36,X30) )
& ! [X37: vertex] :
( ! [X38: list_vertex] :
( ~ $less(length1(X38),X1)
| ~ path(s,X38,X37) )
| ~ mem2(tuple22(X37,X30),diff2(edges,X12)) ) )
| ~ mem1(X30,vertices) )
& mem2(tuple22(X28,X29),X12)
& ( remove2(tuple22(X28,X29),X12) = X27 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X12)
& ( true != X24 )
& ( ( true = X24 )
| ? [X25: lpvertexcm_vertexrp] : mem2(X25,X12) )
& ( ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X12)
| ( true != X24 ) ) )
& ! [X14: lpvertexcm_vertexrp] :
( mem2(X14,edges)
| ~ mem2(X14,X12) )
& ! [X15: vertex] :
( sP4(X15,X13,X1,X12)
| ( ( infinite = get1(X13,X15) )
& ! [X21: list_vertex] :
( ~ $less(length1(X21),X1)
| ~ path(s,X21,X15) )
& ! [X22: vertex] :
( ! [X23: list_vertex] :
( ~ $less(length1(X23),X1)
| ~ path(s,X23,X22) )
| ~ mem2(tuple22(X22,X15),diff2(edges,X12)) ) )
| ~ mem1(X15,vertices) ) )
& ( edges = X11 ) )
& ! [X2: vertex] :
( sP3(X2,X0,X1)
| ( ( get1(X0,X2) = infinite )
& ! [X8: list_vertex] :
( ~ $less(length1(X8),X1)
| ~ path(s,X8,X2) )
& ! [X9: vertex] :
( ! [X10: list_vertex] :
( ~ $less(length1(X10),X1)
| ~ path(s,X10,X9) )
| ~ mem2(tuple22(X9,X2),empty2) ) )
| ~ mem1(X2,vertices) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(nnf_transformation,[],[f367]) ).
tff(f482,plain,
( ? [X0: map_vertex_t19,X1: $int] :
( ? [X11: set_lpvertexcm_vertexrp] :
( ? [X12: set_lpvertexcm_vertexrp,X13: map_vertex_t19] :
( ? [X24: bool] :
( ? [X27: set_lpvertexcm_vertexrp,X28: vertex,X29: vertex] :
( ? [X39: map_vertex_t19] :
( ? [X49: vertex] :
( ? [X50: $int] :
( ? [X51: vertex,X52: list_vertex] :
( $less($sum(path_weight(X52,X51),weight(X51,X49)),X50)
& mem2(tuple22(X51,X49),diff2(edges,X27))
& $less(length1(X52),X1)
& path(s,X52,X51) )
& ( finite(X50) = get1(X39,X49) ) )
& mem1(X49,vertices) )
& ! [X40: vertex] :
( sP6(X40,X39,X1,X12,X29,X28)
| ( ( infinite = get1(X39,X40) )
& ! [X46: list_vertex] :
( ~ $less(length1(X46),X1)
| ~ path(s,X46,X40) )
& ! [X47: vertex] :
( ! [X48: list_vertex] :
( ~ $less(length1(X48),X1)
| ~ path(s,X48,X47) )
| ~ mem2(tuple22(X47,X40),add2(tuple22(X28,X29),diff2(edges,X12))) ) )
| ~ mem1(X40,vertices) ) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X28,X29),edges)
& ~ mem2(tuple22(X28,X29),diff2(edges,X12))
& ! [X30: vertex] :
( sP5(X30,X13,X1,X12)
| ( ( infinite = get1(X13,X30) )
& ! [X36: list_vertex] :
( ~ $less(length1(X36),X1)
| ~ path(s,X36,X30) )
& ! [X37: vertex] :
( ! [X38: list_vertex] :
( ~ $less(length1(X38),X1)
| ~ path(s,X38,X37) )
| ~ mem2(tuple22(X37,X30),diff2(edges,X12)) ) )
| ~ mem1(X30,vertices) )
& mem2(tuple22(X28,X29),X12)
& ( remove2(tuple22(X28,X29),X12) = X27 ) )
& ? [X26: lpvertexcm_vertexrp] : mem2(X26,X12)
& ( true != X24 )
& ( ( true = X24 )
| ? [X25: lpvertexcm_vertexrp] : mem2(X25,X12) )
& ( ! [X25: lpvertexcm_vertexrp] : ~ mem2(X25,X12)
| ( true != X24 ) ) )
& ! [X14: lpvertexcm_vertexrp] :
( mem2(X14,edges)
| ~ mem2(X14,X12) )
& ! [X15: vertex] :
( sP4(X15,X13,X1,X12)
| ( ( infinite = get1(X13,X15) )
& ! [X21: list_vertex] :
( ~ $less(length1(X21),X1)
| ~ path(s,X21,X15) )
& ! [X22: vertex] :
( ! [X23: list_vertex] :
( ~ $less(length1(X23),X1)
| ~ path(s,X23,X22) )
| ~ mem2(tuple22(X22,X15),diff2(edges,X12)) ) )
| ~ mem1(X15,vertices) ) )
& ( edges = X11 ) )
& ! [X2: vertex] :
( sP3(X2,X0,X1)
| ( ( get1(X0,X2) = infinite )
& ! [X8: list_vertex] :
( ~ $less(length1(X8),X1)
| ~ path(s,X8,X2) )
& ! [X9: vertex] :
( ! [X10: list_vertex] :
( ~ $less(length1(X10),X1)
| ~ path(s,X10,X9) )
| ~ mem2(tuple22(X9,X2),empty2) ) )
| ~ mem1(X2,vertices) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(flattening,[],[f481]) ).
tff(f483,plain,
( ? [X0: map_vertex_t19,X1: $int] :
( ? [X2: set_lpvertexcm_vertexrp] :
( ? [X3: set_lpvertexcm_vertexrp,X4: map_vertex_t19] :
( ? [X5: bool] :
( ? [X6: set_lpvertexcm_vertexrp,X7: vertex,X8: vertex] :
( ? [X9: map_vertex_t19] :
( ? [X10: vertex] :
( ? [X11: $int] :
( ? [X12: vertex,X13: list_vertex] :
( $less($sum(path_weight(X13,X12),weight(X12,X10)),X11)
& mem2(tuple22(X12,X10),diff2(edges,X6))
& $less(length1(X13),X1)
& path(s,X13,X12) )
& ( finite(X11) = get1(X9,X10) ) )
& mem1(X10,vertices) )
& ! [X14: vertex] :
( sP6(X14,X9,X1,X3,X8,X7)
| ( ( infinite = get1(X9,X14) )
& ! [X15: list_vertex] :
( ~ $less(length1(X15),X1)
| ~ path(s,X15,X14) )
& ! [X16: vertex] :
( ! [X17: list_vertex] :
( ~ $less(length1(X17),X1)
| ~ path(s,X17,X16) )
| ~ mem2(tuple22(X16,X14),add2(tuple22(X7,X8),diff2(edges,X3))) ) )
| ~ mem1(X14,vertices) ) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& mem2(tuple22(X7,X8),edges)
& ~ mem2(tuple22(X7,X8),diff2(edges,X3))
& ! [X18: vertex] :
( sP5(X18,X4,X1,X3)
| ( ( infinite = get1(X4,X18) )
& ! [X19: list_vertex] :
( ~ $less(length1(X19),X1)
| ~ path(s,X19,X18) )
& ! [X20: vertex] :
( ! [X21: list_vertex] :
( ~ $less(length1(X21),X1)
| ~ path(s,X21,X20) )
| ~ mem2(tuple22(X20,X18),diff2(edges,X3)) ) )
| ~ mem1(X18,vertices) )
& mem2(tuple22(X7,X8),X3)
& ( remove2(tuple22(X7,X8),X3) = X6 ) )
& ? [X22: lpvertexcm_vertexrp] : mem2(X22,X3)
& ( true != X5 )
& ( ( true = X5 )
| ? [X23: lpvertexcm_vertexrp] : mem2(X23,X3) )
& ( ! [X24: lpvertexcm_vertexrp] : ~ mem2(X24,X3)
| ( true != X5 ) ) )
& ! [X25: lpvertexcm_vertexrp] :
( mem2(X25,edges)
| ~ mem2(X25,X3) )
& ! [X26: vertex] :
( sP4(X26,X4,X1,X3)
| ( ( infinite = get1(X4,X26) )
& ! [X27: list_vertex] :
( ~ $less(length1(X27),X1)
| ~ path(s,X27,X26) )
& ! [X28: vertex] :
( ! [X29: list_vertex] :
( ~ $less(length1(X29),X1)
| ~ path(s,X29,X28) )
| ~ mem2(tuple22(X28,X26),diff2(edges,X3)) ) )
| ~ mem1(X26,vertices) ) )
& ( edges = X2 ) )
& ! [X30: vertex] :
( sP3(X30,X0,X1)
| ( ( infinite = get1(X0,X30) )
& ! [X31: list_vertex] :
( ~ $less(length1(X31),X1)
| ~ path(s,X31,X30) )
& ! [X32: vertex] :
( ! [X33: list_vertex] :
( ~ $less(length1(X33),X1)
| ~ path(s,X33,X32) )
| ~ mem2(tuple22(X32,X30),empty2) ) )
| ~ mem1(X30,vertices) )
& ( $less(1,X1)
| ( 1 = X1 ) )
& ( $less(X1,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = X1 ) ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(rectify,[],[f482]) ).
tff(f484,plain,
( $less($sum(path_weight(sK97,sK96),weight(sK96,sK94)),sK95)
& mem2(tuple22(sK96,sK94),diff2(edges,sK90))
& $less(length1(sK97),sK85)
& path(s,sK97,sK96)
& ( finite(sK95) = get1(sK93,sK94) )
& mem1(sK94,vertices)
& ! [X14: vertex] :
( sP6(X14,sK93,sK85,sK87,sK92,sK91)
| ( ( infinite = get1(sK93,X14) )
& ! [X15: list_vertex] :
( ~ $less(length1(X15),sK85)
| ~ path(s,X15,X14) )
& ! [X16: vertex] :
( ! [X17: list_vertex] :
( ~ $less(length1(X17),sK85)
| ~ path(s,X17,X16) )
| ~ mem2(tuple22(X16,X14),add2(tuple22(sK91,sK92),diff2(edges,sK87))) ) )
| ~ mem1(X14,vertices) )
& ( $less(1,sK85)
| ( 1 = sK85 ) )
& mem2(tuple22(sK91,sK92),edges)
& ~ mem2(tuple22(sK91,sK92),diff2(edges,sK87))
& ! [X18: vertex] :
( sP5(X18,sK88,sK85,sK87)
| ( ( infinite = get1(sK88,X18) )
& ! [X19: list_vertex] :
( ~ $less(length1(X19),sK85)
| ~ path(s,X19,X18) )
& ! [X20: vertex] :
( ! [X21: list_vertex] :
( ~ $less(length1(X21),sK85)
| ~ path(s,X21,X20) )
| ~ mem2(tuple22(X20,X18),diff2(edges,sK87)) ) )
| ~ mem1(X18,vertices) )
& mem2(tuple22(sK91,sK92),sK87)
& ( sK90 = remove2(tuple22(sK91,sK92),sK87) )
& mem2(sK98,sK87)
& ( true != sK89 )
& ( ( true = sK89 )
| mem2(sK99,sK87) )
& ( ! [X24: lpvertexcm_vertexrp] : ~ mem2(X24,sK87)
| ( true != sK89 ) )
& ! [X25: lpvertexcm_vertexrp] :
( mem2(X25,edges)
| ~ mem2(X25,sK87) )
& ! [X26: vertex] :
( sP4(X26,sK88,sK85,sK87)
| ( ( infinite = get1(sK88,X26) )
& ! [X27: list_vertex] :
( ~ $less(length1(X27),sK85)
| ~ path(s,X27,X26) )
& ! [X28: vertex] :
( ! [X29: list_vertex] :
( ~ $less(length1(X29),sK85)
| ~ path(s,X29,X28) )
| ~ mem2(tuple22(X28,X26),diff2(edges,sK87)) ) )
| ~ mem1(X26,vertices) )
& ( edges = sK86 )
& ! [X30: vertex] :
( sP3(X30,sK84,sK85)
| ( ( infinite = get1(sK84,X30) )
& ! [X31: list_vertex] :
( ~ $less(length1(X31),sK85)
| ~ path(s,X31,X30) )
& ! [X32: vertex] :
( ! [X33: list_vertex] :
( ~ $less(length1(X33),sK85)
| ~ path(s,X33,X32) )
| ~ mem2(tuple22(X32,X30),empty2) ) )
| ~ mem1(X30,vertices) )
& ( $less(1,sK85)
| ( 1 = sK85 ) )
& ( $less(sK85,$sum(cardinal1(vertices),$uminus(1)))
| ( $sum(cardinal1(vertices),$uminus(1)) = sK85 ) )
& ( $less(1,$sum(cardinal1(vertices),$uminus(1)))
| ( 1 = $sum(cardinal1(vertices),$uminus(1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84,sK85,sK86,sK87,sK88,sK89,sK90,sK91,sK92,sK93,sK94,sK95,sK96,sK97,sK98,sK99]),skolemize(X0,sK84),skolemize(X1,sK85),skolemize(X2,sK86),skolemize(X3,sK87),skolemize(X4,sK88),skolemize(X5,sK89),skolemize(X6,sK90),skolemize(X7,sK91),skolemize(X8,sK92),skolemize(X9,sK93),skolemize(X10,sK94),skolemize(X11,sK95),skolemize(X12,sK96),skolemize(X13,sK97),skolemize(X22,sK98),skolemize(X23,sK99)],[f483]) ).
tff(f582,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( ~ mem2(X0,add2(X1,X2))
| mem2(X0,X2)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f394]) ).
tff(f583,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( mem2(X0,add2(X1,X2))
| ~ mem2(X0,X2) ),
inference(cnf_transformation,[],[f394]) ).
tff(f584,plain,
! [X2: set_lpvertexcm_vertexrp,X0: lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] :
( mem2(X0,add2(X1,X2))
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f394]) ).
tff(f601,plain,
! [X0: lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X0,X1)
| ( add2(X0,remove2(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f281]) ).
tff(f631,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X2,diff2(X0,X1))
| ~ mem2(X2,X1) ),
inference(cnf_transformation,[],[f418]) ).
tff(f632,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( ~ mem2(X2,diff2(X0,X1))
| mem2(X2,X0) ),
inference(cnf_transformation,[],[f418]) ).
tff(f633,plain,
! [X2: lpvertexcm_vertexrp,X0: set_lpvertexcm_vertexrp,X1: set_lpvertexcm_vertexrp] :
( mem2(X2,diff2(X0,X1))
| ~ mem2(X2,X0)
| mem2(X2,X1) ),
inference(cnf_transformation,[],[f418]) ).
tff(f766,plain,
! [X0: $int] : ( infinite != finite(X0) ),
inference(cnf_transformation,[],[f180]) ).
tff(f767,plain,
! [X0: $int] : ( finite_proj_1(finite(X0)) = X0 ),
inference(cnf_transformation,[],[f181]) ).
tff(f811,plain,
! [X2: $int,X3: set_lpvertexcm_vertexrp,X10: list_vertex,X0: vertex,X1: map_vertex_t19,X9: vertex,X4: vertex,X5: vertex] :
( ~ $less($sum(path_weight(X10,X9),weight(X9,X0)),sK76(X0,X1,X2,X3,X4,X5))
| ~ mem2(tuple22(X9,X0),add2(tuple22(X5,X4),diff2(edges,X3)))
| ~ $less(length1(X10),X2)
| ~ path(s,X10,X9)
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[],[f471]) ).
tff(f815,plain,
! [X2: $int,X3: set_lpvertexcm_vertexrp,X0: vertex,X1: map_vertex_t19,X4: vertex,X5: vertex] :
( ~ sP6(X0,X1,X2,X3,X4,X5)
| ( get1(X1,X0) = finite(sK76(X0,X1,X2,X3,X4,X5)) ) ),
inference(cnf_transformation,[],[f471]) ).
tff(f837,plain,
edges = sK86,
inference(cnf_transformation,[],[f484]) ).
tff(f846,plain,
sK90 = remove2(tuple22(sK91,sK92),sK87),
inference(cnf_transformation,[],[f484]) ).
tff(f847,plain,
mem2(tuple22(sK91,sK92),sK87),
inference(cnf_transformation,[],[f484]) ).
tff(f854,plain,
! [X16: vertex,X14: vertex,X17: list_vertex] :
( sP6(X14,sK93,sK85,sK87,sK92,sK91)
| ~ $less(length1(X17),sK85)
| ~ path(s,X17,X16)
| ~ mem2(tuple22(X16,X14),add2(tuple22(sK91,sK92),diff2(edges,sK87)))
| ~ mem1(X14,vertices) ),
inference(cnf_transformation,[],[f484]) ).
tff(f856,plain,
! [X14: vertex] :
( sP6(X14,sK93,sK85,sK87,sK92,sK91)
| ( infinite = get1(sK93,X14) )
| ~ mem1(X14,vertices) ),
inference(cnf_transformation,[],[f484]) ).
tff(f857,plain,
mem1(sK94,vertices),
inference(cnf_transformation,[],[f484]) ).
tff(f858,plain,
finite(sK95) = get1(sK93,sK94),
inference(cnf_transformation,[],[f484]) ).
tff(f859,plain,
path(s,sK97,sK96),
inference(cnf_transformation,[],[f484]) ).
tff(f860,plain,
$less(length1(sK97),sK85),
inference(cnf_transformation,[],[f484]) ).
tff(f861,plain,
mem2(tuple22(sK96,sK94),diff2(edges,sK90)),
inference(cnf_transformation,[],[f484]) ).
tff(f862,plain,
$less($sum(path_weight(sK97,sK96),weight(sK96,sK94)),sK95),
inference(cnf_transformation,[],[f484]) ).
tff(f868,plain,
! [X2: $int,X3: set_lpvertexcm_vertexrp,X10: list_vertex,X0: vertex,X1: map_vertex_t19,X9: vertex,X4: vertex,X5: vertex] :
( ~ $less($sum(path_weight(X10,X9),weight(X9,X0)),sK76(X0,X1,X2,X3,X4,X5))
| ~ mem2(tuple22(X9,X0),add2(tuple22(X5,X4),diff2(sK86,X3)))
| ~ $less(length1(X10),X2)
| ~ path(s,X10,X9)
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(definition_unfolding,[],[f811,f837]) ).
tff(f871,plain,
mem2(tuple22(sK96,sK94),diff2(sK86,sK90)),
inference(definition_unfolding,[],[f861,f837]) ).
tff(f872,plain,
! [X16: vertex,X14: vertex,X17: list_vertex] :
( sP6(X14,sK93,sK85,sK87,sK92,sK91)
| ~ $less(length1(X17),sK85)
| ~ path(s,X17,X16)
| ~ mem2(tuple22(X16,X14),add2(tuple22(sK91,sK92),diff2(sK86,sK87)))
| ~ mem1(X14,vertices) ),
inference(definition_unfolding,[],[f854,f837]) ).
tff(f883,plain,
! [X2: set_lpvertexcm_vertexrp,X1: lpvertexcm_vertexrp] : mem2(X1,add2(X1,X2)),
inference(equality_resolution,[],[f584]) ).
tff(f899,definition,
sF101 = path_weight(sK97,sK96),
introduced(definition,[new_symbols(definition,[sF101])],[function_definition]) ).
tff(f900,plain,
path_weight(sK97,sK96) = sF101,
inference(reorient_equations,[],[f899]) ).
tff(f901,definition,
sF102 = weight(sK96,sK94),
introduced(definition,[new_symbols(definition,[sF102])],[function_definition]) ).
tff(f902,plain,
weight(sK96,sK94) = sF102,
inference(reorient_equations,[],[f901]) ).
tff(f903,definition,
sF103 = $sum(sF101,sF102),
introduced(definition,[new_symbols(definition,[sF103])],[function_definition]) ).
tff(f904,plain,
$sum(sF101,sF102) = sF103,
inference(reorient_equations,[],[f903]) ).
tff(f905,plain,
$less(sF103,sK95),
inference(definition_folding,[],[f862,f904,f902,f900]) ).
tff(f906,definition,
sF104 = tuple22(sK96,sK94),
introduced(definition,[new_symbols(definition,[sF104])],[function_definition]) ).
tff(f907,plain,
tuple22(sK96,sK94) = sF104,
inference(reorient_equations,[],[f906]) ).
tff(f908,definition,
sF105 = diff2(sK86,sK90),
introduced(definition,[new_symbols(definition,[sF105])],[function_definition]) ).
tff(f909,plain,
diff2(sK86,sK90) = sF105,
inference(reorient_equations,[],[f908]) ).
tff(f910,plain,
mem2(sF104,sF105),
inference(definition_folding,[],[f871,f909,f907]) ).
tff(f911,definition,
sF106 = length1(sK97),
introduced(definition,[new_symbols(definition,[sF106])],[function_definition]) ).
tff(f912,plain,
length1(sK97) = sF106,
inference(reorient_equations,[],[f911]) ).
tff(f913,plain,
$less(sF106,sK85),
inference(definition_folding,[],[f860,f912]) ).
tff(f914,definition,
sF107 = finite(sK95),
introduced(definition,[new_symbols(definition,[sF107])],[function_definition]) ).
tff(f915,plain,
finite(sK95) = sF107,
inference(reorient_equations,[],[f914]) ).
tff(f916,definition,
sF108 = get1(sK93,sK94),
introduced(definition,[new_symbols(definition,[sF108])],[function_definition]) ).
tff(f917,plain,
get1(sK93,sK94) = sF108,
inference(reorient_equations,[],[f916]) ).
tff(f918,plain,
sF107 = sF108,
inference(definition_folding,[],[f858,f917,f915]) ).
tff(f919,definition,
sF109 = tuple22(sK91,sK92),
introduced(definition,[new_symbols(definition,[sF109])],[function_definition]) ).
tff(f920,plain,
tuple22(sK91,sK92) = sF109,
inference(reorient_equations,[],[f919]) ).
tff(f921,definition,
sF110 = diff2(sK86,sK87),
introduced(definition,[new_symbols(definition,[sF110])],[function_definition]) ).
tff(f922,plain,
diff2(sK86,sK87) = sF110,
inference(reorient_equations,[],[f921]) ).
tff(f923,definition,
sF111 = add2(sF109,sF110),
introduced(definition,[new_symbols(definition,[sF111])],[function_definition]) ).
tff(f924,plain,
add2(sF109,sF110) = sF111,
inference(reorient_equations,[],[f923]) ).
tff(f925,plain,
! [X16: vertex,X14: vertex,X17: list_vertex] :
( ~ mem2(tuple22(X16,X14),sF111)
| ~ $less(length1(X17),sK85)
| ~ path(s,X17,X16)
| sP6(X14,sK93,sK85,sK87,sK92,sK91)
| ~ mem1(X14,vertices) ),
inference(definition_folding,[],[f872,f924,f922,f920]) ).
tff(f929,plain,
mem2(sF109,sK87),
inference(definition_folding,[],[f847,f920]) ).
tff(f930,definition,
sF112 = remove2(sF109,sK87),
introduced(definition,[new_symbols(definition,[sF112])],[function_definition]) ).
tff(f931,plain,
remove2(sF109,sK87) = sF112,
inference(reorient_equations,[],[f930]) ).
tff(f932,plain,
sK90 = sF112,
inference(definition_folding,[],[f846,f931,f920]) ).
tff(f946,plain,
get1(sK93,sK94) = sF107,
inference(forward_demodulation,[],[f917,f918]) ).
tff(f947,plain,
sK90 = remove2(sF109,sK87),
inference(forward_demodulation,[],[f931,f932]) ).
tff(f976,plain,
infinite != sF107,
inference(superposition,[],[f766,f915]) ).
tff(f979,plain,
sK95 = finite_proj_1(sF107),
inference(superposition,[],[f767,f915]) ).
tff(f981,plain,
! [X2: $int,X3: set_lpvertexcm_vertexrp,X0: vertex,X1: map_vertex_t19,X4: vertex,X5: vertex] :
( ~ $less($sum(sF101,weight(sK96,X0)),sK76(X0,X1,X2,X3,X4,X5))
| ~ mem2(tuple22(sK96,X0),add2(tuple22(X5,X4),diff2(sK86,X3)))
| ~ $less(length1(sK97),X2)
| ~ path(s,sK97,sK96)
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(superposition,[],[f868,f900]) ).
tff(f986,plain,
! [X2: $int,X3: set_lpvertexcm_vertexrp,X0: vertex,X1: map_vertex_t19,X4: vertex,X5: vertex] :
( ~ $less($sum(sF101,weight(sK96,X0)),sK76(X0,X1,X2,X3,X4,X5))
| ~ mem2(tuple22(sK96,X0),add2(tuple22(X5,X4),diff2(sK86,X3)))
| ~ $less(length1(sK97),X2)
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(forward_subsumption_resolution,[],[f981,f859]) ).
tff(f989,plain,
! [X2: $int,X3: set_lpvertexcm_vertexrp,X0: vertex,X1: map_vertex_t19,X4: vertex,X5: vertex] :
( ~ $less($sum(sF101,weight(sK96,X0)),sK76(X0,X1,X2,X3,X4,X5))
| ~ $less(sF106,X2)
| ~ mem2(tuple22(sK96,X0),add2(tuple22(X5,X4),diff2(sK86,X3)))
| ~ sP6(X0,X1,X2,X3,X4,X5) ),
inference(forward_demodulation,[],[f986,f912]) ).
tff(f1007,plain,
! [X0: list_vertex] :
( ~ mem2(sF104,sF111)
| ~ $less(length1(X0),sK85)
| ~ path(s,X0,sK96)
| sP6(sK94,sK93,sK85,sK87,sK92,sK91)
| ~ mem1(sK94,vertices) ),
inference(superposition,[],[f925,f907]) ).
tff(f1012,plain,
! [X0: list_vertex] :
( ~ path(s,X0,sK96)
| ~ $less(length1(X0),sK85)
| ~ mem2(sF104,sF111)
| sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_subsumption_resolution,[],[f1007,f857]) ).
tff(f1024,plain,
mem2(sF109,sF111),
inference(superposition,[],[f883,f924]) ).
tff(f1041,plain,
( ~ $less(length1(sK97),sK85)
| ~ mem2(sF104,sF111)
| sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(resolution,[],[f1012,f859]) ).
tff(f1042,plain,
( ~ $less(sF106,sK85)
| ~ mem2(sF104,sF111)
| sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_demodulation,[],[f1041,f912]) ).
tff(f1043,plain,
( sP6(sK94,sK93,sK85,sK87,sK92,sK91)
| ~ mem2(sF104,sF111) ),
inference(forward_subsumption_resolution,[],[f1042,f913]) ).
tff(f1109,plain,
! [X2: set_lpvertexcm_vertexrp,X3: vertex,X0: map_vertex_t19,X1: $int,X4: vertex] :
( ~ $less($sum(sF101,sF102),sK76(sK94,X0,X1,X2,X3,X4))
| ~ $less(sF106,X1)
| ~ mem2(tuple22(sK96,sK94),add2(tuple22(X4,X3),diff2(sK86,X2)))
| ~ sP6(sK94,X0,X1,X2,X3,X4) ),
inference(superposition,[],[f989,f902]) ).
tff(f1110,plain,
! [X2: set_lpvertexcm_vertexrp,X3: vertex,X0: map_vertex_t19,X1: $int,X4: vertex] :
( ~ $less(sF103,sK76(sK94,X0,X1,X2,X3,X4))
| ~ $less(sF106,X1)
| ~ mem2(tuple22(sK96,sK94),add2(tuple22(X4,X3),diff2(sK86,X2)))
| ~ sP6(sK94,X0,X1,X2,X3,X4) ),
inference(forward_demodulation,[],[f1109,f904]) ).
tff(f1111,plain,
! [X2: set_lpvertexcm_vertexrp,X3: vertex,X0: map_vertex_t19,X1: $int,X4: vertex] :
( ~ $less(sF103,sK76(sK94,X0,X1,X2,X3,X4))
| ~ mem2(sF104,add2(tuple22(X4,X3),diff2(sK86,X2)))
| ~ $less(sF106,X1)
| ~ sP6(sK94,X0,X1,X2,X3,X4) ),
inference(forward_demodulation,[],[f1110,f907]) ).
tff(f1198,plain,
! [X0: lpvertexcm_vertexrp] :
( ~ mem2(X0,sF110)
| mem2(X0,sF111) ),
inference(superposition,[],[f583,f924]) ).
tff(f1207,plain,
! [X0: lpvertexcm_vertexrp] :
( ~ mem2(X0,sF105)
| ~ mem2(X0,sK90) ),
inference(superposition,[],[f631,f909]) ).
tff(f1212,plain,
! [X0: lpvertexcm_vertexrp] :
( ~ mem2(X0,sF105)
| mem2(X0,sK86) ),
inference(superposition,[],[f632,f909]) ).
tff(f1221,plain,
~ mem2(sF104,sK90),
inference(resolution,[],[f1207,f910]) ).
tff(f1228,plain,
mem2(sF104,sK86),
inference(resolution,[],[f1212,f910]) ).
tff(f1639,plain,
sK87 = add2(sF109,remove2(sF109,sK87)),
inference(resolution,[],[f601,f929]) ).
tff(f1642,plain,
sK87 = add2(sF109,sK90),
inference(forward_demodulation,[],[f1639,f947]) ).
tff(f1977,plain,
! [X0: lpvertexcm_vertexrp] :
( ~ mem2(X0,sK87)
| mem2(X0,sK90)
| ( sF109 = X0 ) ),
inference(superposition,[],[f582,f1642]) ).
tff(f2049,plain,
! [X0: lpvertexcm_vertexrp] :
( ~ mem2(X0,sK86)
| mem2(X0,sF110)
| mem2(X0,sK87) ),
inference(superposition,[],[f633,f922]) ).
tff(f4046,plain,
! [X0: vertex] :
( ~ mem1(X0,vertices)
| ( infinite = get1(sK93,X0) )
| ( get1(sK93,X0) = finite(sK76(X0,sK93,sK85,sK87,sK92,sK91)) ) ),
inference(resolution,[],[f815,f856]) ).
tff(f5708,plain,
( ( infinite = get1(sK93,sK94) )
| ( get1(sK93,sK94) = finite(sK76(sK94,sK93,sK85,sK87,sK92,sK91)) ) ),
inference(resolution,[],[f4046,f857]) ).
tff(f5713,plain,
( ( infinite = sF107 )
| ( get1(sK93,sK94) = finite(sK76(sK94,sK93,sK85,sK87,sK92,sK91)) ) ),
inference(forward_demodulation,[],[f5708,f946]) ).
tff(f5714,plain,
get1(sK93,sK94) = finite(sK76(sK94,sK93,sK85,sK87,sK92,sK91)),
inference(forward_subsumption_resolution,[],[f5713,f976]) ).
tff(f5715,plain,
sF107 = finite(sK76(sK94,sK93,sK85,sK87,sK92,sK91)),
inference(forward_demodulation,[],[f5714,f946]) ).
tff(f5729,plain,
finite_proj_1(sF107) = sK76(sK94,sK93,sK85,sK87,sK92,sK91),
inference(superposition,[],[f767,f5715]) ).
tff(f5749,plain,
sK95 = sK76(sK94,sK93,sK85,sK87,sK92,sK91),
inference(forward_demodulation,[],[f5729,f979]) ).
tff(f5762,plain,
( ~ $less(sF103,sK95)
| ~ mem2(sF104,add2(tuple22(sK91,sK92),diff2(sK86,sK87)))
| ~ $less(sF106,sK85)
| ~ sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(superposition,[],[f1111,f5749]) ).
tff(f5772,plain,
( ~ mem2(sF104,add2(tuple22(sK91,sK92),diff2(sK86,sK87)))
| ~ $less(sF106,sK85)
| ~ sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_subsumption_resolution,[],[f5762,f905]) ).
tff(f5779,plain,
( ~ mem2(sF104,add2(tuple22(sK91,sK92),diff2(sK86,sK87)))
| ~ sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_subsumption_resolution,[],[f5772,f913]) ).
tff(f5786,plain,
( ~ mem2(sF104,add2(tuple22(sK91,sK92),sF110))
| ~ sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_demodulation,[],[f5779,f922]) ).
tff(f5790,plain,
( ~ mem2(sF104,add2(sF109,sF110))
| ~ sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_demodulation,[],[f5786,f920]) ).
tff(f5794,plain,
( ~ mem2(sF104,sF111)
| ~ sP6(sK94,sK93,sK85,sK87,sK92,sK91) ),
inference(forward_demodulation,[],[f5790,f924]) ).
tff(f5796,plain,
~ mem2(sF104,sF111),
inference(forward_subsumption_resolution,[],[f5794,f1043]) ).
tff(f9201,plain,
( mem2(sF104,sF110)
| mem2(sF104,sK87) ),
inference(resolution,[],[f2049,f1228]) ).
tff(f9230,plain,
( mem2(sF104,sK87)
| mem2(sF104,sF111) ),
inference(resolution,[],[f9201,f1198]) ).
tff(f9236,plain,
mem2(sF104,sK87),
inference(forward_subsumption_resolution,[],[f9230,f5796]) ).
tff(f9243,plain,
( mem2(sF104,sK90)
| ( sF104 = sF109 ) ),
inference(resolution,[],[f9236,f1977]) ).
tff(f9250,plain,
sF104 = sF109,
inference(forward_subsumption_resolution,[],[f9243,f1221]) ).
tff(f9290,plain,
~ mem2(sF109,sF111),
inference(superposition,[],[f5796,f9250]) ).
tff(f9296,plain,
$false,
inference(forward_subsumption_resolution,[],[f9290,f1024]) ).
%------------------------------------------------------------------------------
%----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/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n009.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:20:00 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.24/0.94 % (3057314)Will run a generic schedule for satisfiability detection.
% 4.24/0.94 % (3057320)% WARNING: option uhcvi not known.
% 4.24/0.94 % (3057320)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3659276578:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.24/0.94 % (3057319)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4120719023_2999 on theBenchmark for (2999ds/0Mi)
% 4.24/0.94 % (3057321)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1767324779:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.24/0.94 % (3057324)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3854726575:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.24/0.94 % (3057322)dis+10_1_sil=32000:sp=arity:random_seed=3327567515:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.24/0.94 % (3057323)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2399726500:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.24/0.94 % (3057325)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2017860326:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.24/0.94 % (3057319)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.24/0.94 % (3057319)Terminated due to inappropriate strategy.
% 4.24/0.94 % (3057319)------------------------------
% 4.24/0.94 % (3057319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.24/0.94 % (3057319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.24/0.94 % (3057319)CaDiCaL version: 2.1.3
% 4.24/0.94 % (3057319)Termination reason: Inappropriate
% 4.24/0.94 % (3057319)Time elapsed: 0.015 s
% 4.24/0.94 % (3057319)Peak memory usage: 11 MB
% 4.24/0.94 % (3057319)Instructions burned: 27 (million)
% 4.24/0.94 % (3057319)------------------------------
% 4.24/0.94 % (3057319)------------------------------
% 4.24/0.94 % (3057333)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2940031668:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.24/0.94 % (3057333)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.24/0.94 % (3057333)Terminated due to inappropriate strategy.
% 4.24/0.94 % (3057333)------------------------------
% 4.24/0.94 % (3057333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.24/0.94 % (3057333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.24/0.94 % (3057333)CaDiCaL version: 2.1.3
% 4.24/0.94 % (3057333)Termination reason: Inappropriate
% 4.24/0.94 % (3057333)Time elapsed: 0.016 s
% 4.24/0.94 % (3057333)Peak memory usage: 11 MB
% 4.24/0.94 % (3057333)Instructions burned: 22 (million)
% 4.24/0.94 % (3057333)------------------------------
% 4.24/0.94 % (3057333)------------------------------
% 4.24/0.94 % (3057343)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2074393813:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.24/0.94 % (3057322)Instruction limit reached!
% 4.24/0.94 % (3057322)------------------------------
% 4.24/0.94 % (3057322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.24/0.94 % (3057322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.24/0.94 % (3057322)CaDiCaL version: 2.1.3
% 4.24/0.94 % (3057322)Termination reason: Instruction limit
% 4.24/0.94 % (3057322)Termination phase: Saturation
% 4.24/0.94 % (3057322)Time elapsed: 0.081 s
% 4.24/0.94 % (3057322)Peak memory usage: 13 MB
% 4.24/0.94 % (3057322)Instructions burned: 103 (million)
% 4.24/0.94 % (3057323)Instruction limit reached!
% 4.24/0.94 % (3057323)------------------------------
% 4.24/0.94 % (3057323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.24/0.94 % (3057323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.24/0.94 % (3057323)CaDiCaL version: 2.1.3
% 4.24/0.94 % (3057323)Termination reason: Instruction limit
% 4.24/0.94 % (3057323)Termination phase: Saturation
% 4.24/0.94 % (3057323)Time elapsed: 0.110 s
% 4.24/0.94 % (3057323)Peak memory usage: 13 MB
% 4.24/0.94 % (3057323)Instructions burned: 116 (million)
% 4.24/0.94 % (3057324)Instruction limit reached!
% 4.24/0.94 % (3057324)------------------------------
% 4.24/0.94 % (3057324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.24/0.94 % (3057324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.24/0.94 % (3057324)CaDiCaL version: 2.1.3
% 4.24/0.94 % (3057324)Termination reason: Instruction limit
% 8.23/1.59 % (3057324)Termination phase: Saturation
% 8.23/1.59 % (3057324)Time elapsed: 0.113 s
% 8.23/1.59 % (3057324)Peak memory usage: 14 MB
% 8.23/1.59 % (3057324)Instructions burned: 132 (million)
% 8.23/1.59 % (3057345)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4255639939:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.23/1.59 % (3057325)Instruction limit reached!
% 8.23/1.59 % (3057325)------------------------------
% 8.23/1.59 % (3057325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/1.59 % (3057325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/1.59 % (3057346)ott-21_1_sil=16000:fs=off:random_seed=3731175270:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.23/1.59 % (3057325)CaDiCaL version: 2.1.3
% 8.23/1.59 % (3057325)Termination reason: Instruction limit
% 8.23/1.59 % (3057325)Termination phase: Saturation
% 8.23/1.59 % (3057325)Time elapsed: 0.143 s
% 8.23/1.59 % (3057325)Peak memory usage: 14 MB
% 8.23/1.59 % (3057325)Instructions burned: 159 (million)
% 8.23/1.59 % (3057347)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2759961566:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.23/1.59 % (3057351)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3708131130:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.23/1.59 % (3057343)Instruction limit reached!
% 8.23/1.59 % (3057343)------------------------------
% 8.23/1.59 % (3057343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/1.59 % (3057343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/1.59 % (3057343)CaDiCaL version: 2.1.3
% 8.23/1.59 % (3057343)Termination reason: Instruction limit
% 8.23/1.59 % (3057343)Termination phase: Saturation
% 8.23/1.59 % (3057343)Time elapsed: 0.097 s
% 8.23/1.59 % (3057343)Peak memory usage: 14 MB
% 8.23/1.59 % (3057343)Instructions burned: 131 (million)
% 8.23/1.59 % (3057351)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.23/1.59 % (3057351)Terminated due to inappropriate strategy.
% 8.23/1.59 % (3057351)------------------------------
% 8.23/1.59 % (3057351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/1.59 % (3057351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/1.59 % (3057351)CaDiCaL version: 2.1.3
% 8.23/1.59 % (3057351)Termination reason: Inappropriate
% 8.23/1.59 % (3057351)Time elapsed: 0.011 s
% 8.23/1.59 % (3057351)Peak memory usage: 11 MB
% 8.23/1.59 % (3057351)Instructions burned: 22 (million)
% 8.23/1.59 % (3057351)------------------------------
% 8.23/1.59 % (3057351)------------------------------
% 8.23/1.59 % (3057353)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4129550547:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.23/1.59 % (3057354)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3021299957:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.23/1.59 % (3057354)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.23/1.59 % (3057354)Terminated due to inappropriate strategy.
% 8.23/1.59 % (3057354)------------------------------
% 8.23/1.59 % (3057354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/1.59 % (3057354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/1.59 % (3057354)CaDiCaL version: 2.1.3
% 8.23/1.59 % (3057354)Termination reason: Inappropriate
% 8.23/1.59 % (3057354)Time elapsed: 0.020 s
% 8.23/1.59 % (3057354)Peak memory usage: 11 MB
% 8.23/1.59 % (3057354)Instructions burned: 22 (million)
% 8.23/1.59 % (3057354)------------------------------
% 8.23/1.59 % (3057354)------------------------------
% 8.23/1.59 % (3057360)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2733464269:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 8.23/1.59 % (3057346)Instruction limit reached!
% 8.23/1.59 % (3057346)------------------------------
% 8.23/1.59 % (3057346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.23/1.59 % (3057346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.23/1.59 % (3057346)CaDiCaL version: 2.1.3
% 8.23/1.59 % (3057346)Termination reason: Instruction limit
% 8.23/1.59 % (3057346)Termination phase: Saturation
% 10.68/2.03 % (3057346)Time elapsed: 0.161 s
% 10.68/2.03 % (3057346)Peak memory usage: 13 MB
% 10.68/2.03 % (3057346)Instructions burned: 180 (million)
% 10.68/2.03 % (3057369)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2200946049:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 10.68/2.03 % (3057360)Instruction limit reached!
% 10.68/2.03 % (3057360)------------------------------
% 10.68/2.03 % (3057360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057360)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057360)Termination reason: Instruction limit
% 10.68/2.03 % (3057360)Termination phase: Saturation
% 10.68/2.03 % (3057360)Time elapsed: 0.294 s
% 10.68/2.03 % (3057360)Peak memory usage: 20 MB
% 10.68/2.03 % (3057360)Instructions burned: 692 (million)
% 10.68/2.03 % (3057380)fmb+10_1_sil=64000:random_seed=1825774921:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 10.68/2.03 % (3057380)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.68/2.03 % (3057380)Terminated due to inappropriate strategy.
% 10.68/2.03 % (3057380)------------------------------
% 10.68/2.03 % (3057380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057380)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057380)Termination reason: Inappropriate
% 10.68/2.03 % (3057380)Time elapsed: 0.014 s
% 10.68/2.03 % (3057380)Peak memory usage: 11 MB
% 10.68/2.03 % (3057380)Instructions burned: 25 (million)
% 10.68/2.03 % (3057380)------------------------------
% 10.68/2.03 % (3057380)------------------------------
% 10.68/2.03 % (3057385)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4245958594:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 10.68/2.03 % (3057345)Instruction limit reached!
% 10.68/2.03 % (3057345)------------------------------
% 10.68/2.03 % (3057345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057345)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057345)Termination reason: Instruction limit
% 10.68/2.03 % (3057345)Termination phase: Saturation
% 10.68/2.03 % (3057345)Time elapsed: 0.488 s
% 10.68/2.03 % (3057345)Peak memory usage: 15 MB
% 10.68/2.03 % (3057345)Instructions burned: 685 (million)
% 10.68/2.03 % (3057385)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.68/2.03 % (3057385)Terminated due to inappropriate strategy.
% 10.68/2.03 % (3057385)------------------------------
% 10.68/2.03 % (3057385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057385)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057385)Termination reason: Inappropriate
% 10.68/2.03 % (3057385)Time elapsed: 0.012 s
% 10.68/2.03 % (3057385)Peak memory usage: 11 MB
% 10.68/2.03 % (3057385)Instructions burned: 22 (million)
% 10.68/2.03 % (3057385)------------------------------
% 10.68/2.03 % (3057385)------------------------------
% 10.68/2.03 % (3057389)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1250551627:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 10.68/2.03 % (3057388)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3547665292:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 10.68/2.03 % (3057347)Instruction limit reached!
% 10.68/2.03 % (3057347)------------------------------
% 10.68/2.03 % (3057347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057347)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057347)Termination reason: Instruction limit
% 10.68/2.03 % (3057347)Termination phase: Saturation
% 10.68/2.03 % (3057347)Time elapsed: 0.492 s
% 10.68/2.03 % (3057347)Peak memory usage: 15 MB
% 10.68/2.03 % (3057347)Instructions burned: 477 (million)
% 10.68/2.03 % (3057388)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.68/2.03 % (3057388)Terminated due to inappropriate strategy.
% 10.68/2.03 % (3057388)------------------------------
% 10.68/2.03 % (3057388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057388)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057388)Termination reason: Inappropriate
% 10.68/2.03 % (3057388)Time elapsed: 0.018 s
% 10.68/2.03 % (3057388)Peak memory usage: 11 MB
% 10.68/2.03 % (3057388)Instructions burned: 22 (million)
% 10.68/2.03 % (3057388)------------------------------
% 10.68/2.03 % (3057388)------------------------------
% 10.68/2.03 % (3057392)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4205545442:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 10.68/2.03 % (3057394)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1508270604:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 10.68/2.03 % (3057394)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.68/2.03 % (3057394)Terminated due to inappropriate strategy.
% 10.68/2.03 % (3057394)------------------------------
% 10.68/2.03 % (3057394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057394)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057394)Termination reason: Inappropriate
% 10.68/2.03 % (3057394)Time elapsed: 0.015 s
% 10.68/2.03 % (3057394)Peak memory usage: 11 MB
% 10.68/2.03 % (3057394)Instructions burned: 27 (million)
% 10.68/2.03 % (3057394)------------------------------
% 10.68/2.03 % (3057394)------------------------------
% 10.68/2.03 % (3057397)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1378783564:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 10.68/2.03 % (3057397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.68/2.03 % (3057397)Terminated due to inappropriate strategy.
% 10.68/2.03 % (3057397)------------------------------
% 10.68/2.03 % (3057397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057397)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057397)Termination reason: Inappropriate
% 10.68/2.03 % (3057397)Time elapsed: 0.017 s
% 10.68/2.03 % (3057397)Peak memory usage: 11 MB
% 10.68/2.03 % (3057397)Instructions burned: 22 (million)
% 10.68/2.03 % (3057397)------------------------------
% 10.68/2.03 % (3057397)------------------------------
% 10.68/2.03 % (3057404)ott-2_1_sil=16000:newcnf=on:random_seed=3108730451:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 10.68/2.03 % (3057369)Instruction limit reached!
% 10.68/2.03 % (3057369)------------------------------
% 10.68/2.03 % (3057369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057369)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057369)Termination reason: Instruction limit
% 10.68/2.03 % (3057369)Termination phase: Saturation
% 10.68/2.03 % (3057369)Time elapsed: 0.743 s
% 10.68/2.03 % (3057369)Peak memory usage: 19 MB
% 10.68/2.03 % (3057369)Instructions burned: 879 (million)
% 10.68/2.03 % (3057423)ott+10_1_sil=32000:tgt=ground:random_seed=1121860524:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 10.68/2.03 % (3057353)Instruction limit reached!
% 10.68/2.03 % (3057353)------------------------------
% 10.68/2.03 % (3057353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057353)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057353)Termination reason: Instruction limit
% 10.68/2.03 % (3057353)Termination phase: Saturation
% 10.68/2.03 % (3057353)Time elapsed: 1.049 s
% 10.68/2.03 % (3057353)Peak memory usage: 24 MB
% 10.68/2.03 % (3057353)Instructions burned: 1180 (million)
% 10.68/2.03 % (3057434)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2511209806:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 10.68/2.03 % (3057434)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 10.68/2.03 % (3057434)Terminated due to inappropriate strategy.
% 10.68/2.03 % (3057434)------------------------------
% 10.68/2.03 % (3057434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057434)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057434)Termination reason: Inappropriate
% 10.68/2.03 % (3057434)Time elapsed: 0.016 s
% 10.68/2.03 % (3057434)Peak memory usage: 11 MB
% 10.68/2.03 % (3057434)Instructions burned: 27 (million)
% 10.68/2.03 % (3057434)------------------------------
% 10.68/2.03 % (3057434)------------------------------
% 10.68/2.03 % (3057440)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2703249456:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 10.68/2.03 % (3057404)Instruction limit reached!
% 10.68/2.03 % (3057404)------------------------------
% 10.68/2.03 % (3057404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.03 % (3057404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.03 % (3057404)CaDiCaL version: 2.1.3
% 10.68/2.03 % (3057404)Termination reason: Instruction limit
% 10.68/2.03 % (3057404)Termination phase: Saturation
% 10.68/2.03 % (3057404)Time elapsed: 0.693 s
% 10.68/2.03 % (3057404)Peak memory usage: 16 MB
% 10.68/2.03 % (3057404)Instructions burned: 870 (million)
% 10.68/2.03 % (3057443)dis+21_1_sil=32000:sas=cadical:random_seed=4156163609:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi)
% 10.68/2.03 % (3057423) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3057314-3057423"...
% 10.68/2.03 % (3057423)...printing done.
% 10.68/2.03 % (3057423)Refutation found. Thanks to Tanya!
% 10.68/2.03 % SZS status Theorem for theBenchmark
% 10.68/2.03 % SZS output start Proof for theBenchmark
% See solution above
% 10.68/2.04 % (3057423)------------------------------
% 10.68/2.04 % (3057423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.68/2.04 % (3057423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.04 % (3057423)CaDiCaL version: 2.1.3
% 10.68/2.04 % (3057423)Termination reason: Refutation
% 10.68/2.04 % (3057423)Time elapsed: 0.601 s
% 10.68/2.04 % (3057423)Peak memory usage: 19 MB
% 10.68/2.04 % (3057423)Instructions burned: 633 (million)
% 10.68/2.04 % (3057314)Success in time 1.789 s
% 10.68/2.04 % Vampire exiting
%------------------------------------------------------------------------------