----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Nov 30 13:22:32 1997
The command was "C:\BIN\OTTER95.EXE".

WARNING: clear(symbol_elim) flag already clear.
clear(symbol_elim).
set(order_eq).
set(sort_literals).
set(unit_deletion).
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([V,Id,union(x,x),cart(x,x),composite(x,x),restrict(x,x,x),intersection(x,x),compreln(x),complement(x),equal(x,x),member(x,x),subclass(x,x),disjoint(x,x)]).
assign(max_mem,300).
assign(stats_level,0).

formula_list(sos).
all x equal(restrict(complement(x),V,V),compreln(x)).
all w z (member(w,cart(V,V))& -member(w,z)->member(w,composite(Id,complement(z)))).
all x subclass(compreln(x),cart(V,V)).
all x disjoint(compreln(x),x).
all x subclass(compreln(x),complement(x)).
all x equal(compreln(restrict(x,V,V)),compreln(x)).
all x equal(compreln(compreln(x)),restrict(x,V,V)).
all x y equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))).
all x y equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))).
end_of_list.

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

list(sos).
0 [] equal(restrict(complement(x),V,V),compreln(x)).
0 [] -member(w,cart(V,V))|member(w,z)|member(w,composite(Id,complement(z))).
0 [] subclass(compreln(x),cart(V,V)).
0 [] disjoint(compreln(x),x).
0 [] subclass(compreln(x),complement(x)).
0 [] equal(compreln(restrict(x,V,V)),compreln(x)).
0 [] equal(compreln(compreln(x)),restrict(x,V,V)).
0 [] equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))).
0 [] equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))).
end_of_list.

------------> process usable:

------------> process sos:
** KEPT (pick-wt=8): 1 [] equal(restrict(complement(x),V,V),compreln(x)).
---> New Demodulator: 2 [new_demod,1] equal(restrict(complement(x),V,V),compreln(x)).
** KEPT (pick-wt=14): 3 [] -member(x,cart(V,V))|member(x,y)|member(x,composite(Id,complement(y))).
** KEPT (pick-wt=6): 4 [] subclass(compreln(x),cart(V,V)).
** KEPT (pick-wt=4): 5 [] disjoint(compreln(x),x).
** KEPT (pick-wt=5): 6 [] subclass(compreln(x),complement(x)).
** KEPT (pick-wt=8): 7 [] equal(compreln(restrict(x,V,V)),compreln(x)).
---> New Demodulator: 8 [new_demod,7] equal(compreln(restrict(x,V,V)),compreln(x)).
** KEPT (pick-wt=8): 9 [] equal(compreln(compreln(x)),restrict(x,V,V)).
---> New Demodulator: 10 [new_demod,9] equal(compreln(compreln(x)),restrict(x,V,V)).
** KEPT (pick-wt=10): 11 [] equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))).
---> New Demodulator: 12 [new_demod,11] equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))).
** KEPT (pick-wt=10): 13 [] equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))).
---> New Demodulator: 14 [new_demod,13] equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))).
>>>> Starting back demodulation with 2.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 10.
>>>> Starting back demodulation with 12.
>>>> Starting back demodulation with 14.

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

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

Search stopped because sos empty.

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

list(usable).
5 [] disjoint(compreln(x),x).
6 [] subclass(compreln(x),complement(x)).
4 [] subclass(compreln(x),cart(V,V)).
1 [] equal(restrict(complement(x),V,V),compreln(x)).
7 [] equal(compreln(restrict(x,V,V)),compreln(x)).
9 [] equal(compreln(compreln(x)),restrict(x,V,V)).
11 [] equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))).
13 [] equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))).
3 [] -member(x,cart(V,V))|member(x,y)|member(x,composite(Id,complement(y))).
end_of_list.

list(sos).
end_of_list.

list(demodulators).
2 [new_demod,1] equal(restrict(complement(x),V,V),compreln(x)).
8 [new_demod,7] equal(compreln(restrict(x,V,V)),compreln(x)).
10 [new_demod,9] equal(compreln(compreln(x)),restrict(x,V,V)).
12 [new_demod,11] equal(compreln(union(x,y)),intersection(compreln(x),compreln(y))).
14 [new_demod,13] equal(compreln(intersection(x,y)),union(compreln(x),compreln(y))).
end_of_list.


The job finished        Sun Nov 30 13:22:32 1997