| ?- prove(thy(queue_lemma_defs) => forall(_Q,del_min_correct(_Q))).

[reading queue_lemma_defs
  [reading queues.o]
  [reading queue_induction
    [reading queues.o]]
  [reading queue_induction
    [reading queues.o]]]

Parsed as predicates: [defined/1,del_min_correct/1,del_min_complete/1,contains/2,=< /2,< /2]

Fresh Clauses :

   49(1) : del_min_complete(empty)and!B.(del_min_complete(B)=>!C.(del_min_complete(insert(B,C)))) -> !D.(del_min_complete(D))
   50(1) : del_min_correct(empty)and!B.(del_min_correct(B)=>!C.(del_min_correct(insert(B,C)))) -> !D.(del_min_correct(D))
   51(1) : defined(empty)
   52(1) : defined(B)==defined(insert(B,C))
   53(1) : del_min_complete(B)==(~ (B=empty)and defined(B)=>defined(queue(del_min(B))))
   54(1) : del_min_correct(B)==!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)

Persisting Clauses:

    1(1) : B<B -> 
    2(1) : B=<B
*   3(1) : B<C -> B=<C
    4(1) : contains(empty,B) -> 
*   5(1) : B<C,D<B -> D<C
    6(1) : B<C,C<B,B=C
*   7(1) : B=<C -> B=C,B<C
    8(1) : queue(pair(B,C))=B
    9(1) : elem(pair(B,C))=C
   10(1) : delete(insert(B,C),C)=C
   11(1) : contains(insert(B,C),C)
   12(1) : del_min(insert(empty,B))=pair(empty,B)
   13(1) : contains(insert(B,C),D)==contains(B,D),C=D
   14(1) : delete(insert(B,C),D)=insert(delete(B,D),C),C=D
   15(1) : B=<elem(del_min(C)) -> del_min(insert(C,B))=pair(C,B),C=empty
   16(1) : elem(del_min(B))<C -> del_min(insert(B,C))=pair(insert(queue(del_min(B)),C),elem(del_min(B))),B=empty

anti_symmetric_relation_symbol(=<).
composition_of_relations(<, <, <).
composition_of_relations(<, =<, <).
composition_of_relations(=<, <, <).
composition_of_relations(=<, =<, =<).
explicit_total_ordering_relation_symbol(<).
irreflexive_relation_symbol(<).
nonstrict_total_ordering_relation_symbol(=<).
reflexive_closure(<, =<).
reflexive_closure(=<, =<).
reflexive_relation_symbol(=<).
strict_part(<, <).
strict_part(=<, <).
special_relation(<).
special_relation(=<).
special_user_relation(<).
symbol_admits_var_elim(<).
total_ordering_relation_symbol(<).
total_relation_symbol(<).
transitive_relation_symbol(<).
transitive_relation_symbol(=<).
firstOrder.



Current precedence:

   First predicates:      [del_min_correct,del_min_complete]
   Other symbols:      [second,first,del_min,delete,contains,empty,insert,queue,elem,pair,=<,defined,<]


Parsed as predicates: [defined/1,del_min_correct/1,del_min_complete/1,contains/2,=< /2,< /2]

Fresh Clauses :

   49(1) : del_min_complete(empty)and!B.(del_min_complete(B)=>!C.(del_min_complete(insert(B,C)))) -> !D.(del_min_complete(D))
   50(1) : del_min_correct(empty)and!B.(del_min_correct(B)=>!C.(del_min_correct(insert(B,C)))) -> !D.(del_min_correct(D))
   51(1) : defined(empty)
   52(1) : defined(B)==defined(insert(B,C))
   53(1) : del_min_complete(B)==(~ (B=empty)and defined(B)=>defined(queue(del_min(B))))
   54(1) : del_min_correct(B)==!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)
   55(1) + !B.(del_min_correct(B)) -> 

Persisting Clauses:

    1(1) : B<B -> 
    2(1) : B=<B
*   3(1) : B<C -> B=<C
    4(1) : contains(empty,B) -> 
*   5(1) : B<C,D<B -> D<C
    6(1) : B<C,C<B,B=C
*   7(1) : B=<C -> B=C,B<C
    8(1) : queue(pair(B,C))=B
    9(1) : elem(pair(B,C))=C
   10(1) : delete(insert(B,C),C)=C
   11(1) : contains(insert(B,C),C)
   12(1) : del_min(insert(empty,B))=pair(empty,B)
   13(1) : contains(insert(B,C),D)==contains(B,D),C=D
   14(1) : delete(insert(B,C),D)=insert(delete(B,D),C),C=D
   15(1) : B=<elem(del_min(C)) -> del_min(insert(C,B))=pair(C,B),C=empty
   16(1) : elem(del_min(B))<C -> del_min(insert(B,C))=pair(insert(queue(del_min(B)),C),elem(del_min(B))),B=empty

anti_symmetric_relation_symbol(=<).
composition_of_relations(<, <, <).
composition_of_relations(<, =<, <).
composition_of_relations(=<, <, <).
composition_of_relations(=<, =<, =<).
explicit_total_ordering_relation_symbol(<).
irreflexive_relation_symbol(<).
nonstrict_total_ordering_relation_symbol(=<).
reflexive_closure(<, =<).
reflexive_closure(=<, =<).
reflexive_relation_symbol(=<).
strict_part(<, <).
strict_part(=<, <).
special_relation(<).
special_relation(=<).
special_user_relation(<).
symbol_admits_var_elim(<).
total_ordering_relation_symbol(<).
total_relation_symbol(<).
transitive_relation_symbol(<).
transitive_relation_symbol(=<).
firstOrder.



Current precedence:

   First predicates:      [del_min_correct,del_min_complete]
   Other symbols:      [second,first,del_min,delete,contains,empty,insert,queue,elem,pair,=<,defined,<]

keeping clause
*  56(2) : !B.(del_min_complete(B)=>!C.(del_min_complete(insert(B,C)))),del_min_complete(empty) -> del_min_complete(D)

keeping clause
*  57(2) : !B.(del_min_correct(B)=>!C.(del_min_correct(insert(B,C)))),del_min_correct(empty) -> del_min_correct(D)

keeping clause
   51(1) : defined(empty)

keeping clause
   52(1) : defined(insert(B,C))==defined(B)

keeping clause
   53(1) : del_min_complete(B)==(~ (B=empty)and defined(B)=>defined(queue(del_min(B))))

keeping clause
   54(1) : del_min_correct(B)==!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)

keeping clause
   58(2) + !B,C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C) -> 

keeping clause
*  61(5) : !B.((~ (B=empty)and defined(B)=>defined(queue(del_min(B))))=>!C.(~ (insert(B,C)=empty)and defined(B)=>defined(queue(del_min(insert(B,C)))))),defined(D) -> defined(queue(del_min(D))),D=empty

keeping clause
*  65(6) : !B.(!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)=>!E,F,G.(~ (insert(B,E)=empty)and elem(del_min(insert(B,E)))=G and contains(insert(B,E),F)=>G=<F)),contains(H,I) -> elem(del_min(H))=<I,H=empty

keeping clause
   66(3) + !B,C.(~ (s$9=empty)and elem(del_min(s$9))=C and contains(s$9,B)=>C=<B) -> 

keeping clause
*  67(6) : (~ (s$1=empty)and defined(s$1)=>defined(queue(del_min(s$1))))=>!B.(~ (insert(s$1,B)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,B))))),defined(C) -> defined(queue(del_min(C))),C=empty

keeping clause
*  68(7) : !B,C.(~ (s$4=empty)and elem(del_min(s$4))=C and contains(s$4,B)=>C=<B)=>!D,E,F.(~ (insert(s$4,D)=empty)and elem(del_min(insert(s$4,D)))=F and contains(insert(s$4,D),E)=>F=<E),contains(G,H) -> elem(del_min(G))=<H,G=empty

keeping clause
   69(4) + !B.(~ (s$9=empty)and elem(del_min(s$9))=B and contains(s$9,s$1)=>B=<s$1) -> 

keeping clause
   70(4) + s$1=s$8(s$9)

keeping clause
   71(5) + !B.(~ (s$9=empty)and elem(del_min(s$9))=B and contains(s$9,s$8(s$9))=>B=<s$8(s$9)) -> 

keeping clause
*  72(7) + (~ (s$8(s$9)=empty)and defined(s$8(s$9))=>defined(queue(del_min(s$8(s$9)))))=>!B.(~ (insert(s$8(s$9),B)=empty)and defined(s$8(s$9))=>defined(queue(del_min(insert(s$8(s$9),B))))),defined(C) -> defined(queue(del_min(C))),C=empty

keeping clause
* 79(11) : contains(s$4,B) -> elem(del_min(s$4))=<B,p$499

keeping clause
* 80(11) : p$499,contains(B,C) -> s$4=empty,elem(del_min(B))=<C,B=empty

keeping clause
*  74(8) : !B,C,D.(~ (insert(s$4,B)=empty)and elem(del_min(insert(s$4,B)))=D and contains(insert(s$4,B),C)=>D=<C),contains(E,F) -> elem(del_min(E))=<F,E=empty

keeping clause
   75(6) + ~ (s$9=empty)and elem(del_min(s$9))=s$2 and contains(s$9,s$8(s$9))=>s$2=<s$8(s$9) -> 

keeping clause
   76(6) + s$2=s$7(s$9)

keeping clause
   81(7) + ~ (s$9=empty)and elem(del_min(s$9))=s$7(s$9)and contains(s$9,s$8(s$9))=>s$7(s$9)=<s$8(s$9) -> 

keeping clause
  87(10) + defined(s$8(s$9)) -> defined(queue(del_min(s$8(s$9)))),s$8(s$9)=empty

keeping clause
*  83(8) + !B.(~ (insert(s$8(s$9),B)=empty)and defined(s$8(s$9))=>defined(queue(del_min(insert(s$8(s$9),B))))),defined(C) -> defined(queue(del_min(C))),C=empty

keeping clause
*  84(9) : !B,C.(~ (insert(s$4,s$3)=empty)and elem(del_min(insert(s$4,s$3)))=C and contains(insert(s$4,s$3),B)=>C=<B),contains(D,E) -> elem(del_min(D))=<E,D=empty

keeping clause
   85(9) : s$3=s$5(s$4)

keeping clause
* 88(10) : !B,C.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=C and contains(insert(s$4,s$5(s$4)),B)=>C=<B),contains(D,E) -> elem(del_min(D))=<E,D=empty

keeping clause
   89(8) + ~ (s$9=empty)and elem(del_min(s$9))=s$7(s$9)and contains(s$9,s$8(s$9))

keeping clause
   91(9) + s$8(s$9)<s$7(s$9)

keeping clause
*  92(9) + ~ (insert(s$8(s$9),s$4)=empty)and defined(s$8(s$9))=>defined(queue(del_min(insert(s$8(s$9),s$4)))),defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
   93(9) + s$2(s$8(s$9))=s$4

keeping clause
* 94(11) : !B.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=B and contains(insert(s$4,s$5(s$4)),s$5)=>B=<s$5),contains(C,D) -> elem(del_min(C))=<D,C=empty

keeping clause
  95(11) : s$8(insert(s$4,s$5(s$4)))=s$5

keeping clause
   96(9) + ~ (s$9=empty)and elem(del_min(s$9))=s$7(s$9)

keeping clause
   97(9) + contains(s$9,s$8(s$9))

keeping clause
  98(10) + defined(B) -> defined(queue(del_min(B))),~ (insert(s$8(s$9),s$4)=empty)and defined(s$8(s$9)),B=empty

keeping clause
* 99(10) + defined(queue(del_min(insert(s$8(s$9),s$4)))),defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
*100(12) : ~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5)=>s$6=<s$5,contains(B,C) -> elem(del_min(B))=<C,B=empty

keeping clause
 101(12) : s$7(insert(s$4,s$5(s$4)))=s$6

keeping clause
*104(11) + s$9=empty -> 

keeping clause
 103(10) + s$7(s$9)=elem(del_min(s$9))

keeping clause
 105(11) + s$8(s$9)<elem(del_min(s$9))

keeping clause
*112(12) + insert(s$8(s$9),s$4)=empty,defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
 107(11) + defined(B) -> defined(queue(del_min(B))),defined(s$8(s$9)),B=empty

keeping clause
*108(13) : contains(B,C) -> elem(del_min(B))=<C,~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5),B=empty

keeping clause
*113(14) : contains(B,C) -> s$5<s$6,elem(del_min(B))=<C,B=empty

keeping clause
 115(13) + defined(B) -> defined(queue(del_min(B))),elem(del_min(s$8(s$9)))<s$4,B=empty,s$8(s$9)=empty

keeping clause
*117(14) + defined(queue(del_min(s$8(s$9)))),defined(B) -> defined(queue(del_min(B))),s$8(s$9)=empty,B=empty

keeping clause
 128(16) + s$5<s$6

keeping clause
 141(17) + defined(B) -> s$8(s$9)=empty,defined(queue(del_min(B))),B=empty

keeping clause
 142(15) + ~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5)

keeping clause
 143(16) + ~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6

keeping clause
 144(16) + contains(insert(s$4,s$5(s$4)),s$5)

keeping clause
*147(18) + insert(s$4,s$5(s$4))=empty -> 

keeping clause
 146(17) + elem(del_min(insert(s$4,s$5(s$4))))=s$6

keeping clause
 148(17) + s$5(s$4)=s$5,contains(s$4,s$5)

keeping clause
 164(20) + elem(del_min(s$4))<s$5(s$4),s$4=empty,s$5(s$4)=s$6

keeping clause
 166(20) + s$5(s$4)=<elem(del_min(s$4)),s$4=empty,elem(del_min(s$4))=s$6

keeping clause
 151(18) + defined(B) -> contains(s$9,empty),defined(queue(del_min(B))),B=empty

keeping clause
 152(18) + defined(B) -> empty<elem(del_min(s$9)),defined(queue(del_min(B))),B=empty

keeping clause
 168(20) + defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
*176(19) + insert(s$4,s$5)=empty -> contains(s$4,s$5)

keeping clause
 178(18) + elem(del_min(insert(s$4,s$5)))=s$6,contains(s$4,s$5)

keeping clause
 190(21) + elem(del_min(s$4))<s$5,contains(s$4,s$5),s$4=empty,s$5=s$6

keeping clause
 192(21) + s$5=<elem(del_min(s$4)),contains(s$4,s$5),s$4=empty,elem(del_min(s$4))=s$6

keeping clause
 193(22) + s$5(s$4)=s$6,s$4=empty,elem(del_min(s$4))=s$6

keeping clause
*198(23) + insert(s$4,s$6)=empty -> elem(del_min(s$4))=s$6,s$4=empty

keeping clause
 199(23) + elem(del_min(s$4))=s$6,s$4=empty,contains(insert(s$4,s$6),s$5)

keeping clause
 200(23) + elem(del_min(insert(s$4,s$6)))=s$6,s$4=empty,elem(del_min(s$4))=s$6

keeping clause
 205(24) + s$6=<elem(del_min(s$4)),s$4=empty

keeping clause
 218(27) + contains(s$4,s$5),s$4=empty

keeping clause
 236(29) + s$4=empty,p$499

keeping clause
*258(31) + insert(empty,s$5(empty))=empty -> p$499

keeping clause
 259(31) + contains(insert(empty,s$5(empty)),s$5),p$499

keeping clause
 260(31) + s$5(empty)=s$6,p$499

keeping clause
*261(31) + insert(empty,s$5)=empty -> p$499

keeping clause
 262(31) + s$5=s$6,p$499

keeping clause
 263(32) + p$499

keeping clause
*268(33) + contains(B,C) -> elem(del_min(B))=<C,s$4=empty,B=empty

keeping clause
 275(35) + s$4=empty

keeping clause
 277(36) + s$8(insert(empty,s$5(empty)))=s$5

keeping clause
 278(36) + s$7(insert(empty,s$5(empty)))=s$6

keeping clause
*279(36) + insert(empty,s$5(empty))=empty -> 

keeping clause
 280(36) + contains(insert(empty,s$5(empty)),s$5)

keeping clause
 281(36) + s$5(empty)=s$6

keeping clause
 282(37) + s$5=s$6

keeping clause
*283(38) + insert(empty,s$6)=empty -> 

keeping clause
 284(38) + false


Proof:
======

   1 : A<A ->                                                           [input]
   4 : contains(empty,A) ->                                             [input]
   9 : elem(pair(A,B))=B                                                [input]
  12 : del_min(insert(empty,A))=pair(empty,A)                           [input]
  13 : contains(insert(A,B),C)==contains(A,C),B=C                       [input]
  15 : A=<elem(del_min(B)) -> del_min(insert(B,A))=pair(B,A),B=empty    [input]
  16 : elem(del_min(A))<B -> del_min(insert(A,B))=pair(insert(queue(del_min(A)),B),elem(del_min(A))),A=empty [input]
  50 : del_min_correct(empty)and!A.(del_min_correct(A)=>!B.(del_min_correct(insert(A,B)))) -> !C.(del_min_correct(C)) [input]
  54 : del_min_correct(A)==!B,C.(~ (A=empty)and elem(del_min(A))=C and contains(A,B)=>C=<B) [input]
  55 + !A.(del_min_correct(A)) ->                                       [input]
  57 : del_min_correct(empty),!A.(del_min_correct(A)=>!B.(del_min_correct(insert(A,B)))) -> del_min_correct(C) [condensement of 50]
  58 + !A,B,C.(~ (A=empty)and elem(del_min(A))=C and contains(A,B)=>C=<B) ->  [reduction of 55 by [54]]
  62 : !A.(!B,C.(~ (A=empty)and elem(del_min(A))=C and contains(A,B)=>C=<B)=>!D,E,F.(~ (insert(A,D)=empty)and elem(del_min(insert(A,D)))=F and contains(insert(A,D),E)=>F=<E)) -> !H,I.(~ (G=empty)and elem(del_min(G))=I and contains(G,H)=>I=<H) [reduction of 57 by [54,54,54,4,L,L,L,L,L,L,L,54]]
  63 : ~ (A=empty),elem(del_min(A))=B,contains(A,C),!D.(!E,F.(~ (D=empty)and elem(del_min(D))=F and contains(D,E)=>F=<E)=>!G,H,I.(~ (insert(D,G)=empty)and elem(del_min(insert(D,G)))=I and contains(insert(D,G),H)=>I=<H)) -> B=<C [condensement of 62]
  64 : !A.(!B,C.(~ (A=empty)and elem(del_min(A))=C and contains(A,B)=>C=<B)=>!D,E,F.(~ (insert(A,D)=empty)and elem(del_min(insert(A,D)))=F and contains(insert(A,D),E)=>F=<E)),contains(G,H),elem(del_min(G))=I -> I=<H,G=empty [reduction of 63 by [L]]
  65 : !A.(!B,C.(~ (A=empty)and elem(del_min(A))=C and contains(A,B)=>C=<B)=>!D,E,F.(~ (insert(A,D)=empty)and elem(del_min(insert(A,D)))=F and contains(insert(A,D),E)=>F=<E)),contains(G,H) -> G=empty,elem(del_min(G))=<H [variable elimination from 64]
  66 + !A,B.(~ (s$9=empty)and elem(del_min(s$9))=B and contains(s$9,A)=>B=<A) ->  [expansion from 58]
  68 : contains(A,B),!C,D.(~ (s$4=empty)and elem(del_min(s$4))=D and contains(s$4,C)=>D=<C)=>!E,F,G.(~ (insert(s$4,E)=empty)and elem(del_min(insert(s$4,E)))=G and contains(insert(s$4,E),F)=>G=<F) -> elem(del_min(A))=<B,A=empty [expansion from 65]
  69 + !A.(~ (s$9=empty)and elem(del_min(s$9))=A and contains(s$9,s$1)=>A=<s$1) ->  [expansion from 66]
  70 + s$1=s$8(s$9)                                         [expansion from 66]
  71 + !A.(~ (s$9=empty)and elem(del_min(s$9))=A and contains(s$9,s$8(s$9))=>A=<s$8(s$9)) ->  [reduction of 69 by [70,70]]
  73 : ~ (s$4=empty),elem(del_min(s$4))=A,contains(s$4,B),contains(C,D) -> A=<B,elem(del_min(C))=<D,C=empty [expansion from 68]
  74 : contains(A,B),!C,D,E.(~ (insert(s$4,C)=empty)and elem(del_min(insert(s$4,C)))=E and contains(insert(s$4,C),D)=>E=<D) -> elem(del_min(A))=<B,A=empty [expansion from 68]
  75 + ~ (s$9=empty)and elem(del_min(s$9))=s$2 and contains(s$9,s$8(s$9))=>s$2=<s$8(s$9) ->  [expansion from 71]
  76 + s$2=s$7(s$9)                                         [expansion from 71]
  77 : contains(A,B),contains(s$4,C),elem(del_min(s$4))=D -> A=empty,elem(del_min(A))=<B,D=<C,s$4=empty [reduction of 73 by [L]]
  78 : contains(A,B),contains(s$4,C) -> A=empty,s$4=empty,elem(del_min(A))=<B,elem(del_min(s$4))=<C [variable elimination from 77]
  79 : contains(s$4,A) -> p$499,elem(del_min(s$4))=<A [variable elimination from 78]
  80 : p$499,contains(A,B) -> A=empty,s$4=empty,elem(del_min(A))=<B [variable elimination from 78]
  81 + ~ (s$9=empty)and elem(del_min(s$9))=s$7(s$9)and contains(s$9,s$8(s$9))=>s$7(s$9)=<s$8(s$9) ->  [reduction of 75 by [76,76]]
  84 : contains(A,B),!C,D.(~ (insert(s$4,s$3)=empty)and elem(del_min(insert(s$4,s$3)))=D and contains(insert(s$4,s$3),C)=>D=<C) -> elem(del_min(A))=<B,A=empty [expansion from 74]
  85 : s$3=s$5(s$4)                                         [expansion from 74]
  88 : contains(A,B),!C,D.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=D and contains(insert(s$4,s$5(s$4)),C)=>D=<C) -> A=empty,elem(del_min(A))=<B [reduction of 84 by [85,85,85,85,85]]
  89 + ~ (s$9=empty)and elem(del_min(s$9))=s$7(s$9)and contains(s$9,s$8(s$9)) [expansion from 81]
  90 + s$7(s$9)=<s$8(s$9) ->                                [expansion from 81]
  91 + s$8(s$9)<s$7(s$9)                          [totality resolution from 90]
  94 : contains(A,B),!C.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=C and contains(insert(s$4,s$5(s$4)),s$5)=>C=<s$5) -> elem(del_min(A))=<B,A=empty [expansion from 88]
  96 + ~ (s$9=empty)and elem(del_min(s$9))=s$7(s$9)         [expansion from 89]
  97 + contains(s$9,s$8(s$9))                               [expansion from 89]
 100 : contains(A,B),~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5)=>s$6=<s$5 -> elem(del_min(A))=<B,A=empty [expansion from 94]
 102 + ~ (s$9=empty)                                        [expansion from 96]
 103 + elem(del_min(s$9))=s$7(s$9)                          [expansion from 96]
 104 + s$9=empty ->                                   [reduction of 102 by [L]]
 105 + s$8(s$9)<elem(del_min(s$9))                   [reduction of 91 by [103]]
 108 : contains(A,B) -> elem(del_min(A))=<B,A=empty,~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5) [expansion from 100]
 109 : contains(A,B),s$6=<s$5 -> elem(del_min(A))=<B,A=empty [expansion from 100]
 113 : contains(A,B) -> s$5<s$6,elem(del_min(A))=<B,A=empty [totality resolution from 109]
 125 + s$5<s$6,elem(del_min(s$9))=<s$8(s$9),s$9=empty [negative chaining of 97 from 113]
 128 + s$5<s$6                              [reduction of 125 by [105,L,104,L]]
 137 + elem(del_min(s$9))=<s$8(s$9),~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5),s$9=empty [negative chaining of 97 from 108]
 142 + ~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 and contains(insert(s$4,s$5(s$4)),s$5) [reduction of 137 by [105,L,104,L]]
 143 + ~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$6 [expansion from 142]
 144 + contains(insert(s$4,s$5(s$4)),s$5)                  [expansion from 142]
 146 + elem(del_min(insert(s$4,s$5(s$4))))=s$6             [expansion from 143]
 148 + contains(s$4,s$5),s$5(s$4)=s$5                 [chaining of 13 from 144]
 149 + s$5(s$4)=<elem(del_min(s$4)) -> elem(pair(s$4,s$5(s$4)))=s$6,s$4=empty [chaining of 15 from 146]
 150 + elem(del_min(s$4))<s$5(s$4) -> elem(pair(insert(queue(del_min(s$4)),s$5(s$4)),elem(del_min(s$4))))=s$6,s$4=empty [chaining of 16 from 146]
 163 + elem(del_min(s$4))<s$5(s$4),elem(pair(s$4,s$5(s$4)))=s$6,s$4=empty [totality resolution from 149]
 164 + elem(del_min(s$4))<s$5(s$4),s$4=empty,s$5(s$4)=s$6 [reduction of 163 by [9]]
 165 + s$5(s$4)=<elem(del_min(s$4)),elem(pair(insert(queue(del_min(s$4)),s$5(s$4)),elem(del_min(s$4))))=s$6,s$4=empty [totality resolution from 150]
 166 + s$5(s$4)=<elem(del_min(s$4)),s$4=empty,elem(del_min(s$4))=s$6 [reduction of 165 by [9]]
 178 + elem(del_min(insert(s$4,s$5)))=s$6,contains(s$4,s$5) [chaining of 148 from 146]
 179 + s$5=<elem(del_min(s$4)) -> elem(pair(s$4,s$5))=s$6,s$4=empty,contains(s$4,s$5) [chaining of 15 from 178]
 183 + s$4=empty,s$5(s$4)=s$6,s$4=empty,elem(del_min(s$4))=s$6 [chaining of 164 from 166]
 189 + elem(del_min(s$4))<s$5,elem(pair(s$4,s$5))=s$6,s$4=empty,contains(s$4,s$5) [totality resolution from 179]
 190 + elem(del_min(s$4))<s$5,contains(s$4,s$5),s$4=empty,s$5=s$6 [reduction of 189 by [9]]
 193 + s$5(s$4)=s$6,s$4=empty,elem(del_min(s$4))=s$6      [condensement of 183]
 203 + s$6=<elem(del_min(s$4)),s$4=empty,elem(del_min(s$4))=s$6,s$4=empty,elem(del_min(s$4))=s$6 [chaining of 166 from 193]
 205 + s$6=<elem(del_min(s$4)),s$4=empty                  [condensement of 203]
 206 + s$6<s$5,contains(s$4,s$5),s$4=empty,s$5=s$6,s$4=empty [chaining of 190 from 205]
 217 + s$6=<s$5,contains(s$4,s$5),s$4=empty               [condensement of 206]
 218 + s$4=empty,contains(s$4,s$5)                [reduction of 217 by [128,L]]
 230 + s$4=empty,elem(del_min(s$4))=<s$5,p$499 [negative chaining of 218 from 79]
 236 + s$4=empty,p$499                        [reduction of 230 by [128,205,L]]
 249 + elem(del_min(insert(empty,s$5)))=s$6,p$499,contains(s$4,s$5) [chaining of 236 from 178]
 262 + s$5=s$6,p$499                       [reduction of 249 by [12,9,236,4,L]]
 263 + p$499                                         [chaining of 128 from 262]
 268 + contains(A,B) -> A=empty,elem(del_min(A))=<B,s$4=empty [reduction of 80 by [263]]
 269 + elem(del_min(s$9))=<s$8(s$9),s$4=empty,s$9=empty [negative chaining of 97 from 268]
 275 + s$4=empty                            [reduction of 269 by [105,L,104,L]]
 281 + s$5(empty)=s$6                      [reduction of 146 by [275,275,12,9]]
 282 + s$6=s$5                          [reduction of 148 by [275,281,275,4,L]]
 284 + false                                    [reduction of 128 by [282,1,L]]

Length = 83, Depth = 38, Search Depth = 1



Total time: 3920 milliseconds

Number of forward inferences: 95
Number of tableau inferences: 35
Number of generated clauses: 284
Number of kept clauses: 88
yes
| ?- prove(thy(queue_lemma_defs) => forall(_Q,del_min_complete(_Q))).


Parsed as predicates: [defined/1,del_min_correct/1,del_min_complete/1,contains/2,=< /2,< /2]

Fresh Clauses :

   17(1) : del_min_complete(empty)and!B.(del_min_complete(B)=>!C.(del_min_complete(insert(B,C)))) -> !D.(del_min_complete(D))
   18(1) : del_min_correct(empty)and!B.(del_min_correct(B)=>!C.(del_min_correct(insert(B,C)))) -> !D.(del_min_correct(D))
   19(1) : defined(empty)
   20(1) : defined(B)==defined(insert(B,C))
   21(1) : del_min_complete(B)==(~ (B=empty)and defined(B)=>defined(queue(del_min(B))))
   22(1) : del_min_correct(B)==!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)

Persisting Clauses:

    1(1) : B<B -> 
    2(1) : B=<B
*   3(1) : B<C -> B=<C
    4(1) : contains(empty,B) -> 
*   5(1) : B<C,D<B -> D<C
    6(1) : B<C,C<B,B=C
*   7(1) : B=<C -> B=C,B<C
    8(1) : queue(pair(B,C))=B
    9(1) : elem(pair(B,C))=C
   10(1) : delete(insert(B,C),C)=C
   11(1) : contains(insert(B,C),C)
   12(1) : del_min(insert(empty,B))=pair(empty,B)
   13(1) : contains(insert(B,C),D)==contains(B,D),C=D
   14(1) : delete(insert(B,C),D)=insert(delete(B,D),C),C=D
   15(1) : B=<elem(del_min(C)) -> del_min(insert(C,B))=pair(C,B),C=empty
   16(1) : elem(del_min(B))<C -> del_min(insert(B,C))=pair(insert(queue(del_min(B)),C),elem(del_min(B))),B=empty

anti_symmetric_relation_symbol(=<).
composition_of_relations(<, <, <).
composition_of_relations(<, =<, <).
composition_of_relations(=<, <, <).
composition_of_relations(=<, =<, =<).
explicit_total_ordering_relation_symbol(<).
irreflexive_relation_symbol(<).
nonstrict_total_ordering_relation_symbol(=<).
reflexive_closure(<, =<).
reflexive_closure(=<, =<).
reflexive_relation_symbol(=<).
strict_part(<, <).
strict_part(=<, <).
special_relation(<).
special_relation(=<).
special_user_relation(<).
symbol_admits_var_elim(<).
total_ordering_relation_symbol(<).
total_relation_symbol(<).
transitive_relation_symbol(<).
transitive_relation_symbol(=<).
firstOrder.



Current precedence:

   First predicates:      [del_min_correct,del_min_complete]
   Other symbols:      [second,first,del_min,delete,contains,empty,insert,queue,elem,pair,=<,defined,<]


Parsed as predicates: [defined/1,del_min_correct/1,del_min_complete/1,contains/2,=< /2,< /2]

Fresh Clauses :

   17(1) : del_min_complete(empty)and!B.(del_min_complete(B)=>!C.(del_min_complete(insert(B,C)))) -> !D.(del_min_complete(D))
   18(1) : del_min_correct(empty)and!B.(del_min_correct(B)=>!C.(del_min_correct(insert(B,C)))) -> !D.(del_min_correct(D))
   19(1) : defined(empty)
   20(1) : defined(B)==defined(insert(B,C))
   21(1) : del_min_complete(B)==(~ (B=empty)and defined(B)=>defined(queue(del_min(B))))
   22(1) : del_min_correct(B)==!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)
   23(1) + !B.(del_min_complete(B)) -> 

Persisting Clauses:

    1(1) : B<B -> 
    2(1) : B=<B
*   3(1) : B<C -> B=<C
    4(1) : contains(empty,B) -> 
*   5(1) : B<C,D<B -> D<C
    6(1) : B<C,C<B,B=C
*   7(1) : B=<C -> B=C,B<C
    8(1) : queue(pair(B,C))=B
    9(1) : elem(pair(B,C))=C
   10(1) : delete(insert(B,C),C)=C
   11(1) : contains(insert(B,C),C)
   12(1) : del_min(insert(empty,B))=pair(empty,B)
   13(1) : contains(insert(B,C),D)==contains(B,D),C=D
   14(1) : delete(insert(B,C),D)=insert(delete(B,D),C),C=D
   15(1) : B=<elem(del_min(C)) -> del_min(insert(C,B))=pair(C,B),C=empty
   16(1) : elem(del_min(B))<C -> del_min(insert(B,C))=pair(insert(queue(del_min(B)),C),elem(del_min(B))),B=empty

anti_symmetric_relation_symbol(=<).
composition_of_relations(<, <, <).
composition_of_relations(<, =<, <).
composition_of_relations(=<, <, <).
composition_of_relations(=<, =<, =<).
explicit_total_ordering_relation_symbol(<).
irreflexive_relation_symbol(<).
nonstrict_total_ordering_relation_symbol(=<).
reflexive_closure(<, =<).
reflexive_closure(=<, =<).
reflexive_relation_symbol(=<).
strict_part(<, <).
strict_part(=<, <).
special_relation(<).
special_relation(=<).
special_user_relation(<).
symbol_admits_var_elim(<).
total_ordering_relation_symbol(<).
total_relation_symbol(<).
transitive_relation_symbol(<).
transitive_relation_symbol(=<).
firstOrder.



Current precedence:

   First predicates:      [del_min_correct,del_min_complete]
   Other symbols:      [second,first,del_min,delete,contains,empty,insert,queue,elem,pair,=<,defined,<]

keeping clause
*  24(2) : !B.(del_min_complete(B)=>!C.(del_min_complete(insert(B,C)))),del_min_complete(empty) -> del_min_complete(D)

keeping clause
*  25(2) : !B.(del_min_correct(B)=>!C.(del_min_correct(insert(B,C)))),del_min_correct(empty) -> del_min_correct(D)

keeping clause
   19(1) : defined(empty)

keeping clause
   20(1) : defined(insert(B,C))==defined(B)

keeping clause
   21(1) : del_min_complete(B)==(~ (B=empty)and defined(B)=>defined(queue(del_min(B))))

keeping clause
   22(1) : del_min_correct(B)==!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)

keeping clause
   26(2) + !B.(~ (B=empty)and defined(B)=>defined(queue(del_min(B)))) -> 

keeping clause
*  29(5) : !B.((~ (B=empty)and defined(B)=>defined(queue(del_min(B))))=>!C.(~ (insert(B,C)=empty)and defined(B)=>defined(queue(del_min(insert(B,C)))))),defined(D) -> defined(queue(del_min(D))),D=empty

keeping clause
*  33(6) : !B.(!C,D.(~ (B=empty)and elem(del_min(B))=D and contains(B,C)=>D=<C)=>!E,F,G.(~ (insert(B,E)=empty)and elem(del_min(insert(B,E)))=G and contains(insert(B,E),F)=>G=<F)),contains(H,I) -> elem(del_min(H))=<I,H=empty

keeping clause
   34(3) + ~ (s$9=empty)and defined(s$9)=>defined(queue(del_min(s$9))) -> 

keeping clause
*  35(6) : (~ (s$1=empty)and defined(s$1)=>defined(queue(del_min(s$1))))=>!B.(~ (insert(s$1,B)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,B))))),defined(C) -> defined(queue(del_min(C))),C=empty

keeping clause
*  36(7) : !B,C.(~ (s$4=empty)and elem(del_min(s$4))=C and contains(s$4,B)=>C=<B)=>!D,E,F.(~ (insert(s$4,D)=empty)and elem(del_min(insert(s$4,D)))=F and contains(insert(s$4,D),E)=>F=<E),contains(G,H) -> elem(del_min(G))=<H,G=empty

keeping clause
   37(4) + ~ (s$9=empty)and defined(s$9)

keeping clause
   38(4) + defined(queue(del_min(s$9))) -> 

keeping clause
   46(9) : defined(s$1) -> defined(queue(del_min(s$1))),s$1=empty

keeping clause
*  40(7) : !B.(~ (insert(s$1,B)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,B))))),defined(C) -> defined(queue(del_min(C))),C=empty

keeping clause
* 49(11) : contains(s$4,B) -> elem(del_min(s$4))=<B,p$499

keeping clause
* 50(11) : p$499,contains(B,C) -> s$4=empty,elem(del_min(B))=<C,B=empty

keeping clause
*  42(8) : !B,C,D.(~ (insert(s$4,B)=empty)and elem(del_min(insert(s$4,B)))=D and contains(insert(s$4,B),C)=>D=<C),contains(E,F) -> elem(del_min(E))=<F,E=empty

keeping clause
*  51(6) + s$9=empty -> 

keeping clause
   44(5) + defined(s$9)

keeping clause
*  52(8) : ~ (insert(s$1,s$1)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,s$1)))),defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
   53(8) : s$2(s$1)=s$1

keeping clause
*  54(9) : !B,C.(~ (insert(s$4,s$2)=empty)and elem(del_min(insert(s$4,s$2)))=C and contains(insert(s$4,s$2),B)=>C=<B),contains(D,E) -> elem(del_min(D))=<E,D=empty

keeping clause
   55(9) : s$2=s$5(s$4)

keeping clause
* 56(10) : !B,C.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=C and contains(insert(s$4,s$5(s$4)),B)=>C=<B),contains(D,E) -> elem(del_min(D))=<E,D=empty

keeping clause
   57(9) : defined(B) -> defined(queue(del_min(B))),~ (insert(s$1,s$1)=empty)and defined(s$1),B=empty

keeping clause
*  58(9) : defined(queue(del_min(insert(s$1,s$1)))),defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
* 59(11) : !B.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=B and contains(insert(s$4,s$5(s$4)),s$3)=>B=<s$3),contains(C,D) -> elem(del_min(C))=<D,C=empty

keeping clause
  60(11) : s$3=s$8(insert(s$4,s$5(s$4)))

keeping clause
* 61(12) : !B.(~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=B and contains(insert(s$4,s$5(s$4)),s$8(insert(s$4,s$5(s$4))))=>B=<s$8(insert(s$4,s$5(s$4)))),contains(C,D) -> elem(del_min(C))=<D,C=empty

keeping clause
* 66(11) : insert(s$1,s$1)=empty,defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
  63(10) : defined(B) -> defined(queue(del_min(B))),defined(s$1),B=empty

keeping clause
* 64(13) : ~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$4 and contains(insert(s$4,s$5(s$4)),s$8(insert(s$4,s$5(s$4))))=>s$4=<s$8(insert(s$4,s$5(s$4))),contains(B,C) -> elem(del_min(B))=<C,B=empty

keeping clause
  65(13) : s$7(insert(s$4,s$5(s$4)))=s$4

keeping clause
* 67(14) : contains(B,C) -> elem(del_min(B))=<C,~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$4 and contains(insert(s$4,s$5(s$4)),s$8(insert(s$4,s$5(s$4)))),B=empty

keeping clause
* 75(15) : contains(B,C) -> s$8(insert(s$4,s$5(s$4)))<s$4,elem(del_min(B))=<C,B=empty

keeping clause
  79(12) : defined(B) -> defined(queue(del_min(B))),elem(del_min(s$1))<s$1,B=empty,s$1=empty

keeping clause
* 83(14) : defined(queue(del_min(s$1))),defined(B) -> defined(queue(del_min(B))),s$1=empty,B=empty

keeping clause
  84(16) : s$8(insert(s$4,s$5(s$4)))<s$4,elem(del_min(insert(B,C)))=<C,insert(B,C)=empty

keeping clause
* 85(16) : contains(B,C) -> s$8(insert(s$4,s$5(s$4)))<s$4,elem(del_min(insert(B,D)))=<C,D=C,insert(B,D)=empty

keeping clause
 106(17) : defined(B) -> s$1=empty,defined(queue(del_min(B))),B=empty

keeping clause
 101(17) : s$8(insert(s$4,s$5(s$4)))<s$4,elem(del_min(insert(insert(B,C),D)))=<C,D=C,insert(insert(B,C),D)=empty

keeping clause
*102(17) : contains(B,C) -> s$8(insert(s$4,s$5(s$4)))<s$4,elem(del_min(insert(insert(B,D),E)))=<C,D=C,E=C,insert(insert(B,D),E)=empty

keeping clause
 103(15) : elem(del_min(insert(B,C)))=<C,~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$4 and contains(insert(s$4,s$5(s$4)),s$8(insert(s$4,s$5(s$4)))),insert(B,C)=empty

keeping clause
*104(15) : contains(B,C) -> elem(del_min(insert(B,D)))=<C,~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$4 and contains(insert(s$4,s$5(s$4)),s$8(insert(s$4,s$5(s$4)))),D=C,insert(B,D)=empty

keeping clause
 108(16) : elem(del_min(insert(B,C)))=<C,~ (insert(s$4,s$5(s$4))=empty)and elem(del_min(insert(s$4,s$5(s$4))))=s$4,insert(B,C)=empty

keeping clause
 109(16) : elem(del_min(insert(B,C)))=<C,contains(insert(s$4,s$5(s$4)),s$8(insert(s$4,s$5(s$4)))),insert(B,C)=empty

keeping clause
*126(19) : insert(s$1,empty)=empty,defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
*127(19) : insert(empty,s$1)=empty,defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
*128(19) : defined(queue(del_min(insert(s$1,empty)))),defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
 130(20) : defined(B) -> defined(queue(del_min(B))),B=empty

keeping clause
*143(18) : insert(s$4,s$5(s$4))=empty -> elem(del_min(insert(B,C)))=<C,insert(B,C)=empty

keeping clause
 136(17) : elem(del_min(insert(B,C)))=<C,elem(del_min(insert(s$4,s$5(s$4))))=s$4,insert(B,C)=empty

keeping clause
 144(22) + false


Proof:
======

   8 : queue(pair(A,B))=A                                               [input]
  12 : del_min(insert(empty,A))=pair(empty,A)                           [input]
  15 : A=<elem(del_min(B)) -> del_min(insert(B,A))=pair(B,A),B=empty    [input]
  16 : elem(del_min(A))<B -> del_min(insert(A,B))=pair(insert(queue(del_min(A)),B),elem(del_min(A))),A=empty [input]
  17 : del_min_complete(empty)and!A.(del_min_complete(A)=>!B.(del_min_complete(insert(A,B)))) -> !C.(del_min_complete(C)) [input]
  19 : defined(empty)                                                   [input]
  20 : defined(A)==defined(insert(A,B))                                 [input]
  21 : del_min_complete(A)==(~ (A=empty)and defined(A)=>defined(queue(del_min(A)))) [input]
  23 + !A.(del_min_complete(A)) ->                                      [input]
  24 : del_min_complete(empty),!A.(del_min_complete(A)=>!B.(del_min_complete(insert(A,B)))) -> del_min_complete(C) [condensement of 17]
  26 + !A.(~ (A=empty)and defined(A)=>defined(queue(del_min(A)))) ->  [reduction of 23 by [21]]
  27 : !A.((~ (A=empty)and defined(A)=>defined(queue(del_min(A))))=>!B.(~ (insert(A,B)=empty)and defined(A)=>defined(queue(del_min(insert(A,B)))))) -> ~ (C=empty)and defined(C)=>defined(queue(del_min(C))) [reduction of 24 by [21,20,21,21,19,L,L,L,L,21]]
  28 : ~ (A=empty),defined(A),!B.((~ (B=empty)and defined(B)=>defined(queue(del_min(B))))=>!C.(~ (insert(B,C)=empty)and defined(B)=>defined(queue(del_min(insert(B,C)))))) -> defined(queue(del_min(A))) [condensement of 27]
  29 : !A.((~ (A=empty)and defined(A)=>defined(queue(del_min(A))))=>!B.(~ (insert(A,B)=empty)and defined(A)=>defined(queue(del_min(insert(A,B)))))),defined(C) -> defined(queue(del_min(C))),C=empty [reduction of 28 by [L]]
  34 + ~ (s$9=empty)and defined(s$9)=>defined(queue(del_min(s$9))) ->  [expansion from 26]
  35 : defined(A),(~ (s$1=empty)and defined(s$1)=>defined(queue(del_min(s$1))))=>!B.(~ (insert(s$1,B)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,B))))) -> defined(queue(del_min(A))),A=empty [expansion from 29]
  37 + ~ (s$9=empty)and defined(s$9)                        [expansion from 34]
  38 + defined(queue(del_min(s$9))) ->                      [expansion from 34]
  39 : ~ (s$1=empty),defined(s$1),defined(A) -> defined(queue(del_min(s$1))),defined(queue(del_min(A))),A=empty [expansion from 35]
  40 : defined(A),!B.(~ (insert(s$1,B)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,B))))) -> defined(queue(del_min(A))),A=empty [expansion from 35]
  43 + ~ (s$9=empty)                                        [expansion from 37]
  44 + defined(s$9)                                         [expansion from 37]
  45 : defined(A),defined(s$1) -> A=empty,defined(queue(del_min(A))),defined(queue(del_min(s$1))),s$1=empty [reduction of 39 by [L]]
  46 : defined(s$1) -> defined(queue(del_min(s$1))),s$1=empty [condensement of 45]
  51 + s$9=empty ->                                    [reduction of 43 by [L]]
  52 : defined(A),~ (insert(s$1,s$1)=empty)and defined(s$1)=>defined(queue(del_min(insert(s$1,s$1)))) -> defined(queue(del_min(A))),A=empty [expansion from 40]
  57 : defined(A) -> defined(queue(del_min(A))),A=empty,~ (insert(s$1,s$1)=empty)and defined(s$1) [expansion from 52]
  58 : defined(A),defined(queue(del_min(insert(s$1,s$1)))) -> defined(queue(del_min(A))),A=empty [expansion from 52]
  63 : defined(A) -> defined(queue(del_min(A))),A=empty,defined(s$1) [expansion from 57]
  71 : defined(queue(pair(s$1,s$1))),s$1=<elem(del_min(s$1)),defined(A) -> s$1=empty,defined(queue(del_min(A))),A=empty [negative chaining of 15 from 58]
  74 : defined(queue(pair(insert(queue(del_min(s$1)),s$1),elem(del_min(s$1))))),elem(del_min(s$1))<s$1,defined(A) -> s$1=empty,defined(queue(del_min(A))),A=empty [negative chaining of 16 from 58]
  78 : defined(queue(pair(s$1,s$1))),defined(A) -> elem(del_min(s$1))<s$1,s$1=empty,defined(queue(del_min(A))),A=empty [totality resolution from 71]
  79 : defined(A) -> A=empty,defined(queue(del_min(A))),s$1=empty,elem(del_min(s$1))<s$1 [reduction of 78 by [8,63]]
  81 : defined(queue(pair(insert(queue(del_min(s$1)),s$1),elem(del_min(s$1))))),defined(A) -> s$1=<elem(del_min(s$1)),s$1=empty,defined(queue(del_min(A))),A=empty [totality resolution from 74]
  82 : defined(A),defined(queue(del_min(s$1))) -> A=empty,defined(queue(del_min(A))),s$1=empty [reduction of 81 by [8,20,79]]
  83 : defined(A),defined(queue(del_min(s$1))) -> s$1=empty,defined(queue(del_min(A))),A=empty [reduction of 82 by [L]]
  99 : defined(s$1),defined(A) -> s$1=empty,defined(queue(del_min(A))),s$1=empty,A=empty [negative chaining of 46 from 83]
 105 : defined(s$1),defined(A) -> defined(queue(del_min(A))),s$1=empty,A=empty [condensement of 99]
 106 : defined(A) -> A=empty,s$1=empty,defined(queue(del_min(A))) [reduction of 105 by [63]]
 117 : defined(queue(del_min(insert(empty,s$1)))),defined(A),defined(B) -> defined(queue(del_min(A))),A=empty,defined(queue(del_min(B))),B=empty [negative chaining of 106 from 58]
 129 : defined(queue(del_min(insert(empty,s$1)))),defined(A) -> defined(queue(del_min(A))),A=empty [condensement of 117]
 130 : defined(A) -> A=empty,defined(queue(del_min(A))) [reduction of 129 by [12,8,19]]
 137 + defined(s$9) -> s$9=empty             [negative chaining of 130 from 38]
 144 + false                                    [reduction of 137 by [44,51,L]]

Length = 44, Depth = 22, Search Depth = 4



Total time: 3800 milliseconds

Number of forward inferences: 40
Number of tableau inferences: 29
Number of generated clauses: 144
Number of kept clauses: 55
yes
| ?-