----- Otter 3.0.4, August 1995 ----- The job was started by Macintosh user on a Macintosh, Sun Feb 1 13:39:17 1998 The command was "OTTER 3.0.4". set(auto). 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). assign(max_seconds,60). formula_list(usable). Contains(b,apples). Label(a,apples). Label(b,oranges). Label(c,bananas). Contains(a,apples)|Contains(a,bananas)|Contains(a,oranges). Contains(b,apples)|Contains(b,bananas)|Contains(b,oranges). Contains(c,apples)|Contains(c,bananas)|Contains(c,oranges). all x y z (Contains(x,y)&z!=x-> -Contains(z,y)). a!=b&b!=c&a!=c. all x y (Label(x,y)-> -Contains(x,y)). -Contains(c,oranges). end_of_list. -------> usable clausifies to: list(usable). 0 [] Contains(b,apples). 0 [] Label(a,apples). 0 [] Label(b,oranges). 0 [] Label(c,bananas). 0 [] Contains(a,apples)|Contains(a,bananas)|Contains(a,oranges). 0 [] Contains(b,apples)|Contains(b,bananas)|Contains(b,oranges). 0 [] Contains(c,apples)|Contains(c,bananas)|Contains(c,oranges). 0 [] -Contains(x,y)|z=x| -Contains(z,y). 0 [] a!=b. 0 [] b!=c. 0 [] a!=c. 0 [] -Label(x,y)| -Contains(x,y). 0 [] -Contains(c,oranges). end_of_list. SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deleteion, 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: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=9): 1 [] -Contains(x,y)|z=x| -Contains(z,y). ** KEPT (pick-wt=3): 3 [copy,2,flip.1] b!=a. ** KEPT (pick-wt=3): 5 [copy,4,flip.1] c!=b. ** KEPT (pick-wt=3): 7 [copy,6,flip.1] c!=a. ** KEPT (pick-wt=6): 8 [] -Label(x,y)| -Contains(x,y). ** KEPT (pick-wt=3): 9 [] -Contains(c,oranges). ------------> process sos: ** KEPT (pick-wt=3): 11 [] Contains(b,apples). ** KEPT (pick-wt=3): 12 [] Label(a,apples). ** KEPT (pick-wt=3): 13 [] Label(b,oranges). ** KEPT (pick-wt=3): 14 [] Label(c,bananas). ** KEPT (pick-wt=9): 15 [] Contains(a,apples)|Contains(a,bananas)|Contains(a,oranges). Following clause subsumed by 11 during input processing: 0 [] Contains(b,apples)|Contains(b,bananas)|Contains(b,oranges). ** KEPT (pick-wt=6): 17 [copy,16,unit_del,9] Contains(c,apples)|Contains(c,bananas). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=3) 11 [] Contains(b,apples). given clause #2: (wt=3) 12 [] Label(a,apples). given clause #3: (wt=3) 13 [] Label(b,oranges). given clause #4: (wt=3) 14 [] Label(c,bananas). given clause #5: (wt=3) 18 [hyper,11,10] b=b. given clause #6: (wt=9) 15 [] Contains(a,apples)|Contains(a,bananas)|Contains(a,oranges). given clause #7: (wt=6) 17 [copy,16,unit_del,9] Contains(c,apples)|Contains(c,bananas). given clause #8: (wt=3) 32 [hyper,17,1,11,unit_del,5] Contains(c,bananas). -----> EMPTY CLAUSE at 0.22 sec ----> 36 [hyper,32,8,14] $F. Length of proof is 3. Level of proof is 2. ---------------- PROOF ---------------- 1 [] -Contains(x,y)|z=x| -Contains(z,y). 4 [] b!=c. 5 [copy,4,flip.1] c!=b. 8 [] -Label(x,y)| -Contains(x,y). 9 [] -Contains(c,oranges). 11 [] Contains(b,apples). 14 [] Label(c,bananas). 16 [] Contains(c,apples)|Contains(c,bananas)|Contains(c,oranges). 17 [copy,16,unit_del,9] Contains(c,apples)|Contains(c,bananas). 32 [hyper,17,1,11,unit_del,5] Contains(c,bananas). 36 [hyper,32,8,14] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 8 clauses generated 43 clauses kept 31 clauses forward subsumed 25 clauses back subsumed 5 Kbytes malloced 79 ----------- times (seconds) ----------- user CPU time 0.52 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 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.13 demod time 0.00 The job finished Sun Feb 1 13:39:17 1998