Skip to content
Permalink
Browse files

Verification for the kernel theory

Verification for the kernel theory (prover9 proof)
  • Loading branch information...
jessiezj-li committed Aug 13, 2019
1 parent fff346f commit d6be54de87ab5d085be2d90cc57cc7a6c4c0c0de
Showing with 5,198 additions and 0 deletions.
  1. +90 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_1.1.proof
  2. +101 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_1.2.proof
  3. +38 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_1.3.proof
  4. +38 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_1.4.proof
  5. +88 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_1.5.proof
  6. +47 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_1.6.proof
  7. +83 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_2.1.proof
  8. +47 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_2.2.proof
  9. +90 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_3.1.proof
  10. +82 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_3.2.proof
  11. +38 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_3.3.proof
  12. +38 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_3.4.proof
  13. +76 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_4.1.proof
  14. +73 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_4.2.proof
  15. +78 −0 ontologies/vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_4.3.proof
  16. +45 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_2.1.proof
  17. +26 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_2.2.proof
  18. +32 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_2.3.proof
  19. +54 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_2.4.proof
  20. +63 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_2.5.proof
  21. +45 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_4.1.proof
  22. +26 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_4.2.proof
  23. +32 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_4.3.proof
  24. +53 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_4.4.proof
  25. +54 −0 .../vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakBi_4.5.proof
  26. +45 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.1.proof
  27. +26 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.2.proof
  28. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.3.proof
  29. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.4.proof
  30. +32 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.5.proof
  31. +53 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.6.proof
  32. +54 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.7.proof
  33. +54 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_1.8.proof
  34. +45 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.1.proof
  35. +28 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.2.proof
  36. +32 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.3.proof
  37. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.4.proof
  38. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.5.proof
  39. +53 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.6.proof
  40. +53 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.7.proof
  41. +54 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_2.8.proof
  42. +45 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.1.proof
  43. +26 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.2.proof
  44. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.3.proof
  45. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.4.proof
  46. +32 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.5.proof
  47. +54 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.6.proof
  48. +56 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.7.proof
  49. +57 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_3.8.proof
  50. +45 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.1.proof
  51. +26 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.2.proof
  52. +32 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.3.proof
  53. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.4.proof
  54. +38 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.5.proof
  55. +53 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.6.proof
  56. +54 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.7.proof
  57. +54 −0 ...vision_cardworld/kernel_verification/depiction_to_incidence/Depiction_Incidence_WeakTri_4.8.proof
  58. +56 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_1.proof
  59. +47 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_2.proof
  60. +46 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_3.proof
  61. +31 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakBi_1.proof
  62. +28 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakBi_2.proof
  63. +32 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakBi_3.proof
  64. +35 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakBi_4.proof
  65. +35 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakBi_5.proof
  66. +31 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_1.proof
  67. +28 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_2.proof
  68. +32 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_3.proof
  69. +32 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_4.proof
  70. +32 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_5.proof
  71. +35 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_6.proof
  72. +35 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_7.proof
  73. +35 −0 ontologies/vision_cardworld/kernel_verification/image_to_incidence/Image_Incidence_WeakTri_8.proof
  74. +48 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_1.proof
  75. +69 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_2.proof
  76. +75 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_1.1.proof
  77. +46 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_1.2.proof
  78. +56 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_1.3.proof
  79. +50 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_1.4.proof
  80. +78 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_2.1.proof
  81. +39 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_2.2.proof
  82. +50 −0 ...n_cardworld/kernel_verification/incidence_to_depiction/Incidence_Depiction_Intermediate_2.3.proof
  83. +56 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_image/Incidence_Image_1.proof
  84. +48 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_image/Incidence_Image_2.proof
  85. +50 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_image/Incidence_Image_3.proof
  86. +48 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_scene/Incidence_Scene_1.proof
  87. +51 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_scene/Incidence_Scene_2.proof
  88. +64 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_scene/Incidence_Scene_3.proof
  89. +37 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_scene/Incidence_Scene_4.1.proof
  90. +37 −0 ontologies/vision_cardworld/kernel_verification/incidence_to_scene/Incidence_Scene_4.2.proof
  91. +56 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_1.proof
  92. +47 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_2.proof
  93. +46 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_3.proof
  94. +41 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.1.proof
  95. +46 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.2.proof
  96. +50 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.3.proof
  97. +60 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.4.proof
  98. +52 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.5.proof
  99. +51 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.6.proof
  100. +52 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_4.7.proof
  101. +31 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakBi_1.proof
  102. +28 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakBi_2.proof
  103. +32 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakBi_3.proof
  104. +35 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakBi_4.proof
  105. +35 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakBi_5.proof
  106. +31 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_1.proof
  107. +28 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_2.proof
  108. +32 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_3.proof
  109. +32 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_4.proof
  110. +32 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_5.proof
  111. +35 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_6.proof
  112. +35 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_7.proof
  113. +35 −0 ontologies/vision_cardworld/kernel_verification/scene_to_incidence/Scene_Incidence_WeakTri_8.proof
@@ -0,0 +1,90 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 23859 was started by zhuojun on Zhuojun-Li.local,
Fri Jul 26 01:01:54 2019
The command was "/Users/zhuojun/Desktop/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.02 (+ 0.01) seconds.
% Length of proof is 70.
% Level of proof is 11.
% Maximum clause weight is 23.
% Given clauses 88.

1 (all x (image_object(x) <-> region(x) | line(x) | pixel(x))) # label(non_clause). [assumption].
2 (all x (scene_object(x) <-> surface(x) | edge(x) | point(x))) # label(non_clause). [assumption].
6 (all x -(point(x) & edge(x))) # label(non_clause). [assumption].
9 (all x (scene_object(x) <-> -image_object(x))) # label(non_clause). [assumption].
10 (all x all y (part(x,y) -> scene_object(x) & scene_object(y))) # label(non_clause). [assumption].
12 (all x all y (part(x,y) -> part(y,x))) # label(non_clause). [assumption].
16 (all x all y (in(x,y) -> image_object(x) & image_object(y))) # label(non_clause). [assumption].
22 (all i all s (pixel(i) & depicts(i,s) -> -edge(s) & -surface(s))) # label(non_clause). [assumption].
26 (all x all y (def_in(x,y) <-> pixel(x) & edge(y) & (exists z (point(z) & depicts(x,z) & part(z,y))))) # label(non_clause). [assumption].
27 (all x (g_line(x) <-> point(x))) # label(non_clause). [assumption].
28 (all x (plane(x) <-> edge(x))) # label(non_clause). [assumption].
29 (all x (g_point(x) <-> pixel(x))) # label(non_clause). [assumption].
30 (all x all y (g_in(x,y) <-> in(x,y) | in(y,x) | part(x,y) | part(y,x) | depicts(x,y) & image_object(x) & scene_object(y) | def_in(x,y) & pixel(x) & edge(y) | x = y)) # label(non_clause). [assumption].
31 (all x all y all z (plane(x) & g_line(y) & g_point(z) & g_in(z,y) & g_in(y,x) -> g_in(z,x))) # label(non_clause) # label(goal). [goal].
35 image_object(x) | -pixel(x). [clausify(1)].
36 -scene_object(x) | -image_object(x). [clausify(9)].
38 -in(x,y) | image_object(x). [clausify(16)].
39 -in(x,y) | image_object(y). [clausify(16)].
42 -g_in(x,y) | in(x,y) | in(y,x) | part(x,y) | part(y,x) | image_object(x) | pixel(x) | y = x. [clausify(30)].
77 def_in(x,y) | -pixel(x) | -edge(y) | -point(z) | -depicts(x,z) | -part(z,y). [clausify(26)].
85 g_in(x,y) | -def_in(x,y) | -pixel(x) | -edge(y). [clausify(30)].
88 -g_line(x) | point(x). [clausify(27)].
89 g_line(c2). [deny(31)].
91 -plane(x) | edge(x). [clausify(28)].
92 plane(c1). [deny(31)].
94 -g_point(x) | pixel(x). [clausify(29)].
95 g_point(c3). [deny(31)].
99 scene_object(x) | -point(x). [clausify(2)].
100 -point(x) | -edge(x). [clausify(6)].
103 -part(x,y) | scene_object(x). [clausify(10)].
104 -part(x,y) | scene_object(y). [clausify(10)].
106 -part(x,y) | part(y,x). [clausify(12)].
112 -pixel(x) | -depicts(x,y) | -edge(y). [clausify(22)].
115 -g_in(x,y) | in(x,y) | in(y,x) | part(x,y) | part(y,x) | depicts(x,y) | edge(y) | y = x. [clausify(30)].
122 g_in(x,y) | y != x. [clausify(30)].
123 g_in(c3,c2). [deny(31)].
124 g_in(c2,c1). [deny(31)].
125 -g_in(c3,c1). [deny(31)].
126 -scene_object(x) | -pixel(x). [resolve(36,b,35,a)].
127 -in(x,y) | -scene_object(x). [resolve(38,b,36,b)].
128 -in(x,y) | -scene_object(y). [resolve(39,b,36,b)].
130 -g_in(x,y) | in(x,y) | in(y,x) | part(x,y) | part(y,x) | pixel(x) | y = x | -scene_object(x). [resolve(42,f,36,b)].
158 g_in(x,y) | -pixel(x) | -edge(y) | -pixel(x) | -edge(y) | -point(z) | -depicts(x,z) | -part(z,y). [resolve(85,b,77,a)].
159 g_in(x,y) | -pixel(x) | -edge(y) | -point(z) | -depicts(x,z) | -part(z,y). [copy(158),merge(d),merge(e)].
163 point(c2). [resolve(89,a,88,a)].
164 edge(c1). [resolve(92,a,91,a)].
165 pixel(c3). [resolve(95,a,94,a)].
182 in(c3,c2) | in(c2,c3) | part(c3,c2) | part(c2,c3) | depicts(c3,c2) | edge(c2) | c3 = c2. [resolve(123,a,115,a),flip(g)].
185 c3 != c1. [ur(122,a,125,a),flip(a)].
190 in(c2,c1) | in(c1,c2) | part(c2,c1) | part(c1,c2) | pixel(c2) | c2 = c1 | -scene_object(c2). [resolve(130,a,124,a),flip(f)].
210 -edge(c2). [resolve(163,a,100,a)].
211 scene_object(c2). [resolve(163,a,99,b)].
214 in(c3,c2) | in(c2,c3) | part(c3,c2) | part(c2,c3) | depicts(c3,c2) | c3 = c2. [back_unit_del(182),unit_del(f,210)].
218 in(c2,c1) | in(c1,c2) | part(c2,c1) | part(c1,c2) | pixel(c2) | c2 = c1. [back_unit_del(190),unit_del(g,211)].
222 -scene_object(c3). [ur(126,b,165,a)].
223 -depicts(c3,c1). [ur(112,a,165,a,c,164,a)].
224 -pixel(c2). [resolve(211,a,126,a)].
226 -in(x,c2). [ur(128,b,211,a)].
227 -in(c2,x). [ur(127,b,211,a)].
228 part(c2,c1) | part(c1,c2) | c2 = c1. [back_unit_del(218),unit_del(a,227),unit_del(b,226),unit_del(e,224)].
229 part(c3,c2) | part(c2,c3) | depicts(c3,c2) | c3 = c2. [back_unit_del(214),unit_del(a,226),unit_del(b,227)].
239 part(c1,c2) | c2 = c1. [resolve(228,a,106,a),merge(c)].
241 c2 = c1 | part(c2,c1). [resolve(239,a,106,a)].
243 -part(x,c3). [ur(104,b,222,a)].
244 -part(c3,x). [ur(103,b,222,a)].
248 depicts(c3,c2) | c3 = c2. [back_unit_del(229),unit_del(a,244),unit_del(b,243)].
249 c2 = c1 | g_in(x,c1) | -pixel(x) | -depicts(x,c2). [resolve(241,b,159,f),unit_del(d,164),unit_del(e,163)].
254 c2 = c1 | c3 = c2. [resolve(249,d,248,a),unit_del(b,125),unit_del(c,165)].
256 c2 = c1. [para(254(b,1),125(a,1)),unit_del(b,124)].
257 $F. [back_rewrite(248),rewrite([256(2),256(5)]),unit_del(a,223),unit_del(b,185)].

============================== end of proof ==========================
@@ -0,0 +1,101 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 23254 was started by zhuojun on Zhuojun-Li.local,
Thu Jul 25 23:49:30 2019
The command was "/Users/zhuojun/Desktop/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 40.56 (+ 0.95) seconds.
% Length of proof is 81.
% Level of proof is 16.
% Maximum clause weight is 30.
% Given clauses 17117.

1 (all x (image_object(x) <-> region(x) | line(x) | pixel(x))) # label(non_clause). [assumption].
2 (all x (scene_object(x) <-> surface(x) | edge(x) | point(x))) # label(non_clause). [assumption].
9 (all x (scene_object(x) <-> -image_object(x))) # label(non_clause). [assumption].
10 (all x all y (part(x,y) -> scene_object(x) & scene_object(y))) # label(non_clause). [assumption].
12 (all x all y (part(x,y) -> part(y,x))) # label(non_clause). [assumption].
16 (all x (edge(x) -> (exists s (surface(s) & part(x,s))))) # label(non_clause). [assumption].
23 (all x all y (in(x,y) -> image_object(x) & image_object(y))) # label(non_clause). [assumption].
25 (all i all s (depicts(i,s) -> image_object(i) & scene_object(s))) # label(non_clause). [assumption].
29 (all i all s (pixel(i) & depicts(i,s) -> -edge(s) & -surface(s))) # label(non_clause). [assumption].
33 (all x all y (def_in(x,y) <-> pixel(x) & edge(y) & (exists z (point(z) & depicts(x,z) & part(z,y))))) # label(non_clause). [assumption].
34 (all x (g_line(x) <-> point(x))) # label(non_clause). [assumption].
35 (all x (plane(x) <-> edge(x))) # label(non_clause). [assumption].
36 (all x (g_point(x) <-> pixel(x))) # label(non_clause). [assumption].
37 (all x all y (g_in(x,y) <-> in(x,y) | in(y,x) | part(x,y) | part(y,x) | depicts(x,y) | depicts(y,x) | def_in(x,y) | def_in(y,x) | x = y)) # label(non_clause). [assumption].
38 (all p all q (plane(q) & g_in(p,q) & g_point(p) -> (exists l (g_line(l) & g_in(p,l) & g_in(l,q))))) # label(non_clause) # label(goal). [goal].
42 image_object(x) | -pixel(x). [clausify(1)].
43 -scene_object(x) | -image_object(x). [clausify(9)].
45 -in(x,y) | image_object(x). [clausify(23)].
46 -in(x,y) | image_object(y). [clausify(23)].
50 scene_object(x) | -edge(x). [clausify(2)].
52 -part(x,y) | scene_object(x). [clausify(10)].
53 -part(x,y) | scene_object(y). [clausify(10)].
56 -depicts(x,y) | scene_object(y). [clausify(25)].
59 -scene_object(x) | -pixel(x). [resolve(43,b,42,a)].
61 -in(x,y) | -scene_object(x). [resolve(45,b,43,b)].
62 -in(x,y) | -scene_object(y). [resolve(46,b,43,b)].
67 -pixel(x) | -depicts(x,y) | -edge(y). [clausify(29)].
72 -def_in(x,y) | pixel(x). [clausify(33)].
74 -g_point(x) | pixel(x). [clausify(36)].
80 -pixel(x) | -edge(x). [resolve(59,a,50,a)].
82 -pixel(x) | -part(x,y). [resolve(59,a,52,b)].
83 -pixel(x) | -part(y,x). [resolve(59,a,53,b)].
84 -pixel(x) | -depicts(y,x). [resolve(59,a,56,b)].
89 g_line(x) | -point(x). [clausify(34)].
91 -g_line(x) | -g_in(c1,x) | -g_in(x,c2). [deny(38)].
93 -plane(x) | edge(x). [clausify(35)].
94 plane(c2). [deny(38)].
96 g_point(c1). [deny(38)].
98 -g_point(x) | -depicts(x,y) | -edge(y). [resolve(74,b,67,a)].
111 -part(x,y) | -g_point(x). [resolve(82,a,74,b)].
112 -part(x,y) | -g_point(y). [resolve(83,a,74,b)].
113 -depicts(x,y) | -g_point(y). [resolve(84,a,74,b)].
120 -part(x,y) | part(y,x). [clausify(12)].
125 -edge(x) | part(x,f1(x)). [clausify(16)].
154 -def_in(x,y) | point(f10(x,y)). [clausify(33)].
155 -def_in(x,y) | depicts(x,f10(x,y)). [clausify(33)].
156 -def_in(x,y) | part(f10(x,y),y). [clausify(33)].
157 -g_in(x,y) | in(x,y) | in(y,x) | part(x,y) | part(y,x) | depicts(x,y) | depicts(y,x) | def_in(x,y) | def_in(y,x) | y = x. [clausify(37)].
160 g_in(x,y) | -part(x,y). [clausify(37)].
162 g_in(x,y) | -depicts(x,y). [clausify(37)].
167 g_in(c1,c2). [deny(38)].
184 -in(x,y) | -edge(x). [resolve(61,b,50,a)].
190 -in(x,y) | -edge(y). [resolve(62,b,50,a)].
221 -edge(x) | -def_in(x,y). [resolve(80,a,72,b)].
230 -g_in(c1,x) | -g_in(x,c2) | -point(x). [resolve(91,a,89,a)].
231 edge(c2). [resolve(94,a,93,a)].
234 -depicts(c1,x) | -edge(x). [resolve(98,a,96,a)].
241 -part(c1,x). [resolve(111,b,96,a)].
242 -part(x,c1). [resolve(112,b,96,a)].
243 -depicts(x,c1). [resolve(113,b,96,a)].
248 in(c1,c2) | in(c2,c1) | depicts(c1,c2) | def_in(c1,c2) | def_in(c2,c1) | c2 = c1. [resolve(167,a,157,a),unit_del(c,241),unit_del(d,242),unit_del(f,243)].
257 part(c2,f1(c2)). [resolve(231,a,125,a)].
295 in(c1,c2) | in(c2,c1) | depicts(c1,c2) | def_in(c1,c2) | c2 = c1. [resolve(248,e,221,b),unit_del(f,231)].
309 part(f1(c2),c2). [resolve(257,a,120,a)].
579 in(c1,c2) | in(c2,c1) | depicts(c1,c2) | c2 = c1 | part(f10(c1,c2),c2). [resolve(295,d,156,a)].
580 in(c1,c2) | in(c2,c1) | depicts(c1,c2) | c2 = c1 | depicts(c1,f10(c1,c2)). [resolve(295,d,155,a)].
581 in(c1,c2) | in(c2,c1) | depicts(c1,c2) | c2 = c1 | point(f10(c1,c2)). [resolve(295,d,154,a)].
3774 in(c1,c2) | depicts(c1,c2) | c2 = c1 | part(f10(c1,c2),c2). [resolve(579,b,184,a),unit_del(e,231)].
3808 in(c1,c2) | depicts(c1,c2) | c2 = c1 | depicts(c1,f10(c1,c2)). [resolve(580,b,184,a),unit_del(e,231)].
3848 in(c1,c2) | depicts(c1,c2) | c2 = c1 | point(f10(c1,c2)). [resolve(581,b,184,a),unit_del(e,231)].
20442 depicts(c1,c2) | c2 = c1 | point(f10(c1,c2)). [resolve(3848,a,190,a),unit_del(d,231)].
20453 c2 = c1 | point(f10(c1,c2)). [resolve(20442,a,234,a),unit_del(c,231)].
20786 depicts(c1,c2) | c2 = c1 | part(f10(c1,c2),c2). [resolve(3774,a,190,a),unit_del(d,231)].
20807 depicts(c1,c2) | c2 = c1 | g_in(f10(c1,c2),c2). [resolve(20786,c,160,b)].
20820 depicts(c1,c2) | c2 = c1 | -g_in(c1,f10(c1,c2)) | -point(f10(c1,c2)). [resolve(20807,c,230,b)].
20985 depicts(c1,c2) | c2 = c1 | depicts(c1,f10(c1,c2)). [resolve(3808,a,190,a),unit_del(d,231)].
20987 depicts(c1,c2) | c2 = c1 | g_in(c1,f10(c1,c2)). [resolve(20985,c,162,b)].
41159 depicts(c1,c2) | c2 = c1 | -point(f10(c1,c2)). [resolve(20820,c,20987,c),merge(d),merge(e)].
41160 depicts(c1,c2) | c2 = c1. [resolve(41159,c,20453,b),merge(c)].
41162 c2 = c1. [resolve(41160,a,234,a),unit_del(b,231)].
70534 $F. [back_rewrite(309),rewrite([41162(1),41162(3)]),unit_del(a,242)].

============================== end of proof ==========================
@@ -0,0 +1,38 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 21841 was started by zhuojun on Zhuojun-Li.local,
Thu Jul 25 17:09:37 2019
The command was "/Users/zhuojun/Desktop/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.02 (+ 0.01) seconds.
% Length of proof is 18.
% Level of proof is 5.
% Maximum clause weight is 6.
% Given clauses 91.

18 (all x (point(x) -> (exists e (edge(e) & part(x,e))))) # label(non_clause). [assumption].
34 (all x (g_line(x) <-> point(x))) # label(non_clause). [assumption].
35 (all x (plane(x) <-> edge(x))) # label(non_clause). [assumption].
37 (all x all y (g_in(x,y) <-> in(x,y) | in(y,x) | part(x,y) | part(y,x) | depicts(x,y) | depicts(y,x) | x = y)) # label(non_clause). [assumption].
38 (all l (g_line(l) -> (exists x (plane(x) & g_in(l,x))))) # label(non_clause) # label(goal). [goal].
88 -g_line(x) | point(x). [clausify(34)].
89 g_line(c1). [deny(38)].
90 plane(x) | -edge(x). [clausify(35)].
92 -plane(x) | -g_in(c1,x). [deny(38)].
123 -point(x) | edge(f2(x)). [clausify(18)].
124 -point(x) | part(x,f2(x)). [clausify(18)].
153 g_in(x,y) | -part(x,y). [clausify(37)].
207 point(c1). [resolve(89,a,88,a)].
208 -g_in(c1,x) | -edge(x). [resolve(92,a,90,a)].
219 part(c1,f2(c1)). [resolve(207,a,124,a)].
220 edge(f2(c1)). [resolve(207,a,123,a)].
231 g_in(c1,f2(c1)). [resolve(219,a,153,b)].
257 $F. [resolve(231,a,208,a),unit_del(a,220)].

============================== end of proof ==========================
@@ -0,0 +1,38 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 21848 was started by zhuojun on Zhuojun-Li.local,
Thu Jul 25 17:10:15 2019
The command was "/Users/zhuojun/Desktop/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.02 (+ 0.01) seconds.
% Length of proof is 18.
% Level of proof is 5.
% Maximum clause weight is 6.
% Given clauses 107.

22 (all e (edge(e) -> (exists p1 exists p2 (point(p1) & point(p2) & part(p1,e) & part(p2,e) & p1 != p2)))) # label(non_clause). [assumption].
34 (all x (g_line(x) <-> point(x))) # label(non_clause). [assumption].
35 (all x (plane(x) <-> edge(x))) # label(non_clause). [assumption].
37 (all x all y (g_in(x,y) <-> in(x,y) | in(y,x) | part(x,y) | part(y,x) | depicts(x,y) | depicts(y,x) | x = y)) # label(non_clause). [assumption].
38 (all x (plane(x) -> (exists y (g_line(y) & g_in(y,x))))) # label(non_clause) # label(goal). [goal].
87 g_line(x) | -point(x). [clausify(34)].
89 -g_line(x) | -g_in(x,c1). [deny(38)].
91 -plane(x) | edge(x). [clausify(35)].
92 plane(c1). [deny(38)].
137 -edge(x) | point(f7(x)). [clausify(22)].
139 -edge(x) | part(f7(x),x). [clausify(22)].
153 g_in(x,y) | -part(x,y). [clausify(37)].
207 -g_in(x,c1) | -point(x). [resolve(89,a,87,a)].
208 edge(c1). [resolve(92,a,91,a)].
220 part(f7(c1),c1). [resolve(208,a,139,a)].
222 point(f7(c1)). [resolve(208,a,137,a)].
246 g_in(f7(c1),c1). [resolve(220,a,153,b)].
307 $F. [resolve(246,a,207,a),unit_del(a,222)].

============================== end of proof ==========================

0 comments on commit d6be54d

Please sign in to comment.
You can’t perform that action at this time.