WATCH: 0.00 CPU 0.01 WC
----- Otter 3.3f, August 2004 -----
The process was started by sutcliff on cl5-020,
Wed Aug  3 13:45:15 2011
The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter".  The process ID is 17123.

set(prolog_style_variables).
set(tptp_eq).
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).
clear(print_given).

formula_list(usable).
-(-((all P Q (-a_truth(P)|a_truth(Q)| -a_truth(implies(P,Q))))& (all P Q a_truth(implies(P,implies(Q,P))))& (exists A (-a_truth(implies(A,A))))& (all P Q a_truth(implies(implies(not(P),not(Q)),implies(Q,P))))& (all P Q R a_truth(implies(implies(P,implies(Q,R)),implies(implies(P,Q),implies(P,R))))))).
end_of_list.

-------> usable clausifies to:

list(usable).
0 [] -a_truth(P)|a_truth(Q)| -a_truth(implies(P,Q)).
0 [] a_truth(implies(X1,implies(X2,X1))).
0 [] -a_truth(implies($c1,$c1)).
0 [] a_truth(implies(implies(not(X3),not(X4)),implies(X4,X3))).
0 [] a_truth(implies(implies(X5,implies(X6,R)),implies(implies(X5,X6),implies(X5,R)))).
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=8): 1 [] -a_truth(A)|a_truth(B)| -a_truth(implies(A,B)).
** KEPT (pick-wt=4): 2 [] -a_truth(implies($c1,$c1)).

------------> process sos:
** KEPT (pick-wt=6): 3 [] a_truth(implies(A,implies(B,A))).
** KEPT (pick-wt=10): 4 [] a_truth(implies(implies(not(A),not(B)),implies(B,A))).
** KEPT (pick-wt=14): 5 [] a_truth(implies(implies(A,implies(B,C)),implies(implies(A,B),implies(A,C)))).

======= end of input processing =======

=========== start of search ===========

-------- PROOF -------- 

----> UNIT CONFLICT at   0.00 sec ----> 19 [binary,18.1,2.1] $F.

Length of proof is 3.  Level of proof is 2.

---------------- PROOF ----------------

1 [] -a_truth(A)|a_truth(B)| -a_truth(implies(A,B)).
2 [] -a_truth(implies($c1,$c1)).
3 [] a_truth(implies(A,implies(B,A))).
4 [] a_truth(implies(implies(not(A),not(B)),implies(B,A))).
5 [] a_truth(implies(implies(A,implies(B,C)),implies(implies(A,B),implies(A,C)))).
8 [hyper,4,1,3] a_truth(implies(A,implies(implies(not(B),not(C)),implies(C,B)))).
15 [hyper,5,1,3] a_truth(implies(implies(A,B),implies(A,A))).
18 [hyper,15,1,8] a_truth(implies(A,A)).
19 [binary,18.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                  7
clauses generated             37
clauses kept                  18
clauses forward subsumed      24
clauses back subsumed          0
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 17123 finished Wed Aug  3 13:45:15 2011
Otter interrupted
PROOF FOUND

WATCH: 0.27 CPU 0.36 WC

FINAL WATCH: 0.27 CPU 0.36 WC