%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP130-3.004 : TPTP v8.1.0. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.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:25 EDT 2022
% Result : Satisfiable 2.16s 2.58s
% Output : Saturation 2.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP130-3.004 : TPTP v8.1.0. Released v1.2.0.
% 0.12/0.13 % Command : bliksem %s
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon Jun 13 19:50:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 2.16/2.58 *** allocated 10000 integers for termspace/termends
% 2.16/2.58 *** allocated 10000 integers for clauses
% 2.16/2.58 *** allocated 10000 integers for justifications
% 2.16/2.58 Bliksem 1.12
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Automatic Strategy Selection
% 2.16/2.58
% 2.16/2.58 Clauses:
% 2.16/2.58 [
% 2.16/2.58 [ next( 'e_0', 'e_1' ) ],
% 2.16/2.58 [ next( 'e_1', 'e_2' ) ],
% 2.16/2.58 [ next( 'e_2', 'e_3' ) ],
% 2.16/2.58 [ next( 'e_3', 'e_4' ) ],
% 2.16/2.58 [ greater( 'e_1', 'e_0' ) ],
% 2.16/2.58 [ greater( 'e_2', 'e_0' ) ],
% 2.16/2.58 [ greater( 'e_3', 'e_0' ) ],
% 2.16/2.58 [ greater( 'e_4', 'e_0' ) ],
% 2.16/2.58 [ greater( 'e_2', 'e_1' ) ],
% 2.16/2.58 [ greater( 'e_3', 'e_1' ) ],
% 2.16/2.58 [ greater( 'e_4', 'e_1' ) ],
% 2.16/2.58 [ greater( 'e_3', 'e_2' ) ],
% 2.16/2.58 [ greater( 'e_4', 'e_2' ) ],
% 2.16/2.58 [ greater( 'e_4', 'e_3' ) ],
% 2.16/2.58 [ ~( cycle( X, Y ) ), ~( cycle( X, Z ) ), equalish( Y, Z ) ],
% 2.16/2.58 [ ~( 'group_element'( X ) ), cycle( X, 'e_0' ), cycle( X, 'e_1' ), cycle(
% 2.16/2.58 X, 'e_2' ), cycle( X, 'e_3' ) ],
% 2.16/2.58 [ cycle( 'e_4', 'e_0' ) ],
% 2.16/2.58 [ ~( cycle( X, Y ) ), ~( cycle( Z, T ) ), ~( next( X, Z ) ), ~( greater(
% 2.16/2.58 Y, 'e_0' ) ), ~( next( T, U ) ), equalish( Y, U ) ],
% 2.16/2.58 [ ~( cycle( X, Y ) ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U ) ), ~(
% 2.16/2.58 next( Z, T ) ), ~( greater( Z, X ) ), ~( greater( Y, U ) ) ],
% 2.16/2.58 [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~( greater( Y, X
% 2.16/2.58 ) ) ],
% 2.16/2.58 [ ~( cycle( X, Y ) ), ~( product( X, 'e_1', Z ) ), ~( greater( Y, 'e_0'
% 2.16/2.58 ) ), ~( next( X, T ) ), equalish( Z, T ) ],
% 2.16/2.58 [ 'group_element'( 'e_1' ) ],
% 2.16/2.58 [ 'group_element'( 'e_2' ) ],
% 2.16/2.58 [ 'group_element'( 'e_3' ) ],
% 2.16/2.58 [ 'group_element'( 'e_4' ) ],
% 2.16/2.58 [ ~( equalish( 'e_1', 'e_2' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_1', 'e_3' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_1', 'e_4' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_2', 'e_1' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_2', 'e_3' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_2', 'e_4' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_3', 'e_1' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_3', 'e_2' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_3', 'e_4' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_4', 'e_1' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_4', 'e_2' ) ) ],
% 2.16/2.58 [ ~( equalish( 'e_4', 'e_3' ) ) ],
% 2.16/2.58 [ ~( 'group_element'( X ) ), ~( 'group_element'( Y ) ), product( X, Y,
% 2.16/2.58 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), product( X, Y,
% 2.16/2.58 'e_4' ) ],
% 2.16/2.58 [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), equalish( Z, T ) ]
% 2.16/2.58 ,
% 2.16/2.58 [ ~( product( X, Y, Z ) ), ~( product( X, T, Z ) ), equalish( Y, T ) ]
% 2.16/2.58 ,
% 2.16/2.58 [ ~( product( X, Y, Z ) ), ~( product( T, Y, Z ) ), equalish( X, T ) ]
% 2.16/2.58 ,
% 2.16/2.58 [ ~( product( X, Y, Z ) ), ~( product( X, Z, T ) ), product( T, Y, X ) ]
% 2.16/2.58
% 2.16/2.58 ] .
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 percentage equality = 0.000000, percentage horn = 0.952381
% 2.16/2.58 This is a near-Horn, non-equality problem
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Options Used:
% 2.16/2.58
% 2.16/2.58 useres = 1
% 2.16/2.58 useparamod = 0
% 2.16/2.58 useeqrefl = 0
% 2.16/2.58 useeqfact = 0
% 2.16/2.58 usefactor = 1
% 2.16/2.58 usesimpsplitting = 0
% 2.16/2.58 usesimpdemod = 0
% 2.16/2.58 usesimpres = 4
% 2.16/2.58
% 2.16/2.58 resimpinuse = 1000
% 2.16/2.58 resimpclauses = 20000
% 2.16/2.58 substype = standard
% 2.16/2.58 backwardsubs = 1
% 2.16/2.58 selectoldest = 5
% 2.16/2.58
% 2.16/2.58 litorderings [0] = split
% 2.16/2.58 litorderings [1] = liftord
% 2.16/2.58
% 2.16/2.58 termordering = none
% 2.16/2.58
% 2.16/2.58 litapriori = 1
% 2.16/2.58 termapriori = 0
% 2.16/2.58 litaposteriori = 0
% 2.16/2.58 termaposteriori = 0
% 2.16/2.58 demodaposteriori = 0
% 2.16/2.58 ordereqreflfact = 0
% 2.16/2.58
% 2.16/2.58 litselect = negative
% 2.16/2.58
% 2.16/2.58 maxweight = 30000
% 2.16/2.58 maxdepth = 30000
% 2.16/2.58 maxlength = 115
% 2.16/2.58 maxnrvars = 195
% 2.16/2.58 excuselevel = 0
% 2.16/2.58 increasemaxweight = 0
% 2.16/2.58
% 2.16/2.58 maxselected = 10000000
% 2.16/2.58 maxnrclauses = 10000000
% 2.16/2.58
% 2.16/2.58 showgenerated = 0
% 2.16/2.58 showkept = 0
% 2.16/2.58 showselected = 0
% 2.16/2.58 showdeleted = 0
% 2.16/2.58 showresimp = 1
% 2.16/2.58 showstatus = 2000
% 2.16/2.58
% 2.16/2.58 prologoutput = 1
% 2.16/2.58 nrgoals = 5000000
% 2.16/2.58 totalproof = 1
% 2.16/2.58
% 2.16/2.58 Symbols occurring in the translation:
% 2.16/2.58
% 2.16/2.58 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.16/2.58 . [1, 2] (w:1, o:27, a:1, s:1, b:0),
% 2.16/2.58 ! [4, 1] (w:1, o:21, a:1, s:1, b:0),
% 2.16/2.58 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.16/2.58 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.16/2.58 'e_0' [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.16/2.58 'e_1' [40, 0] (w:1, o:10, a:1, s:1, b:0),
% 2.16/2.58 next [41, 2] (w:1, o:52, a:1, s:1, b:0),
% 2.16/2.58 'e_2' [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 2.16/2.58 'e_3' [43, 0] (w:1, o:12, a:1, s:1, b:0),
% 2.16/2.58 'e_4' [44, 0] (w:1, o:13, a:1, s:1, b:0),
% 2.16/2.58 greater [45, 2] (w:1, o:53, a:1, s:1, b:0),
% 2.16/2.58 cycle [48, 2] (w:1, o:54, a:1, s:1, b:0),
% 2.16/2.58 equalish [50, 2] (w:1, o:55, a:1, s:1, b:0),
% 2.16/2.58 'group_element' [51, 1] (w:1, o:26, a:1, s:1, b:0),
% 2.16/2.58 product [55, 3] (w:1, o:56, a:1, s:1, b:0).
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Starting Search:
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Intermediate Status:
% 2.16/2.58 Generated: 6519
% 2.16/2.58 Kept: 2006
% 2.16/2.58 Inuse: 788
% 2.16/2.58 Deleted: 216
% 2.16/2.58 Deletedinuse: 50
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Intermediate Status:
% 2.16/2.58 Generated: 21667
% 2.16/2.58 Kept: 4013
% 2.16/2.58 Inuse: 1510
% 2.16/2.58 Deleted: 1210
% 2.16/2.58 Deletedinuse: 439
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Intermediate Status:
% 2.16/2.58 Generated: 41008
% 2.16/2.58 Kept: 6019
% 2.16/2.58 Inuse: 2148
% 2.16/2.58 Deleted: 2134
% 2.16/2.58 Deletedinuse: 949
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Intermediate Status:
% 2.16/2.58 Generated: 72504
% 2.16/2.58 Kept: 8019
% 2.16/2.58 Inuse: 2941
% 2.16/2.58 Deleted: 3137
% 2.16/2.58 Deletedinuse: 1371
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58 Resimplifying inuse:
% 2.16/2.58 Done
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 found a saturation!
% 2.16/2.58 % SZS status Satisfiable
% 2.16/2.58 % SZS output start Saturation
% 2.16/2.58
% 2.16/2.58 clause( 9324, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_2', 'e_2' ), product( 'e_1', 'e_4', 'e_2' ),
% 2.16/2.58 product( 'e_2', X, 'e_3' ), ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9327, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_2', 'e_2' ), equalish( X, 'e_2' ), product(
% 2.16/2.58 'e_1', 'e_4', 'e_2' ), ~( product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9326, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_2', 'e_2' ), equalish( X, 'e_4' ), product(
% 2.16/2.58 'e_1', 'e_4', 'e_2' ), ~( product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9325, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_2', 'e_2' ), equalish( X, 'e_3' ), product(
% 2.16/2.58 'e_1', 'e_4', 'e_2' ), ~( product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9323, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_2', 'e_2' ), product( 'e_1', 'e_4', 'e_2' ),
% 2.16/2.58 product( 'e_3', 'e_4', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9316, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_1', 'e_2' ),
% 2.16/2.58 product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9319, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), equalish( X, 'e_3' ), product(
% 2.16/2.58 'e_3', 'e_1', 'e_2' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9318, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), equalish( X, 'e_1' ), product(
% 2.16/2.58 'e_3', 'e_1', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9317, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), equalish( X, 'e_2' ), product(
% 2.16/2.58 'e_3', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9320, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_1', 'e_2' ),
% 2.16/2.58 ~( product( 'e_2', 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9315, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_1', 'e_2' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8078, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', X, 'e_4' ), product( 'e_3', 'e_1', 'e_3' ), ~(
% 2.16/2.58 product( 'e_4', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9301, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_1', 'e_3' ), product( 'e_4', X, 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9311, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_4', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_4', 'e_2' ), product( 'e_2', X, 'e_3' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9304, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), equalish( X, 'e_4' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 'e_1', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9303, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), equalish( X, 'e_2' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9302, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), equalish( X, 'e_1' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 X, 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9314, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_4', 'e_4',
% 2.16/2.58 'e_1' ), equalish( X, 'e_2' ), product( 'e_1', 'e_4', 'e_2' ), ~( product(
% 2.16/2.58 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9313, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_4', 'e_4',
% 2.16/2.58 'e_1' ), equalish( X, 'e_4' ), product( 'e_1', 'e_4', 'e_2' ), ~( product(
% 2.16/2.58 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9312, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_4', 'e_4',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_1', 'e_4', 'e_2' ), ~( product(
% 2.16/2.58 X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9310, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_4', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_4', 'e_2' ), product( 'e_3', 'e_4', 'e_2' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 9306, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9309, [ product( 'e_3', 'e_1', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_3', 'e_4', 'e_1' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9308, [ product( 'e_3', 'e_1', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_4', 'e_1' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9307, [ product( 'e_3', 'e_1', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_3', 'e_4', 'e_1' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9305, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9292, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9297, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_2' ), product( 'e_3', X, 'e_1' ), ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9164, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_1', 'e_3' ), product( 'e_1', 'e_2', 'e_4' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 9283, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9287, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9295, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9294, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9293, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9300, [ product( 'e_1', 'e_4', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_1', 'e_4', 'e_2' ), ~( product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9299, [ product( 'e_1', 'e_4', 'e_1' ), equalish( X, 'e_4' ),
% 2.16/2.58 product( 'e_1', 'e_4', 'e_2' ), ~( product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9298, [ product( 'e_1', 'e_4', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_1', 'e_4', 'e_2' ), ~( product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9296, [ product( 'e_1', 'e_4', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_2' ), product( 'e_1', 'e_4', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9286, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9285, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_1' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9284, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9289, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_1' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9288, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9221, [ product( 'e_3', 'e_3', 'e_2' ), product( 'e_2', X, 'e_3' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9225, [ product( 'e_3', 'e_3', 'e_2' ), product( 'e_3', X, 'e_1' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9251, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_2', X, 'e_3' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9255, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', X, 'e_1' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9262, [ product( 'e_2', 'e_3', 'e_1' ), product( 'e_2', X, 'e_3' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9267, [ product( 'e_2', 'e_3', 'e_1' ), product( 'e_3', X, 'e_1' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9290, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9273, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_2', X, 'e_3' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9277, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', X, 'e_1' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9224, [ equalish( X, 'e_2' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9223, [ equalish( X, 'e_4' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9222, [ equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9228, [ equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9227, [ equalish( X, 'e_4' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9226, [ equalish( X, 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9231, [ cycle( 'e_2', 'e_0' ), product( 'e_2', X, 'e_3' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9235, [ cycle( 'e_2', 'e_0' ), product( 'e_3', X, 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9282, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9281, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9241, [ cycle( 'e_3', 'e_0' ), product( 'e_2', X, 'e_3' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9245, [ cycle( 'e_3', 'e_0' ), product( 'e_3', X, 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9254, [ equalish( X, 'e_2' ), product( 'e_3', 'e_4', 'e_1' ), ~(
% 2.16/2.58 product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9253, [ equalish( X, 'e_4' ), product( 'e_3', 'e_4', 'e_1' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9252, [ equalish( X, 'e_3' ), product( 'e_3', 'e_4', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9258, [ equalish( X, 'e_3' ), product( 'e_3', 'e_4', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9257, [ equalish( X, 'e_4' ), product( 'e_3', 'e_4', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9256, [ equalish( X, 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9265, [ equalish( X, 'e_2' ), product( 'e_2', 'e_3', 'e_1' ), ~(
% 2.16/2.58 product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9264, [ equalish( X, 'e_4' ), product( 'e_2', 'e_3', 'e_1' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9263, [ equalish( X, 'e_3' ), product( 'e_2', 'e_3', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9270, [ equalish( X, 'e_3' ), product( 'e_2', 'e_3', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9269, [ equalish( X, 'e_4' ), product( 'e_2', 'e_3', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9268, [ equalish( X, 'e_1' ), product( 'e_2', 'e_3', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9276, [ equalish( X, 'e_2' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9275, [ equalish( X, 'e_4' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9274, [ equalish( X, 'e_3' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9280, [ equalish( X, 'e_3' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9279, [ equalish( X, 'e_4' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9278, [ equalish( X, 'e_1' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9272, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9271, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9261, [ product( 'e_2', 'e_3', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9260, [ product( 'e_2', 'e_3', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9259, [ product( 'e_3', 'e_4', 'e_1' ), ~( product( 'e_1', 'e_4',
% 2.16/2.58 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9250, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9249, [ product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9234, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product(
% 2.16/2.58 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9233, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_4' ), ~( product(
% 2.16/2.58 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9232, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product( X
% 2.16/2.58 , 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9238, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product(
% 2.16/2.58 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9237, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_4' ), ~( product(
% 2.16/2.58 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9236, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_1' ), ~( product( X
% 2.16/2.58 , 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9244, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), ~( product(
% 2.16/2.58 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9243, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_4' ), ~( product(
% 2.16/2.58 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9242, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), ~( product( X
% 2.16/2.58 , 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9248, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), ~( product(
% 2.16/2.58 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9247, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_4' ), ~( product(
% 2.16/2.58 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9246, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_1' ), ~( product( X
% 2.16/2.58 , 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9240, [ cycle( 'e_3', 'e_0' ), product( 'e_1', 'e_4', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9239, [ cycle( 'e_3', 'e_0' ), product( 'e_3', 'e_4', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9230, [ cycle( 'e_2', 'e_0' ), product( 'e_1', 'e_4', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9229, [ cycle( 'e_2', 'e_0' ), product( 'e_3', 'e_4', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9220, [ product( 'e_3', 'e_3', 'e_2' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9211, [ product( 'e_3', 'e_3', 'e_2' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9166, [ product( 'e_4', X, 'e_1' ), product( 'e_4', 'e_2', 'e_2' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9182, [ equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9181, [ equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9180, [ equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9176, [ product( 'e_3', 'e_3', 'e_2' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9169, [ equalish( X, 'e_4' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9168, [ equalish( X, 'e_2' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9167, [ equalish( X, 'e_1' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9163, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_1', 'e_2',
% 2.16/2.58 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9149, [ product( 'e_1', X, 'e_4' ), ~( product( 'e_4', X, 'e_3' ) )
% 2.16/2.58 ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9155, [ product( 'e_4', X, 'e_2' ), ~( product( 'e_2', X, 'e_3' ) )
% 2.16/2.58 ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9159, [ product( 'e_2', X, 'e_1' ), ~( product( 'e_1', X, 'e_3' ) )
% 2.16/2.58 ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9152, [ equalish( X, 'e_1' ), ~( product( 'e_4', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9151, [ equalish( X, 'e_3' ), ~( product( 'e_4', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9150, [ equalish( X, 'e_4' ), ~( product( X, 'e_3', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9158, [ equalish( X, 'e_4' ), ~( product( 'e_2', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9157, [ equalish( X, 'e_3' ), ~( product( 'e_2', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9156, [ equalish( X, 'e_2' ), ~( product( X, 'e_3', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9162, [ equalish( X, 'e_2' ), ~( product( 'e_1', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9161, [ equalish( X, 'e_3' ), ~( product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9160, [ equalish( X, 'e_1' ), ~( product( X, 'e_3', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9153, [ product( 'e_1', 'e_3', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9148, [ product( 'e_2', 'e_3', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9147, [ product( 'e_4', 'e_3', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8978, [ product( 'e_2', 'e_3', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8977, [ product( 'e_2', 'e_3', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8976, [ product( 'e_2', 'e_3', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_2' ), ~( product( X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9071, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_3', X, 'e_2' )
% 2.16/2.58 , ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9074, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9073, [ equalish( X, 'e_1' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9072, [ equalish( X, 'e_2' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9070, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9055, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_2', X, 'e_3' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9064, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_3', X, 'e_1' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9058, [ equalish( X, 'e_2' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9057, [ equalish( X, 'e_4' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9056, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9067, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9066, [ equalish( X, 'e_4' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9065, [ equalish( X, 'e_1' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9052, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9051, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9000, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8999, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_2' ), ~( product( 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8998, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_2' ), ~( product( X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8997, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8973, [ product( 'e_2', 'e_3', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8968, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_2' ), ~( product( 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8967, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_2' ), ~( product( 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8966, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_2' ), ~( product( X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8972, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_2' ), ~( product( 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8971, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_2' ), ~( product( 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8970, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_2' ), ~( product( X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8969, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_2' ),
% 2.16/2.58 product( 'e_3', 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8965, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_2' ),
% 2.16/2.58 product( 'e_3', 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8943, [ product( 'e_4', X, 'e_3' ), product( 'e_4', 'e_2', 'e_2' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8946, [ equalish( X, 'e_4' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8945, [ equalish( X, 'e_1' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8944, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8936, [ product( 'e_2', X, 'e_4' ), ~( product( 'e_4', X, 'e_1' ) )
% 2.16/2.58 ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8933, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8939, [ equalish( X, 'e_2' ), ~( product( 'e_4', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8938, [ equalish( X, 'e_1' ), ~( product( 'e_4', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8937, [ equalish( X, 'e_4' ), ~( product( X, 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8932, [ product( 'e_4', 'e_1', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8647, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_3', X, 'e_4' )
% 2.16/2.58 , ~( product( 'e_4', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8650, [ equalish( X, 'e_3' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_4', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8649, [ equalish( X, 'e_2' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( 'e_4', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8648, [ equalish( X, 'e_4' ), product( 'e_4', 'e_2', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8632, [ product( 'e_4', 'e_2', 'e_2' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8554, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8557, [ product( 'e_3', 'e_1', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_2' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8556, [ product( 'e_3', 'e_1', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8555, [ product( 'e_3', 'e_1', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8558, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), ~( product( 'e_2', 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8553, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8476, [ product( 'e_3', 'e_3', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_2' ), ~( product( 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8475, [ product( 'e_3', 'e_3', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_2' ), ~( product( 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8474, [ product( 'e_3', 'e_3', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_2' ), ~( product( X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8467, [ product( 'e_3', 'e_3', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8429, [ cycle( 'e_3', 'e_0' ), product( 'e_3', 'e_1', 'e_1' ),
% 2.16/2.58 product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8432, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_3'
% 2.16/2.58 , 'e_1', 'e_1' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8431, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_1' ), product( 'e_3'
% 2.16/2.58 , 'e_1', 'e_1' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8430, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), product( 'e_3'
% 2.16/2.58 , 'e_1', 'e_1' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8428, [ cycle( 'e_3', 'e_0' ), product( 'e_3', 'e_1', 'e_1' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8382, [ product( 'e_3', 'e_1', 'e_2' ), product( 'e_2', X, 'e_3' )
% 2.16/2.58 , ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8392, [ product( 'e_3', 'e_1', 'e_2' ), product( 'e_3', X, 'e_1' )
% 2.16/2.58 , ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8385, [ equalish( X, 'e_2' ), product( 'e_3', 'e_1', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8384, [ equalish( X, 'e_4' ), product( 'e_3', 'e_1', 'e_2' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8383, [ equalish( X, 'e_3' ), product( 'e_3', 'e_1', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8395, [ equalish( X, 'e_3' ), product( 'e_3', 'e_1', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8394, [ equalish( X, 'e_4' ), product( 'e_3', 'e_1', 'e_2' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8393, [ equalish( X, 'e_1' ), product( 'e_3', 'e_1', 'e_2' ), ~(
% 2.16/2.58 product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8377, [ product( 'e_3', 'e_1', 'e_2' ), product( 'e_1', 'e_4',
% 2.16/2.58 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8376, [ product( 'e_3', 'e_1', 'e_2' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8234, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_2', 'e_1', 'e_2' ), ~( product(
% 2.16/2.58 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8233, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_2', 'e_1', 'e_2' ), ~( product(
% 2.16/2.58 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8232, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_2', 'e_1', 'e_2' ), ~( product(
% 2.16/2.58 X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8226, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), product( 'e_3', 'e_3', 'e_3' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 8081, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), equalish( X, 'e_3' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 'e_4', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8080, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), equalish( X, 'e_2' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 'e_4', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8079, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), equalish( X, 'e_4' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 X, 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8088, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_2', X, 'e_3' ), ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8100, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', X, 'e_1' ), ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8091, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_3', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8090, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_4' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_3', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8089, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( X, 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8103, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_1', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8102, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_4' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_1', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8101, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( X, 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8083, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_1', 'e_4', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8082, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_4', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8065, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8006, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', 'e_1', 'e_3' ), product( 'e_4', 'e_2', 'e_3' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 8068, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8067, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8066, [ product( 'e_2', 'e_1', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8061, [ product( 'e_2', 'e_1', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8057, [ product( 'e_1', X, 'e_2' ), ~( product( 'e_2', X, 'e_4' ) )
% 2.16/2.58 ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8060, [ equalish( X, 'e_1' ), ~( product( 'e_2', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8059, [ equalish( X, 'e_4' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8058, [ equalish( X, 'e_2' ), ~( product( X, 'e_4', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8055, [ product( 'e_2', 'e_4', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8007, [ product( 'e_1', X, 'e_3' ), ~( product( 'e_3', X, 'e_2' ) )
% 2.16/2.58 ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8010, [ equalish( X, 'e_1' ), ~( product( 'e_3', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8009, [ equalish( X, 'e_2' ), ~( product( 'e_3', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8008, [ equalish( X, 'e_3' ), ~( product( X, 'e_2', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8004, [ product( 'e_3', 'e_2', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7086, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_3', 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), product(
% 2.16/2.58 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7088, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_3', 'e_1' ), equalish( X, 'e_1' ), product( 'e_3',
% 2.16/2.58 'e_4', 'e_1' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7087, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_3', 'e_1' ), equalish( X, 'e_2' ), product( 'e_3',
% 2.16/2.58 'e_4', 'e_1' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7085, [ product( 'e_2', 'e_2', 'e_1' ), cycle( 'e_2', 'e_0' ),
% 2.16/2.58 product( 'e_3', 'e_3', 'e_1' ), product( 'e_3', 'e_4', 'e_1' ), product(
% 2.16/2.58 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7080, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), product( 'e_3', X, 'e_2' ), ~(
% 2.16/2.58 product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7083, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~( product(
% 2.16/2.58 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7082, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), equalish( X, 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), ~( product(
% 2.16/2.58 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7081, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), equalish( X, 'e_2' ), product( 'e_3', 'e_3', 'e_2' ), ~( product(
% 2.16/2.58 X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7084, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), ~( product( 'e_2', 'e_3', 'e_1'
% 2.16/2.58 ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7079, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_4',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 7045, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), product( 'e_3', X, 'e_2' ), ~(
% 2.16/2.58 product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7048, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_3', 'e_3', 'e_2' ), ~( product(
% 2.16/2.58 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7047, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_1' ), equalish( X, 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), ~( product(
% 2.16/2.58 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7046, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_1' ), equalish( X, 'e_2' ), product( 'e_3', 'e_3', 'e_2' ), ~( product(
% 2.16/2.58 X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7049, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), ~( product( 'e_2', 'e_3', 'e_1'
% 2.16/2.58 ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7044, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_3', 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 6642, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_4', X, 'e_3' ), ~( product( 'e_3', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6645, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_4' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_3', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6644, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6643, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( X, 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6640, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_3', 'e_1', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6631, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_3', X, 'e_4' ), ~( product( 'e_4', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6636, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_4', X, 'e_1' ), ~( product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6634, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_4', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6633, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_4', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6632, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_4' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( X, 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6639, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_4' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_1', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6638, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6637, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_1' ), ~( product( X, 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6630, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_1', 'e_2', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6629, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_4', 'e_2',
% 2.16/2.58 'e_1' ), product( 'e_4', 'e_2', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6591, [ equalish( X, 'e_2' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_2', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6590, [ equalish( X, 'e_2' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_2', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6589, [ equalish( X, 'e_2' ), product( 'e_2', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( X, 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6588, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_2', 'e_2',
% 2.16/2.58 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5986, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_2', 'e_1', 'e_2' ), ~( product(
% 2.16/2.58 'e_3', 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5985, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_2', 'e_1', 'e_2' ), ~( product(
% 2.16/2.58 'e_3', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5984, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), equalish( X, 'e_3' ), product( 'e_2', 'e_1', 'e_2' ), ~( product(
% 2.16/2.58 X, 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5975, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_3', 'e_3',
% 2.16/2.58 'e_1' ), product( 'e_2', 'e_1', 'e_2' ), product( 'e_3', 'e_3', 'e_3' ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 5884, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5887, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_3' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5886, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_1' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5885, [ product( 'e_2', 'e_2', 'e_1' ), equalish( X, 'e_2' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5871, [ product( 'e_2', 'e_2', 'e_1' ), product( 'e_2', 'e_1',
% 2.16/2.58 'e_2' ), product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4380, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_4', X, 'e_3' ), ~( product( 'e_3', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4382, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_1' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4381, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4376, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4364, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', X, 'e_4' ), ~( product( 'e_4', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4369, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_4', X, 'e_1' ), ~( product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4367, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_4', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4366, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_4', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4365, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_4' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4372, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_4' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_1', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4371, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4370, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_1' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4373, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4363, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_1', 'e_2', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4362, [ cycle( 'e_3', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4327, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), ~( product(
% 2.16/2.58 'e_2', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4326, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), ~( product(
% 2.16/2.58 'e_2', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4325, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_2' ), ~( product( X
% 2.16/2.58 , 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4324, [ cycle( 'e_3', 'e_0' ), product( 'e_2', 'e_2', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3532, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_4', X, 'e_3' ), ~( product( 'e_3', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3535, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_4' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_3', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3534, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_1' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3533, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3529, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_1', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3513, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_3', X, 'e_4' ), ~( product( 'e_4', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3518, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_4', X, 'e_1' ), ~( product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3516, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_4', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3515, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_4', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3514, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_4' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3521, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_4' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_1', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3520, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3519, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_1' ), product( 'e_4'
% 2.16/2.58 , 'e_2', 'e_1' ), ~( product( X, 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3522, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3512, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_1', 'e_2', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3511, [ cycle( 'e_2', 'e_0' ), product( 'e_4', 'e_2', 'e_1' ),
% 2.16/2.58 product( 'e_4', 'e_2', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3507, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product(
% 2.16/2.58 'e_2', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3506, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product(
% 2.16/2.58 'e_2', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3505, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( product( X
% 2.16/2.58 , 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3501, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_2', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3362, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_2' ),
% 2.16/2.58 product( 'e_3', X, 'e_2' ), ~( product( 'e_2', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3364, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_1' ), product( 'e_2'
% 2.16/2.58 , 'e_1', 'e_2' ), ~( product( 'e_2', X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3363, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), product( 'e_2'
% 2.16/2.58 , 'e_1', 'e_2' ), ~( product( X, 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3360, [ cycle( 'e_2', 'e_0' ), product( 'e_2', 'e_1', 'e_2' ),
% 2.16/2.58 product( 'e_2', 'e_1', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2905, [ cycle( 'e_2', 'e_0' ), product( 'e_3', 'e_3', 'e_1' ),
% 2.16/2.58 equalish( X, 'e_3' ), product( 'e_3', 'e_4', 'e_1' ), ~( product( 'e_3',
% 2.16/2.58 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2904, [ cycle( 'e_2', 'e_0' ), product( 'e_3', 'e_3', 'e_1' ),
% 2.16/2.58 equalish( X, 'e_3' ), product( 'e_3', 'e_4', 'e_1' ), ~( product( 'e_3',
% 2.16/2.58 X, 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2903, [ cycle( 'e_2', 'e_0' ), product( 'e_3', 'e_3', 'e_1' ),
% 2.16/2.58 equalish( X, 'e_3' ), product( 'e_3', 'e_4', 'e_1' ), ~( product( X,
% 2.16/2.58 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2889, [ cycle( 'e_2', 'e_0' ), product( 'e_3', 'e_3', 'e_1' ),
% 2.16/2.58 product( 'e_3', 'e_4', 'e_1' ), product( 'e_3', 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2023, [ ~( greater( 'e_1', X ) ), ~( cycle( 'e_2', Z ) ), ~( cycle(
% 2.16/2.58 X, Y ) ), ~( greater( Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2022, [ ~( greater( 'e_1', 'e_1' ) ), ~( cycle( 'e_2', X ) ), ~(
% 2.16/2.58 greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2021, [ ~( greater( 'e_1', 'e_2' ) ), ~( cycle( 'e_2', X ) ), ~(
% 2.16/2.58 greater( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2020, [ ~( cycle( 'e_2', X ) ), ~( cycle( X, 'e_1' ) ), ~( greater(
% 2.16/2.58 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2018, [ ~( cycle( 'e_0', 'e_0' ) ), ~( cycle( X, 'e_1' ) ), ~(
% 2.16/2.58 greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2017, [ ~( cycle( 'e_0', 'e_0' ) ), ~( cycle( X, 'e_2' ) ), ~(
% 2.16/2.58 greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2016, [ ~( cycle( 'e_0', 'e_0' ) ), ~( cycle( X, 'e_3' ) ), ~(
% 2.16/2.58 greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2015, [ ~( cycle( 'e_0', 'e_0' ) ), ~( cycle( X, 'e_4' ) ), ~(
% 2.16/2.58 greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2014, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( X, 'e_1' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2013, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( X, 'e_2' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2012, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( X, 'e_3' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2011, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( X, 'e_4' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2010, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( X, 'e_2' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2009, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( X, 'e_3' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2008, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( X, 'e_4' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2007, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( X, 'e_3' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2006, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( X, 'e_4' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2027, [ ~( cycle( 'e_0', X ) ), equalish( X, 'e_1' ), ~( greater( X
% 2.16/2.58 , 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2028, [ ~( cycle( 'e_0', 'e_0' ) ), ~( greater( 'e_0', 'e_0' ) ) ]
% 2.16/2.58 )
% 2.16/2.58 .
% 2.16/2.58 clause( 2019, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( 'e_0', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2026, [ ~( cycle( 'e_0', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2025, [ ~( cycle( 'e_0', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2024, [ ~( cycle( 'e_0', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1955, [ equalish( X, 'e_1' ), ~( product( 'e_1', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1954, [ equalish( X, 'e_1' ), ~( product( 'e_1', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1953, [ equalish( X, 'e_1' ), ~( product( X, 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1952, [ product( 'e_1', 'e_1', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1943, [ equalish( X, 'e_0' ), ~( cycle( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1942, [ ~( product( 'e_1', 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1941, [ ~( product( 'e_1', 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1940, [ ~( product( 'e_1', 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1939, [ cycle( 'e_1', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 384, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1', 'e_2'
% 2.16/2.58 ), product( 'e_3', 'e_1', 'e_3' ), product( 'e_4', X, 'e_3' ), ~(
% 2.16/2.58 product( 'e_3', X, 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 396, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_2', 'e_2'
% 2.16/2.58 ), product( 'e_1', 'e_2', 'e_3' ), product( 'e_4', X, 'e_1' ), ~(
% 2.16/2.58 product( 'e_1', X, 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 335, [ product( 'e_4', 'e_4', 'e_1' ), product( 'e_4', 'e_4', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_4' ), product( 'e_4', 'e_4', 'e_3' ), ~( product(
% 2.16/2.58 'e_4', 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 334, [ product( 'e_4', 'e_4', 'e_1' ), product( 'e_4', 'e_4', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_4' ), product( 'e_4', 'e_4', 'e_3' ), ~( product(
% 2.16/2.58 'e_4', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 333, [ product( 'e_4', 'e_4', 'e_1' ), product( 'e_4', 'e_4', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_4' ), product( 'e_4', 'e_4', 'e_3' ), ~( product( X,
% 2.16/2.58 'e_4', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 387, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_4' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 'e_3', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 386, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_1' ), product( 'e_3', 'e_1', 'e_3' ), ~( product(
% 2.16/2.58 'e_3', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 385, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_3' ), product( 'e_3', 'e_1', 'e_3' ), ~( product( X,
% 2.16/2.58 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 399, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_2', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_4' ), product( 'e_1', 'e_2', 'e_3' ), ~( product(
% 2.16/2.58 'e_1', 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 398, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_2', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_2' ), product( 'e_1', 'e_2', 'e_3' ), ~( product(
% 2.16/2.58 'e_1', X, 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 397, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_2', 'e_2'
% 2.16/2.58 ), equalish( X, 'e_1' ), product( 'e_1', 'e_2', 'e_3' ), ~( product( X,
% 2.16/2.58 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 271, [ product( 'e_1', 'e_2', 'e_1' ), product( 'e_1', 'e_2', 'e_2'
% 2.16/2.58 ), product( 'e_1', 'e_2', 'e_3' ), product( 'e_1', 'e_2', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 266, [ product( 'e_3', 'e_1', 'e_1' ), product( 'e_3', 'e_1', 'e_2'
% 2.16/2.58 ), product( 'e_3', 'e_1', 'e_3' ), product( 'e_3', 'e_1', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 208, [ ~( cycle( X, 'e_4' ) ), ~( cycle( 'e_2', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_3', 'e_1' ) ), ~( greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 207, [ ~( cycle( X, 'e_3' ) ), ~( cycle( 'e_2', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_3', 'e_1' ) ), ~( greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 206, [ ~( cycle( X, 'e_2' ) ), ~( cycle( 'e_2', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_3', 'e_1' ) ), ~( greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 341, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( X, 'e_4' ) ), ~(
% 2.16/2.58 greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 340, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( X, 'e_3' ) ), ~(
% 2.16/2.58 greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 339, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( X, 'e_2' ) ), ~(
% 2.16/2.58 greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 338, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( X, 'e_1' ) ), ~(
% 2.16/2.58 greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 337, [ equalish( 'e_4', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 157, [ product( 'e_4', 'e_4', 'e_1' ), product( 'e_4', 'e_4', 'e_2'
% 2.16/2.58 ), product( 'e_4', 'e_4', 'e_3' ), product( 'e_4', 'e_4', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 329, [ equalish( 'e_3', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 313, [ equalish( 'e_2', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 300, [ equalish( 'e_1', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 291, [ ~( cycle( 'e_2', 'e_3' ) ), ~( cycle( X, 'e_4' ) ), ~(
% 2.16/2.58 greater( 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 288, [ ~( cycle( 'e_1', 'e_3' ) ), ~( cycle( 'e_0', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 165, [ equalish( X, 'e_4' ), ~( cycle( 'e_1', 'e_3' ) ), ~( cycle(
% 2.16/2.58 'e_0', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 282, [ ~( cycle( 'e_2', 'e_3' ) ), ~( cycle( 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 106, [ product( X, 'e_4', 'e_4' ), product( X, 'e_4', 'e_1' ),
% 2.16/2.58 product( X, 'e_4', 'e_2' ), product( X, 'e_4', 'e_3' ), ~(
% 2.16/2.58 'group_element'( X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 281, [ ~( cycle( 'e_2', 'e_3' ) ), ~( cycle( 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 280, [ ~( cycle( 'e_2', 'e_3' ) ), ~( cycle( 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 164, [ equalish( X, 'e_4' ), ~( cycle( 'e_2', 'e_3' ) ), ~( cycle(
% 2.16/2.58 'e_1', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 105, [ product( X, 'e_3', 'e_4' ), product( X, 'e_3', 'e_1' ),
% 2.16/2.58 product( X, 'e_3', 'e_2' ), product( X, 'e_3', 'e_3' ), ~(
% 2.16/2.58 'group_element'( X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 274, [ ~( cycle( 'e_1', 'e_2' ) ), ~( cycle( 'e_0', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 172, [ equalish( X, 'e_3' ), ~( cycle( 'e_1', 'e_2' ) ), ~( cycle(
% 2.16/2.58 'e_0', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 270, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 104, [ product( X, 'e_2', 'e_4' ), product( X, 'e_2', 'e_1' ),
% 2.16/2.58 product( X, 'e_2', 'e_2' ), product( X, 'e_2', 'e_3' ), ~(
% 2.16/2.58 'group_element'( X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 269, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 268, [ ~( cycle( 'e_2', 'e_2' ) ), ~( cycle( 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 171, [ equalish( X, 'e_3' ), ~( cycle( 'e_2', 'e_2' ) ), ~( cycle(
% 2.16/2.58 'e_1', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 264, [ cycle( 'e_3', 'e_0' ), ~( cycle( 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 103, [ product( X, 'e_1', 'e_4' ), product( X, 'e_1', 'e_1' ),
% 2.16/2.58 product( X, 'e_1', 'e_2' ), product( X, 'e_1', 'e_3' ), ~(
% 2.16/2.58 'group_element'( X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 263, [ ~( cycle( 'e_4', 'e_2' ) ), ~( cycle( 'e_3', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 170, [ equalish( X, 'e_3' ), ~( cycle( 'e_4', 'e_2' ) ), ~( cycle(
% 2.16/2.58 'e_3', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 85, [ ~( cycle( X, 'e_2' ) ), ~( cycle( 'e_2', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_3', X ) ), ~( greater( 'e_2', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 260, [ ~( cycle( 'e_1', 'e_1' ) ), ~( cycle( 'e_0', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 180, [ equalish( X, 'e_2' ), ~( cycle( 'e_1', 'e_1' ) ), ~( cycle(
% 2.16/2.58 'e_0', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 257, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_3' ), ~( product(
% 2.16/2.58 'e_2', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 259, [ cycle( 'e_2', 'e_0' ), equalish( X, 'e_2' ), ~( cycle( 'e_2'
% 2.16/2.58 , X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 84, [ ~( greater( 'e_2', 'e_3' ) ), ~( cycle( 'e_2', 'e_0' ) ), ~(
% 2.16/2.58 cycle( 'e_3', X ) ), ~( greater( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 256, [ cycle( 'e_2', 'e_0' ), cycle( 'e_2', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 254, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 83, [ ~( greater( 'e_2', 'e_2' ) ), ~( cycle( 'e_3', X ) ), ~(
% 2.16/2.58 cycle( 'e_2', 'e_0' ) ), ~( greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 253, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 252, [ ~( cycle( 'e_3', 'e_1' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 179, [ equalish( X, 'e_2' ), ~( cycle( 'e_3', 'e_1' ) ), ~( cycle(
% 2.16/2.58 'e_2', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 249, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 248, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 247, [ ~( cycle( 'e_2', 'e_0' ) ), ~( cycle( 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 187, [ equalish( X, 'e_1' ), ~( cycle( 'e_2', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_1', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 186, [ equalish( X, 'e_1' ), ~( cycle( 'e_3', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_2', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 246, [ ~( cycle( 'e_4', 'e_3' ) ), ~( cycle( 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 245, [ ~( cycle( 'e_4', 'e_3' ) ), ~( cycle( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 197, [ ~( cycle( X, 'e_4' ) ), ~( cycle( 'e_4', 'e_3' ) ), ~(
% 2.16/2.58 greater( 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 243, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 242, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 78, [ ~( cycle( X, 'e_0' ) ), ~( cycle( 'e_0', 'e_0' ) ), ~( cycle(
% 2.16/2.58 'e_1', X ) ), ~( greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 196, [ ~( cycle( X, 'e_4' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~(
% 2.16/2.58 greater( 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 77, [ ~( greater( 'e_0', 'e_1' ) ), ~( cycle( 'e_0', 'e_0' ) ), ~(
% 2.16/2.58 cycle( 'e_1', X ) ), ~( greater( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 239, [ cycle( 'e_2', 'e_0' ), ~( cycle( 'e_3', 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 236, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 235, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 195, [ ~( cycle( X, 'e_3' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~(
% 2.16/2.58 greater( 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 224, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 223, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 75, [ ~( greater( 'e_0', X ) ), ~( cycle( X, Y ) ), ~( cycle( 'e_0'
% 2.16/2.58 , 'e_0' ) ), ~( cycle( 'e_1', Z ) ), ~( greater( Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 194, [ ~( cycle( X, 'e_2' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~(
% 2.16/2.58 greater( 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 211, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_2', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 210, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 209, [ ~( cycle( 'e_3', 'e_0' ) ), ~( cycle( 'e_0', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 193, [ ~( cycle( X, 'e_1' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~(
% 2.16/2.58 greater( 'e_3', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 199, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_4' ), ~( product(
% 2.16/2.58 'e_3', 'e_1', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 201, [ cycle( 'e_3', 'e_0' ), equalish( X, 'e_1' ), ~( cycle( 'e_3'
% 2.16/2.58 , X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 73, [ ~( greater( 'e_2', X ) ), ~( cycle( X, Y ) ), ~( cycle( 'e_2'
% 2.16/2.58 , 'e_0' ) ), ~( cycle( 'e_3', Z ) ), ~( greater( Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 198, [ cycle( 'e_3', 'e_0' ), ~( cycle( 'e_4', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 192, [ cycle( 'e_3', 'e_0' ), cycle( 'e_3', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 190, [ ~( cycle( 'e_3', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 72, [ ~( greater( 'e_3', X ) ), ~( cycle( X, Y ) ), ~( cycle( 'e_3'
% 2.16/2.58 , 'e_0' ) ), ~( cycle( 'e_4', Z ) ), ~( greater( Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 189, [ ~( cycle( 'e_3', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 188, [ ~( cycle( 'e_3', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 185, [ equalish( X, 'e_1' ), ~( cycle( 'e_3', X ) ), ~( greater( X
% 2.16/2.58 , 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 66, [ equalish( Z, 'e_1' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y,
% 2.16/2.58 'e_0' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 181, [ ~( cycle( 'e_4', 'e_1' ) ), ~( cycle( 'e_3', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 178, [ equalish( X, 'e_2' ), ~( cycle( 'e_4', 'e_1' ) ), ~( cycle(
% 2.16/2.58 'e_3', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 65, [ equalish( Z, 'e_2' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y,
% 2.16/2.58 'e_1' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 64, [ equalish( Z, 'e_3' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y,
% 2.16/2.58 'e_2' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 63, [ equalish( Z, 'e_4' ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y,
% 2.16/2.58 'e_3' ) ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 54, [ product( X, X, 'e_4' ), product( X, X, 'e_1' ), product( X, X
% 2.16/2.58 , 'e_2' ), product( X, X, 'e_3' ), ~( 'group_element'( X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 87, [ ~( greater( 'e_3', 'e_4' ) ), ~( cycle( 'e_3', 'e_0' ) ), ~(
% 2.16/2.58 cycle( 'e_4', X ) ), ~( greater( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 86, [ ~( greater( 'e_3', 'e_3' ) ), ~( cycle( 'e_4', X ) ), ~(
% 2.16/2.58 cycle( 'e_3', 'e_0' ) ), ~( greater( 'e_0', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 150, [ ~( product( 'e_0', 'e_1', X ) ), equalish( X, 'e_1' ), ~(
% 2.16/2.58 cycle( 'e_0', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 102, [ ~( product( 'e_0', 'e_1', Y ) ), ~( cycle( 'e_0', X ) ),
% 2.16/2.58 equalish( Y, 'e_1' ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 148, [ ~( product( 'e_1', 'e_1', X ) ), equalish( X, 'e_2' ), ~(
% 2.16/2.58 cycle( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 52, [ ~( greater( X, X ) ), ~( cycle( X, X ) ), ~( cycle( X, 'e_0'
% 2.16/2.58 ) ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 147, [ ~( product( 'e_1', 'e_1', X ) ), equalish( X, 'e_2' ), ~(
% 2.16/2.58 cycle( 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 146, [ ~( product( 'e_1', 'e_1', X ) ), equalish( X, 'e_2' ), ~(
% 2.16/2.58 cycle( 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 145, [ ~( product( 'e_1', 'e_1', X ) ), equalish( X, 'e_2' ), ~(
% 2.16/2.58 cycle( 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 101, [ ~( product( 'e_1', 'e_1', Y ) ), ~( cycle( 'e_1', X ) ),
% 2.16/2.58 equalish( Y, 'e_2' ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 50, [ ~( greater( X, X ) ), ~( greater( 'e_0', 'e_0' ) ), ~( cycle(
% 2.16/2.58 X, 'e_0' ) ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 143, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~(
% 2.16/2.58 cycle( 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 142, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~(
% 2.16/2.58 cycle( 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 141, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~(
% 2.16/2.58 cycle( 'e_2', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 140, [ ~( product( 'e_2', 'e_1', X ) ), equalish( X, 'e_3' ), ~(
% 2.16/2.58 cycle( 'e_2', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 49, [ ~( greater( X, 'e_0' ) ), ~( cycle( 'e_0', X ) ), ~( cycle( X
% 2.16/2.58 , 'e_0' ) ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 100, [ ~( product( 'e_2', 'e_1', Y ) ), ~( cycle( 'e_2', X ) ),
% 2.16/2.58 equalish( Y, 'e_3' ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 48, [ ~( greater( Z, X ) ), ~( greater( Y, 'e_0' ) ), ~( cycle( Z,
% 2.16/2.58 'e_0' ) ), ~( cycle( X, Y ) ), ~( next( Z, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 135, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 134, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 47, [ ~( greater( Z, X ) ), ~( greater( Y, Y ) ), ~( cycle( Z,
% 2.16/2.58 'e_0' ) ), ~( cycle( X, Y ) ), ~( next( Z, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 133, [ ~( cycle( 'e_2', 'e_1' ) ), ~( cycle( 'e_1', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 123, [ equalish( X, 'e_2' ), ~( cycle( 'e_2', 'e_1' ) ), ~( cycle(
% 2.16/2.58 'e_1', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 46, [ ~( greater( X, X ) ), ~( greater( 'e_0', Y ) ), ~( cycle( Z,
% 2.16/2.58 Y ) ), ~( cycle( X, 'e_0' ) ), ~( next( X, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 129, [ cycle( 'e_3', 'e_0' ), ~( cycle( 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 45, [ ~( greater( Y, X ) ), ~( cycle( Y, 'e_0' ) ), ~( cycle( Z, X
% 2.16/2.58 ) ), ~( cycle( X, Y ) ), ~( next( Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 125, [ ~( cycle( 'e_4', 'e_3' ) ), ~( cycle( 'e_3', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 121, [ equalish( X, 'e_4' ), ~( cycle( 'e_4', 'e_3' ) ), ~( cycle(
% 2.16/2.58 'e_3', X ) ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 44, [ equalish( Z, Y ), ~( greater( Z, 'e_0' ) ), ~( cycle( Y, X )
% 2.16/2.58 ), ~( cycle( X, Z ) ), ~( next( X, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 116, [ ~( product( 'e_3', 'e_1', X ) ), equalish( X, 'e_4' ), ~(
% 2.16/2.58 cycle( 'e_3', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 43, [ ~( next( X, X ) ), ~( greater( Y, 'e_0' ) ), ~( cycle( X, Y )
% 2.16/2.58 ), equalish( Y, Z ), ~( next( Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 99, [ ~( product( 'e_3', 'e_1', Y ) ), ~( cycle( 'e_3', X ) ),
% 2.16/2.58 equalish( Y, 'e_4' ), ~( greater( X, 'e_0' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 67, [ ~( greater( 'e_0', 'e_0' ) ), ~( cycle( X, 'e_0' ) ),
% 2.16/2.58 equalish( 'e_0', 'e_1' ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 41, [ ~( product( X, Y, Z ) ), product( T, Y, X ), ~( product( X, Z
% 2.16/2.58 , T ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 40, [ equalish( X, T ), ~( product( X, Y, Z ) ), ~( product( T, Y,
% 2.16/2.58 Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 109, [ ~( cycle( X, 'e_1' ) ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 39, [ equalish( Y, T ), ~( product( X, Y, Z ) ), ~( product( X, T,
% 2.16/2.58 Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 108, [ ~( cycle( X, 'e_2' ) ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 107, [ ~( cycle( X, 'e_3' ) ), ~( next( X, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 38, [ equalish( Z, T ), ~( product( X, Y, Z ) ), ~( product( X, Y,
% 2.16/2.58 T ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 98, [ ~( product( 'e_3', 'e_1', 'e_4' ) ), ~( cycle( 'e_3', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 97, [ ~( product( 'e_2', 'e_1', 'e_4' ) ), ~( cycle( 'e_2', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 96, [ ~( product( 'e_2', 'e_1', 'e_3' ) ), ~( cycle( 'e_2', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 37, [ ~( 'group_element'( X ) ), product( X, Y, 'e_4' ), product( X
% 2.16/2.58 , Y, 'e_1' ), product( X, Y, 'e_2' ), product( X, Y, 'e_3' ), ~(
% 2.16/2.58 'group_element'( Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 92, [ ~( product( 'e_0', 'e_1', 'e_4' ) ), ~( cycle( 'e_0', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 91, [ ~( product( 'e_0', 'e_1', 'e_3' ) ), ~( cycle( 'e_0', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 20, [ ~( cycle( X, Y ) ), ~( greater( Y, 'e_0' ) ), ~( product( X,
% 2.16/2.58 'e_1', Z ) ), equalish( Z, T ), ~( next( X, T ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 90, [ ~( product( 'e_0', 'e_1', 'e_2' ) ), ~( cycle( 'e_0', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 89, [ ~( product( 'e_0', 'e_1', 'e_1' ) ), ~( cycle( 'e_0', 'e_0' )
% 2.16/2.58 ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 58, [ product( Y, Y, X ), ~( product( X, Y, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 55, [ equalish( X, X ), ~( product( Y, Z, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 19, [ ~( cycle( X, 'e_0' ) ), ~( product( X, 'e_1', Y ) ), ~(
% 2.16/2.58 greater( Y, X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 56, [ equalish( X, X ), ~( product( Y, X, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 57, [ equalish( X, X ), ~( product( X, Y, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 59, [ equalish( X, 'e_0' ), ~( cycle( 'e_4', X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 71, [ equalish( 'e_0', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 18, [ ~( cycle( X, Y ) ), ~( greater( Z, X ) ), ~( greater( Y, U )
% 2.16/2.58 ), ~( cycle( Z, 'e_0' ) ), ~( cycle( T, U ) ), ~( next( Z, T ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 42, [ equalish( Y, Y ), ~( cycle( X, Y ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 25, [ ~( equalish( 'e_1', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 26, [ ~( equalish( 'e_1', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 27, [ ~( equalish( 'e_1', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 17, [ ~( next( X, Z ) ), ~( greater( Y, 'e_0' ) ), equalish( Y, U )
% 2.16/2.58 , ~( cycle( Z, T ) ), ~( cycle( X, Y ) ), ~( next( T, U ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 28, [ ~( equalish( 'e_2', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 29, [ ~( equalish( 'e_2', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 30, [ ~( equalish( 'e_2', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 31, [ ~( equalish( 'e_3', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 15, [ cycle( X, 'e_3' ), cycle( X, 'e_0' ), cycle( X, 'e_1' ),
% 2.16/2.58 cycle( X, 'e_2' ), ~( 'group_element'( X ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 32, [ ~( equalish( 'e_3', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 33, [ ~( equalish( 'e_3', 'e_4' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 34, [ ~( equalish( 'e_4', 'e_1' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 35, [ ~( equalish( 'e_4', 'e_2' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 14, [ ~( cycle( X, Y ) ), equalish( Y, Z ), ~( cycle( X, Z ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 36, [ ~( equalish( 'e_4', 'e_3' ) ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 3, [ next( 'e_3', 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 4, [ greater( 'e_1', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 5, [ greater( 'e_2', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 2, [ next( 'e_2', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 6, [ greater( 'e_3', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 7, [ greater( 'e_4', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 8, [ greater( 'e_2', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 9, [ greater( 'e_3', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 1, [ next( 'e_1', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 10, [ greater( 'e_4', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 11, [ greater( 'e_3', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 12, [ greater( 'e_4', 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 13, [ greater( 'e_4', 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 0, [ next( 'e_0', 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 16, [ cycle( 'e_4', 'e_0' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 21, [ 'group_element'( 'e_1' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 22, [ 'group_element'( 'e_2' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 23, [ 'group_element'( 'e_3' ) ] )
% 2.16/2.58 .
% 2.16/2.58 clause( 24, [ 'group_element'( 'e_4' ) ] )
% 2.16/2.58 .
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 % SZS output end Saturation
% 2.16/2.58 end of saturation!
% 2.16/2.58
% 2.16/2.58 Memory use:
% 2.16/2.58
% 2.16/2.58 space for terms: 225532
% 2.16/2.58 space for clauses: 356641
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 clauses generated: 97637
% 2.16/2.58 clauses kept: 9328
% 2.16/2.58 clauses selected: 3518
% 2.16/2.58 clauses deleted: 8779
% 2.16/2.58 clauses inuse deleted: 2969
% 2.16/2.58
% 2.16/2.58 subsentry: 1061288
% 2.16/2.58 literals s-matched: 162862
% 2.16/2.58 literals matched: 133690
% 2.16/2.58 full subsumption: 10536
% 2.16/2.58
% 2.16/2.58 checksum: 1044436848
% 2.16/2.58
% 2.16/2.58
% 2.16/2.58 Bliksem ended
%------------------------------------------------------------------------------