# Generated with Euler 27.035 on Mon Aug 06 00:26:42 GMT+02:00 2001
# for query http://www.agfa.com/w3c/euler/simulteq.lemma.n3
# given [http://www.agfa.com/w3c/euler/simulteq.axiom.n3]

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://www.agfa.com/w3c/euler/simulteq.axiom.n3#>.

 {{[ :lh
  [ :lh :1; :op
      :times; :rh :u]; :op :plus; :rh
      [ :rh :v; :op
          :times; :lh :1]] :is :5} :simult {[ :lh [ :lh :2; :op
      :times; :rh :u]; :op
      :plus; :rh [ :lh :4; :op
          :times; :rh :v]] :is
          :14}} log:implies
{{:u :is [ :lh [ :lh [ :lh :1; :op
      :times; :rh :14]; :op
      :minus; :rh [ :lh :4; :op
          :times; :rh :5]]; :op
      :slash; :rh [ :lh [ :lh :1; :op
          :times; :rh :2]; :op
          :minus; :rh [ :lh :4; :op
              :times; :rh :1]]]} :simult {:v :is
      [ :lh [ :lh [ :lh :1; :op
          :times; :rh :14]; :op
          :minus; :rh [ :lh :2; :op
              :times; :rh :5]]; :op
          :slash; :rh [ :lh [ :lh :1; :op
              :times; :rh :4]; :op
              :minus; :rh [ :lh :2; :op
                  :times; :rh :1]]]}}.

# Proof found for http://www.agfa.com/w3c/euler/simulteq.lemma.n3 in 4 steps (947 steps/sec)