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
|
============================== prooftrans ============================
Prover9 (32) version 2009-02A, February 2009.
Process 15826 was started by mccune on cleo,
Wed Feb 25 12:25:50 2009
The command was "/home/mccune/bin/prover9 -f subset_trans.in".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 14.
% Level of proof is 4.
% Maximum clause weight is 6.
% Given clauses 6.
1 (all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y))))) # label(non_clause). [assumption].
2 (all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z))) # label(non_clause) # label(goal). [goal].
3 subset(x,y) | member(f1(x,y),x). [clausify(1)].
4 -subset(x,y) | -member(z,x) | member(z,y). [clausify(1)].
5 subset(x,y) | -member(f1(x,y),y). [clausify(1)].
6 subset(c1,c2). [deny(2)].
7 subset(c2,c3). [deny(2)].
8 -subset(c1,c3). [deny(2)].
11 -member(x,c1) | member(x,c2). [resolve(6,a,4,a)].
12 -member(x,c2) | member(x,c3). [resolve(7,a,4,a)].
13 member(f1(c1,c3),c1). [resolve(8,a,3,a)].
14 -member(f1(c1,c3),c3). [resolve(8,a,5,a)].
15 member(f1(c1,c3),c2). [resolve(13,a,11,a)].
18A -member(f1(c1,c3),c2). [resolve(12,b,14,a)].
18 $F. [resolve(15,a,18A,a)].
============================== end of proof ==========================
|
