----- Otter 3.3f, August 2004 ----- The process was started by frain on omega, Mon Mar 17 08:11:26 2008 The command was "otter". The process ID is 23801. 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"("f"(x1),x1). 0 [] "P"("f"("f"(x2)),"f"(x2)), "P"("f"(x2),x2) -> "P"("f"("f"(x2)),x2). 0 [] "P"("f"("f"("f"("f"(x3)))),"f"("f"(x3))), "P"("f"("f"(x3)),x3) -> "P"("f"("f"("f"("f"(x3)))),x3). 0 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"(x4)))))))),"f"("f"("f"("f"(x4))))), "P"("f"("f"("f"("f"(x4)))),x4) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"(x4)))))))),x4). 0 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("a")))))))),"a") -> . end_of_list. SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3. 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=15): 1 [] "P"("f"("f"(x)),"f"(x)), "P"("f"(x),x) -> "P"("f"("f"(x)),x). ** KEPT (pick-wt=21): 2 [] "P"("f"("f"("f"("f"(x)))),"f"("f"(x))), "P"("f"("f"(x)),x) -> "P"("f"("f"("f"("f"(x)))),x). ** KEPT (pick-wt=33): 3 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),"f"("f"("f"("f"(x))))), "P"("f"("f"("f"("f"(x)))),x) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x). ** KEPT (pick-wt=11): 4 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("a")))))))),"a") -> . ------------> process sos: ** KEPT (pick-wt=4): 5 [] -> "P"("f"(x),x). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 5 [] -> "P"("f"(x),x). given clause #2: (wt=5) 6 [hyper,1,5.1,5.1] -> "P"("f"("f"(x)),x). given clause #3: (wt=7) 7 [hyper,2,6.1,6.1] -> "P"("f"("f"("f"("f"(x)))),x). ----> UNIT CONFLICT at 0.00 sec ----> 9 [binary,8.1,4.1] -> . Length of proof is 3. Level of proof is 3. ---------------- PROOF ---------------- 1 [] "P"("f"("f"(x)),"f"(x)), "P"("f"(x),x) -> "P"("f"("f"(x)),x). 2 [] "P"("f"("f"("f"("f"(x)))),"f"("f"(x))), "P"("f"("f"(x)),x) -> "P"("f"("f"("f"("f"(x)))),x). 3 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),"f"("f"("f"("f"(x))))), "P"("f"("f"("f"("f"(x)))),x) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x). 4 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("a")))))))),"a") -> . 5 [] -> "P"("f"(x),x). 6 [hyper,1,5.1,5.1] -> "P"("f"("f"(x)),x). 7 [hyper,2,6.1,6.1] -> "P"("f"("f"("f"("f"(x)))),x). 8 [hyper,3,7.1,7.1] -> "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x). 9 [binary,8.1,4.1] -> . ------------ end of proof ------------- ;; BEGINNING OF PROOF OBJECT ( (1 (input) (or (not ("P" ("f" ("f" v0)) ("f" v0))) (or (not ("P" ("f" v0) v0)) ("P" ("f" ("f" v0)) v0))) (1)) (2 (input) (or (not ("P" ("f" ("f" ("f" ("f" v0)))) ("f" ("f" v0)))) (or (not ("P" ("f" ("f" v0)) v0)) ("P" ("f" ("f" ("f" ("f" v0)))) v0))) (2)) (3 (input) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) ("f" ("f" ("f" ("f" v0)))))) (or (not ("P" ("f" ("f" ("f" ("f" v0)))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0))) (3)) (4 (input) (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("a"))))))))) ("a"))) (4)) (5 (input) ("P" ("f" v0) v0) (5)) (6 (instantiate 5 ((v0 . ("f" v0)))) ("P" ("f" ("f" v0)) ("f" v0)) NIL) (7 (resolve 1 (1) 6 ()) (or (not ("P" ("f" v0) v0)) ("P" ("f" ("f" v0)) v0)) NIL) (8 (instantiate 7 ((v0 . v64))) (or (not ("P" ("f" v64) v64)) ("P" ("f" ("f" v64)) v64)) NIL) (9 (instantiate 5 ((v0 . v64))) ("P" ("f" v64) v64) NIL) (10 (resolve 8 (1) 9 ()) ("P" ("f" ("f" v64)) v64) NIL) (11 (instantiate 10 ((v64 . v0))) ("P" ("f" ("f" v0)) v0) (6)) (12 (instantiate 11 ((v0 . ("f" ("f" v0))))) ("P" ("f" ("f" ("f" ("f" v0)))) ("f" ("f" v0))) NIL) (13 (resolve 2 (1) 12 ()) (or (not ("P" ("f" ("f" v0)) v0)) ("P" ("f" ("f" ("f" ("f" v0)))) v0)) NIL) (14 (instantiate 13 ((v0 . v64))) (or (not ("P" ("f" ("f" v64)) v64)) ("P" ("f" ("f" ("f" ("f" v64)))) v64)) NIL) (15 (instantiate 11 ((v0 . v64))) ("P" ("f" ("f" v64)) v64) NIL) (16 (resolve 14 (1) 15 ()) ("P" ("f" ("f" ("f" ("f" v64)))) v64) NIL) (17 (instantiate 16 ((v64 . v0))) ("P" ("f" ("f" ("f" ("f" v0)))) v0) (7)) (18 (instantiate 17 ((v0 . ("f" ("f" ("f" ("f" v0))))))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) ("f" ("f" ("f" ("f" v0))))) NIL) (19 (resolve 3 (1) 18 ()) (or (not ("P" ("f" ("f" ("f" ("f" v0)))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0)) NIL) (20 (instantiate 19 ((v0 . v64))) (or (not ("P" ("f" ("f" ("f" ("f" v64)))) v64)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))) v64)) NIL) (21 (instantiate 17 ((v0 . v64))) ("P" ("f" ("f" ("f" ("f" v64)))) v64) NIL) (22 (resolve 20 (1) 21 ()) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))) v64) NIL) (23 (instantiate 22 ((v64 . v0))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0) (8)) (24 (instantiate 23 ((v0 . ("a")))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("a"))))))))) ("a")) NIL) (25 (resolve 4 () 24 ()) false (9)) ) ;; END OF PROOF OBJECT Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 3 clauses generated 5 clauses kept 8 clauses forward subsumed 2 clauses back subsumed 2 Kbytes malloced 976 ----------- times (seconds) ----------- user CPU time 0.00 (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 23801 finished Mon Mar 17 08:11:26 2008