----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Thu Apr 19 22:36:18 2001
The command was "C:\BIN\OTTER95.EXE".

WARNING: clear(symbol_elim) flag already clear.
clear(symbol_elim).
set(order_eq).
set(sort_literals).
set(dynamic_demod_all).
   dependent: set(dynamic_demod).
set(back_demod).
set(process_input).
clear(print_given).
set(print_lists_at_end).
set(lrpo).
set(lex_order_vars).

lex([OMEGA,FULL,REGULAR,U(x),tc(x),P(x),TC,H(x),intersection(x,x),image(x,x),A(x),inverse(x),full(x),equal(x,x),member(x,x),subclass(x,x)]).
assign(max_mem,300).
assign(stats_level,0).

list(usable).
0 [] subclass(x,x).
end_of_list.

formula_list(sos).
all x equal(U(intersection(FULL,P(x))),H(x)).
equal(H(FULL),intersection(FULL,P(FULL))).
equal(U(H(FULL)),H(FULL)).
equal(H(OMEGA),OMEGA).
subclass(OMEGA,intersection(REGULAR,H(FULL))).
all x equal(U(image(inverse(TC),P(x))),H(x)).
all x full(H(x)).
all x equal(tc(H(x)),H(x)).
all x subclass(H(x),x).
equal(intersection(REGULAR,H(FULL)),OMEGA).
all x y (subclass(x,H(y))->subclass(tc(x),y)).
all x equal(image(inverse(TC),P(x)),P(H(x))).
all x y (member(x,H(y))->subclass(tc(x),y)).
all x y (subclass(x,y)->subclass(H(x),H(y))).
all x y z (member(x,H(A(y)))&member(z,y)->member(x,H(z))).
all x (full(x)->equal(H(x),x)).
equal(H(REGULAR),REGULAR).
all x equal(H(tc(x)),tc(x)).
all x equal(H(H(x)),H(x)).
all x y (full(x)&subclass(x,y)->subclass(x,H(y))).
all x equal(intersection(x,P(H(x))),H(x)).
all x y (subclass(tc(x),y)->subclass(x,H(y))).
all x y equal(H(intersection(x,y)),intersection(H(x),H(y))).
all x equal(H(P(x)),P(H(x))).
all x y (subclass(intersection(x,P(y)),y)->subclass(intersection(REGULAR,H(x)),y)).
all x equal(intersection(x,image(inverse(TC),P(x))),H(x)).
all x y (member(x,y)&subclass(tc(x),y)->member(x,H(y))).
end_of_list.

-------> sos clausifies to:

list(sos).
0 [] equal(U(intersection(FULL,P(x))),H(x)).
0 [] equal(H(FULL),intersection(FULL,P(FULL))).
0 [] equal(U(H(FULL)),H(FULL)).
0 [] equal(H(OMEGA),OMEGA).
0 [] subclass(OMEGA,intersection(REGULAR,H(FULL))).
0 [] equal(U(image(inverse(TC),P(x))),H(x)).
0 [] full(H(x)).
0 [] equal(tc(H(x)),H(x)).
0 [] subclass(H(x),x).
0 [] equal(intersection(REGULAR,H(FULL)),OMEGA).
0 [] -subclass(x,H(y))|subclass(tc(x),y).
0 [] equal(image(inverse(TC),P(x)),P(H(x))).
0 [] -member(x,H(y))|subclass(tc(x),y).
0 [] -subclass(x,y)|subclass(H(x),H(y)).
0 [] -member(x,H(A(y)))| -member(z,y)|member(x,H(z)).
0 [] -full(x)|equal(H(x),x).
0 [] equal(H(REGULAR),REGULAR).
0 [] equal(H(tc(x)),tc(x)).
0 [] equal(H(H(x)),H(x)).
0 [] -full(x)| -subclass(x,y)|subclass(x,H(y)).
0 [] equal(intersection(x,P(H(x))),H(x)).
0 [] -subclass(tc(x),y)|subclass(x,H(y)).
0 [] equal(H(intersection(x,y)),intersection(H(x),H(y))).
0 [] equal(H(P(x)),P(H(x))).
0 [] -subclass(intersection(x,P(y)),y)|subclass(intersection(REGULAR,H(x)),y).
0 [] equal(intersection(x,image(inverse(TC),P(x))),H(x)).
0 [] -member(x,y)| -subclass(tc(x),y)|member(x,H(y)).
end_of_list.

list(demodulators).
1 [] equal(intersection(x,y),intersection(y,x)).
2 [] equal(U(P(x)),x).
end_of_list.
LRPO dependent demodulator: 1 [] equal(intersection(x,y),intersection(y,x)).

------------> process usable:
** KEPT (pick-wt=3): 3 [] subclass(x,x).

------------> process sos:
** KEPT (pick-wt=8): 4 [] equal(U(intersection(FULL,P(x))),H(x)).
---> New Demodulator: 5 [new_demod,4] equal(U(intersection(FULL,P(x))),H(x)).
** KEPT (pick-wt=7): 7 [copy,6,flip.1] equal(intersection(FULL,P(FULL)),H(FULL)).
---> New Demodulator: 8 [new_demod,7] equal(intersection(FULL,P(FULL)),H(FULL)).
** KEPT (pick-wt=6): 9 [] equal(U(H(FULL)),H(FULL)).
---> New Demodulator: 10 [new_demod,9] equal(U(H(FULL)),H(FULL)).
** KEPT (pick-wt=4): 11 [] equal(H(OMEGA),OMEGA).
---> New Demodulator: 12 [new_demod,11] equal(H(OMEGA),OMEGA).
** KEPT (pick-wt=6): 13 [] subclass(OMEGA,intersection(REGULAR,H(FULL))).
** KEPT (pick-wt=9): 14 [] equal(U(image(inverse(TC),P(x))),H(x)).
---> New Demodulator: 15 [new_demod,14] equal(U(image(inverse(TC),P(x))),H(x)).
** KEPT (pick-wt=3): 16 [] full(H(x)).
** KEPT (pick-wt=6): 17 [] equal(tc(H(x)),H(x)).
---> New Demodulator: 18 [new_demod,17] equal(tc(H(x)),H(x)).
** KEPT (pick-wt=4): 19 [] subclass(H(x),x).
** KEPT (pick-wt=6): 20 [] equal(intersection(REGULAR,H(FULL)),OMEGA).
---> New Demodulator: 21 [new_demod,20] equal(intersection(REGULAR,H(FULL)),OMEGA).
** KEPT (pick-wt=8): 22 [] -subclass(x,H(y))|subclass(tc(x),y).
** KEPT (pick-wt=9): 23 [] equal(image(inverse(TC),P(x)),P(H(x))).
---> New Demodulator: 24 [new_demod,23] equal(image(inverse(TC),P(x)),P(H(x))).
** KEPT (pick-wt=8): 25 [] -member(x,H(y))|subclass(tc(x),y).
** KEPT (pick-wt=8): 26 [] -subclass(x,y)|subclass(H(x),H(y)).
** KEPT (pick-wt=12): 27 [] -member(x,H(A(y)))| -member(z,y)|member(x,H(z)).
** KEPT (pick-wt=6): 28 [] -full(x)|equal(H(x),x).
** KEPT (pick-wt=4): 29 [] equal(H(REGULAR),REGULAR).
---> New Demodulator: 30 [new_demod,29] equal(H(REGULAR),REGULAR).
** KEPT (pick-wt=6): 31 [] equal(H(tc(x)),tc(x)).
---> New Demodulator: 32 [new_demod,31] equal(H(tc(x)),tc(x)).
** KEPT (pick-wt=6): 33 [] equal(H(H(x)),H(x)).
---> New Demodulator: 34 [new_demod,33] equal(H(H(x)),H(x)).
** KEPT (pick-wt=9): 35 [] -full(x)| -subclass(x,y)|subclass(x,H(y)).
** KEPT (pick-wt=8): 36 [] equal(intersection(x,P(H(x))),H(x)).
---> New Demodulator: 37 [new_demod,36] equal(intersection(x,P(H(x))),H(x)).
** KEPT (pick-wt=8): 38 [] -subclass(tc(x),y)|subclass(x,H(y)).
** KEPT (pick-wt=10): 40 [copy,39,flip.1] equal(intersection(H(x),H(y)),H(intersection(x,y))).
---> New Demodulator: 41 [new_demod,40] equal(intersection(H(x),H(y)),H(intersection(x,y))).
** KEPT (pick-wt=7): 42 [] equal(H(P(x)),P(H(x))).
---> New Demodulator: 43 [new_demod,42] equal(H(P(x)),P(H(x))).
** KEPT (pick-wt=12): 44 [] -subclass(intersection(x,P(y)),y)|subclass(intersection(REGULAR,H(x)),y).
** KEPT (pick-wt=5): 46 [copy,45,demod,24,37] equal(H(x),H(x)).
** KEPT (pick-wt=11): 47 [] -member(x,y)| -subclass(tc(x),y)|member(x,H(y)).
>>>> Starting back demodulation with 5.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 10.
>>>> Starting back demodulation with 12.
>>>> Starting back demodulation with 15.
>>>> Starting back demodulation with 18.
>>>> Starting back demodulation with 21.
    >> back demodulating 13 with 21.
>>>> Starting back demodulation with 24.
    >> back demodulating 14 with 24.
>>>> Starting back demodulation with 30.
>>>> Starting back demodulation with 32.
>>>> Starting back demodulation with 34.
>>>> Starting back demodulation with 37.
>>>> Starting back demodulation with 41.
>>>> Starting back demodulation with 43.

======= end of input processing =======

=========== start of search ===========

Search stopped because sos empty.

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

list(usable).
3 [] subclass(x,x).
16 [] full(H(x)).
11 [] equal(H(OMEGA),OMEGA).
19 [] subclass(H(x),x).
29 [] equal(H(REGULAR),REGULAR).
46 [copy,45,demod,24,37] equal(H(x),H(x)).
9 [] equal(U(H(FULL)),H(FULL)).
17 [] equal(tc(H(x)),H(x)).
20 [] equal(intersection(REGULAR,H(FULL)),OMEGA).
28 [] -full(x)|equal(H(x),x).
31 [] equal(H(tc(x)),tc(x)).
33 [] equal(H(H(x)),H(x)).
7 [copy,6,flip.1] equal(intersection(FULL,P(FULL)),H(FULL)).
42 [] equal(H(P(x)),P(H(x))).
4 [] equal(U(intersection(FULL,P(x))),H(x)).
22 [] -subclass(x,H(y))|subclass(tc(x),y).
25 [] -member(x,H(y))|subclass(tc(x),y).
26 [] -subclass(x,y)|subclass(H(x),H(y)).
36 [] equal(intersection(x,P(H(x))),H(x)).
38 [] -subclass(tc(x),y)|subclass(x,H(y)).
23 [] equal(image(inverse(TC),P(x)),P(H(x))).
35 [] -full(x)| -subclass(x,y)|subclass(x,H(y)).
40 [copy,39,flip.1] equal(intersection(H(x),H(y)),H(intersection(x,y))).
47 [] -member(x,y)| -subclass(tc(x),y)|member(x,H(y)).
27 [] -member(x,H(A(y)))| -member(z,y)|member(x,H(z)).
44 [] -subclass(intersection(x,P(y)),y)|subclass(intersection(REGULAR,H(x)),y).
end_of_list.

list(sos).
end_of_list.

list(demodulators).
1 [] equal(intersection(x,y),intersection(y,x)).
2 [] equal(U(P(x)),x).
5 [new_demod,4] equal(U(intersection(FULL,P(x))),H(x)).
8 [new_demod,7] equal(intersection(FULL,P(FULL)),H(FULL)).
10 [new_demod,9] equal(U(H(FULL)),H(FULL)).
12 [new_demod,11] equal(H(OMEGA),OMEGA).
18 [new_demod,17] equal(tc(H(x)),H(x)).
21 [new_demod,20] equal(intersection(REGULAR,H(FULL)),OMEGA).
24 [new_demod,23] equal(image(inverse(TC),P(x)),P(H(x))).
30 [new_demod,29] equal(H(REGULAR),REGULAR).
32 [new_demod,31] equal(H(tc(x)),tc(x)).
34 [new_demod,33] equal(H(H(x)),H(x)).
37 [new_demod,36] equal(intersection(x,P(H(x))),H(x)).
41 [new_demod,40] equal(intersection(H(x),H(y)),H(intersection(x,y))).
43 [new_demod,42] equal(H(P(x)),P(H(x))).
end_of_list.


The job finished        Thu Apr 19 22:36:18 2001