problem-set/puzzles/carroll/letters.ver1.out created : 07/19/88 revised : 07/19/88 OTTER version 0.91, 14 June 1988. set(hyper_res). set(UR_res). set(binary_res). list(sos). 1 -DATED | ON_BLUE_PAPER. 2 -IN_THIRD_PERSON | IN_BLACK_INK. 3 IN_THIRD_PERSON | -IN_BLACK_INK. 4 -CAN_BE_READ | -FILED. 5 -ON_ONE_SHEET | DATED. 6 CROSSED | IN_BLACK_INK. 7 -BY_BROWN | BEGINS_WITH_DEAR_SIR. 8 -ON_BLUE_PAPER | FILED. 9 ON_ONE_SHEET | -CROSSED. 10 -BEGINS_WITH_DEAR_SIR | -IN_THIRD_PERSON. end_of_list. new given clause: 1 -DATED | ON_BLUE_PAPER. new given clause: 2 -IN_THIRD_PERSON | IN_BLACK_INK. new given clause: 3 IN_THIRD_PERSON | -IN_BLACK_INK. new given clause: 4 -CAN_BE_READ | -FILED. new given clause: 5 -ON_ONE_SHEET | DATED. ** KEPT: 11 (5,1) -ON_ONE_SHEET | ON_BLUE_PAPER. new given clause: 6 CROSSED | IN_BLACK_INK. ** KEPT: 12 (6,3) CROSSED | IN_THIRD_PERSON. new given clause: 7 -BY_BROWN | BEGINS_WITH_DEAR_SIR. new given clause: 8 -ON_BLUE_PAPER | FILED. ** KEPT: 13 (8,1) FILED | -DATED. ** KEPT: 14 (8,4) -ON_BLUE_PAPER | -CAN_BE_READ. new given clause: 9 ON_ONE_SHEET | -CROSSED. ** KEPT: 15 (9,5) -CROSSED | DATED. ** KEPT: 16 (9,6) ON_ONE_SHEET | IN_BLACK_INK. new given clause: 10 -BEGINS_WITH_DEAR_SIR | -IN_THIRD_PERSON. ** KEPT: 17 (10,7) -IN_THIRD_PERSON | -BY_BROWN. ** KEPT: 18 (10,3) -BEGINS_WITH_DEAR_SIR | -IN_BLACK_INK. new given clause: 11 (5,1) -ON_ONE_SHEET | ON_BLUE_PAPER. ** KEPT: 19 (11,9) ON_BLUE_PAPER | -CROSSED. ** KEPT: 20 (11,8) -ON_ONE_SHEET | FILED. new given clause: 12 (6,3) CROSSED | IN_THIRD_PERSON. ** KEPT: 21 (12,9) IN_THIRD_PERSON | ON_ONE_SHEET. ** KEPT: 22 (12,10) CROSSED | -BEGINS_WITH_DEAR_SIR. new given clause: 13 (8,1) FILED | -DATED. ** KEPT: 23 (13,4) -DATED | -CAN_BE_READ. new given clause: 14 (8,4) -ON_BLUE_PAPER | -CAN_BE_READ. ** KEPT: 24 (14,11) -CAN_BE_READ | -ON_ONE_SHEET. new given clause: 15 (9,5) -CROSSED | DATED. ** KEPT: 25 (15,12) DATED | IN_THIRD_PERSON. ** KEPT: 26 (15,6) DATED | IN_BLACK_INK. ** KEPT: 27 (15,13) -CROSSED | FILED. new given clause: 16 (9,6) ON_ONE_SHEET | IN_BLACK_INK. ** KEPT: 28 (16,11) IN_BLACK_INK | ON_BLUE_PAPER. new given clause: 17 (10,7) -IN_THIRD_PERSON | -BY_BROWN. ** KEPT: 29 (17,12) -BY_BROWN | CROSSED. ** KEPT: 30 (17,3) -BY_BROWN | -IN_BLACK_INK. new given clause: 18 (10,3) -BEGINS_WITH_DEAR_SIR | -IN_BLACK_INK. ** KEPT: 31 (18,16) -BEGINS_WITH_DEAR_SIR | ON_ONE_SHEET. new given clause: 19 (11,9) ON_BLUE_PAPER | -CROSSED. ** KEPT: 32 (19,14) -CROSSED | -CAN_BE_READ. ** KEPT: 33 (19,12) ON_BLUE_PAPER | IN_THIRD_PERSON. new given clause: 20 (11,8) -ON_ONE_SHEET | FILED. ** KEPT: 34 (20,16) FILED | IN_BLACK_INK. new given clause: 21 (12,9) IN_THIRD_PERSON | ON_ONE_SHEET. ** KEPT: 35 (21,17) ON_ONE_SHEET | -BY_BROWN. ** KEPT: 36 (21,20) IN_THIRD_PERSON | FILED. new given clause: 22 (12,10) CROSSED | -BEGINS_WITH_DEAR_SIR. ** KEPT: 37 (22,19) -BEGINS_WITH_DEAR_SIR | ON_BLUE_PAPER. ** KEPT: 38 (22,15) -BEGINS_WITH_DEAR_SIR | DATED. new given clause: 23 (13,4) -DATED | -CAN_BE_READ. new given clause: 24 (14,11) -CAN_BE_READ | -ON_ONE_SHEET. ** KEPT: 39 (24,21) -CAN_BE_READ | IN_THIRD_PERSON. ** KEPT: 40 (24,16) -CAN_BE_READ | IN_BLACK_INK. new given clause: 25 (15,12) DATED | IN_THIRD_PERSON. ** KEPT: 41 (25,17) DATED | -BY_BROWN. new given clause: 26 (15,6) DATED | IN_BLACK_INK. new given clause: 27 (15,13) -CROSSED | FILED. ** KEPT: 42 (27,22) FILED | -BEGINS_WITH_DEAR_SIR. new given clause: 28 (16,11) IN_BLACK_INK | ON_BLUE_PAPER. new given clause: 29 (17,12) -BY_BROWN | CROSSED. ** KEPT: 43 (29,27) -BY_BROWN | FILED. ** KEPT: 44 (29,19) -BY_BROWN | ON_BLUE_PAPER. new given clause: 30 (17,3) -BY_BROWN | -IN_BLACK_INK. new given clause: 31 (18,16) -BEGINS_WITH_DEAR_SIR | ON_ONE_SHEET. ** KEPT: 45 (31,24) -BEGINS_WITH_DEAR_SIR | -CAN_BE_READ. new given clause: 32 (19,14) -CROSSED | -CAN_BE_READ. ** KEPT: 46 (32,29) -CAN_BE_READ | -BY_BROWN. new given clause: 33 (19,12) ON_BLUE_PAPER | IN_THIRD_PERSON. new given clause: 34 (20,16) FILED | IN_BLACK_INK. new given clause: 35 (21,17) ON_ONE_SHEET | -BY_BROWN. new given clause: 36 (21,20) IN_THIRD_PERSON | FILED. new given clause: 37 (22,19) -BEGINS_WITH_DEAR_SIR | ON_BLUE_PAPER. new given clause: 38 (22,15) -BEGINS_WITH_DEAR_SIR | DATED. new given clause: 39 (24,21) -CAN_BE_READ | IN_THIRD_PERSON. new given clause: 40 (24,16) -CAN_BE_READ | IN_BLACK_INK. new given clause: 41 (25,17) DATED | -BY_BROWN. new given clause: 42 (27,22) FILED | -BEGINS_WITH_DEAR_SIR. new given clause: 43 (29,27) -BY_BROWN | FILED. new given clause: 44 (29,19) -BY_BROWN | ON_BLUE_PAPER. new given clause: 45 (31,24) -BEGINS_WITH_DEAR_SIR | -CAN_BE_READ. new given clause: 46 (32,29) -CAN_BE_READ | -BY_BROWN. ------------ END OF SEARCH ------------ sos empty. --------------- options --------------- set(binary_res). set(hyper_res). 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(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). clear(order_eq). 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, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 10 clauses given 46 clauses generated 160 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 2 clauses forward subsumed 122 (clauses subsumed by sos) 106 unit deletions 0 clauses kept 36 empty clauses 0 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 0.88 input time 0.07 binary_res time 0.08 hyper_res time 0.06 UR_res time 0.04 para_into time 0.00 para_from time 0.00 pre_process time 0.30 demod time 0.00 weigh time 0.01 for_sub time 0.10 unit_del time 0.00 post_process time 0.05 back_sub time 0.03 conflict time 0.00 factor time 0.00 FPA build time 0.04 IS build time 0.02 print_cl time 0.14 cl integrate time 0.01 window time 0.00