----- Otter 3.3f, August 2004 ----- The process was started by frain on omega, Mon Mar 17 08:12:51 2008 The command was "otter". The process ID is 23822. 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"("f"("f"("f"("f"("f"("f"("f"("f"(x5)))))))))))))))),"f"("f"("f"("f"("f"("f"("f"("f"(x5))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"(x5)))))))),x5) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x5)))))))))))))))),x5). 0 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6)))))))))))))))))))))))))))))))),"f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6))))))))))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6)))))))))))))))),x6) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6)))))))))))))))))))))))))))))))),x6). 0 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("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=57): 4 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),"f"("f"("f"("f"("f"("f"("f"("f"(x))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),x). ** KEPT (pick-wt=105): 5 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))))))))))))))))))),"f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x))))))))))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),x) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))))))))))))))))))),x). ** KEPT (pick-wt=35): 6 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("a")))))))))))))))))))))))))))))))),"a") -> . ------------> process sos: ** KEPT (pick-wt=4): 7 [] -> "P"("f"(x),x). ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=4) 7 [] -> "P"("f"(x),x). given clause #2: (wt=5) 8 [hyper,1,7.1,7.1] -> "P"("f"("f"(x)),x). given clause #3: (wt=7) 9 [hyper,2,8.1,8.1] -> "P"("f"("f"("f"("f"(x)))),x). given clause #4: (wt=11) 10 [hyper,3,9.1,9.1] -> "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x). given clause #5: (wt=19) 11 [hyper,4,10.1,10.1] -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),x). ----> UNIT CONFLICT at 0.00 sec ----> 13 [binary,12.1,6.1] -> . Length of proof is 5. Level of proof is 5. ---------------- 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"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),"f"("f"("f"("f"("f"("f"("f"("f"(x))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),x). 5 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))))))))))))))))))),"f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x))))))))))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),x) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))))))))))))))))))),x). 6 [] "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("a")))))))))))))))))))))))))))))))),"a") -> . 7 [] -> "P"("f"(x),x). 8 [hyper,1,7.1,7.1] -> "P"("f"("f"(x)),x). 9 [hyper,2,8.1,8.1] -> "P"("f"("f"("f"("f"(x)))),x). 10 [hyper,3,9.1,9.1] -> "P"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))),x). 11 [hyper,4,10.1,10.1] -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))),x). 12 [hyper,5,11.1,11.1] -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x)))))))))))))))))))))))))))))))),x). 13 [binary,12.1,6.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) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) v0))) (4)) (5 (input) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))))))))))))))))))) ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))))) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))))))))))))))))))) v0))) (5)) (6 (input) (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("a"))))))))))))))))))))))))))))))))) ("a"))) (6)) (7 (input) ("P" ("f" v0) v0) (7)) (8 (instantiate 7 ((v0 . ("f" v0)))) ("P" ("f" ("f" v0)) ("f" v0)) NIL) (9 (resolve 1 (1) 8 ()) (or (not ("P" ("f" v0) v0)) ("P" ("f" ("f" v0)) v0)) NIL) (10 (instantiate 9 ((v0 . v64))) (or (not ("P" ("f" v64) v64)) ("P" ("f" ("f" v64)) v64)) NIL) (11 (instantiate 7 ((v0 . v64))) ("P" ("f" v64) v64) NIL) (12 (resolve 10 (1) 11 ()) ("P" ("f" ("f" v64)) v64) NIL) (13 (instantiate 12 ((v64 . v0))) ("P" ("f" ("f" v0)) v0) (8)) (14 (instantiate 13 ((v0 . ("f" ("f" v0))))) ("P" ("f" ("f" ("f" ("f" v0)))) ("f" ("f" v0))) NIL) (15 (resolve 2 (1) 14 ()) (or (not ("P" ("f" ("f" v0)) v0)) ("P" ("f" ("f" ("f" ("f" v0)))) v0)) NIL) (16 (instantiate 15 ((v0 . v64))) (or (not ("P" ("f" ("f" v64)) v64)) ("P" ("f" ("f" ("f" ("f" v64)))) v64)) NIL) (17 (instantiate 13 ((v0 . v64))) ("P" ("f" ("f" v64)) v64) NIL) (18 (resolve 16 (1) 17 ()) ("P" ("f" ("f" ("f" ("f" v64)))) v64) NIL) (19 (instantiate 18 ((v64 . v0))) ("P" ("f" ("f" ("f" ("f" v0)))) v0) (9)) (20 (instantiate 19 ((v0 . ("f" ("f" ("f" ("f" v0))))))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) ("f" ("f" ("f" ("f" v0))))) NIL) (21 (resolve 3 (1) 20 ()) (or (not ("P" ("f" ("f" ("f" ("f" v0)))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0)) NIL) (22 (instantiate 21 ((v0 . v64))) (or (not ("P" ("f" ("f" ("f" ("f" v64)))) v64)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))) v64)) NIL) (23 (instantiate 19 ((v0 . v64))) ("P" ("f" ("f" ("f" ("f" v64)))) v64) NIL) (24 (resolve 22 (1) 23 ()) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))) v64) NIL) (25 (instantiate 24 ((v64 . v0))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0) (10)) (26 (instantiate 25 ((v0 . ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0))))))))))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0))))))))) NIL) (27 (resolve 4 (1) 26 ()) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) v0)) NIL) (28 (instantiate 27 ((v0 . v64))) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))) v64)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))))))))))) v64)) NIL) (29 (instantiate 25 ((v0 . v64))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))) v64) NIL) (30 (resolve 28 (1) 29 ()) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))))))))))) v64) NIL) (31 (instantiate 30 ((v64 . v0))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) v0) (11)) (32 (instantiate 31 ((v0 . ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0))))))))))))))))))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))))))))))))))))))) ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0))))))))))))))))) NIL) (33 (resolve 5 (1) 32 ()) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))) v0)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))))))))))))))))))) v0)) NIL) (34 (instantiate 33 ((v0 . v64))) (or (not ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))))))))))) v64)) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))))))))))))))))))))))))))) v64)) NIL) (35 (instantiate 31 ((v0 . v64))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))))))))))) v64) NIL) (36 (resolve 34 (1) 35 ()) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v64)))))))))))))))))))))))))))))))) v64) NIL) (37 (instantiate 36 ((v64 . v0))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" v0)))))))))))))))))))))))))))))))) v0) (12)) (38 (instantiate 37 ((v0 . ("a")))) ("P" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("f" ("a"))))))))))))))))))))))))))))))))) ("a")) NIL) (39 (resolve 6 () 38 ()) false (13)) ) ;; END OF PROOF OBJECT Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 5 clauses generated 9 clauses kept 12 clauses forward subsumed 4 clauses back subsumed 4 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 23822 finished Mon Mar 17 08:12:51 2008