Permalink
Browse files

incidence_geometry and ordered_incidence_geometry hierarchies: refere…

…nce in p9 and output files changed
  • Loading branch information...
torstenhahmann@gmail.com
torstenhahmann@gmail.com committed Jun 10, 2013
1 parent 9bdc45c commit 5df7f810910e59df1c9c33eaf4f475ab0ee66abb
Showing with 233 additions and 233 deletions.
  1. +3 −3 ontologies/incidence_geometry/consistency/output/ig_2d_nontrivial.m4.out
  2. +6 −6 ontologies/incidence_geometry/consistency/output/ig_nontrivial.m4.out
  3. +3 −3 ontologies/incidence_geometry/theorems/output/ig_2d_theorems.m4.out
  4. +4 −4 ontologies/incidence_geometry/theorems/output/ig_2d_theorems_1.p9.out
  5. +4 −4 ontologies/incidence_geometry/theorems/output/ig_2d_theorems_2.p9.out
  6. +6 −6 ontologies/incidence_geometry/theorems/output/ig_theorems.m4.out
  7. +7 −7 ontologies/incidence_geometry/theorems/output/ig_theorems_1.p9.out
  8. +7 −7 ontologies/incidence_geometry/theorems/output/ig_theorems_2.p9.out
  9. +6 −6 ontologies/ordered_incidence_geometry/consistency/output/woig_2d.m4.out
  10. +7 −7 ontologies/ordered_incidence_geometry/consistency/output/woig_2d_nontrivial.m4.out
  11. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems.m4.out
  12. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems_1.m4.out
  13. +4 −4 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems_2.p9.out
  14. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems_3.m4.out
  15. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems_4.m4.out
  16. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems_5.m4.out
  17. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_2d_theorems_6.m4.out
  18. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems.m4.out
  19. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems_1.m4.out
  20. +4 −4 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems_2.p9.out
  21. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems_3.m4.out
  22. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems_4.m4.out
  23. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems_5.m4.out
  24. +3 −3 ontologies/ordered_incidence_geometry/theorems/output/b_3d_theorems_6.m4.out
  25. +7 −7 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems.m4.out
  26. +8 −8 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_1.p9.out
  27. +8 −8 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_2.p9.out
  28. +8 −8 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_3.p9.out
  29. +7 −7 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_4.m4.out
  30. +8 −8 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_5.p9.out
  31. +7 −7 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_6.m4.out
  32. +7 −7 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_7.m4.out
  33. +7 −7 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_8.m4.out
  34. +7 −7 ontologies/ordered_incidence_geometry/theorems/output/woig_2d_theorems_9.m4.out
  35. +8 −8 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems.m4.out
  36. +9 −9 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems_1.p9.out
  37. +9 −9 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems_2.p9.out
  38. +9 −9 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems_3.p9.out
  39. +9 −9 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems_4.p9.out
  40. +9 −9 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems_5.p9.out
  41. +9 −9 ontologies/ordered_incidence_geometry/theorems/output/woig_theorems_6.p9.out
@@ -2,19 +2,19 @@
Mace4 (64) version 2009-11A, November 2009.
Process 25655 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 21:27:02 2012
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig//consistency/p9/ig_2d_nontrivial.p9 ig/p9/ig_2d.p9".
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig/consistency/input/ig_2d_nontrivial.p9 ig/input/ig_2d.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig//consistency/p9/ig_2d_nontrivial.p9
% Reading from file ig/consistency/input/ig_2d_nontrivial.p9
formulas(sos).
(exists x exists y exists z (L(x) & L(y) & on(z,x) & on(z,y))).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
@@ -2,19 +2,19 @@
Mace4 (64) version 2009-11A, November 2009.
Process 3472 was started by torsten on scotus.mie.utoronto.ca,
Sun Nov 4 10:01:44 2012
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig//consistency/p9/ig_nontrivial.p9 ig/p9/ig.p9 ig/p9/ig_2d_lin.p9 ig/p9/ig_2d_slin.p9 ig/p9/ig_2d.p9".
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig/consistency/input/ig_nontrivial.p9 ig/input/ig.p9 ig/input/ig_2d_lin.p9 ig/input/ig_2d_slin.p9 ig/input/ig_2d.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig//consistency/p9/ig_nontrivial.p9
% Reading from file ig/consistency/input/ig_nontrivial.p9
formulas(sos).
(exists x Pl(x)).
end_of_list.
% Reading from file ig/p9/ig.p9
% Reading from file ig/input/ig.p9
formulas(sos).
@@ -27,21 +27,21 @@ formulas(sos).
(all p all q all l all x (Pt(p) & Pt(q) & p != q & L(l) & on(p,l) & on(q,l) & Pl(x) & on(p,x) & on(q,x) -> (all r (Pt(r) & on(r,l) -> on(r,x))))).
end_of_list.
% Reading from file ig/p9/ig_2d_lin.p9
% Reading from file ig/input/ig_2d_lin.p9
formulas(sos).
(all x all y (Pt(x) & Pt(y) & x != y -> (exists z (L(z) & on(x,z) & on(y,z))))).
end_of_list.
% Reading from file ig/p9/ig_2d_slin.p9
% Reading from file ig/input/ig_2d_slin.p9
formulas(sos).
(all l all m all x all y (x != y & L(l) & L(m) & on(x,l) & on(y,l) & on(x,m) & on(y,m) -> l = m)).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
@@ -2,20 +2,20 @@
Mace4 (64) version 2009-11A, November 2009.
Process 25876 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:08:05 2012
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig//theorems/p9/ig_2d_theorems.p9 ig/p9/ig_2d.p9".
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig/theorems/input/ig_2d_theorems.p9 ig/input/ig_2d.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig//theorems/p9/ig_2d_theorems.p9
% Reading from file ig/theorems/input/ig_2d_theorems.p9
formulas(sos).
(all x (Pt(x) -> -L(x))).
(all x (L(x) -> -Pt(x))).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
@@ -2,27 +2,27 @@
Prover9 (64) version 2009-11A, November 2009.
Process 25883 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:08:09 2012
The command was "prover9 -t 600 -f ig/p9/ig_2d.p9 ig//theorems/p9/options.txt ig//theorems/p9/ig_2d_theorems_1.p9".
The command was "prover9 -t 600 -f ig/input/ig_2d.p9 ig/theorems/input/options.txt ig/theorems/input/ig_2d_theorems_1.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
(all x all y (on(x,y) -> Pt(x) & -Pt(y))).
(all x (L(x) -> (exists y exists z (on(y,x) & on(z,x) & y != z)))).
end_of_list.
% Reading from file ig//theorems/p9/options.txt
% Reading from file ig/theorems/input/options.txt
clear(auto_denials).
clear(print_initial_clauses).
clear(print_kept).
clear(print_given).
% Reading from file ig//theorems/p9/ig_2d_theorems_1.p9
% Reading from file ig/theorems/input/ig_2d_theorems_1.p9
formulas(goals).
@@ -2,27 +2,27 @@
Prover9 (64) version 2009-11A, November 2009.
Process 25887 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:08:13 2012
The command was "prover9 -t 600 -f ig/p9/ig_2d.p9 ig//theorems/p9/options.txt ig//theorems/p9/ig_2d_theorems_2.p9".
The command was "prover9 -t 600 -f ig/input/ig_2d.p9 ig/theorems/input/options.txt ig/theorems/input/ig_2d_theorems_2.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
(all x all y (on(x,y) -> Pt(x) & -Pt(y))).
(all x (L(x) -> (exists y exists z (on(y,x) & on(z,x) & y != z)))).
end_of_list.
% Reading from file ig//theorems/p9/options.txt
% Reading from file ig/theorems/input/options.txt
clear(auto_denials).
clear(print_initial_clauses).
clear(print_kept).
clear(print_given).
% Reading from file ig//theorems/p9/ig_2d_theorems_2.p9
% Reading from file ig/theorems/input/ig_2d_theorems_2.p9
formulas(goals).
@@ -2,20 +2,20 @@
Mace4 (64) version 2009-11A, November 2009.
Process 25838 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:07:36 2012
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig//theorems/p9/ig_theorems.p9 ig/p9/ig.p9 ig/p9/ig_2d_lin.p9 ig/p9/ig_2d_slin.p9 ig/p9/ig_2d.p9".
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f ig/theorems/input/ig_theorems.p9 ig/input/ig.p9 ig/input/ig_2d_lin.p9 ig/input/ig_2d_slin.p9 ig/input/ig_2d.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig//theorems/p9/ig_theorems.p9
% Reading from file ig/theorems/input/ig_theorems.p9
formulas(sos).
(all x (Pl(x) -> -L(x))).
(all x (Pl(x) -> -Pt(x))).
end_of_list.
% Reading from file ig/p9/ig.p9
% Reading from file ig/input/ig.p9
formulas(sos).
@@ -28,21 +28,21 @@ formulas(sos).
(all p all q all l all x (Pt(p) & Pt(q) & p != q & L(l) & on(p,l) & on(q,l) & Pl(x) & on(p,x) & on(q,x) -> (all r (Pt(r) & on(r,l) -> on(r,x))))).
end_of_list.
% Reading from file ig/p9/ig_2d_lin.p9
% Reading from file ig/input/ig_2d_lin.p9
formulas(sos).
(all x all y (Pt(x) & Pt(y) & x != y -> (exists z (L(z) & on(x,z) & on(y,z))))).
end_of_list.
% Reading from file ig/p9/ig_2d_slin.p9
% Reading from file ig/input/ig_2d_slin.p9
formulas(sos).
(all l all m all x all y (x != y & L(l) & L(m) & on(x,l) & on(y,l) & on(x,m) & on(y,m) -> l = m)).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
@@ -2,12 +2,12 @@
Prover9 (64) version 2009-11A, November 2009.
Process 25850 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:07:41 2012
The command was "prover9 -t 600 -f ig/p9/ig.p9 ig/p9/ig_2d_lin.p9 ig/p9/ig_2d_slin.p9 ig/p9/ig_2d.p9 ig//theorems/p9/options.txt ig//theorems/p9/ig_theorems_1.p9".
The command was "prover9 -t 600 -f ig/input/ig.p9 ig/input/ig_2d_lin.p9 ig/input/ig_2d_slin.p9 ig/input/ig_2d.p9 ig/theorems/input/options.txt ig/theorems/input/ig_theorems_1.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig/p9/ig.p9
% Reading from file ig/input/ig.p9
formulas(sos).
@@ -20,36 +20,36 @@ formulas(sos).
(all p all q all l all x (Pt(p) & Pt(q) & p != q & L(l) & on(p,l) & on(q,l) & Pl(x) & on(p,x) & on(q,x) -> (all r (Pt(r) & on(r,l) -> on(r,x))))).
end_of_list.
% Reading from file ig/p9/ig_2d_lin.p9
% Reading from file ig/input/ig_2d_lin.p9
formulas(sos).
(all x all y (Pt(x) & Pt(y) & x != y -> (exists z (L(z) & on(x,z) & on(y,z))))).
end_of_list.
% Reading from file ig/p9/ig_2d_slin.p9
% Reading from file ig/input/ig_2d_slin.p9
formulas(sos).
(all l all m all x all y (x != y & L(l) & L(m) & on(x,l) & on(y,l) & on(x,m) & on(y,m) -> l = m)).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
(all x all y (on(x,y) -> Pt(x) & -Pt(y))).
(all x (L(x) -> (exists y exists z (on(y,x) & on(z,x) & y != z)))).
end_of_list.
% Reading from file ig//theorems/p9/options.txt
% Reading from file ig/theorems/input/options.txt
clear(auto_denials).
clear(print_initial_clauses).
clear(print_kept).
clear(print_given).
% Reading from file ig//theorems/p9/ig_theorems_1.p9
% Reading from file ig/theorems/input/ig_theorems_1.p9
formulas(goals).
@@ -2,12 +2,12 @@
Prover9 (64) version 2009-11A, November 2009.
Process 25855 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:07:47 2012
The command was "prover9 -t 600 -f ig/p9/ig.p9 ig/p9/ig_2d_lin.p9 ig/p9/ig_2d_slin.p9 ig/p9/ig_2d.p9 ig//theorems/p9/options.txt ig//theorems/p9/ig_theorems_2.p9".
The command was "prover9 -t 600 -f ig/input/ig.p9 ig/input/ig_2d_lin.p9 ig/input/ig_2d_slin.p9 ig/input/ig_2d.p9 ig/theorems/input/options.txt ig/theorems/input/ig_theorems_2.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file ig/p9/ig.p9
% Reading from file ig/input/ig.p9
formulas(sos).
@@ -20,36 +20,36 @@ formulas(sos).
(all p all q all l all x (Pt(p) & Pt(q) & p != q & L(l) & on(p,l) & on(q,l) & Pl(x) & on(p,x) & on(q,x) -> (all r (Pt(r) & on(r,l) -> on(r,x))))).
end_of_list.
% Reading from file ig/p9/ig_2d_lin.p9
% Reading from file ig/input/ig_2d_lin.p9
formulas(sos).
(all x all y (Pt(x) & Pt(y) & x != y -> (exists z (L(z) & on(x,z) & on(y,z))))).
end_of_list.
% Reading from file ig/p9/ig_2d_slin.p9
% Reading from file ig/input/ig_2d_slin.p9
formulas(sos).
(all l all m all x all y (x != y & L(l) & L(m) & on(x,l) & on(y,l) & on(x,m) & on(y,m) -> l = m)).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
(all x all y (on(x,y) -> Pt(x) & -Pt(y))).
(all x (L(x) -> (exists y exists z (on(y,x) & on(z,x) & y != z)))).
end_of_list.
% Reading from file ig//theorems/p9/options.txt
% Reading from file ig/theorems/input/options.txt
clear(auto_denials).
clear(print_initial_clauses).
clear(print_kept).
clear(print_given).
% Reading from file ig//theorems/p9/ig_theorems_2.p9
% Reading from file ig/theorems/input/ig_theorems_2.p9
formulas(goals).
@@ -2,18 +2,18 @@
Mace4 (64) version 2009-11A, November 2009.
Process 26121 was started by torsten on scotus.mie.utoronto.ca,
Wed Oct 24 22:34:59 2012
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f oig/p9/woig_2d.p9 oig/p9/b_2d.p9 ig/p9/ig_2d_lin.p9 ig/p9/ig_2d_slin.p9 ig/p9/ig_2d.p9".
The command was "mace4 -c -t 600 -s 60 -n 2 -N 20 -f oig/input/woig_2d.p9 oig/input/b_2d.p9 ig/input/ig_2d_lin.p9 ig/input/ig_2d_slin.p9 ig/input/ig_2d.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file oig/p9/woig_2d.p9
% Reading from file oig/input/woig_2d.p9
formulas(sos).
end_of_list.
% Reading from file oig/p9/b_2d.p9
% Reading from file oig/input/b_2d.p9
formulas(sos).
@@ -24,21 +24,21 @@ formulas(sos).
(all a all b all c all p all l (on(a,l) & on(b,l) & on(c,l) & on(p,l) & p != a & p != b & p != c & B(a,p,b) -> B(b,p,c) & -B(a,p,c) | B(a,p,c) & -B(b,p,c))).
end_of_list.
% Reading from file ig/p9/ig_2d_lin.p9
% Reading from file ig/input/ig_2d_lin.p9
formulas(sos).
(all x all y (Pt(x) & Pt(y) & x != y -> (exists z (L(z) & on(x,z) & on(y,z))))).
end_of_list.
% Reading from file ig/p9/ig_2d_slin.p9
% Reading from file ig/input/ig_2d_slin.p9
formulas(sos).
(all l all m all x all y (x != y & L(l) & L(m) & on(x,l) & on(y,l) & on(x,m) & on(y,m) -> l = m)).
end_of_list.
% Reading from file ig/p9/ig_2d.p9
% Reading from file ig/input/ig_2d.p9
formulas(sos).
Oops, something went wrong.

0 comments on commit 5df7f81

Please sign in to comment.