From ee17c2dee41284120359d9ce086f17a98cc6792a Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Tue, 20 Sep 2016 11:58:24 +0200 Subject: [PATCH] twaalgos: Implement dt*a_sat_minimize_incr(...) functions * python/spot/__init__.py: Add 'incr' boolean argument. * spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_incr(...). * spot/twaalgos/dtbasat.hh: Declare it. * spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_incr(...) and deal with options. * spot/twaalgos/dtwasat.hh: Declare it. * spot/twaalgos/postproc.cc: Add option --sat-minimize=incr. * spot/twaalgos/postproc.hh: Add incr parameter. * tests/core/satmin.test: Add tests for incremental version. Update expected result. * tests/core/satmin2.test: Add tests for incremental version. * tests/python/satmin.py: Add tests for incremental version. --- python/spot/__init__.py | 9 +- spot/twaalgos/dtbasat.cc | 87 +++++- spot/twaalgos/dtbasat.hh | 16 ++ spot/twaalgos/dtwasat.cc | 119 +++++++- spot/twaalgos/dtwasat.hh | 24 +- spot/twaalgos/postproc.cc | 14 +- spot/twaalgos/postproc.hh | 1 + tests/core/satmin.test | 564 +++++++++++++++++++++++++++++++++++++- tests/core/satmin2.test | 155 ++++++++++- tests/python/satmin.py | 88 ++++++ 10 files changed, 1051 insertions(+), 26 deletions(-) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 5dba7a193..2660fb418 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -858,7 +858,8 @@ for fun in ['remove_x', 'relabel', 'relabel_bse', # Better interface to the corresponding C++ function. def sat_minimize(aut, acc=None, colored=False, state_based=False, states=0, - max_states=0, dichotomy=False): + max_states=0, dichotomy=False, + param=0, incr=False): args='' if acc is not None: if type(acc) is not str: @@ -875,7 +876,11 @@ def sat_minimize(aut, acc=None, colored=False, raise ValueError("argument 'states' should be a positive integer") args += ',max-states=' + str(max_states) if dichotomy: - args += ',dichotomy'; + args += ',dichotomy' + if param: + args += ',param=' + str(param) + if incr: + args += ',incr' from spot.impl import sat_minimize as sm return sm(aut, args, state_based) diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index 1852cdc81..3bbf357d7 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -738,13 +738,96 @@ namespace spot if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); - // Print log if env var SPOT_SATLOG is set. - print_log(t, target_state_number, res, solver); + print_log(t, target_state_number, res, solver); // If SPOT_SATLOG is set. trace << "dtba_sat_synthetize(...) = " << res << '\n'; return res; } + twa_graph_ptr + dtba_sat_minimize_incr(const const_twa_graph_ptr& a, + bool state_based, int max_states, int sat_incr_steps) + { + if (!a->acc().is_buchi()) + throw std::runtime_error + (": dtba_sat_minimize_incr() can only work with Büchi acceptance."); + const_twa_graph_ptr prev = a; + dict d; + d.cand_size = (max_states < 0) ? + stats_reachable(prev).states - 1 : max_states; + if (d.cand_size == 0) + return nullptr; + + trace << "dtba_sat_minimize_incr(..., states = " << d.cand_size + << ", state_based = " << state_based << ")\n"; + + bool naive = sat_incr_steps < 0; + trace << "sat_incr_steps: " << sat_incr_steps << '\n'; + + twa_graph_ptr next = spot::make_twa_graph(spot::make_bdd_dict()); + while (next && d.cand_size > 0) + { + // First iteration of classic solving. + satsolver solver; + timer_map t1; + t1.start("encode"); + dtba_to_sat(solver, prev, d, state_based); + t1.stop("encode"); + t1.start("solve"); + satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); + next = solution.second.empty() ? nullptr : + sat_build(solution.second, d, prev, state_based); + print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + + trace << "First iteration done\n"; + + // Compute the AP used. + bdd ap = prev->ap_vars(); + + // Incremental solving loop. + unsigned orig_cand_size = d.cand_size; + unsigned alpha_size = d.alpha_vect.size(); + for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps); + ++k) + { + t1.start("encode"); + prev = next; + int reach_states = stats_reachable(prev).states; + cnf_comment("Next iteration: ", reach_states - 1, "\n"); + + trace << "Encoding the deletion of state " << reach_states - 1 << '\n'; + + // Add new constraints. + for (unsigned i = reach_states - 1; i < d.cand_size; ++i) + for (unsigned l = 0; l < alpha_size; ++l) + for (unsigned j = 0; j < orig_cand_size; ++j) + solver.add({-d.transid(j, l, i), 0}); + + d.cand_size = reach_states - 1; + t1.stop("encode"); + t1.start("solve"); + satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); + next = solution.second.empty() ? nullptr : + sat_build(solution.second, d, prev, state_based); + print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + } + + if (next) + { + trace << "Starting from scratch\n"; + prev = next; + d = dict(); + d.cand_size = stats_reachable(prev).states - 1; + if (d.cand_size == 0) + next = nullptr; + } + } + + return prev == a ? nullptr : std::const_pointer_cast(prev); + } + twa_graph_ptr dtba_sat_minimize(const const_twa_graph_ptr& a, bool state_based, int max_states) diff --git a/spot/twaalgos/dtbasat.hh b/spot/twaalgos/dtbasat.hh index ac2f43552..7620d5a40 100644 --- a/spot/twaalgos/dtbasat.hh +++ b/spot/twaalgos/dtbasat.hh @@ -65,4 +65,20 @@ namespace spot dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, bool state_based = false, int max_states = -1); + + /// \brief Attempt to minimize a det. TBA with a SAT solver. + /// + /// This acts like dtba_sat_synthetize() and obtains a first minimized + /// automaton. Then, incrementally, it encodes the deletion of one state + /// and solves it as many time as param value. + /// If param >= 0, this process is fully repeated until the minimal automaton + /// is found. Otherwise, it continues to delete states one by one + /// incrementally until the minimal automaton is found. + /// + /// If no smaller TBA exist, this returns a null pointer. + SPOT_API twa_graph_ptr + dtba_sat_minimize_incr(const const_twa_graph_ptr& a, + bool state_based = false, + int max_states = -1, + int param = 2); } diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 9421806f6..d8b99fa8e 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -541,7 +541,7 @@ namespace spot // Compute the AP used. bdd ap = ref->ap_vars(); - // Count the number of atomic propositions + // Count the number of atomic propositions. int nap = 0; { bdd cur = ap; @@ -1015,8 +1015,7 @@ namespace spot if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); - // Print log if env var SPOT_SATLOG is set. - print_log(t, target_state_number, res, solver); + print_log(t, target_state_number, res, solver); // if SPOT_SATLOG is set. trace << "dtwa_sat_synthetize(...) = " << res << '\n'; return res; @@ -1055,6 +1054,97 @@ namespace spot } } + twa_graph_ptr + dtwa_sat_minimize_incr(const const_twa_graph_ptr& a, + unsigned target_acc_number, + const acc_cond::acc_code& target_acc, + bool state_based, int max_states, + bool colored, int sat_incr_steps) + { + const_twa_graph_ptr prev = a; + + dict d(prev); + d.cand_size = (max_states < 0) ? + stats_reachable(prev).states - 1 : max_states; + d.cand_nacc = target_acc_number; + d.cand_acc = target_acc; + if (d.cand_size == 0) + return nullptr; + + trace << "dtwa_sat_minimize_incr(..., nacc = " << target_acc_number + << ", acc = \"" << target_acc << "\", states = " << d.cand_size + << ", state_based = " << state_based << ")\n"; + + bool naive = sat_incr_steps < 0; + trace << "sat_incr_steps: " << sat_incr_steps << '\n'; + + twa_graph_ptr next = spot::make_twa_graph(spot::make_bdd_dict()); + while (next && d.cand_size > 0) + { + // First iteration of classic solving. + satsolver solver; + timer_map t1; + t1.start("encode"); + dtwa_to_sat(solver, prev, d, state_based, colored); + t1.stop("encode"); + t1.start("solve"); + satsolver::solution_pair solution = solver.get_solution(); + t1.stop("solve"); + next = solution.second.empty() ? nullptr : + sat_build(solution.second, d, prev, state_based); + print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + + trace << "First iteraton done\n"; + + // Compute the AP used. + bdd ap = prev->ap_vars(); + + // Incremental solving loop. + unsigned orig_cand_size = d.cand_size; + unsigned alpha_size = d.alpha_vect.size(); + for (int k = 0; next && d.cand_size > 0 && (naive || k < sat_incr_steps); + ++k) + { + t1.start("encode"); + prev = next; + int reach_states = stats_reachable(prev).states; + cnf_comment("Next iteration:", reach_states - 1, "\n"); + + trace << "Encoding the deletion of state " << reach_states - 1 << '\n'; + + // Add new constraints. + for (unsigned i = reach_states - 1; i < d.cand_size; ++i) + for (unsigned l = 0; l < alpha_size; ++l) + for (unsigned j = 0; j < orig_cand_size; ++j) + solver.add({-d.transid(j, l, i), 0}); + + d.cand_size = reach_states - 1; + t1.stop("encode"); + t1.start("solve"); + solution = solver.get_solution(); + t1.stop("solve"); + next = solution.second.empty() ? nullptr : + sat_build(solution.second, d, prev, state_based); + print_log(t1, d.cand_size, next, solver); // If SPOT_SATLOG is set. + } + + if (next) + { + trace << "Starting from scratch\n"; + prev = next; + d = dict(prev); + d.cand_size = stats_reachable(prev).states - 1; + d.cand_nacc = target_acc_number; + d.cand_acc = target_acc; + if (d.cand_size == 0) + next = nullptr; + } + + }; + + return prev == a ? nullptr : std::const_pointer_cast(prev); + } + twa_graph_ptr dtwa_sat_minimize(const const_twa_graph_ptr& a, unsigned target_acc_number, @@ -1135,6 +1225,8 @@ namespace spot auto accstr = om.get_str("acc"); bool colored = om.get("colored", 0); int preproc = om.get("preproc", 3); + bool incr = om.get("incr", 0); + int param = om.get("param", 0); // No more om.get() below this. om.report_unused_options(); @@ -1227,11 +1319,24 @@ namespace spot { auto orig = a; if (!target_is_buchi || !a->acc().is_buchi() || colored) - a = (dicho ? dtwa_sat_minimize_dichotomy : dtwa_sat_minimize) - (a, nacc, target_acc, state_based, max_states, colored); + { + if (incr) + a = dtwa_sat_minimize_incr(a, nacc, target_acc, state_based, + max_states, colored, param); + else + a = (dicho ? dtwa_sat_minimize_dichotomy + : dtwa_sat_minimize) + (a, nacc, target_acc, state_based, max_states, colored); + } else - a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize) - (a, state_based, max_states); + { + if (incr) + a = dtba_sat_minimize_incr(a, state_based, max_states, param); + else + a = (dicho ? dtba_sat_minimize_dichotomy + : dtba_sat_minimize) + (a, state_based, max_states); + } if (!a && !user_supplied_acc) a = orig; diff --git a/spot/twaalgos/dtwasat.hh b/spot/twaalgos/dtwasat.hh index 1e2645268..02dd79fde 100644 --- a/spot/twaalgos/dtwasat.hh +++ b/spot/twaalgos/dtwasat.hh @@ -83,6 +83,25 @@ namespace spot int max_states = -1, bool colored = false); + /// \brief Attempt to minimize a deterministic TωA with a SAT solver. + /// + /// It acts like dtwa_sat_synthetisze() and obtains a first minimized + /// automaton. Then, incrementally, it encodes and solves the deletion of one + /// state as many time as param value. + /// If param >= 0, this process is fully repeated until the minimal automaton + /// is found. Otherwise, it continues to delete states one by one + /// incrementally until the minimal automaton is found. + /// + /// If no smaller TGBA exists, this returns a null pointer. + SPOT_API twa_graph_ptr + dtwa_sat_minimize_incr(const const_twa_graph_ptr& a, + unsigned target_acc_number, + const acc_cond::acc_code& target_acc, + bool state_based = false, + int max_states = -1, + bool colored = false, + int param = 2); + /// \brief High-level interface to SAT-based minimization /// /// Minimize the automaton \a aut, using options \a opt. @@ -94,7 +113,10 @@ namespace spot /// acc = "generalized-Buchi 2" /// acc = "Rabin 3" /// acc = "same" /* default */ - /// dichotomy = 1 // use dichotomy instead of decreasing loop + /// dichotomy = 1 // use dichotomy + /// incr = 1 // use satsolver incrementally to attempt to delete a + /// fixed number of states before starting from scratch + /// incr < 0 // use satsolver incrementally, never restart /// colored = 1 // build a colored TωA /// SPOT_API twa_graph_ptr diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index b119663a8..d8e190d93 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -69,6 +69,7 @@ namespace spot scc_filter_ = opt->get("scc-filter", -1); ba_simul_ = opt->get("ba-simul", -1); tba_determinisation_ = opt->get("tba-det", 0); + incr_ = opt->get("incr", 0); sat_minimize_ = opt->get("sat-minimize", 0); sat_acc_ = opt->get("sat-acc", 0); sat_states_ = opt->get("sat-states", 0); @@ -427,8 +428,10 @@ namespace spot res = dtba_sat_synthetize(res, sat_states_, state_based_); else if (sat_minimize_ == 1 || sat_minimize_ == -1) res = dtba_sat_minimize(res, state_based_); - else // sat_minimize_ == 2 + else if (sat_minimize_ == 2) res = dtba_sat_minimize_dichotomy(res, state_based_); + else // sat_minimize_ = 3 + res = dtba_sat_minimize_incr(res, state_based_, -1, incr_); } else { @@ -442,12 +445,17 @@ namespace spot (res, target_acc, acc_cond::acc_code::generalized_buchi(target_acc), state_based_); - else // sat_minimize_ == 2 + else if (sat_minimize_ == 2) res = dtwa_sat_minimize_dichotomy (res, target_acc, acc_cond::acc_code::generalized_buchi(target_acc), state_based_); - } + else // sat_minimize_ = 3 + res = dtwa_sat_minimize_incr + (res, target_acc, + acc_cond::acc_code::generalized_buchi(target_acc), + state_based_, -1, false, incr_); + } if (res) { diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index b9d1174eb..135746493 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -188,6 +188,7 @@ namespace spot int scc_filter_ = -1; int ba_simul_ = -1; bool tba_determinisation_ = false; + int incr_ = 0; int sat_minimize_ = 0; int sat_acc_ = 0; int sat_states_ = 0; diff --git a/tests/core/satmin.test b/tests/core/satmin.test index 7145c9e46..0d00e0d86 100755 --- a/tests/core/satmin.test +++ b/tests/core/satmin.test @@ -103,11 +103,17 @@ $ltlcross -F formulas \ "{5} $ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \ "{6} $ltl2tgba --det --lbtt -x sat-minimize %f >%T" \ "{7} $ltl2tgba --det --lbtt -x sat-minimize=2 %f >%T" \ + "{8} $ltl2tgba --det --lbtt -x sat-minimize=3 %f >%T" \ + "{9} $ltl2tgba --det --lbtt -x 'sat-minimize=3, incr=-1' %f >%T" \ + "{10} $ltl2tgba --det --lbtt -x 'sat-minimize=3, incr=0' %f >%T" \ + "{11} $ltl2tgba --det --lbtt -x 'sat-minimize=3, incr=1' %f >%T" \ + "{12} $ltl2tgba --det --lbtt -x 'sat-minimize=3, incr=2' %f >%T" \ + "{13} $ltl2tgba --det --lbtt -x 'sat-minimize=3, incr=50' %f >%T" \ --csv=det.csv -grep -v ',\"5\",' det.csv | cut -d ',' -f '1,2,6' > extracted +grep -v ',\"5\",' det.csv | cut -d ',' -f '1,2,6' > output -cat >expected <<'EOF' +cat > expected << EOF "formula","tool","states" "X(X(p0))","1",4 "X(X(p0))","2",4 @@ -115,552 +121,1104 @@ cat >expected <<'EOF' "X(X(p0))","4",4 "X(X(p0))","6",4 "X(X(p0))","7",4 +"X(X(p0))","8",4 +"X(X(p0))","9",4 +"X(X(p0))","10",4 +"X(X(p0))","11",4 +"X(X(p0))","12",4 +"X(X(p0))","13",4 "!(X(X(p0)))","1",4 "!(X(X(p0)))","2",4 "!(X(X(p0)))","3",4 "!(X(X(p0)))","4",4 "!(X(X(p0)))","6",4 "!(X(X(p0)))","7",4 +"!(X(X(p0)))","8",4 +"!(X(X(p0)))","9",4 +"!(X(X(p0)))","10",4 +"!(X(X(p0)))","11",4 +"!(X(X(p0)))","12",4 +"!(X(X(p0)))","13",4 "G(F((p0) -> (X(X(X(p1))))))","1",1 "G(F((p0) -> (X(X(X(p1))))))","2",1 "G(F((p0) -> (X(X(X(p1))))))","3",1 "G(F((p0) -> (X(X(X(p1))))))","4",1 "G(F((p0) -> (X(X(X(p1))))))","6",1 "G(F((p0) -> (X(X(X(p1))))))","7",1 +"G(F((p0) -> (X(X(X(p1))))))","8",1 +"G(F((p0) -> (X(X(X(p1))))))","9",1 +"G(F((p0) -> (X(X(X(p1))))))","10",1 +"G(F((p0) -> (X(X(X(p1))))))","11",1 +"G(F((p0) -> (X(X(X(p1))))))","12",1 +"G(F((p0) -> (X(X(X(p1))))))","13",1 "!(G(F((p0) -> (X(X(X(p1)))))))","1",2 "!(G(F((p0) -> (X(X(X(p1)))))))","2",2 "!(G(F((p0) -> (X(X(X(p1)))))))","3",2 "!(G(F((p0) -> (X(X(X(p1)))))))","4",2 "!(G(F((p0) -> (X(X(X(p1)))))))","6",2 "!(G(F((p0) -> (X(X(X(p1)))))))","7",2 +"!(G(F((p0) -> (X(X(X(p1)))))))","8",2 +"!(G(F((p0) -> (X(X(X(p1)))))))","9",2 +"!(G(F((p0) -> (X(X(X(p1)))))))","10",2 +"!(G(F((p0) -> (X(X(X(p1)))))))","11",2 +"!(G(F((p0) -> (X(X(X(p1)))))))","12",2 +"!(G(F((p0) -> (X(X(X(p1)))))))","13",2 "F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","1",5 "F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","2",5 "F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","3",5 "F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","4",5 "F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","6",5 "F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","7",5 +"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","8",5 +"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","9",5 +"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","10",5 +"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","11",5 +"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","12",5 +"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","13",5 "!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","1",4 "!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","2",4 "!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","3",4 "!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","4",4 "!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","6",4 "!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","7",4 +"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","8",4 +"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","9",4 +"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","10",4 +"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","11",4 +"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","12",4 +"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","13",4 "F((p0) & (X((p1) U (p2))))","1",3 "F((p0) & (X((p1) U (p2))))","2",3 "F((p0) & (X((p1) U (p2))))","3",3 "F((p0) & (X((p1) U (p2))))","4",3 "F((p0) & (X((p1) U (p2))))","6",3 "F((p0) & (X((p1) U (p2))))","7",3 +"F((p0) & (X((p1) U (p2))))","8",3 +"F((p0) & (X((p1) U (p2))))","9",3 +"F((p0) & (X((p1) U (p2))))","10",3 +"F((p0) & (X((p1) U (p2))))","11",3 +"F((p0) & (X((p1) U (p2))))","12",3 +"F((p0) & (X((p1) U (p2))))","13",3 "!(F((p0) & (X((p1) U (p2)))))","1",2 "!(F((p0) & (X((p1) U (p2)))))","2",2 "!(F((p0) & (X((p1) U (p2)))))","3",2 "!(F((p0) & (X((p1) U (p2)))))","4",2 "!(F((p0) & (X((p1) U (p2)))))","6",2 "!(F((p0) & (X((p1) U (p2)))))","7",2 +"!(F((p0) & (X((p1) U (p2)))))","8",2 +"!(F((p0) & (X((p1) U (p2)))))","9",2 +"!(F((p0) & (X((p1) U (p2)))))","10",2 +"!(F((p0) & (X((p1) U (p2)))))","11",2 +"!(F((p0) & (X((p1) U (p2)))))","12",2 +"!(F((p0) & (X((p1) U (p2)))))","13",2 "F((p0) & (X((p1) & (X(F(p2))))))","1",4 "F((p0) & (X((p1) & (X(F(p2))))))","2",4 "F((p0) & (X((p1) & (X(F(p2))))))","3",4 "F((p0) & (X((p1) & (X(F(p2))))))","4",4 "F((p0) & (X((p1) & (X(F(p2))))))","6",4 "F((p0) & (X((p1) & (X(F(p2))))))","7",4 +"F((p0) & (X((p1) & (X(F(p2))))))","8",4 +"F((p0) & (X((p1) & (X(F(p2))))))","9",4 +"F((p0) & (X((p1) & (X(F(p2))))))","10",4 +"F((p0) & (X((p1) & (X(F(p2))))))","11",4 +"F((p0) & (X((p1) & (X(F(p2))))))","12",4 +"F((p0) & (X((p1) & (X(F(p2))))))","13",4 "!(F((p0) & (X((p1) & (X(F(p2)))))))","1",3 "!(F((p0) & (X((p1) & (X(F(p2)))))))","2",3 "!(F((p0) & (X((p1) & (X(F(p2)))))))","3",3 "!(F((p0) & (X((p1) & (X(F(p2)))))))","4",3 "!(F((p0) & (X((p1) & (X(F(p2)))))))","6",3 "!(F((p0) & (X((p1) & (X(F(p2)))))))","7",3 +"!(F((p0) & (X((p1) & (X(F(p2)))))))","8",3 +"!(F((p0) & (X((p1) & (X(F(p2)))))))","9",3 +"!(F((p0) & (X((p1) & (X(F(p2)))))))","10",3 +"!(F((p0) & (X((p1) & (X(F(p2)))))))","11",3 +"!(F((p0) & (X((p1) & (X(F(p2)))))))","12",3 +"!(F((p0) & (X((p1) & (X(F(p2)))))))","13",3 "(p0) U ((p1) & (X((p2) U (p3))))","1",4 "(p0) U ((p1) & (X((p2) U (p3))))","2",4 "(p0) U ((p1) & (X((p2) U (p3))))","3",4 "(p0) U ((p1) & (X((p2) U (p3))))","4",4 "(p0) U ((p1) & (X((p2) U (p3))))","6",4 "(p0) U ((p1) & (X((p2) U (p3))))","7",4 +"(p0) U ((p1) & (X((p2) U (p3))))","8",4 +"(p0) U ((p1) & (X((p2) U (p3))))","9",4 +"(p0) U ((p1) & (X((p2) U (p3))))","10",4 +"(p0) U ((p1) & (X((p2) U (p3))))","11",4 +"(p0) U ((p1) & (X((p2) U (p3))))","12",4 +"(p0) U ((p1) & (X((p2) U (p3))))","13",4 "!((p0) U ((p1) & (X((p2) U (p3)))))","1",4 "!((p0) U ((p1) & (X((p2) U (p3)))))","2",4 "!((p0) U ((p1) & (X((p2) U (p3)))))","3",4 "!((p0) U ((p1) & (X((p2) U (p3)))))","4",4 "!((p0) U ((p1) & (X((p2) U (p3)))))","6",4 "!((p0) U ((p1) & (X((p2) U (p3)))))","7",4 +"!((p0) U ((p1) & (X((p2) U (p3)))))","8",4 +"!((p0) U ((p1) & (X((p2) U (p3)))))","9",4 +"!((p0) U ((p1) & (X((p2) U (p3)))))","10",4 +"!((p0) U ((p1) & (X((p2) U (p3)))))","11",4 +"!((p0) U ((p1) & (X((p2) U (p3)))))","12",4 +"!((p0) U ((p1) & (X((p2) U (p3)))))","13",4 "(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","1",4 "(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","2",4 "(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","3",4 "(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","4",4 "(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","6",4 "(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","7",4 +"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","8",4 +"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","9",4 +"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","10",4 +"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","11",4 +"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","12",4 +"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","13",4 "!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","1",3 "!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","2",3 "!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","3",3 "!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","4",3 "!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","6",3 "!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","7",3 +"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","8",3 +"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","9",3 +"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","10",3 +"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","11",3 +"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","12",3 +"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","13",3 "(G(F(p0))) & (G(F(p1)))","1",1 "(G(F(p0))) & (G(F(p1)))","2",1 "(G(F(p0))) & (G(F(p1)))","3",1 "(G(F(p0))) & (G(F(p1)))","4",1 "(G(F(p0))) & (G(F(p1)))","6",1 "(G(F(p0))) & (G(F(p1)))","7",1 +"(G(F(p0))) & (G(F(p1)))","8",1 +"(G(F(p0))) & (G(F(p1)))","9",1 +"(G(F(p0))) & (G(F(p1)))","10",1 +"(G(F(p0))) & (G(F(p1)))","11",1 +"(G(F(p0))) & (G(F(p1)))","12",1 +"(G(F(p0))) & (G(F(p1)))","13",1 "!((G(F(p0))) & (G(F(p1))))","1",3 "!((G(F(p0))) & (G(F(p1))))","2",3 "!((G(F(p0))) & (G(F(p1))))","3",3 "!((G(F(p0))) & (G(F(p1))))","4",3 "!((G(F(p0))) & (G(F(p1))))","6",3 "!((G(F(p0))) & (G(F(p1))))","7",3 +"!((G(F(p0))) & (G(F(p1))))","8",3 +"!((G(F(p0))) & (G(F(p1))))","9",3 +"!((G(F(p0))) & (G(F(p1))))","10",3 +"!((G(F(p0))) & (G(F(p1))))","11",3 +"!((G(F(p0))) & (G(F(p1))))","12",3 +"!((G(F(p0))) & (G(F(p1))))","13",3 "(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","1",1 "(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","2",1 "(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","3",1 "(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","4",1 "(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","6",1 "(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","7",1 +"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","8",1 +"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","9",1 +"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","10",1 +"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","11",1 +"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","12",1 +"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","13",1 "!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","1",2 "!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","2",2 "!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","3",2 "!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","4",2 "!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","6",2 "!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","7",2 +"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","8",2 +"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","9",2 +"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","10",2 +"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","11",2 +"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","12",2 +"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","13",2 "G(F(p0))","1",1 "G(F(p0))","2",1 "G(F(p0))","3",1 "G(F(p0))","4",1 "G(F(p0))","6",1 "G(F(p0))","7",1 +"G(F(p0))","8",1 +"G(F(p0))","9",1 +"G(F(p0))","10",1 +"G(F(p0))","11",1 +"G(F(p0))","12",1 +"G(F(p0))","13",1 "!(G(F(p0)))","1",2 "!(G(F(p0)))","2",2 "!(G(F(p0)))","3",2 "!(G(F(p0)))","4",2 "!(G(F(p0)))","6",2 "!(G(F(p0)))","7",2 +"!(G(F(p0)))","8",2 +"!(G(F(p0)))","9",2 +"!(G(F(p0)))","10",2 +"!(G(F(p0)))","11",2 +"!(G(F(p0)))","12",2 +"!(G(F(p0)))","13",2 "(p0) U ((p1) U ((p2) U (p3)))","1",4 "(p0) U ((p1) U ((p2) U (p3)))","2",4 "(p0) U ((p1) U ((p2) U (p3)))","3",4 "(p0) U ((p1) U ((p2) U (p3)))","4",4 "(p0) U ((p1) U ((p2) U (p3)))","6",4 "(p0) U ((p1) U ((p2) U (p3)))","7",4 +"(p0) U ((p1) U ((p2) U (p3)))","8",4 +"(p0) U ((p1) U ((p2) U (p3)))","9",4 +"(p0) U ((p1) U ((p2) U (p3)))","10",4 +"(p0) U ((p1) U ((p2) U (p3)))","11",4 +"(p0) U ((p1) U ((p2) U (p3)))","12",4 +"(p0) U ((p1) U ((p2) U (p3)))","13",4 "!((p0) U ((p1) U ((p2) U (p3))))","1",4 "!((p0) U ((p1) U ((p2) U (p3))))","2",4 "!((p0) U ((p1) U ((p2) U (p3))))","3",4 "!((p0) U ((p1) U ((p2) U (p3))))","4",4 "!((p0) U ((p1) U ((p2) U (p3))))","6",4 "!((p0) U ((p1) U ((p2) U (p3))))","7",4 +"!((p0) U ((p1) U ((p2) U (p3))))","8",4 +"!((p0) U ((p1) U ((p2) U (p3))))","9",4 +"!((p0) U ((p1) U ((p2) U (p3))))","10",4 +"!((p0) U ((p1) U ((p2) U (p3))))","11",4 +"!((p0) U ((p1) U ((p2) U (p3))))","12",4 +"!((p0) U ((p1) U ((p2) U (p3))))","13",4 "(G((p0) -> (F(p1)))) & (G(p2))","1",2 "(G((p0) -> (F(p1)))) & (G(p2))","2",2 "(G((p0) -> (F(p1)))) & (G(p2))","3",2 "(G((p0) -> (F(p1)))) & (G(p2))","4",2 "(G((p0) -> (F(p1)))) & (G(p2))","6",2 "(G((p0) -> (F(p1)))) & (G(p2))","7",2 +"(G((p0) -> (F(p1)))) & (G(p2))","8",2 +"(G((p0) -> (F(p1)))) & (G(p2))","9",2 +"(G((p0) -> (F(p1)))) & (G(p2))","10",2 +"(G((p0) -> (F(p1)))) & (G(p2))","11",2 +"(G((p0) -> (F(p1)))) & (G(p2))","12",2 +"(G((p0) -> (F(p1)))) & (G(p2))","13",2 "!((G((p0) -> (F(p1)))) & (G(p2)))","1",3 "!((G((p0) -> (F(p1)))) & (G(p2)))","2",3 "!((G((p0) -> (F(p1)))) & (G(p2)))","3",3 "!((G((p0) -> (F(p1)))) & (G(p2)))","4",3 "!((G((p0) -> (F(p1)))) & (G(p2)))","6",3 "!((G((p0) -> (F(p1)))) & (G(p2)))","7",3 +"!((G((p0) -> (F(p1)))) & (G(p2)))","8",3 +"!((G((p0) -> (F(p1)))) & (G(p2)))","9",3 +"!((G((p0) -> (F(p1)))) & (G(p2)))","10",3 +"!((G((p0) -> (F(p1)))) & (G(p2)))","11",3 +"!((G((p0) -> (F(p1)))) & (G(p2)))","12",3 +"!((G((p0) -> (F(p1)))) & (G(p2)))","13",3 "((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","1",4 "((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","2",4 "((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","3",4 "((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","4",4 "((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","6",4 "((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","7",4 +"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","8",4 +"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","9",4 +"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","10",4 +"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","11",4 +"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","12",4 +"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","13",4 "!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","1",3 "!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","2",3 "!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","3",3 "!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","4",3 "!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","6",3 "!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","7",3 +"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","8",3 +"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","9",3 +"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","10",3 +"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","11",3 +"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","12",3 +"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","13",3 "(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","1",4 "(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","2",4 "(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","3",4 "(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","4",3 "(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","6",3 "(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","7",3 +"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","8",3 +"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","9",3 +"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","10",3 +"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","11",3 +"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","12",3 +"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","13",3 "!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","1",3 "!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","2",3 "!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","3",3 "!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","4",3 "!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","6",3 "!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","7",3 +"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","8",3 +"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","9",3 +"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","10",3 +"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","11",3 +"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","12",3 +"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","13",3 "(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","1",3 "(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","2",3 "(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","3",3 "(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","4",3 "(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","6",3 "(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","7",3 +"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","8",3 +"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","9",3 +"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","10",3 +"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","11",3 +"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","12",3 +"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","13",3 "!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","1",3 "!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","2",3 "!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","3",3 "!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","4",3 "!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","6",3 "!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","7",3 +"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","8",3 +"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","9",3 +"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","10",3 +"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","11",3 +"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","12",3 +"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","13",3 "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","1",1 "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","2",1 "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","3",1 "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","4",1 "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","6",1 "(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","7",1 +"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","8",1 +"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","9",1 +"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","10",1 +"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","11",1 +"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","12",1 +"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","13",1 "!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","1",5 "!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","2",5 "!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","3",5 "!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","4",5 "!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","6",5 "!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","7",5 +"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","8",5 +"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","9",5 +"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","10",5 +"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","11",5 +"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","12",5 +"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","13",5 "G((p0) -> ((p1) U (p2)))","1",2 "G((p0) -> ((p1) U (p2)))","2",2 "G((p0) -> ((p1) U (p2)))","3",2 "G((p0) -> ((p1) U (p2)))","4",2 "G((p0) -> ((p1) U (p2)))","6",2 "G((p0) -> ((p1) U (p2)))","7",2 +"G((p0) -> ((p1) U (p2)))","8",2 +"G((p0) -> ((p1) U (p2)))","9",2 +"G((p0) -> ((p1) U (p2)))","10",2 +"G((p0) -> ((p1) U (p2)))","11",2 +"G((p0) -> ((p1) U (p2)))","12",2 +"G((p0) -> ((p1) U (p2)))","13",2 "!(G((p0) -> ((p1) U (p2))))","1",3 "!(G((p0) -> ((p1) U (p2))))","2",3 "!(G((p0) -> ((p1) U (p2))))","3",3 "!(G((p0) -> ((p1) U (p2))))","4",3 "!(G((p0) -> ((p1) U (p2))))","6",3 "!(G((p0) -> ((p1) U (p2))))","7",3 +"!(G((p0) -> ((p1) U (p2))))","8",3 +"!(G((p0) -> ((p1) U (p2))))","9",3 +"!(G((p0) -> ((p1) U (p2))))","10",3 +"!(G((p0) -> ((p1) U (p2))))","11",3 +"!(G((p0) -> ((p1) U (p2))))","12",3 +"!(G((p0) -> ((p1) U (p2))))","13",3 "G(F((p0) <-> (X(X(p1)))))","1",9 "G(F((p0) <-> (X(X(p1)))))","2",7 "G(F((p0) <-> (X(X(p1)))))","3",4 "G(F((p0) <-> (X(X(p1)))))","4",4 "G(F((p0) <-> (X(X(p1)))))","6",4 "G(F((p0) <-> (X(X(p1)))))","7",4 +"G(F((p0) <-> (X(X(p1)))))","8",4 +"G(F((p0) <-> (X(X(p1)))))","9",4 +"G(F((p0) <-> (X(X(p1)))))","10",4 +"G(F((p0) <-> (X(X(p1)))))","11",4 +"G(F((p0) <-> (X(X(p1)))))","12",4 +"G(F((p0) <-> (X(X(p1)))))","13",4 "!(G(F((p0) <-> (X(X(p1))))))","1",7 "!(G(F((p0) <-> (X(X(p1))))))","2",7 "!(G(F((p0) <-> (X(X(p1))))))","3",7 "!(G(F((p0) <-> (X(X(p1))))))","4",7 "!(G(F((p0) <-> (X(X(p1))))))","6",7 "!(G(F((p0) <-> (X(X(p1))))))","7",7 +"!(G(F((p0) <-> (X(X(p1))))))","8",7 +"!(G(F((p0) <-> (X(X(p1))))))","9",7 +"!(G(F((p0) <-> (X(X(p1))))))","10",7 +"!(G(F((p0) <-> (X(X(p1))))))","11",7 +"!(G(F((p0) <-> (X(X(p1))))))","12",7 +"!(G(F((p0) <-> (X(X(p1))))))","13",7 "(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","1",1 "(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","2",1 "(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","3",1 "(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","4",1 "(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","6",1 "(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","7",1 +"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","8",1 +"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","9",1 +"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","10",1 +"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","11",1 +"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","12",1 +"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","13",1 "!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","1",2 "!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","2",2 "!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","3",2 "!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","4",2 "!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","6",2 "!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","7",2 +"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","8",2 +"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","9",2 +"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","10",2 +"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","11",2 +"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","12",2 +"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","13",2 "G((p0) -> (X(X(X(p1)))))","1",8 "G((p0) -> (X(X(X(p1)))))","2",8 "G((p0) -> (X(X(X(p1)))))","3",8 "G((p0) -> (X(X(X(p1)))))","4",8 "G((p0) -> (X(X(X(p1)))))","6",8 "G((p0) -> (X(X(X(p1)))))","7",8 +"G((p0) -> (X(X(X(p1)))))","8",8 +"G((p0) -> (X(X(X(p1)))))","9",8 +"G((p0) -> (X(X(X(p1)))))","10",8 +"G((p0) -> (X(X(X(p1)))))","11",8 +"G((p0) -> (X(X(X(p1)))))","12",8 +"G((p0) -> (X(X(X(p1)))))","13",8 "!(G((p0) -> (X(X(X(p1))))))","1",9 "!(G((p0) -> (X(X(X(p1))))))","2",9 "!(G((p0) -> (X(X(X(p1))))))","3",9 "!(G((p0) -> (X(X(X(p1))))))","4",9 "!(G((p0) -> (X(X(X(p1))))))","6",9 "!(G((p0) -> (X(X(X(p1))))))","7",9 +"!(G((p0) -> (X(X(X(p1))))))","8",9 +"!(G((p0) -> (X(X(X(p1))))))","9",9 +"!(G((p0) -> (X(X(X(p1))))))","10",9 +"!(G((p0) -> (X(X(X(p1))))))","11",9 +"!(G((p0) -> (X(X(X(p1))))))","12",9 +"!(G((p0) -> (X(X(X(p1))))))","13",9 "G((p0) -> (F(p1)))","1",2 "G((p0) -> (F(p1)))","2",2 "G((p0) -> (F(p1)))","3",2 "G((p0) -> (F(p1)))","4",2 "G((p0) -> (F(p1)))","6",2 "G((p0) -> (F(p1)))","7",2 +"G((p0) -> (F(p1)))","8",2 +"G((p0) -> (F(p1)))","9",2 +"G((p0) -> (F(p1)))","10",2 +"G((p0) -> (F(p1)))","11",2 +"G((p0) -> (F(p1)))","12",2 +"G((p0) -> (F(p1)))","13",2 "!(G((p0) -> (F(p1))))","1",2 "!(G((p0) -> (F(p1))))","2",2 "!(G((p0) -> (F(p1))))","3",2 "!(G((p0) -> (F(p1))))","4",2 "!(G((p0) -> (F(p1))))","6",2 "!(G((p0) -> (F(p1))))","7",2 +"!(G((p0) -> (F(p1))))","8",2 +"!(G((p0) -> (F(p1))))","9",2 +"!(G((p0) -> (F(p1))))","10",2 +"!(G((p0) -> (F(p1))))","11",2 +"!(G((p0) -> (F(p1))))","12",2 +"!(G((p0) -> (F(p1))))","13",2 "G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","1",1 "G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","2",1 "G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","3",1 "G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","4",1 "G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","6",1 "G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","7",1 +"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","8",1 +"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","9",1 +"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","10",1 +"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","11",1 +"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","12",1 +"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","13",1 "!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","1",2 "!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","2",2 "!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","3",2 "!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","4",2 "!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","6",2 "!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","7",2 +"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","8",2 +"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","9",2 +"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","10",2 +"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","11",2 +"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","12",2 +"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","13",2 "X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","1",4 "X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","2",5 "X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","3",5 "X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","4",5 "X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","6",5 "X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","7",5 +"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","8",5 +"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","9",5 +"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","10",5 +"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","11",5 +"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","12",5 +"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","13",5 "!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","1",6 "!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","2",6 "!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","3",6 "!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","4",6 "!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","6",6 "!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","7",6 +"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","8",6 +"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","9",6 +"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","10",6 +"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","11",6 +"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","12",6 +"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","13",6 "((!(p0)) M (!(p1))) W (F(!(p2)))","1",4 "((!(p0)) M (!(p1))) W (F(!(p2)))","2",5 "((!(p0)) M (!(p1))) W (F(!(p2)))","3",3 "((!(p0)) M (!(p1))) W (F(!(p2)))","4",3 "((!(p0)) M (!(p1))) W (F(!(p2)))","6",3 "((!(p0)) M (!(p1))) W (F(!(p2)))","7",3 +"((!(p0)) M (!(p1))) W (F(!(p2)))","8",3 +"((!(p0)) M (!(p1))) W (F(!(p2)))","9",3 +"((!(p0)) M (!(p1))) W (F(!(p2)))","10",3 +"((!(p0)) M (!(p1))) W (F(!(p2)))","11",3 +"((!(p0)) M (!(p1))) W (F(!(p2)))","12",3 +"((!(p0)) M (!(p1))) W (F(!(p2)))","13",3 "!(((!(p0)) M (!(p1))) W (F(!(p2))))","1",3 "!(((!(p0)) M (!(p1))) W (F(!(p2))))","2",3 "!(((!(p0)) M (!(p1))) W (F(!(p2))))","3",3 "!(((!(p0)) M (!(p1))) W (F(!(p2))))","4",3 "!(((!(p0)) M (!(p1))) W (F(!(p2))))","6",3 "!(((!(p0)) M (!(p1))) W (F(!(p2))))","7",3 +"!(((!(p0)) M (!(p1))) W (F(!(p2))))","8",3 +"!(((!(p0)) M (!(p1))) W (F(!(p2))))","9",3 +"!(((!(p0)) M (!(p1))) W (F(!(p2))))","10",3 +"!(((!(p0)) M (!(p1))) W (F(!(p2))))","11",3 +"!(((!(p0)) M (!(p1))) W (F(!(p2))))","12",3 +"!(((!(p0)) M (!(p1))) W (F(!(p2))))","13",3 "((p0) & (F(p1)) & (G(F(p2)))) R (p1)","1",2 "((p0) & (F(p1)) & (G(F(p2)))) R (p1)","2",3 "((p0) & (F(p1)) & (G(F(p2)))) R (p1)","3",3 "((p0) & (F(p1)) & (G(F(p2)))) R (p1)","4",3 "((p0) & (F(p1)) & (G(F(p2)))) R (p1)","6",3 "((p0) & (F(p1)) & (G(F(p2)))) R (p1)","7",3 +"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","8",3 +"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","9",3 +"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","10",3 +"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","11",3 +"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","12",3 +"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","13",3 "!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","1",5 "!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","2",5 "!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","3",5 "!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","4",5 "!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","6",5 "!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","7",5 +"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","8",5 +"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","9",5 +"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","10",5 +"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","11",5 +"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","12",5 +"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","13",5 "((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","1",3 "((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","2",2 "((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","3",2 "((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","4",2 "((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","6",2 "((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","7",2 +"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","8",2 +"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","9",2 +"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","10",2 +"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","11",2 +"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","12",2 +"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","13",2 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","1",4 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","2",4 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","3",4 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","4",4 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","6",4 "!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","7",4 +"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","8",4 +"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","9",4 +"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","10",4 +"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","11",4 +"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","12",4 +"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","13",4 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","1",5 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","2",7 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","3",6 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","4",6 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","6",6 "X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","7",6 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","8",6 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","9",6 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","10",6 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","11",6 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","12",6 +"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","13",6 "!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","1",8 "!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","2",8 "!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","3",8 "!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","4",8 "!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","6",8 "!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","7",8 +"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","8",8 +"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","9",8 +"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","10",8 +"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","11",8 +"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","12",8 +"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","13",8 "(F(p0)) W (G(p1))","1",3 "(F(p0)) W (G(p1))","2",2 "(F(p0)) W (G(p1))","3",2 "(F(p0)) W (G(p1))","4",2 "(F(p0)) W (G(p1))","6",2 "(F(p0)) W (G(p1))","7",2 +"(F(p0)) W (G(p1))","8",2 +"(F(p0)) W (G(p1))","9",2 +"(F(p0)) W (G(p1))","10",2 +"(F(p0)) W (G(p1))","11",2 +"(F(p0)) W (G(p1))","12",2 +"(F(p0)) W (G(p1))","13",2 "!((F(p0)) W (G(p1)))","1",2 "!((F(p0)) W (G(p1)))","2",2 "!((F(p0)) W (G(p1)))","3",2 "!((F(p0)) W (G(p1)))","4",2 "!((F(p0)) W (G(p1)))","6",2 "!((F(p0)) W (G(p1)))","7",2 +"!((F(p0)) W (G(p1)))","8",2 +"!((F(p0)) W (G(p1)))","9",2 +"!((F(p0)) W (G(p1)))","10",2 +"!((F(p0)) W (G(p1)))","11",2 +"!((F(p0)) W (G(p1)))","12",2 +"!((F(p0)) W (G(p1)))","13",2 "(G(F(p1))) | (G(p0))","1",3 "(G(F(p1))) | (G(p0))","2",3 "(G(F(p1))) | (G(p0))","3",2 "(G(F(p1))) | (G(p0))","4",2 "(G(F(p1))) | (G(p0))","6",2 "(G(F(p1))) | (G(p0))","7",2 +"(G(F(p1))) | (G(p0))","8",2 +"(G(F(p1))) | (G(p0))","9",2 +"(G(F(p1))) | (G(p0))","10",2 +"(G(F(p1))) | (G(p0))","11",2 +"(G(F(p1))) | (G(p0))","12",2 +"(G(F(p1))) | (G(p0))","13",2 "!((G(F(p1))) | (G(p0)))","1",3 "!((G(F(p1))) | (G(p0)))","2",3 "!((G(F(p1))) | (G(p0)))","3",3 "!((G(F(p1))) | (G(p0)))","4",3 "!((G(F(p1))) | (G(p0)))","6",3 "!((G(F(p1))) | (G(p0)))","7",3 +"!((G(F(p1))) | (G(p0)))","8",3 +"!((G(F(p1))) | (G(p0)))","9",3 +"!((G(F(p1))) | (G(p0)))","10",3 +"!((G(F(p1))) | (G(p0)))","11",3 +"!((G(F(p1))) | (G(p0)))","12",3 +"!((G(F(p1))) | (G(p0)))","13",3 "(p0) M (G((F(!(p1))) | (X(!(p0)))))","1",5 "(p0) M (G((F(!(p1))) | (X(!(p0)))))","2",5 "(p0) M (G((F(!(p1))) | (X(!(p0)))))","3",5 "(p0) M (G((F(!(p1))) | (X(!(p0)))))","4",5 "(p0) M (G((F(!(p1))) | (X(!(p0)))))","6",5 "(p0) M (G((F(!(p1))) | (X(!(p0)))))","7",5 +"(p0) M (G((F(!(p1))) | (X(!(p0)))))","8",5 +"(p0) M (G((F(!(p1))) | (X(!(p0)))))","9",5 +"(p0) M (G((F(!(p1))) | (X(!(p0)))))","10",5 +"(p0) M (G((F(!(p1))) | (X(!(p0)))))","11",5 +"(p0) M (G((F(!(p1))) | (X(!(p0)))))","12",5 +"(p0) M (G((F(!(p1))) | (X(!(p0)))))","13",5 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","1",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","2",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","3",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","4",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","6",4 "!((p0) M (G((F(!(p1))) | (X(!(p0))))))","7",4 +"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","8",4 +"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","9",4 +"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","10",4 +"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","11",4 +"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","12",4 +"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","13",4 "(G(!(p0))) R (X(F(p1)))","1",4 "(G(!(p0))) R (X(F(p1)))","2",4 "(G(!(p0))) R (X(F(p1)))","3",3 "(G(!(p0))) R (X(F(p1)))","4",3 "(G(!(p0))) R (X(F(p1)))","6",3 "(G(!(p0))) R (X(F(p1)))","7",3 +"(G(!(p0))) R (X(F(p1)))","8",3 +"(G(!(p0))) R (X(F(p1)))","9",3 +"(G(!(p0))) R (X(F(p1)))","10",3 +"(G(!(p0))) R (X(F(p1)))","11",3 +"(G(!(p0))) R (X(F(p1)))","12",3 +"(G(!(p0))) R (X(F(p1)))","13",3 "!((G(!(p0))) R (X(F(p1))))","1",3 "!((G(!(p0))) R (X(F(p1))))","2",3 "!((G(!(p0))) R (X(F(p1))))","3",3 "!((G(!(p0))) R (X(F(p1))))","4",3 "!((G(!(p0))) R (X(F(p1))))","6",3 "!((G(!(p0))) R (X(F(p1))))","7",3 +"!((G(!(p0))) R (X(F(p1))))","8",3 +"!((G(!(p0))) R (X(F(p1))))","9",3 +"!((G(!(p0))) R (X(F(p1))))","10",3 +"!((G(!(p0))) R (X(F(p1))))","11",3 +"!((G(!(p0))) R (X(F(p1))))","12",3 +"!((G(!(p0))) R (X(F(p1))))","13",3 "X(F((!(p0)) | (G(F(p1)))))","1",4 "X(F((!(p0)) | (G(F(p1)))))","2",4 "X(F((!(p0)) | (G(F(p1)))))","3",3 "X(F((!(p0)) | (G(F(p1)))))","4",3 "X(F((!(p0)) | (G(F(p1)))))","6",3 "X(F((!(p0)) | (G(F(p1)))))","7",3 +"X(F((!(p0)) | (G(F(p1)))))","8",3 +"X(F((!(p0)) | (G(F(p1)))))","9",3 +"X(F((!(p0)) | (G(F(p1)))))","10",3 +"X(F((!(p0)) | (G(F(p1)))))","11",3 +"X(F((!(p0)) | (G(F(p1)))))","12",3 +"X(F((!(p0)) | (G(F(p1)))))","13",3 "!(X(F((!(p0)) | (G(F(p1))))))","1",3 "!(X(F((!(p0)) | (G(F(p1))))))","2",3 "!(X(F((!(p0)) | (G(F(p1))))))","3",3 "!(X(F((!(p0)) | (G(F(p1))))))","4",3 "!(X(F((!(p0)) | (G(F(p1))))))","6",3 "!(X(F((!(p0)) | (G(F(p1))))))","7",3 +"!(X(F((!(p0)) | (G(F(p1))))))","8",3 +"!(X(F((!(p0)) | (G(F(p1))))))","9",3 +"!(X(F((!(p0)) | (G(F(p1))))))","10",3 +"!(X(F((!(p0)) | (G(F(p1))))))","11",3 +"!(X(F((!(p0)) | (G(F(p1))))))","12",3 +"!(X(F((!(p0)) | (G(F(p1))))))","13",3 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","1",6 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","2",6 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","3",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","4",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","6",5 "(G((F(!(p0))) U (!(p0)))) U (X(p0))","7",5 +"(G((F(!(p0))) U (!(p0)))) U (X(p0))","8",5 +"(G((F(!(p0))) U (!(p0)))) U (X(p0))","9",5 +"(G((F(!(p0))) U (!(p0)))) U (X(p0))","10",5 +"(G((F(!(p0))) U (!(p0)))) U (X(p0))","11",5 +"(G((F(!(p0))) U (!(p0)))) U (X(p0))","12",5 +"(G((F(!(p0))) U (!(p0)))) U (X(p0))","13",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","1",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","2",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","3",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","4",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","6",5 "!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","7",5 +"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","8",5 +"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","9",5 +"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","10",5 +"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","11",5 +"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","12",5 +"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","13",5 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","1",4 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","2",5 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","3",4 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","4",4 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","6",4 "((p0) | (G((p0) M (!(p1))))) W (F(p2))","7",4 +"((p0) | (G((p0) M (!(p1))))) W (F(p2))","8",4 +"((p0) | (G((p0) M (!(p1))))) W (F(p2))","9",4 +"((p0) | (G((p0) M (!(p1))))) W (F(p2))","10",4 +"((p0) | (G((p0) M (!(p1))))) W (F(p2))","11",4 +"((p0) | (G((p0) M (!(p1))))) W (F(p2))","12",4 +"((p0) | (G((p0) M (!(p1))))) W (F(p2))","13",4 "!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","1",4 "!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","2",4 "!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","3",4 "!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","4",4 "!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","6",4 "!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","7",4 +"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","8",4 +"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","9",4 +"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","10",4 +"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","11",4 +"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","12",4 +"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","13",4 "(F(p0)) W (X(p1))","1",6 "(F(p0)) W (X(p1))","2",6 "(F(p0)) W (X(p1))","3",6 "(F(p0)) W (X(p1))","4",6 "(F(p0)) W (X(p1))","6",6 "(F(p0)) W (X(p1))","7",6 +"(F(p0)) W (X(p1))","8",6 +"(F(p0)) W (X(p1))","9",6 +"(F(p0)) W (X(p1))","10",6 +"(F(p0)) W (X(p1))","11",6 +"(F(p0)) W (X(p1))","12",6 +"(F(p0)) W (X(p1))","13",6 "!((F(p0)) W (X(p1)))","1",4 "!((F(p0)) W (X(p1)))","2",4 "!((F(p0)) W (X(p1)))","3",4 "!((F(p0)) W (X(p1)))","4",4 "!((F(p0)) W (X(p1)))","6",4 "!((F(p0)) W (X(p1)))","7",4 +"!((F(p0)) W (X(p1)))","8",4 +"!((F(p0)) W (X(p1)))","9",4 +"!((F(p0)) W (X(p1)))","10",4 +"!((F(p0)) W (X(p1)))","11",4 +"!((F(p0)) W (X(p1)))","12",4 +"!((F(p0)) W (X(p1)))","13",4 "(X(G(!(p0)))) R (F(p1))","1",2 "(X(G(!(p0)))) R (F(p1))","2",2 "(X(G(!(p0)))) R (F(p1))","3",2 "(X(G(!(p0)))) R (F(p1))","4",2 "(X(G(!(p0)))) R (F(p1))","6",2 "(X(G(!(p0)))) R (F(p1))","7",2 +"(X(G(!(p0)))) R (F(p1))","8",2 +"(X(G(!(p0)))) R (F(p1))","9",2 +"(X(G(!(p0)))) R (F(p1))","10",2 +"(X(G(!(p0)))) R (F(p1))","11",2 +"(X(G(!(p0)))) R (F(p1))","12",2 +"(X(G(!(p0)))) R (F(p1))","13",2 "!((X(G(!(p0)))) R (F(p1)))","1",3 "!((X(G(!(p0)))) R (F(p1)))","2",3 "!((X(G(!(p0)))) R (F(p1)))","3",3 "!((X(G(!(p0)))) R (F(p1)))","4",3 "!((X(G(!(p0)))) R (F(p1)))","6",3 "!((X(G(!(p0)))) R (F(p1)))","7",3 +"!((X(G(!(p0)))) R (F(p1)))","8",3 +"!((X(G(!(p0)))) R (F(p1)))","9",3 +"!((X(G(!(p0)))) R (F(p1)))","10",3 +"!((X(G(!(p0)))) R (F(p1)))","11",3 +"!((X(G(!(p0)))) R (F(p1)))","12",3 +"!((X(G(!(p0)))) R (F(p1)))","13",3 "(G(F(p0))) | ((p1) & (F(p2)))","1",4 "(G(F(p0))) | ((p1) & (F(p2)))","2",4 "(G(F(p0))) | ((p1) & (F(p2)))","3",4 "(G(F(p0))) | ((p1) & (F(p2)))","4",4 "(G(F(p0))) | ((p1) & (F(p2)))","6",4 "(G(F(p0))) | ((p1) & (F(p2)))","7",4 +"(G(F(p0))) | ((p1) & (F(p2)))","8",4 +"(G(F(p0))) | ((p1) & (F(p2)))","9",4 +"(G(F(p0))) | ((p1) & (F(p2)))","10",4 +"(G(F(p0))) | ((p1) & (F(p2)))","11",4 +"(G(F(p0))) | ((p1) & (F(p2)))","12",4 +"(G(F(p0))) | ((p1) & (F(p2)))","13",4 "!((G(F(p0))) | ((p1) & (F(p2))))","1",5 "!((G(F(p0))) | ((p1) & (F(p2))))","2",5 "!((G(F(p0))) | ((p1) & (F(p2))))","3",5 "!((G(F(p0))) | ((p1) & (F(p2))))","4",5 "!((G(F(p0))) | ((p1) & (F(p2))))","6",5 "!((G(F(p0))) | ((p1) & (F(p2))))","7",5 +"!((G(F(p0))) | ((p1) & (F(p2))))","8",5 +"!((G(F(p0))) | ((p1) & (F(p2))))","9",5 +"!((G(F(p0))) | ((p1) & (F(p2))))","10",5 +"!((G(F(p0))) | ((p1) & (F(p2))))","11",5 +"!((G(F(p0))) | ((p1) & (F(p2))))","12",5 +"!((G(F(p0))) | ((p1) & (F(p2))))","13",5 "X((p0) R ((F(p1)) R (F(!(p1)))))","1",6 "X((p0) R ((F(p1)) R (F(!(p1)))))","2",6 "X((p0) R ((F(p1)) R (F(!(p1)))))","3",4 "X((p0) R ((F(p1)) R (F(!(p1)))))","4",4 "X((p0) R ((F(p1)) R (F(!(p1)))))","6",4 "X((p0) R ((F(p1)) R (F(!(p1)))))","7",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","8",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","9",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","10",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","11",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","12",4 +"X((p0) R ((F(p1)) R (F(!(p1)))))","13",4 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","1",3 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","2",3 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","3",3 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","4",3 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","6",3 "!(X((p0) R ((F(p1)) R (F(!(p1))))))","7",3 +"!(X((p0) R ((F(p1)) R (F(!(p1))))))","8",3 +"!(X((p0) R ((F(p1)) R (F(!(p1))))))","9",3 +"!(X((p0) R ((F(p1)) R (F(!(p1))))))","10",3 +"!(X((p0) R ((F(p1)) R (F(!(p1))))))","11",3 +"!(X((p0) R ((F(p1)) R (F(!(p1))))))","12",3 +"!(X((p0) R ((F(p1)) R (F(!(p1))))))","13",3 "G((X(p0)) M (F(p0)))","1",2 "G((X(p0)) M (F(p0)))","2",2 "G((X(p0)) M (F(p0)))","3",1 "G((X(p0)) M (F(p0)))","4",1 "G((X(p0)) M (F(p0)))","6",1 "G((X(p0)) M (F(p0)))","7",1 +"G((X(p0)) M (F(p0)))","8",1 +"G((X(p0)) M (F(p0)))","9",1 +"G((X(p0)) M (F(p0)))","10",1 +"G((X(p0)) M (F(p0)))","11",1 +"G((X(p0)) M (F(p0)))","12",1 +"G((X(p0)) M (F(p0)))","13",1 "!(G((X(p0)) M (F(p0))))","1",2 "!(G((X(p0)) M (F(p0))))","2",2 "!(G((X(p0)) M (F(p0))))","3",2 "!(G((X(p0)) M (F(p0))))","4",2 "!(G((X(p0)) M (F(p0))))","6",2 "!(G((X(p0)) M (F(p0))))","7",2 +"!(G((X(p0)) M (F(p0))))","8",2 +"!(G((X(p0)) M (F(p0))))","9",2 +"!(G((X(p0)) M (F(p0))))","10",2 +"!(G((X(p0)) M (F(p0))))","11",2 +"!(G((X(p0)) M (F(p0))))","12",2 +"!(G((X(p0)) M (F(p0))))","13",2 "X((G(F(p1))) | (G(p0)))","1",4 "X((G(F(p1))) | (G(p0)))","2",4 "X((G(F(p1))) | (G(p0)))","3",3 "X((G(F(p1))) | (G(p0)))","4",3 "X((G(F(p1))) | (G(p0)))","6",3 "X((G(F(p1))) | (G(p0)))","7",3 +"X((G(F(p1))) | (G(p0)))","8",3 +"X((G(F(p1))) | (G(p0)))","9",3 +"X((G(F(p1))) | (G(p0)))","10",3 +"X((G(F(p1))) | (G(p0)))","11",3 +"X((G(F(p1))) | (G(p0)))","12",3 +"X((G(F(p1))) | (G(p0)))","13",3 "!(X((G(F(p1))) | (G(p0))))","1",4 "!(X((G(F(p1))) | (G(p0))))","2",4 "!(X((G(F(p1))) | (G(p0))))","3",4 "!(X((G(F(p1))) | (G(p0))))","4",4 "!(X((G(F(p1))) | (G(p0))))","6",4 "!(X((G(F(p1))) | (G(p0))))","7",4 +"!(X((G(F(p1))) | (G(p0))))","8",4 +"!(X((G(F(p1))) | (G(p0))))","9",4 +"!(X((G(F(p1))) | (G(p0))))","10",4 +"!(X((G(F(p1))) | (G(p0))))","11",4 +"!(X((G(F(p1))) | (G(p0))))","12",4 +"!(X((G(F(p1))) | (G(p0))))","13",4 "(G(p0)) R (F(p1))","1",2 "(G(p0)) R (F(p1))","2",2 "(G(p0)) R (F(p1))","3",2 "(G(p0)) R (F(p1))","4",2 "(G(p0)) R (F(p1))","6",2 "(G(p0)) R (F(p1))","7",2 +"(G(p0)) R (F(p1))","8",2 +"(G(p0)) R (F(p1))","9",2 +"(G(p0)) R (F(p1))","10",2 +"(G(p0)) R (F(p1))","11",2 +"(G(p0)) R (F(p1))","12",2 +"(G(p0)) R (F(p1))","13",2 "!((G(p0)) R (F(p1)))","1",3 "!((G(p0)) R (F(p1)))","2",3 "!((G(p0)) R (F(p1)))","3",3 "!((G(p0)) R (F(p1)))","4",3 "!((G(p0)) R (F(p1)))","6",3 "!((G(p0)) R (F(p1)))","7",3 +"!((G(p0)) R (F(p1)))","8",3 +"!((G(p0)) R (F(p1)))","9",3 +"!((G(p0)) R (F(p1)))","10",3 +"!((G(p0)) R (F(p1)))","11",3 +"!((G(p0)) R (F(p1)))","12",3 +"!((G(p0)) R (F(p1)))","13",3 "G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","1",2 "G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","2",3 "G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","3",2 "G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","4",2 "G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","6",2 "G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","7",2 +"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","8",2 +"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","9",2 +"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","10",2 +"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","11",2 +"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","12",2 +"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","13",2 "!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","1",4 "!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","2",4 "!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","3",4 "!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","4",4 "!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","6",4 "!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","7",4 +"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","8",4 +"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","9",4 +"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","10",4 +"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","11",4 +"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","12",4 +"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","13",4 "X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","1",4 "X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","2",5 "X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","3",5 "X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","4",5 "X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","6",5 "X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","7",5 +"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","8",5 +"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","9",5 +"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","10",5 +"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","11",5 +"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","12",5 +"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","13",5 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","1",7 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","2",7 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","3",7 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","4",7 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","6",7 "!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","7",7 +"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","8",7 +"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","9",7 +"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","10",7 +"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","11",7 +"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","12",7 +"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","13",7 "X((G(F(p0))) | (G(!(p0))))","1",4 "X((G(F(p0))) | (G(!(p0))))","2",4 "X((G(F(p0))) | (G(!(p0))))","3",3 "X((G(F(p0))) | (G(!(p0))))","4",3 "X((G(F(p0))) | (G(!(p0))))","6",3 "X((G(F(p0))) | (G(!(p0))))","7",3 +"X((G(F(p0))) | (G(!(p0))))","8",3 +"X((G(F(p0))) | (G(!(p0))))","9",3 +"X((G(F(p0))) | (G(!(p0))))","10",3 +"X((G(F(p0))) | (G(!(p0))))","11",3 +"X((G(F(p0))) | (G(!(p0))))","12",3 +"X((G(F(p0))) | (G(!(p0))))","13",3 "!(X((G(F(p0))) | (G(!(p0)))))","1",4 "!(X((G(F(p0))) | (G(!(p0)))))","2",4 "!(X((G(F(p0))) | (G(!(p0)))))","3",4 "!(X((G(F(p0))) | (G(!(p0)))))","4",4 "!(X((G(F(p0))) | (G(!(p0)))))","6",4 "!(X((G(F(p0))) | (G(!(p0)))))","7",4 +"!(X((G(F(p0))) | (G(!(p0)))))","8",4 +"!(X((G(F(p0))) | (G(!(p0)))))","9",4 +"!(X((G(F(p0))) | (G(!(p0)))))","10",4 +"!(X((G(F(p0))) | (G(!(p0)))))","11",4 +"!(X((G(F(p0))) | (G(!(p0)))))","12",4 +"!(X((G(F(p0))) | (G(!(p0)))))","13",4 "G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","1",4 "G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","2",4 "G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","3",4 "G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","4",4 "G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","6",4 "G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","7",4 +"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","8",4 +"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","9",4 +"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","10",4 +"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","11",4 +"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","12",4 +"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","13",4 "!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","1",4 "!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","2",4 "!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","3",4 "!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","4",4 "!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","6",4 "!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","7",4 +"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","8",4 +"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","9",4 +"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","10",4 +"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","11",4 +"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","12",4 +"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","13",4 "G((p0) | (F(p0)))","1",1 "G((p0) | (F(p0)))","2",1 "G((p0) | (F(p0)))","3",1 "G((p0) | (F(p0)))","4",1 "G((p0) | (F(p0)))","6",1 "G((p0) | (F(p0)))","7",1 +"G((p0) | (F(p0)))","8",1 +"G((p0) | (F(p0)))","9",1 +"G((p0) | (F(p0)))","10",1 +"G((p0) | (F(p0)))","11",1 +"G((p0) | (F(p0)))","12",1 +"G((p0) | (F(p0)))","13",1 "!(G((p0) | (F(p0))))","1",2 "!(G((p0) | (F(p0))))","2",2 "!(G((p0) | (F(p0))))","3",2 "!(G((p0) | (F(p0))))","4",2 "!(G((p0) | (F(p0))))","6",2 "!(G((p0) | (F(p0))))","7",2 +"!(G((p0) | (F(p0))))","8",2 +"!(G((p0) | (F(p0))))","9",2 +"!(G((p0) | (F(p0))))","10",2 +"!(G((p0) | (F(p0))))","11",2 +"!(G((p0) | (F(p0))))","12",2 +"!(G((p0) | (F(p0))))","13",2 EOF -diff expected extracted +diff expected output diff --git a/tests/core/satmin2.test b/tests/core/satmin2.test index f19cbf7db..e5f52a183 100755 --- a/tests/core/satmin2.test +++ b/tests/core/satmin2.test @@ -46,22 +46,36 @@ State: 2 [!0] 2 --END-- EOF - cat >expected < output diff output expected + # At some point, this formula was correctly minimized, but # the output was not marked as state-based. ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out grep 'properties:.*state-acc' out grep 'properties:.*deterministic' out +ltl2tgba -BD -x 'sat-minimize=3,incr=-1' "GF(a <-> XXb)" -H >out +grep 'properties:.*state-acc' out +grep 'properties:.*deterministic' out +ltl2tgba -BD -x 'sat-minimize=3,incr=0' "GF(a <-> XXb)" -H >out +grep 'properties:.*state-acc' out +grep 'properties:.*deterministic' out +ltl2tgba -BD -x 'sat-minimize=3,incr=1' "GF(a <-> XXb)" -H >out +grep 'properties:.*state-acc' out +grep 'properties:.*deterministic' out +ltl2tgba -BD -x 'sat-minimize=3,incr=2' "GF(a <-> XXb)" -H >out +grep 'properties:.*state-acc' out +grep 'properties:.*deterministic' out +ltl2tgba -BD -x 'sat-minimize=3,incr=50' "GF(a <-> XXb)" -H >out +grep 'properties:.*state-acc' out +grep 'properties:.*deterministic' out # DRA produced by ltl2dstar for GFp0 -> GFp1 @@ -96,18 +110,48 @@ State: 3 {1 3} 2 --END-- EOF - # Let's try to find a smaller transition-based Streett automaton We # easily really check the expected automaton, because different SAT # solver (even different versions of glucose) can return different # automata. $autfilt --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa --stats=%s >output test `cat output` = 1 +$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=-1' test.hoa \ + --stats=%s >output +test `cat output` = 1 +$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=0' test.hoa \ + --stats=%s >output +test `cat output` = 1 +$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=1' test.hoa \ + --stats=%s >output +test `cat output` = 1 +$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=2' test.hoa \ + --stats=%s >output +test `cat output` = 1 +$autfilt --sat-minimize='acc="Fin(0)|Inf(1)",incr=50' test.hoa \ + --stats=%s >output +test `cat output` = 1 # How about a state-based DSA? $autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)"' test.hoa \ --stats=%s > output test `cat output` = 3 +$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=-1' test.hoa \ + --stats=%s > output +test `cat output` = 3 +$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=0' test.hoa \ + --stats=%s > output +test `cat output` = 3 +$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=1' test.hoa \ + --stats=%s > output +test `cat output` = 3 +$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=2' test.hoa \ + --stats=%s > output +test `cat output` = 3 +$autfilt -S --sat-minimize='acc="Fin(0)|Inf(1)",incr=50' test.hoa \ + --stats=%s > output +test `cat output` = 3 + # How about a state-based DPA? $autfilt -S --sat-minimize='acc="parity max even 3",colored' -H test.hoa \ @@ -118,6 +162,47 @@ grep 'States: 3' output grep 'acc-name: parity max even 3' output grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output test 3 = `grep -c 'State: [012] {[012]}' output` +$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=-1' \ + -H test.hoa > output +cat output +grep 'properties:.*colored' output +grep 'States: 3' output +grep 'acc-name: parity max even 3' output +grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output +test 3 = `grep -c 'State: [012] {[012]}' output` +$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=0' \ + -H test.hoa > output +cat output +grep 'properties:.*colored' output +grep 'States: 3' output +grep 'acc-name: parity max even 3' output +grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output +test 3 = `grep -c 'State: [012] {[012]}' output` +$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=1' \ + -H test.hoa > output +cat output +grep 'properties:.*colored' output +grep 'States: 3' output +grep 'acc-name: parity max even 3' output +grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output +test 3 = `grep -c 'State: [012] {[012]}' output` +$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=2' \ + -H test.hoa > output +cat output +grep 'properties:.*colored' output +grep 'States: 3' output +grep 'acc-name: parity max even 3' output +grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output +test 3 = `grep -c 'State: [012] {[012]}' output` +$autfilt -S --sat-minimize='acc="parity max even 3",colored,incr=50' \ + -H test.hoa > output +cat output +grep 'properties:.*colored' output +grep 'States: 3' output +grep 'acc-name: parity max even 3' output +grep 'Acceptance: 3 Inf(2) | (Fin(1) & Inf(0))' output +test 3 = `grep -c 'State: [012] {[012]}' output` + # I get headaches whenever I think about this acceptance condition, so # it should be a good test case. @@ -136,9 +221,6 @@ State: 1 [!0] 1 {1} --END-- EOF - -$autfilt -H --sat-minimize special.hoa > output - cat >expected < output diff output expected +$autfilt -H --sat-minimize='incr=-1' special.hoa > output +diff output expected +$autfilt -H --sat-minimize='incr=0' special.hoa > output +diff output expected +$autfilt -H --sat-minimize='incr=1' special.hoa > output +diff output expected +$autfilt -H --sat-minimize='incr=2' special.hoa > output +diff output expected +$autfilt -H --sat-minimize='incr=50' special.hoa > output +diff output expected + cat >foo.hoa <out test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=-1' foo.hoa \ + --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=0' foo.hoa \ + --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=1' foo.hoa \ + --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=2' foo.hoa \ + --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Streett 1",max-states=2,incr=50' foo.hoa \ + --stats=%s >out +test "`cat out`" = 1 + $autfilt --sat-minimize='acc="Rabin 1",max-states=4' foo.hoa \ --stats=%s >out && exit 1 test -z "`cat out`" +$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=-1' foo.hoa \ + --stats=%s >out && exit 1 +test -z "`cat out`" +$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=0' foo.hoa \ + --stats=%s >out && exit 1 +test -z "`cat out`" +$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=1' foo.hoa \ + --stats=%s >out && exit 1 +test -z "`cat out`" +$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=2' foo.hoa \ + --stats=%s >out && exit 1 +test -z "`cat out`" +$autfilt --sat-minimize='acc="Rabin 1",max-states=4,incr=50' foo.hoa \ + --stats=%s >out && exit 1 +test -z "`cat out`" + $autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1' foo.hoa \ --stats=%s >out test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=-1' \ + foo.hoa --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=0' \ + foo.hoa --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=1' \ + foo.hoa --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=2' \ + foo.hoa --stats=%s >out +test "`cat out`" = 1 +$autfilt --sat-minimize='acc="Inf(0)&Fin(1)|Inf(2)",states=1,incr=50' \ + foo.hoa --stats=%s >out +test "`cat out`" = 1 diff --git a/tests/python/satmin.py b/tests/python/satmin.py index e2f801745..fc08006d0 100644 --- a/tests/python/satmin.py +++ b/tests/python/satmin.py @@ -25,20 +25,108 @@ assert aut.num_sets() == 1 assert aut.num_states() == 3 assert aut.is_deterministic() + min1 = spot.sat_minimize(aut, acc='Rabin 1') assert min1.num_sets() == 2 assert min1.num_states() == 2 +min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 +min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=-1) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 +min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=0) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 +min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=1) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 +min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=2) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 +min1 = spot.sat_minimize(aut, acc='Rabin 1', incr=True, param=50) +assert min1.num_sets() == 2 +assert min1.num_states() == 2 + min2 = spot.sat_minimize(aut, acc='Streett 2', dichotomy=True) assert min2.num_sets() == 4 assert min2.num_states() == 1 +min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 +min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=-1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 +min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=0) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 +min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=1) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 +min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=2) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 +min2 = spot.sat_minimize(aut, acc='Streett 2', incr=True, param=50) +assert min2.num_sets() == 4 +assert min2.num_states() == 1 + min3 = spot.sat_minimize(aut, acc='Rabin 2', state_based=True, max_states=5, dichotomy=True) assert min3.num_sets() == 4 assert min3.num_states() == 3 +min3 = spot.sat_minimize(aut, acc='Rabin 2', + state_based=True, max_states=5, incr=True) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 +min3 = spot.sat_minimize(aut, acc='Rabin 2', + state_based=True, max_states=5, incr=True, param=-1) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 +min3 = spot.sat_minimize(aut, acc='Rabin 2', + state_based=True, max_states=5, incr=True, param=0) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 +min3 = spot.sat_minimize(aut, acc='Rabin 2', + state_based=True, max_states=5, incr=True, param=1) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 +min3 = spot.sat_minimize(aut, acc='Rabin 2', + state_based=True, max_states=5, incr=True, param=2) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 +min3 = spot.sat_minimize(aut, acc='Rabin 2', + state_based=True, max_states=5, incr=True, param=50) +assert min3.num_sets() == 4 +assert min3.num_states() == 3 + min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, dichotomy=True) assert min4.num_sets() == 3 assert min4.num_states() == 2 +min4 = spot.sat_minimize(aut, acc='parity max odd 3', + colored=True, incr=True) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 +min4 = spot.sat_minimize(aut, acc='parity max odd 3', + colored=True, incr=True, param=-1) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 +min4 = spot.sat_minimize(aut, acc='parity max odd 3', + colored=True, incr=True, param=0) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 +min4 = spot.sat_minimize(aut, acc='parity max odd 3', + colored=True, incr=True, param=1) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 +min4 = spot.sat_minimize(aut, acc='parity max odd 3', + colored=True, incr=True, param=2) +assert min4.num_sets() == 3 +assert min4.num_states() == 2 +min4 = spot.sat_minimize(aut, acc='parity max odd 3', + colored=True, incr=True, param=50) +assert min4.num_sets() == 3 +assert min4.num_states() == 2