FDL > PVS > Graphs > ramsey new > subgraph clique > pf:subgraph clique > 1 > 1 > 1 > 1 > 2 > 1 > 1 > 1 (2 nodes)

Conclusion

-1. C!1(i!1)
-2. C!1(j!1)
-3. vert(g!1)(i!1) AND V!1(i!1)
-4. card(C!1) > = p!1
-5. FORALL i_2004:T, j : ((NOT (i_2004 = j)) AND C!1(i_2004) AND C!1(j)) IMPLIES ((NOT (i_2004 = j)) AND edges(g!1)(dbl[T](i_2004, j)) AND (FORALL x:T : ((x = i_2004) OR (x = j)) IMPLIES V!1(x)))

1. i!1 = j!1
2. edges(g!1)(dbl[T](i!1, j!1))

Tactic
 INST?
Premise 1.   (has proof of 1 step)

-1. C!1(i!1)
-2. C!1(j!1)
-3. vert(g!1)(i!1) AND V!1(i!1)
-4. card(C!1) > = p!1
-5. ((NOT (i!1 = j!1)) AND C!1(i!1) AND C!1(j!1)) IMPLIES ((NOT (i!1 = j!1)) AND edges(g!1)(dbl[T](i!1, j!1)) AND (FORALL x:T : ((x = i!1) OR (x = j!1)) IMPLIES V!1(x)))

1. i!1 = j!1
2. edges(g!1)(dbl[T](i!1, j!1))