initialize
call initialize-database
define sort bool with constructors
    true :  --> bool
    false :  --> bool
    .
declare constructor variables b : bool.
assume
    { b = true,
      b = false }
    bool-complete
call auto-strategy  bool-complete
call activate-lemma  bool-complete
define sort nat with constructors
    0 :  --> nat
    s : nat --> nat
    .
declare constructor variables w,x,y,z : nat.
declare operators
    1      :         --> nat
    2      :         --> nat
    plus   : nat nat --> nat
    times  : nat nat --> nat
    sqr    :     nat --> nat
    minus  : nat nat --> nat
    leq : nat nat --> bool
    .
assert one :
    1=s(0)
    .
call analyze-operator 1
call auto-strategy  1-def-auto
call activate-lemma  1-def-auto
assert two :
    2=s(1)
    .
call analyze-operator 2
call auto-strategy  2-def-auto
call activate-lemma  2-def-auto
assert plus1 :
    plus(x,0)=x
    .
assert plus2 :
    plus(x,s(y))=s(plus(x,y))
    .
call analyze-operator plus
call auto-strategy  plus-def-auto
call activate-lemma  plus-def-auto
assert times1 :
    times(x,0)=0
    .
assert times2 :
    times(x,s(y))=plus(times(x,y),x)
    .
call analyze-operator times
call auto-strategy  times-def-auto
call activate-lemma  times-def-auto
assert sqr1 :
    sqr(x)=times(x,x)
    .
call analyze-operator sqr
call auto-strategy  sqr-def-auto
call activate-lemma  sqr-def-auto
assert leq1 :
    leq(0,y)=true
    .
assert leq2 :
    leq(s(x),0)=false
    .
assert leq3 :
    leq(s(x),s(y))=leq(x,y)
    .
call analyze-operator leq
call auto-strategy  leq-def-auto
call activate-lemma  leq-def-auto
assert minus1 :
    minus(x,0)=x
    .
assert minus2 :
    minus(s(x),s(y))=minus(x,y)
    .
call analyze-operator minus
assume
    { def minus(x,y), leq(y,x)=/=true }
    minus-def
call auto-strategy  minus-def
call activate-lemma  minus-def
assume
    { plus(0,y)=y }
    plus3
call auto-strategy  plus3
call activate-lemma  plus3
assume
    { plus(s(x),y)=s(plus(x,y)) }
    plus4
call auto-strategy  plus4
call activate-lemma  plus4
assume
    { plus(x,y)=plus(y,x) }
    plus-commutative
call auto-strategy  plus-commutative
call activate-lemma  plus-commutative
assume
    { plus(x,plus(y,z))=plus(y,plus(x,z)) }
    plus-comm-ext
call auto-strategy  plus-comm-ext
call activate-lemma  plus-comm-ext
assume
    { plus(plus(x,y),z)=plus(x,plus(y,z)) }
    plus-associative
call auto-strategy  plus-associative
call activate-lemma  plus-associative
assume
    { times(0,y)=0 }
    times3
call auto-strategy  times3
call activate-lemma  times3
assume
    { times(s(x),y)=plus(times(x,y),y) }
    times4
call auto-strategy  times4
call activate-lemma  times4
assume
    { times(2,x)=plus(x,x) }
    times-2-x
call auto-strategy  times-2-x
call activate-lemma  times-2-x
assume
    { times(plus(x,y),z)=plus(times(x,z),times(y,z)) }
    times-plus-distributive-1
call auto-strategy  times-plus-distributive-1
call activate-lemma  times-plus-distributive-1
assume
    { times(x,plus(y,z))=plus(times(x,y),times(x,z)) }
    times-plus-distributive-2
call auto-strategy  times-plus-distributive-2
call activate-lemma  times-plus-distributive-2
assume
    { times(x,y)=times(y,x) }
    times-commutative
call auto-strategy  times-commutative
call activate-lemma  times-commutative
assume
    { times(x,times(y,z))=times(y,times(x,z)) }
    times-comm-ext
call auto-strategy  times-comm-ext
call activate-lemma  times-comm-ext
assume
    { times(times(x,y),z)=times(x, times(y,z)) }
    times-associative
call auto-strategy  times-associative
call activate-lemma  times-associative
assume
    { leq(x,x)=true }
    leq-reflexive
call auto-strategy  leq-reflexive
call activate-lemma  leq-reflexive
assume
    { leq(s(x),x)=/=true }
    leq-sx-x
call auto-strategy  leq-sx-x
call activate-lemma  leq-sx-x
assume
    { leq(x,z)=true,
      leq(x,y)=/=true,
      leq(y,z)=/=true }
    leq-transitive
call auto-strategy  leq-transitive
//call activate-lemma  leq-transitive
assume
    { leq(x,s(y))=true,
      leq(x,y)=/=true }
    leq-s-monotonic
call auto-strategy  leq-s-monotonic
call activate-lemma  leq-s-monotonic
assume
    { leq(x,plus(y,z))=true,
      leq(x,y)=/=true }
    leq-plus-monotonic-1
call auto-strategy  leq-plus-monotonic-1
call activate-lemma  leq-plus-monotonic-1
//assume
//    { leq(x,plus(z,y))=true,
//      leq(x,y)=/=true }
//    leq-plus-monotonic-2
//call simplify  leq-plus-monotonic-2
//call activate-lemma  leq-plus-monotonic-2
assume
    { leq(plus(w,x),plus(y,z))=true,
      leq(w,y)=/=true,
      leq(x,z)=/=true }
    leq-plus-monotonic
call auto-strategy  leq-plus-monotonic
call activate-lemma  leq-plus-monotonic
assume
    { leq(x,plus(x,y))=true }
    leq-x-plus-x-y
call simplify  leq-x-plus-x-y
call activate-lemma  leq-x-plus-x-y
assume
    { leq(plus(x,z),plus(y,z)) = leq(x,y) }
    leq-plus-plus-1
call auto-strategy  leq-plus-plus-1
call activate-lemma  leq-plus-plus-1
assume
    { leq(plus(z,x),plus(z,y)) = leq(x,y) }
    leq-plus-plus-2
call simplify  leq-plus-plus-2
call activate-lemma  leq-plus-plus-2
assume
    { leq(times(w,x),times(y,z))=true,
      leq(w,y)=/=true,
      leq(x,z)=/=true }
    leq-times-monotonic
call auto-strategy  leq-times-monotonic
call activate-lemma  leq-times-monotonic
assume
    { leq(plus(times(x,y),times(x,y)),plus(times(x,x),times(y,y))) = true }
    leq-plus-times
call variables-strategy  { y x } leq-plus-times
call activate-lemma  leq-plus-times
assume
    { leq(x,y)=true,
      leq(y,x)=true }
    leq-complete
call auto-strategy  leq-complete
call activate-lemma  leq-complete
assume
    { leq(y,x) = true,
       leq(s(x),y) = true }
    leq-complete-1
call auto-strategy  leq-complete-1
call activate-lemma  leq-complete-1
assume
    { leq(s(x),y)=/=true,
      x=/=y }
    unequal-from-leq-s
call auto-strategy  unequal-from-leq-s
call activate-lemma  unequal-from-leq-s
assume
    { minus(s(x),y)=s(minus(x,y)),
      leq(y,x)=/=true }
    minus3
call auto-strategy  minus3
call activate-lemma  minus3
assume
    { minus(plus(x,z),y)=plus(minus(x,y),z), leq(y,x)=/=true }
    minus-plus
call auto-strategy  minus-plus
call activate-lemma  minus-plus
assume
    { plus(minus(w,x),minus(y,z))=minus(plus(w,y),plus(x,z)),
      leq(x,w)=/=true,
      leq(z,y)=/=true
     }
    plus-minus-minus
call auto-strategy  plus-minus-minus
call activate-lemma  plus-minus-minus
call deactivate-lemmas { minus-plus }
assume
    { minus(plus(x,z),plus(y,z)) = minus(x,y) }
    minus-plus-plus-1
call auto-strategy  minus-plus-plus-1
call activate-lemma  minus-plus-plus-1
assume
    { minus(plus(z,x),plus(z,y))=minus(x,y) }
    minus-plus-plus-2
call simplify  minus-plus-plus-2
call activate-lemma  minus-plus-plus-2
assume
    { times(minus(x,y),minus(x,y)) = minus(plus(times(x,x),times(y,y)),plus(times(x,y),times(x,y))),
     leq(y,x)=/=true }
    times-minus-minus
call auto-strategy  times-minus-minus
call activate-lemma  times-minus-minus
assume
    { leq(s(0),times(y,y)) = true,
      y=0 }
    leq-s0-times
call auto-strategy  leq-s0-times
call activate-lemma  leq-s0-times
//assume
//    { minus(x,z)=minus(y,z),
//      x=/=y,
//      leq(z,x)=/=true }
//    minus-leq
//call auto-strategy  minus-leq
//call activate-lemma  minus-leq
assume
    { minus(x,y) =/= 0,
     leq(s(y),x) =/= true}
    minus-leq-sy-x
call auto-strategy  minus-leq-sy-x
call activate-lemma  minus-leq-sy-x
assume
    { x<y,
      leq(s(x),y)=/=true }
    leq-indord
call auto-strategy  leq-indord
call activate-lemma  leq-indord
assume
    { leq(minus(x,z),y) = leq(x,plus(y,z)),
      leq(z,x) =/= true }
    leq-minus-plus
call auto-strategy  leq-minus-plus
call activate-lemma  leq-minus-plus
assume
    { leq(s(x),plus(y,z))=true,
      leq(s(0),y) =/= true,
      leq(x,z) =/= true }
    leq-sx-plus-y-z
call auto-strategy  leq-sx-plus-y-z
call activate-lemma  leq-sx-plus-y-z
assume
    { leq(s(times(x,x)),plus(times(y,y),times(y,y))) = true,
      y = 0,
      leq(x,y) =/= true }
    leq-s-x2-2-y2
call simplify  leq-s-x2-2-y2
call activate-lemma  leq-s-x2-2-y2
assume
    { leq(plus(times(y,y),plus(times(y,y),plus(times(y,y),times(y,y)))),times(x,x)) = true,
      leq(plus(y,y),x) =/= true }
    leq-4y2-x2
apply lemma-subs
    leq-times-monotonic
    [w <-- plus(y,y) , y <-- x, x <-- plus(y,y) , z <-- x] ..
    leq-4y2-x2
call cont-proof-attempt :ind-lemmas {}  leq-4y2-x2
call activate-lemma  leq-4y2-x2
assume
    { leq(s(plus(times(y,y),times(y,y))),times(x,x)) = true,
      y = 0,
      leq(plus(y,y),x) =/= true }
    leq-s-2-y2-x2
apply lemma-subs
    leq-transitive
    [x <-- s(plus(times(y,y),times(y,y))), y<--times(plus(y,y),plus(y,y)) , z <-- times(x,x)] ..
    leq-s-2-y2-x2
call cont-proof-attempt :ind-lemmas {} leq-s-2-y2-x2 
call activate-lemma  leq-s-2-y2-x2
//assume
//    { times(plus(x,x),plus(x,x))=plus(times(x,x),plus(times(x,x),plus(times(x,x),times(x,x)))) }
//    times-2x2
//call simplify  times-2x2
//call activate-lemma  times-2x2
//assume
//    { plus(times(minus(x,y),minus(x,y)),times(minus(x,y),minus(x,y))) = times(minus(plus(y,y),x),minus(plus(y,y),x)),
//      plus(times(y,y),times(y,y)) =/= times(x,x),
//      leq(y,x) =/= true,
//      leq(x,plus(y,y)) =/= true }
//    2-minus-x-y-2
call deactivate-lemmas  { leq-plus-monotonic leq-plus-monotonic-1 leq-times-monotonic }
//call simplify  2-minus-x-y-2
//apply const-rewrite 12 13 [2:1:2:2:2] 2-minus-x-y-2
//call simplify  2-minus-x-y-2
//call activate-lemma  2-minus-x-y-2
assume
    { plus(times(y,y),times(y,y)) =/= times(x,x),
      y = 0 }
    neq-plus-2y2-x2
apply lit-add
    leq(x,y)=true
    leq(plus(y,y),x)=true
    . ..
    neq-plus-2y2-x2
apply lemma-subs
    unequal-from-leq-s
    [y <-- plus(times(y,y),times(y,y)) , x <-- times(x,x)] ..
    neq-plus-2y2-x2
set current g-node neq-plus-2y2-x2 [1^2]
call simplify-open-subgoals  neq-plus-2y2-x2
set current g-node neq-plus-2y2-x2 [1:2]
apply lemma-subs
    unequal-from-leq-s
    [x <-- plus(times(y,y),times(y,y)) , y <-- times(x,x)] ..
    neq-plus-2y2-x2
set current g-node neq-plus-2y2-x2 [1:2]
call simplify-open-subgoals  neq-plus-2y2-x2
set current g-node neq-plus-2y2-x2 [1:3]
apply lemma-subs
    leq-complete
    [y <-- plus(y,y) , x <-- x] ..
    neq-plus-2y2-x2
call simplify  neq-plus-2y2-x2
apply lemma-subs
    leq-complete
    [x <-- x , y <-- y] ..
    neq-plus-2y2-x2
apply ind-subs
    neq-plus-2y2-x2
    [ y<--minus(x,y), x<--minus(plus(y,y),x) ] ..
    neq-plus-2y2-x2
set current g-node neq-plus-2y2-x2 [1:3:1:2:1^2]
call simplify-open-subgoals  neq-plus-2y2-x2
set current g-node neq-plus-2y2-x2 [1:3:1:2:1^3:5]
set weight y neq-plus-2y2-x2
apply lemma-subs
    leq-indord
    [x <-- minus(x,y)] ..
    neq-plus-2y2-x2
apply lemma-rewrite
    1
    [1:1]
    minus3
    1
    [x <-- x , y <-- y] ..
    neq-plus-2y2-x2
apply lemma-rewrite
    1
    [1]
    leq-minus-plus
    1
    [x <-- s(x) , z <-- y , y <-- y] ..
    neq-plus-2y2-x2
call simplify  neq-plus-2y2-x2
call simplify  neq-plus-2y2-x2
call activate-lemma  neq-plus-2y2-x2
assume
    { times(2,sqr(y))=/=sqr(x), y=0 }
    sqrtirrat1
call simplify  sqrtirrat1