----- Otter 3.2, August 2001 -----
The process was started by ??? on ???,
Sat Nov 29 22:37:30 2003
The command was "otter".

set(auto).
   dependent: set(auto1).
   dependent: set(process_input).
   dependent: clear(print_kept).
   dependent: clear(print_new_demod).
   dependent: clear(print_back_demod).
   dependent: clear(print_back_sub).
   dependent: set(control_memory).
   dependent: assign(max_mem, 12000).
   dependent: assign(pick_given_ratio, 4).
   dependent: assign(stats_level, 1).
   dependent: assign(max_seconds, 10800).
clear(print_given).
assign(max_seconds,8).
assign(max_distinct_vars,2).
assign(max_literals,1).
assign(max_mem,44000).
assign(max_weight,20).
include("booleanAx.txt").
------- start included file booleanAx.txt-------
include("1_2booleanAx.txt").
------- start included file 1_2booleanAx.txt-------

formula_list(usable).
all x y (u(x,y)=u(y,x)).
all x y z (u(x,u(y,z))=u(u(x,y),z)).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] u(x,y)=u(y,x).
0 [] u(x,u(y,z))=u(u(x,y),z).
end_of_list.
------- end included file 1_2booleanAx.txt-------
include("3booleanAx.txt").
------- start included file 3booleanAx.txt-------

formula_list(usable).
all x y (u(c(u(c(x),y)),c(u(c(x),c(y))))=x).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x.
end_of_list.
------- end included file 3booleanAx.txt-------
------- end included file booleanAx.txt-------
include("peirceanAx0.txt").
------- start included file peirceanAx0.txt-------

formula_list(usable).
all x y z (k(x,k(y,z))=k(k(x,y),z)).
all x (r(r(x))=x).
all x y (r(u(x,y))=u(r(x),r(y))).
all x y (r(k(x,y))=k(r(y),r(x))).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] k(x,k(y,z))=k(k(x,y),z).
0 [] r(r(x))=x.
0 [] r(u(x,y))=u(r(x),r(y)).
0 [] r(k(x,y))=k(r(y),r(x)).
end_of_list.
------- end included file peirceanAx0.txt-------
include("peirceanAx1.txt").
------- start included file peirceanAx1.txt-------

formula_list(usable).
all x y z (k(u(x,y),z)=u(k(x,z),k(y,z))).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] k(u(x,y),z)=u(k(x,z),k(y,z)).
end_of_list.
------- end included file peirceanAx1.txt-------
include("peirceanAx2.txt").
------- start included file peirceanAx2.txt-------

formula_list(usable).
all x (k(x,I)=x).
all x y (u(k(r(x),c(k(x,y))),c(y))=c(y)).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] k(x,I)=x.
0 [] u(k(r(x),c(k(x,y))),c(y))=c(y).
end_of_list.
------- end included file peirceanAx2.txt-------
include("uzDef.txt").
------- start included file uzDef.txt-------

formula_list(usable).
D=c(I).
U=u(I,D).
Z=c(U).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] D=c(I).
0 [] U=u(I,D).
0 [] Z=c(U).
end_of_list.
------- end included file uzDef.txt-------
include("xiii.txt").
------- start included file xiii.txt-------

formula_list(usable).
all x (k(x,Z)=Z).
all x (k(Z,x)=Z).
all x (d(x,U)=U).
all x (d(U,x)=U).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] k(x,Z)=Z.
0 [] k(Z,x)=Z.
0 [] d(x,U)=U.
0 [] d(U,x)=U.
end_of_list.
------- end included file xiii.txt-------
include("i.txt").
------- start included file i.txt-------

formula_list(usable).
all x y (i(x,y)->i(r(x),r(y))).
all x y (r(u(x,y))=u(r(x),r(y))).
all x (r(c(x))=c(r(x))).
all x y (r(n(x,y))=n(r(x),r(y))).
all x (r(r(x))=x).
all x y (r(d(x,y))=d(r(y),r(x))).
all x y (r(k(x,y))=k(r(y),r(x))).
r(I)=I.
r(Z)=Z.
r(U)=U.
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] -i(x,y)|i(r(x),r(y)).
0 [] r(u(x,y))=u(r(x),r(y)).
0 [] r(c(x))=c(r(x)).
0 [] r(n(x,y))=n(r(x),r(y)).
0 [] r(r(x))=x.
0 [] r(d(x,y))=d(r(y),r(x)).
0 [] r(k(x,y))=k(r(y),r(x)).
0 [] r(I)=I.
0 [] r(Z)=Z.
0 [] r(U)=U.
end_of_list.
------- end included file i.txt-------
include("xvii_b.txt").
------- start included file xvii_b.txt-------

formula_list(usable).
all x (k(k(U,r(x)),U)=k(k(U,x),U)).
-(all x (r(k(k(U,x),U))=k(k(U,x),U))).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] k(k(U,r(x)),U)=k(k(U,x),U).
0 [] r(k(k(U,$c1),U))!=k(k(U,$c1),U).
end_of_list.
------- end included file xvii_b.txt-------

SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2.

This is a Horn set with equality.  The strategy will be
Knuth-Bendix and hyper_res, with positive clauses in
sos and nonpositive clauses in usable.

   dependent: set(knuth_bendix).
   dependent: set(para_from).
   dependent: set(para_into).
   dependent: clear(para_from_right).
   dependent: clear(para_into_right).
   dependent: set(para_from_vars).
   dependent: set(eq_units_both_ways).
   dependent: set(dynamic_demod_all).
   dependent: set(dynamic_demod).
   dependent: set(order_eq).
   dependent: set(back_demod).
   dependent: set(lrpo).
   dependent: set(hyper_res).
   dependent: clear(order_hyper).

------------> process usable:
** KEPT (pick-wt=8): 1 [] -i(x,y)|i(r(x),r(y)).
** KEPT (pick-wt=12): 2 [] r(k(k(U,$c1),U))!=k(k(U,$c1),U).

------------> process sos:
** KEPT (pick-wt=7): 3 [] u(x,y)=u(y,x).
** KEPT (pick-wt=11): 5 [copy,4,flip.1] u(u(x,y),z)=u(x,u(y,z)).
---> New Demodulator: 6 [new_demod,5] u(u(x,y),z)=u(x,u(y,z)).
** KEPT (pick-wt=14): 7 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x.
---> New Demodulator: 8 [new_demod,7] u(c(u(c(x),y)),c(u(c(x),c(y))))=x.
** KEPT (pick-wt=11): 10 [copy,9,flip.1] k(k(x,y),z)=k(x,k(y,z)).
---> New Demodulator: 11 [new_demod,10] k(k(x,y),z)=k(x,k(y,z)).
** KEPT (pick-wt=5): 12 [] r(r(x))=x.
---> New Demodulator: 13 [new_demod,12] r(r(x))=x.
** KEPT (pick-wt=10): 14 [] r(u(x,y))=u(r(x),r(y)).
---> New Demodulator: 15 [new_demod,14] r(u(x,y))=u(r(x),r(y)).
** KEPT (pick-wt=10): 16 [] r(k(x,y))=k(r(y),r(x)).
---> New Demodulator: 17 [new_demod,16] r(k(x,y))=k(r(y),r(x)).
** KEPT (pick-wt=13): 19 [copy,18,flip.1] u(k(x,y),k(z,y))=k(u(x,z),y).
---> New Demodulator: 20 [new_demod,19] u(k(x,y),k(z,y))=k(u(x,z),y).
** KEPT (pick-wt=5): 21 [] k(x,I)=x.
---> New Demodulator: 22 [new_demod,21] k(x,I)=x.
** KEPT (pick-wt=13): 23 [] u(k(r(x),c(k(x,y))),c(y))=c(y).
---> New Demodulator: 24 [new_demod,23] u(k(r(x),c(k(x,y))),c(y))=c(y).
** KEPT (pick-wt=4): 26 [copy,25,flip.1] c(I)=D.
---> New Demodulator: 27 [new_demod,26] c(I)=D.
** KEPT (pick-wt=5): 29 [copy,28,flip.1] u(I,D)=U.
---> New Demodulator: 30 [new_demod,29] u(I,D)=U.
** KEPT (pick-wt=4): 32 [copy,31,flip.1] c(U)=Z.
---> New Demodulator: 33 [new_demod,32] c(U)=Z.
** KEPT (pick-wt=5): 34 [] k(x,Z)=Z.
---> New Demodulator: 35 [new_demod,34] k(x,Z)=Z.
** KEPT (pick-wt=5): 36 [] k(Z,x)=Z.
---> New Demodulator: 37 [new_demod,36] k(Z,x)=Z.
** KEPT (pick-wt=5): 38 [] d(x,U)=U.
---> New Demodulator: 39 [new_demod,38] d(x,U)=U.
** KEPT (pick-wt=5): 40 [] d(U,x)=U.
---> New Demodulator: 41 [new_demod,40] d(U,x)=U.
** KEPT (pick-wt=11): 43 [copy,42,demod,15] u(r(x),r(y))=u(r(x),r(y)).
** KEPT (pick-wt=7): 44 [] r(c(x))=c(r(x)).
---> New Demodulator: 45 [new_demod,44] r(c(x))=c(r(x)).
** KEPT (pick-wt=10): 46 [] r(n(x,y))=n(r(x),r(y)).
---> New Demodulator: 47 [new_demod,46] r(n(x,y))=n(r(x),r(y)).
** KEPT (pick-wt=3): 49 [copy,48,demod,13] x=x.
** KEPT (pick-wt=10): 50 [] r(d(x,y))=d(r(y),r(x)).
---> New Demodulator: 51 [new_demod,50] r(d(x,y))=d(r(y),r(x)).
  Following clause subsumed by 49 during input processing: 0 [demod,17] k(r(y),r(x))=k(r(y),r(x)).
** KEPT (pick-wt=4): 52 [] r(I)=I.
---> New Demodulator: 53 [new_demod,52] r(I)=I.
** KEPT (pick-wt=4): 54 [] r(Z)=Z.
---> New Demodulator: 55 [new_demod,54] r(Z)=Z.
** KEPT (pick-wt=4): 56 [] r(U)=U.
---> New Demodulator: 57 [new_demod,56] r(U)=U.
** KEPT (pick-wt=12): 59 [copy,58,demod,11,11] k(U,k(r(x),U))=k(U,k(x,U)).
---> New Demodulator: 60 [new_demod,59] k(U,k(r(x),U))=k(U,k(x,U)).
  Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] u(x,y)=u(y,x).
>>>> Starting back demodulation with 6.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 11.
    >> back demodulating 2 with 11.

----> UNIT CONFLICT at   0.04 sec ----> 62 [binary,61.1,49.1] $F.

Length of proof is 4.  Level of proof is 3.

---------------- PROOF ----------------

2 [] r(k(k(U,$c1),U))!=k(k(U,$c1),U).
9 [] k(x,k(y,z))=k(k(x,y),z).
11,10 [copy,9,flip.1] k(k(x,y),z)=k(x,k(y,z)).
13,12 [] r(r(x))=x.
17,16 [] r(k(x,y))=k(r(y),r(x)).
48 [] r(r(x))=x.
49 [copy,48,demod,13] x=x.
57,56 [] r(U)=U.
58 [] k(k(U,r(x)),U)=k(k(U,x),U).
60,59 [copy,58,demod,11,11] k(U,k(r(x),U))=k(U,k(x,U)).
61 [back_demod,2,demod,11,17,17,57,57,11,60,11] k(U,k($c1,U))!=k(U,k($c1,U)).
62 [binary,61.1,49.1] $F.

------------ end of proof -------------


Search stopped by max_proofs option.

============ end of search ============

-------------- statistics -------------
clauses given                  0
clauses generated              0
clauses kept                  29
clauses forward subsumed       2
clauses back subsumed          0
Kbytes malloced              127

----------- times (seconds) -----------
user CPU time          0.24          (0 hr, 0 min, 0 sec)
system CPU time        0.00          (0 hr, 0 min, 0 sec)
wall-clock time        1             (0 hr, 0 min, 1 sec)
hyper_res time         0.00
para_into time         0.00
para_from time         0.00
for_sub time           0.00
back_sub time          0.00
conflict time          0.00
demod time             0.00

That finishes the proof of the theorem.

Process 0 finished Sat Nov 29 22:37:31 2003