/
cycle_path_subgraph_nonisolated2most_group_11.proof
50 lines (45 loc) · 2.41 KB
/
cycle_path_subgraph_nonisolated2most_group_11.proof
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 3667 was started by cchui on MacBook-Pro.local,
Thu Nov 8 18:54:58 2018
The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 9.37 (+ 0.02) seconds.
% Length of proof is 30.
% Level of proof is 6.
% Maximum clause weight is 12.
% Given clauses 127.
4 (all l all q (line(l) & plane(q) & -in(l,q) -> (exists p (point(p) & in(p,l) & -in(p,q))))) # label(non_clause). [assumption].
19 (all x (atom(x) <-> point(x))) # label(non_clause). [assumption].
20 (all x (bond(x) <-> line(x))) # label(non_clause). [assumption].
21 (all x (group(x) <-> plane(x))) # label(non_clause). [assumption].
23 (all x all y (mol(x,y) <-> in(x,y))) # label(non_clause). [assumption].
24 (all b all g (bond(b) & group(g) & -mol(b,g) -> (exists a (atom(a) & mol(a,b) & -mol(a,g))))) # label(non_clause) # label(goal). [goal].
25 atom(x) | -point(x). [clausify(19)].
27 -atom(x) | -mol(x,c1) | mol(x,c2). [deny(24)].
29 -bond(x) | line(x). [clausify(20)].
30 bond(c1). [deny(24)].
32 -group(x) | plane(x). [clausify(21)].
33 group(c2). [deny(24)].
40 -line(x) | -plane(y) | in(x,y) | point(f2(x,y)). [clausify(4)].
41 -line(x) | -plane(y) | in(x,y) | in(f2(x,y),x). [clausify(4)].
42 -line(x) | -plane(y) | in(x,y) | -in(f2(x,y),y). [clausify(4)].
66 -mol(x,y) | in(x,y). [clausify(23)].
67 mol(x,y) | -in(x,y). [clausify(23)].
68 -mol(c1,c2). [deny(24)].
69 -mol(x,c1) | mol(x,c2) | -point(x). [resolve(27,a,25,a)].
70 line(c1). [resolve(30,a,29,a)].
71 plane(c2). [resolve(33,a,32,a)].
81 -in(c1,c2). [ur(67,a,68,a)].
97 -line(x) | in(x,c2) | in(f2(x,c2),x). [resolve(71,a,41,b)].
98 -line(x) | in(x,c2) | point(f2(x,c2)). [resolve(71,a,40,b)].
100 -in(f2(c1,c2),c2). [ur(42,a,70,a,b,71,a,c,81,a)].
275 in(f2(c1,c2),c1). [resolve(97,a,70,a),unit_del(a,81)].
300 point(f2(c1,c2)). [resolve(98,a,70,a),unit_del(a,81)].
305 -mol(f2(c1,c2),c2). [ur(66,b,100,a)].
336 -mol(f2(c1,c2),c1). [ur(69,b,305,a,c,300,a)].
390 $F. [ur(67,a,336,a),unit_del(a,275)].
============================== end of proof ==========================