    subset_trans.out

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".
% 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.

(all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y)))))
label(non_clause)
(all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z)))
label(non_clause)
label(goal)
subset(x,y)
member(f1(x,y),x)
-subset(x,y)
-member(z,x)
member(z,y)
subset(x,y)
-member(f1(x,y),y)
subset(c1,c2)
subset(c2,c3)
-subset(c1,c3)
-member(x,c1)
member(x,c2)
-member(x,c2)
member(x,c3)
member(f1(c1,c3),c1)
-member(f1(c1,c3),c3)
member(f1(c1,c3),c2)
$F