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