%------------------------------------------------------------------------------
% File       : Vampire---4.3
% Problem    : ALG043+1 : TPTP v7.1.0. Released v2.7.0.
% Transform  : none
% Format     : tptp:raw
% Command    : vampire --mode casc -t %d %s

% Computer   : n157.star.cs.uiowa.edu
% Model      : x86_64 x86_64
% CPU        : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory     : 32218.625MB
% OS         : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit   : 300s
% DateTime   : Tue Sep  4 10:09:56 EDT 2018

% Result     : Theorem 0.08s
% Output     : Refutation 0.08s
% Verified   : 
% Statistics : Number of formulae       :  324 ( 567 expanded)
%              Number of leaves         :   50 ( 198 expanded)
%              Depth                    :   68
%              Number of atoms          : 3266 (4219 expanded)
%              Number of equality atoms : 1660 (2566 expanded)
%              Maximal formula depth    :   65 (   9 average)
%              Maximal term depth       :    2 (   1 average)

% Comments   : 
%------------------------------------------------------------------------------
%----WARNING: Vampire---4.3 format not known, defaulting to TPTP
fof(f2,axiom,
    ( e0 = op(e3,e3)
    & e1 = op(e3,e2)
    & e2 = op(e3,e1)
    & e3 = op(e3,e0)
    & e1 = op(e2,e3)
    & e0 = op(e2,e2)
    & e3 = op(e2,e1)
    & e2 = op(e2,e0)
    & e2 = op(e1,e3)
    & e3 = op(e1,e2)
    & e0 = op(e1,e1)
    & e1 = op(e1,e0)
    & e3 = op(e0,e3)
    & e2 = op(e0,e2)
    & e1 = op(e0,e1)
    & e0 = op(e0,e0) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).

fof(f3,axiom,(
    e0 = unit ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).

fof(f4,conjecture,
    ( ( e3 = op(e3,e3)
      | e3 = op(e2,e3)
      | e3 = op(e1,e3)
      | e3 = op(e0,e3) )
    & ( e3 = op(e3,e3)
      | e3 = op(e3,e2)
      | e3 = op(e3,e1)
      | e3 = op(e3,e0) )
    & ( e2 = op(e3,e3)
      | e2 = op(e2,e3)
      | e2 = op(e1,e3)
      | e2 = op(e0,e3) )
    & ( e2 = op(e3,e3)
      | e2 = op(e3,e2)
      | e2 = op(e3,e1)
      | e2 = op(e3,e0) )
    & ( e1 = op(e3,e3)
      | e1 = op(e2,e3)
      | e1 = op(e1,e3)
      | e1 = op(e0,e3) )
    & ( e1 = op(e3,e3)
      | e1 = op(e3,e2)
      | e1 = op(e3,e1)
      | e1 = op(e3,e0) )
    & ( e0 = op(e3,e3)
      | e0 = op(e2,e3)
      | e0 = op(e1,e3)
      | e0 = op(e0,e3) )
    & ( e0 = op(e3,e3)
      | e0 = op(e3,e2)
      | e0 = op(e3,e1)
      | e0 = op(e3,e0) )
    & ( e3 = op(e3,e2)
      | e3 = op(e2,e2)
      | e3 = op(e1,e2)
      | e3 = op(e0,e2) )
    & ( e3 = op(e2,e3)
      | e3 = op(e2,e2)
      | e3 = op(e2,e1)
      | e3 = op(e2,e0) )
    & ( e2 = op(e3,e2)
      | e2 = op(e2,e2)
      | e2 = op(e1,e2)
      | e2 = op(e0,e2) )
    & ( e2 = op(e2,e3)
      | e2 = op(e2,e2)
      | e2 = op(e2,e1)
      | e2 = op(e2,e0) )
    & ( e1 = op(e3,e2)
      | e1 = op(e2,e2)
      | e1 = op(e1,e2)
      | e1 = op(e0,e2) )
    & ( e1 = op(e2,e3)
      | e1 = op(e2,e2)
      | e1 = op(e2,e1)
      | e1 = op(e2,e0) )
    & ( e0 = op(e3,e2)
      | e0 = op(e2,e2)
      | e0 = op(e1,e2)
      | e0 = op(e0,e2) )
    & ( e0 = op(e2,e3)
      | e0 = op(e2,e2)
      | e0 = op(e2,e1)
      | e0 = op(e2,e0) )
    & ( e3 = op(e3,e1)
      | e3 = op(e2,e1)
      | e3 = op(e1,e1)
      | e3 = op(e0,e1) )
    & ( e3 = op(e1,e3)
      | e3 = op(e1,e2)
      | e3 = op(e1,e1)
      | e3 = op(e1,e0) )
    & ( e2 = op(e3,e1)
      | e2 = op(e2,e1)
      | e2 = op(e1,e1)
      | e2 = op(e0,e1) )
    & ( e2 = op(e1,e3)
      | e2 = op(e1,e2)
      | e2 = op(e1,e1)
      | e2 = op(e1,e0) )
    & ( e1 = op(e3,e1)
      | e1 = op(e2,e1)
      | e1 = op(e1,e1)
      | e1 = op(e0,e1) )
    & ( e1 = op(e1,e3)
      | e1 = op(e1,e2)
      | e1 = op(e1,e1)
      | e1 = op(e1,e0) )
    & ( e0 = op(e3,e1)
      | e0 = op(e2,e1)
      | e0 = op(e1,e1)
      | e0 = op(e0,e1) )
    & ( e0 = op(e1,e3)
      | e0 = op(e1,e2)
      | e0 = op(e1,e1)
      | e0 = op(e1,e0) )
    & ( e3 = op(e3,e0)
      | e3 = op(e2,e0)
      | e3 = op(e1,e0)
      | e3 = op(e0,e0) )
    & ( e3 = op(e0,e3)
      | e3 = op(e0,e2)
      | e3 = op(e0,e1)
      | e3 = op(e0,e0) )
    & ( e2 = op(e3,e0)
      | e2 = op(e2,e0)
      | e2 = op(e1,e0)
      | e2 = op(e0,e0) )
    & ( e2 = op(e0,e3)
      | e2 = op(e0,e2)
      | e2 = op(e0,e1)
      | e2 = op(e0,e0) )
    & ( e1 = op(e3,e0)
      | e1 = op(e2,e0)
      | e1 = op(e1,e0)
      | e1 = op(e0,e0) )
    & ( e1 = op(e0,e3)
      | e1 = op(e0,e2)
      | e1 = op(e0,e1)
      | e1 = op(e0,e0) )
    & ( e0 = op(e3,e0)
      | e0 = op(e2,e0)
      | e0 = op(e1,e0)
      | e0 = op(e0,e0) )
    & ( e0 = op(e0,e3)
      | e0 = op(e0,e2)
      | e0 = op(e0,e1)
      | e0 = op(e0,e0) )
    & ( e3 = unit
      | e2 = unit
      | e1 = unit
      | e0 = unit )
    & e3 = op(e3,unit)
    & e3 = op(unit,e3)
    & e2 = op(e2,unit)
    & e2 = op(unit,e2)
    & e1 = op(e1,unit)
    & e1 = op(unit,e1)
    & e0 = op(e0,unit)
    & e0 = op(unit,e0)
    & ( e3 = op(e3,e3)
      | e2 = op(e3,e3)
      | e1 = op(e3,e3)
      | e0 = op(e3,e3) )
    & ( e3 = op(e3,e2)
      | e2 = op(e3,e2)
      | e1 = op(e3,e2)
      | e0 = op(e3,e2) )
    & ( e3 = op(e3,e1)
      | e2 = op(e3,e1)
      | e1 = op(e3,e1)
      | e0 = op(e3,e1) )
    & ( e3 = op(e3,e0)
      | e2 = op(e3,e0)
      | e1 = op(e3,e0)
      | e0 = op(e3,e0) )
    & ( e3 = op(e2,e3)
      | e2 = op(e2,e3)
      | e1 = op(e2,e3)
      | e0 = op(e2,e3) )
    & ( e3 = op(e2,e2)
      | e2 = op(e2,e2)
      | e1 = op(e2,e2)
      | e0 = op(e2,e2) )
    & ( e3 = op(e2,e1)
      | e2 = op(e2,e1)
      | e1 = op(e2,e1)
      | e0 = op(e2,e1) )
    & ( e3 = op(e2,e0)
      | e2 = op(e2,e0)
      | e1 = op(e2,e0)
      | e0 = op(e2,e0) )
    & ( e3 = op(e1,e3)
      | e2 = op(e1,e3)
      | e1 = op(e1,e3)
      | e0 = op(e1,e3) )
    & ( e3 = op(e1,e2)
      | e2 = op(e1,e2)
      | e1 = op(e1,e2)
      | e0 = op(e1,e2) )
    & ( e3 = op(e1,e1)
      | e2 = op(e1,e1)
      | e1 = op(e1,e1)
      | e0 = op(e1,e1) )
    & ( e3 = op(e1,e0)
      | e2 = op(e1,e0)
      | e1 = op(e1,e0)
      | e0 = op(e1,e0) )
    & ( e3 = op(e0,e3)
      | e2 = op(e0,e3)
      | e1 = op(e0,e3)
      | e0 = op(e0,e3) )
    & ( e3 = op(e0,e2)
      | e2 = op(e0,e2)
      | e1 = op(e0,e2)
      | e0 = op(e0,e2) )
    & ( e3 = op(e0,e1)
      | e2 = op(e0,e1)
      | e1 = op(e0,e1)
      | e0 = op(e0,e1) )
    & ( e3 = op(e0,e0)
      | e2 = op(e0,e0)
      | e1 = op(e0,e0)
      | e0 = op(e0,e0) )
    & ( ( e3 = op(e3,e3)
        & e3 = op(e2,e2)
        & e3 = op(e1,e1)
        & e3 = op(e0,e0) )
      | ( e2 = op(e3,e3)
        & e2 = op(e2,e2)
        & e2 = op(e1,e1)
        & e2 = op(e0,e0) )
      | ( e1 = op(e3,e3)
        & e1 = op(e2,e2)
        & e1 = op(e1,e1)
        & e1 = op(e0,e0) )
      | ( e0 = op(e3,e3)
        & e0 = op(e2,e2)
        & e0 = op(e1,e1)
        & e0 = op(e0,e0) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).

fof(f5,negated_conjecture,(
    ~ ( ( e3 = op(e3,e3)
        | e3 = op(e2,e3)
        | e3 = op(e1,e3)
        | e3 = op(e0,e3) )
      & ( e3 = op(e3,e3)
        | e3 = op(e3,e2)
        | e3 = op(e3,e1)
        | e3 = op(e3,e0) )
      & ( e2 = op(e3,e3)
        | e2 = op(e2,e3)
        | e2 = op(e1,e3)
        | e2 = op(e0,e3) )
      & ( e2 = op(e3,e3)
        | e2 = op(e3,e2)
        | e2 = op(e3,e1)
        | e2 = op(e3,e0) )
      & ( e1 = op(e3,e3)
        | e1 = op(e2,e3)
        | e1 = op(e1,e3)
        | e1 = op(e0,e3) )
      & ( e1 = op(e3,e3)
        | e1 = op(e3,e2)
        | e1 = op(e3,e1)
        | e1 = op(e3,e0) )
      & ( e0 = op(e3,e3)
        | e0 = op(e2,e3)
        | e0 = op(e1,e3)
        | e0 = op(e0,e3) )
      & ( e0 = op(e3,e3)
        | e0 = op(e3,e2)
        | e0 = op(e3,e1)
        | e0 = op(e3,e0) )
      & ( e3 = op(e3,e2)
        | e3 = op(e2,e2)
        | e3 = op(e1,e2)
        | e3 = op(e0,e2) )
      & ( e3 = op(e2,e3)
        | e3 = op(e2,e2)
        | e3 = op(e2,e1)
        | e3 = op(e2,e0) )
      & ( e2 = op(e3,e2)
        | e2 = op(e2,e2)
        | e2 = op(e1,e2)
        | e2 = op(e0,e2) )
      & ( e2 = op(e2,e3)
        | e2 = op(e2,e2)
        | e2 = op(e2,e1)
        | e2 = op(e2,e0) )
      & ( e1 = op(e3,e2)
        | e1 = op(e2,e2)
        | e1 = op(e1,e2)
        | e1 = op(e0,e2) )
      & ( e1 = op(e2,e3)
        | e1 = op(e2,e2)
        | e1 = op(e2,e1)
        | e1 = op(e2,e0) )
      & ( e0 = op(e3,e2)
        | e0 = op(e2,e2)
        | e0 = op(e1,e2)
        | e0 = op(e0,e2) )
      & ( e0 = op(e2,e3)
        | e0 = op(e2,e2)
        | e0 = op(e2,e1)
        | e0 = op(e2,e0) )
      & ( e3 = op(e3,e1)
        | e3 = op(e2,e1)
        | e3 = op(e1,e1)
        | e3 = op(e0,e1) )
      & ( e3 = op(e1,e3)
        | e3 = op(e1,e2)
        | e3 = op(e1,e1)
        | e3 = op(e1,e0) )
      & ( e2 = op(e3,e1)
        | e2 = op(e2,e1)
        | e2 = op(e1,e1)
        | e2 = op(e0,e1) )
      & ( e2 = op(e1,e3)
        | e2 = op(e1,e2)
        | e2 = op(e1,e1)
        | e2 = op(e1,e0) )
      & ( e1 = op(e3,e1)
        | e1 = op(e2,e1)
        | e1 = op(e1,e1)
        | e1 = op(e0,e1) )
      & ( e1 = op(e1,e3)
        | e1 = op(e1,e2)
        | e1 = op(e1,e1)
        | e1 = op(e1,e0) )
      & ( e0 = op(e3,e1)
        | e0 = op(e2,e1)
        | e0 = op(e1,e1)
        | e0 = op(e0,e1) )
      & ( e0 = op(e1,e3)
        | e0 = op(e1,e2)
        | e0 = op(e1,e1)
        | e0 = op(e1,e0) )
      & ( e3 = op(e3,e0)
        | e3 = op(e2,e0)
        | e3 = op(e1,e0)
        | e3 = op(e0,e0) )
      & ( e3 = op(e0,e3)
        | e3 = op(e0,e2)
        | e3 = op(e0,e1)
        | e3 = op(e0,e0) )
      & ( e2 = op(e3,e0)
        | e2 = op(e2,e0)
        | e2 = op(e1,e0)
        | e2 = op(e0,e0) )
      & ( e2 = op(e0,e3)
        | e2 = op(e0,e2)
        | e2 = op(e0,e1)
        | e2 = op(e0,e0) )
      & ( e1 = op(e3,e0)
        | e1 = op(e2,e0)
        | e1 = op(e1,e0)
        | e1 = op(e0,e0) )
      & ( e1 = op(e0,e3)
        | e1 = op(e0,e2)
        | e1 = op(e0,e1)
        | e1 = op(e0,e0) )
      & ( e0 = op(e3,e0)
        | e0 = op(e2,e0)
        | e0 = op(e1,e0)
        | e0 = op(e0,e0) )
      & ( e0 = op(e0,e3)
        | e0 = op(e0,e2)
        | e0 = op(e0,e1)
        | e0 = op(e0,e0) )
      & ( e3 = unit
        | e2 = unit
        | e1 = unit
        | e0 = unit )
      & e3 = op(e3,unit)
      & e3 = op(unit,e3)
      & e2 = op(e2,unit)
      & e2 = op(unit,e2)
      & e1 = op(e1,unit)
      & e1 = op(unit,e1)
      & e0 = op(e0,unit)
      & e0 = op(unit,e0)
      & ( e3 = op(e3,e3)
        | e2 = op(e3,e3)
        | e1 = op(e3,e3)
        | e0 = op(e3,e3) )
      & ( e3 = op(e3,e2)
        | e2 = op(e3,e2)
        | e1 = op(e3,e2)
        | e0 = op(e3,e2) )
      & ( e3 = op(e3,e1)
        | e2 = op(e3,e1)
        | e1 = op(e3,e1)
        | e0 = op(e3,e1) )
      & ( e3 = op(e3,e0)
        | e2 = op(e3,e0)
        | e1 = op(e3,e0)
        | e0 = op(e3,e0) )
      & ( e3 = op(e2,e3)
        | e2 = op(e2,e3)
        | e1 = op(e2,e3)
        | e0 = op(e2,e3) )
      & ( e3 = op(e2,e2)
        | e2 = op(e2,e2)
        | e1 = op(e2,e2)
        | e0 = op(e2,e2) )
      & ( e3 = op(e2,e1)
        | e2 = op(e2,e1)
        | e1 = op(e2,e1)
        | e0 = op(e2,e1) )
      & ( e3 = op(e2,e0)
        | e2 = op(e2,e0)
        | e1 = op(e2,e0)
        | e0 = op(e2,e0) )
      & ( e3 = op(e1,e3)
        | e2 = op(e1,e3)
        | e1 = op(e1,e3)
        | e0 = op(e1,e3) )
      & ( e3 = op(e1,e2)
        | e2 = op(e1,e2)
        | e1 = op(e1,e2)
        | e0 = op(e1,e2) )
      & ( e3 = op(e1,e1)
        | e2 = op(e1,e1)
        | e1 = op(e1,e1)
        | e0 = op(e1,e1) )
      & ( e3 = op(e1,e0)
        | e2 = op(e1,e0)
        | e1 = op(e1,e0)
        | e0 = op(e1,e0) )
      & ( e3 = op(e0,e3)
        | e2 = op(e0,e3)
        | e1 = op(e0,e3)
        | e0 = op(e0,e3) )
      & ( e3 = op(e0,e2)
        | e2 = op(e0,e2)
        | e1 = op(e0,e2)
        | e0 = op(e0,e2) )
      & ( e3 = op(e0,e1)
        | e2 = op(e0,e1)
        | e1 = op(e0,e1)
        | e0 = op(e0,e1) )
      & ( e3 = op(e0,e0)
        | e2 = op(e0,e0)
        | e1 = op(e0,e0)
        | e0 = op(e0,e0) )
      & ( ( e3 = op(e3,e3)
          & e3 = op(e2,e2)
          & e3 = op(e1,e1)
          & e3 = op(e0,e0) )
        | ( e2 = op(e3,e3)
          & e2 = op(e2,e2)
          & e2 = op(e1,e1)
          & e2 = op(e0,e0) )
        | ( e1 = op(e3,e3)
          & e1 = op(e2,e2)
          & e1 = op(e1,e1)
          & e1 = op(e0,e0) )
        | ( e0 = op(e3,e3)
          & e0 = op(e2,e2)
          & e0 = op(e1,e1)
          & e0 = op(e0,e0) ) ) ) ),
    inference(negated_conjecture,[],[f4])).

fof(f6,plain,
    ( ( e3 != op(e3,e3)
      & e3 != op(e2,e3)
      & e3 != op(e1,e3)
      & e3 != op(e0,e3) )
    | ( e3 != op(e3,e3)
      & e3 != op(e3,e2)
      & e3 != op(e3,e1)
      & e3 != op(e3,e0) )
    | ( e2 != op(e3,e3)
      & e2 != op(e2,e3)
      & e2 != op(e1,e3)
      & e2 != op(e0,e3) )
    | ( e2 != op(e3,e3)
      & e2 != op(e3,e2)
      & e2 != op(e3,e1)
      & e2 != op(e3,e0) )
    | ( e1 != op(e3,e3)
      & e1 != op(e2,e3)
      & e1 != op(e1,e3)
      & e1 != op(e0,e3) )
    | ( e1 != op(e3,e3)
      & e1 != op(e3,e2)
      & e1 != op(e3,e1)
      & e1 != op(e3,e0) )
    | ( e0 != op(e3,e3)
      & e0 != op(e2,e3)
      & e0 != op(e1,e3)
      & e0 != op(e0,e3) )
    | ( e0 != op(e3,e3)
      & e0 != op(e3,e2)
      & e0 != op(e3,e1)
      & e0 != op(e3,e0) )
    | ( e3 != op(e3,e2)
      & e3 != op(e2,e2)
      & e3 != op(e1,e2)
      & e3 != op(e0,e2) )
    | ( e3 != op(e2,e3)
      & e3 != op(e2,e2)
      & e3 != op(e2,e1)
      & e3 != op(e2,e0) )
    | ( e2 != op(e3,e2)
      & e2 != op(e2,e2)
      & e2 != op(e1,e2)
      & e2 != op(e0,e2) )
    | ( e2 != op(e2,e3)
      & e2 != op(e2,e2)
      & e2 != op(e2,e1)
      & e2 != op(e2,e0) )
    | ( e1 != op(e3,e2)
      & e1 != op(e2,e2)
      & e1 != op(e1,e2)
      & e1 != op(e0,e2) )
    | ( e1 != op(e2,e3)
      & e1 != op(e2,e2)
      & e1 != op(e2,e1)
      & e1 != op(e2,e0) )
    | ( e0 != op(e3,e2)
      & e0 != op(e2,e2)
      & e0 != op(e1,e2)
      & e0 != op(e0,e2) )
    | ( e0 != op(e2,e3)
      & e0 != op(e2,e2)
      & e0 != op(e2,e1)
      & e0 != op(e2,e0) )
    | ( e3 != op(e3,e1)
      & e3 != op(e2,e1)
      & e3 != op(e1,e1)
      & e3 != op(e0,e1) )
    | ( e3 != op(e1,e3)
      & e3 != op(e1,e2)
      & e3 != op(e1,e1)
      & e3 != op(e1,e0) )
    | ( e2 != op(e3,e1)
      & e2 != op(e2,e1)
      & e2 != op(e1,e1)
      & e2 != op(e0,e1) )
    | ( e2 != op(e1,e3)
      & e2 != op(e1,e2)
      & e2 != op(e1,e1)
      & e2 != op(e1,e0) )
    | ( e1 != op(e3,e1)
      & e1 != op(e2,e1)
      & e1 != op(e1,e1)
      & e1 != op(e0,e1) )
    | ( e1 != op(e1,e3)
      & e1 != op(e1,e2)
      & e1 != op(e1,e1)
      & e1 != op(e1,e0) )
    | ( e0 != op(e3,e1)
      & e0 != op(e2,e1)
      & e0 != op(e1,e1)
      & e0 != op(e0,e1) )
    | ( e0 != op(e1,e3)
      & e0 != op(e1,e2)
      & e0 != op(e1,e1)
      & e0 != op(e1,e0) )
    | ( e3 != op(e3,e0)
      & e3 != op(e2,e0)
      & e3 != op(e1,e0)
      & e3 != op(e0,e0) )
    | ( e3 != op(e0,e3)
      & e3 != op(e0,e2)
      & e3 != op(e0,e1)
      & e3 != op(e0,e0) )
    | ( e2 != op(e3,e0)
      & e2 != op(e2,e0)
      & e2 != op(e1,e0)
      & e2 != op(e0,e0) )
    | ( e2 != op(e0,e3)
      & e2 != op(e0,e2)
      & e2 != op(e0,e1)
      & e2 != op(e0,e0) )
    | ( e1 != op(e3,e0)
      & e1 != op(e2,e0)
      & e1 != op(e1,e0)
      & e1 != op(e0,e0) )
    | ( e1 != op(e0,e3)
      & e1 != op(e0,e2)
      & e1 != op(e0,e1)
      & e1 != op(e0,e0) )
    | ( e0 != op(e3,e0)
      & e0 != op(e2,e0)
      & e0 != op(e1,e0)
      & e0 != op(e0,e0) )
    | ( e0 != op(e0,e3)
      & e0 != op(e0,e2)
      & e0 != op(e0,e1)
      & e0 != op(e0,e0) )
    | ( e3 != unit
      & e2 != unit
      & e1 != unit
      & e0 != unit )
    | e3 != op(e3,unit)
    | e3 != op(unit,e3)
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | e0 != op(e0,unit)
    | e0 != op(unit,e0)
    | ( e3 != op(e3,e3)
      & e2 != op(e3,e3)
      & e1 != op(e3,e3)
      & e0 != op(e3,e3) )
    | ( e3 != op(e3,e2)
      & e2 != op(e3,e2)
      & e1 != op(e3,e2)
      & e0 != op(e3,e2) )
    | ( e3 != op(e3,e1)
      & e2 != op(e3,e1)
      & e1 != op(e3,e1)
      & e0 != op(e3,e1) )
    | ( e3 != op(e3,e0)
      & e2 != op(e3,e0)
      & e1 != op(e3,e0)
      & e0 != op(e3,e0) )
    | ( e3 != op(e2,e3)
      & e2 != op(e2,e3)
      & e1 != op(e2,e3)
      & e0 != op(e2,e3) )
    | ( e3 != op(e2,e2)
      & e2 != op(e2,e2)
      & e1 != op(e2,e2)
      & e0 != op(e2,e2) )
    | ( e3 != op(e2,e1)
      & e2 != op(e2,e1)
      & e1 != op(e2,e1)
      & e0 != op(e2,e1) )
    | ( e3 != op(e2,e0)
      & e2 != op(e2,e0)
      & e1 != op(e2,e0)
      & e0 != op(e2,e0) )
    | ( e3 != op(e1,e3)
      & e2 != op(e1,e3)
      & e1 != op(e1,e3)
      & e0 != op(e1,e3) )
    | ( e3 != op(e1,e2)
      & e2 != op(e1,e2)
      & e1 != op(e1,e2)
      & e0 != op(e1,e2) )
    | ( e3 != op(e1,e1)
      & e2 != op(e1,e1)
      & e1 != op(e1,e1)
      & e0 != op(e1,e1) )
    | ( e3 != op(e1,e0)
      & e2 != op(e1,e0)
      & e1 != op(e1,e0)
      & e0 != op(e1,e0) )
    | ( e3 != op(e0,e3)
      & e2 != op(e0,e3)
      & e1 != op(e0,e3)
      & e0 != op(e0,e3) )
    | ( e3 != op(e0,e2)
      & e2 != op(e0,e2)
      & e1 != op(e0,e2)
      & e0 != op(e0,e2) )
    | ( e3 != op(e0,e1)
      & e2 != op(e0,e1)
      & e1 != op(e0,e1)
      & e0 != op(e0,e1) )
    | ( e3 != op(e0,e0)
      & e2 != op(e0,e0)
      & e1 != op(e0,e0)
      & e0 != op(e0,e0) )
    | ( ( e3 != op(e3,e3)
        | e3 != op(e2,e2)
        | e3 != op(e1,e1)
        | e3 != op(e0,e0) )
      & ( e2 != op(e3,e3)
        | e2 != op(e2,e2)
        | e2 != op(e1,e1)
        | e2 != op(e0,e0) )
      & ( e1 != op(e3,e3)
        | e1 != op(e2,e2)
        | e1 != op(e1,e1)
        | e1 != op(e0,e0) )
      & ( e0 != op(e3,e3)
        | e0 != op(e2,e2)
        | e0 != op(e1,e1)
        | e0 != op(e0,e0) ) ) ),
    inference(ennf_transformation,[],[f5])).

fof(f7,plain,
    ( ( ( e3 != op(e3,e3)
        | e3 != op(e2,e2)
        | e3 != op(e1,e1)
        | e3 != op(e0,e0) )
      & ( e2 != op(e3,e3)
        | e2 != op(e2,e2)
        | e2 != op(e1,e1)
        | e2 != op(e0,e0) )
      & ( e1 != op(e3,e3)
        | e1 != op(e2,e2)
        | e1 != op(e1,e1)
        | e1 != op(e0,e0) )
      & ( e0 != op(e3,e3)
        | e0 != op(e2,e2)
        | e0 != op(e1,e1)
        | e0 != op(e0,e0) ) )
    | ~ sP0 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP0])])).

fof(f8,plain,
    ( ( e3 != op(e0,e0)
      & e2 != op(e0,e0)
      & e1 != op(e0,e0)
      & e0 != op(e0,e0) )
    | ~ sP1 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP1])])).

fof(f9,plain,
    ( ( e3 != op(e0,e1)
      & e2 != op(e0,e1)
      & e1 != op(e0,e1)
      & e0 != op(e0,e1) )
    | ~ sP2 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP2])])).

fof(f10,plain,
    ( ( e3 != op(e0,e2)
      & e2 != op(e0,e2)
      & e1 != op(e0,e2)
      & e0 != op(e0,e2) )
    | ~ sP3 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP3])])).

fof(f11,plain,
    ( ( e3 != op(e0,e3)
      & e2 != op(e0,e3)
      & e1 != op(e0,e3)
      & e0 != op(e0,e3) )
    | ~ sP4 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP4])])).

fof(f12,plain,
    ( ( e3 != op(e1,e0)
      & e2 != op(e1,e0)
      & e1 != op(e1,e0)
      & e0 != op(e1,e0) )
    | ~ sP5 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP5])])).

fof(f13,plain,
    ( ( e3 != op(e1,e1)
      & e2 != op(e1,e1)
      & e1 != op(e1,e1)
      & e0 != op(e1,e1) )
    | ~ sP6 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP6])])).

fof(f14,plain,
    ( ( e3 != op(e1,e2)
      & e2 != op(e1,e2)
      & e1 != op(e1,e2)
      & e0 != op(e1,e2) )
    | ~ sP7 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP7])])).

fof(f15,plain,
    ( ( e3 != op(e1,e3)
      & e2 != op(e1,e3)
      & e1 != op(e1,e3)
      & e0 != op(e1,e3) )
    | ~ sP8 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP8])])).

fof(f16,plain,
    ( ( e3 != op(e2,e0)
      & e2 != op(e2,e0)
      & e1 != op(e2,e0)
      & e0 != op(e2,e0) )
    | ~ sP9 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP9])])).

fof(f17,plain,
    ( ( e3 != op(e2,e1)
      & e2 != op(e2,e1)
      & e1 != op(e2,e1)
      & e0 != op(e2,e1) )
    | ~ sP10 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP10])])).

fof(f18,plain,
    ( ( e3 != op(e2,e2)
      & e2 != op(e2,e2)
      & e1 != op(e2,e2)
      & e0 != op(e2,e2) )
    | ~ sP11 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP11])])).

fof(f19,plain,
    ( ( e3 != op(e2,e3)
      & e2 != op(e2,e3)
      & e1 != op(e2,e3)
      & e0 != op(e2,e3) )
    | ~ sP12 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP12])])).

fof(f20,plain,
    ( ( e3 != op(e3,e0)
      & e2 != op(e3,e0)
      & e1 != op(e3,e0)
      & e0 != op(e3,e0) )
    | ~ sP13 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP13])])).

fof(f21,plain,
    ( ( e3 != op(e3,e1)
      & e2 != op(e3,e1)
      & e1 != op(e3,e1)
      & e0 != op(e3,e1) )
    | ~ sP14 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP14])])).

fof(f22,plain,
    ( ( e3 != op(e3,e2)
      & e2 != op(e3,e2)
      & e1 != op(e3,e2)
      & e0 != op(e3,e2) )
    | ~ sP15 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP15])])).

fof(f23,plain,
    ( ( e3 != op(e3,e3)
      & e2 != op(e3,e3)
      & e1 != op(e3,e3)
      & e0 != op(e3,e3) )
    | ~ sP16 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP16])])).

fof(f24,plain,
    ( ( e3 != unit
      & e2 != unit
      & e1 != unit
      & e0 != unit )
    | ~ sP17 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP17])])).

fof(f25,plain,
    ( ( e0 != op(e0,e3)
      & e0 != op(e0,e2)
      & e0 != op(e0,e1)
      & e0 != op(e0,e0) )
    | ~ sP18 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP18])])).

fof(f26,plain,
    ( ( e0 != op(e3,e0)
      & e0 != op(e2,e0)
      & e0 != op(e1,e0)
      & e0 != op(e0,e0) )
    | ~ sP19 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP19])])).

fof(f27,plain,
    ( ( e1 != op(e0,e3)
      & e1 != op(e0,e2)
      & e1 != op(e0,e1)
      & e1 != op(e0,e0) )
    | ~ sP20 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP20])])).

fof(f28,plain,
    ( ( e1 != op(e3,e0)
      & e1 != op(e2,e0)
      & e1 != op(e1,e0)
      & e1 != op(e0,e0) )
    | ~ sP21 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP21])])).

fof(f29,plain,
    ( ( e2 != op(e0,e3)
      & e2 != op(e0,e2)
      & e2 != op(e0,e1)
      & e2 != op(e0,e0) )
    | ~ sP22 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP22])])).

fof(f30,plain,
    ( ( e2 != op(e3,e0)
      & e2 != op(e2,e0)
      & e2 != op(e1,e0)
      & e2 != op(e0,e0) )
    | ~ sP23 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP23])])).

fof(f31,plain,
    ( ( e3 != op(e0,e3)
      & e3 != op(e0,e2)
      & e3 != op(e0,e1)
      & e3 != op(e0,e0) )
    | ~ sP24 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP24])])).

fof(f32,plain,
    ( ( e3 != op(e3,e0)
      & e3 != op(e2,e0)
      & e3 != op(e1,e0)
      & e3 != op(e0,e0) )
    | ~ sP25 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP25])])).

fof(f33,plain,
    ( ( e0 != op(e1,e3)
      & e0 != op(e1,e2)
      & e0 != op(e1,e1)
      & e0 != op(e1,e0) )
    | ~ sP26 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP26])])).

fof(f34,plain,
    ( ( e0 != op(e3,e1)
      & e0 != op(e2,e1)
      & e0 != op(e1,e1)
      & e0 != op(e0,e1) )
    | ~ sP27 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP27])])).

fof(f35,plain,
    ( ( e1 != op(e1,e3)
      & e1 != op(e1,e2)
      & e1 != op(e1,e1)
      & e1 != op(e1,e0) )
    | ~ sP28 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP28])])).

fof(f36,plain,
    ( ( e1 != op(e3,e1)
      & e1 != op(e2,e1)
      & e1 != op(e1,e1)
      & e1 != op(e0,e1) )
    | ~ sP29 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP29])])).

fof(f37,plain,
    ( ( e2 != op(e1,e3)
      & e2 != op(e1,e2)
      & e2 != op(e1,e1)
      & e2 != op(e1,e0) )
    | ~ sP30 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP30])])).

fof(f38,plain,
    ( ( e2 != op(e3,e1)
      & e2 != op(e2,e1)
      & e2 != op(e1,e1)
      & e2 != op(e0,e1) )
    | ~ sP31 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP31])])).

fof(f39,plain,
    ( ( e3 != op(e1,e3)
      & e3 != op(e1,e2)
      & e3 != op(e1,e1)
      & e3 != op(e1,e0) )
    | ~ sP32 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP32])])).

fof(f40,plain,
    ( ( e3 != op(e3,e1)
      & e3 != op(e2,e1)
      & e3 != op(e1,e1)
      & e3 != op(e0,e1) )
    | ~ sP33 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP33])])).

fof(f41,plain,
    ( ( e0 != op(e2,e3)
      & e0 != op(e2,e2)
      & e0 != op(e2,e1)
      & e0 != op(e2,e0) )
    | ~ sP34 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP34])])).

fof(f42,plain,
    ( ( e0 != op(e3,e2)
      & e0 != op(e2,e2)
      & e0 != op(e1,e2)
      & e0 != op(e0,e2) )
    | ~ sP35 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP35])])).

fof(f43,plain,
    ( ( e1 != op(e2,e3)
      & e1 != op(e2,e2)
      & e1 != op(e2,e1)
      & e1 != op(e2,e0) )
    | ~ sP36 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP36])])).

fof(f44,plain,
    ( ( e1 != op(e3,e2)
      & e1 != op(e2,e2)
      & e1 != op(e1,e2)
      & e1 != op(e0,e2) )
    | ~ sP37 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP37])])).

fof(f45,plain,
    ( ( e2 != op(e2,e3)
      & e2 != op(e2,e2)
      & e2 != op(e2,e1)
      & e2 != op(e2,e0) )
    | ~ sP38 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP38])])).

fof(f46,plain,
    ( ( e2 != op(e3,e2)
      & e2 != op(e2,e2)
      & e2 != op(e1,e2)
      & e2 != op(e0,e2) )
    | ~ sP39 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP39])])).

fof(f47,plain,
    ( ( e3 != op(e2,e3)
      & e3 != op(e2,e2)
      & e3 != op(e2,e1)
      & e3 != op(e2,e0) )
    | ~ sP40 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP40])])).

fof(f48,plain,
    ( ( e3 != op(e3,e2)
      & e3 != op(e2,e2)
      & e3 != op(e1,e2)
      & e3 != op(e0,e2) )
    | ~ sP41 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP41])])).

fof(f49,plain,
    ( ( e0 != op(e3,e3)
      & e0 != op(e3,e2)
      & e0 != op(e3,e1)
      & e0 != op(e3,e0) )
    | ~ sP42 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP42])])).

fof(f50,plain,
    ( ( e0 != op(e3,e3)
      & e0 != op(e2,e3)
      & e0 != op(e1,e3)
      & e0 != op(e0,e3) )
    | ~ sP43 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP43])])).

fof(f51,plain,
    ( ( e1 != op(e3,e3)
      & e1 != op(e3,e2)
      & e1 != op(e3,e1)
      & e1 != op(e3,e0) )
    | ~ sP44 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP44])])).

fof(f52,plain,
    ( ( e1 != op(e3,e3)
      & e1 != op(e2,e3)
      & e1 != op(e1,e3)
      & e1 != op(e0,e3) )
    | ~ sP45 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP45])])).

fof(f53,plain,
    ( ( e2 != op(e3,e3)
      & e2 != op(e3,e2)
      & e2 != op(e3,e1)
      & e2 != op(e3,e0) )
    | ~ sP46 ),
    introduced(predicate_definition_introduction,[new_symbols(naming,[sP46])])).

fof(f54,plain,
    ( ( e3 != op(e3,e3)
      & e3 != op(e2,e3)
      & e3 != op(e1,e3)
      & e3 != op(e0,e3) )
    | ( e3 != op(e3,e3)
      & e3 != op(e3,e2)
      & e3 != op(e3,e1)
      & e3 != op(e3,e0) )
    | ( e2 != op(e3,e3)
      & e2 != op(e2,e3)
      & e2 != op(e1,e3)
      & e2 != op(e0,e3) )
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | sP18
    | sP17
    | e3 != op(e3,unit)
    | e3 != op(unit,e3)
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | e0 != op(e0,unit)
    | e0 != op(unit,e0)
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP1
    | sP0 ),
    inference(definition_folding,[],[f6,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7])).

fof(f55,plain,
    ( ( e2 != op(e3,e3)
      & e2 != op(e3,e2)
      & e2 != op(e3,e1)
      & e2 != op(e3,e0) )
    | ~ sP46 ),
    inference(nnf_transformation,[],[f53])).

fof(f56,plain,
    ( ( e1 != op(e3,e3)
      & e1 != op(e2,e3)
      & e1 != op(e1,e3)
      & e1 != op(e0,e3) )
    | ~ sP45 ),
    inference(nnf_transformation,[],[f52])).

fof(f57,plain,
    ( ( e1 != op(e3,e3)
      & e1 != op(e3,e2)
      & e1 != op(e3,e1)
      & e1 != op(e3,e0) )
    | ~ sP44 ),
    inference(nnf_transformation,[],[f51])).

fof(f58,plain,
    ( ( e0 != op(e3,e3)
      & e0 != op(e2,e3)
      & e0 != op(e1,e3)
      & e0 != op(e0,e3) )
    | ~ sP43 ),
    inference(nnf_transformation,[],[f50])).

fof(f59,plain,
    ( ( e0 != op(e3,e3)
      & e0 != op(e3,e2)
      & e0 != op(e3,e1)
      & e0 != op(e3,e0) )
    | ~ sP42 ),
    inference(nnf_transformation,[],[f49])).

fof(f60,plain,
    ( ( e3 != op(e3,e2)
      & e3 != op(e2,e2)
      & e3 != op(e1,e2)
      & e3 != op(e0,e2) )
    | ~ sP41 ),
    inference(nnf_transformation,[],[f48])).

fof(f61,plain,
    ( ( e3 != op(e2,e3)
      & e3 != op(e2,e2)
      & e3 != op(e2,e1)
      & e3 != op(e2,e0) )
    | ~ sP40 ),
    inference(nnf_transformation,[],[f47])).

fof(f62,plain,
    ( ( e2 != op(e3,e2)
      & e2 != op(e2,e2)
      & e2 != op(e1,e2)
      & e2 != op(e0,e2) )
    | ~ sP39 ),
    inference(nnf_transformation,[],[f46])).

fof(f63,plain,
    ( ( e2 != op(e2,e3)
      & e2 != op(e2,e2)
      & e2 != op(e2,e1)
      & e2 != op(e2,e0) )
    | ~ sP38 ),
    inference(nnf_transformation,[],[f45])).

fof(f64,plain,
    ( ( e1 != op(e3,e2)
      & e1 != op(e2,e2)
      & e1 != op(e1,e2)
      & e1 != op(e0,e2) )
    | ~ sP37 ),
    inference(nnf_transformation,[],[f44])).

fof(f65,plain,
    ( ( e1 != op(e2,e3)
      & e1 != op(e2,e2)
      & e1 != op(e2,e1)
      & e1 != op(e2,e0) )
    | ~ sP36 ),
    inference(nnf_transformation,[],[f43])).

fof(f66,plain,
    ( ( e0 != op(e3,e2)
      & e0 != op(e2,e2)
      & e0 != op(e1,e2)
      & e0 != op(e0,e2) )
    | ~ sP35 ),
    inference(nnf_transformation,[],[f42])).

fof(f67,plain,
    ( ( e0 != op(e2,e3)
      & e0 != op(e2,e2)
      & e0 != op(e2,e1)
      & e0 != op(e2,e0) )
    | ~ sP34 ),
    inference(nnf_transformation,[],[f41])).

fof(f68,plain,
    ( ( e3 != op(e3,e1)
      & e3 != op(e2,e1)
      & e3 != op(e1,e1)
      & e3 != op(e0,e1) )
    | ~ sP33 ),
    inference(nnf_transformation,[],[f40])).

fof(f69,plain,
    ( ( e3 != op(e1,e3)
      & e3 != op(e1,e2)
      & e3 != op(e1,e1)
      & e3 != op(e1,e0) )
    | ~ sP32 ),
    inference(nnf_transformation,[],[f39])).

fof(f70,plain,
    ( ( e2 != op(e3,e1)
      & e2 != op(e2,e1)
      & e2 != op(e1,e1)
      & e2 != op(e0,e1) )
    | ~ sP31 ),
    inference(nnf_transformation,[],[f38])).

fof(f71,plain,
    ( ( e2 != op(e1,e3)
      & e2 != op(e1,e2)
      & e2 != op(e1,e1)
      & e2 != op(e1,e0) )
    | ~ sP30 ),
    inference(nnf_transformation,[],[f37])).

fof(f72,plain,
    ( ( e1 != op(e3,e1)
      & e1 != op(e2,e1)
      & e1 != op(e1,e1)
      & e1 != op(e0,e1) )
    | ~ sP29 ),
    inference(nnf_transformation,[],[f36])).

fof(f73,plain,
    ( ( e1 != op(e1,e3)
      & e1 != op(e1,e2)
      & e1 != op(e1,e1)
      & e1 != op(e1,e0) )
    | ~ sP28 ),
    inference(nnf_transformation,[],[f35])).

fof(f74,plain,
    ( ( e0 != op(e3,e1)
      & e0 != op(e2,e1)
      & e0 != op(e1,e1)
      & e0 != op(e0,e1) )
    | ~ sP27 ),
    inference(nnf_transformation,[],[f34])).

fof(f75,plain,
    ( ( e0 != op(e1,e3)
      & e0 != op(e1,e2)
      & e0 != op(e1,e1)
      & e0 != op(e1,e0) )
    | ~ sP26 ),
    inference(nnf_transformation,[],[f33])).

fof(f76,plain,
    ( ( e3 != op(e3,e0)
      & e3 != op(e2,e0)
      & e3 != op(e1,e0)
      & e3 != op(e0,e0) )
    | ~ sP25 ),
    inference(nnf_transformation,[],[f32])).

fof(f77,plain,
    ( ( e3 != op(e0,e3)
      & e3 != op(e0,e2)
      & e3 != op(e0,e1)
      & e3 != op(e0,e0) )
    | ~ sP24 ),
    inference(nnf_transformation,[],[f31])).

fof(f78,plain,
    ( ( e2 != op(e3,e0)
      & e2 != op(e2,e0)
      & e2 != op(e1,e0)
      & e2 != op(e0,e0) )
    | ~ sP23 ),
    inference(nnf_transformation,[],[f30])).

fof(f79,plain,
    ( ( e2 != op(e0,e3)
      & e2 != op(e0,e2)
      & e2 != op(e0,e1)
      & e2 != op(e0,e0) )
    | ~ sP22 ),
    inference(nnf_transformation,[],[f29])).

fof(f80,plain,
    ( ( e1 != op(e3,e0)
      & e1 != op(e2,e0)
      & e1 != op(e1,e0)
      & e1 != op(e0,e0) )
    | ~ sP21 ),
    inference(nnf_transformation,[],[f28])).

fof(f81,plain,
    ( ( e1 != op(e0,e3)
      & e1 != op(e0,e2)
      & e1 != op(e0,e1)
      & e1 != op(e0,e0) )
    | ~ sP20 ),
    inference(nnf_transformation,[],[f27])).

fof(f82,plain,
    ( ( e0 != op(e3,e0)
      & e0 != op(e2,e0)
      & e0 != op(e1,e0)
      & e0 != op(e0,e0) )
    | ~ sP19 ),
    inference(nnf_transformation,[],[f26])).

fof(f83,plain,
    ( ( e0 != op(e0,e3)
      & e0 != op(e0,e2)
      & e0 != op(e0,e1)
      & e0 != op(e0,e0) )
    | ~ sP18 ),
    inference(nnf_transformation,[],[f25])).

fof(f84,plain,
    ( ( e3 != unit
      & e2 != unit
      & e1 != unit
      & e0 != unit )
    | ~ sP17 ),
    inference(nnf_transformation,[],[f24])).

fof(f85,plain,
    ( ( e3 != op(e3,e3)
      & e2 != op(e3,e3)
      & e1 != op(e3,e3)
      & e0 != op(e3,e3) )
    | ~ sP16 ),
    inference(nnf_transformation,[],[f23])).

fof(f86,plain,
    ( ( e3 != op(e3,e2)
      & e2 != op(e3,e2)
      & e1 != op(e3,e2)
      & e0 != op(e3,e2) )
    | ~ sP15 ),
    inference(nnf_transformation,[],[f22])).

fof(f87,plain,
    ( ( e3 != op(e3,e1)
      & e2 != op(e3,e1)
      & e1 != op(e3,e1)
      & e0 != op(e3,e1) )
    | ~ sP14 ),
    inference(nnf_transformation,[],[f21])).

fof(f88,plain,
    ( ( e3 != op(e3,e0)
      & e2 != op(e3,e0)
      & e1 != op(e3,e0)
      & e0 != op(e3,e0) )
    | ~ sP13 ),
    inference(nnf_transformation,[],[f20])).

fof(f89,plain,
    ( ( e3 != op(e2,e3)
      & e2 != op(e2,e3)
      & e1 != op(e2,e3)
      & e0 != op(e2,e3) )
    | ~ sP12 ),
    inference(nnf_transformation,[],[f19])).

fof(f90,plain,
    ( ( e3 != op(e2,e2)
      & e2 != op(e2,e2)
      & e1 != op(e2,e2)
      & e0 != op(e2,e2) )
    | ~ sP11 ),
    inference(nnf_transformation,[],[f18])).

fof(f91,plain,
    ( ( e3 != op(e2,e1)
      & e2 != op(e2,e1)
      & e1 != op(e2,e1)
      & e0 != op(e2,e1) )
    | ~ sP10 ),
    inference(nnf_transformation,[],[f17])).

fof(f92,plain,
    ( ( e3 != op(e2,e0)
      & e2 != op(e2,e0)
      & e1 != op(e2,e0)
      & e0 != op(e2,e0) )
    | ~ sP9 ),
    inference(nnf_transformation,[],[f16])).

fof(f93,plain,
    ( ( e3 != op(e1,e3)
      & e2 != op(e1,e3)
      & e1 != op(e1,e3)
      & e0 != op(e1,e3) )
    | ~ sP8 ),
    inference(nnf_transformation,[],[f15])).

fof(f94,plain,
    ( ( e3 != op(e1,e2)
      & e2 != op(e1,e2)
      & e1 != op(e1,e2)
      & e0 != op(e1,e2) )
    | ~ sP7 ),
    inference(nnf_transformation,[],[f14])).

fof(f95,plain,
    ( ( e3 != op(e1,e1)
      & e2 != op(e1,e1)
      & e1 != op(e1,e1)
      & e0 != op(e1,e1) )
    | ~ sP6 ),
    inference(nnf_transformation,[],[f13])).

fof(f96,plain,
    ( ( e3 != op(e1,e0)
      & e2 != op(e1,e0)
      & e1 != op(e1,e0)
      & e0 != op(e1,e0) )
    | ~ sP5 ),
    inference(nnf_transformation,[],[f12])).

fof(f97,plain,
    ( ( e3 != op(e0,e3)
      & e2 != op(e0,e3)
      & e1 != op(e0,e3)
      & e0 != op(e0,e3) )
    | ~ sP4 ),
    inference(nnf_transformation,[],[f11])).

fof(f98,plain,
    ( ( e3 != op(e0,e2)
      & e2 != op(e0,e2)
      & e1 != op(e0,e2)
      & e0 != op(e0,e2) )
    | ~ sP3 ),
    inference(nnf_transformation,[],[f10])).

fof(f99,plain,
    ( ( e3 != op(e0,e1)
      & e2 != op(e0,e1)
      & e1 != op(e0,e1)
      & e0 != op(e0,e1) )
    | ~ sP2 ),
    inference(nnf_transformation,[],[f9])).

fof(f100,plain,
    ( ( e3 != op(e0,e0)
      & e2 != op(e0,e0)
      & e1 != op(e0,e0)
      & e0 != op(e0,e0) )
    | ~ sP1 ),
    inference(nnf_transformation,[],[f8])).

fof(f101,plain,
    ( ( ( e3 != op(e3,e3)
        | e3 != op(e2,e2)
        | e3 != op(e1,e1)
        | e3 != op(e0,e0) )
      & ( e2 != op(e3,e3)
        | e2 != op(e2,e2)
        | e2 != op(e1,e1)
        | e2 != op(e0,e0) )
      & ( e1 != op(e3,e3)
        | e1 != op(e2,e2)
        | e1 != op(e1,e1)
        | e1 != op(e0,e0) )
      & ( e0 != op(e3,e3)
        | e0 != op(e2,e2)
        | e0 != op(e1,e1)
        | e0 != op(e0,e0) ) )
    | ~ sP0 ),
    inference(nnf_transformation,[],[f7])).

fof(f103,plain,
    ( e2 != op(e3,e1)
    | ~ sP46 ),
    inference(cnf_transformation,[],[f55])).

fof(f108,plain,
    ( e1 != op(e2,e3)
    | ~ sP45 ),
    inference(cnf_transformation,[],[f56])).

fof(f112,plain,
    ( e1 != op(e3,e2)
    | ~ sP44 ),
    inference(cnf_transformation,[],[f57])).

fof(f117,plain,
    ( e0 != op(e3,e3)
    | ~ sP43 ),
    inference(cnf_transformation,[],[f58])).

fof(f121,plain,
    ( e0 != op(e3,e3)
    | ~ sP42 ),
    inference(cnf_transformation,[],[f59])).

fof(f123,plain,
    ( e3 != op(e1,e2)
    | ~ sP41 ),
    inference(cnf_transformation,[],[f60])).

fof(f127,plain,
    ( e3 != op(e2,e1)
    | ~ sP40 ),
    inference(cnf_transformation,[],[f61])).

fof(f130,plain,
    ( e2 != op(e0,e2)
    | ~ sP39 ),
    inference(cnf_transformation,[],[f62])).

fof(f134,plain,
    ( e2 != op(e2,e0)
    | ~ sP38 ),
    inference(cnf_transformation,[],[f63])).

fof(f141,plain,
    ( e1 != op(e3,e2)
    | ~ sP37 ),
    inference(cnf_transformation,[],[f64])).

fof(f145,plain,
    ( e1 != op(e2,e3)
    | ~ sP36 ),
    inference(cnf_transformation,[],[f65])).

fof(f148,plain,
    ( e0 != op(e2,e2)
    | ~ sP35 ),
    inference(cnf_transformation,[],[f66])).

fof(f152,plain,
    ( e0 != op(e2,e2)
    | ~ sP34 ),
    inference(cnf_transformation,[],[f67])).

fof(f156,plain,
    ( e3 != op(e2,e1)
    | ~ sP33 ),
    inference(cnf_transformation,[],[f68])).

fof(f160,plain,
    ( e3 != op(e1,e2)
    | ~ sP32 ),
    inference(cnf_transformation,[],[f69])).

fof(f165,plain,
    ( e2 != op(e3,e1)
    | ~ sP31 ),
    inference(cnf_transformation,[],[f70])).

fof(f169,plain,
    ( e2 != op(e1,e3)
    | ~ sP30 ),
    inference(cnf_transformation,[],[f71])).

fof(f170,plain,
    ( e1 != op(e0,e1)
    | ~ sP29 ),
    inference(cnf_transformation,[],[f72])).

fof(f174,plain,
    ( e1 != op(e1,e0)
    | ~ sP28 ),
    inference(cnf_transformation,[],[f73])).

fof(f179,plain,
    ( e0 != op(e1,e1)
    | ~ sP27 ),
    inference(cnf_transformation,[],[f74])).

fof(f183,plain,
    ( e0 != op(e1,e1)
    | ~ sP26 ),
    inference(cnf_transformation,[],[f75])).

fof(f189,plain,
    ( e3 != op(e3,e0)
    | ~ sP25 ),
    inference(cnf_transformation,[],[f76])).

fof(f193,plain,
    ( e3 != op(e0,e3)
    | ~ sP24 ),
    inference(cnf_transformation,[],[f77])).

fof(f196,plain,
    ( e2 != op(e2,e0)
    | ~ sP23 ),
    inference(cnf_transformation,[],[f78])).

fof(f200,plain,
    ( e2 != op(e0,e2)
    | ~ sP22 ),
    inference(cnf_transformation,[],[f79])).

fof(f203,plain,
    ( e1 != op(e1,e0)
    | ~ sP21 ),
    inference(cnf_transformation,[],[f80])).

fof(f207,plain,
    ( e1 != op(e0,e1)
    | ~ sP20 ),
    inference(cnf_transformation,[],[f81])).

fof(f210,plain,
    ( e0 != op(e0,e0)
    | ~ sP19 ),
    inference(cnf_transformation,[],[f82])).

fof(f214,plain,
    ( e0 != op(e0,e0)
    | ~ sP18 ),
    inference(cnf_transformation,[],[f83])).

fof(f218,plain,
    ( e0 != unit
    | ~ sP17 ),
    inference(cnf_transformation,[],[f84])).

fof(f222,plain,
    ( e0 != op(e3,e3)
    | ~ sP16 ),
    inference(cnf_transformation,[],[f85])).

fof(f227,plain,
    ( e1 != op(e3,e2)
    | ~ sP15 ),
    inference(cnf_transformation,[],[f86])).

fof(f232,plain,
    ( e2 != op(e3,e1)
    | ~ sP14 ),
    inference(cnf_transformation,[],[f87])).

fof(f237,plain,
    ( e3 != op(e3,e0)
    | ~ sP13 ),
    inference(cnf_transformation,[],[f88])).

fof(f239,plain,
    ( e1 != op(e2,e3)
    | ~ sP12 ),
    inference(cnf_transformation,[],[f89])).

fof(f242,plain,
    ( e0 != op(e2,e2)
    | ~ sP11 ),
    inference(cnf_transformation,[],[f90])).

fof(f249,plain,
    ( e3 != op(e2,e1)
    | ~ sP10 ),
    inference(cnf_transformation,[],[f91])).

fof(f252,plain,
    ( e2 != op(e2,e0)
    | ~ sP9 ),
    inference(cnf_transformation,[],[f92])).

fof(f256,plain,
    ( e2 != op(e1,e3)
    | ~ sP8 ),
    inference(cnf_transformation,[],[f93])).

fof(f261,plain,
    ( e3 != op(e1,e2)
    | ~ sP7 ),
    inference(cnf_transformation,[],[f94])).

fof(f262,plain,
    ( e0 != op(e1,e1)
    | ~ sP6 ),
    inference(cnf_transformation,[],[f95])).

fof(f267,plain,
    ( e1 != op(e1,e0)
    | ~ sP5 ),
    inference(cnf_transformation,[],[f96])).

fof(f273,plain,
    ( e3 != op(e0,e3)
    | ~ sP4 ),
    inference(cnf_transformation,[],[f97])).

fof(f276,plain,
    ( e2 != op(e0,e2)
    | ~ sP3 ),
    inference(cnf_transformation,[],[f98])).

fof(f279,plain,
    ( e1 != op(e0,e1)
    | ~ sP2 ),
    inference(cnf_transformation,[],[f99])).

fof(f282,plain,
    ( e0 != op(e0,e0)
    | ~ sP1 ),
    inference(cnf_transformation,[],[f100])).

fof(f286,plain,
    ( e0 != op(e3,e3)
    | e0 != op(e2,e2)
    | e0 != op(e1,e1)
    | e0 != op(e0,e0)
    | ~ sP0 ),
    inference(cnf_transformation,[],[f101])).

fof(f291,plain,
    ( e3 != op(e0,e3)
    | e3 != op(e3,e0)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | sP18
    | sP17
    | e3 != op(e3,unit)
    | e3 != op(unit,e3)
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | e0 != op(e0,unit)
    | e0 != op(unit,e0)
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP1
    | sP0 ),
    inference(cnf_transformation,[],[f54])).

fof(f354,plain,(
    e0 = unit ),
    inference(cnf_transformation,[],[f3])).

fof(f361,plain,(
    e0 = op(e0,e0) ),
    inference(cnf_transformation,[],[f2])).

fof(f362,plain,(
    e1 = op(e0,e1) ),
    inference(cnf_transformation,[],[f2])).

fof(f363,plain,(
    e2 = op(e0,e2) ),
    inference(cnf_transformation,[],[f2])).

fof(f364,plain,(
    e3 = op(e0,e3) ),
    inference(cnf_transformation,[],[f2])).

fof(f365,plain,(
    e1 = op(e1,e0) ),
    inference(cnf_transformation,[],[f2])).

fof(f366,plain,(
    e0 = op(e1,e1) ),
    inference(cnf_transformation,[],[f2])).

fof(f367,plain,(
    e3 = op(e1,e2) ),
    inference(cnf_transformation,[],[f2])).

fof(f368,plain,(
    e2 = op(e1,e3) ),
    inference(cnf_transformation,[],[f2])).

fof(f369,plain,(
    e2 = op(e2,e0) ),
    inference(cnf_transformation,[],[f2])).

fof(f370,plain,(
    e3 = op(e2,e1) ),
    inference(cnf_transformation,[],[f2])).

fof(f371,plain,(
    e0 = op(e2,e2) ),
    inference(cnf_transformation,[],[f2])).

fof(f372,plain,(
    e1 = op(e2,e3) ),
    inference(cnf_transformation,[],[f2])).

fof(f373,plain,(
    e3 = op(e3,e0) ),
    inference(cnf_transformation,[],[f2])).

fof(f374,plain,(
    e2 = op(e3,e1) ),
    inference(cnf_transformation,[],[f2])).

fof(f375,plain,(
    e1 = op(e3,e2) ),
    inference(cnf_transformation,[],[f2])).

fof(f376,plain,(
    e0 = op(e3,e3) ),
    inference(cnf_transformation,[],[f2])).

fof(f380,plain,
    ( op(e3,e3) != unit
    | ~ sP43 ),
    inference(definition_unfolding,[],[f117,f354])).

fof(f384,plain,
    ( op(e3,e3) != unit
    | ~ sP42 ),
    inference(definition_unfolding,[],[f121,f354])).

fof(f390,plain,
    ( e2 != op(unit,e2)
    | ~ sP39 ),
    inference(definition_unfolding,[],[f130,f354])).

fof(f391,plain,
    ( e2 != op(e2,unit)
    | ~ sP38 ),
    inference(definition_unfolding,[],[f134,f354])).

fof(f395,plain,
    ( op(e2,e2) != unit
    | ~ sP35 ),
    inference(definition_unfolding,[],[f148,f354])).

fof(f399,plain,
    ( op(e2,e2) != unit
    | ~ sP34 ),
    inference(definition_unfolding,[],[f152,f354])).

fof(f406,plain,
    ( e1 != op(unit,e1)
    | ~ sP29 ),
    inference(definition_unfolding,[],[f170,f354])).

fof(f407,plain,
    ( e1 != op(e1,unit)
    | ~ sP28 ),
    inference(definition_unfolding,[],[f174,f354])).

fof(f410,plain,
    ( op(e1,e1) != unit
    | ~ sP27 ),
    inference(definition_unfolding,[],[f179,f354])).

fof(f414,plain,
    ( op(e1,e1) != unit
    | ~ sP26 ),
    inference(definition_unfolding,[],[f183,f354])).

fof(f416,plain,
    ( e3 != op(e3,unit)
    | ~ sP25 ),
    inference(definition_unfolding,[],[f189,f354])).

fof(f420,plain,
    ( e3 != op(unit,e3)
    | ~ sP24 ),
    inference(definition_unfolding,[],[f193,f354])).

fof(f425,plain,
    ( e2 != op(e2,unit)
    | ~ sP23 ),
    inference(definition_unfolding,[],[f196,f354])).

fof(f429,plain,
    ( e2 != op(unit,e2)
    | ~ sP22 ),
    inference(definition_unfolding,[],[f200,f354])).

fof(f434,plain,
    ( e1 != op(e1,unit)
    | ~ sP21 ),
    inference(definition_unfolding,[],[f203,f354])).

fof(f438,plain,
    ( e1 != op(unit,e1)
    | ~ sP20 ),
    inference(definition_unfolding,[],[f207,f354])).

fof(f443,plain,
    ( op(unit,unit) != unit
    | ~ sP19 ),
    inference(definition_unfolding,[],[f210,f354,f354,f354])).

fof(f447,plain,
    ( op(unit,unit) != unit
    | ~ sP18 ),
    inference(definition_unfolding,[],[f214,f354,f354,f354])).

fof(f448,plain,
    ( unit != unit
    | ~ sP17 ),
    inference(definition_unfolding,[],[f218,f354])).

fof(f449,plain,
    ( op(e3,e3) != unit
    | ~ sP16 ),
    inference(definition_unfolding,[],[f222,f354])).

fof(f452,plain,
    ( e3 != op(e3,unit)
    | ~ sP13 ),
    inference(definition_unfolding,[],[f237,f354])).

fof(f457,plain,
    ( op(e2,e2) != unit
    | ~ sP11 ),
    inference(definition_unfolding,[],[f242,f354])).

fof(f460,plain,
    ( e2 != op(e2,unit)
    | ~ sP9 ),
    inference(definition_unfolding,[],[f252,f354])).

fof(f465,plain,
    ( op(e1,e1) != unit
    | ~ sP6 ),
    inference(definition_unfolding,[],[f262,f354])).

fof(f468,plain,
    ( e1 != op(e1,unit)
    | ~ sP5 ),
    inference(definition_unfolding,[],[f267,f354])).

fof(f470,plain,
    ( e3 != op(unit,e3)
    | ~ sP4 ),
    inference(definition_unfolding,[],[f273,f354])).

fof(f475,plain,
    ( e2 != op(unit,e2)
    | ~ sP3 ),
    inference(definition_unfolding,[],[f276,f354])).

fof(f480,plain,
    ( e1 != op(unit,e1)
    | ~ sP2 ),
    inference(definition_unfolding,[],[f279,f354])).

fof(f485,plain,
    ( op(unit,unit) != unit
    | ~ sP1 ),
    inference(definition_unfolding,[],[f282,f354,f354,f354])).

fof(f489,plain,
    ( op(e3,e3) != unit
    | op(e2,e2) != unit
    | op(e1,e1) != unit
    | op(unit,unit) != unit
    | ~ sP0 ),
    inference(definition_unfolding,[],[f286,f354,f354,f354,f354,f354,f354])).

fof(f552,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | sP18
    | sP17
    | e3 != op(e3,unit)
    | e3 != op(unit,e3)
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP1
    | sP0 ),
    inference(definition_unfolding,[],[f291,f354,f354,f354,f354,f354,f354])).

fof(f557,plain,(
    op(e3,e3) = unit ),
    inference(definition_unfolding,[],[f376,f354])).

fof(f558,plain,(
    e3 = op(e3,unit) ),
    inference(definition_unfolding,[],[f373,f354])).

fof(f559,plain,(
    op(e2,e2) = unit ),
    inference(definition_unfolding,[],[f371,f354])).

fof(f560,plain,(
    e2 = op(e2,unit) ),
    inference(definition_unfolding,[],[f369,f354])).

fof(f561,plain,(
    op(e1,e1) = unit ),
    inference(definition_unfolding,[],[f366,f354])).

fof(f562,plain,(
    e1 = op(e1,unit) ),
    inference(definition_unfolding,[],[f365,f354])).

fof(f563,plain,(
    e3 = op(unit,e3) ),
    inference(definition_unfolding,[],[f364,f354])).

fof(f564,plain,(
    e2 = op(unit,e2) ),
    inference(definition_unfolding,[],[f363,f354])).

fof(f565,plain,(
    e1 = op(unit,e1) ),
    inference(definition_unfolding,[],[f362,f354])).

fof(f566,plain,(
    op(unit,unit) = unit ),
    inference(definition_unfolding,[],[f361,f354,f354,f354])).

fof(f568,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | sP18
    | sP17
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP1
    | sP0 ),
    inference(duplicate_literal_removal,[],[f552])).

fof(f631,plain,(
    ~ sP17 ),
    inference(trivial_inequality_removal,[],[f448])).

fof(f1912,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | sP18
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP1
    | sP0 ),
    inference(subsumption_resolution,[],[f568,f631])).

fof(f1913,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | sP18
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP0 ),
    inference(subsumption_resolution,[],[f1912,f485])).

fof(f1914,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | sP19
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP0 ),
    inference(subsumption_resolution,[],[f1913,f447])).

fof(f1915,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP29
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP0 ),
    inference(subsumption_resolution,[],[f1914,f443])).

fof(f1916,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | sP20
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP0 ),
    inference(subsumption_resolution,[],[f1915,f406])).

fof(f1917,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP2
    | sP0 ),
    inference(subsumption_resolution,[],[f1916,f438])).

fof(f1918,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP28
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP0 ),
    inference(subsumption_resolution,[],[f1917,f480])).

fof(f1919,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | sP21
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP0 ),
    inference(subsumption_resolution,[],[f1918,f407])).

fof(f1920,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP5
    | sP4
    | sP3
    | sP0 ),
    inference(subsumption_resolution,[],[f1919,f434])).

fof(f1921,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP39
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP4
    | sP3
    | sP0 ),
    inference(subsumption_resolution,[],[f1920,f468])).

fof(f1922,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | sP22
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP4
    | sP3
    | sP0 ),
    inference(subsumption_resolution,[],[f1921,f390])).

fof(f1923,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP4
    | sP3
    | sP0 ),
    inference(subsumption_resolution,[],[f1922,f429])).

fof(f1924,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP38
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1923,f475])).

fof(f1925,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | sP23
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1924,f391])).

fof(f1926,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP9
    | sP8
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1925,f425])).

fof(f1927,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP30
    | sP27
    | sP26
    | sP25
    | sP24
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP8
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1926,f460])).

fof(f1928,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | sP25
    | sP24
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP8
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1927,f169])).

fof(f1929,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | sP25
    | sP24
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1928,f256])).

fof(f1930,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | sP24
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP13
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1929,f416])).

fof(f1931,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | sP24
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1930,f452])).

fof(f1932,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP4
    | sP0 ),
    inference(subsumption_resolution,[],[f1931,f420])).

fof(f1933,plain,
    ( e3 != op(unit,e3)
    | e3 != op(e3,unit)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f1932,f470])).

fof(f1963,plain,
    ( unit != unit
    | ~ sP43 ),
    inference(backward_demodulation,[],[f557,f380])).

fof(f1964,plain,
    ( unit != unit
    | ~ sP42 ),
    inference(backward_demodulation,[],[f557,f384])).

fof(f1965,plain,
    ( unit != unit
    | ~ sP16 ),
    inference(backward_demodulation,[],[f557,f449])).

fof(f1969,plain,
    ( unit != unit
    | op(e2,e2) != unit
    | op(e1,e1) != unit
    | op(unit,unit) != unit
    | ~ sP0 ),
    inference(backward_demodulation,[],[f557,f489])).

fof(f1981,plain,
    ( op(e2,e2) != unit
    | op(e1,e1) != unit
    | op(unit,unit) != unit
    | ~ sP0 ),
    inference(trivial_inequality_removal,[],[f1969])).

fof(f1982,plain,(
    ~ sP16 ),
    inference(trivial_inequality_removal,[],[f1965])).

fof(f1983,plain,(
    ~ sP42 ),
    inference(trivial_inequality_removal,[],[f1964])).

fof(f1984,plain,(
    ~ sP43 ),
    inference(trivial_inequality_removal,[],[f1963])).

fof(f1986,plain,
    ( e1 != e1
    | ~ sP44 ),
    inference(backward_demodulation,[],[f375,f112])).

fof(f1989,plain,
    ( e1 != e1
    | ~ sP37 ),
    inference(backward_demodulation,[],[f375,f141])).

fof(f1990,plain,
    ( e1 != e1
    | ~ sP15 ),
    inference(backward_demodulation,[],[f375,f227])).

fof(f2000,plain,(
    ~ sP15 ),
    inference(trivial_inequality_removal,[],[f1990])).

fof(f2001,plain,(
    ~ sP37 ),
    inference(trivial_inequality_removal,[],[f1989])).

fof(f2002,plain,(
    ~ sP44 ),
    inference(trivial_inequality_removal,[],[f1986])).

fof(f2003,plain,
    ( e2 != e2
    | ~ sP46 ),
    inference(backward_demodulation,[],[f374,f103])).

fof(f2006,plain,
    ( e2 != e2
    | ~ sP31 ),
    inference(backward_demodulation,[],[f374,f165])).

fof(f2009,plain,
    ( e2 != e2
    | ~ sP14 ),
    inference(backward_demodulation,[],[f374,f232])).

fof(f2018,plain,(
    ~ sP14 ),
    inference(trivial_inequality_removal,[],[f2009])).

fof(f2019,plain,(
    ~ sP31 ),
    inference(trivial_inequality_removal,[],[f2006])).

fof(f2020,plain,(
    ~ sP46 ),
    inference(trivial_inequality_removal,[],[f2003])).

fof(f2035,plain,
    ( e3 != e3
    | e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(backward_demodulation,[],[f558,f1933])).

fof(f2036,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP46
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(trivial_inequality_removal,[],[f2035])).

fof(f2069,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP44
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2036,f2020])).

fof(f2070,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP43
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2069,f2002])).

fof(f2071,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP42
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2070,f1984])).

fof(f2072,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP37
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2071,f1983])).

fof(f2073,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP31
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2072,f2001])).

fof(f2074,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP16
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2073,f2019])).

fof(f2075,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP15
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2074,f1982])).

fof(f2076,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP14
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2075,f2000])).

fof(f2077,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(e2,unit)
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2076,f2018])).

fof(f2078,plain,
    ( e1 != e1
    | ~ sP45 ),
    inference(backward_demodulation,[],[f372,f108])).

fof(f2081,plain,
    ( e1 != e1
    | ~ sP36 ),
    inference(backward_demodulation,[],[f372,f145])).

fof(f2082,plain,
    ( e1 != e1
    | ~ sP12 ),
    inference(backward_demodulation,[],[f372,f239])).

fof(f2091,plain,(
    ~ sP12 ),
    inference(trivial_inequality_removal,[],[f2082])).

fof(f2092,plain,(
    ~ sP36 ),
    inference(trivial_inequality_removal,[],[f2081])).

fof(f2093,plain,(
    ~ sP45 ),
    inference(trivial_inequality_removal,[],[f2078])).

fof(f2103,plain,
    ( unit != unit
    | ~ sP35 ),
    inference(backward_demodulation,[],[f559,f395])).

fof(f2104,plain,
    ( unit != unit
    | ~ sP34 ),
    inference(backward_demodulation,[],[f559,f399])).

fof(f2105,plain,
    ( unit != unit
    | ~ sP11 ),
    inference(backward_demodulation,[],[f559,f457])).

fof(f2114,plain,
    ( unit != unit
    | op(e1,e1) != unit
    | op(unit,unit) != unit
    | ~ sP0 ),
    inference(backward_demodulation,[],[f559,f1981])).

fof(f2115,plain,
    ( op(e1,e1) != unit
    | op(unit,unit) != unit
    | ~ sP0 ),
    inference(trivial_inequality_removal,[],[f2114])).

fof(f2116,plain,(
    ~ sP11 ),
    inference(trivial_inequality_removal,[],[f2105])).

fof(f2117,plain,(
    ~ sP34 ),
    inference(trivial_inequality_removal,[],[f2104])).

fof(f2118,plain,(
    ~ sP35 ),
    inference(trivial_inequality_removal,[],[f2103])).

fof(f2119,plain,
    ( e3 != e3
    | ~ sP40 ),
    inference(backward_demodulation,[],[f370,f127])).

fof(f2122,plain,
    ( e3 != e3
    | ~ sP33 ),
    inference(backward_demodulation,[],[f370,f156])).

fof(f2127,plain,
    ( e3 != e3
    | ~ sP10 ),
    inference(backward_demodulation,[],[f370,f249])).

fof(f2135,plain,(
    ~ sP10 ),
    inference(trivial_inequality_removal,[],[f2127])).

fof(f2136,plain,(
    ~ sP33 ),
    inference(trivial_inequality_removal,[],[f2122])).

fof(f2137,plain,(
    ~ sP40 ),
    inference(trivial_inequality_removal,[],[f2119])).

fof(f2152,plain,
    ( e2 != e2
    | e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(backward_demodulation,[],[f560,f2077])).

fof(f2153,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP45
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(trivial_inequality_removal,[],[f2152])).

fof(f2159,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP40
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2153,f2093])).

fof(f2160,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP36
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2159,f2137])).

fof(f2161,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP35
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2160,f2092])).

fof(f2162,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP34
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2161,f2118])).

fof(f2163,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP33
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2162,f2117])).

fof(f2164,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP12
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2163,f2136])).

fof(f2165,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP11
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2164,f2091])).

fof(f2166,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP10
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2165,f2116])).

fof(f2167,plain,
    ( e3 != op(unit,e3)
    | e2 != op(e1,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2166,f2135])).

fof(f2178,plain,
    ( e2 != e2
    | e3 != op(unit,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(backward_demodulation,[],[f368,f2167])).

fof(f2179,plain,
    ( e3 != op(unit,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(e1,unit)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(trivial_inequality_removal,[],[f2178])).

fof(f2182,plain,
    ( e3 != e3
    | ~ sP41 ),
    inference(backward_demodulation,[],[f367,f123])).

fof(f2185,plain,
    ( e3 != e3
    | ~ sP32 ),
    inference(backward_demodulation,[],[f367,f160])).

fof(f2190,plain,
    ( e3 != e3
    | ~ sP7 ),
    inference(backward_demodulation,[],[f367,f261])).

fof(f2194,plain,(
    ~ sP7 ),
    inference(trivial_inequality_removal,[],[f2190])).

fof(f2195,plain,(
    ~ sP32 ),
    inference(trivial_inequality_removal,[],[f2185])).

fof(f2196,plain,(
    ~ sP41 ),
    inference(trivial_inequality_removal,[],[f2182])).

fof(f2206,plain,
    ( unit != unit
    | ~ sP27 ),
    inference(backward_demodulation,[],[f561,f410])).

fof(f2207,plain,
    ( unit != unit
    | ~ sP26 ),
    inference(backward_demodulation,[],[f561,f414])).

fof(f2208,plain,
    ( unit != unit
    | ~ sP6 ),
    inference(backward_demodulation,[],[f561,f465])).

fof(f2209,plain,
    ( unit != unit
    | op(unit,unit) != unit
    | ~ sP0 ),
    inference(backward_demodulation,[],[f561,f2115])).

fof(f2210,plain,
    ( op(unit,unit) != unit
    | ~ sP0 ),
    inference(trivial_inequality_removal,[],[f2209])).

fof(f2211,plain,(
    ~ sP6 ),
    inference(trivial_inequality_removal,[],[f2208])).

fof(f2212,plain,(
    ~ sP26 ),
    inference(trivial_inequality_removal,[],[f2207])).

fof(f2213,plain,(
    ~ sP27 ),
    inference(trivial_inequality_removal,[],[f2206])).

fof(f2226,plain,
    ( e1 != e1
    | e3 != op(unit,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(backward_demodulation,[],[f562,f2179])).

fof(f2227,plain,
    ( e3 != op(unit,e3)
    | sP41
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(trivial_inequality_removal,[],[f2226])).

fof(f2231,plain,
    ( e3 != op(unit,e3)
    | sP32
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2227,f2196])).

fof(f2232,plain,
    ( e3 != op(unit,e3)
    | sP27
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2231,f2195])).

fof(f2233,plain,
    ( e3 != op(unit,e3)
    | sP26
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2232,f2213])).

fof(f2234,plain,
    ( e3 != op(unit,e3)
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP7
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2233,f2212])).

fof(f2235,plain,
    ( e3 != op(unit,e3)
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP6
    | sP0 ),
    inference(subsumption_resolution,[],[f2234,f2194])).

fof(f2236,plain,
    ( e3 != op(unit,e3)
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit
    | sP0 ),
    inference(subsumption_resolution,[],[f2235,f2211])).

fof(f2237,plain,
    ( e3 != op(unit,e3)
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit ),
    inference(subsumption_resolution,[],[f2236,f2210])).

fof(f2248,plain,
    ( e3 != e3
    | e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit ),
    inference(backward_demodulation,[],[f563,f2237])).

fof(f2249,plain,
    ( e2 != op(unit,e2)
    | e1 != op(unit,e1)
    | op(unit,unit) != unit ),
    inference(trivial_inequality_removal,[],[f2248])).

fof(f2264,plain,
    ( e2 != e2
    | e1 != op(unit,e1)
    | op(unit,unit) != unit ),
    inference(backward_demodulation,[],[f564,f2249])).

fof(f2265,plain,
    ( e1 != op(unit,e1)
    | op(unit,unit) != unit ),
    inference(trivial_inequality_removal,[],[f2264])).

fof(f2281,plain,
    ( e1 != e1
    | op(unit,unit) != unit ),
    inference(backward_demodulation,[],[f565,f2265])).

fof(f2282,plain,(
    op(unit,unit) != unit ),
    inference(trivial_inequality_removal,[],[f2281])).

fof(f2286,plain,(
    $false ),
    inference(subsumption_resolution,[],[f566,f2282])).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem    : ALG043+1 : TPTP v7.1.0. Released v2.7.0.
% 0.00/0.04  % Command    : vampire --mode casc -t %d %s
% 0.03/0.24  % Computer   : n157.star.cs.uiowa.edu
% 0.03/0.24  % Model      : x86_64 x86_64
% 0.03/0.24  % CPU        : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.24  % Memory     : 32218.625MB
% 0.03/0.24  % OS         : Linux 3.10.0-693.2.2.el7.x86_64
% 0.03/0.24  % CPULimit   : 300
% 0.03/0.24  % DateTime   : Wed Aug 29 18:25:56 CDT 2018
% 0.03/0.24  % CPUTime    : 
% 0.08/0.28  % ott+1002_2_av=off:bd=preordered:irw=on:lma=on:nm=64:nwc=10:sp=reverse_arity:updr=off_2 on theBenchmark
% 0.08/0.45  % Refutation found. Thanks to Tanya!
% 0.08/0.45  % SZS status Theorem for theBenchmark
% 0.08/0.45  % SZS output start Proof for theBenchmark
% 0.08/0.45  fof(f2,axiom,(
% 0.08/0.45    e0 = op(e3,e3) & e1 = op(e3,e2) & e2 = op(e3,e1) & e3 = op(e3,e0) & e1 = op(e2,e3) & e0 = op(e2,e2) & e3 = op(e2,e1) & e2 = op(e2,e0) & e2 = op(e1,e3) & e3 = op(e1,e2) & e0 = op(e1,e1) & e1 = op(e1,e0) & e3 = op(e0,e3) & e2 = op(e0,e2) & e1 = op(e0,e1) & e0 = op(e0,e0)),
% 0.08/0.45    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)).
% 0.08/0.45  fof(f3,axiom,(
% 0.08/0.45    e0 = unit),
% 0.08/0.45    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)).
% 0.08/0.45  fof(f4,conjecture,(
% 0.08/0.45    (e3 = op(e3,e3) | e3 = op(e2,e3) | e3 = op(e1,e3) | e3 = op(e0,e3)) & (e3 = op(e3,e3) | e3 = op(e3,e2) | e3 = op(e3,e1) | e3 = op(e3,e0)) & (e2 = op(e3,e3) | e2 = op(e2,e3) | e2 = op(e1,e3) | e2 = op(e0,e3)) & (e2 = op(e3,e3) | e2 = op(e3,e2) | e2 = op(e3,e1) | e2 = op(e3,e0)) & (e1 = op(e3,e3) | e1 = op(e2,e3) | e1 = op(e1,e3) | e1 = op(e0,e3)) & (e1 = op(e3,e3) | e1 = op(e3,e2) | e1 = op(e3,e1) | e1 = op(e3,e0)) & (e0 = op(e3,e3) | e0 = op(e2,e3) | e0 = op(e1,e3) | e0 = op(e0,e3)) & (e0 = op(e3,e3) | e0 = op(e3,e2) | e0 = op(e3,e1) | e0 = op(e3,e0)) & (e3 = op(e3,e2) | e3 = op(e2,e2) | e3 = op(e1,e2) | e3 = op(e0,e2)) & (e3 = op(e2,e3) | e3 = op(e2,e2) | e3 = op(e2,e1) | e3 = op(e2,e0)) & (e2 = op(e3,e2) | e2 = op(e2,e2) | e2 = op(e1,e2) | e2 = op(e0,e2)) & (e2 = op(e2,e3) | e2 = op(e2,e2) | e2 = op(e2,e1) | e2 = op(e2,e0)) & (e1 = op(e3,e2) | e1 = op(e2,e2) | e1 = op(e1,e2) | e1 = op(e0,e2)) & (e1 = op(e2,e3) | e1 = op(e2,e2) | e1 = op(e2,e1) | e1 = op(e2,e0)) & (e0 = op(e3,e2) | e0 = op(e2,e2) | e0 = op(e1,e2) | e0 = op(e0,e2)) & (e0 = op(e2,e3) | e0 = op(e2,e2) | e0 = op(e2,e1) | e0 = op(e2,e0)) & (e3 = op(e3,e1) | e3 = op(e2,e1) | e3 = op(e1,e1) | e3 = op(e0,e1)) & (e3 = op(e1,e3) | e3 = op(e1,e2) | e3 = op(e1,e1) | e3 = op(e1,e0)) & (e2 = op(e3,e1) | e2 = op(e2,e1) | e2 = op(e1,e1) | e2 = op(e0,e1)) & (e2 = op(e1,e3) | e2 = op(e1,e2) | e2 = op(e1,e1) | e2 = op(e1,e0)) & (e1 = op(e3,e1) | e1 = op(e2,e1) | e1 = op(e1,e1) | e1 = op(e0,e1)) & (e1 = op(e1,e3) | e1 = op(e1,e2) | e1 = op(e1,e1) | e1 = op(e1,e0)) & (e0 = op(e3,e1) | e0 = op(e2,e1) | e0 = op(e1,e1) | e0 = op(e0,e1)) & (e0 = op(e1,e3) | e0 = op(e1,e2) | e0 = op(e1,e1) | e0 = op(e1,e0)) & (e3 = op(e3,e0) | e3 = op(e2,e0) | e3 = op(e1,e0) | e3 = op(e0,e0)) & (e3 = op(e0,e3) | e3 = op(e0,e2) | e3 = op(e0,e1) | e3 = op(e0,e0)) & (e2 = op(e3,e0) | e2 = op(e2,e0) | e2 = op(e1,e0) | e2 = op(e0,e0)) & (e2 = op(e0,e3) | e2 = op(e0,e2) | e2 = op(e0,e1) | e2 = op(e0,e0)) & (e1 = op(e3,e0) | e1 = op(e2,e0) | e1 = op(e1,e0) | e1 = op(e0,e0)) & (e1 = op(e0,e3) | e1 = op(e0,e2) | e1 = op(e0,e1) | e1 = op(e0,e0)) & (e0 = op(e3,e0) | e0 = op(e2,e0) | e0 = op(e1,e0) | e0 = op(e0,e0)) & (e0 = op(e0,e3) | e0 = op(e0,e2) | e0 = op(e0,e1) | e0 = op(e0,e0)) & (e3 = unit | e2 = unit | e1 = unit | e0 = unit) & e3 = op(e3,unit) & e3 = op(unit,e3) & e2 = op(e2,unit) & e2 = op(unit,e2) & e1 = op(e1,unit) & e1 = op(unit,e1) & e0 = op(e0,unit) & e0 = op(unit,e0) & (e3 = op(e3,e3) | e2 = op(e3,e3) | e1 = op(e3,e3) | e0 = op(e3,e3)) & (e3 = op(e3,e2) | e2 = op(e3,e2) | e1 = op(e3,e2) | e0 = op(e3,e2)) & (e3 = op(e3,e1) | e2 = op(e3,e1) | e1 = op(e3,e1) | e0 = op(e3,e1)) & (e3 = op(e3,e0) | e2 = op(e3,e0) | e1 = op(e3,e0) | e0 = op(e3,e0)) & (e3 = op(e2,e3) | e2 = op(e2,e3) | e1 = op(e2,e3) | e0 = op(e2,e3)) & (e3 = op(e2,e2) | e2 = op(e2,e2) | e1 = op(e2,e2) | e0 = op(e2,e2)) & (e3 = op(e2,e1) | e2 = op(e2,e1) | e1 = op(e2,e1) | e0 = op(e2,e1)) & (e3 = op(e2,e0) | e2 = op(e2,e0) | e1 = op(e2,e0) | e0 = op(e2,e0)) & (e3 = op(e1,e3) | e2 = op(e1,e3) | e1 = op(e1,e3) | e0 = op(e1,e3)) & (e3 = op(e1,e2) | e2 = op(e1,e2) | e1 = op(e1,e2) | e0 = op(e1,e2)) & (e3 = op(e1,e1) | e2 = op(e1,e1) | e1 = op(e1,e1) | e0 = op(e1,e1)) & (e3 = op(e1,e0) | e2 = op(e1,e0) | e1 = op(e1,e0) | e0 = op(e1,e0)) & (e3 = op(e0,e3) | e2 = op(e0,e3) | e1 = op(e0,e3) | e0 = op(e0,e3)) & (e3 = op(e0,e2) | e2 = op(e0,e2) | e1 = op(e0,e2) | e0 = op(e0,e2)) & (e3 = op(e0,e1) | e2 = op(e0,e1) | e1 = op(e0,e1) | e0 = op(e0,e1)) & (e3 = op(e0,e0) | e2 = op(e0,e0) | e1 = op(e0,e0) | e0 = op(e0,e0)) & ((e3 = op(e3,e3) & e3 = op(e2,e2) & e3 = op(e1,e1) & e3 = op(e0,e0)) | (e2 = op(e3,e3) & e2 = op(e2,e2) & e2 = op(e1,e1) & e2 = op(e0,e0)) | (e1 = op(e3,e3) & e1 = op(e2,e2) & e1 = op(e1,e1) & e1 = op(e0,e0)) | (e0 = op(e3,e3) & e0 = op(e2,e2) & e0 = op(e1,e1) & e0 = op(e0,e0)))),
% 0.08/0.45    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 0.08/0.45  fof(f5,negated_conjecture,(
% 0.08/0.45    ~((e3 = op(e3,e3) | e3 = op(e2,e3) | e3 = op(e1,e3) | e3 = op(e0,e3)) & (e3 = op(e3,e3) | e3 = op(e3,e2) | e3 = op(e3,e1) | e3 = op(e3,e0)) & (e2 = op(e3,e3) | e2 = op(e2,e3) | e2 = op(e1,e3) | e2 = op(e0,e3)) & (e2 = op(e3,e3) | e2 = op(e3,e2) | e2 = op(e3,e1) | e2 = op(e3,e0)) & (e1 = op(e3,e3) | e1 = op(e2,e3) | e1 = op(e1,e3) | e1 = op(e0,e3)) & (e1 = op(e3,e3) | e1 = op(e3,e2) | e1 = op(e3,e1) | e1 = op(e3,e0)) & (e0 = op(e3,e3) | e0 = op(e2,e3) | e0 = op(e1,e3) | e0 = op(e0,e3)) & (e0 = op(e3,e3) | e0 = op(e3,e2) | e0 = op(e3,e1) | e0 = op(e3,e0)) & (e3 = op(e3,e2) | e3 = op(e2,e2) | e3 = op(e1,e2) | e3 = op(e0,e2)) & (e3 = op(e2,e3) | e3 = op(e2,e2) | e3 = op(e2,e1) | e3 = op(e2,e0)) & (e2 = op(e3,e2) | e2 = op(e2,e2) | e2 = op(e1,e2) | e2 = op(e0,e2)) & (e2 = op(e2,e3) | e2 = op(e2,e2) | e2 = op(e2,e1) | e2 = op(e2,e0)) & (e1 = op(e3,e2) | e1 = op(e2,e2) | e1 = op(e1,e2) | e1 = op(e0,e2)) & (e1 = op(e2,e3) | e1 = op(e2,e2) | e1 = op(e2,e1) | e1 = op(e2,e0)) & (e0 = op(e3,e2) | e0 = op(e2,e2) | e0 = op(e1,e2) | e0 = op(e0,e2)) & (e0 = op(e2,e3) | e0 = op(e2,e2) | e0 = op(e2,e1) | e0 = op(e2,e0)) & (e3 = op(e3,e1) | e3 = op(e2,e1) | e3 = op(e1,e1) | e3 = op(e0,e1)) & (e3 = op(e1,e3) | e3 = op(e1,e2) | e3 = op(e1,e1) | e3 = op(e1,e0)) & (e2 = op(e3,e1) | e2 = op(e2,e1) | e2 = op(e1,e1) | e2 = op(e0,e1)) & (e2 = op(e1,e3) | e2 = op(e1,e2) | e2 = op(e1,e1) | e2 = op(e1,e0)) & (e1 = op(e3,e1) | e1 = op(e2,e1) | e1 = op(e1,e1) | e1 = op(e0,e1)) & (e1 = op(e1,e3) | e1 = op(e1,e2) | e1 = op(e1,e1) | e1 = op(e1,e0)) & (e0 = op(e3,e1) | e0 = op(e2,e1) | e0 = op(e1,e1) | e0 = op(e0,e1)) & (e0 = op(e1,e3) | e0 = op(e1,e2) | e0 = op(e1,e1) | e0 = op(e1,e0)) & (e3 = op(e3,e0) | e3 = op(e2,e0) | e3 = op(e1,e0) | e3 = op(e0,e0)) & (e3 = op(e0,e3) | e3 = op(e0,e2) | e3 = op(e0,e1) | e3 = op(e0,e0)) & (e2 = op(e3,e0) | e2 = op(e2,e0) | e2 = op(e1,e0) | e2 = op(e0,e0)) & (e2 = op(e0,e3) | e2 = op(e0,e2) | e2 = op(e0,e1) | e2 = op(e0,e0)) & (e1 = op(e3,e0) | e1 = op(e2,e0) | e1 = op(e1,e0) | e1 = op(e0,e0)) & (e1 = op(e0,e3) | e1 = op(e0,e2) | e1 = op(e0,e1) | e1 = op(e0,e0)) & (e0 = op(e3,e0) | e0 = op(e2,e0) | e0 = op(e1,e0) | e0 = op(e0,e0)) & (e0 = op(e0,e3) | e0 = op(e0,e2) | e0 = op(e0,e1) | e0 = op(e0,e0)) & (e3 = unit | e2 = unit | e1 = unit | e0 = unit) & e3 = op(e3,unit) & e3 = op(unit,e3) & e2 = op(e2,unit) & e2 = op(unit,e2) & e1 = op(e1,unit) & e1 = op(unit,e1) & e0 = op(e0,unit) & e0 = op(unit,e0) & (e3 = op(e3,e3) | e2 = op(e3,e3) | e1 = op(e3,e3) | e0 = op(e3,e3)) & (e3 = op(e3,e2) | e2 = op(e3,e2) | e1 = op(e3,e2) | e0 = op(e3,e2)) & (e3 = op(e3,e1) | e2 = op(e3,e1) | e1 = op(e3,e1) | e0 = op(e3,e1)) & (e3 = op(e3,e0) | e2 = op(e3,e0) | e1 = op(e3,e0) | e0 = op(e3,e0)) & (e3 = op(e2,e3) | e2 = op(e2,e3) | e1 = op(e2,e3) | e0 = op(e2,e3)) & (e3 = op(e2,e2) | e2 = op(e2,e2) | e1 = op(e2,e2) | e0 = op(e2,e2)) & (e3 = op(e2,e1) | e2 = op(e2,e1) | e1 = op(e2,e1) | e0 = op(e2,e1)) & (e3 = op(e2,e0) | e2 = op(e2,e0) | e1 = op(e2,e0) | e0 = op(e2,e0)) & (e3 = op(e1,e3) | e2 = op(e1,e3) | e1 = op(e1,e3) | e0 = op(e1,e3)) & (e3 = op(e1,e2) | e2 = op(e1,e2) | e1 = op(e1,e2) | e0 = op(e1,e2)) & (e3 = op(e1,e1) | e2 = op(e1,e1) | e1 = op(e1,e1) | e0 = op(e1,e1)) & (e3 = op(e1,e0) | e2 = op(e1,e0) | e1 = op(e1,e0) | e0 = op(e1,e0)) & (e3 = op(e0,e3) | e2 = op(e0,e3) | e1 = op(e0,e3) | e0 = op(e0,e3)) & (e3 = op(e0,e2) | e2 = op(e0,e2) | e1 = op(e0,e2) | e0 = op(e0,e2)) & (e3 = op(e0,e1) | e2 = op(e0,e1) | e1 = op(e0,e1) | e0 = op(e0,e1)) & (e3 = op(e0,e0) | e2 = op(e0,e0) | e1 = op(e0,e0) | e0 = op(e0,e0)) & ((e3 = op(e3,e3) & e3 = op(e2,e2) & e3 = op(e1,e1) & e3 = op(e0,e0)) | (e2 = op(e3,e3) & e2 = op(e2,e2) & e2 = op(e1,e1) & e2 = op(e0,e0)) | (e1 = op(e3,e3) & e1 = op(e2,e2) & e1 = op(e1,e1) & e1 = op(e0,e0)) | (e0 = op(e3,e3) & e0 = op(e2,e2) & e0 = op(e1,e1) & e0 = op(e0,e0))))),
% 0.08/0.45    inference(negated_conjecture,[],[f4])).
% 0.08/0.45  fof(f6,plain,(
% 0.08/0.45    (e3 != op(e3,e3) & e3 != op(e2,e3) & e3 != op(e1,e3) & e3 != op(e0,e3)) | (e3 != op(e3,e3) & e3 != op(e3,e2) & e3 != op(e3,e1) & e3 != op(e3,e0)) | (e2 != op(e3,e3) & e2 != op(e2,e3) & e2 != op(e1,e3) & e2 != op(e0,e3)) | (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0)))),
% 0.08/0.45    inference(ennf_transformation,[],[f5])).
% 0.08/0.45  fof(f7,plain,(
% 0.08/0.45    ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0))) | ~sP0),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP0])])).
% 0.08/0.45  fof(f8,plain,(
% 0.08/0.45    (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ~sP1),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP1])])).
% 0.08/0.45  fof(f9,plain,(
% 0.08/0.45    (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | ~sP2),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP2])])).
% 0.08/0.45  fof(f10,plain,(
% 0.08/0.45    (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | ~sP3),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP3])])).
% 0.08/0.45  fof(f11,plain,(
% 0.08/0.45    (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | ~sP4),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP4])])).
% 0.08/0.45  fof(f12,plain,(
% 0.08/0.45    (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | ~sP5),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP5])])).
% 0.08/0.45  fof(f13,plain,(
% 0.08/0.45    (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | ~sP6),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP6])])).
% 0.08/0.45  fof(f14,plain,(
% 0.08/0.45    (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | ~sP7),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP7])])).
% 0.08/0.45  fof(f15,plain,(
% 0.08/0.45    (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | ~sP8),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP8])])).
% 0.08/0.45  fof(f16,plain,(
% 0.08/0.45    (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | ~sP9),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP9])])).
% 0.08/0.45  fof(f17,plain,(
% 0.08/0.45    (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | ~sP10),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP10])])).
% 0.08/0.45  fof(f18,plain,(
% 0.08/0.45    (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | ~sP11),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP11])])).
% 0.08/0.45  fof(f19,plain,(
% 0.08/0.45    (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | ~sP12),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP12])])).
% 0.08/0.45  fof(f20,plain,(
% 0.08/0.45    (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | ~sP13),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP13])])).
% 0.08/0.45  fof(f21,plain,(
% 0.08/0.45    (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | ~sP14),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP14])])).
% 0.08/0.45  fof(f22,plain,(
% 0.08/0.45    (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | ~sP15),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP15])])).
% 0.08/0.45  fof(f23,plain,(
% 0.08/0.45    (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | ~sP16),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP16])])).
% 0.08/0.45  fof(f24,plain,(
% 0.08/0.45    (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | ~sP17),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP17])])).
% 0.08/0.45  fof(f25,plain,(
% 0.08/0.45    (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | ~sP18),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP18])])).
% 0.08/0.45  fof(f26,plain,(
% 0.08/0.45    (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | ~sP19),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP19])])).
% 0.08/0.45  fof(f27,plain,(
% 0.08/0.45    (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | ~sP20),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP20])])).
% 0.08/0.45  fof(f28,plain,(
% 0.08/0.45    (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | ~sP21),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP21])])).
% 0.08/0.45  fof(f29,plain,(
% 0.08/0.45    (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | ~sP22),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP22])])).
% 0.08/0.45  fof(f30,plain,(
% 0.08/0.45    (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | ~sP23),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP23])])).
% 0.08/0.45  fof(f31,plain,(
% 0.08/0.45    (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | ~sP24),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP24])])).
% 0.08/0.45  fof(f32,plain,(
% 0.08/0.45    (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | ~sP25),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP25])])).
% 0.08/0.45  fof(f33,plain,(
% 0.08/0.45    (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | ~sP26),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP26])])).
% 0.08/0.45  fof(f34,plain,(
% 0.08/0.45    (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | ~sP27),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP27])])).
% 0.08/0.45  fof(f35,plain,(
% 0.08/0.45    (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | ~sP28),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP28])])).
% 0.08/0.45  fof(f36,plain,(
% 0.08/0.45    (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | ~sP29),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP29])])).
% 0.08/0.45  fof(f37,plain,(
% 0.08/0.45    (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | ~sP30),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP30])])).
% 0.08/0.45  fof(f38,plain,(
% 0.08/0.45    (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | ~sP31),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP31])])).
% 0.08/0.45  fof(f39,plain,(
% 0.08/0.45    (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | ~sP32),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP32])])).
% 0.08/0.45  fof(f40,plain,(
% 0.08/0.45    (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | ~sP33),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP33])])).
% 0.08/0.45  fof(f41,plain,(
% 0.08/0.45    (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | ~sP34),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP34])])).
% 0.08/0.45  fof(f42,plain,(
% 0.08/0.45    (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | ~sP35),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP35])])).
% 0.08/0.45  fof(f43,plain,(
% 0.08/0.45    (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | ~sP36),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP36])])).
% 0.08/0.45  fof(f44,plain,(
% 0.08/0.45    (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | ~sP37),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP37])])).
% 0.08/0.45  fof(f45,plain,(
% 0.08/0.45    (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | ~sP38),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP38])])).
% 0.08/0.45  fof(f46,plain,(
% 0.08/0.45    (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | ~sP39),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP39])])).
% 0.08/0.45  fof(f47,plain,(
% 0.08/0.45    (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | ~sP40),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP40])])).
% 0.08/0.45  fof(f48,plain,(
% 0.08/0.45    (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | ~sP41),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP41])])).
% 0.08/0.45  fof(f49,plain,(
% 0.08/0.45    (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | ~sP42),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP42])])).
% 0.08/0.45  fof(f50,plain,(
% 0.08/0.45    (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | ~sP43),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP43])])).
% 0.08/0.45  fof(f51,plain,(
% 0.08/0.45    (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | ~sP44),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP44])])).
% 0.08/0.45  fof(f52,plain,(
% 0.08/0.45    (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | ~sP45),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP45])])).
% 0.08/0.45  fof(f53,plain,(
% 0.08/0.45    (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | ~sP46),
% 0.08/0.45    introduced(predicate_definition_introduction,[new_symbols(naming,[sP46])])).
% 0.08/0.45  fof(f54,plain,(
% 0.08/0.45    (e3 != op(e3,e3) & e3 != op(e2,e3) & e3 != op(e1,e3) & e3 != op(e0,e3)) | (e3 != op(e3,e3) & e3 != op(e3,e2) & e3 != op(e3,e1) & e3 != op(e3,e0)) | (e2 != op(e3,e3) & e2 != op(e2,e3) & e2 != op(e1,e3) & e2 != op(e0,e3)) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.45    inference(definition_folding,[],[f6,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7])).
% 0.08/0.45  fof(f55,plain,(
% 0.08/0.45    (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | ~sP46),
% 0.08/0.45    inference(nnf_transformation,[],[f53])).
% 0.08/0.45  fof(f56,plain,(
% 0.08/0.45    (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | ~sP45),
% 0.08/0.45    inference(nnf_transformation,[],[f52])).
% 0.08/0.45  fof(f57,plain,(
% 0.08/0.45    (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | ~sP44),
% 0.08/0.45    inference(nnf_transformation,[],[f51])).
% 0.08/0.45  fof(f58,plain,(
% 0.08/0.45    (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | ~sP43),
% 0.08/0.45    inference(nnf_transformation,[],[f50])).
% 0.08/0.45  fof(f59,plain,(
% 0.08/0.45    (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | ~sP42),
% 0.08/0.45    inference(nnf_transformation,[],[f49])).
% 0.08/0.46  fof(f60,plain,(
% 0.08/0.46    (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | ~sP41),
% 0.08/0.46    inference(nnf_transformation,[],[f48])).
% 0.08/0.46  fof(f61,plain,(
% 0.08/0.46    (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | ~sP40),
% 0.08/0.46    inference(nnf_transformation,[],[f47])).
% 0.08/0.46  fof(f62,plain,(
% 0.08/0.46    (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | ~sP39),
% 0.08/0.46    inference(nnf_transformation,[],[f46])).
% 0.08/0.46  fof(f63,plain,(
% 0.08/0.46    (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | ~sP38),
% 0.08/0.46    inference(nnf_transformation,[],[f45])).
% 0.08/0.46  fof(f64,plain,(
% 0.08/0.46    (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | ~sP37),
% 0.08/0.46    inference(nnf_transformation,[],[f44])).
% 0.08/0.46  fof(f65,plain,(
% 0.08/0.46    (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | ~sP36),
% 0.08/0.46    inference(nnf_transformation,[],[f43])).
% 0.08/0.46  fof(f66,plain,(
% 0.08/0.46    (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | ~sP35),
% 0.08/0.46    inference(nnf_transformation,[],[f42])).
% 0.08/0.46  fof(f67,plain,(
% 0.08/0.46    (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | ~sP34),
% 0.08/0.46    inference(nnf_transformation,[],[f41])).
% 0.08/0.46  fof(f68,plain,(
% 0.08/0.46    (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | ~sP33),
% 0.08/0.46    inference(nnf_transformation,[],[f40])).
% 0.08/0.46  fof(f69,plain,(
% 0.08/0.46    (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | ~sP32),
% 0.08/0.46    inference(nnf_transformation,[],[f39])).
% 0.08/0.46  fof(f70,plain,(
% 0.08/0.46    (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | ~sP31),
% 0.08/0.46    inference(nnf_transformation,[],[f38])).
% 0.08/0.46  fof(f71,plain,(
% 0.08/0.46    (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | ~sP30),
% 0.08/0.46    inference(nnf_transformation,[],[f37])).
% 0.08/0.46  fof(f72,plain,(
% 0.08/0.46    (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | ~sP29),
% 0.08/0.46    inference(nnf_transformation,[],[f36])).
% 0.08/0.46  fof(f73,plain,(
% 0.08/0.46    (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | ~sP28),
% 0.08/0.46    inference(nnf_transformation,[],[f35])).
% 0.08/0.46  fof(f74,plain,(
% 0.08/0.46    (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | ~sP27),
% 0.08/0.46    inference(nnf_transformation,[],[f34])).
% 0.08/0.46  fof(f75,plain,(
% 0.08/0.46    (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | ~sP26),
% 0.08/0.46    inference(nnf_transformation,[],[f33])).
% 0.08/0.46  fof(f76,plain,(
% 0.08/0.46    (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | ~sP25),
% 0.08/0.46    inference(nnf_transformation,[],[f32])).
% 0.08/0.46  fof(f77,plain,(
% 0.08/0.46    (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | ~sP24),
% 0.08/0.46    inference(nnf_transformation,[],[f31])).
% 0.08/0.46  fof(f78,plain,(
% 0.08/0.46    (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | ~sP23),
% 0.08/0.46    inference(nnf_transformation,[],[f30])).
% 0.08/0.46  fof(f79,plain,(
% 0.08/0.46    (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | ~sP22),
% 0.08/0.46    inference(nnf_transformation,[],[f29])).
% 0.08/0.46  fof(f80,plain,(
% 0.08/0.46    (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | ~sP21),
% 0.08/0.46    inference(nnf_transformation,[],[f28])).
% 0.08/0.46  fof(f81,plain,(
% 0.08/0.46    (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | ~sP20),
% 0.08/0.46    inference(nnf_transformation,[],[f27])).
% 0.08/0.46  fof(f82,plain,(
% 0.08/0.46    (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | ~sP19),
% 0.08/0.46    inference(nnf_transformation,[],[f26])).
% 0.08/0.46  fof(f83,plain,(
% 0.08/0.46    (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | ~sP18),
% 0.08/0.46    inference(nnf_transformation,[],[f25])).
% 0.08/0.46  fof(f84,plain,(
% 0.08/0.46    (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | ~sP17),
% 0.08/0.46    inference(nnf_transformation,[],[f24])).
% 0.08/0.46  fof(f85,plain,(
% 0.08/0.46    (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | ~sP16),
% 0.08/0.46    inference(nnf_transformation,[],[f23])).
% 0.08/0.46  fof(f86,plain,(
% 0.08/0.46    (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | ~sP15),
% 0.08/0.46    inference(nnf_transformation,[],[f22])).
% 0.08/0.46  fof(f87,plain,(
% 0.08/0.46    (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | ~sP14),
% 0.08/0.46    inference(nnf_transformation,[],[f21])).
% 0.08/0.46  fof(f88,plain,(
% 0.08/0.46    (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | ~sP13),
% 0.08/0.46    inference(nnf_transformation,[],[f20])).
% 0.08/0.46  fof(f89,plain,(
% 0.08/0.46    (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | ~sP12),
% 0.08/0.46    inference(nnf_transformation,[],[f19])).
% 0.08/0.46  fof(f90,plain,(
% 0.08/0.46    (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | ~sP11),
% 0.08/0.46    inference(nnf_transformation,[],[f18])).
% 0.08/0.46  fof(f91,plain,(
% 0.08/0.46    (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | ~sP10),
% 0.08/0.46    inference(nnf_transformation,[],[f17])).
% 0.08/0.46  fof(f92,plain,(
% 0.08/0.46    (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | ~sP9),
% 0.08/0.46    inference(nnf_transformation,[],[f16])).
% 0.08/0.46  fof(f93,plain,(
% 0.08/0.46    (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | ~sP8),
% 0.08/0.46    inference(nnf_transformation,[],[f15])).
% 0.08/0.46  fof(f94,plain,(
% 0.08/0.46    (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | ~sP7),
% 0.08/0.46    inference(nnf_transformation,[],[f14])).
% 0.08/0.46  fof(f95,plain,(
% 0.08/0.46    (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | ~sP6),
% 0.08/0.46    inference(nnf_transformation,[],[f13])).
% 0.08/0.46  fof(f96,plain,(
% 0.08/0.46    (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | ~sP5),
% 0.08/0.46    inference(nnf_transformation,[],[f12])).
% 0.08/0.46  fof(f97,plain,(
% 0.08/0.46    (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | ~sP4),
% 0.08/0.46    inference(nnf_transformation,[],[f11])).
% 0.08/0.46  fof(f98,plain,(
% 0.08/0.46    (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | ~sP3),
% 0.08/0.46    inference(nnf_transformation,[],[f10])).
% 0.08/0.46  fof(f99,plain,(
% 0.08/0.46    (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | ~sP2),
% 0.08/0.46    inference(nnf_transformation,[],[f9])).
% 0.08/0.46  fof(f100,plain,(
% 0.08/0.46    (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ~sP1),
% 0.08/0.46    inference(nnf_transformation,[],[f8])).
% 0.08/0.46  fof(f101,plain,(
% 0.08/0.46    ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0))) | ~sP0),
% 0.08/0.46    inference(nnf_transformation,[],[f7])).
% 0.08/0.46  fof(f103,plain,(
% 0.08/0.46    e2 != op(e3,e1) | ~sP46),
% 0.08/0.46    inference(cnf_transformation,[],[f55])).
% 0.08/0.46  fof(f108,plain,(
% 0.08/0.46    e1 != op(e2,e3) | ~sP45),
% 0.08/0.46    inference(cnf_transformation,[],[f56])).
% 0.08/0.46  fof(f112,plain,(
% 0.08/0.46    e1 != op(e3,e2) | ~sP44),
% 0.08/0.46    inference(cnf_transformation,[],[f57])).
% 0.08/0.46  fof(f117,plain,(
% 0.08/0.46    e0 != op(e3,e3) | ~sP43),
% 0.08/0.46    inference(cnf_transformation,[],[f58])).
% 0.08/0.46  fof(f121,plain,(
% 0.08/0.46    e0 != op(e3,e3) | ~sP42),
% 0.08/0.46    inference(cnf_transformation,[],[f59])).
% 0.08/0.46  fof(f123,plain,(
% 0.08/0.46    e3 != op(e1,e2) | ~sP41),
% 0.08/0.46    inference(cnf_transformation,[],[f60])).
% 0.08/0.46  fof(f127,plain,(
% 0.08/0.46    e3 != op(e2,e1) | ~sP40),
% 0.08/0.46    inference(cnf_transformation,[],[f61])).
% 0.08/0.46  fof(f130,plain,(
% 0.08/0.46    e2 != op(e0,e2) | ~sP39),
% 0.08/0.46    inference(cnf_transformation,[],[f62])).
% 0.08/0.46  fof(f134,plain,(
% 0.08/0.46    e2 != op(e2,e0) | ~sP38),
% 0.08/0.46    inference(cnf_transformation,[],[f63])).
% 0.08/0.46  fof(f141,plain,(
% 0.08/0.46    e1 != op(e3,e2) | ~sP37),
% 0.08/0.46    inference(cnf_transformation,[],[f64])).
% 0.08/0.46  fof(f145,plain,(
% 0.08/0.46    e1 != op(e2,e3) | ~sP36),
% 0.08/0.46    inference(cnf_transformation,[],[f65])).
% 0.08/0.46  fof(f148,plain,(
% 0.08/0.46    e0 != op(e2,e2) | ~sP35),
% 0.08/0.46    inference(cnf_transformation,[],[f66])).
% 0.08/0.46  fof(f152,plain,(
% 0.08/0.46    e0 != op(e2,e2) | ~sP34),
% 0.08/0.46    inference(cnf_transformation,[],[f67])).
% 0.08/0.46  fof(f156,plain,(
% 0.08/0.46    e3 != op(e2,e1) | ~sP33),
% 0.08/0.46    inference(cnf_transformation,[],[f68])).
% 0.08/0.46  fof(f160,plain,(
% 0.08/0.46    e3 != op(e1,e2) | ~sP32),
% 0.08/0.46    inference(cnf_transformation,[],[f69])).
% 0.08/0.46  fof(f165,plain,(
% 0.08/0.46    e2 != op(e3,e1) | ~sP31),
% 0.08/0.46    inference(cnf_transformation,[],[f70])).
% 0.08/0.46  fof(f169,plain,(
% 0.08/0.46    e2 != op(e1,e3) | ~sP30),
% 0.08/0.46    inference(cnf_transformation,[],[f71])).
% 0.08/0.46  fof(f170,plain,(
% 0.08/0.46    e1 != op(e0,e1) | ~sP29),
% 0.08/0.46    inference(cnf_transformation,[],[f72])).
% 0.08/0.46  fof(f174,plain,(
% 0.08/0.46    e1 != op(e1,e0) | ~sP28),
% 0.08/0.46    inference(cnf_transformation,[],[f73])).
% 0.08/0.46  fof(f179,plain,(
% 0.08/0.46    e0 != op(e1,e1) | ~sP27),
% 0.08/0.46    inference(cnf_transformation,[],[f74])).
% 0.08/0.46  fof(f183,plain,(
% 0.08/0.46    e0 != op(e1,e1) | ~sP26),
% 0.08/0.46    inference(cnf_transformation,[],[f75])).
% 0.08/0.46  fof(f189,plain,(
% 0.08/0.46    e3 != op(e3,e0) | ~sP25),
% 0.08/0.46    inference(cnf_transformation,[],[f76])).
% 0.08/0.46  fof(f193,plain,(
% 0.08/0.46    e3 != op(e0,e3) | ~sP24),
% 0.08/0.46    inference(cnf_transformation,[],[f77])).
% 0.08/0.46  fof(f196,plain,(
% 0.08/0.46    e2 != op(e2,e0) | ~sP23),
% 0.08/0.46    inference(cnf_transformation,[],[f78])).
% 0.08/0.46  fof(f200,plain,(
% 0.08/0.46    e2 != op(e0,e2) | ~sP22),
% 0.08/0.46    inference(cnf_transformation,[],[f79])).
% 0.08/0.46  fof(f203,plain,(
% 0.08/0.46    e1 != op(e1,e0) | ~sP21),
% 0.08/0.46    inference(cnf_transformation,[],[f80])).
% 0.08/0.46  fof(f207,plain,(
% 0.08/0.46    e1 != op(e0,e1) | ~sP20),
% 0.08/0.46    inference(cnf_transformation,[],[f81])).
% 0.08/0.46  fof(f210,plain,(
% 0.08/0.46    e0 != op(e0,e0) | ~sP19),
% 0.08/0.46    inference(cnf_transformation,[],[f82])).
% 0.08/0.46  fof(f214,plain,(
% 0.08/0.46    e0 != op(e0,e0) | ~sP18),
% 0.08/0.46    inference(cnf_transformation,[],[f83])).
% 0.08/0.46  fof(f218,plain,(
% 0.08/0.46    e0 != unit | ~sP17),
% 0.08/0.46    inference(cnf_transformation,[],[f84])).
% 0.08/0.46  fof(f222,plain,(
% 0.08/0.46    e0 != op(e3,e3) | ~sP16),
% 0.08/0.46    inference(cnf_transformation,[],[f85])).
% 0.08/0.46  fof(f227,plain,(
% 0.08/0.46    e1 != op(e3,e2) | ~sP15),
% 0.08/0.46    inference(cnf_transformation,[],[f86])).
% 0.08/0.46  fof(f232,plain,(
% 0.08/0.46    e2 != op(e3,e1) | ~sP14),
% 0.08/0.46    inference(cnf_transformation,[],[f87])).
% 0.08/0.46  fof(f237,plain,(
% 0.08/0.46    e3 != op(e3,e0) | ~sP13),
% 0.08/0.46    inference(cnf_transformation,[],[f88])).
% 0.08/0.46  fof(f239,plain,(
% 0.08/0.46    e1 != op(e2,e3) | ~sP12),
% 0.08/0.46    inference(cnf_transformation,[],[f89])).
% 0.08/0.46  fof(f242,plain,(
% 0.08/0.46    e0 != op(e2,e2) | ~sP11),
% 0.08/0.46    inference(cnf_transformation,[],[f90])).
% 0.08/0.46  fof(f249,plain,(
% 0.08/0.46    e3 != op(e2,e1) | ~sP10),
% 0.08/0.46    inference(cnf_transformation,[],[f91])).
% 0.08/0.46  fof(f252,plain,(
% 0.08/0.46    e2 != op(e2,e0) | ~sP9),
% 0.08/0.46    inference(cnf_transformation,[],[f92])).
% 0.08/0.46  fof(f256,plain,(
% 0.08/0.46    e2 != op(e1,e3) | ~sP8),
% 0.08/0.46    inference(cnf_transformation,[],[f93])).
% 0.08/0.46  fof(f261,plain,(
% 0.08/0.46    e3 != op(e1,e2) | ~sP7),
% 0.08/0.46    inference(cnf_transformation,[],[f94])).
% 0.08/0.46  fof(f262,plain,(
% 0.08/0.46    e0 != op(e1,e1) | ~sP6),
% 0.08/0.46    inference(cnf_transformation,[],[f95])).
% 0.08/0.46  fof(f267,plain,(
% 0.08/0.46    e1 != op(e1,e0) | ~sP5),
% 0.08/0.46    inference(cnf_transformation,[],[f96])).
% 0.08/0.46  fof(f273,plain,(
% 0.08/0.46    e3 != op(e0,e3) | ~sP4),
% 0.08/0.46    inference(cnf_transformation,[],[f97])).
% 0.08/0.46  fof(f276,plain,(
% 0.08/0.46    e2 != op(e0,e2) | ~sP3),
% 0.08/0.46    inference(cnf_transformation,[],[f98])).
% 0.08/0.46  fof(f279,plain,(
% 0.08/0.46    e1 != op(e0,e1) | ~sP2),
% 0.08/0.46    inference(cnf_transformation,[],[f99])).
% 0.08/0.46  fof(f282,plain,(
% 0.08/0.46    e0 != op(e0,e0) | ~sP1),
% 0.08/0.46    inference(cnf_transformation,[],[f100])).
% 0.08/0.46  fof(f286,plain,(
% 0.08/0.46    e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0) | ~sP0),
% 0.08/0.46    inference(cnf_transformation,[],[f101])).
% 0.08/0.46  fof(f291,plain,(
% 0.08/0.46    e3 != op(e0,e3) | e3 != op(e3,e0) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46    inference(cnf_transformation,[],[f54])).
% 0.08/0.46  fof(f354,plain,(
% 0.08/0.46    e0 = unit),
% 0.08/0.46    inference(cnf_transformation,[],[f3])).
% 0.08/0.46  fof(f361,plain,(
% 0.08/0.46    e0 = op(e0,e0)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f362,plain,(
% 0.08/0.46    e1 = op(e0,e1)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f363,plain,(
% 0.08/0.46    e2 = op(e0,e2)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f364,plain,(
% 0.08/0.46    e3 = op(e0,e3)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f365,plain,(
% 0.08/0.46    e1 = op(e1,e0)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f366,plain,(
% 0.08/0.46    e0 = op(e1,e1)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f367,plain,(
% 0.08/0.46    e3 = op(e1,e2)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f368,plain,(
% 0.08/0.46    e2 = op(e1,e3)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f369,plain,(
% 0.08/0.46    e2 = op(e2,e0)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f370,plain,(
% 0.08/0.46    e3 = op(e2,e1)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f371,plain,(
% 0.08/0.46    e0 = op(e2,e2)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f372,plain,(
% 0.08/0.46    e1 = op(e2,e3)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f373,plain,(
% 0.08/0.46    e3 = op(e3,e0)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f374,plain,(
% 0.08/0.46    e2 = op(e3,e1)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f375,plain,(
% 0.08/0.46    e1 = op(e3,e2)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f376,plain,(
% 0.08/0.46    e0 = op(e3,e3)),
% 0.08/0.46    inference(cnf_transformation,[],[f2])).
% 0.08/0.46  fof(f380,plain,(
% 0.08/0.46    op(e3,e3) != unit | ~sP43),
% 0.08/0.46    inference(definition_unfolding,[],[f117,f354])).
% 0.08/0.46  fof(f384,plain,(
% 0.08/0.46    op(e3,e3) != unit | ~sP42),
% 0.08/0.46    inference(definition_unfolding,[],[f121,f354])).
% 0.08/0.46  fof(f390,plain,(
% 0.08/0.46    e2 != op(unit,e2) | ~sP39),
% 0.08/0.46    inference(definition_unfolding,[],[f130,f354])).
% 0.08/0.46  fof(f391,plain,(
% 0.08/0.46    e2 != op(e2,unit) | ~sP38),
% 0.08/0.46    inference(definition_unfolding,[],[f134,f354])).
% 0.08/0.46  fof(f395,plain,(
% 0.08/0.46    op(e2,e2) != unit | ~sP35),
% 0.08/0.46    inference(definition_unfolding,[],[f148,f354])).
% 0.08/0.46  fof(f399,plain,(
% 0.08/0.46    op(e2,e2) != unit | ~sP34),
% 0.08/0.46    inference(definition_unfolding,[],[f152,f354])).
% 0.08/0.46  fof(f406,plain,(
% 0.08/0.46    e1 != op(unit,e1) | ~sP29),
% 0.08/0.46    inference(definition_unfolding,[],[f170,f354])).
% 0.08/0.46  fof(f407,plain,(
% 0.08/0.46    e1 != op(e1,unit) | ~sP28),
% 0.08/0.46    inference(definition_unfolding,[],[f174,f354])).
% 0.08/0.46  fof(f410,plain,(
% 0.08/0.46    op(e1,e1) != unit | ~sP27),
% 0.08/0.46    inference(definition_unfolding,[],[f179,f354])).
% 0.08/0.46  fof(f414,plain,(
% 0.08/0.46    op(e1,e1) != unit | ~sP26),
% 0.08/0.46    inference(definition_unfolding,[],[f183,f354])).
% 0.08/0.46  fof(f416,plain,(
% 0.08/0.46    e3 != op(e3,unit) | ~sP25),
% 0.08/0.46    inference(definition_unfolding,[],[f189,f354])).
% 0.08/0.46  fof(f420,plain,(
% 0.08/0.46    e3 != op(unit,e3) | ~sP24),
% 0.08/0.46    inference(definition_unfolding,[],[f193,f354])).
% 0.08/0.46  fof(f425,plain,(
% 0.08/0.46    e2 != op(e2,unit) | ~sP23),
% 0.08/0.46    inference(definition_unfolding,[],[f196,f354])).
% 0.08/0.46  fof(f429,plain,(
% 0.08/0.46    e2 != op(unit,e2) | ~sP22),
% 0.08/0.46    inference(definition_unfolding,[],[f200,f354])).
% 0.08/0.46  fof(f434,plain,(
% 0.08/0.46    e1 != op(e1,unit) | ~sP21),
% 0.08/0.46    inference(definition_unfolding,[],[f203,f354])).
% 0.08/0.46  fof(f438,plain,(
% 0.08/0.46    e1 != op(unit,e1) | ~sP20),
% 0.08/0.46    inference(definition_unfolding,[],[f207,f354])).
% 0.08/0.46  fof(f443,plain,(
% 0.08/0.46    op(unit,unit) != unit | ~sP19),
% 0.08/0.46    inference(definition_unfolding,[],[f210,f354,f354,f354])).
% 0.08/0.46  fof(f447,plain,(
% 0.08/0.46    op(unit,unit) != unit | ~sP18),
% 0.08/0.46    inference(definition_unfolding,[],[f214,f354,f354,f354])).
% 0.08/0.46  fof(f448,plain,(
% 0.08/0.46    unit != unit | ~sP17),
% 0.08/0.46    inference(definition_unfolding,[],[f218,f354])).
% 0.08/0.46  fof(f449,plain,(
% 0.08/0.46    op(e3,e3) != unit | ~sP16),
% 0.08/0.46    inference(definition_unfolding,[],[f222,f354])).
% 0.08/0.46  fof(f452,plain,(
% 0.08/0.46    e3 != op(e3,unit) | ~sP13),
% 0.08/0.46    inference(definition_unfolding,[],[f237,f354])).
% 0.08/0.46  fof(f457,plain,(
% 0.08/0.46    op(e2,e2) != unit | ~sP11),
% 0.08/0.46    inference(definition_unfolding,[],[f242,f354])).
% 0.08/0.46  fof(f460,plain,(
% 0.08/0.46    e2 != op(e2,unit) | ~sP9),
% 0.08/0.46    inference(definition_unfolding,[],[f252,f354])).
% 0.08/0.46  fof(f465,plain,(
% 0.08/0.46    op(e1,e1) != unit | ~sP6),
% 0.08/0.46    inference(definition_unfolding,[],[f262,f354])).
% 0.08/0.46  fof(f468,plain,(
% 0.08/0.46    e1 != op(e1,unit) | ~sP5),
% 0.08/0.46    inference(definition_unfolding,[],[f267,f354])).
% 0.08/0.46  fof(f470,plain,(
% 0.08/0.46    e3 != op(unit,e3) | ~sP4),
% 0.08/0.46    inference(definition_unfolding,[],[f273,f354])).
% 0.08/0.46  fof(f475,plain,(
% 0.08/0.46    e2 != op(unit,e2) | ~sP3),
% 0.08/0.46    inference(definition_unfolding,[],[f276,f354])).
% 0.08/0.46  fof(f480,plain,(
% 0.08/0.46    e1 != op(unit,e1) | ~sP2),
% 0.08/0.46    inference(definition_unfolding,[],[f279,f354])).
% 0.08/0.46  fof(f485,plain,(
% 0.08/0.46    op(unit,unit) != unit | ~sP1),
% 0.08/0.46    inference(definition_unfolding,[],[f282,f354,f354,f354])).
% 0.08/0.46  fof(f489,plain,(
% 0.08/0.46    op(e3,e3) != unit | op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(definition_unfolding,[],[f286,f354,f354,f354,f354,f354,f354])).
% 0.08/0.46  fof(f552,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46    inference(definition_unfolding,[],[f291,f354,f354,f354,f354,f354,f354])).
% 0.08/0.46  fof(f557,plain,(
% 0.08/0.46    op(e3,e3) = unit),
% 0.08/0.46    inference(definition_unfolding,[],[f376,f354])).
% 0.08/0.46  fof(f558,plain,(
% 0.08/0.46    e3 = op(e3,unit)),
% 0.08/0.46    inference(definition_unfolding,[],[f373,f354])).
% 0.08/0.46  fof(f559,plain,(
% 0.08/0.46    op(e2,e2) = unit),
% 0.08/0.46    inference(definition_unfolding,[],[f371,f354])).
% 0.08/0.46  fof(f560,plain,(
% 0.08/0.46    e2 = op(e2,unit)),
% 0.08/0.46    inference(definition_unfolding,[],[f369,f354])).
% 0.08/0.46  fof(f561,plain,(
% 0.08/0.46    op(e1,e1) = unit),
% 0.08/0.46    inference(definition_unfolding,[],[f366,f354])).
% 0.08/0.46  fof(f562,plain,(
% 0.08/0.46    e1 = op(e1,unit)),
% 0.08/0.46    inference(definition_unfolding,[],[f365,f354])).
% 0.08/0.46  fof(f563,plain,(
% 0.08/0.46    e3 = op(unit,e3)),
% 0.08/0.46    inference(definition_unfolding,[],[f364,f354])).
% 0.08/0.46  fof(f564,plain,(
% 0.08/0.46    e2 = op(unit,e2)),
% 0.08/0.46    inference(definition_unfolding,[],[f363,f354])).
% 0.08/0.46  fof(f565,plain,(
% 0.08/0.46    e1 = op(unit,e1)),
% 0.08/0.46    inference(definition_unfolding,[],[f362,f354])).
% 0.08/0.46  fof(f566,plain,(
% 0.08/0.46    op(unit,unit) = unit),
% 0.08/0.46    inference(definition_unfolding,[],[f361,f354,f354,f354])).
% 0.08/0.46  fof(f568,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46    inference(duplicate_literal_removal,[],[f552])).
% 0.08/0.46  fof(f631,plain,(
% 0.08/0.46    ~sP17),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f448])).
% 0.08/0.46  fof(f1912,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f568,f631])).
% 0.08/0.46  fof(f1913,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1912,f485])).
% 0.08/0.46  fof(f1914,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1913,f447])).
% 0.08/0.46  fof(f1915,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1914,f443])).
% 0.08/0.46  fof(f1916,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1915,f406])).
% 0.08/0.46  fof(f1917,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1916,f438])).
% 0.08/0.46  fof(f1918,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1917,f480])).
% 0.08/0.46  fof(f1919,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1918,f407])).
% 0.08/0.46  fof(f1920,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1919,f434])).
% 0.08/0.46  fof(f1921,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1920,f468])).
% 0.08/0.46  fof(f1922,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1921,f390])).
% 0.08/0.46  fof(f1923,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1922,f429])).
% 0.08/0.46  fof(f1924,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1923,f475])).
% 0.08/0.46  fof(f1925,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1924,f391])).
% 0.08/0.46  fof(f1926,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1925,f425])).
% 0.08/0.46  fof(f1927,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1926,f460])).
% 0.08/0.46  fof(f1928,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP8 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1927,f169])).
% 0.08/0.46  fof(f1929,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1928,f256])).
% 0.08/0.46  fof(f1930,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1929,f416])).
% 0.08/0.46  fof(f1931,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1930,f452])).
% 0.08/0.46  fof(f1932,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1931,f420])).
% 0.08/0.46  fof(f1933,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f1932,f470])).
% 0.08/0.46  fof(f1963,plain,(
% 0.08/0.46    unit != unit | ~sP43),
% 0.08/0.46    inference(backward_demodulation,[],[f557,f380])).
% 0.08/0.46  fof(f1964,plain,(
% 0.08/0.46    unit != unit | ~sP42),
% 0.08/0.46    inference(backward_demodulation,[],[f557,f384])).
% 0.08/0.46  fof(f1965,plain,(
% 0.08/0.46    unit != unit | ~sP16),
% 0.08/0.46    inference(backward_demodulation,[],[f557,f449])).
% 0.08/0.46  fof(f1969,plain,(
% 0.08/0.46    unit != unit | op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f557,f489])).
% 0.08/0.46  fof(f1981,plain,(
% 0.08/0.46    op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1969])).
% 0.08/0.46  fof(f1982,plain,(
% 0.08/0.46    ~sP16),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1965])).
% 0.08/0.46  fof(f1983,plain,(
% 0.08/0.46    ~sP42),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1964])).
% 0.08/0.46  fof(f1984,plain,(
% 0.08/0.46    ~sP43),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1963])).
% 0.08/0.46  fof(f1986,plain,(
% 0.08/0.46    e1 != e1 | ~sP44),
% 0.08/0.46    inference(backward_demodulation,[],[f375,f112])).
% 0.08/0.46  fof(f1989,plain,(
% 0.08/0.46    e1 != e1 | ~sP37),
% 0.08/0.46    inference(backward_demodulation,[],[f375,f141])).
% 0.08/0.46  fof(f1990,plain,(
% 0.08/0.46    e1 != e1 | ~sP15),
% 0.08/0.46    inference(backward_demodulation,[],[f375,f227])).
% 0.08/0.46  fof(f2000,plain,(
% 0.08/0.46    ~sP15),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1990])).
% 0.08/0.46  fof(f2001,plain,(
% 0.08/0.46    ~sP37),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1989])).
% 0.08/0.46  fof(f2002,plain,(
% 0.08/0.46    ~sP44),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f1986])).
% 0.08/0.46  fof(f2003,plain,(
% 0.08/0.46    e2 != e2 | ~sP46),
% 0.08/0.46    inference(backward_demodulation,[],[f374,f103])).
% 0.08/0.46  fof(f2006,plain,(
% 0.08/0.46    e2 != e2 | ~sP31),
% 0.08/0.46    inference(backward_demodulation,[],[f374,f165])).
% 0.08/0.46  fof(f2009,plain,(
% 0.08/0.46    e2 != e2 | ~sP14),
% 0.08/0.46    inference(backward_demodulation,[],[f374,f232])).
% 0.08/0.46  fof(f2018,plain,(
% 0.08/0.46    ~sP14),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2009])).
% 0.08/0.46  fof(f2019,plain,(
% 0.08/0.46    ~sP31),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2006])).
% 0.08/0.46  fof(f2020,plain,(
% 0.08/0.46    ~sP46),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2003])).
% 0.08/0.46  fof(f2035,plain,(
% 0.08/0.46    e3 != e3 | e3 != op(unit,e3) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f558,f1933])).
% 0.08/0.46  fof(f2036,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2035])).
% 0.08/0.46  fof(f2069,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2036,f2020])).
% 0.08/0.46  fof(f2070,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2069,f2002])).
% 0.08/0.46  fof(f2071,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2070,f1984])).
% 0.08/0.46  fof(f2072,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2071,f1983])).
% 0.08/0.46  fof(f2073,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2072,f2001])).
% 0.08/0.46  fof(f2074,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2073,f2019])).
% 0.08/0.46  fof(f2075,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2074,f1982])).
% 0.08/0.46  fof(f2076,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2075,f2000])).
% 0.08/0.46  fof(f2077,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2076,f2018])).
% 0.08/0.46  fof(f2078,plain,(
% 0.08/0.46    e1 != e1 | ~sP45),
% 0.08/0.46    inference(backward_demodulation,[],[f372,f108])).
% 0.08/0.46  fof(f2081,plain,(
% 0.08/0.46    e1 != e1 | ~sP36),
% 0.08/0.46    inference(backward_demodulation,[],[f372,f145])).
% 0.08/0.46  fof(f2082,plain,(
% 0.08/0.46    e1 != e1 | ~sP12),
% 0.08/0.46    inference(backward_demodulation,[],[f372,f239])).
% 0.08/0.46  fof(f2091,plain,(
% 0.08/0.46    ~sP12),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2082])).
% 0.08/0.46  fof(f2092,plain,(
% 0.08/0.46    ~sP36),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2081])).
% 0.08/0.46  fof(f2093,plain,(
% 0.08/0.46    ~sP45),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2078])).
% 0.08/0.46  fof(f2103,plain,(
% 0.08/0.46    unit != unit | ~sP35),
% 0.08/0.46    inference(backward_demodulation,[],[f559,f395])).
% 0.08/0.46  fof(f2104,plain,(
% 0.08/0.46    unit != unit | ~sP34),
% 0.08/0.46    inference(backward_demodulation,[],[f559,f399])).
% 0.08/0.46  fof(f2105,plain,(
% 0.08/0.46    unit != unit | ~sP11),
% 0.08/0.46    inference(backward_demodulation,[],[f559,f457])).
% 0.08/0.46  fof(f2114,plain,(
% 0.08/0.46    unit != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f559,f1981])).
% 0.08/0.46  fof(f2115,plain,(
% 0.08/0.46    op(e1,e1) != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2114])).
% 0.08/0.46  fof(f2116,plain,(
% 0.08/0.46    ~sP11),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2105])).
% 0.08/0.46  fof(f2117,plain,(
% 0.08/0.46    ~sP34),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2104])).
% 0.08/0.46  fof(f2118,plain,(
% 0.08/0.46    ~sP35),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2103])).
% 0.08/0.46  fof(f2119,plain,(
% 0.08/0.46    e3 != e3 | ~sP40),
% 0.08/0.46    inference(backward_demodulation,[],[f370,f127])).
% 0.08/0.46  fof(f2122,plain,(
% 0.08/0.46    e3 != e3 | ~sP33),
% 0.08/0.46    inference(backward_demodulation,[],[f370,f156])).
% 0.08/0.46  fof(f2127,plain,(
% 0.08/0.46    e3 != e3 | ~sP10),
% 0.08/0.46    inference(backward_demodulation,[],[f370,f249])).
% 0.08/0.46  fof(f2135,plain,(
% 0.08/0.46    ~sP10),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2127])).
% 0.08/0.46  fof(f2136,plain,(
% 0.08/0.46    ~sP33),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2122])).
% 0.08/0.46  fof(f2137,plain,(
% 0.08/0.46    ~sP40),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2119])).
% 0.08/0.46  fof(f2152,plain,(
% 0.08/0.46    e2 != e2 | e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f560,f2077])).
% 0.08/0.46  fof(f2153,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2152])).
% 0.08/0.46  fof(f2159,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2153,f2093])).
% 0.08/0.46  fof(f2160,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2159,f2137])).
% 0.08/0.46  fof(f2161,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2160,f2092])).
% 0.08/0.46  fof(f2162,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2161,f2118])).
% 0.08/0.46  fof(f2163,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2162,f2117])).
% 0.08/0.46  fof(f2164,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2163,f2136])).
% 0.08/0.46  fof(f2165,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP11 | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2164,f2091])).
% 0.08/0.46  fof(f2166,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP10 | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2165,f2116])).
% 0.08/0.46  fof(f2167,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2166,f2135])).
% 0.08/0.46  fof(f2178,plain,(
% 0.08/0.46    e2 != e2 | e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f368,f2167])).
% 0.08/0.46  fof(f2179,plain,(
% 0.08/0.46    e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2178])).
% 0.08/0.46  fof(f2182,plain,(
% 0.08/0.46    e3 != e3 | ~sP41),
% 0.08/0.46    inference(backward_demodulation,[],[f367,f123])).
% 0.08/0.46  fof(f2185,plain,(
% 0.08/0.46    e3 != e3 | ~sP32),
% 0.08/0.46    inference(backward_demodulation,[],[f367,f160])).
% 0.08/0.46  fof(f2190,plain,(
% 0.08/0.46    e3 != e3 | ~sP7),
% 0.08/0.46    inference(backward_demodulation,[],[f367,f261])).
% 0.08/0.46  fof(f2194,plain,(
% 0.08/0.46    ~sP7),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2190])).
% 0.08/0.46  fof(f2195,plain,(
% 0.08/0.46    ~sP32),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2185])).
% 0.08/0.46  fof(f2196,plain,(
% 0.08/0.46    ~sP41),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2182])).
% 0.08/0.46  fof(f2206,plain,(
% 0.08/0.46    unit != unit | ~sP27),
% 0.08/0.46    inference(backward_demodulation,[],[f561,f410])).
% 0.08/0.46  fof(f2207,plain,(
% 0.08/0.46    unit != unit | ~sP26),
% 0.08/0.46    inference(backward_demodulation,[],[f561,f414])).
% 0.08/0.46  fof(f2208,plain,(
% 0.08/0.46    unit != unit | ~sP6),
% 0.08/0.46    inference(backward_demodulation,[],[f561,f465])).
% 0.08/0.46  fof(f2209,plain,(
% 0.08/0.46    unit != unit | op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f561,f2115])).
% 0.08/0.46  fof(f2210,plain,(
% 0.08/0.46    op(unit,unit) != unit | ~sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2209])).
% 0.08/0.46  fof(f2211,plain,(
% 0.08/0.46    ~sP6),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2208])).
% 0.08/0.46  fof(f2212,plain,(
% 0.08/0.46    ~sP26),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2207])).
% 0.08/0.46  fof(f2213,plain,(
% 0.08/0.46    ~sP27),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2206])).
% 0.08/0.46  fof(f2226,plain,(
% 0.08/0.46    e1 != e1 | e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(backward_demodulation,[],[f562,f2179])).
% 0.08/0.46  fof(f2227,plain,(
% 0.08/0.46    e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2226])).
% 0.08/0.46  fof(f2231,plain,(
% 0.08/0.46    e3 != op(unit,e3) | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2227,f2196])).
% 0.08/0.46  fof(f2232,plain,(
% 0.08/0.46    e3 != op(unit,e3) | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2231,f2195])).
% 0.08/0.46  fof(f2233,plain,(
% 0.08/0.46    e3 != op(unit,e3) | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2232,f2213])).
% 0.08/0.46  fof(f2234,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2233,f2212])).
% 0.08/0.46  fof(f2235,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP6 | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2234,f2194])).
% 0.08/0.46  fof(f2236,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP0),
% 0.08/0.46    inference(subsumption_resolution,[],[f2235,f2211])).
% 0.08/0.46  fof(f2237,plain,(
% 0.08/0.46    e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46    inference(subsumption_resolution,[],[f2236,f2210])).
% 0.08/0.46  fof(f2248,plain,(
% 0.08/0.46    e3 != e3 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46    inference(backward_demodulation,[],[f563,f2237])).
% 0.08/0.46  fof(f2249,plain,(
% 0.08/0.46    e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2248])).
% 0.08/0.46  fof(f2264,plain,(
% 0.08/0.46    e2 != e2 | e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46    inference(backward_demodulation,[],[f564,f2249])).
% 0.08/0.46  fof(f2265,plain,(
% 0.08/0.46    e1 != op(unit,e1) | op(unit,unit) != unit),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2264])).
% 0.08/0.46  fof(f2281,plain,(
% 0.08/0.46    e1 != e1 | op(unit,unit) != unit),
% 0.08/0.46    inference(backward_demodulation,[],[f565,f2265])).
% 0.08/0.46  fof(f2282,plain,(
% 0.08/0.46    op(unit,unit) != unit),
% 0.08/0.46    inference(trivial_inequality_removal,[],[f2281])).
% 0.08/0.46  fof(f2286,plain,(
% 0.08/0.46    $false),
% 0.08/0.46    inference(subsumption_resolution,[],[f566,f2282])).
% 0.08/0.46  % SZS output end Proof for theBenchmark
% 0.08/0.46  % ------------------------------
% 0.08/0.46  % Version: Vampire 4.2.2 (commit 552c234 on 2018-07-02 14:53:33 +0100)
% 0.08/0.46  % Termination reason: Refutation
% 0.08/0.46  
% 0.08/0.46  % Memory used [KB]: 1535
% 0.08/0.46  % Time elapsed: 0.178 s
% 0.08/0.46  % ------------------------------
% 0.08/0.46  % ------------------------------
% 0.08/0.46  % Success in time 0.214 s
%------------------------------------------------------------------------------
