Bliksem---1.12.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Bliksem---1.12
% Problem  : GRP127-3.004 : TPTP v8.1.0. Released v1.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : bliksem %s

% Computer : n013.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 0s
% DateTime : Sat Jul 16 07:35:16 EDT 2022

% Result   : Unsatisfiable 0.46s 1.12s
% Output   : Refutation 0.46s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : GRP127-3.004 : TPTP v8.1.0. Released v1.2.0.
% 0.11/0.13  % Command  : bliksem %s
% 0.13/0.34  % Computer : n013.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % DateTime : Mon Jun 13 14:35:13 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.46/1.12  *** allocated 10000 integers for termspace/termends
% 0.46/1.12  *** allocated 10000 integers for clauses
% 0.46/1.12  *** allocated 10000 integers for justifications
% 0.46/1.12  Bliksem 1.12
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  Automatic Strategy Selection
% 0.46/1.12  
% 0.46/1.12  Clauses:
% 0.46/1.12  [
% 0.46/1.12     [ next( 'e_0', 'e_1' ) ],
% 0.46/1.12     [ next( 'e_1', 'e_2' ) ],
% 0.46/1.12     [ next( 'e_2', 'e_3' ) ],
% 0.46/1.12     [ next( 'e_3', 'e_4' ) ],
% 0.46/1.12     [ greater( 'e_1', 'e_0' ) ],
% 0.46/1.12     [ greater( 'e_2', 'e_0' ) ],
% 0.46/1.12     [ greater( 'e_3', 'e_0' ) ],
% 0.46/1.12     [ greater( 'e_4', 'e_0' ) ],
% 0.46/1.12     [ greater( 'e_2', 'e_1' ) ],
% 0.46/1.12     [ greater( 'e_3', 'e_1' ) ],
% 0.46/1.12     [ greater( 'e_4', 'e_1' ) ],
% 0.46/1.12     [ greater( 'e_3', 'e_2' ) ],
% 0.46/1.12     [ greater( 'e_4', 'e_2' ) ],
% 0.46/1.12     [ greater( 'e_4', 'e_3' ) ],
% 0.46/1.12     [ ~( cycle( X, Y ) ), ~( cycle( X, Z ) ), equalish( Y, Z ) ],
% 0.46/1.12     [ ~( 'group_element'( X ) ), cycle( X, 'e_0' ), cycle( X, 'e_1' ), cycle( 
% 0.46/1.12    X, 'e_2' ), cycle( X, 'e_3' ) ],
% 0.46/1.12     [ cycle( 'e_4', 'e_0' ) ],
% 0.46/1.12     [ ~( cycle( X, Y ) ), ~( cycle( Z, T ) ), ~( next( X, Z ) ), ~( greater( 
% 0.46/1.12    Y, 'e_0' ) ), ~( next( T, U ) ), equalish( Y, U ) ],
% 0.46/1.12     [ ~( cycle( X, Y ) ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U ) ), ~( 
% 0.46/1.12    next( Z, T ) ), ~( greater( Z, X ) ), ~( greater( Y, U ) ) ],
% 0.46/1.12     [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( greater( Y, X
% 0.46/1.12     ) ) ],
% 0.46/1.12     [ ~( cycle( X, Y ) ), ~( product( X, 'e_1', Z ) ), ~( greater( Y, 'e_0'
% 0.46/1.12     ) ), ~( next( X, T ) ), equalish( Z, T ) ],
% 0.46/1.12     [ 'group_element'( 'e_1' ) ],
% 0.46/1.12     [ 'group_element'( 'e_2' ) ],
% 0.46/1.12     [ 'group_element'( 'e_3' ) ],
% 0.46/1.12     [ 'group_element'( 'e_4' ) ],
% 0.46/1.12     [ ~( equalish( 'e_1', 'e_2' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_1', 'e_3' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_1', 'e_4' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_2', 'e_1' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_2', 'e_3' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_2', 'e_4' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_3', 'e_1' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_3', 'e_2' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_3', 'e_4' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_4', 'e_1' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_4', 'e_2' ) ) ],
% 0.46/1.12     [ ~( equalish( 'e_4', 'e_3' ) ) ],
% 0.46/1.12     [ ~( 'group_element'( X ) ), ~( 'group_element'( Y ) ), product( X, Y, 
% 0.46/1.12    'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), product( X, Y, 
% 0.46/1.12    'e_4' ) ],
% 0.46/1.12     [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), equalish( Z, T ) ]
% 0.46/1.12    ,
% 0.46/1.12     [ ~( product( X, Y, Z ) ), ~( product( X, T, Z ) ), equalish( Y, T ) ]
% 0.46/1.12    ,
% 0.46/1.12     [ ~( product( X, Y, Z ) ), ~( product( T, Y, Z ) ), equalish( X, T ) ]
% 0.46/1.12    ,
% 0.46/1.12     [ product( X, X, X ) ],
% 0.46/1.12     [ ~( product( X, Y, Z ) ), ~( product( Z, X, T ) ), product( T, X, Y ) ]
% 0.46/1.12    
% 0.46/1.12  ] .
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  percentage equality = 0.000000, percentage horn = 0.953488
% 0.46/1.12  This is a near-Horn, non-equality  problem
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  Options Used:
% 0.46/1.12  
% 0.46/1.12  useres =            1
% 0.46/1.12  useparamod =        0
% 0.46/1.12  useeqrefl =         0
% 0.46/1.12  useeqfact =         0
% 0.46/1.12  usefactor =         1
% 0.46/1.12  usesimpsplitting =  0
% 0.46/1.12  usesimpdemod =      0
% 0.46/1.12  usesimpres =        4
% 0.46/1.12  
% 0.46/1.12  resimpinuse      =  1000
% 0.46/1.12  resimpclauses =     20000
% 0.46/1.12  substype =          standard
% 0.46/1.12  backwardsubs =      1
% 0.46/1.12  selectoldest =      5
% 0.46/1.12  
% 0.46/1.12  litorderings [0] =  split
% 0.46/1.12  litorderings [1] =  liftord
% 0.46/1.12  
% 0.46/1.12  termordering =      none
% 0.46/1.12  
% 0.46/1.12  litapriori =        1
% 0.46/1.12  termapriori =       0
% 0.46/1.12  litaposteriori =    0
% 0.46/1.12  termaposteriori =   0
% 0.46/1.12  demodaposteriori =  0
% 0.46/1.12  ordereqreflfact =   0
% 0.46/1.12  
% 0.46/1.12  litselect =         negative
% 0.46/1.12  
% 0.46/1.12  maxweight =         30000
% 0.46/1.12  maxdepth =          30000
% 0.46/1.12  maxlength =         115
% 0.46/1.12  maxnrvars =         195
% 0.46/1.12  excuselevel =       0
% 0.46/1.12  increasemaxweight = 0
% 0.46/1.12  
% 0.46/1.12  maxselected =       10000000
% 0.46/1.12  maxnrclauses =      10000000
% 0.46/1.12  
% 0.46/1.12  showgenerated =    0
% 0.46/1.12  showkept =         0
% 0.46/1.12  showselected =     0
% 0.46/1.12  showdeleted =      0
% 0.46/1.12  showresimp =       1
% 0.46/1.12  showstatus =       2000
% 0.46/1.12  
% 0.46/1.12  prologoutput =     1
% 0.46/1.12  nrgoals =          5000000
% 0.46/1.12  totalproof =       1
% 0.46/1.12  
% 0.46/1.12  Symbols occurring in the translation:
% 0.46/1.12  
% 0.46/1.12  {}  [0, 0]      (w:1, o:2, a:1, s:1, b:0), 
% 0.46/1.12  .  [1, 2]      (w:1, o:27, a:1, s:1, b:0), 
% 0.46/1.12  !  [4, 1]      (w:1, o:21, a:1, s:1, b:0), 
% 0.46/1.12  =  [13, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.46/1.12  ==>  [14, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.46/1.12  'e_0'  [39, 0]      (w:1, o:9, a:1, s:1, b:0), 
% 0.46/1.12  'e_1'  [40, 0]      (w:1, o:10, a:1, s:1, b:0), 
% 0.46/1.12  next  [41, 2]      (w:1, o:52, a:1, s:1, b:0), 
% 0.46/1.12  'e_2'  [42, 0]      (w:1, o:11, a:1, s:1, b:0), 
% 0.46/1.12  'e_3'  [43, 0]      (w:1, o:12, a:1, s:1, b:0), 
% 0.46/1.12  'e_4'  [44, 0]      (w:1, o:13, a:1, s:1, b:0), 
% 0.46/1.12  greater  [45, 2]      (w:1, o:53, a:1, s:1, b:0), 
% 0.46/1.12  cycle  [48, 2]      (w:1, o:54, a:1, s:1, b:0), 
% 0.46/1.12  equalish  [50, 2]      (w:1, o:55, a:1, s:1, b:0), 
% 0.46/1.12  'group_element'  [51, 1]      (w:1, o:26, a:1, s:1, b:0), 
% 0.46/1.12  product  [55, 3]      (w:1, o:56, a:1, s:1, b:0).
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  Starting Search:
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  Bliksems!, er is een bewijs:
% 0.46/1.12  % SZS status Unsatisfiable
% 0.46/1.12  % SZS output start Refutation
% 0.46/1.12  
% 0.46/1.12  clause( 0, [ next( 'e_0', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 1, [ next( 'e_1', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 2, [ next( 'e_2', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 3, [ next( 'e_3', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 4, [ greater( 'e_1', 'e_0' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 5, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 6, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 12, [ greater( 'e_4', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 15, [ cycle( X, 'e_3' ), cycle( X, 'e_0' ), cycle( X, 'e_1' ), 
% 0.46/1.12    cycle( X, 'e_2' ), ~( 'group_element'( X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 17, [ ~( next( X, Z ) ), ~( greater( Y, 'e_0' ) ), equalish( Y, U )
% 0.46/1.12    , ~( cycle( Z, T ) ), ~( cycle( X, Y ) ), ~( next( T, U ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 18, [ ~( cycle( X, Y ) ), ~( greater( Z, X ) ), ~( greater( Y, U )
% 0.46/1.12     ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U ) ), ~( next( Z, T ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 19, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( 
% 0.46/1.12    greater( Y, X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 20, [ ~( cycle( X, Y ) ), ~( greater( Y, 'e_0' ) ), ~( product( X, 
% 0.46/1.12    'e_1', Z ) ), equalish( Z, T ), ~( next( X, T ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 21, [ 'group_element'( 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 22, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 23, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 24, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 25, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 26, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 27, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 28, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 29, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 30, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 31, [ ~( equalish( 'e_3', 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 32, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 33, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 35, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 36, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( X
% 0.46/1.12    , Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~( 
% 0.46/1.12    'group_element'( Y ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 38, [ equalish( Z, T ), ~( product( X, Y, Z ) ), ~( product( X, Y, 
% 0.46/1.12    T ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T, 
% 0.46/1.12    Z ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 40, [ equalish( X, T ), ~( product( X, Y, Z ) ), ~( product( T, Y, 
% 0.46/1.12    Z ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 41, [ product( X, X, X ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 42, [ ~( product( X, Y, Z ) ), product( T, X, Y ), ~( product( Z, X
% 0.46/1.12    , T ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 61, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_1' ), cycle( 'e_2', 
% 0.46/1.12    'e_2' ), cycle( 'e_2', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 62, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ), cycle( 'e_3', 
% 0.46/1.12    'e_2' ), cycle( 'e_3', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 65, [ equalish( Z, 'e_2' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y, 
% 0.46/1.12    'e_1' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 66, [ equalish( Z, 'e_1' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y, 
% 0.46/1.12    'e_0' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 71, [ ~( greater( 'e_3', X ) ), ~( cycle( X, Y ) ), ~( cycle( 'e_3'
% 0.46/1.12    , 'e_0' ) ), ~( cycle( 'e_4', Z ) ), ~( greater( Y, Z ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 97, [ ~( product( 'e_2', 'e_1', 'e_3' ) ), ~( cycle( 'e_2', 'e_0' )
% 0.46/1.12     ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 98, [ ~( product( 'e_2', 'e_1', 'e_4' ) ), ~( cycle( 'e_2', 'e_0' )
% 0.46/1.12     ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 101, [ ~( product( 'e_2', 'e_1', Y ) ), ~( cycle( 'e_2', X ) ), 
% 0.46/1.12    equalish( Y, 'e_3' ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 104, [ product( X, 'e_1', 'e_4' ), product( X, 'e_1', 'e_1' ), 
% 0.46/1.12    product( X, 'e_1', 'e_2' ), product( X, 'e_1', 'e_3' ), ~( 
% 0.46/1.12    'group_element'( X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 105, [ product( X, 'e_2', 'e_4' ), product( X, 'e_2', 'e_1' ), 
% 0.46/1.12    product( X, 'e_2', 'e_2' ), product( X, 'e_2', 'e_3' ), ~( 
% 0.46/1.12    'group_element'( X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 106, [ product( X, 'e_3', 'e_4' ), product( X, 'e_3', 'e_1' ), 
% 0.46/1.12    product( X, 'e_3', 'e_2' ), product( X, 'e_3', 'e_3' ), ~( 
% 0.46/1.12    'group_element'( X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 107, [ product( X, 'e_4', 'e_4' ), product( X, 'e_4', 'e_1' ), 
% 0.46/1.12    product( X, 'e_4', 'e_2' ), product( X, 'e_4', 'e_3' ), ~( 
% 0.46/1.12    'group_element'( X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 143, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~( 
% 0.46/1.12    cycle( 'e_2', 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 174, [ equalish( X, 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 
% 0.46/1.12    'e_2', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 182, [ equalish( X, 'e_1' ), ~( cycle( 'e_3', X ) ), ~( greater( X
% 0.46/1.12    , 'e_0' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 185, [ ~( cycle( 'e_3', 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 186, [ ~( cycle( 'e_3', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 189, [ ~( cycle( X, 'e_1' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.12    greater( 'e_3', X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 190, [ ~( cycle( X, 'e_2' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.12    greater( 'e_3', X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 191, [ ~( cycle( X, 'e_3' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.12    greater( 'e_3', X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 194, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 207, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 220, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 232, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 234, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), ~( cycle( 
% 0.46/1.12    'e_3', 'e_0' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 235, [ cycle( 'e_2', 'e_0' ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 248, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 249, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 251, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), ~( cycle( 
% 0.46/1.12    'e_3', 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 252, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 253, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( 
% 0.46/1.12    'e_2', 'e_1', X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 260, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2'
% 0.46/1.12     ), product( 'e_2', 'e_1', 'e_3' ), product( 'e_2', 'e_1', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 262, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 'e_2'
% 0.46/1.12     ), product( 'e_4', 'e_1', 'e_3' ), product( 'e_4', 'e_1', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 268, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2'
% 0.46/1.12     ), product( 'e_4', 'e_2', 'e_3' ), product( 'e_4', 'e_2', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 274, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 'e_2'
% 0.46/1.12     ), product( 'e_4', 'e_3', 'e_3' ), product( 'e_4', 'e_3', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 280, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 'e_2'
% 0.46/1.12     ), product( 'e_2', 'e_4', 'e_3' ), product( 'e_2', 'e_4', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 281, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 'e_2'
% 0.46/1.12     ), product( 'e_3', 'e_4', 'e_3' ), product( 'e_3', 'e_4', 'e_4' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 320, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2'
% 0.46/1.12     ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 329, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 'e_2'
% 0.46/1.12     ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 337, [ product( 'e_2', 'e_4', 'e_1' ), equalish( X, 'e_4' ), 
% 0.46/1.12    product( 'e_2', 'e_4', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 339, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_1', 'e_1'
% 0.46/1.12     ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_2'
% 0.46/1.12    , 'e_4', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 343, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 'e_2'
% 0.46/1.12     ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 345, [ product( 'e_4', 'e_1', 'e_1' ), equalish( X, 'e_4' ), 
% 0.46/1.12    product( 'e_4', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 348, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_1'
% 0.46/1.12     ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_4'
% 0.46/1.12    , 'e_1', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 369, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2'
% 0.46/1.12     ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 374, [ product( 'e_4', 'e_2', 'e_1' ), equalish( X, 'e_3' ), 
% 0.46/1.12    product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_4', 'e_2', X ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 390, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 'e_2'
% 0.46/1.12     ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 396, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 'e_2'
% 0.46/1.12     ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 400, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 'e_2'
% 0.46/1.12     ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 402, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_2', 'e_4', X ), 
% 0.46/1.12    ~( product( 'e_4', X, 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 414, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 'e_2'
% 0.46/1.12     ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 418, [ equalish( X, 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), ~( 
% 0.46/1.12    product( 'e_4', X, 'e_2' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 428, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_4', 'e_2', 'e_1'
% 0.46/1.12     ), product( 'e_4', 'e_2', 'e_2' ), product( 'e_2', 'e_4', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 446, [ product( 'e_4', 'e_2', 'e_1' ), equalish( 'e_4', 'e_2' ), 
% 0.46/1.12    product( 'e_3', 'e_4', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 447, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_3', 'e_4', 'e_1'
% 0.46/1.12     ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 450, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_1' ), ~( 
% 0.46/1.12    product( X, 'e_4', 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 501, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_4', 'e_1'
% 0.46/1.12     ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 504, [ product( 'e_2', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.46/1.12    product( 'e_2', 'e_4', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 505, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.46/1.12    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 512, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.46/1.12    'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 517, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.46/1.12    product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 522, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 526, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product( 
% 0.46/1.12    'e_4', X, 'e_1' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 543, [ product( 'e_4', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.46/1.12    equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_2'
% 0.46/1.12    , 'e_1', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 618, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_1', 'e_1' ), 
% 0.46/1.12    product( 'e_4', 'e_3', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 620, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), product( 
% 0.46/1.12    'e_4', 'e_3', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 621, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 622, [ cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 623, [ ~( product( 'e_2', 'e_1', 'e_4' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 624, [ ~( product( 'e_2', 'e_1', 'e_3' ) ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 626, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2'
% 0.46/1.12     ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 632, [ product( 'e_2', 'e_1', 'e_1' ) ] )
% 0.46/1.12  .
% 0.46/1.12  clause( 636, [] )
% 0.46/1.12  .
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  % SZS output end Refutation
% 0.46/1.12  found a proof!
% 0.46/1.12  
% 0.46/1.12  % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 0.46/1.12  
% 0.46/1.12  initialclauses(
% 0.46/1.12  [ clause( 638, [ next( 'e_0', 'e_1' ) ] )
% 0.46/1.12  , clause( 639, [ next( 'e_1', 'e_2' ) ] )
% 0.46/1.12  , clause( 640, [ next( 'e_2', 'e_3' ) ] )
% 0.46/1.12  , clause( 641, [ next( 'e_3', 'e_4' ) ] )
% 0.46/1.12  , clause( 642, [ greater( 'e_1', 'e_0' ) ] )
% 0.46/1.12  , clause( 643, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.12  , clause( 644, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.12  , clause( 645, [ greater( 'e_4', 'e_0' ) ] )
% 0.46/1.12  , clause( 646, [ greater( 'e_2', 'e_1' ) ] )
% 0.46/1.12  , clause( 647, [ greater( 'e_3', 'e_1' ) ] )
% 0.46/1.12  , clause( 648, [ greater( 'e_4', 'e_1' ) ] )
% 0.46/1.12  , clause( 649, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.12  , clause( 650, [ greater( 'e_4', 'e_2' ) ] )
% 0.46/1.12  , clause( 651, [ greater( 'e_4', 'e_3' ) ] )
% 0.46/1.12  , clause( 652, [ ~( cycle( X, Y ) ), ~( cycle( X, Z ) ), equalish( Y, Z ) ]
% 0.46/1.12     )
% 0.46/1.12  , clause( 653, [ ~( 'group_element'( X ) ), cycle( X, 'e_0' ), cycle( X, 
% 0.46/1.12    'e_1' ), cycle( X, 'e_2' ), cycle( X, 'e_3' ) ] )
% 0.46/1.12  , clause( 654, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.12  , clause( 655, [ ~( cycle( X, Y ) ), ~( cycle( Z, T ) ), ~( next( X, Z ) )
% 0.46/1.12    , ~( greater( Y, 'e_0' ) ), ~( next( T, U ) ), equalish( Y, U ) ] )
% 0.46/1.12  , clause( 656, [ ~( cycle( X, Y ) ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U
% 0.46/1.12     ) ), ~( next( Z, T ) ), ~( greater( Z, X ) ), ~( greater( Y, U ) ) ] )
% 0.46/1.12  , clause( 657, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( 
% 0.46/1.12    greater( Y, X ) ) ] )
% 0.46/1.12  , clause( 658, [ ~( cycle( X, Y ) ), ~( product( X, 'e_1', Z ) ), ~( 
% 0.46/1.12    greater( Y, 'e_0' ) ), ~( next( X, T ) ), equalish( Z, T ) ] )
% 0.46/1.12  , clause( 659, [ 'group_element'( 'e_1' ) ] )
% 0.46/1.12  , clause( 660, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.12  , clause( 661, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.12  , clause( 662, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.12  , clause( 663, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.46/1.12  , clause( 664, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 0.46/1.12  , clause( 665, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 0.46/1.12  , clause( 666, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 0.46/1.12  , clause( 667, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 0.46/1.12  , clause( 668, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.12  , clause( 669, [ ~( equalish( 'e_3', 'e_1' ) ) ] )
% 0.46/1.12  , clause( 670, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 0.46/1.12  , clause( 671, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 0.46/1.12  , clause( 672, [ ~( equalish( 'e_4', 'e_1' ) ) ] )
% 0.46/1.12  , clause( 673, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.46/1.12  , clause( 674, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.46/1.12  , clause( 675, [ ~( 'group_element'( X ) ), ~( 'group_element'( Y ) ), 
% 0.46/1.12    product( X, Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), 
% 0.46/1.12    product( X, Y, 'e_4' ) ] )
% 0.46/1.12  , clause( 676, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), equalish( 
% 0.46/1.12    Z, T ) ] )
% 0.46/1.12  , clause( 677, [ ~( product( X, Y, Z ) ), ~( product( X, T, Z ) ), equalish( 
% 0.46/1.12    Y, T ) ] )
% 0.46/1.12  , clause( 678, [ ~( product( X, Y, Z ) ), ~( product( T, Y, Z ) ), equalish( 
% 0.46/1.12    X, T ) ] )
% 0.46/1.12  , clause( 679, [ product( X, X, X ) ] )
% 0.46/1.12  , clause( 680, [ ~( product( X, Y, Z ) ), ~( product( Z, X, T ) ), product( 
% 0.46/1.12    T, X, Y ) ] )
% 0.46/1.12  ] ).
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  subsumption(
% 0.46/1.12  clause( 0, [ next( 'e_0', 'e_1' ) ] )
% 0.46/1.12  , clause( 638, [ next( 'e_0', 'e_1' ) ] )
% 0.46/1.12  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  subsumption(
% 0.46/1.12  clause( 1, [ next( 'e_1', 'e_2' ) ] )
% 0.46/1.12  , clause( 639, [ next( 'e_1', 'e_2' ) ] )
% 0.46/1.12  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  subsumption(
% 0.46/1.12  clause( 2, [ next( 'e_2', 'e_3' ) ] )
% 0.46/1.12  , clause( 640, [ next( 'e_2', 'e_3' ) ] )
% 0.46/1.12  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.12  
% 0.46/1.12  
% 0.46/1.12  subsumption(
% 0.46/1.12  clause( 3, [ next( 'e_3', 'e_4' ) ] )
% 0.46/1.12  , clause( 641, [ next( 'e_3', 'e_4' ) ] )
% 0.46/1.12  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 4, [ greater( 'e_1', 'e_0' ) ] )
% 0.46/1.13  , clause( 642, [ greater( 'e_1', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 5, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 643, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 6, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.13  , clause( 644, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , clause( 649, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 12, [ greater( 'e_4', 'e_2' ) ] )
% 0.46/1.13  , clause( 650, [ greater( 'e_4', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 15, [ cycle( X, 'e_3' ), cycle( X, 'e_0' ), cycle( X, 'e_1' ), 
% 0.46/1.13    cycle( X, 'e_2' ), ~( 'group_element'( X ) ) ] )
% 0.46/1.13  , clause( 653, [ ~( 'group_element'( X ) ), cycle( X, 'e_0' ), cycle( X, 
% 0.46/1.13    'e_1' ), cycle( X, 'e_2' ), cycle( X, 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 4 ), ==>( 1, 
% 0.46/1.13    1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.13  , clause( 654, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 17, [ ~( next( X, Z ) ), ~( greater( Y, 'e_0' ) ), equalish( Y, U )
% 0.46/1.13    , ~( cycle( Z, T ) ), ~( cycle( X, Y ) ), ~( next( T, U ) ) ] )
% 0.46/1.13  , clause( 655, [ ~( cycle( X, Y ) ), ~( cycle( Z, T ) ), ~( next( X, Z ) )
% 0.46/1.13    , ~( greater( Y, 'e_0' ) ), ~( next( T, U ) ), equalish( Y, U ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 0.46/1.13    , U )] ), permutation( 0, [ ==>( 0, 4 ), ==>( 1, 3 ), ==>( 2, 0 ), ==>( 3
% 0.46/1.13    , 1 ), ==>( 4, 5 ), ==>( 5, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 18, [ ~( cycle( X, Y ) ), ~( greater( Z, X ) ), ~( greater( Y, U )
% 0.46/1.13     ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U ) ), ~( next( Z, T ) ) ] )
% 0.46/1.13  , clause( 656, [ ~( cycle( X, Y ) ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U
% 0.46/1.13     ) ), ~( next( Z, T ) ), ~( greater( Z, X ) ), ~( greater( Y, U ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 0.46/1.13    , U )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 3 ), ==>( 2, 4 ), ==>( 3
% 0.46/1.13    , 5 ), ==>( 4, 1 ), ==>( 5, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 19, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( 
% 0.46/1.13    greater( Y, X ) ) ] )
% 0.46/1.13  , clause( 657, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( 
% 0.46/1.13    greater( Y, X ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.46/1.13     ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 20, [ ~( cycle( X, Y ) ), ~( greater( Y, 'e_0' ) ), ~( product( X, 
% 0.46/1.13    'e_1', Z ) ), equalish( Z, T ), ~( next( X, T ) ) ] )
% 0.46/1.13  , clause( 658, [ ~( cycle( X, Y ) ), ~( product( X, 'e_1', Z ) ), ~( 
% 0.46/1.13    greater( Y, 'e_0' ) ), ~( next( X, T ) ), equalish( Z, T ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2, 1 ), ==>( 3, 4 ), 
% 0.46/1.13    ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 21, [ 'group_element'( 'e_1' ) ] )
% 0.46/1.13  , clause( 659, [ 'group_element'( 'e_1' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 22, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.13  , clause( 660, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 23, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.13  , clause( 661, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 24, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.13  , clause( 662, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 25, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 663, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 26, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 664, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 27, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 0.46/1.13  , clause( 665, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 28, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 666, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 29, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 667, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 30, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.13  , clause( 668, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 31, [ ~( equalish( 'e_3', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 669, [ ~( equalish( 'e_3', 'e_1' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 32, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 670, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 33, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 0.46/1.13  , clause( 671, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 35, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 673, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 36, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 674, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( X
% 0.46/1.13    , Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~( 
% 0.46/1.13    'group_element'( Y ) ) ] )
% 0.46/1.13  , clause( 675, [ ~( 'group_element'( X ) ), ~( 'group_element'( Y ) ), 
% 0.46/1.13    product( X, Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), 
% 0.46/1.13    product( X, Y, 'e_4' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.46/1.13     ), ==>( 1, 5 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 ), ==>( 5, 1 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 38, [ equalish( Z, T ), ~( product( X, Y, Z ) ), ~( product( X, Y, 
% 0.46/1.13    T ) ) ] )
% 0.46/1.13  , clause( 676, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), equalish( 
% 0.46/1.13    Z, T ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 1 ), ==>( 1, 2 ), ==>( 2, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T, 
% 0.46/1.13    Z ) ) ] )
% 0.46/1.13  , clause( 677, [ ~( product( X, Y, Z ) ), ~( product( X, T, Z ) ), equalish( 
% 0.46/1.13    Y, T ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 1 ), ==>( 1, 2 ), ==>( 2, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 40, [ equalish( X, T ), ~( product( X, Y, Z ) ), ~( product( T, Y, 
% 0.46/1.13    Z ) ) ] )
% 0.46/1.13  , clause( 678, [ ~( product( X, Y, Z ) ), ~( product( T, Y, Z ) ), equalish( 
% 0.46/1.13    X, T ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 1 ), ==>( 1, 2 ), ==>( 2, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 41, [ product( X, X, X ) ] )
% 0.46/1.13  , clause( 679, [ product( X, X, X ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 42, [ ~( product( X, Y, Z ) ), product( T, X, Y ), ~( product( Z, X
% 0.46/1.13    , T ) ) ] )
% 0.46/1.13  , clause( 680, [ ~( product( X, Y, Z ) ), ~( product( Z, X, T ) ), product( 
% 0.46/1.13    T, X, Y ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 0 ), ==>( 1, 2 ), ==>( 2, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1018, [ cycle( 'e_2', 'e_3' ), cycle( 'e_2', 'e_0' ), cycle( 'e_2'
% 0.46/1.13    , 'e_1' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 15, [ cycle( X, 'e_3' ), cycle( X, 'e_0' ), cycle( X, 'e_1' ), 
% 0.46/1.13    cycle( X, 'e_2' ), ~( 'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 22, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 61, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_1' ), cycle( 'e_2', 
% 0.46/1.13    'e_2' ), cycle( 'e_2', 'e_3' ) ] )
% 0.46/1.13  , clause( 1018, [ cycle( 'e_2', 'e_3' ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_1' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1019, [ cycle( 'e_3', 'e_3' ), cycle( 'e_3', 'e_0' ), cycle( 'e_3'
% 0.46/1.13    , 'e_1' ), cycle( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , clause( 15, [ cycle( X, 'e_3' ), cycle( X, 'e_0' ), cycle( X, 'e_1' ), 
% 0.46/1.13    cycle( X, 'e_2' ), ~( 'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 23, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_3' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 62, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ), cycle( 'e_3', 
% 0.46/1.13    'e_2' ), cycle( 'e_3', 'e_3' ) ] )
% 0.46/1.13  , clause( 1019, [ cycle( 'e_3', 'e_3' ), cycle( 'e_3', 'e_0' ), cycle( 
% 0.46/1.13    'e_3', 'e_1' ), cycle( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1021, [ ~( next( X, Y ) ), ~( greater( Z, 'e_0' ) ), equalish( Z, 
% 0.46/1.13    'e_2' ), ~( cycle( Y, 'e_1' ) ), ~( cycle( X, Z ) ) ] )
% 0.46/1.13  , clause( 17, [ ~( next( X, Z ) ), ~( greater( Y, 'e_0' ) ), equalish( Y, U
% 0.46/1.13     ), ~( cycle( Z, T ) ), ~( cycle( X, Y ) ), ~( next( T, U ) ) ] )
% 0.46/1.13  , 5, clause( 1, [ next( 'e_1', 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y ), :=( T, 'e_1' )
% 0.46/1.13    , :=( U, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 65, [ equalish( Z, 'e_2' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y, 
% 0.46/1.13    'e_1' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 0.46/1.13  , clause( 1021, [ ~( next( X, Y ) ), ~( greater( Z, 'e_0' ) ), equalish( Z
% 0.46/1.13    , 'e_2' ), ~( cycle( Y, 'e_1' ) ), ~( cycle( X, Z ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 4 ), ==>( 1, 1 ), ==>( 2, 0 ), ==>( 3, 2 ), 
% 0.46/1.13    ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1024, [ ~( next( X, Y ) ), ~( greater( Z, 'e_0' ) ), equalish( Z, 
% 0.46/1.13    'e_1' ), ~( cycle( Y, 'e_0' ) ), ~( cycle( X, Z ) ) ] )
% 0.46/1.13  , clause( 17, [ ~( next( X, Z ) ), ~( greater( Y, 'e_0' ) ), equalish( Y, U
% 0.46/1.13     ), ~( cycle( Z, T ) ), ~( cycle( X, Y ) ), ~( next( T, U ) ) ] )
% 0.46/1.13  , 5, clause( 0, [ next( 'e_0', 'e_1' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y ), :=( T, 'e_0' )
% 0.46/1.13    , :=( U, 'e_1' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 66, [ equalish( Z, 'e_1' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y, 
% 0.46/1.13    'e_0' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 0.46/1.13  , clause( 1024, [ ~( next( X, Y ) ), ~( greater( Z, 'e_0' ) ), equalish( Z
% 0.46/1.13    , 'e_1' ), ~( cycle( Y, 'e_0' ) ), ~( cycle( X, Z ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 4 ), ==>( 1, 1 ), ==>( 2, 0 ), ==>( 3, 2 ), 
% 0.46/1.13    ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1026, [ ~( cycle( X, Y ) ), ~( greater( 'e_3', X ) ), ~( greater( Y
% 0.46/1.13    , Z ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_4', Z ) ) ] )
% 0.46/1.13  , clause( 18, [ ~( cycle( X, Y ) ), ~( greater( Z, X ) ), ~( greater( Y, U
% 0.46/1.13     ) ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U ) ), ~( next( Z, T ) ) ] )
% 0.46/1.13  , 5, clause( 3, [ next( 'e_3', 'e_4' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, 'e_3' ), :=( T, 
% 0.46/1.13    'e_4' ), :=( U, Z )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 71, [ ~( greater( 'e_3', X ) ), ~( cycle( X, Y ) ), ~( cycle( 'e_3'
% 0.46/1.13    , 'e_0' ) ), ~( cycle( 'e_4', Z ) ), ~( greater( Y, Z ) ) ] )
% 0.46/1.13  , clause( 1026, [ ~( cycle( X, Y ) ), ~( greater( 'e_3', X ) ), ~( greater( 
% 0.46/1.13    Y, Z ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_4', Z ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ), 
% 0.46/1.13    permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2, 4 ), ==>( 3, 2 ), 
% 0.46/1.13    ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1030, [ ~( cycle( 'e_2', 'e_0' ) ), ~( product( 'e_2', 'e_1', 'e_3'
% 0.46/1.13     ) ) ] )
% 0.46/1.13  , clause( 19, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( 
% 0.46/1.13    greater( Y, X ) ) ] )
% 0.46/1.13  , 2, clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' ), :=( Y, 'e_3' )] ), substitution( 1
% 0.46/1.13    , [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 97, [ ~( product( 'e_2', 'e_1', 'e_3' ) ), ~( cycle( 'e_2', 'e_0' )
% 0.46/1.13     ) ] )
% 0.46/1.13  , clause( 1030, [ ~( cycle( 'e_2', 'e_0' ) ), ~( product( 'e_2', 'e_1', 
% 0.46/1.13    'e_3' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1031, [ ~( cycle( 'e_2', 'e_0' ) ), ~( product( 'e_2', 'e_1', 'e_4'
% 0.46/1.13     ) ) ] )
% 0.46/1.13  , clause( 19, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( 
% 0.46/1.13    greater( Y, X ) ) ] )
% 0.46/1.13  , 2, clause( 12, [ greater( 'e_4', 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' ), :=( Y, 'e_4' )] ), substitution( 1
% 0.46/1.13    , [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 98, [ ~( product( 'e_2', 'e_1', 'e_4' ) ), ~( cycle( 'e_2', 'e_0' )
% 0.46/1.13     ) ] )
% 0.46/1.13  , clause( 1031, [ ~( cycle( 'e_2', 'e_0' ) ), ~( product( 'e_2', 'e_1', 
% 0.46/1.13    'e_4' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1032, [ ~( cycle( 'e_2', X ) ), ~( greater( X, 'e_0' ) ), ~( 
% 0.46/1.13    product( 'e_2', 'e_1', Y ) ), equalish( Y, 'e_3' ) ] )
% 0.46/1.13  , clause( 20, [ ~( cycle( X, Y ) ), ~( greater( Y, 'e_0' ) ), ~( product( X
% 0.46/1.13    , 'e_1', Z ) ), equalish( Z, T ), ~( next( X, T ) ) ] )
% 0.46/1.13  , 4, clause( 2, [ next( 'e_2', 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' ), :=( Y, X ), :=( Z, Y ), :=( T, 
% 0.46/1.13    'e_3' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 101, [ ~( product( 'e_2', 'e_1', Y ) ), ~( cycle( 'e_2', X ) ), 
% 0.46/1.13    equalish( Y, 'e_3' ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1032, [ ~( cycle( 'e_2', X ) ), ~( greater( X, 'e_0' ) ), ~( 
% 0.46/1.13    product( 'e_2', 'e_1', Y ) ), equalish( Y, 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 0.46/1.13     ), ==>( 1, 3 ), ==>( 2, 0 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1034, [ ~( 'group_element'( X ) ), product( X, 'e_1', 'e_4' ), 
% 0.46/1.13    product( X, 'e_1', 'e_1' ), product( X, 'e_1', 'e_2' ), product( X, 'e_1'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( 
% 0.46/1.13    X, Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~( 
% 0.46/1.13    'group_element'( Y ) ) ] )
% 0.46/1.13  , 5, clause( 21, [ 'group_element'( 'e_1' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_1' )] ), substitution( 1, [] )
% 0.46/1.13    ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 104, [ product( X, 'e_1', 'e_4' ), product( X, 'e_1', 'e_1' ), 
% 0.46/1.13    product( X, 'e_1', 'e_2' ), product( X, 'e_1', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , clause( 1034, [ ~( 'group_element'( X ) ), product( X, 'e_1', 'e_4' ), 
% 0.46/1.13    product( X, 'e_1', 'e_1' ), product( X, 'e_1', 'e_2' ), product( X, 'e_1'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 4 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1036, [ ~( 'group_element'( X ) ), product( X, 'e_2', 'e_4' ), 
% 0.46/1.13    product( X, 'e_2', 'e_1' ), product( X, 'e_2', 'e_2' ), product( X, 'e_2'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( 
% 0.46/1.13    X, Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~( 
% 0.46/1.13    'group_element'( Y ) ) ] )
% 0.46/1.13  , 5, clause( 22, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_2' )] ), substitution( 1, [] )
% 0.46/1.13    ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 105, [ product( X, 'e_2', 'e_4' ), product( X, 'e_2', 'e_1' ), 
% 0.46/1.13    product( X, 'e_2', 'e_2' ), product( X, 'e_2', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , clause( 1036, [ ~( 'group_element'( X ) ), product( X, 'e_2', 'e_4' ), 
% 0.46/1.13    product( X, 'e_2', 'e_1' ), product( X, 'e_2', 'e_2' ), product( X, 'e_2'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 4 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1038, [ ~( 'group_element'( X ) ), product( X, 'e_3', 'e_4' ), 
% 0.46/1.13    product( X, 'e_3', 'e_1' ), product( X, 'e_3', 'e_2' ), product( X, 'e_3'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( 
% 0.46/1.13    X, Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~( 
% 0.46/1.13    'group_element'( Y ) ) ] )
% 0.46/1.13  , 5, clause( 23, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_3' )] ), substitution( 1, [] )
% 0.46/1.13    ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 106, [ product( X, 'e_3', 'e_4' ), product( X, 'e_3', 'e_1' ), 
% 0.46/1.13    product( X, 'e_3', 'e_2' ), product( X, 'e_3', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , clause( 1038, [ ~( 'group_element'( X ) ), product( X, 'e_3', 'e_4' ), 
% 0.46/1.13    product( X, 'e_3', 'e_1' ), product( X, 'e_3', 'e_2' ), product( X, 'e_3'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 4 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1040, [ ~( 'group_element'( X ) ), product( X, 'e_4', 'e_4' ), 
% 0.46/1.13    product( X, 'e_4', 'e_1' ), product( X, 'e_4', 'e_2' ), product( X, 'e_4'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( 
% 0.46/1.13    X, Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~( 
% 0.46/1.13    'group_element'( Y ) ) ] )
% 0.46/1.13  , 5, clause( 24, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_4' )] ), substitution( 1, [] )
% 0.46/1.13    ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 107, [ product( X, 'e_4', 'e_4' ), product( X, 'e_4', 'e_1' ), 
% 0.46/1.13    product( X, 'e_4', 'e_2' ), product( X, 'e_4', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , clause( 1040, [ ~( 'group_element'( X ) ), product( X, 'e_4', 'e_4' ), 
% 0.46/1.13    product( X, 'e_4', 'e_1' ), product( X, 'e_4', 'e_2' ), product( X, 'e_4'
% 0.46/1.13    , 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 4 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1042, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.46/1.13  , clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T
% 0.46/1.13    , Z ) ) ] )
% 0.46/1.13  , 2, clause( 41, [ product( X, X, X ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Y ), :=( T, Y )] ), 
% 0.46/1.13    substitution( 1, [ :=( X, Y )] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.46/1.13  , clause( 1042, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.46/1.13     ), ==>( 1, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1044, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.46/1.13  , clause( 40, [ equalish( X, T ), ~( product( X, Y, Z ) ), ~( product( T, Y
% 0.46/1.13    , Z ) ) ] )
% 0.46/1.13  , 2, clause( 41, [ product( X, X, X ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y ), :=( T, Y )] ), 
% 0.46/1.13    substitution( 1, [ :=( X, Y )] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.46/1.13  , clause( 1044, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 0.46/1.13     ), ==>( 1, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1045, [ ~( product( 'e_2', 'e_1', X ) ), ~( cycle( 'e_2', 'e_2' ) )
% 0.46/1.13    , equalish( X, 'e_3' ) ] )
% 0.46/1.13  , clause( 101, [ ~( product( 'e_2', 'e_1', Y ) ), ~( cycle( 'e_2', X ) ), 
% 0.46/1.13    equalish( Y, 'e_3' ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.13  , 3, clause( 5, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' ), :=( Y, X )] ), substitution( 1, [] )
% 0.46/1.13    ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 143, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~( 
% 0.46/1.13    cycle( 'e_2', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 1045, [ ~( product( 'e_2', 'e_1', X ) ), ~( cycle( 'e_2', 'e_2' )
% 0.46/1.13     ), equalish( X, 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.46/1.13    2 ), ==>( 2, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1046, [ equalish( X, 'e_2' ), ~( greater( X, 'e_0' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_1' ) ), ~( cycle( 'e_2', X ) ) ] )
% 0.46/1.13  , clause( 65, [ equalish( Z, 'e_2' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y
% 0.46/1.13    , 'e_1' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 0.46/1.13  , 4, clause( 2, [ next( 'e_2', 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' ), :=( Y, 'e_3' ), :=( Z, X )] ), 
% 0.46/1.13    substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 174, [ equalish( X, 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 
% 0.46/1.13    'e_2', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1046, [ equalish( X, 'e_2' ), ~( greater( X, 'e_0' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_1' ) ), ~( cycle( 'e_2', X ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.46/1.13    3 ), ==>( 2, 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1047, [ equalish( X, 'e_1' ), ~( greater( X, 'e_0' ) ), ~( cycle( 
% 0.46/1.13    'e_4', 'e_0' ) ), ~( cycle( 'e_3', X ) ) ] )
% 0.46/1.13  , clause( 66, [ equalish( Z, 'e_1' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y
% 0.46/1.13    , 'e_0' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 0.46/1.13  , 4, clause( 3, [ next( 'e_3', 'e_4' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_3' ), :=( Y, 'e_4' ), :=( Z, X )] ), 
% 0.46/1.13    substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1048, [ equalish( X, 'e_1' ), ~( greater( X, 'e_0' ) ), ~( cycle( 
% 0.46/1.13    'e_3', X ) ) ] )
% 0.46/1.13  , clause( 1047, [ equalish( X, 'e_1' ), ~( greater( X, 'e_0' ) ), ~( cycle( 
% 0.46/1.13    'e_4', 'e_0' ) ), ~( cycle( 'e_3', X ) ) ] )
% 0.46/1.13  , 2, clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 182, [ equalish( X, 'e_1' ), ~( cycle( 'e_3', X ) ), ~( greater( X
% 0.46/1.13    , 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1048, [ equalish( X, 'e_1' ), ~( greater( X, 'e_0' ) ), ~( cycle( 
% 0.46/1.13    'e_3', X ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.46/1.13    2 ), ==>( 2, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1049, [ equalish( 'e_2', 'e_1' ), ~( cycle( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 182, [ equalish( X, 'e_1' ), ~( cycle( 'e_3', X ) ), ~( greater( 
% 0.46/1.13    X, 'e_0' ) ) ] )
% 0.46/1.13  , 2, clause( 5, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1050, [ ~( cycle( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 28, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , 0, clause( 1049, [ equalish( 'e_2', 'e_1' ), ~( cycle( 'e_3', 'e_2' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 185, [ ~( cycle( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 1050, [ ~( cycle( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1051, [ equalish( 'e_3', 'e_1' ), ~( cycle( 'e_3', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 182, [ equalish( X, 'e_1' ), ~( cycle( 'e_3', X ) ), ~( greater( 
% 0.46/1.13    X, 'e_0' ) ) ] )
% 0.46/1.13  , 2, clause( 6, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_3' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1052, [ ~( cycle( 'e_3', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 31, [ ~( equalish( 'e_3', 'e_1' ) ) ] )
% 0.46/1.13  , 0, clause( 1051, [ equalish( 'e_3', 'e_1' ), ~( cycle( 'e_3', 'e_3' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 186, [ ~( cycle( 'e_3', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 1052, [ ~( cycle( 'e_3', 'e_3' ) ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1053, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_1' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ), ~( cycle( 'e_4', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 71, [ ~( greater( 'e_3', X ) ), ~( cycle( X, Y ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ), ~( cycle( 'e_4', Z ) ), ~( greater( Y, Z ) ) ] )
% 0.46/1.13  , 4, clause( 4, [ greater( 'e_1', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_1' ), :=( Z, 'e_0' )] ), 
% 0.46/1.13    substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1054, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_1' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1053, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_1' ) ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_4', 'e_0' ) ) ] )
% 0.46/1.13  , 3, clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 189, [ ~( cycle( X, 'e_1' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.13    greater( 'e_3', X ) ) ] )
% 0.46/1.13  , clause( 1054, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_1' ) ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1055, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_2' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ), ~( cycle( 'e_4', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 71, [ ~( greater( 'e_3', X ) ), ~( cycle( X, Y ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ), ~( cycle( 'e_4', Z ) ), ~( greater( Y, Z ) ) ] )
% 0.46/1.13  , 4, clause( 5, [ greater( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_2' ), :=( Z, 'e_0' )] ), 
% 0.46/1.13    substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1056, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_2' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1055, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_2' ) ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_4', 'e_0' ) ) ] )
% 0.46/1.13  , 3, clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 190, [ ~( cycle( X, 'e_2' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.13    greater( 'e_3', X ) ) ] )
% 0.46/1.13  , clause( 1056, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_2' ) ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1058, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_3' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ), ~( cycle( 'e_4', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 71, [ ~( greater( 'e_3', X ) ), ~( cycle( X, Y ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ), ~( cycle( 'e_4', Z ) ), ~( greater( Y, Z ) ) ] )
% 0.46/1.13  , 4, clause( 6, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X ), :=( Y, 'e_3' ), :=( Z, 'e_0' )] ), 
% 0.46/1.13    substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1059, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_3' ) ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1058, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_3' ) ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_4', 'e_0' ) ) ] )
% 0.46/1.13  , 3, clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 191, [ ~( cycle( X, 'e_3' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.13    greater( 'e_3', X ) ) ] )
% 0.46/1.13  , clause( 1059, [ ~( greater( 'e_3', X ) ), ~( cycle( X, 'e_3' ) ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 
% 0.46/1.13    0 ), ==>( 2, 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1060, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ), cycle( 'e_3'
% 0.46/1.13    , 'e_2' ) ] )
% 0.46/1.13  , clause( 186, [ ~( cycle( 'e_3', 'e_3' ) ) ] )
% 0.46/1.13  , 0, clause( 62, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ), cycle( 
% 0.46/1.13    'e_3', 'e_2' ), cycle( 'e_3', 'e_3' ) ] )
% 0.46/1.13  , 3, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1061, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ) ] )
% 0.46/1.13  , clause( 185, [ ~( cycle( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , 0, clause( 1060, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ), cycle( 
% 0.46/1.13    'e_3', 'e_2' ) ] )
% 0.46/1.13  , 2, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 194, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ) ] )
% 0.46/1.13  , clause( 1061, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1062, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 189, [ ~( cycle( X, 'e_1' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.13    greater( 'e_3', X ) ) ] )
% 0.46/1.13  , 2, clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 207, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 1062, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( 'e_3', 'e_0' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1063, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 190, [ ~( cycle( X, 'e_2' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.13    greater( 'e_3', X ) ) ] )
% 0.46/1.13  , 2, clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 220, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_2' ) ) ] )
% 0.46/1.13  , clause( 1063, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( 'e_3', 'e_0' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1064, [ ~( cycle( 'e_2', 'e_3' ) ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 191, [ ~( cycle( X, 'e_3' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~( 
% 0.46/1.13    greater( 'e_3', X ) ) ] )
% 0.46/1.13  , 2, clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 232, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 1064, [ ~( cycle( 'e_2', 'e_3' ) ), ~( cycle( 'e_3', 'e_0' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1065, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_1' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 232, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_3' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 1, clause( 61, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_1' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ), cycle( 'e_2', 'e_3' ) ] )
% 0.46/1.13  , 3, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1066, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_3', 'e_0' ) ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 207, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_1' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 1, clause( 1065, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ), 
% 0.46/1.13    cycle( 'e_2', 'e_1' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , 2, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  factor(
% 0.46/1.13  clause( 1067, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 1066, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_3', 'e_0' ) ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , 0, 1, substitution( 0, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 234, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1067, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1068, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 220, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_2' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 1, clause( 234, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  factor(
% 0.46/1.13  clause( 1069, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 1068, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ), ~( 
% 0.46/1.13    cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , 0, 2, substitution( 0, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 235, [ cycle( 'e_2', 'e_0' ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , clause( 1069, [ ~( cycle( 'e_3', 'e_0' ) ), cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1070, [ equalish( 'e_1', 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( 
% 0.46/1.13    cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 174, [ equalish( X, 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 
% 0.46/1.13    'e_2', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.13  , 3, clause( 4, [ greater( 'e_1', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1071, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 25, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.46/1.13  , 0, clause( 1070, [ equalish( 'e_1', 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), 
% 0.46/1.13    ~( cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 248, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 1071, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_1' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1072, [ equalish( 'e_3', 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( 
% 0.46/1.13    cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 174, [ equalish( X, 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 
% 0.46/1.13    'e_2', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 0.46/1.13  , 3, clause( 6, [ greater( 'e_3', 'e_0' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_3' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1073, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 32, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 0.46/1.13  , 0, clause( 1072, [ equalish( 'e_3', 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), 
% 0.46/1.13    ~( cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 249, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 1073, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_3' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1074, [ ~( cycle( 'e_3', 'e_1' ) ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_1' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 249, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_3' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 1, clause( 61, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_1' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ), cycle( 'e_2', 'e_3' ) ] )
% 0.46/1.13  , 3, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1075, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_3', 'e_1' ) ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 248, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_1' ) ) ]
% 0.46/1.13     )
% 0.46/1.13  , 1, clause( 1074, [ ~( cycle( 'e_3', 'e_1' ) ), cycle( 'e_2', 'e_0' ), 
% 0.46/1.13    cycle( 'e_2', 'e_1' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , 2, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  factor(
% 0.46/1.13  clause( 1076, [ ~( cycle( 'e_3', 'e_1' ) ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 1075, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_3', 'e_1' ) ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , 0, 1, substitution( 0, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 251, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_1' ) ) ] )
% 0.46/1.13  , clause( 1076, [ ~( cycle( 'e_3', 'e_1' ) ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1077, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), cycle( 'e_3'
% 0.46/1.13    , 'e_0' ) ] )
% 0.46/1.13  , clause( 251, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), ~( cycle( 
% 0.46/1.13    'e_3', 'e_1' ) ) ] )
% 0.46/1.13  , 2, clause( 194, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ) ] )
% 0.46/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1078, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_0' ), cycle( 'e_2'
% 0.46/1.13    , 'e_2' ) ] )
% 0.46/1.13  , clause( 235, [ cycle( 'e_2', 'e_0' ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 0.46/1.13  , 1, clause( 1077, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ), cycle( 
% 0.46/1.13    'e_3', 'e_0' ) ] )
% 0.46/1.13  , 2, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  factor(
% 0.46/1.13  clause( 1079, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 1078, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_0' ), cycle( 
% 0.46/1.13    'e_2', 'e_2' ) ] )
% 0.46/1.13  , 0, 1, substitution( 0, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 252, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 1079, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.46/1.13     ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1080, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 143, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~( 
% 0.46/1.13    cycle( 'e_2', 'e_2' ) ) ] )
% 0.46/1.13  , 2, clause( 252, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 0.46/1.13  , 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 253, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( 
% 0.46/1.13    'e_2', 'e_1', X ) ) ] )
% 0.46/1.13  , clause( 1080, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 
% 0.46/1.13    1 ), ==>( 2, 0 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1081, [ product( 'e_2', 'e_1', 'e_4' ), product( 'e_2', 'e_1', 
% 0.46/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , clause( 104, [ product( X, 'e_1', 'e_4' ), product( X, 'e_1', 'e_1' ), 
% 0.46/1.13    product( X, 'e_1', 'e_2' ), product( X, 'e_1', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 22, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 260, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2'
% 0.46/1.13     ), product( 'e_2', 'e_1', 'e_3' ), product( 'e_2', 'e_1', 'e_4' ) ] )
% 0.46/1.13  , clause( 1081, [ product( 'e_2', 'e_1', 'e_4' ), product( 'e_2', 'e_1', 
% 0.46/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1082, [ product( 'e_4', 'e_1', 'e_4' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_1' ), product( 'e_4', 'e_1', 'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , clause( 104, [ product( X, 'e_1', 'e_4' ), product( X, 'e_1', 'e_1' ), 
% 0.46/1.13    product( X, 'e_1', 'e_2' ), product( X, 'e_1', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 24, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_4' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 262, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 'e_2'
% 0.46/1.13     ), product( 'e_4', 'e_1', 'e_3' ), product( 'e_4', 'e_1', 'e_4' ) ] )
% 0.46/1.13  , clause( 1082, [ product( 'e_4', 'e_1', 'e_4' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_1' ), product( 'e_4', 'e_1', 'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1083, [ product( 'e_4', 'e_2', 'e_4' ), product( 'e_4', 'e_2', 
% 0.46/1.13    'e_1' ), product( 'e_4', 'e_2', 'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , clause( 105, [ product( X, 'e_2', 'e_4' ), product( X, 'e_2', 'e_1' ), 
% 0.46/1.13    product( X, 'e_2', 'e_2' ), product( X, 'e_2', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 24, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_4' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 268, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2'
% 0.46/1.13     ), product( 'e_4', 'e_2', 'e_3' ), product( 'e_4', 'e_2', 'e_4' ) ] )
% 0.46/1.13  , clause( 1083, [ product( 'e_4', 'e_2', 'e_4' ), product( 'e_4', 'e_2', 
% 0.46/1.13    'e_1' ), product( 'e_4', 'e_2', 'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1084, [ product( 'e_4', 'e_3', 'e_4' ), product( 'e_4', 'e_3', 
% 0.46/1.13    'e_1' ), product( 'e_4', 'e_3', 'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , clause( 106, [ product( X, 'e_3', 'e_4' ), product( X, 'e_3', 'e_1' ), 
% 0.46/1.13    product( X, 'e_3', 'e_2' ), product( X, 'e_3', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 24, [ 'group_element'( 'e_4' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_4' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 274, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 'e_2'
% 0.46/1.13     ), product( 'e_4', 'e_3', 'e_3' ), product( 'e_4', 'e_3', 'e_4' ) ] )
% 0.46/1.13  , clause( 1084, [ product( 'e_4', 'e_3', 'e_4' ), product( 'e_4', 'e_3', 
% 0.46/1.13    'e_1' ), product( 'e_4', 'e_3', 'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1085, [ product( 'e_2', 'e_4', 'e_4' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_1' ), product( 'e_2', 'e_4', 'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , clause( 107, [ product( X, 'e_4', 'e_4' ), product( X, 'e_4', 'e_1' ), 
% 0.46/1.13    product( X, 'e_4', 'e_2' ), product( X, 'e_4', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 22, [ 'group_element'( 'e_2' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 280, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 'e_2'
% 0.46/1.13     ), product( 'e_2', 'e_4', 'e_3' ), product( 'e_2', 'e_4', 'e_4' ) ] )
% 0.46/1.13  , clause( 1085, [ product( 'e_2', 'e_4', 'e_4' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_1' ), product( 'e_2', 'e_4', 'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1086, [ product( 'e_3', 'e_4', 'e_4' ), product( 'e_3', 'e_4', 
% 0.46/1.13    'e_1' ), product( 'e_3', 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , clause( 107, [ product( X, 'e_4', 'e_4' ), product( X, 'e_4', 'e_1' ), 
% 0.46/1.13    product( X, 'e_4', 'e_2' ), product( X, 'e_4', 'e_3' ), ~( 
% 0.46/1.13    'group_element'( X ) ) ] )
% 0.46/1.13  , 4, clause( 23, [ 'group_element'( 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [ :=( X, 'e_3' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 281, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 'e_2'
% 0.46/1.13     ), product( 'e_3', 'e_4', 'e_3' ), product( 'e_3', 'e_4', 'e_4' ) ] )
% 0.46/1.13  , clause( 1086, [ product( 'e_3', 'e_4', 'e_4' ), product( 'e_3', 'e_4', 
% 0.46/1.13    'e_1' ), product( 'e_3', 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ]
% 0.46/1.13     )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 3 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1090, [ cycle( 'e_2', 'e_0' ), equalish( 'e_4', 'e_3' ), product( 
% 0.46/1.13    'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), product( 'e_2', 
% 0.46/1.13    'e_1', 'e_3' ) ] )
% 0.46/1.13  , clause( 253, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( 
% 0.46/1.13    'e_2', 'e_1', X ) ) ] )
% 0.46/1.13  , 2, clause( 260, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_3' ), product( 'e_2', 'e_1', 'e_4' ) ]
% 0.46/1.13     )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_4' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1091, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.46/1.13    product( 'e_2', 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , clause( 36, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.46/1.13  , 0, clause( 1090, [ cycle( 'e_2', 'e_0' ), equalish( 'e_4', 'e_3' ), 
% 0.46/1.13    product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), product( 
% 0.46/1.13    'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 320, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2'
% 0.46/1.13     ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , clause( 1091, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.46/1.13    product( 'e_2', 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 0 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1092, [ equalish( 'e_2', 'e_4' ), product( 'e_2', 'e_4', 'e_1' ), 
% 0.46/1.13    product( 'e_2', 'e_4', 'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.46/1.13  , 1, clause( 280, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_4', 'e_3' ), product( 'e_2', 'e_4', 'e_4' ) ]
% 0.46/1.13     )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_2' ), :=( Y, 'e_4' )] ), substitution( 1
% 0.46/1.13    , [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1093, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , clause( 30, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.13  , 0, clause( 1092, [ equalish( 'e_2', 'e_4' ), product( 'e_2', 'e_4', 'e_1'
% 0.46/1.13     ), product( 'e_2', 'e_4', 'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 329, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 'e_2'
% 0.46/1.13     ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , clause( 1093, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.46/1.13    , 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1099, [ equalish( X, 'e_4' ), ~( product( 'e_2', X, 'e_3' ) ), 
% 0.46/1.13    product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 'e_2' ) ] )
% 0.46/1.13  , clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T
% 0.46/1.13    , Z ) ) ] )
% 0.46/1.13  , 2, clause( 329, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , 2, substitution( 0, [ :=( X, 'e_2' ), :=( Y, X ), :=( Z, 'e_3' ), :=( T, 
% 0.46/1.13    'e_4' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 337, [ product( 'e_2', 'e_4', 'e_1' ), equalish( X, 'e_4' ), 
% 0.46/1.13    product( 'e_2', 'e_4', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 0.46/1.13  , clause( 1099, [ equalish( X, 'e_4' ), ~( product( 'e_2', X, 'e_3' ) ), 
% 0.46/1.13    product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 
% 0.46/1.13    3 ), ==>( 2, 0 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1100, [ product( 'e_2', 'e_4', 'e_1' ), equalish( 'e_1', 'e_4' ), 
% 0.46/1.13    product( 'e_2', 'e_4', 'e_2' ), product( 'e_2', 'e_1', 'e_1' ), product( 
% 0.46/1.13    'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 337, [ product( 'e_2', 'e_4', 'e_1' ), equalish( X, 'e_4' ), 
% 0.46/1.13    product( 'e_2', 'e_4', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 0.46/1.13  , 3, clause( 320, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.46/1.13    'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1101, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 27, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 0.46/1.13  , 0, clause( 1100, [ product( 'e_2', 'e_4', 'e_1' ), equalish( 'e_1', 'e_4'
% 0.46/1.13     ), product( 'e_2', 'e_4', 'e_2' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.46/1.13    product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 339, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_1', 'e_1'
% 0.46/1.13     ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_2'
% 0.46/1.13    , 'e_4', 'e_2' ) ] )
% 0.46/1.13  , clause( 1101, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 4 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1102, [ equalish( 'e_1', 'e_4' ), product( 'e_4', 'e_1', 'e_1' ), 
% 0.46/1.13    product( 'e_4', 'e_1', 'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.46/1.13  , 1, clause( 262, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_1', 'e_3' ), product( 'e_4', 'e_1', 'e_4' ) ]
% 0.46/1.13     )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_1' ), :=( Y, 'e_4' )] ), substitution( 1
% 0.46/1.13    , [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1103, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , clause( 27, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 0.46/1.13  , 0, clause( 1102, [ equalish( 'e_1', 'e_4' ), product( 'e_4', 'e_1', 'e_1'
% 0.46/1.13     ), product( 'e_4', 'e_1', 'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 343, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 'e_2'
% 0.46/1.13     ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , clause( 1103, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.46/1.13    , 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1109, [ equalish( X, 'e_4' ), ~( product( X, 'e_1', 'e_3' ) ), 
% 0.46/1.13    product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 'e_2' ) ] )
% 0.46/1.13  , clause( 40, [ equalish( X, T ), ~( product( X, Y, Z ) ), ~( product( T, Y
% 0.46/1.13    , Z ) ) ] )
% 0.46/1.13  , 2, clause( 343, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , 2, substitution( 0, [ :=( X, X ), :=( Y, 'e_1' ), :=( Z, 'e_3' ), :=( T, 
% 0.46/1.13    'e_4' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 345, [ product( 'e_4', 'e_1', 'e_1' ), equalish( X, 'e_4' ), 
% 0.46/1.13    product( 'e_4', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 0.46/1.13  , clause( 1109, [ equalish( X, 'e_4' ), ~( product( X, 'e_1', 'e_3' ) ), 
% 0.46/1.13    product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 
% 0.46/1.13    3 ), ==>( 2, 0 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1110, [ product( 'e_4', 'e_1', 'e_1' ), equalish( 'e_2', 'e_4' ), 
% 0.46/1.13    product( 'e_4', 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_1' ), product( 
% 0.46/1.13    'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 345, [ product( 'e_4', 'e_1', 'e_1' ), equalish( X, 'e_4' ), 
% 0.46/1.13    product( 'e_4', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 0.46/1.13  , 3, clause( 320, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.46/1.13    'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1111, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , clause( 30, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.13  , 0, clause( 1110, [ product( 'e_4', 'e_1', 'e_1' ), equalish( 'e_2', 'e_4'
% 0.46/1.13     ), product( 'e_4', 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.46/1.13    product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 348, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_1'
% 0.46/1.13     ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_4'
% 0.46/1.13    , 'e_1', 'e_2' ) ] )
% 0.46/1.13  , clause( 1111, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_1', 
% 0.46/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), 
% 0.46/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 4 ), ==>( 2
% 0.46/1.13    , 1 ), ==>( 3, 2 ), ==>( 4, 3 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1112, [ equalish( 'e_2', 'e_4' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.46/1.13    product( 'e_4', 'e_2', 'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.46/1.13  , 1, clause( 268, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_3' ), product( 'e_4', 'e_2', 'e_4' ) ]
% 0.46/1.13     )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_2' ), :=( Y, 'e_4' )] ), substitution( 1
% 0.46/1.13    , [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1113, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.13  , clause( 30, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 0.46/1.13  , 0, clause( 1112, [ equalish( 'e_2', 'e_4' ), product( 'e_4', 'e_2', 'e_1'
% 0.46/1.13     ), product( 'e_4', 'e_2', 'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 369, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2'
% 0.46/1.13     ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.13  , clause( 1113, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.46/1.13    , 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1119, [ equalish( X, 'e_3' ), ~( product( 'e_4', 'e_2', X ) ), 
% 0.46/1.13    product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.46/1.13  , clause( 38, [ equalish( Z, T ), ~( product( X, Y, Z ) ), ~( product( X, Y
% 0.46/1.13    , T ) ) ] )
% 0.46/1.13  , 2, clause( 369, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 
% 0.46/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.46/1.13  , 2, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_2' ), :=( Z, X ), :=( T, 
% 0.46/1.13    'e_3' )] ), substitution( 1, [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  subsumption(
% 0.46/1.13  clause( 374, [ product( 'e_4', 'e_2', 'e_1' ), equalish( X, 'e_3' ), 
% 0.46/1.13    product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_4', 'e_2', X ) ) ] )
% 0.46/1.13  , clause( 1119, [ equalish( X, 'e_3' ), ~( product( 'e_4', 'e_2', X ) ), 
% 0.46/1.13    product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.46/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 
% 0.46/1.13    3 ), ==>( 2, 0 ), ==>( 3, 2 )] ) ).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1120, [ equalish( 'e_3', 'e_4' ), product( 'e_3', 'e_4', 'e_1' ), 
% 0.46/1.13    product( 'e_3', 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.46/1.13  , 1, clause( 281, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_3', 'e_4', 'e_3' ), product( 'e_3', 'e_4', 'e_4' ) ]
% 0.46/1.13     )
% 0.46/1.13  , 3, substitution( 0, [ :=( X, 'e_3' ), :=( Y, 'e_4' )] ), substitution( 1
% 0.46/1.13    , [] )).
% 0.46/1.13  
% 0.46/1.13  
% 0.46/1.13  resolution(
% 0.46/1.13  clause( 1121, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.46/1.13    'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.46/1.13  , clause( 33, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 0.46/1.13  , 0, clause( 1120, [ equalish( 'e_3', 'e_4' ), product( 'e_3', 'e_4', 'e_1'
% 0.46/1.13     ), product( 'e_3', 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 390, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 'e_2'
% 0.77/1.13     ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.77/1.13  , clause( 1121, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.77/1.13    , 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1122, [ equalish( 'e_4', 'e_3' ), product( 'e_3', 'e_4', 'e_1' ), 
% 0.77/1.13    product( 'e_3', 'e_4', 'e_2' ) ] )
% 0.77/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.77/1.13  , 1, clause( 390, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_2' ), product( 'e_3', 'e_4', 'e_3' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_3' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1123, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , clause( 36, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 1122, [ equalish( 'e_4', 'e_3' ), product( 'e_3', 'e_4', 'e_1'
% 0.77/1.13     ), product( 'e_3', 'e_4', 'e_2' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 396, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 'e_2'
% 0.77/1.13     ) ] )
% 0.77/1.13  , clause( 1123, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.77/1.13     ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1124, [ equalish( 'e_3', 'e_4' ), product( 'e_4', 'e_3', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.77/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.77/1.13  , 1, clause( 274, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_3', 'e_3' ), product( 'e_4', 'e_3', 'e_4' ) ]
% 0.77/1.13     )
% 0.77/1.13  , 3, substitution( 0, [ :=( X, 'e_3' ), :=( Y, 'e_4' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1125, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.77/1.13  , clause( 33, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 0.77/1.13  , 0, clause( 1124, [ equalish( 'e_3', 'e_4' ), product( 'e_4', 'e_3', 'e_1'
% 0.77/1.13     ), product( 'e_4', 'e_3', 'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 400, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 'e_2'
% 0.77/1.13     ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.77/1.13  , clause( 1125, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.77/1.13    , 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1129, [ ~( product( 'e_4', X, 'e_3' ) ), product( 'e_2', 'e_4', X )
% 0.77/1.13    , product( 'e_3', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , clause( 42, [ ~( product( X, Y, Z ) ), product( T, X, Y ), ~( product( Z
% 0.77/1.13    , X, T ) ) ] )
% 0.77/1.13  , 2, clause( 396, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , 1, substitution( 0, [ :=( X, 'e_4' ), :=( Y, X ), :=( Z, 'e_3' ), :=( T, 
% 0.77/1.13    'e_2' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 402, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_2', 'e_4', X ), 
% 0.77/1.13    ~( product( 'e_4', X, 'e_3' ) ) ] )
% 0.77/1.13  , clause( 1129, [ ~( product( 'e_4', X, 'e_3' ) ), product( 'e_2', 'e_4', X
% 0.77/1.13     ), product( 'e_3', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 
% 0.77/1.13    1 ), ==>( 2, 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1130, [ equalish( 'e_4', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_2' ) ] )
% 0.77/1.13  , clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.77/1.13  , 1, clause( 400, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_3', 'e_3' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_3' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1131, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , clause( 36, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 1130, [ equalish( 'e_4', 'e_3' ), product( 'e_4', 'e_3', 'e_1'
% 0.77/1.13     ), product( 'e_4', 'e_3', 'e_2' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 414, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 'e_2'
% 0.77/1.13     ) ] )
% 0.77/1.13  , clause( 1131, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.77/1.13     ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1135, [ equalish( X, 'e_3' ), ~( product( 'e_4', X, 'e_2' ) ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T
% 0.77/1.13    , Z ) ) ] )
% 0.77/1.13  , 2, clause( 414, [ product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_3', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , 1, substitution( 0, [ :=( X, 'e_4' ), :=( Y, X ), :=( Z, 'e_2' ), :=( T, 
% 0.77/1.13    'e_3' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 418, [ equalish( X, 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), ~( 
% 0.77/1.13    product( 'e_4', X, 'e_2' ) ) ] )
% 0.77/1.13  , clause( 1135, [ equalish( X, 'e_3' ), ~( product( 'e_4', X, 'e_2' ) ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.77/1.13    2 ), ==>( 2, 1 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1136, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ]
% 0.77/1.13     )
% 0.77/1.13  , clause( 402, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_2', 'e_4', X )
% 0.77/1.13    , ~( product( 'e_4', X, 'e_3' ) ) ] )
% 0.77/1.13  , 2, clause( 369, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 428, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_4', 'e_2', 'e_1'
% 0.77/1.13     ), product( 'e_4', 'e_2', 'e_2' ), product( 'e_2', 'e_4', 'e_2' ) ] )
% 0.77/1.13  , clause( 1136, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_2', 'e_4', 
% 0.77/1.13    'e_2' ), product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ]
% 0.77/1.13     )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 3 ), ==>( 2
% 0.77/1.13    , 1 ), ==>( 3, 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1137, [ equalish( 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.77/1.13  , 1, clause( 428, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_4', 'e_2', 
% 0.77/1.13    'e_1' ), product( 'e_4', 'e_2', 'e_2' ), product( 'e_2', 'e_4', 'e_2' ) ]
% 0.77/1.13     )
% 0.77/1.13  , 3, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_2' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1138, [ equalish( 'e_4', 'e_2' ), equalish( 'e_4', 'e_2' ), product( 
% 0.77/1.13    'e_3', 'e_4', 'e_1' ), product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.77/1.13  , 1, clause( 1137, [ equalish( 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_1'
% 0.77/1.13     ), product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , 3, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_2' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1139, [ equalish( 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 1138, [ equalish( 'e_4', 'e_2' ), equalish( 'e_4', 'e_2' ), 
% 0.77/1.13    product( 'e_3', 'e_4', 'e_1' ), product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , 0, 1, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 446, [ product( 'e_4', 'e_2', 'e_1' ), equalish( 'e_4', 'e_2' ), 
% 0.77/1.13    product( 'e_3', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , clause( 1139, [ equalish( 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_1' )
% 0.77/1.13    , product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 2 ), ==>( 2
% 0.77/1.13    , 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1140, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_1' ) ] )
% 0.77/1.13  , clause( 35, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.77/1.13  , 0, clause( 446, [ product( 'e_4', 'e_2', 'e_1' ), equalish( 'e_4', 'e_2'
% 0.77/1.13     ), product( 'e_3', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 447, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_3', 'e_4', 'e_1'
% 0.77/1.13     ) ] )
% 0.77/1.13  , clause( 1140, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.77/1.13     ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1144, [ equalish( X, 'e_3' ), ~( product( X, 'e_4', 'e_1' ) ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 40, [ equalish( X, T ), ~( product( X, Y, Z ) ), ~( product( T, Y
% 0.77/1.13    , Z ) ) ] )
% 0.77/1.13  , 2, clause( 447, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_3', 'e_4', 
% 0.77/1.13    'e_1' ) ] )
% 0.77/1.13  , 1, substitution( 0, [ :=( X, X ), :=( Y, 'e_4' ), :=( Z, 'e_1' ), :=( T, 
% 0.77/1.13    'e_3' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 450, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_1' ), ~( 
% 0.77/1.13    product( X, 'e_4', 'e_1' ) ) ] )
% 0.77/1.13  , clause( 1144, [ equalish( X, 'e_3' ), ~( product( X, 'e_4', 'e_1' ) ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 
% 0.77/1.13    2 ), ==>( 2, 1 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1146, [ equalish( 'e_4', 'e_2' ), product( 'e_2', 'e_4', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 
% 0.77/1.13    'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.77/1.13  , 1, clause( 339, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 
% 0.77/1.13    'e_2', 'e_4', 'e_2' ) ] )
% 0.77/1.13  , 4, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_2' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1147, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 35, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.77/1.13  , 0, clause( 1146, [ equalish( 'e_4', 'e_2' ), product( 'e_2', 'e_4', 'e_1'
% 0.77/1.13     ), product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 
% 0.77/1.13    'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 501, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_4', 'e_1'
% 0.77/1.13     ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , clause( 1147, [ product( 'e_2', 'e_4', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2
% 0.77/1.13    , 3 ), ==>( 3, 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1149, [ cycle( 'e_2', 'e_0' ), equalish( 'e_2', 'e_3' ), product( 
% 0.77/1.13    'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_4', 'e_1' ), cycle( 'e_2', 
% 0.77/1.13    'e_0' ) ] )
% 0.77/1.13  , clause( 253, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( 
% 0.77/1.13    'e_2', 'e_1', X ) ) ] )
% 0.77/1.13  , 2, clause( 501, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_4', 
% 0.77/1.13    'e_1' ), cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , 3, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1152, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_4', 'e_1' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 29, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 1149, [ cycle( 'e_2', 'e_0' ), equalish( 'e_2', 'e_3' ), 
% 0.77/1.13    product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_4', 'e_1' ), cycle( 
% 0.77/1.13    'e_2', 'e_0' ) ] )
% 0.77/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1153, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , clause( 1152, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_4', 'e_1' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, 3, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 504, [ product( 'e_2', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    product( 'e_2', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , clause( 1153, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2
% 0.77/1.13    , 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1154, [ equalish( 'e_2', 'e_3' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 450, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_1' ), ~( 
% 0.77/1.13    product( X, 'e_4', 'e_1' ) ) ] )
% 0.77/1.13  , 2, clause( 504, [ product( 'e_2', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    product( 'e_2', 'e_4', 'e_1' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_2' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1155, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_1' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 29, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 1154, [ equalish( 'e_2', 'e_3' ), product( 'e_4', 'e_2', 'e_1'
% 0.77/1.13     ), product( 'e_2', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 505, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 1155, [ product( 'e_4', 'e_2', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_1' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1, 1 ), ==>( 2
% 0.77/1.13    , 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1156, [ product( 'e_4', 'e_2', 'e_1' ), equalish( 'e_1', 'e_3' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_2', 
% 0.77/1.13    'e_1', 'e_1' ) ] )
% 0.77/1.13  , clause( 374, [ product( 'e_4', 'e_2', 'e_1' ), equalish( X, 'e_3' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_4', 'e_2', X ) ) ] )
% 0.77/1.13  , 3, clause( 505, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1157, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_2', 
% 0.77/1.13    'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 253, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( 
% 0.77/1.13    'e_2', 'e_1', X ) ) ] )
% 0.77/1.13  , 2, clause( 1156, [ product( 'e_4', 'e_2', 'e_1' ), equalish( 'e_1', 'e_3'
% 0.77/1.13     ), product( 'e_4', 'e_2', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_2'
% 0.77/1.13    , 'e_1', 'e_1' ) ] )
% 0.77/1.13  , 4, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1158, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_2', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , clause( 1157, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_2', 
% 0.77/1.13    'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, 5, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1159, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , clause( 1158, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_2', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , 1, 3, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 512, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , clause( 1159, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.77/1.13    , 2 ), ==>( 3, 3 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1160, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , clause( 26, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 512, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ), product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 517, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , clause( 1160, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.77/1.13    , 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1161, [ equalish( 'e_4', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 
% 0.77/1.13    'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.77/1.13  , 1, clause( 517, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_2' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_4' ), :=( Y, 'e_2' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1162, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 35, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 0.77/1.13  , 0, clause( 1161, [ equalish( 'e_4', 'e_2' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 522, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 1162, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.77/1.13     ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1164, [ equalish( X, 'e_2' ), ~( product( 'e_4', X, 'e_1' ) ), 
% 0.77/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T
% 0.77/1.13    , Z ) ) ] )
% 0.77/1.13  , 2, clause( 522, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , 1, substitution( 0, [ :=( X, 'e_4' ), :=( Y, X ), :=( Z, 'e_1' ), :=( T, 
% 0.77/1.13    'e_2' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 526, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product( 
% 0.77/1.13    'e_4', X, 'e_1' ) ) ] )
% 0.77/1.13  , clause( 1164, [ equalish( X, 'e_2' ), ~( product( 'e_4', X, 'e_1' ) ), 
% 0.77/1.13    cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 
% 0.77/1.13    2 ), ==>( 2, 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1165, [ equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_1' ), product( 
% 0.77/1.13    'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 418, [ equalish( X, 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), ~( 
% 0.77/1.13    product( 'e_4', X, 'e_2' ) ) ] )
% 0.77/1.13  , 2, clause( 348, [ product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 
% 0.77/1.13    'e_4', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , 4, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1166, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), equalish( 
% 0.77/1.13    'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 253, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( 
% 0.77/1.13    'e_2', 'e_1', X ) ) ] )
% 0.77/1.13  , 2, clause( 1165, [ equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1'
% 0.77/1.13     ), product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 3, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1168, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), equalish( 
% 0.77/1.13    'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , clause( 1166, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), equalish( 
% 0.77/1.13    'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, 6, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1169, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 
% 0.77/1.13    'e_1', 'e_2' ) ] )
% 0.77/1.13  , clause( 1168, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), equalish( 
% 0.77/1.13    'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_1', 
% 0.77/1.13    'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , 1, 2, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 543, [ product( 'e_4', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_2'
% 0.77/1.13    , 'e_1', 'e_2' ) ] )
% 0.77/1.13  , clause( 1169, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_3' ), product( 
% 0.77/1.13    'e_4', 'e_3', 'e_1' ), product( 'e_4', 'e_1', 'e_1' ), product( 'e_2', 
% 0.77/1.13    'e_1', 'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 2 ), ==>( 2
% 0.77/1.13    , 3 ), ==>( 3, 0 ), ==>( 4, 4 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1171, [ product( 'e_4', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , clause( 26, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 543, [ product( 'e_4', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    equalish( 'e_1', 'e_3' ), product( 'e_4', 'e_3', 'e_1' ), product( 'e_2'
% 0.77/1.13    , 'e_1', 'e_2' ) ] )
% 0.77/1.13  , 2, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 618, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , clause( 1171, [ product( 'e_4', 'e_1', 'e_1' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 ), ==>( 2
% 0.77/1.13    , 2 ), ==>( 3, 3 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1172, [ equalish( 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 
% 0.77/1.13    'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.77/1.13  , 1, clause( 618, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_1', 'e_1' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ), product( 'e_2', 'e_1', 'e_2' ) ] )
% 0.77/1.13  , 3, substitution( 0, [ :=( X, 'e_1' ), :=( Y, 'e_2' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1173, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), equalish( 
% 0.77/1.13    'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , clause( 526, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product( 
% 0.77/1.13    'e_4', X, 'e_1' ) ) ] )
% 0.77/1.13  , 2, clause( 1172, [ equalish( 'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), 
% 0.77/1.13    product( 'e_4', 'e_1', 'e_1' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , 2, substitution( 0, [ :=( X, 'e_1' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1175, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), equalish( 
% 0.77/1.13    'e_1', 'e_2' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 1173, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), equalish( 
% 0.77/1.13    'e_1', 'e_2' ), cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , 0, 3, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1176, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), product( 
% 0.77/1.13    'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 1175, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), equalish( 
% 0.77/1.13    'e_1', 'e_2' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , 1, 2, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 620, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), product( 
% 0.77/1.13    'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 1176, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), product( 
% 0.77/1.13    'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2
% 0.77/1.13    , 2 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1178, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 25, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.77/1.13  , 0, clause( 620, [ cycle( 'e_2', 'e_0' ), equalish( 'e_1', 'e_2' ), 
% 0.77/1.13    product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 621, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ] )
% 0.77/1.13  , clause( 1178, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.77/1.13     ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1179, [ cycle( 'e_2', 'e_0' ), equalish( 'e_3', 'e_2' ), cycle( 
% 0.77/1.13    'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 526, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product( 
% 0.77/1.13    'e_4', X, 'e_1' ) ) ] )
% 0.77/1.13  , 2, clause( 621, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_3', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , 1, substitution( 0, [ :=( X, 'e_3' )] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1181, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 32, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 0.77/1.13  , 0, clause( 1179, [ cycle( 'e_2', 'e_0' ), equalish( 'e_3', 'e_2' ), cycle( 
% 0.77/1.13    'e_2', 'e_0' ) ] )
% 0.77/1.13  , 1, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  factor(
% 0.77/1.13  clause( 1182, [ cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 1181, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, 1, substitution( 0, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 622, [ cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , clause( 1182, [ cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1183, [ ~( product( 'e_2', 'e_1', 'e_4' ) ) ] )
% 0.77/1.13  , clause( 98, [ ~( product( 'e_2', 'e_1', 'e_4' ) ), ~( cycle( 'e_2', 'e_0'
% 0.77/1.13     ) ) ] )
% 0.77/1.13  , 1, clause( 622, [ cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 623, [ ~( product( 'e_2', 'e_1', 'e_4' ) ) ] )
% 0.77/1.13  , clause( 1183, [ ~( product( 'e_2', 'e_1', 'e_4' ) ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1184, [ ~( product( 'e_2', 'e_1', 'e_3' ) ) ] )
% 0.77/1.13  , clause( 97, [ ~( product( 'e_2', 'e_1', 'e_3' ) ), ~( cycle( 'e_2', 'e_0'
% 0.77/1.13     ) ) ] )
% 0.77/1.13  , 1, clause( 622, [ cycle( 'e_2', 'e_0' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 624, [ ~( product( 'e_2', 'e_1', 'e_3' ) ) ] )
% 0.77/1.13  , clause( 1184, [ ~( product( 'e_2', 'e_1', 'e_3' ) ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1185, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.77/1.13  , clause( 623, [ ~( product( 'e_2', 'e_1', 'e_4' ) ) ] )
% 0.77/1.13  , 0, clause( 260, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_2' ), product( 'e_2', 'e_1', 'e_3' ), product( 'e_2', 'e_1', 'e_4' ) ]
% 0.77/1.13     )
% 0.77/1.13  , 3, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1186, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , clause( 624, [ ~( product( 'e_2', 'e_1', 'e_3' ) ) ] )
% 0.77/1.13  , 0, clause( 1185, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1'
% 0.77/1.13    , 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 0.77/1.13  , 2, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 626, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 'e_2'
% 0.77/1.13     ) ] )
% 0.77/1.13  , clause( 1186, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.77/1.13     ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1187, [ equalish( 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_1' ) ]
% 0.77/1.13     )
% 0.77/1.13  , clause( 110, [ equalish( X, Y ), ~( product( Y, X, Y ) ) ] )
% 0.77/1.13  , 1, clause( 626, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1', 
% 0.77/1.13    'e_2' ) ] )
% 0.77/1.13  , 1, substitution( 0, [ :=( X, 'e_1' ), :=( Y, 'e_2' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1188, [ product( 'e_2', 'e_1', 'e_1' ) ] )
% 0.77/1.13  , clause( 25, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 0.77/1.13  , 0, clause( 1187, [ equalish( 'e_1', 'e_2' ), product( 'e_2', 'e_1', 'e_1'
% 0.77/1.13     ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 632, [ product( 'e_2', 'e_1', 'e_1' ) ] )
% 0.77/1.13  , clause( 1188, [ product( 'e_2', 'e_1', 'e_1' ) ] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1189, [ equalish( 'e_2', 'e_1' ) ] )
% 0.77/1.13  , clause( 113, [ equalish( X, Y ), ~( product( X, Y, Y ) ) ] )
% 0.77/1.13  , 1, clause( 632, [ product( 'e_2', 'e_1', 'e_1' ) ] )
% 0.77/1.13  , 0, substitution( 0, [ :=( X, 'e_2' ), :=( Y, 'e_1' )] ), substitution( 1
% 0.77/1.13    , [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  resolution(
% 0.77/1.13  clause( 1190, [] )
% 0.77/1.13  , clause( 28, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 0.77/1.13  , 0, clause( 1189, [ equalish( 'e_2', 'e_1' ) ] )
% 0.77/1.13  , 0, substitution( 0, [] ), substitution( 1, [] )).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  subsumption(
% 0.77/1.13  clause( 636, [] )
% 0.77/1.13  , clause( 1190, [] )
% 0.77/1.13  , substitution( 0, [] ), permutation( 0, [] ) ).
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  end.
% 0.77/1.13  
% 0.77/1.13  % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 0.77/1.13  
% 0.77/1.13  Memory use:
% 0.77/1.13  
% 0.77/1.13  space for terms:        9611
% 0.77/1.13  space for clauses:      28066
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  clauses generated:      1578
% 0.77/1.13  clauses kept:           637
% 0.77/1.13  clauses selected:       466
% 0.77/1.13  clauses deleted:        79
% 0.77/1.13  clauses inuse deleted:  0
% 0.77/1.13  
% 0.77/1.13  subsentry:          4738
% 0.77/1.13  literals s-matched: 2925
% 0.77/1.13  literals matched:   2289
% 0.77/1.13  full subsumption:   383
% 0.77/1.13  
% 0.77/1.13  checksum:           1291393453
% 0.77/1.13  
% 0.77/1.13  
% 0.77/1.13  Bliksem ended
%------------------------------------------------------------------------------