| products/sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: autorewrite.mli Sprache: SML
|
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.249Quellennavigators ] |