Online Otter-λ
-->
Examples
----- Otter-lambda 1.4 July 2006 -----
----- Based on Otter 3.2 August 2001-----
The command was "otter2".
set(lambda).
set(binary_res).
dependent: set(factor).
dependent: set(unit_deletion).
set(demod_inf).
set(para_into).
set(para_from).
set(para_from_units_only).
set(process_input).
assign(max_distinct_vars,3).
assign(max_weight,24).
assign(pick_given_ratio,4).
assign(bsub_hint_wt,1).
weight_list(pick_and_purge).
weight(junk,50).
weight(g($(0)),1).
end_of_list.
list(usable).
0 [] u!=v|v=u.
0 [] Set(p).
0 [] Set(q).
0 [] Set(r).
0 [] -Set(x)|Prop(Ap(x,y)).
0 [] Set(x)| -Prop(Ap(x,c(x))).
end_of_list.
list(demodulators).
1 [] in(x,y)=Ap(y,x).
2 [] not($T)=$F.
3 [] j=lambda(u,lambda(v,lambda(x,and(in(x,u),in(x,v))))).
4 [] i=lambda(u,lambda(v,lambda(x,or(in(x,u),in(x,v))))).
5 [] or(x,and(y,z))=and(or(x,y),or(x,z)).
end_of_list.
list(sos).
0 [] x=x.
0 [] Ap(Ap(i,p),Ap(Ap(j,q),r))!=Ap(Ap(j,Ap(Ap(i,p),q)),Ap(Ap(i,p),r)).
end_of_list.
------------> process usable:
** KEPT (pick-wt=6): 6 [] x!=y|y=x.
** KEPT (pick-wt=2): 7 [] Set(p).
** KEPT (pick-wt=2): 8 [] Set(q).
** KEPT (pick-wt=2): 9 [] Set(r).
** KEPT (pick-wt=6): 10 [] -Set(x)|Prop(Ap(x,y)).
** KEPT (pick-wt=7): 11 [] Set(x)| -Prop(Ap(x,c(x))).
------------> process sos:
** KEPT (pick-wt=3): 12 [] x=x.
** KEPT (pick-wt=35): 14 [copy,13,demod,4,1,1,beta,3,1,1,beta,beta,beta,beta,5,3,1,1,4,1,1,beta,beta,beta,beta,4,1,1,beta,beta,beta,beta] lambda(x,and(or(Ap(p,x),Ap(q,x)),or(Ap(p,x),Ap(r,x))))!=lambda(y,and(or(Ap(p,y),Ap(q,y)),or(Ap(p,y),Ap(r,y)))).
----> UNIT CONFLICT at 0.00 sec ----> 15 [binary,14.1,12.1] $F.
Length of proof is 1. Level of proof is 1.
---------------- PROOF ----------------
1 [] in(x,y)=Ap(y,x).
3 [] j=lambda(u,lambda(v,lambda(x,and(in(x,u),in(x,v))))).
4 [] i=lambda(u,lambda(v,lambda(x,or(in(x,u),in(x,v))))).
5 [] or(x,and(y,z))=and(or(x,y),or(x,z)).
12 [] x=x.
13 [] Ap(Ap(i,p),Ap(Ap(j,q),r))!=Ap(Ap(j,Ap(Ap(i,p),q)),Ap(Ap(i,p),r)).
14 [copy,13,demod,4,1,1,beta,3,1,1,beta,beta,beta,beta,5,3,1,1,4,1,1,beta,beta,beta,beta,4,1,1,beta,beta,beta,beta] lambda(x,and(or(Ap(p,x),Ap(q,x)),or(Ap(p,x),Ap(r,x))))!=lambda(y,and(or(Ap(p,y),Ap(q,y)),or(Ap(p,y),Ap(r,y)))).
15 [binary,14.1,12.1] $F.
------------ end of proof -------------
Search stopped by max_proofs option.
============ end of search ============
-------------- statistics -------------
clauses given 0
clauses generated 0
binary_res generated 0
para_from generated 0
para_into generated 0
factors generated 0
demod_inf generated 0
demod & eval rewrites 29
clauses wt,lit,sk delete 0
tautologies deleted 0
clauses forward subsumed 0
(subsumed by sos) 0
unit deletions 0
factor simplifications 0
clauses kept 8
new demodulators 0
empty clauses 1
clauses back demodulated 0
clauses back subsumed 0
usable size 6
sos size 2
demodulators size 5
passive size 0
hot size 0
Kbytes malloced 223
----------- 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 1 (0 hr, 0 min, 1 sec)
input time 0.00
clausify time 0.00
process input 0.00
pick given time 0.00
binary_res time 0.00
para_into time 0.00
para_from time 0.00
pre_process time 0.00
renumber time 0.00
demod time 0.00
order equalities 0.00
unit deleletion 0.00
factor simplify 0.00
weigh cl time 0.00
hints keep time 0.00
sort lits time 0.00
forward subsume 0.00
delete cl time 0.00
keep cl time 0.00
hints time 0.00
print_cl time 0.00
conflict time 0.00
new demod time 0.00
post_process time 0.00
back demod time 0.00
back subsume 0.00
factor time 0.00
unindex time 0.00
That finishes the proof of the theorem.
Process 0 finished Tue Aug 12 16:09:34 2008