problem-set/puzzles/miscell/steamroller.ver2.out created : 07/07/88 revised : 07/07/88 OTTER release 0.9, 19 May 1988 set(UR_res). list(axioms). 1 -Smaller(animal(x3),animal(x1)) | -eats(animal(x3),plant(x4)) | eats(animal(x1),plant(x2)) | eats(animal(x1),animal(x3)). 2 -eats(animal(x),animal(y)) | -eats(animal(y),plant(Grain(z))). 3 -eats(animal(Wolf(x1)),animal(Fox(x2))). 4 -eats(animal(Wolf(x1)),plant(Grain(x2))). 5 -eats(animal(Bird(x1)),animal(Snail(x2))). 6 eats(animal(Bird(x1)),animal(Caterpillar(x2))). 7 eats(animal(Caterpillar(x1)),plant(p1(animal(Caterpillar(x1))))). 8 eats(animal(Snail(x1)),plant(p2(animal(Snail(x1))))). end_of_list. list(sos). 9 Smaller(animal(Caterpillar(x1)),animal(Bird(x2))). 10 Smaller(animal(Snail(x1)),animal(Bird(x2))). 11 Smaller(animal(Bird(x1)),animal(Fox(x2))). 12 Smaller(animal(Fox(x1)),animal(Wolf(x2))). 13 Grain(Stalky). end_of_list. ---------------- PROOF ---------------- 1 -Smaller(animal(x3),animal(x1)) | -eats(animal(x3),plant(x4)) | eats(animal(x1),plant(x2)) | eats(animal(x1),animal(x3)). 2 -eats(animal(x),animal(y)) | -eats(animal(y),plant(Grain(z))). 3 -eats(animal(Wolf(x1)),animal(Fox(x2))). 4 -eats(animal(Wolf(x1)),plant(Grain(x2))). 5 -eats(animal(Bird(x1)),animal(Snail(x2))). 8 eats(animal(Snail(x1)),plant(p2(animal(Snail(x1))))). 10 Smaller(animal(Snail(x1)),animal(Bird(x2))). 11 Smaller(animal(Bird(x1)),animal(Fox(x2))). 12 Smaller(animal(Fox(x1)),animal(Wolf(x2))). 14 (10,1,8,5) eats(animal(Bird(x)),plant(y)). 15 (14,2) -eats(animal(x),animal(Bird(y))). 17 (11,1,14,15) eats(animal(Fox(x)),plant(y)). 19 (17,1,4,3) -Smaller(animal(Fox(x)),animal(Wolf(y))). 20 (19,12) . --------------- options --------------- set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 13 clauses given 7 clauses generated 7 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 0 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 7 empty clauses 1 factors generated 0 clauses back subsumed 1 clauses not processed 3 ----------- times (seconds) ----------- run time 0.48 input time 0.19 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.08 para_into time 0.00 para_from time 0.00 pre_process time 0.04 demod time 0.00 weigh time 0.00 for_sub time 0.01 unit_del time 0.00 post_process time 0.03 back_sub time 0.01 conflict time 0.01 factor time 0.00 FPA build time 0.03 IS build time 0.01 print_cl time 0.11 cl integrate time 0.02 window time 0.00