----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Mon Jun 12 12:36:22 2000 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([0,id(x),Id,omega,FINITE,DEDEKIND,Q,pair(x,x),singleton(x),cart(x,x),intersection(x,x),complement(x),fix(x),D(x),R(x),image(x,x),composite(x,x),K,PS,inverse(x),ONEONE(x),equal(x,x),member(x,x),subclass(x,x)]). assign(max_mem,300). assign(stats_level,0). list(usable). 0 [] subclass(x,x). 0 [] equal(x,x). 0 [] disjoint(x,complement(x)). 0 [] subclass(id(x),Id). end_of_list. formula_list(sos). equal(complement(fix(composite(Q,PS))),DEDEKIND). -member(omega,DEDEKIND). equal(fix(composite(Q,PS)),complement(DEDEKIND)). all x y (member(x,DEDEKIND)&member(pair(x,y),Q)&subclass(x,y)->equal(x,y)). all x y (member(x,DEDEKIND)&member(pair(x,y),Q)&subclass(y,x)->equal(x,y)). all x (ONEONE(x)&subclass(R(x),D(x))&member(D(x),DEDEKIND)->equal(R(x),D(x))). subclass(image(K,DEDEKIND),DEDEKIND). subclass(image(inverse(K),DEDEKIND),DEDEKIND). equal(image(Q,DEDEKIND),DEDEKIND). member(0,DEDEKIND). subclass(FINITE,DEDEKIND). subclass(intersection(Q,cart(omega,omega)),Id). equal(intersection(Q,cart(omega,omega)),id(omega)). all x member(singleton(x),DEDEKIND). end_of_list. -------> sos clausifies to: list(sos). 0 [] equal(complement(fix(composite(Q,PS))),DEDEKIND). 0 [] -member(omega,DEDEKIND). 0 [] equal(fix(composite(Q,PS)),complement(DEDEKIND)). 0 [] -member(x,DEDEKIND)| -member(pair(x,y),Q)| -subclass(x,y)|equal(x,y). 0 [] -member(x,DEDEKIND)| -member(pair(x,y),Q)| -subclass(y,x)|equal(x,y). 0 [] -ONEONE(x)| -subclass(R(x),D(x))| -member(D(x),DEDEKIND)|equal(R(x),D(x)). 0 [] subclass(image(K,DEDEKIND),DEDEKIND). 0 [] subclass(image(inverse(K),DEDEKIND),DEDEKIND). 0 [] equal(image(Q,DEDEKIND),DEDEKIND). 0 [] member(0,DEDEKIND). 0 [] subclass(FINITE,DEDEKIND). 0 [] subclass(intersection(Q,cart(omega,omega)),Id). 0 [] equal(intersection(Q,cart(omega,omega)),id(omega)). 0 [] member(singleton(x),DEDEKIND). end_of_list. list(demodulators). 1 [] equal(intersection(x,y),intersection(y,x)). 2 [] equal(complement(complement(x)),x). 3 [] equal(union(x,y),union(y,x)). end_of_list. LRPO dependent demodulator: 1 [] equal(intersection(x,y),intersection(y,x)). LRPO dependent demodulator: 3 [] equal(union(x,y),union(y,x)). ------------> process usable: ** KEPT (pick-wt=3): 4 [] subclass(x,x). ** KEPT (pick-wt=3): 5 [] equal(x,x). ** KEPT (pick-wt=4): 6 [] disjoint(x,complement(x)). ** KEPT (pick-wt=4): 7 [] subclass(id(x),Id). ------------> process sos: ** KEPT (pick-wt=7): 8 [] equal(complement(fix(composite(Q,PS))),DEDEKIND). ---> New Demodulator: 9 [new_demod,8] equal(complement(fix(composite(Q,PS))),DEDEKIND). ** KEPT (pick-wt=3): 10 [] -member(omega,DEDEKIND). ** KEPT (pick-wt=7): 11 [] equal(fix(composite(Q,PS)),complement(DEDEKIND)). ---> New Demodulator: 12 [new_demod,11] equal(fix(composite(Q,PS)),complement(DEDEKIND)). ** KEPT (pick-wt=14): 13 [] -member(x,DEDEKIND)| -member(pair(x,y),Q)| -subclass(x,y)|equal(x,y). ** KEPT (pick-wt=14): 14 [] -member(x,DEDEKIND)| -member(pair(x,y),Q)| -subclass(y,x)|equal(x,y). ** KEPT (pick-wt=16): 15 [] -ONEONE(x)| -member(D(x),DEDEKIND)| -subclass(R(x),D(x))|equal(R(x),D(x)). ** KEPT (pick-wt=5): 16 [] subclass(image(K,DEDEKIND),DEDEKIND). ** KEPT (pick-wt=6): 17 [] subclass(image(inverse(K),DEDEKIND),DEDEKIND). ** KEPT (pick-wt=5): 18 [] equal(image(Q,DEDEKIND),DEDEKIND). ---> New Demodulator: 19 [new_demod,18] equal(image(Q,DEDEKIND),DEDEKIND). ** KEPT (pick-wt=3): 20 [] member(0,DEDEKIND). ** KEPT (pick-wt=3): 21 [] subclass(FINITE,DEDEKIND). ** KEPT (pick-wt=7): 22 [] subclass(intersection(Q,cart(omega,omega)),Id). ** KEPT (pick-wt=8): 23 [] equal(intersection(Q,cart(omega,omega)),id(omega)). ---> New Demodulator: 24 [new_demod,23] equal(intersection(Q,cart(omega,omega)),id(omega)). ** KEPT (pick-wt=4): 25 [] member(singleton(x),DEDEKIND). >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 12. >> back demodulating 8 with 12. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 24. >> back demodulating 22 with 24. ======= end of input processing ======= =========== start of search =========== Search stopped because sos empty. ============ end of search ============ list(usable). 4 [] subclass(x,x). 5 [] equal(x,x). 6 [] disjoint(x,complement(x)). 7 [] subclass(id(x),Id). 10 [] -member(omega,DEDEKIND). 20 [] member(0,DEDEKIND). 21 [] subclass(FINITE,DEDEKIND). 25 [] member(singleton(x),DEDEKIND). 16 [] subclass(image(K,DEDEKIND),DEDEKIND). 18 [] equal(image(Q,DEDEKIND),DEDEKIND). 17 [] subclass(image(inverse(K),DEDEKIND),DEDEKIND). 11 [] equal(fix(composite(Q,PS)),complement(DEDEKIND)). 23 [] equal(intersection(Q,cart(omega,omega)),id(omega)). 13 [] -member(x,DEDEKIND)| -member(pair(x,y),Q)| -subclass(x,y)|equal(x,y). 14 [] -member(x,DEDEKIND)| -member(pair(x,y),Q)| -subclass(y,x)|equal(x,y). 15 [] -ONEONE(x)| -member(D(x),DEDEKIND)| -subclass(R(x),D(x))|equal(R(x),D(x)). end_of_list. list(sos). end_of_list. list(demodulators). 1 [] equal(intersection(x,y),intersection(y,x)). 2 [] equal(complement(complement(x)),x). 3 [] equal(union(x,y),union(y,x)). 12 [new_demod,11] equal(fix(composite(Q,PS)),complement(DEDEKIND)). 19 [new_demod,18] equal(image(Q,DEDEKIND),DEDEKIND). 24 [new_demod,23] equal(intersection(Q,cart(omega,omega)),id(omega)). end_of_list. The job finished Mon Jun 12 12:36:22 2000