----- Otter 3.3f, August 2004 ----- The process was started by frain on omega, Mon Mar 17 08:23:18 2008 The command was "otter". The process ID is 23973. set(auto). dependent: set(auto1). 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(input_sequent). set(output_sequent). WARNING: set(process_input) flag already set. set(process_input). set(build_proof_object_2). dependent: set(order_history). list(usable). 0 [] "P"(x1,x2) -> "Q"(x1,x2). 0 [] -> "P"(x3,x1). 0 [] "Q"(x3,x1) -> . end_of_list. SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=2. This is a Horn set without equality. The strategy will be hyperresolution, with satellites in sos and nuclei in usable. dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=6): 1 [] "P"(x,y) -> "Q"(x,y). ** KEPT (pick-wt=3): 2 [] "Q"(x,y) -> . ------------> process sos: ** KEPT (pick-wt=3): 3 [] -> "P"(x,y). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=3) 3 [] -> "P"(x,y). ----> UNIT CONFLICT at 0.01 sec ----> 5 [binary,4.1,2.1] -> . Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 1 [] "P"(x,y) -> "Q"(x,y). 2 [] "Q"(x,y) -> . 3 [] -> "P"(x,y). 4 [hyper,1,3.1] -> "Q"(x,y). 5 [binary,4.1,2.1] -> . ------------ end of proof ------------- ;; BEGINNING OF PROOF OBJECT ( (1 (input) (or (not ("P" v0 v1)) ("Q" v0 v1)) (1)) (2 (input) (not ("Q" v0 v1)) (2)) (3 (input) ("P" v0 v1) (3)) (4 (instantiate 1 ((v0 . v64)(v1 . v65))) (or (not ("P" v64 v65)) ("Q" v64 v65)) NIL) (5 (instantiate 3 ((v0 . v64)(v1 . v65))) ("P" v64 v65) NIL) (6 (resolve 4 (1) 5 ()) ("Q" v64 v65) NIL) (7 (instantiate 6 ((v64 . v0)(v65 . v1))) ("Q" v0 v1) (4)) (8 (instantiate 2 ((v0 . v64)(v1 . v65))) (not ("Q" v64 v65)) NIL) (9 (instantiate 7 ((v0 . v64)(v1 . v65))) ("Q" v64 v65) NIL) (10 (resolve 8 () 9 ()) false (5)) ) ;; END OF PROOF OBJECT 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 976 ----------- times (seconds) ----------- user CPU time 0.01 (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) That finishes the proof of the theorem. Process 23973 finished Mon Mar 17 08:23:18 2008