----- Otter 3.0.4, August 1995 ----- The job was started by Macintosh user on a Macintosh, Wed Feb 4 08:33:50 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). set(propositional). dependent: set(sort_literals). formula_list(usable). -((p->q)<-> (-q-> -p)). end_of_list. -------> usable clausifies to: list(usable). 0 [] -p|q. 0 [] p. 0 [] -q. end_of_list. SCAN INPUT: prop=1, horn=1, equality=0, symmetry=0, max_lits=2. The clause set is propositional; the strategy will be ordered hyperresolution with the propositional optimizations, with satellites in sos and nuclei in usable. dependent: set(hyper_res). ------------> process usable: ** KEPT (pick-wt=2): 1 [] -p|q. ** KEPT (pick-wt=1): 2 [] -q. ------------> process sos: ** KEPT (pick-wt=1): 3 [] p. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=1) 3 [] p. . ----> UNIT CONFLICT at 0.23 sec ----> 5 [binary,4.1,2.1] \$F. -------- PROOF -------- Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 1 [] -p|q. 2 [] -q. 3 [] p. 4 [hyper,3,1] q. 5 [binary,4.1,2.1] \$F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 1 clauses generated 1 clauses kept 4 clauses forward subsumed 0 clauses back subsumed 0 Kbytes malloced 55 ----------- times (seconds) ----------- user CPU time 0.75 (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 for_sub time 0.00 back_sub time 0.00 conflict time 0.22 demod time 0.00 The job finished Wed Feb 4 08:33:50 1998