|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
imputations.prf
Sprache: Lisp
Untersuchungsergebnis.summary Download desMT940 {MT940[510] Hlasm[2010] Haskell[2338]}zum Wurzelverzeichnis wechseln
***
*** top (19:14:20 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory graphs
edg_TCC1..............................proved - complete [shostak](0.03 s)
edge?_TCC1............................proved - complete [shostak](0.07 s)
edge?_comm............................proved - complete [shostak](0.03 s)
edges_vert............................proved - complete [shostak](0.07 s)
other_vert............................proved - complete [shostak](0.06 s)
edge_has_2_verts......................proved - complete [shostak](0.04 s)
edges_vert_in.........................proved - complete [shostak](0.03 s)
vert_in...............................proved - complete [shostak](0.04 s)
empty?_rew............................proved - complete [shostak](0.02 s)
edges_of_empty........................proved - complete [shostak](0.04 s)
singleton_edges.......................proved - complete [shostak](0.05 s)
edge_in_card_gt_1.....................proved - complete [shostak](0.11 s)
not_singleton_2_vert..................proved - complete [shostak](0.04 s)
singleton_graph_TCC1..................proved - complete [shostak](0.02 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.65 s)
Proof summary for theory doubletons
dbl_comm..............................proved - complete [shostak](0.01 s)
doubleton_irreflexive.................proved - complete [shostak](0.02 s)
doubleton_nonempty....................proved - complete [shostak](0.01 s)
doubleton_rest_nonempty...............proved - complete [shostak](0.03 s)
dbl_choose_TCC1.......................proved - complete [shostak](0.02 s)
dbl_choose............................proved - complete [shostak](0.02 s)
dbl_rest_choose_TCC1..................proved - complete [shostak](0.01 s)
dbl_rest_choose.......................proved - complete [shostak](0.10 s)
dbl_to_pair_TCC1......................proved - complete [shostak](0.03 s)
dbl_def...............................proved - complete [shostak](0.00 s)
dbl_in................................proved - complete [shostak](0.01 s)
dbl_not_in............................proved - complete [shostak](0.00 s)
dbl_to_pair_lem_TCC1..................proved - complete [shostak](0.01 s)
dbl_to_pair_lem.......................proved - complete [shostak](0.08 s)
dbl_to_pair_inverse_l.................proved - complete [shostak](0.01 s)
dbl_proj..............................proved - complete [shostak](0.01 s)
proj_dbl..............................proved - complete [shostak](0.01 s)
dbl_eq................................proved - complete [shostak](0.04 s)
finite_dbl............................proved - complete [shostak](0.04 s)
finite_doubleton......................proved - complete [shostak](0.00 s)
card_dbl_TCC1.........................proved - complete [shostak](0.01 s)
card_dbl..............................proved - complete [shostak](0.07 s)
dbl_TCC1..............................proved - complete [shostak](0.00 s)
rev_TCC1..............................proved - complete [shostak](0.00 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (0.56 s)
Proof summary for theory graph_deg
incident_edges_TCC1...................proved - complete [shostak](0.04 s)
incident_edges_subset.................proved - complete [shostak](0.03 s)
incident_edges_emptyset...............proved - complete [shostak](0.03 s)
deg_del_edge..........................proved - complete [shostak](0.14 s)
deg_del_edge2.........................proved - complete [shostak](0.05 s)
deg_del_edge3.........................proved - complete [shostak](0.06 s)
deg_del_edge_ge.......................proved - complete [shostak](0.06 s)
deg_del_edge_le.......................proved - complete [shostak](0.05 s)
deg_edge_exists.......................proved - complete [shostak](0.03 s)
deg_to_card...........................proved - complete [shostak](0.11 s)
del_vert_deg_0........................proved - complete [shostak](0.06 s)
deg_del_vert_TCC1.....................proved - complete [shostak](0.02 s)
deg_del_vert..........................proved - complete [shostak](0.17 s)
del_vert_not_incident.................proved - complete [shostak](0.06 s)
singleton_deg.........................proved - complete [shostak](0.05 s)
deg_1_sing............................proved - complete [shostak](0.05 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (1.02 s)
Proof summary for theory graph_ops
union_TCC1............................proved - complete [shostak](0.04 s)
del_vert_TCC1.........................proved - complete [shostak](0.04 s)
del_vert_TCC2.........................proved - complete [shostak](0.07 s)
del_edge_TCC1.........................proved - complete [shostak](0.03 s)
adjacent_TCC1.........................proved - complete [shostak](0.05 s)
del_vert_still_in.....................proved - complete [shostak](0.02 s)
size_del_vert.........................proved - complete [shostak](0.04 s)
del_vert_le...........................proved - complete [shostak](0.05 s)
del_vert_ge...........................proved - complete [shostak](0.04 s)
edge_in_del_vert......................proved - complete [shostak](0.02 s)
edges_del_vert........................proved - complete [shostak](0.02 s)
del_vert_comm.........................proved - complete [shostak](0.08 s)
del_vert_empty?.......................proved - complete [shostak](0.05 s)
del_edge_lem..........................proved - complete [shostak](0.01 s)
del_edge_lem2.........................proved - complete [shostak](0.03 s)
del_edge_lem3.........................proved - complete [shostak](0.03 s)
del_edge_lem5.........................proved - complete [shostak](0.06 s)
vert_del_edge.........................proved - complete [shostak](0.02 s)
del_edge_num..........................proved - complete [shostak](0.08 s)
del_edge_singleton....................proved - complete [shostak](0.03 s)
del_vert_edge_comm....................proved - complete [shostak](0.07 s)
del_vert_edge.........................proved - complete [shostak](0.07 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (0.95 s)
Proof summary for theory graph_deg_sum
deg_lem0..............................proved - incomplete [shostak](0.14 s)
deg_lem2_TCC1.........................proved - complete [shostak](0.03 s)
deg_lem2..............................proved - incomplete [shostak](0.17 s)
edge_induction........................proved - complete [shostak](0.14 s)
deg_thm...............................proved - incomplete [shostak](0.67 s)
subgraph_deg..........................proved - complete [shostak](0.37 s)
sum_gt_bound..........................proved - incomplete [shostak](0.20 s)
deg_gt_one............................proved - incomplete [shostak](0.13 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.85 s)
Proof summary for theory subgraphs
finite_vert_subset....................proved - complete [shostak](0.04 s)
subgraph_TCC1.........................proved - complete [shostak](0.05 s)
subgraph_TCC2.........................proved - complete [shostak](0.02 s)
subgraph_TCC3.........................proved - complete [shostak](0.05 s)
subgraph_vert_sub.....................proved - complete [shostak](0.04 s)
subgraph_lem..........................proved - complete [shostak](0.02 s)
subgraph_smaller......................proved - complete [shostak](0.04 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.25 s)
Proof summary for theory walks
walk?_TCC1............................proved - complete [shostak](0.04 s)
walk?_TCC2............................proved - complete [shostak](0.06 s)
list2prewalk_TCC1.....................proved - complete [shostak](0.01 s)
from?_TCC1............................proved - complete [shostak](0.02 s)
from?_TCC2............................proved - complete [shostak](0.01 s)
verts_of_TCC1.........................proved - incomplete [shostak](0.13 s)
edges_of_TCC1.........................proved - complete [shostak](0.02 s)
edges_of_TCC2.........................proved - complete [shostak](0.01 s)
edges_of_TCC3.........................proved - complete [shostak](0.12 s)
pre_circuit?_TCC1.....................proved - complete [shostak](0.05 s)
pre_circuit?_TCC2.....................proved - complete [shostak](0.05 s)
verts_in?_concat_TCC1.................proved - complete [shostak](0.06 s)
verts_in?_concat......................proved - complete [shostak](0.11 s)
verts_in?_caret_TCC1..................proved - complete [shostak](0.11 s)
verts_in?_caret.......................proved - complete [shostak](0.23 s)
vert_seq_lem..........................proved - complete [shostak](0.03 s)
verts_of_subset.......................proved - incomplete [shostak](0.04 s)
edges_of_subset.......................proved - complete [shostak](0.07 s)
walk_verts_in.........................proved - complete [shostak](0.02 s)
walk_from_vert........................proved - complete [shostak](0.03 s)
walk_edge_in..........................proved - incomplete [shostak](0.11 s)
gen_seq1_TCC1.........................proved - complete [shostak](0.02 s)
gen_seq2_TCC1.........................proved - complete [shostak](0.02 s)
trunc1_TCC1...........................proved - complete [shostak](0.02 s)
trunc1_TCC2...........................proved - complete [shostak](0.09 s)
add1_TCC1.............................proved - complete [shostak](0.02 s)
gen_seq1_is_walk......................proved - complete [shostak](0.02 s)
edge_to_walk_TCC1.....................proved - complete [shostak](0.02 s)
edge_to_walk_TCC2.....................proved - complete [shostak](0.03 s)
edge_to_walk_TCC3.....................proved - complete [shostak](0.03 s)
edge_to_walk..........................proved - complete [shostak](0.05 s)
walk?_rev_TCC1........................proved - complete [shostak](0.07 s)
walk?_rev.............................proved - complete [shostak](0.11 s)
walk?_reverse.........................proved - complete [shostak](0.11 s)
walk?_caret_TCC1......................proved - complete [shostak](0.18 s)
walk?_caret...........................proved - complete [shostak](0.24 s)
l_trunc1_TCC1.........................proved - complete [shostak](0.02 s)
l_trunc1..............................proved - complete [shostak](0.09 s)
walk?_add1............................proved - complete [shostak](0.10 s)
walk_concat_edge_TCC1.................proved - complete [shostak](0.11 s)
walk_concat_edge......................proved - complete [shostak](0.25 s)
walk_concat_TCC1......................proved - complete [shostak](0.13 s)
walk_concat_TCC2......................proved - complete [shostak](0.17 s)
walk_concat...........................proved - complete [shostak](0.52 s)
walk?_cut_TCC1........................proved - complete [shostak](0.05 s)
walk?_cut_TCC2........................proved - complete [shostak](0.18 s)
walk?_cut.............................proved - complete [shostak](1.04 s)
walk_merge............................proved - complete [shostak](0.63 s)
Theory totals: 48 formulas, 48 attempted, 48 succeeded (5.62 s)
Proof summary for theory paths
path?_verts...........................proved - complete [shostak](0.05 s)
path_from_l...........................proved - complete [shostak](0.05 s)
path_from_in..........................proved - complete [shostak](0.06 s)
path?_caret_TCC1......................proved - complete [shostak](0.21 s)
path?_caret...........................proved - complete [shostak](0.43 s)
path_from?_caret_TCC1.................proved - complete [shostak](0.23 s)
path_from?_caret_TCC2.................proved - complete [shostak](0.14 s)
path_from?_caret......................proved - complete [shostak](0.16 s)
path?_rev_TCC1........................proved - complete [shostak](0.09 s)
path?_rev.............................proved - complete [shostak](0.11 s)
path?_gen_seq2........................proved - complete [shostak](0.09 s)
path?_add1_TCC1.......................proved - complete [shostak](0.08 s)
path?_add1............................proved - incomplete [shostak](0.17 s)
path?_trunc1_TCC1.....................proved - complete [shostak](0.10 s)
path?_trunc1_TCC2.....................proved - complete [shostak](0.08 s)
path?_trunc1_TCC3.....................proved - complete [shostak](0.10 s)
path?_trunc1..........................proved - complete [shostak](0.15 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (2.28 s)
Proof summary for theory path_ops
walk?_del_vert........................proved - complete [shostak](0.13 s)
walk?_del_vert_not....................proved - incomplete [shostak](0.12 s)
path?_del_vert........................proved - complete [shostak](0.06 s)
path?_del_verts.......................proved - complete [shostak](0.13 s)
walk_to_path..........................proved - complete [shostak](0.54 s)
walk_to_path_less.....................proved - complete [shostak](1.25 s)
walk_to_path_from.....................proved - complete [shostak](0.11 s)
walk_to_path_from_less................proved - complete [shostak](0.06 s)
path_disjoint_TCC1....................proved - complete [shostak](0.19 s)
path_disjoint_TCC2....................proved - incomplete [shostak](0.38 s)
path_disjoint.........................proved - incomplete [shostak](1.32 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (4.29 s)
Proof summary for theory sep_sets
del_verts_TCC1........................proved - complete [shostak](0.04 s)
del_verts_TCC2........................proved - complete [shostak](0.03 s)
sep_set_exists........................proved - complete [shostak](0.26 s)
min_sep_set_TCC1......................proved - complete [shostak](0.02 s)
min_sep_set_edge......................proved - complete [shostak](0.07 s)
min_sep_set_card......................proved - complete [shostak](0.18 s)
min_sep_set_seps......................proved - complete [shostak](0.06 s)
min_sep_set_vert......................proved - complete [shostak](0.24 s)
ends_not_in_min_sep_set...............proved - complete [shostak](0.02 s)
walk?_del_verts_not...................proved - incomplete [shostak](0.15 s)
adj_verts_TCC1........................proved - complete [shostak](0.11 s)
adj_verts_lem.........................proved - incomplete [shostak](0.14 s)
sep_num_min...........................proved - incomplete [shostak](0.26 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (1.57 s)
Proof summary for theory abstract_min
prep0.................................proved - complete [shostak](0.01 s)
min_f_TCC1............................proved - complete [shostak](0.01 s)
prep1.................................proved - complete [shostak](0.03 s)
min_TCC1..............................proved - complete [shostak](0.03 s)
min_def...............................proved - complete [shostak](0.00 s)
min_in................................proved - complete [shostak](0.00 s)
min_is_min............................proved - complete [shostak](0.01 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.09 s)
Proof summary for theory walk_inductions
walk_prep.............................proved - complete [shostak](0.03 s)
graph_induction_walk..................proved - complete [shostak](0.04 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.07 s)
Proof summary for theory path_circ
path_reduc_TCC1.......................proved - complete [shostak](0.24 s)
path_reduc............................proved - complete [shostak](0.28 s)
trunc_long............................proved - complete [shostak](0.21 s)
trunc_walk............................proved - complete [shostak](0.31 s)
walks_concat_red_TCC1.................proved - complete [shostak](0.10 s)
walks_concat_red_TCC2.................proved - complete [shostak](0.18 s)
walks_concat_red_TCC3.................proved - complete [shostak](0.15 s)
walks_concat_red_TCC4.................proved - complete [shostak](0.16 s)
walks_concat_red_TCC5.................proved - complete [shostak](0.23 s)
walks_concat_red_TCC6.................proved - complete [shostak](0.23 s)
walks_concat_red_TCC7.................proved - complete [shostak](2.01 s)
walks_concat_red......................proved - complete [shostak](0.68 s)
index_rev_TCC1........................proved - complete [shostak](0.04 s)
index_rev_TCC2........................proved - complete [shostak](0.04 s)
index_rev_TCC3........................proved - complete [shostak](0.05 s)
index_rev_TCC4........................proved - complete [shostak](0.05 s)
index_rev.............................proved - complete [shostak](0.04 s)
rev_rev...............................proved - complete [shostak](0.04 s)
ind_rev_rev_TCC1......................proved - complete [shostak](0.04 s)
ind_rev_rev_TCC2......................proved - complete [shostak](0.01 s)
ind_rev_rev_TCC3......................proved - complete [shostak](0.06 s)
ind_rev_rev_TCC4......................proved - complete [shostak](0.05 s)
ind_rev_rev...........................proved - complete [shostak](0.06 s)
second_in_cat_TCC1....................proved - complete [shostak](0.05 s)
second_in_cat_TCC2....................proved - complete [shostak](0.23 s)
second_in_cat_TCC3....................proved - complete [shostak](0.06 s)
second_in_cat.........................proved - complete [shostak](0.31 s)
sec_from_last_TCC1....................proved - complete [shostak](0.05 s)
sec_from_last_TCC2....................proved - complete [shostak](0.24 s)
sec_from_last.........................proved - complete [shostak](0.30 s)
prewalk_same..........................proved - complete [shostak](0.08 s)
compose_long_TCC1.....................proved - complete [shostak](0.06 s)
compose_long_TCC2.....................proved - complete [shostak](0.05 s)
compose_long..........................proved - complete [shostak](0.27 s)
red_compos_TCC1.......................proved - complete [shostak](0.21 s)
red_compos_TCC2.......................proved - complete [shostak](0.21 s)
red_compos_TCC3.......................proved - complete [shostak](0.21 s)
red_compos_TCC4.......................proved - complete [shostak](1.25 s)
red_compos............................proved - complete [shostak](3.64 s)
cycl_red_compos_TCC1..................proved - complete [shostak](0.21 s)
cycl_red_compos_TCC2..................proved - complete [shostak](0.20 s)
cycl_red_compos.......................proved - complete [shostak](2.86 s)
walkers_TCC1..........................proved - complete [shostak](0.01 s)
walkers_TCC2..........................proved - complete [shostak](0.03 s)
walkers_TCC3..........................proved - complete [shostak](0.03 s)
walkers...............................proved - complete [shostak](0.05 s)
path_one_TCC1.........................proved - complete [shostak](0.13 s)
path_one..............................proved - complete [shostak](0.50 s)
rev_eq................................proved - complete [shostak](0.05 s)
front_back_TCC1.......................proved - complete [shostak](0.03 s)
front_back............................proved - complete [shostak](0.05 s)
walk_from_l...........................proved - complete [shostak](0.04 s)
plus_up_TCC1..........................proved - complete [shostak](0.02 s)
plus_up...............................proved - complete [shostak](0.38 s)
two_walks_TCC1........................proved - complete [shostak](0.33 s)
two_walks.............................proved - complete [shostak](0.10 s)
back_short............................proved - complete [shostak](1.21 s)
from_rev_TCC1.........................proved - complete [shostak](0.05 s)
from_rev..............................proved - complete [shostak](0.05 s)
front_short_TCC1......................proved - complete [shostak](0.20 s)
front_short_TCC2......................proved - complete [shostak](0.20 s)
front_short...........................proved - complete [shostak](1.80 s)
add1_rev_TCC1.........................proved - complete [shostak](0.04 s)
add1_rev_TCC2.........................proved - complete [shostak](0.06 s)
add1_rev_TCC3.........................proved - complete [shostak](0.12 s)
add1_rev..............................proved - complete [shostak](0.35 s)
Theory totals: 66 formulas, 66 attempted, 66 succeeded (21.53 s)
Proof summary for theory circuits
reducible?_TCC1.......................proved - complete [shostak](0.06 s)
reducible?_TCC2.......................proved - complete [shostak](0.07 s)
cyclically_reduced?_TCC1..............proved - complete [shostak](0.07 s)
cyclically_reduced?_TCC2..............proved - complete [shostak](0.08 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.28 s)
Proof summary for theory path_lems
Pigeon_hole...........................proved - incomplete [shostak](0.12 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.12 s)
Proof summary for theory subgraphs_from_walk
G_from_TCC1...........................proved - incomplete [shostak](0.17 s)
G_from_vert...........................proved - incomplete [shostak](0.01 s)
vert_G_from...........................proved - incomplete [shostak](0.03 s)
edge?_G_from_TCC1.....................proved - complete [shostak](0.01 s)
edge?_G_from_TCC2.....................proved - complete [shostak](0.06 s)
edge?_G_from..........................proved - incomplete [shostak](0.09 s)
edge?_G_from_rev......................proved - incomplete [shostak](0.10 s)
vert_G_from_not.......................proved - incomplete [shostak](0.04 s)
del_vert_subgraph.....................proved - incomplete [shostak](0.16 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.66 s)
Proof summary for theory graph_from_edges
finite_lem............................proved - complete [shostak](0.14 s)
Union_to_pred.........................proved - complete [shostak](0.06 s)
pred_to_Union.........................proved - complete [shostak](0.02 s)
verts_of_TCC1.........................proved - complete [shostak](0.00 s)
verts_from_TCC1.......................proved - complete [shostak](0.06 s)
verts_from_of.........................proved - complete [shostak](0.04 s)
graph_from_edgeset_TCC1...............proved - complete [shostak](0.11 s)
graph_from_edgeset_rew1...............proved - complete [shostak](0.01 s)
graph_from_edgeset_rew2...............proved - complete [shostak](0.00 s)
no_isolated_verts.....................proved - complete [shostak](0.02 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.46 s)
Proof summary for theory max_subgraphs
prep0.................................proved - complete [shostak](0.05 s)
max_size_TCC1.........................proved - complete [shostak](0.06 s)
prep..................................proved - complete [shostak](0.09 s)
max_subgraph_TCC1.....................proved - complete [shostak](0.16 s)
max_subgraph_def......................proved - complete [shostak](0.02 s)
max_subgraph_in.......................proved - complete [shostak](0.02 s)
max_subgraph_is_max...................proved - complete [shostak](0.04 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.43 s)
Proof summary for theory max_upto
max_TCC1..............................proved - complete [shostak](0.11 s)
max_def...............................proved - complete [shostak](0.03 s)
max_lem...............................proved - complete [shostak](0.02 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.16 s)
Proof summary for theory min_lem
min_lem...............................proved - complete [shostak](0.02 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s)
Proof summary for theory max_subtrees
sing_is_tree..........................proved - complete [shostak](0.05 s)
tree_in...............................proved - complete [shostak](0.47 s)
max_subtree_TCC1......................proved - complete [shostak](0.03 s)
max_subtree_TCC2......................proved - complete [shostak](0.19 s)
max_subtree_tree......................proved - complete [shostak](0.18 s)
max_subtree_subgraph..................proved - complete [shostak](0.02 s)
max_subtree_max.......................proved - complete [shostak](0.20 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.13 s)
Proof summary for theory trees
tree?_TCC1............................proved - complete [shostak](0.05 s)
tree_nonempty.........................proved - complete [shostak](0.06 s)
tree_edge_card........................proved - complete [shostak](0.37 s)
tree_edge_k...........................proved - complete [shostak](0.10 s)
tree_edge.............................proved - complete [shostak](0.84 s)
tree_edge_all.........................proved - complete [shostak](0.02 s)
del_tree_k............................proved - complete [shostak](0.10 s)
del_tree..............................proved - complete [shostak](1.58 s)
del_tree_all..........................proved - complete [shostak](0.02 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (3.14 s)
Proof summary for theory graph_inductions
size_prep.............................proved - complete [shostak](0.20 s)
graph_induction_vert..................proved - complete [shostak](0.04 s)
graph_induction_vert_not..............proved - complete [shostak](0.04 s)
num_edges_prep........................proved - complete [shostak](0.03 s)
graph_induction_edge..................proved - complete [shostak](0.06 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.37 s)
Proof summary for theory tree_circ
exists_c_tree.........................proved - incomplete [shostak](0.01 s)
c_tree_TCC1...........................proved - complete [shostak](0.01 s)
tree_containing_lem...................proved - incomplete [shostak](0.12 s)
tree_deg..............................proved - incomplete [shostak](0.11 s)
small_tree_lem_TCC1...................proved - complete [shostak](0.24 s)
small_tree_lem........................proved - incomplete [shostak](0.17 s)
tree_no_circuits_TCC1.................proved - complete [shostak](0.22 s)
tree_no_circuits......................proved - incomplete [shostak](0.43 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.31 s)
Proof summary for theory circuit_deg
cir_deg_G.............................proved - complete [shostak](0.17 s)
circuit_deg_TCC1......................proved - complete [shostak](0.19 s)
circuit_deg...........................proved - incomplete [shostak](1.29 s)
circuit_subgraph_len_1_TCC1...........proved - complete [shostak](0.19 s)
circuit_subgraph_len_1................proved - incomplete [shostak](0.57 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.40 s)
Proof summary for theory subtrees
walk_acr_TCC1.........................proved - complete [shostak](0.05 s)
walk_acr_TCC2.........................proved - complete [shostak](0.10 s)
walk_acr_TCC3.........................proved - complete [shostak](0.11 s)
walk_acr..............................proved - complete [shostak](0.15 s)
walk_acr2.............................proved - complete [shostak](0.14 s)
add_dbl_TCC1..........................proved - complete [shostak](0.09 s)
add_dbl...............................proved - complete [shostak](0.04 s)
max_tree_all_verts....................proved - complete [shostak](0.94 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.62 s)
Proof summary for theory graph_conn_defs
connected?_TCC1.......................proved - complete [shostak](0.05 s)
path_connected?_TCC1..................proved - complete [shostak](0.05 s)
path_connected?_TCC2..................proved - complete [shostak](0.06 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.16 s)
Proof summary for theory graph_connected
conn_eq_path..........................proved - complete [shostak](0.05 s)
path_eq_piece.........................proved - complete [shostak](0.05 s)
piece_eq_conn.........................proved - complete [shostak](0.05 s)
conn_eq_complected....................proved - complete [shostak](0.07 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.22 s)
Proof summary for theory graph_conn_piece
singleton_piece.......................proved - complete [shostak](0.14 s)
not_piece_has_2.......................proved - complete [shostak](0.14 s)
edge_not_across.......................proved - complete [shostak](0.05 s)
lem1..................................proved - complete [shostak](0.20 s)
H1P_not_empty.........................proved - complete [shostak](0.12 s)
cip0..................................proved - complete [shostak](0.22 s)
cip3..................................proved - complete [shostak](0.15 s)
connected_not_empty...................proved - complete [shostak](0.07 s)
conn_implies_piece....................proved - complete [shostak](0.40 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.48 s)
Proof summary for theory graph_piece_path
union_edge_disj_TCC1..................proved - complete [shostak](0.03 s)
union_edge_disj.......................proved - complete [shostak](0.23 s)
piece_implies_path....................proved - complete [shostak](0.82 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.08 s)
Proof summary for theory graph_path_conn
isolated_not_path.....................proved - complete [shostak](0.12 s)
pic_A.................................proved - complete [shostak](0.22 s)
thw_A.................................proved - complete [shostak](0.56 s)
tree_has_walk.........................proved - complete [shostak](0.26 s)
path_implies_conn.....................proved - complete [shostak](0.71 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.87 s)
Proof summary for theory graph_complected
two_vertices..........................proved - complete [shostak](0.04 s)
sub_T.................................proved - complete [shostak](0.23 s)
rev_lem2..............................proved - complete [shostak](0.26 s)
conn_lem2.............................proved - complete [shostak](0.02 s)
del_rem_lem...........................proved - complete [shostak](0.09 s)
conn_lem3.............................proved - complete [shostak](0.17 s)
BIG...................................proved - complete [shostak](0.66 s)
conn_lem6.............................proved - complete [shostak](0.02 s)
conn_eq_compl.........................proved - complete [shostak](0.10 s)
conn_del_vert.........................proved - complete [shostak](0.08 s)
connected_not_empty...................proved - complete [shostak](0.06 s)
connect_deg_0.........................proved - complete [shostak](0.46 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (2.19 s)
Proof summary for theory ramsey_new
subgraph_clique.......................proved - complete [shostak](0.10 s)
subgraph_indep........................proved - complete [shostak](0.14 s)
r1_TCC1...............................proved - complete [shostak](0.02 s)
r1_TCC2...............................proved - complete [shostak](0.04 s)
r2_TCC1...............................proved - complete [shostak](0.04 s)
card_r1_r2............................proved - complete [shostak](0.18 s)
ramsey_lem............................proved - complete [shostak](1.53 s)
ramseys_theorem.......................proved - complete [shostak](0.04 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (2.10 s)
Proof summary for theory min_walk_reduced
reduced?_TCC1.........................proved - complete [shostak](0.02 s)
reduced?_TCC2.........................proved - complete [shostak](0.03 s)
min_walk_vert.........................proved - complete [shostak](0.19 s)
min_walk_is_reduced_TCC1..............proved - complete [shostak](0.08 s)
min_walk_is_reduced...................proved - complete [shostak](1.72 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.04 s)
Proof summary for theory min_walks
min_walk_from_TCC1....................proved - complete [shostak](0.03 s)
min_walk_from_TCC2....................proved - complete [shostak](0.10 s)
min_walk_def_TCC1.....................proved - complete [shostak](0.12 s)
min_walk_def..........................proved - complete [shostak](0.14 s)
min_walk_in...........................proved - complete [shostak](0.02 s)
min_walk_is_min.......................proved - complete [shostak](0.02 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.42 s)
Proof summary for theory reduce_walks
reduce_TCC1...........................proved - complete [shostak](0.05 s)
reduce_TCC2...........................proved - complete [shostak](0.05 s)
reduce_TCC3...........................proved - complete [shostak](0.06 s)
reduce_TCC4...........................proved - complete [shostak](0.06 s)
reduce_TCC5...........................proved - complete [shostak](0.07 s)
reduce_TCC6...........................proved - complete [shostak](0.19 s)
reduce_lem_TCC1.......................proved - complete [shostak](0.06 s)
reduce_lem_TCC2.......................proved - complete [shostak](0.05 s)
reduce_lem_TCC3.......................proved - complete [shostak](0.07 s)
reduce_lem_TCC4.......................proved - complete [shostak](0.06 s)
reduce_lem............................proved - complete [shostak](1.25 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.97 s)
Proof summary for theory menger
easy_menger...........................proved - incomplete [shostak](0.44 s)
hard_menger...........................proved - incomplete [shostak](0.25 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.69 s)
Proof summary for theory ind_paths
independent?_TCC1.....................proved - complete [shostak](0.04 s)
independent?_TCC2.....................proved - complete [shostak](0.04 s)
independent?_comm.....................proved - complete [shostak](0.04 s)
independent_ne........................proved - complete [shostak](0.03 s)
ind_path_set_2........................proved - complete [shostak](0.06 s)
internal_verts_TCC1...................proved - complete [shostak](0.03 s)
internal_verts_TCC2...................proved - incomplete [shostak](0.10 s)
indep?_lem............................proved - incomplete [shostak](0.09 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.43 s)
Proof summary for theory k_menger
sep_num_B............................proved - complete [shostak]( 0.06 s)
sep_num_implies......................proved - complete [shostak]( 0.05 s)
card_extension_W.....................proved - incomplete [shostak]( 0.20 s)
card_extension_same..................proved - incomplete [shostak]( 0.05 s)
easy_menger_B........................proved - incomplete [shostak]( 3.68 s)
sep_set_small........................proved - complete [shostak]( 0.10 s)
B_many_1.............................proved - complete [shostak](-0.67 s)
sub_tight............................proved - complete [shostak]( 0.03 s)
smaller_tight........................proved - incomplete [shostak]( 0.96 s)
small_tight..........................proved - incomplete [shostak]( 0.27 s)
exists_tight.........................proved - incomplete [shostak]( 0.50 s)
close_tight..........................proved - incomplete [shostak]( 0.95 s)
smaller_close........................proved - incomplete [shostak]( 0.71 s)
small_close..........................proved - incomplete [shostak]( 0.24 s)
exists_close.........................proved - incomplete [shostak]( 0.53 s)
closed_minimal.......................proved - incomplete [shostak]( 1.12 s)
closed_verts.........................proved - incomplete [shostak]( 0.12 s)
attach_edges_TCC1....................proved - complete [shostak]( 0.07 s)
Hverts_TCC1..........................proved - complete [shostak]( 0.11 s)
Mgraph_TCC1..........................proved - complete [shostak]( 0.14 s)
Hst_intersect........................proved - complete [shostak]( 0.07 s)
subset_Ws............................proved - complete [shostak]( 0.05 s)
subset_Wt............................proved - complete [shostak]( 0.06 s)
size_Ws..............................proved - incomplete [shostak]( 1.52 s)
size_Wt..............................proved - incomplete [shostak]( 1.74 s)
Menger_hard..........................proved - complete [shostak]( 0.04 s)
subgraph_walks.......................proved - complete [shostak]( 0.15 s)
subgraph_paths.......................proved - complete [shostak]( 0.06 s)
greatest_is..........................proved - complete [shostak]( 0.66 s)
least_is.............................proved - complete [shostak]( 0.40 s)
set_small_s..........................proved - complete [shostak]( 8.28 s)
set_small_t..........................proved - complete [shostak]( 4.91 s)
separates_Ws.........................proved - complete [shostak]( 0.20 s)
separates_Wt.........................proved - complete [shostak]( 0.21 s)
separ_sub............................proved - complete [shostak]( 0.65 s)
separ_plus...........................proved - complete [shostak]( 0.19 s)
super_separ..........................proved - complete [shostak]( 0.28 s)
intermediate_subgraph................proved - complete [shostak]( 0.59 s)
intermediate_verts...................proved - complete [shostak]( 0.23 s)
one_wedge_s_TCC1.....................proved - complete [shostak]( 0.25 s)
one_wedge_s_TCC2.....................proved - complete [shostak]( 0.23 s)
one_wedge_s_TCC3.....................proved - complete [shostak]( 0.17 s)
one_wedge_s_TCC4.....................proved - complete [shostak]( 0.43 s)
one_wedge_s..........................proved - complete [shostak]( 1.87 s)
one_edge_s...........................proved - incomplete [shostak]( 0.74 s)
short_path_k.........................proved - incomplete [shostak]( 1.22 s)
indep_path_sub.......................proved - complete [shostak]( 0.03 s)
ips_lem1.............................proved - complete [shostak]( 0.05 s)
ips_lem2.............................proved - incomplete [shostak]( 0.48 s)
secoo_TCC1...........................proved - complete [shostak]( 0.02 s)
secpp_TCC1...........................proved - complete [shostak]( 0.01 s)
inj_ips_TCC1.........................proved - complete [shostak]( 0.92 s)
inj_ips..............................proved - incomplete [shostak]( 0.20 s)
long_ipss_paths......................proved - complete [shostak]( 0.07 s)
ipss_W_TCC1..........................proved - complete [shostak]( 3.26 s)
ipss_W...............................proved - complete [shostak]( 0.58 s)
long_ipst_paths......................proved - complete [shostak]( 0.06 s)
ipst_W_TCC1..........................proved - complete [shostak]( 3.26 s)
ipst_W...............................proved - complete [shostak]( 0.80 s)
long_ipss_2..........................proved - complete [shostak]( 0.09 s)
long_ipst_2..........................proved - complete [shostak]( 0.09 s)
ind_path_set_secoo_TCC1..............proved - complete [shostak]( 0.04 s)
ind_path_set_secoo...................proved - incomplete [shostak]( 0.64 s)
ind_path_set_secpp_TCC1..............proved - complete [shostak]( 0.04 s)
ind_path_set_secpp...................proved - incomplete [shostak]( 0.67 s)
uniq_w_ipss..........................proved - incomplete [shostak]( 0.18 s)
uniq_w_ipst..........................proved - incomplete [shostak]( 0.19 s)
low_card_sep.........................proved - incomplete [shostak]( 0.08 s)
smaller_ips..........................proved - complete [shostak]( 0.27 s)
few_many.............................proved - complete [shostak]( 0.06 s)
min_B................................proved - incomplete [shostak]( 0.03 s)
no_sep_req...........................proved - incomplete [shostak]( 0.03 s)
k_sep_close..........................proved - incomplete [shostak]( 0.05 s)
p_Ht_TCC1............................proved - incomplete [shostak]( 0.99 s)
p_Ht_TCC2............................proved - incomplete [shostak]( 0.60 s)
p_Ht_TCC3............................proved - incomplete [shostak]( 0.95 s)
p_Ht.................................proved - incomplete [shostak]( 1.08 s)
q_Hs_TCC1............................proved - incomplete [shostak]( 0.99 s)
q_Hs_TCC2............................proved - incomplete [shostak]( 0.84 s)
q_Hs_TCC3............................proved - incomplete [shostak]( 0.95 s)
q_Hs.................................proved - incomplete [shostak]( 0.79 s)
disjoint_M_paths_TCC1................proved - incomplete [shostak]( 0.03 s)
disjoint_M_paths_TCC2................proved - incomplete [shostak]( 0.03 s)
disjoint_M_paths_TCC3................proved - incomplete [shostak]( 0.11 s)
disjoint_M_paths_TCC4................proved - incomplete [shostak]( 0.04 s)
disjoint_M_paths_TCC5................proved - incomplete [shostak]( 0.11 s)
disjoint_M_paths_TCC6................proved - incomplete [shostak]( 0.03 s)
disjoint_M_paths_TCC7................proved - incomplete [shostak]( 0.15 s)
disjoint_M_paths_TCC8................proved - incomplete [shostak]( 0.04 s)
disjoint_M_paths_TCC9................proved - incomplete [shostak]( 0.11 s)
disjoint_M_paths.....................proved - incomplete [shostak]( 2.87 s)
sec_image............................proved - complete [shostak]( 0.50 s)
Map_s_TCC1...........................proved - complete [shostak]( 0.06 s)
Map_s................................proved - incomplete [shostak]( 0.25 s)
Map_t_TCC1...........................proved - complete [shostak]( 0.06 s)
Map_t................................proved - incomplete [shostak]( 0.25 s)
Mapper_ips...........................proved - incomplete [shostak](15.41 s)
non_attached_induct..................proved - incomplete [shostak]( 0.10 s)
plus_sep_vert........................proved - complete [shostak]( 0.20 s)
separ_del_vert.......................proved - complete [shostak]( 0.21 s)
plus_path_set_TCC1...................proved - complete [shostak]( 0.08 s)
plus_path_set_TCC2...................proved - complete [shostak]( 0.30 s)
plus_path_set........................proved - incomplete [shostak]( 1.22 s)
short_path_attach....................proved - incomplete [shostak]( 1.25 s)
bridge_one...........................proved - incomplete [shostak]( 1.15 s)
bridge_two_TCC1......................proved - complete [shostak]( 0.04 s)
bridge_two...........................proved - incomplete [shostak]( 1.18 s)
bridge_three.........................proved - complete [shostak]( 0.20 s)
C_induct_lemma.......................proved - incomplete [shostak]( 0.16 s)
Menger_k_hard........................proved - incomplete [shostak]( 0.03 s)
Many_indep_paths.....................proved - incomplete [shostak]( 0.33 s)
hard_menger_trad.....................proved - incomplete [shostak]( 2.98 s)
Theory totals: 112 formulas, 112 attempted, 112 succeeded (83.29 s)
Proof summary for theory finite_sets_card_from
card_extension........................proved - incomplete [shostak](0.05 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)
Proof summary for theory easy_menger
easy_menger...........................proved - incomplete [shostak](0.44 s)
easy_meng_1...........................proved - incomplete [shostak](0.43 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.86 s)
Proof summary for theory subgraph_paths
walk?_subgraph........................proved - complete [shostak](0.12 s)
path?_subgraph........................proved - complete [shostak](0.06 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.18 s)
Proof summary for theory complem
powerset_finite.......................proved - complete [shostak](0.69 s)
all_edges_power.......................proved - complete [shostak](0.08 s)
all_edges_finite......................proved - complete [shostak](0.22 s)
completion_TCC1.......................proved - complete [shostak](0.02 s)
completion_TCC2.......................proved - complete [shostak](0.07 s)
completion_is_subgraph................proved - complete [shostak](0.30 s)
complement_TCC1.......................proved - complete [shostak](0.03 s)
complement_TCC2.......................proved - complete [shostak](0.06 s)
comp_comp_lem.........................proved - complete [shostak](0.06 s)
isol_TCC1.............................proved - complete [shostak](0.01 s)
path_or_not_path......................proved - complete [shostak](2.73 s)
five_degrees_separation...............proved - complete [shostak](2.63 s)
paths_or_not..........................proved - complete [shostak](0.27 s)
five_degrees_separated................proved - complete [shostak](0.13 s)
strong_implies........................proved - complete [shostak](0.11 s)
imply_strong..........................proved - complete [shostak](0.02 s)
completion_is_transitive..............proved - complete [shostak](0.08 s)
trans_complem.........................proved - complete [shostak](0.54 s)
t_close_TCC1..........................proved - complete [shostak](0.15 s)
t_close_1.............................proved - complete [shostak](0.03 s)
t_close_2.............................proved - complete [shostak](0.03 s)
t_close_3.............................proved - complete [shostak](0.08 s)
trans_fill............................proved - complete [shostak](0.31 s)
complem_fill..........................proved - complete [shostak](0.04 s)
subgraph_conn.........................proved - complete [shostak](0.17 s)
complete_conn.........................proved - complete [shostak](0.18 s)
short_path_TCC1.......................proved - complete [shostak](0.17 s)
short_path_TCC2.......................proved - complete [shostak](0.12 s)
short_path............................proved - complete [shostak](1.60 s)
trans_walk............................proved - complete [shostak](0.27 s)
trans_connected.......................proved - complete [shostak](0.23 s)
disjoint_trans........................proved - complete [shostak](0.14 s)
disjoint_trans_strong.................proved - complete [shostak](0.02 s)
subgraph_trans........................proved - complete [shostak](0.16 s)
subgraph_trans_strong.................proved - complete [shostak](0.03 s)
t_close_4.............................proved - complete [shostak](0.12 s)
closure_connect.......................proved - complete [shostak](0.53 s)
connected_complem.....................proved - complete [shostak](0.30 s)
p_close_TCC1..........................proved - complete [shostak](0.15 s)
p_close_TCC2..........................proved - complete [shostak](0.07 s)
p_subgraph_t..........................proved - complete [shostak](0.15 s)
p_transitive..........................proved - complete [shostak](0.12 s)
p_close_1.............................proved - complete [shostak](0.13 s)
p_close_trans.........................proved - complete [shostak](0.01 s)
t_subgraph............................proved - complete [shostak](0.14 s)
Theory totals: 45 formulas, 45 attempted, 45 succeeded (13.48 s)
Proof summary for theory los_graph
los_graphic...........................proved - complete [shostak](0.04 s)
Los...................................proved - complete [shostak](0.03 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.07 s)
Proof summary for theory sep_set_lems
sep_num_0.............................proved - complete [shostak](0.05 s)
sep_num_gt_0..........................proved - complete [shostak](0.37 s)
sep_num_is_1..........................proved - complete [shostak](0.19 s)
sep_num_le1...........................proved - complete [shostak](0.28 s)
separable?_comm.......................proved - complete [shostak](0.04 s)
separates_comm........................proved - complete [shostak](0.07 s)
sep_num_comm..........................proved - complete [shostak](0.09 s)
v_not_in..............................proved - incomplete [shostak](0.20 s)
path_thru_each........................proved - incomplete [shostak](0.21 s)
one_to_each...........................proved - incomplete [shostak](0.36 s)
walk?_del_verts.......................proved - complete [shostak](0.10 s)
del_verts_eq..........................proved - complete [shostak](0.10 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (2.07 s)
Proof summary for theory tree_paths
dual_paths?_TCC1......................proved - complete [shostak](0.08 s)
dual_paths?_TCC2......................proved - complete [shostak](0.07 s)
dual_paths?_TCC3......................proved - complete [shostak](0.09 s)
dual_paths?_TCC4......................proved - complete [shostak](0.09 s)
min_dual_paths_TCC1...................proved - complete [shostak](0.02 s)
min_dual_paths_TCC2...................proved - complete [shostak](0.13 s)
min_dual_def..........................proved - complete [shostak](0.23 s)
min_dual_exists.......................proved - complete [shostak](0.04 s)
dual_path_trunc_TCC1..................proved - complete [shostak](0.03 s)
dual_path_trunc_TCC2..................proved - complete [shostak](0.25 s)
dual_path_trunc_TCC3..................proved - complete [shostak](0.26 s)
dual_path_trunc_TCC4..................proved - complete [shostak](0.28 s)
dual_path_trunc_TCC5..................proved - complete [shostak](0.21 s)
dual_path_trunc_TCC6..................proved - complete [shostak](0.33 s)
dual_path_trunc_TCC7..................proved - complete [shostak](0.23 s)
dual_path_trunc_TCC8..................proved - complete [shostak](0.40 s)
dual_path_trunc.......................proved - complete [shostak](0.23 s)
dual_path_length......................proved - complete [shostak](0.38 s)
min_dual_reduc_TCC1...................proved - complete [shostak](0.04 s)
min_dual_reduc_TCC2...................proved - complete [shostak](0.03 s)
min_dual_reduc_TCC3...................proved - complete [shostak](0.05 s)
min_dual_reduc_TCC4...................proved - complete [shostak](0.04 s)
min_dual_reduc........................proved - complete [shostak](1.10 s)
min_dual_distin_TCC1..................proved - complete [shostak](0.18 s)
min_dual_distin_TCC2..................proved - complete [shostak](0.18 s)
min_dual_distin.......................proved - complete [shostak](0.77 s)
dual_cycle_TCC1.......................proved - complete [shostak](0.16 s)
dual_cycle_TCC2.......................proved - complete [shostak](0.16 s)
dual_cycle_TCC3.......................proved - complete [shostak](0.03 s)
dual_cycle_TCC4.......................proved - complete [shostak](0.34 s)
dual_cycle............................proved - complete [shostak](5.91 s)
tree_one_path.........................proved - incomplete [shostak](2.38 s)
Theory totals: 32 formulas, 32 attempted, 32 succeeded (14.69 s)
Proof summary for theory cycles
cycle?_TCC1...........................proved - complete [shostak](0.10 s)
cycle?_TCC2...........................proved - complete [shostak](0.11 s)
cycle_l_gt_3..........................proved - complete [shostak](0.05 s)
cycle_has_path_TCC1...................proved - complete [shostak](0.09 s)
cycle_has_path........................proved - complete [shostak](0.30 s)
cycle_gt3.............................proved - complete [shostak](0.07 s)
cycle_def.............................proved - complete [shostak](0.10 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.81 s)
Proof summary for theory cycle_deg
reachable_TCC1........................proved - complete [shostak](0.05 s)
reachable_subset......................proved - complete [shostak](0.10 s)
reachable_conn........................proved - complete [shostak](1.51 s)
conn_compon...........................proved - complete [shostak](0.99 s)
sub_cycle_TCC1........................proved - complete [shostak](0.07 s)
sub_cycle.............................proved - complete [shostak](0.15 s)
uniq_del_vert.........................proved - complete [shostak](0.06 s)
del_edge_uniq.........................proved - complete [shostak](0.98 s)
charact_tree..........................proved - complete [shostak](0.33 s)
exclus_cycl...........................proved - incomplete [shostak](1.20 s)
num_edge_tree.........................proved - incomplete [shostak](0.75 s)
iff_tree..............................proved - incomplete [shostak](0.33 s)
tree_num_iff..........................proved - incomplete [shostak](0.18 s)
deg_gt_1_cycle........................proved - incomplete [shostak](0.52 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (7.22 s)
Proof summary for theory abstract_max
prep0.................................proved - complete [shostak](0.01 s)
max_f_TCC1............................proved - complete [shostak](0.01 s)
prep1.................................proved - complete [shostak](0.04 s)
max_TCC1..............................proved - complete [shostak](0.05 s)
max_def...............................proved - complete [shostak](0.00 s)
max_in................................proved - complete [shostak](0.00 s)
max_is_max............................proved - complete [shostak](0.01 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.12 s)
Proof summary for theory old_menger
easy_menger...........................proved - incomplete [shostak](0.43 s)
hard_menger...........................proved - incomplete [shostak](0.33 s)
easy_meng_1...........................proved - incomplete [shostak](0.43 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.18 s)
Proof summary for theory h_menger
path_not_thru.........................proved - complete [shostak](0.41 s)
adjacent_fact.........................proved - complete [shostak](0.44 s)
sep_num_del...........................proved - complete [shostak](0.27 s)
separates_del.........................proved - complete [shostak](0.23 s)
induction_step_comm...................proved - complete [shostak](0.04 s)
separable?_del........................proved - complete [shostak](0.06 s)
seq_j_TCC1............................proved - complete [shostak](0.02 s)
seq_j_TCC2............................proved - complete [shostak](0.04 s)
seq_j_TCC3............................proved - complete [shostak](0.06 s)
seq_j.................................proved - complete [shostak](0.29 s)
short_path_case.......................proved - incomplete [shostak](0.39 s)
finale................................proved - incomplete [shostak](1.45 s)
h_menger..............................proved - incomplete [shostak](0.08 s)
hard_menger...........................proved - incomplete [shostak](0.30 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (4.09 s)
Proof summary for theory meng_scaff_prelude
line20_TCC1...........................proved - complete [shostak](0.03 s)
line20_TCC2...........................proved - complete [shostak](0.03 s)
line20_TCC3...........................proved - complete [shostak](0.04 s)
line20_TCC4...........................proved - complete [shostak](0.04 s)
line20_TCC5...........................proved - complete [shostak](0.04 s)
line20_TCC6...........................proved - incomplete [shostak](0.03 s)
line20................................proved - incomplete [shostak](0.61 s)
join2_TCC1............................proved - complete [shostak](0.06 s)
join2_TCC2............................proved - complete [shostak](0.41 s)
path_meng_t...........................proved - complete [shostak](0.07 s)
path_H_def_TCC1.......................proved - complete [shostak](0.10 s)
path_H_def............................proved - incomplete [shostak](0.44 s)
path_H_ind_TCC1.......................proved - complete [shostak](0.03 s)
path_H_ind_TCC2.......................proved - complete [shostak](0.50 s)
path_H_ind_TCC3.......................proved - complete [shostak](0.02 s)
path_H_ind_TCC4.......................proved - complete [shostak](0.72 s)
path_H_ind............................proved - incomplete [shostak](1.05 s)
path_comps_ind3_TCC1..................proved - complete [shostak](0.02 s)
path_comps_ind3_TCC2..................proved - complete [shostak](0.12 s)
path_comps_ind3_TCC3..................proved - complete [shostak](0.53 s)
path_comps_ind3_TCC4..................proved - complete [shostak](0.55 s)
path_comps_ind3_TCC5..................proved - complete [shostak](0.02 s)
path_comps_ind3_TCC6..................proved - complete [shostak](0.03 s)
path_comps_ind3.......................proved - incomplete [shostak](0.16 s)
path_H_trunc_TCC1.....................proved - complete [shostak](0.51 s)
path_H_trunc_TCC2.....................proved - complete [shostak](0.44 s)
path_H_trunc..........................proved - incomplete [shostak](0.77 s)
meng_last_TCC1........................proved - complete [shostak](0.02 s)
meng_last_TCC2........................proved - complete [shostak](0.02 s)
meng_last_TCC3........................proved - complete [shostak](0.87 s)
meng_last_TCC4........................proved - complete [shostak](0.88 s)
meng_last.............................proved - complete [shostak](0.32 s)
ind_verts_W_TCC1......................proved - complete [shostak](0.21 s)
ind_verts_W_TCC2......................proved - complete [shostak](0.21 s)
ind_verts_W...........................proved - incomplete [shostak](0.11 s)
ind_verts_w_TCC1......................proved - complete [shostak](0.20 s)
ind_verts_w_TCC2......................proved - complete [shostak](0.21 s)
ind_verts_w...........................proved - incomplete [shostak](0.11 s)
path_meng_in_TCC1.....................proved - complete [shostak](0.02 s)
path_meng_in_TCC2.....................proved - incomplete [shostak](0.02 s)
path_meng_in_TCC3.....................proved - incomplete [shostak](1.02 s)
path_meng_in..........................proved - incomplete [shostak](1.63 s)
join2_lem_TCC1........................proved - complete [shostak](0.04 s)
join2_lem_TCC2........................proved - complete [shostak](0.03 s)
join2_lem_TCC3........................proved - complete [shostak](0.09 s)
join2_lem_TCC4........................proved - complete [shostak](0.08 s)
join2_lem.............................proved - complete [shostak](0.77 s)
path_from_to_walk_from................proved - complete [shostak](0.07 s)
paths_H_disj_TCC1.....................proved - complete [shostak](0.02 s)
paths_H_disj_TCC2.....................proved - complete [shostak](0.03 s)
paths_H_disj..........................proved - incomplete [shostak](0.48 s)
prelude...............................proved - incomplete [shostak](7.44 s)
Theory totals: 52 formulas, 52 attempted, 52 succeeded (22.29 s)
Proof summary for theory meng_scaff
first_TCC1............................proved - complete [shostak](0.03 s)
first_lem.............................proved - complete [shostak](0.05 s)
first_not_TCC1........................proved - complete [shostak](0.03 s)
first_not.............................proved - complete [shostak](0.06 s)
meng_to_G_sep_TCC1....................proved - complete [shostak](0.13 s)
meng_to_G_sep_TCC2....................proved - complete [shostak](0.12 s)
meng_to_G_sep_TCC3....................proved - complete [shostak](0.14 s)
meng_to_G_sep_TCC4....................proved - complete [shostak](0.14 s)
meng_to_G_sep.........................proved - incomplete [shostak](4.07 s)
prep_14_TCC1..........................proved - complete [shostak](0.04 s)
prep_14_TCC2..........................proved - complete [shostak](0.04 s)
prep_14...............................proved - incomplete [shostak](0.35 s)
line14_TCC1...........................proved - complete [shostak](0.03 s)
line14_TCC2...........................proved - complete [shostak](0.38 s)
line14_TCC3...........................proved - complete [shostak](0.38 s)
line14_TCC4...........................proved - complete [shostak](0.38 s)
line14................................proved - incomplete [shostak](0.58 s)
line15ab..............................proved - incomplete [shostak](0.29 s)
prep_16...............................proved - incomplete [shostak](1.16 s)
line16................................proved - incomplete [shostak](0.61 s)
line19_TCC1...........................proved - complete [shostak](0.03 s)
line19_TCC2...........................proved - complete [shostak](0.07 s)
line19_TCC3...........................proved - complete [shostak](0.07 s)
line19_TCC4...........................proved - complete [shostak](0.08 s)
line19_TCC5...........................proved - complete [shostak](0.02 s)
line19................................proved - complete [shostak](0.78 s)
line17_prep...........................proved - complete [shostak](0.18 s)
line17_TCC1...........................proved - complete [shostak](0.34 s)
line17_TCC2...........................proved - complete [shostak](0.35 s)
line17_TCC3...........................proved - complete [shostak](0.38 s)
line17_TCC4...........................proved - complete [shostak](0.38 s)
line17................................proved - complete [shostak](0.30 s)
pre20.................................proved - incomplete [shostak](0.31 s)
Theory totals: 33 formulas, 33 attempted, 33 succeeded (12.29 s)
Proof summary for theory meng_scaff_defs
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.269Quellennavigators
]
|
|
|
|
|
|
