Exercise logic.propositional.proof.top
Description
Prove two propositions equivalent (with top-level decomposition)
Test report
| Tests | 282 |
| Errors | 24 |
| Warnings | 0 |
| Time | 1.014867s |
| Rating |  |
Suites
- Exercise logic.propositional.proof.top (tests: 282, errors: 24, warnings: 0, 1.014858s)
Errors
equivalence implemented: assertion failed parser/pretty-printer: "parse error for ~(p /\\ q) || s || ~r == ~(p /\\ q) || (r -> s): parsed as p == p, q == q, s || ~r == r -> s" parser/pretty-printer: "parse error for ~~(p -> q) /\\ ~(p /\\ q) == (p -> q) /\\ (~p || ~q): parsed as ~~(p -> q) == p -> q, ~(p /\\ q) == ~p || ~q" parser/pretty-printer: "parse error for p /\\ ~q == p /\\ ~q, q /\\ ~p == (p || q) /\\ ~p: parsed as p == p, q == q, q /\\ ~p == (p || q) /\\ ~p" parser/pretty-printer: "parse error for q /\\ ((p /\\ r) || ~p) == q /\\ ((~p /\\ ~r) || r): parsed as q == q, (p /\\ r) || ~p == (~p /\\ ~r) || r" parser/pretty-printer: "parse error for p || q == p || q: parsed as p == p, q == q" parser/pretty-printer: "parse error for ~p == ~p, q == ~~q, p -> s == ~s -> ~p: parsed as p == p, q == ~~q, p -> s == ~s -> ~p" parser/pretty-printer: "parse error for p /\\ q == ~~p /\\ ~~q: parsed as p == ~~p, q == ~~q" parser/pretty-printer: "parse error for p || q == p || q: parsed as p == p, q == q" parser/pretty-printer: "parse error for ~p || q == ~p || q || q: parsed as p == p, q == q || q" parser/pretty-printer: "parse error for p == p, q == q, ~p /\\ ~q == ~p /\\ ~q: parsed as p == p, q == q, p == p, q == q" parser/pretty-printer: "parse error for ~p || ~q || r == (p /\\ ~q) || ~p || r: parsed as ~p || ~q == (p /\\ ~q) || ~p, r == r" parser/pretty-printer: "parse error for ~p /\\ ~q == ~p /\\ ~q, (~p || q) /\\ p == p /\\ q: parsed as p == p, q == q, (~p || q) /\\ p == p /\\ q" parser/pretty-printer: "parse error for ~~p || ~~(q || r) == p || q || r: parsed as ~~p == p, ~~(q || r) == q || r" parser/pretty-printer: "parse error for ~p || ~(q || r) == ~p || (~q /\\ ~r): parsed as p == p, ~(q || r) == ~q /\\ ~r" parser/pretty-printer: "parse error for ~q == ~q, ~p == ~p || ~p: parsed as q == q, ~p == ~p || ~p" parser/pretty-printer: "parse error for p /\\ q == ~~p /\\ ~~q, ~p /\\ ~q == ~p /\\ ~q: parsed as p == ~~p, q == ~~q, p == p, q == q" parser/pretty-printer: "parse error for ((~p || q) /\\ (~p || r)) || (~(~p || q) /\\ ~(~p || r)) == ~p || (q /\\ r) || (p /\\ ~q /\\ ~r): parsed as (~p || q) /\\ (~p || r) == ~p || (q /\\ r), ~(~p || q) /\\ ~(~p || r) == p /\\ ~q /\\ ~r" parser/pretty-printer: "parse error for q == q, ~p == ~p: parsed as q == q, p == p" parser/pretty-printer: "parse error for p /\\ q == p /\\ q: parsed as p == p, q == q" parser/pretty-printer: "parse error for (~p /\\ ~r) || (q /\\ ~r) || q == (~p /\\ ~r) || q: parsed as p == p, r == r, (q /\\ ~r) || q == q" parser/pretty-printer: "parse error for q /\\ r == q /\\ r, (~r /\\ q /\\ p) || (~q /\\ p) == (p /\\ ~q) || (p /\\ ~r): parsed as q == q, r == r, (~r /\\ q /\\ p) || (~q /\\ p) == (p /\\ ~q) || (p /\\ ~r)" parser/pretty-printer: "parse error for (r /\\ p /\\ q) || (~q /\\ r) == (p /\\ r) || (~p /\\ ~q /\\ r), ~r == ~r, p == p, q == q: parsed as (r /\\ p /\\ q) || (~q /\\ r) == (p /\\ r) || (~p /\\ ~q /\\ r), r == r, p == p, q == q" parser/pretty-printer: "parse error for p /\\ (q || s) == p /\\ ((q /\\ ~s) || s): parsed as p == p, q || s == (q /\\ ~s) || s"Tests
Exercise logic.propositional.proof.top (tests: 282, errors: 24, warnings: 0, 1.014858s)
Examples (tests: 279, errors: 23, warnings: 0, 1.009958s)
start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~(p /\\ q) || s || ~r == ~(p /\\ q) || (r -> s): parsed as p == p, q == q, s || ~r == r -> s" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~~(p -> q) /\\ ~(p /\\ q) == (p -> q) /\\ (~p || ~q): parsed as ~~(p -> q) == p -> q, ~(p /\\ q) == ~p || ~q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p /\\ ~q == p /\\ ~q, q /\\ ~p == (p || q) /\\ ~p: parsed as p == p, q == q, q /\\ ~p == (p || q) /\\ ~p" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for q /\\ ((p /\\ r) || ~p) == q /\\ ((~p /\\ ~r) || r): parsed as q == q, (p /\\ r) || ~p == (~p /\\ ~r) || r" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p || q == p || q: parsed as p == p, q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~p == ~p, q == ~~q, p -> s == ~s -> ~p: parsed as p == p, q == ~~q, p -> s == ~s -> ~p" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p /\\ q == ~~p /\\ ~~q: parsed as p == ~~p, q == ~~q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p || q == p || q: parsed as p == p, q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~p || q == ~p || q || q: parsed as p == p, q == q || q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p == p, q == q, ~p /\\ ~q == ~p /\\ ~q: parsed as p == p, q == q, p == p, q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~p || ~q || r == (p /\\ ~q) || ~p || r: parsed as ~p || ~q == (p /\\ ~q) || ~p, r == r" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~p /\\ ~q == ~p /\\ ~q, (~p || q) /\\ p == p /\\ q: parsed as p == p, q == q, (~p || q) /\\ p == p /\\ q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~~p || ~~(q || r) == p || q || r: parsed as ~~p == p, ~~(q || r) == q || r" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~p || ~(q || r) == ~p || (~q /\\ ~r): parsed as p == p, ~(q || r) == ~q /\\ ~r" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ~q == ~q, ~p == ~p || ~p: parsed as q == q, ~p == ~p || ~p" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p /\\ q == ~~p /\\ ~~q, ~p /\\ ~q == ~p /\\ ~q: parsed as p == ~~p, q == ~~q, p == p, q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for ((~p || q) /\\ (~p || r)) || (~(~p || q) /\\ ~(~p || r)) == ~p || (q /\\ r) || (p /\\ ~q /\\ ~r): parsed as (~p || q) /\\ (~p || r) == ~p || (q /\\ r), ~(~p || q) /\\ ~(~p || r) == p /\\ ~q /\\ ~r" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for q == q, ~p == ~p: parsed as q == q, p == p" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p /\\ q == p /\\ q: parsed as p == p, q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for (~p /\\ ~r) || (q /\\ ~r) || q == (~p /\\ ~r) || q: parsed as p == p, r == r, (q /\\ ~r) || q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for q /\\ r == q /\\ r, (~r /\\ q /\\ p) || (~q /\\ p) == (p /\\ ~q) || (p /\\ ~r): parsed as q == q, r == r, (~r /\\ q /\\ p) || (~q /\\ p) == (p /\\ ~q) || (p /\\ ~r)" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for (r /\\ p /\\ q) || (~q /\\ r) == (p /\\ r) || (~p /\\ ~q /\\ r), ~r == ~r, p == p, q == q: parsed as (r /\\ p /\\ q) || (~q /\\ r) == (p /\\ r) || (~p /\\ ~q /\\ r), r == r, p == p, q == q" equivalences no similar steps self similarity parameters start term is suitable start term is not ready final term is suitable final term is ready parser/pretty-printer: "parse error for p /\\ (q || s) == p /\\ ((q /\\ ~s) || s): parsed as p == p, q || s == (q /\\ ~s) || s" equivalences no similar steps self similarity parameters exercise terms defined equivalence implemented: assertion failed similarity implemented