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
|
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 9270 was started by mccune on cleo,
Tue Jan 22 11:28:26 2008
The command was "prover9 -f bw.in".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 5.51 (+ 0.02) seconds: fixed_point_combinator.
% Length of proof is 13.
% Level of proof is 6.
% Maximum clause weight is 60.
% Given clauses 117.
1 a = b. [assumption].
2 f(c,g(h(g(a),d))) != g(h(g(b),d)). [assumption].
3 f(c,x) = x. [assumption].
4 f(c,g(h(g(b),d))) != g(h(g(b),d)). [para(1(a,1),2(a,1,2,1,1,1))].
5 $F. [resolve(3,a,4,a)].
============================== end of proof ==========================
|
