cycle_path_subgraph_nonisolated2most_group_13.proof

============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 3684 was started by cchui on MacBook-Pro.local,
Thu Nov  8 18:55:39 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 2.47 (+ 0.01) seconds.
% Length of proof is 57.
% Level of proof is 3.
% Maximum clause weight is 64.
% Given clauses 53.

1 (all x all y all z all u all q all l1 all l2 all l3 (plane(q) & point(x) & point(y) & point(z) & point(u) & in(x,q) & in(y,q) & in(z,q) & in(u,q) & line(l1) & in(l1,q) & in(x,l1) & in(y,l1) & line(l2) & in(l2,q) & in(x,l2) & in(z,l2) & line(l3) & in(l3,q) & in(x,l3) & in(u,l3) -> u = z | y = z | u = y)) # 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 a1 all a2 all a3 all a4 all g all b1 all b2 all b3 (group(g) & atom(a1) & atom(a2) & atom(a3) & atom(a4) & mol(a1,g) & mol(a2,g) & mol(a3,g) & mol(a4,g) & bond(b1) & mol(b1,g) & mol(a1,b1) & mol(a2,b1) & bond(b2) & mol(b2,g) & mol(a1,b2) & mol(a3,b2) & bond(b3) & mol(b3,g) & mol(a1,b3) & mol(a4,b3) -> a4 = a3 | a2 = a3 | a4 = a2)) # label(non_clause) # label(goal).  [goal].
26 -atom(x) | point(x).  [clausify(19)].
27 atom(c1).  [deny(24)].
28 atom(c2).  [deny(24)].
29 atom(c3).  [deny(24)].
30 atom(c4).  [deny(24)].
32 -bond(x) | line(x).  [clausify(20)].
33 bond(c6).  [deny(24)].
34 bond(c7).  [deny(24)].
35 bond(c8).  [deny(24)].
37 -group(x) | plane(x).  [clausify(21)].
38 group(c5).  [deny(24)].
42 -mol(x,y) | in(x,y).  [clausify(23)].
43 mol(c1,c5).  [deny(24)].
44 mol(c2,c5).  [deny(24)].
45 mol(c3,c5).  [deny(24)].
46 mol(c4,c5).  [deny(24)].
47 mol(c6,c5).  [deny(24)].
48 mol(c1,c6).  [deny(24)].
49 mol(c2,c6).  [deny(24)].
50 mol(c7,c5).  [deny(24)].
51 mol(c1,c7).  [deny(24)].
52 mol(c3,c7).  [deny(24)].
53 mol(c8,c5).  [deny(24)].
54 mol(c1,c8).  [deny(24)].
55 mol(c4,c8).  [deny(24)].
56 -plane(x) | -point(y) | -point(z) | -point(u) | -point(w) | -in(y,x) | -in(z,x) | -in(u,x) | -in(w,x) | -line(v5) | -in(v5,x) | -in(y,v5) | -in(z,v5) | -line(v6) | -in(v6,x) | -in(y,v6) | -in(u,v6) | -line(v7) | -in(v7,x) | -in(y,v7) | -in(w,v7) | w = u | u = z | w = z.  [clausify(1)].
86 c4 != c3.  [deny(24)].
87 c3 != c2.  [deny(24)].
88 c4 != c2.  [deny(24)].
89 point(c1).  [resolve(27,a,26,a)].
90 point(c2).  [resolve(28,a,26,a)].
91 point(c3).  [resolve(29,a,26,a)].
92 point(c4).  [resolve(30,a,26,a)].
93 line(c6).  [resolve(33,a,32,a)].
94 line(c7).  [resolve(34,a,32,a)].
95 line(c8).  [resolve(35,a,32,a)].
96 plane(c5).  [resolve(38,a,37,a)].
97 in(c1,c5).  [resolve(43,a,42,a)].
98 in(c2,c5).  [resolve(44,a,42,a)].
99 in(c3,c5).  [resolve(45,a,42,a)].
100 in(c4,c5).  [resolve(46,a,42,a)].
101 in(c6,c5).  [resolve(47,a,42,a)].
102 in(c1,c6).  [resolve(48,a,42,a)].
103 in(c2,c6).  [resolve(49,a,42,a)].
104 in(c7,c5).  [resolve(50,a,42,a)].
105 in(c1,c7).  [resolve(51,a,42,a)].
106 in(c3,c7).  [resolve(52,a,42,a)].
107 in(c8,c5).  [resolve(53,a,42,a)].
108 in(c1,c8).  [resolve(54,a,42,a)].
109 in(c4,c8).  [resolve(55,a,42,a)].
448 $F.  [ur(56,a,96,a,b,89,a,c,91,a,d,90,a,e,92,a,f,97,a,g,99,a,h,98,a,i,100,a,j,94,a,k,104,a,l,105,a,m,106,a,n,93,a,o,101,a,p,102,a,q,103,a,r,95,a,s,107,a,t,108,a,v,88,a,w,87,a(flip),x,86,a),unit_del(a,109)].

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