[請益] prover9
Assumption：
exists x ( exists y ( x!=y & (G(x) & G(y)) )).
Goals:
exists x G(x).
卻跑出 Prover9 Exit:Exhausted.
Some, but not all, of the requested proofs were found.
請問怎麼會這樣 謝謝~
以下是詳細資訊；
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.01) seconds.
% Length of proof is 5.
% Level of proof is 2.
% Maximum clause weight is 0.
% Given clauses 0.
1 (exists x exists y (x != y & G(x) & G(y))) # label(non_clause).
[assumption].
2 (exists x G(x)) # label(non_clause) # label(goal). [goal].
3 -G(x). [deny(2)].
4 G(c1). [clausify(1)].
7 $F. [resolve(3,a,4,a)].
============================== end of proof ==========================
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 118.169.224.47
→
01/28 18:19, , 1F
01/28 18:19, 1F
討論串 (同標題文章)