%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP195-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n006.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:36:04 EDT 2022
% Result : Unsatisfiable 143.51s 143.91s
% Output : Refutation 143.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRP195-1 : TPTP v8.1.0. Released v2.2.0.
% 0.12/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n006.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 10:08:11 EDT 2022
% 0.12/0.33 % CPUTime :
% 143.51/143.91 *** allocated 10000 integers for termspace/termends
% 143.51/143.91 *** allocated 10000 integers for clauses
% 143.51/143.91 *** allocated 10000 integers for justifications
% 143.51/143.91 Bliksem 1.12
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 Automatic Strategy Selection
% 143.51/143.91
% 143.51/143.91 Clauses:
% 143.51/143.91 [
% 143.51/143.91 [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply( Y, Z ) ) )
% 143.51/143.91 ],
% 143.51/143.91 [ =( multiply( X, multiply( Y, Y ) ), multiply( Y, multiply( Y, X ) ) )
% 143.51/143.91 ],
% 143.51/143.91 [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b, multiply( a
% 143.51/143.91 , multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a, multiply( a,
% 143.51/143.91 multiply( a, multiply( a, multiply( b, multiply( b, multiply( b, b ) ) )
% 143.51/143.91 ) ) ) ) ) ) ]
% 143.51/143.91 ] .
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 percentage equality = 1.000000, percentage horn = 1.000000
% 143.51/143.91 This is a pure equality problem
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 Options Used:
% 143.51/143.91
% 143.51/143.91 useres = 1
% 143.51/143.91 useparamod = 1
% 143.51/143.91 useeqrefl = 1
% 143.51/143.91 useeqfact = 1
% 143.51/143.91 usefactor = 1
% 143.51/143.91 usesimpsplitting = 0
% 143.51/143.91 usesimpdemod = 5
% 143.51/143.91 usesimpres = 3
% 143.51/143.91
% 143.51/143.91 resimpinuse = 1000
% 143.51/143.91 resimpclauses = 20000
% 143.51/143.91 substype = eqrewr
% 143.51/143.91 backwardsubs = 1
% 143.51/143.91 selectoldest = 5
% 143.51/143.91
% 143.51/143.91 litorderings [0] = split
% 143.51/143.91 litorderings [1] = extend the termordering, first sorting on arguments
% 143.51/143.91
% 143.51/143.91 termordering = kbo
% 143.51/143.91
% 143.51/143.91 litapriori = 0
% 143.51/143.91 termapriori = 1
% 143.51/143.91 litaposteriori = 0
% 143.51/143.91 termaposteriori = 0
% 143.51/143.91 demodaposteriori = 0
% 143.51/143.91 ordereqreflfact = 0
% 143.51/143.91
% 143.51/143.91 litselect = negord
% 143.51/143.91
% 143.51/143.91 maxweight = 15
% 143.51/143.91 maxdepth = 30000
% 143.51/143.91 maxlength = 115
% 143.51/143.91 maxnrvars = 195
% 143.51/143.91 excuselevel = 1
% 143.51/143.91 increasemaxweight = 1
% 143.51/143.91
% 143.51/143.91 maxselected = 10000000
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91
% 143.51/143.91 showgenerated = 0
% 143.51/143.91 showkept = 0
% 143.51/143.91 showselected = 0
% 143.51/143.91 showdeleted = 0
% 143.51/143.91 showresimp = 1
% 143.51/143.91 showstatus = 2000
% 143.51/143.91
% 143.51/143.91 prologoutput = 1
% 143.51/143.91 nrgoals = 5000000
% 143.51/143.91 totalproof = 1
% 143.51/143.91
% 143.51/143.91 Symbols occurring in the translation:
% 143.51/143.91
% 143.51/143.91 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 143.51/143.91 . [1, 2] (w:1, o:19, a:1, s:1, b:0),
% 143.51/143.91 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 143.51/143.91 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 143.51/143.91 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 143.51/143.91 multiply [41, 2] (w:1, o:44, a:1, s:1, b:0),
% 143.51/143.91 a [43, 0] (w:1, o:12, a:1, s:1, b:0),
% 143.51/143.91 b [44, 0] (w:1, o:13, a:1, s:1, b:0).
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 15
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 383
% 143.51/143.91 Kept: 8
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 16
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 16
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 383
% 143.51/143.91 Kept: 8
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 17
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 17
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 383
% 143.51/143.91 Kept: 8
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 18
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 18
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 383
% 143.51/143.91 Kept: 8
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 19
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 19
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 8812
% 143.51/143.91 Kept: 34
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 20
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 20
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 8812
% 143.51/143.91 Kept: 34
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 21
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 21
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 8812
% 143.51/143.91 Kept: 34
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 22
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 22
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 8812
% 143.51/143.91 Kept: 34
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 23
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 23
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 261958
% 143.51/143.91 Kept: 161
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 24
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 24
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 261958
% 143.51/143.91 Kept: 161
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 25
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 25
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 261958
% 143.51/143.91 Kept: 161
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 26
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91 Failed to find proof!
% 143.51/143.91 maxweight = 26
% 143.51/143.91 maxnrclauses = 10000000
% 143.51/143.91 Generated: 261958
% 143.51/143.91 Kept: 161
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 The strategy used was not complete!
% 143.51/143.91
% 143.51/143.91 Increased maxweight to 27
% 143.51/143.91
% 143.51/143.91 Starting Search:
% 143.51/143.91
% 143.51/143.91 Resimplifying inuse:
% 143.51/143.91 Done
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 Bliksems!, er is een bewijs:
% 143.51/143.91 % SZS status Unsatisfiable
% 143.51/143.91 % SZS output start Refutation
% 143.51/143.91
% 143.51/143.91 clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 143.51/143.91 , Z ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 1, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y, Y )
% 143.51/143.91 , X ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 2, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.91 multiply( multiply( a, a ), a ), a ), b ), b ), b ), b ), multiply(
% 143.51/143.91 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.91 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 5, [ =( multiply( multiply( multiply( multiply( Y, Z ), Y ), Z ), X
% 143.51/143.91 ), multiply( multiply( multiply( multiply( X, Y ), Z ), Y ), Z ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 6, [ =( multiply( multiply( multiply( Y, Z ), X ), X ), multiply(
% 143.51/143.91 multiply( multiply( X, X ), Y ), Z ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 7, [ =( multiply( multiply( multiply( Z, Y ), Y ), X ), multiply(
% 143.51/143.91 multiply( multiply( Z, X ), Y ), Y ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 26, [ =( multiply( multiply( multiply( multiply( X, Z ), Y ), Y ),
% 143.51/143.91 Z ), multiply( multiply( multiply( multiply( Z, Z ), X ), Y ), Y ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 440, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.91 multiply( Y, Z ), Y ), Z ), X ), Z ), Y ), multiply( multiply( multiply(
% 143.51/143.91 multiply( multiply( multiply( Y, Y ), X ), Y ), Z ), Z ), Z ) ) ] )
% 143.51/143.91 .
% 143.51/143.91 clause( 1164, [] )
% 143.51/143.91 .
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 % SZS output end Refutation
% 143.51/143.91 found a proof!
% 143.51/143.91
% 143.51/143.91 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 143.51/143.91
% 143.51/143.91 initialclauses(
% 143.51/143.91 [ clause( 1166, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 143.51/143.91 Y, Z ) ) ) ] )
% 143.51/143.91 , clause( 1167, [ =( multiply( X, multiply( Y, Y ) ), multiply( Y, multiply(
% 143.51/143.91 Y, X ) ) ) ] )
% 143.51/143.91 , clause( 1168, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b
% 143.51/143.91 , multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.91 multiply( a, multiply( a, multiply( a, multiply( b, multiply( b, multiply(
% 143.51/143.91 b, b ) ) ) ) ) ) ) ) ) ] )
% 143.51/143.91 ] ).
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 eqswap(
% 143.51/143.91 clause( 1169, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X,
% 143.51/143.91 Y ), Z ) ) ] )
% 143.51/143.91 , clause( 1166, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 143.51/143.91 Y, Z ) ) ) ] )
% 143.51/143.91 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 subsumption(
% 143.51/143.91 clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 143.51/143.91 , Z ) ) ] )
% 143.51/143.91 , clause( 1169, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X
% 143.51/143.91 , Y ), Z ) ) ] )
% 143.51/143.91 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 143.51/143.91 permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.91
% 143.51/143.91
% 143.51/143.91 paramod(
% 143.51/143.91 clause( 1179, [ =( multiply( X, multiply( Y, Y ) ), multiply( multiply( Y,
% 143.51/143.91 Y ), X ) ) ] )
% 143.51/143.91 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.91 ), Z ) ) ] )
% 143.51/143.91 , 0, clause( 1167, [ =( multiply( X, multiply( Y, Y ) ), multiply( Y,
% 143.51/143.92 multiply( Y, X ) ) ) ] )
% 143.51/143.92 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, Y ), :=( Z, X )] ),
% 143.51/143.92 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1181, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y,
% 143.51/143.92 Y ), X ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1179, [ =( multiply( X, multiply( Y, Y ) ), multiply( multiply(
% 143.51/143.92 Y, Y ), X ) ) ] )
% 143.51/143.92 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y )] ),
% 143.51/143.92 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 1, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y, Y )
% 143.51/143.92 , X ) ) ] )
% 143.51/143.92 , clause( 1181, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y
% 143.51/143.92 , Y ), X ) ) ] )
% 143.51/143.92 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 143.51/143.92 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1245, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( b, multiply( multiply( b
% 143.51/143.92 , b ), b ) ) ) ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1168, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( b, multiply( b, multiply(
% 143.51/143.92 b, b ) ) ) ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 27, substitution( 0, [ :=( X, b ), :=( Y, b ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1352, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( multiply( b, multiply( b
% 143.51/143.92 , b ) ), b ) ) ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1245, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( b, multiply( multiply( b
% 143.51/143.92 , b ), b ) ) ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 25, substitution( 0, [ :=( X, b ), :=( Y, multiply( b, b ) ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1456, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( multiply( multiply( b, b
% 143.51/143.92 ), b ), b ) ) ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1352, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( multiply( b, multiply( b
% 143.51/143.92 , b ) ), b ) ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 26, substitution( 0, [ :=( X, b ), :=( Y, b ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1556, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( multiply( a, multiply( multiply( b, b
% 143.51/143.92 ), b ) ), b ) ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1456, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( a, multiply( multiply( multiply( b, b
% 143.51/143.92 ), b ), b ) ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 23, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( b, b ),
% 143.51/143.92 b ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1654, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( multiply( multiply( a, multiply( b, b
% 143.51/143.92 ) ), b ), b ) ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1556, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( multiply( a, multiply( multiply( b, b
% 143.51/143.92 ), b ) ), b ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 24, substitution( 0, [ :=( X, a ), :=( Y, multiply( b, b ) ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1750, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( multiply( multiply( multiply( a, b )
% 143.51/143.92 , b ), b ), b ) ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1654, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( multiply( multiply( a, multiply( b, b
% 143.51/143.92 ) ), b ), b ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 25, substitution( 0, [ :=( X, a ), :=( Y, b ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1842, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( a, multiply( multiply( multiply( a, b )
% 143.51/143.92 , b ), b ) ), b ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1750, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( a, multiply( multiply( multiply( multiply( a, b )
% 143.51/143.92 , b ), b ), b ) ) ) ) ) ) ] )
% 143.51/143.92 , 0, 21, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 a, b ), b ), b ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 1932, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( multiply( a, multiply( multiply( a, b )
% 143.51/143.92 , b ) ), b ), b ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1842, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( a, multiply( multiply( multiply( a, b )
% 143.51/143.92 , b ), b ) ), b ) ) ) ) ) ] )
% 143.51/143.92 , 0, 22, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( a, b ),
% 143.51/143.92 b ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2020, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( multiply( multiply( a, multiply( a, b )
% 143.51/143.92 ), b ), b ), b ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 1932, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( multiply( a, multiply( multiply( a, b )
% 143.51/143.92 , b ) ), b ), b ) ) ) ) ) ] )
% 143.51/143.92 , 0, 23, substitution( 0, [ :=( X, a ), :=( Y, multiply( a, b ) ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2106, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( multiply( multiply( multiply( a, a ), b
% 143.51/143.92 ), b ), b ), b ) ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2020, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( multiply( multiply( a, multiply( a, b )
% 143.51/143.92 ), b ), b ), b ) ) ) ) ) ] )
% 143.51/143.92 , 0, 24, substitution( 0, [ :=( X, a ), :=( Y, a ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2114, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( a, multiply( multiply( multiply( multiply( a, a ), b
% 143.51/143.92 ), b ), b ) ), b ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2106, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( a, multiply( multiply( multiply( multiply( multiply( a, a ), b
% 143.51/143.92 ), b ), b ), b ) ) ) ) ) ] )
% 143.51/143.92 , 0, 19, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 multiply( a, a ), b ), b ), b ) ), :=( Z, b )] ), substitution( 1, [] )
% 143.51/143.92 ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2122, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( a, multiply( multiply( multiply( a, a ), b
% 143.51/143.92 ), b ) ), b ), b ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2114, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( a, multiply( multiply( multiply( multiply( a, a ), b
% 143.51/143.92 ), b ), b ) ), b ) ) ) ) ] )
% 143.51/143.92 , 0, 20, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 a, a ), b ), b ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2130, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( a, multiply( multiply( a, a ), b
% 143.51/143.92 ) ), b ), b ), b ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2122, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( a, multiply( multiply( multiply( a, a ), b
% 143.51/143.92 ), b ) ), b ), b ) ) ) ) ] )
% 143.51/143.92 , 0, 21, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( a, a ),
% 143.51/143.92 b ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2138, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( a, multiply( a, a ) ),
% 143.51/143.92 b ), b ), b ), b ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2130, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( a, multiply( multiply( a, a ), b
% 143.51/143.92 ) ), b ), b ), b ) ) ) ) ] )
% 143.51/143.92 , 0, 22, substitution( 0, [ :=( X, a ), :=( Y, multiply( a, a ) ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 2146, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 b ), b ), b ), b ) ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2138, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( a, multiply( a, a ) ),
% 143.51/143.92 b ), b ), b ), b ) ) ) ) ] )
% 143.51/143.92 , 0, 23, substitution( 0, [ :=( X, a ), :=( Y, a ), :=( Z, a )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41653, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( a, multiply( multiply( multiply( multiply( multiply( a, a ), a
% 143.51/143.92 ), b ), b ), b ) ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 2146, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 b ), b ), b ), b ) ) ) ) ] )
% 143.51/143.92 , 0, 17, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, a ), a ), b ), b ), b ) ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41660, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( a, multiply( multiply( multiply( multiply( a, a ), a
% 143.51/143.92 ), b ), b ) ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41653, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( a, multiply( multiply( multiply( multiply( multiply( a, a ), a
% 143.51/143.92 ), b ), b ), b ) ), b ) ) ) ] )
% 143.51/143.92 , 0, 18, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 multiply( a, a ), a ), b ), b ) ), :=( Z, b )] ), substitution( 1, [] )
% 143.51/143.92 ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41667, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( a, multiply( multiply( multiply( a, a ), a
% 143.51/143.92 ), b ) ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41660, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( a, multiply( multiply( multiply( multiply( a, a ), a
% 143.51/143.92 ), b ), b ) ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 19, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 a, a ), a ), b ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41674, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( a, multiply( multiply( a, a ), a
% 143.51/143.92 ) ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41667, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( a, multiply( multiply( multiply( a, a ), a
% 143.51/143.92 ), b ) ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 20, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( a, a ),
% 143.51/143.92 a ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41681, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( a, multiply( a, a ) ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41674, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( a, multiply( multiply( a, a ), a
% 143.51/143.92 ) ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 21, substitution( 0, [ :=( X, a ), :=( Y, multiply( a, a ) ), :=( Z, a
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41688, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41681, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( a, multiply( a, a ) ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 22, substitution( 0, [ :=( X, a ), :=( Y, a ), :=( Z, a )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41694, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( a, multiply( multiply( b, a ), b ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41688, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( b, multiply( a, b ) ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 12, substitution( 0, [ :=( X, b ), :=( Y, a ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41699, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( multiply( a, multiply( b, a ) ), b ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41694, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( a, multiply( multiply( b, a ), b ) ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 10, substitution( 0, [ :=( X, a ), :=( Y, multiply( b, a ) ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41704, [ ~( =( multiply( a, multiply( b, multiply( a, multiply( b,
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41699, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( multiply( a, multiply( b, a ) ), b ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 11, substitution( 0, [ :=( X, a ), :=( Y, b ), :=( Z, a )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41708, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 multiply( b, multiply( multiply( a, b ), a ) ), b ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41704, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 b, multiply( multiply( multiply( a, b ), a ), b ) ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 8, substitution( 0, [ :=( X, b ), :=( Y, multiply( multiply( a, b ), a
% 143.51/143.92 ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 41709, [ ~( =( multiply( multiply( a, b ), multiply( a, multiply(
% 143.51/143.92 multiply( b, multiply( multiply( a, b ), a ) ), b ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41708, [ ~( =( multiply( a, multiply( b, multiply( a, multiply(
% 143.51/143.92 multiply( b, multiply( multiply( a, b ), a ) ), b ) ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 2, substitution( 0, [ :=( X, a ), :=( Y, b ), :=( Z, multiply( a,
% 143.51/143.92 multiply( multiply( b, multiply( multiply( a, b ), a ) ), b ) ) )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42767, [ ~( =( multiply( multiply( a, b ), multiply( a, multiply(
% 143.51/143.92 multiply( multiply( b, multiply( a, b ) ), a ), b ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 41709, [ ~( =( multiply( multiply( a, b ), multiply( a,
% 143.51/143.92 multiply( multiply( b, multiply( multiply( a, b ), a ) ), b ) ) ),
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( multiply( a,
% 143.51/143.92 a ), a ), a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 9, substitution( 0, [ :=( X, b ), :=( Y, multiply( a, b ) ), :=( Z, a
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42770, [ ~( =( multiply( multiply( a, b ), multiply( a, multiply(
% 143.51/143.92 multiply( multiply( multiply( b, a ), b ), a ), b ) ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42767, [ ~( =( multiply( multiply( a, b ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( b, multiply( a, b ) ), a ), b ) ) ),
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( multiply( a,
% 143.51/143.92 a ), a ), a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 10, substitution( 0, [ :=( X, b ), :=( Y, a ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42772, [ ~( =( multiply( multiply( a, b ), multiply( multiply( a,
% 143.51/143.92 multiply( multiply( multiply( b, a ), b ), a ) ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42770, [ ~( =( multiply( multiply( a, b ), multiply( a,
% 143.51/143.92 multiply( multiply( multiply( multiply( b, a ), b ), a ), b ) ) ),
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( multiply( a,
% 143.51/143.92 a ), a ), a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 6, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( multiply(
% 143.51/143.92 b, a ), b ), a ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42774, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 multiply( a, multiply( multiply( b, a ), b ) ), a ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42772, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 a, multiply( multiply( multiply( b, a ), b ), a ) ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 7, substitution( 0, [ :=( X, a ), :=( Y, multiply( multiply( b, a ), b
% 143.51/143.92 ) ), :=( Z, a )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42776, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 multiply( multiply( a, multiply( b, a ) ), b ), a ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42774, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 multiply( a, multiply( multiply( b, a ), b ) ), a ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 8, substitution( 0, [ :=( X, a ), :=( Y, multiply( b, a ) ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42778, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ), a ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42776, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 multiply( multiply( a, multiply( b, a ) ), b ), a ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 9, substitution( 0, [ :=( X, a ), :=( Y, b ), :=( Z, a )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42779, [ ~( =( multiply( multiply( multiply( a, b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ), a ) ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42778, [ ~( =( multiply( multiply( a, b ), multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ), a ), b ) ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 2, substitution( 0, [ :=( X, multiply( a, b ) ), :=( Y, multiply(
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ), a ) ), :=( Z, b )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42780, [ ~( =( multiply( multiply( multiply( multiply( a, b ),
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ) ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42779, [ ~( =( multiply( multiply( multiply( a, b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ), a ) ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 3, substitution( 0, [ :=( X, multiply( a, b ) ), :=( Y, multiply(
% 143.51/143.92 multiply( multiply( a, b ), a ), b ) ), :=( Z, a )] ), substitution( 1, [] )
% 143.51/143.92 ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42781, [ ~( =( multiply( multiply( multiply( multiply( multiply( a
% 143.51/143.92 , b ), multiply( multiply( a, b ), a ) ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42780, [ ~( =( multiply( multiply( multiply( multiply( a, b )
% 143.51/143.92 , multiply( multiply( multiply( a, b ), a ), b ) ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 4, substitution( 0, [ :=( X, multiply( a, b ) ), :=( Y, multiply(
% 143.51/143.92 multiply( a, b ), a ) ), :=( Z, b )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42782, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( a, b ), multiply( a, b ) ), a ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42781, [ ~( =( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( a, b ), multiply( multiply( a, b ), a ) ), b ), a ), b ),
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( multiply( a,
% 143.51/143.92 a ), a ), a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 5, substitution( 0, [ :=( X, multiply( a, b ) ), :=( Y, multiply( a, b
% 143.51/143.92 ) ), :=( Z, a )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42783, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, b ), a ), b ), a ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42782, [ ~( =( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, b ), multiply( a, b ) ), a ), b ), a ), b ),
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( multiply( a,
% 143.51/143.92 a ), a ), a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 6, substitution( 0, [ :=( X, multiply( a, b ) ), :=( Y, a ), :=( Z, b
% 143.51/143.92 )] ), substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42792, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, a ), a ), a ), b ), b ), b ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.92 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.92 , clause( 42783, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, b ), a ), b ), a ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 2, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, a ), a ), a ), b ), b ), b ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.92 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.92 , clause( 42792, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, a ), a ), a ), b ), b ), b ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.92 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.92 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42803, [ =( multiply( multiply( Y, Y ), X ), multiply( multiply( X
% 143.51/143.92 , Y ), Y ) ) ] )
% 143.51/143.92 , clause( 1, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y, Y
% 143.51/143.92 ), X ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42862, [ =( multiply( multiply( multiply( X, Y ), multiply( X, Y )
% 143.51/143.92 ), Z ), multiply( multiply( multiply( Z, X ), Y ), multiply( X, Y ) ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42803, [ =( multiply( multiply( Y, Y ), X ), multiply(
% 143.51/143.92 multiply( X, Y ), Y ) ) ] )
% 143.51/143.92 , 0, 11, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 143.51/143.92 substitution( 1, [ :=( X, Z ), :=( Y, multiply( X, Y ) )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42868, [ =( multiply( multiply( multiply( X, Y ), multiply( X, Y )
% 143.51/143.92 ), Z ), multiply( multiply( multiply( multiply( Z, X ), Y ), X ), Y ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42862, [ =( multiply( multiply( multiply( X, Y ), multiply( X
% 143.51/143.92 , Y ) ), Z ), multiply( multiply( multiply( Z, X ), Y ), multiply( X, Y )
% 143.51/143.92 ) ) ] )
% 143.51/143.92 , 0, 10, substitution( 0, [ :=( X, multiply( multiply( Z, X ), Y ) ), :=( Y
% 143.51/143.92 , X ), :=( Z, Y )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z
% 143.51/143.92 )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42870, [ =( multiply( multiply( multiply( multiply( X, Y ), X ), Y
% 143.51/143.92 ), Z ), multiply( multiply( multiply( multiply( Z, X ), Y ), X ), Y ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42868, [ =( multiply( multiply( multiply( X, Y ), multiply( X
% 143.51/143.92 , Y ) ), Z ), multiply( multiply( multiply( multiply( Z, X ), Y ), X ), Y
% 143.51/143.92 ) ) ] )
% 143.51/143.92 , 0, 2, substitution( 0, [ :=( X, multiply( X, Y ) ), :=( Y, X ), :=( Z, Y
% 143.51/143.92 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 5, [ =( multiply( multiply( multiply( multiply( Y, Z ), Y ), Z ), X
% 143.51/143.92 ), multiply( multiply( multiply( multiply( X, Y ), Z ), Y ), Z ) ) ] )
% 143.51/143.92 , clause( 42870, [ =( multiply( multiply( multiply( multiply( X, Y ), X ),
% 143.51/143.92 Y ), Z ), multiply( multiply( multiply( multiply( Z, X ), Y ), X ), Y ) )
% 143.51/143.92 ] )
% 143.51/143.92 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 143.51/143.92 permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42872, [ =( multiply( multiply( Y, Y ), X ), multiply( multiply( X
% 143.51/143.92 , Y ), Y ) ) ] )
% 143.51/143.92 , clause( 1, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y, Y
% 143.51/143.92 ), X ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42873, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 143.51/143.92 Y, Z ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42876, [ =( multiply( multiply( multiply( X, X ), Y ), Z ),
% 143.51/143.92 multiply( multiply( multiply( Y, Z ), X ), X ) ) ] )
% 143.51/143.92 , clause( 42872, [ =( multiply( multiply( Y, Y ), X ), multiply( multiply(
% 143.51/143.92 X, Y ), Y ) ) ] )
% 143.51/143.92 , 0, clause( 42873, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 143.51/143.92 multiply( Y, Z ) ) ) ] )
% 143.51/143.92 , 0, 8, substitution( 0, [ :=( X, multiply( Y, Z ) ), :=( Y, X )] ),
% 143.51/143.92 substitution( 1, [ :=( X, multiply( X, X ) ), :=( Y, Y ), :=( Z, Z )] )
% 143.51/143.92 ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42882, [ =( multiply( multiply( multiply( Y, Z ), X ), X ),
% 143.51/143.92 multiply( multiply( multiply( X, X ), Y ), Z ) ) ] )
% 143.51/143.92 , clause( 42876, [ =( multiply( multiply( multiply( X, X ), Y ), Z ),
% 143.51/143.92 multiply( multiply( multiply( Y, Z ), X ), X ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 6, [ =( multiply( multiply( multiply( Y, Z ), X ), X ), multiply(
% 143.51/143.92 multiply( multiply( X, X ), Y ), Z ) ) ] )
% 143.51/143.92 , clause( 42882, [ =( multiply( multiply( multiply( Y, Z ), X ), X ),
% 143.51/143.92 multiply( multiply( multiply( X, X ), Y ), Z ) ) ] )
% 143.51/143.92 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 143.51/143.92 permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42884, [ =( multiply( multiply( Y, Y ), X ), multiply( multiply( X
% 143.51/143.92 , Y ), Y ) ) ] )
% 143.51/143.92 , clause( 1, [ =( multiply( multiply( X, Y ), Y ), multiply( multiply( Y, Y
% 143.51/143.92 ), X ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42885, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 143.51/143.92 Y, Z ) ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42892, [ =( multiply( multiply( X, multiply( Y, Y ) ), Z ),
% 143.51/143.92 multiply( X, multiply( multiply( Z, Y ), Y ) ) ) ] )
% 143.51/143.92 , clause( 42884, [ =( multiply( multiply( Y, Y ), X ), multiply( multiply(
% 143.51/143.92 X, Y ), Y ) ) ] )
% 143.51/143.92 , 0, clause( 42885, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 143.51/143.92 multiply( Y, Z ) ) ) ] )
% 143.51/143.92 , 0, 10, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 143.51/143.92 :=( X, X ), :=( Y, multiply( Y, Y ) ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42895, [ =( multiply( multiply( X, multiply( Y, Y ) ), Z ),
% 143.51/143.92 multiply( multiply( X, multiply( Z, Y ) ), Y ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42892, [ =( multiply( multiply( X, multiply( Y, Y ) ), Z ),
% 143.51/143.92 multiply( X, multiply( multiply( Z, Y ), Y ) ) ) ] )
% 143.51/143.92 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, multiply( Z, Y ) ), :=( Z, Y
% 143.51/143.92 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42900, [ =( multiply( multiply( X, multiply( Y, Y ) ), Z ),
% 143.51/143.92 multiply( multiply( multiply( X, Z ), Y ), Y ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42895, [ =( multiply( multiply( X, multiply( Y, Y ) ), Z ),
% 143.51/143.92 multiply( multiply( X, multiply( Z, Y ) ), Y ) ) ] )
% 143.51/143.92 , 0, 9, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 143.51/143.92 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 42902, [ =( multiply( multiply( multiply( X, Y ), Y ), Z ),
% 143.51/143.92 multiply( multiply( multiply( X, Z ), Y ), Y ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 42900, [ =( multiply( multiply( X, multiply( Y, Y ) ), Z ),
% 143.51/143.92 multiply( multiply( multiply( X, Z ), Y ), Y ) ) ] )
% 143.51/143.92 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y )] ),
% 143.51/143.92 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 7, [ =( multiply( multiply( multiply( Z, Y ), Y ), X ), multiply(
% 143.51/143.92 multiply( multiply( Z, X ), Y ), Y ) ) ] )
% 143.51/143.92 , clause( 42902, [ =( multiply( multiply( multiply( X, Y ), Y ), Z ),
% 143.51/143.92 multiply( multiply( multiply( X, Z ), Y ), Y ) ) ] )
% 143.51/143.92 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 143.51/143.92 permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 42905, [ =( multiply( multiply( multiply( Z, Z ), X ), Y ),
% 143.51/143.92 multiply( multiply( multiply( X, Y ), Z ), Z ) ) ] )
% 143.51/143.92 , clause( 6, [ =( multiply( multiply( multiply( Y, Z ), X ), X ), multiply(
% 143.51/143.92 multiply( multiply( X, X ), Y ), Z ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 43185, [ =( multiply( multiply( multiply( X, X ), multiply( Y, Z )
% 143.51/143.92 ), Z ), multiply( multiply( multiply( multiply( Y, X ), Z ), Z ), X ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 7, [ =( multiply( multiply( multiply( Z, Y ), Y ), X ), multiply(
% 143.51/143.92 multiply( multiply( Z, X ), Y ), Y ) ) ] )
% 143.51/143.92 , 0, clause( 42905, [ =( multiply( multiply( multiply( Z, Z ), X ), Y ),
% 143.51/143.92 multiply( multiply( multiply( X, Y ), Z ), Z ) ) ] )
% 143.51/143.92 , 0, 11, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 143.51/143.92 substitution( 1, [ :=( X, multiply( Y, Z ) ), :=( Y, Z ), :=( Z, X )] )
% 143.51/143.92 ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 43210, [ =( multiply( multiply( multiply( multiply( X, X ), Y ), Z
% 143.51/143.92 ), Z ), multiply( multiply( multiply( multiply( Y, X ), Z ), Z ), X ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 43185, [ =( multiply( multiply( multiply( X, X ), multiply( Y
% 143.51/143.92 , Z ) ), Z ), multiply( multiply( multiply( multiply( Y, X ), Z ), Z ), X
% 143.51/143.92 ) ) ] )
% 143.51/143.92 , 0, 2, substitution( 0, [ :=( X, multiply( X, X ) ), :=( Y, Y ), :=( Z, Z
% 143.51/143.92 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 43211, [ =( multiply( multiply( multiply( multiply( Y, X ), Z ), Z
% 143.51/143.92 ), X ), multiply( multiply( multiply( multiply( X, X ), Y ), Z ), Z ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 43210, [ =( multiply( multiply( multiply( multiply( X, X ), Y ),
% 143.51/143.92 Z ), Z ), multiply( multiply( multiply( multiply( Y, X ), Z ), Z ), X ) )
% 143.51/143.92 ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 26, [ =( multiply( multiply( multiply( multiply( X, Z ), Y ), Y ),
% 143.51/143.92 Z ), multiply( multiply( multiply( multiply( Z, Z ), X ), Y ), Y ) ) ] )
% 143.51/143.92 , clause( 43211, [ =( multiply( multiply( multiply( multiply( Y, X ), Z ),
% 143.51/143.92 Z ), X ), multiply( multiply( multiply( multiply( X, X ), Y ), Z ), Z ) )
% 143.51/143.92 ] )
% 143.51/143.92 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 143.51/143.92 permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 43212, [ =( multiply( multiply( multiply( multiply( Z, X ), Y ), X
% 143.51/143.92 ), Y ), multiply( multiply( multiply( multiply( X, Y ), X ), Y ), Z ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 5, [ =( multiply( multiply( multiply( multiply( Y, Z ), Y ), Z )
% 143.51/143.92 , X ), multiply( multiply( multiply( multiply( X, Y ), Z ), Y ), Z ) ) ]
% 143.51/143.92 )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 43213, [ =( multiply( multiply( multiply( multiply( Y, Y ), X ), Z
% 143.51/143.92 ), Z ), multiply( multiply( multiply( multiply( X, Y ), Z ), Z ), Y ) )
% 143.51/143.92 ] )
% 143.51/143.92 , clause( 26, [ =( multiply( multiply( multiply( multiply( X, Z ), Y ), Y )
% 143.51/143.92 , Z ), multiply( multiply( multiply( multiply( Z, Z ), X ), Y ), Y ) ) ]
% 143.51/143.92 )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 43220, [ =( multiply( multiply( multiply( multiply( X, X ),
% 143.51/143.92 multiply( multiply( Y, X ), Z ) ), Z ), Z ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Z ), X ), Z ), Y ), Z ), X ) ) ] )
% 143.51/143.92 , clause( 43212, [ =( multiply( multiply( multiply( multiply( Z, X ), Y ),
% 143.51/143.92 X ), Y ), multiply( multiply( multiply( multiply( X, Y ), X ), Y ), Z ) )
% 143.51/143.92 ] )
% 143.51/143.92 , 0, clause( 43213, [ =( multiply( multiply( multiply( multiply( Y, Y ), X
% 143.51/143.92 ), Z ), Z ), multiply( multiply( multiply( multiply( X, Y ), Z ), Z ), Y
% 143.51/143.92 ) ) ] )
% 143.51/143.92 , 0, 16, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 143.51/143.92 substitution( 1, [ :=( X, multiply( multiply( Y, X ), Z ) ), :=( Y, X ),
% 143.51/143.92 :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 43232, [ =( multiply( multiply( multiply( multiply( multiply( X, X
% 143.51/143.92 ), multiply( Y, X ) ), Z ), Z ), Z ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Z ), X ), Z ), Y ), Z ), X ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 43220, [ =( multiply( multiply( multiply( multiply( X, X ),
% 143.51/143.92 multiply( multiply( Y, X ), Z ) ), Z ), Z ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Z ), X ), Z ), Y ), Z ), X ) ) ] )
% 143.51/143.92 , 0, 3, substitution( 0, [ :=( X, multiply( X, X ) ), :=( Y, multiply( Y, X
% 143.51/143.92 ) ), :=( Z, Z )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z
% 143.51/143.92 )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 43234, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( X, X ), Y ), X ), Z ), Z ), Z ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Z ), X ), Z ), Y ), Z ), X ) ) ] )
% 143.51/143.92 , clause( 0, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 143.51/143.92 ), Z ) ) ] )
% 143.51/143.92 , 0, clause( 43232, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 X, X ), multiply( Y, X ) ), Z ), Z ), Z ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Z ), X ), Z ), Y ), Z ), X ) ) ] )
% 143.51/143.92 , 0, 4, substitution( 0, [ :=( X, multiply( X, X ) ), :=( Y, Y ), :=( Z, X
% 143.51/143.92 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 43235, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( X, Z ), X ), Z ), Y ), Z ), X ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, X ), Y ), X ), Z ), Z ), Z ) ) ] )
% 143.51/143.92 , clause( 43234, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( X, X ), Y ), X ), Z ), Z ), Z ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Z ), X ), Z ), Y ), Z ), X ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 440, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( Y, Z ), Y ), Z ), X ), Z ), Y ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( Y, Y ), X ), Y ), Z ), Z ), Z ) ) ] )
% 143.51/143.92 , clause( 43235, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( X, Z ), X ), Z ), Y ), Z ), X ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, X ), Y ), X ), Z ), Z ), Z ) ) ] )
% 143.51/143.92 , substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 143.51/143.92 permutation( 0, [ ==>( 0, 0 )] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 43236, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( X, X ), Z ), X ), Y ), Y ), Y ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Y ), X ), Y ), Z ), Y ), X ) ) ] )
% 143.51/143.92 , clause( 440, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( Y, Z ), Y ), Z ), X ), Z ), Y ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( Y, Y ), X ), Y ), Z ), Z ), Z ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqswap(
% 143.51/143.92 clause( 43237, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, b ), a ), b ), a ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, a ), a ),
% 143.51/143.92 a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , clause( 2, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, a ), a ), a ), b ), b ), b ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.92 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 paramod(
% 143.51/143.92 clause( 43238, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, b ), a ), b ), a ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.92 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.92 , clause( 43236, [ =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( X, X ), Z ), X ), Y ), Y ), Y ), multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( X, Y ), X ), Y ), Z ), Y ), X ) ) ] )
% 143.51/143.92 , 0, clause( 43237, [ ~( =( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( multiply( a, b ), a ), b ), a ), b ), a ), b ),
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( multiply( a,
% 143.51/143.92 a ), a ), a ), b ), b ), b ), b ) ) ) ] )
% 143.51/143.92 , 0, 18, substitution( 0, [ :=( X, a ), :=( Y, b ), :=( Z, a )] ),
% 143.51/143.92 substitution( 1, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 eqrefl(
% 143.51/143.92 clause( 43239, [] )
% 143.51/143.92 , clause( 43238, [ ~( =( multiply( multiply( multiply( multiply( multiply(
% 143.51/143.92 multiply( multiply( a, b ), a ), b ), a ), b ), a ), b ), multiply(
% 143.51/143.92 multiply( multiply( multiply( multiply( multiply( multiply( a, b ), a ),
% 143.51/143.92 b ), a ), b ), a ), b ) ) ) ] )
% 143.51/143.92 , 0, substitution( 0, [] )).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 subsumption(
% 143.51/143.92 clause( 1164, [] )
% 143.51/143.92 , clause( 43239, [] )
% 143.51/143.92 , substitution( 0, [] ), permutation( 0, [] ) ).
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 end.
% 143.51/143.92
% 143.51/143.92 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 143.51/143.92
% 143.51/143.92 Memory use:
% 143.51/143.92
% 143.51/143.92 space for terms: 30752
% 143.51/143.92 space for clauses: 117837
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 clauses generated: 12345553
% 143.51/143.92 clauses kept: 1165
% 143.51/143.92 clauses selected: 811
% 143.51/143.92 clauses deleted: 205
% 143.51/143.92 clauses inuse deleted: 0
% 143.51/143.92
% 143.51/143.92 subsentry: 4326240
% 143.51/143.92 literals s-matched: 1559129
% 143.51/143.92 literals matched: 1558765
% 143.51/143.92 full subsumption: 0
% 143.51/143.92
% 143.51/143.92 checksum: -50015141
% 143.51/143.92
% 143.51/143.92
% 143.51/143.92 Bliksem ended
%------------------------------------------------------------------------------