%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP755-1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n032.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:39:26 EDT 2022
% Result : Unsatisfiable 1.60s 1.99s
% Output : Refutation 1.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GRP755-1 : TPTP v8.1.0. Released v4.0.0.
% 0.02/0.09 % Command : bliksem %s
% 0.10/0.28 % Computer : n032.cluster.edu
% 0.10/0.28 % Model : x86_64 x86_64
% 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.28 % Memory : 8042.1875MB
% 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.28 % CPULimit : 300
% 0.10/0.28 % DateTime : Mon Jun 13 15:37:27 EDT 2022
% 0.10/0.28 % CPUTime :
% 1.60/1.99 *** allocated 10000 integers for termspace/termends
% 1.60/1.99 *** allocated 10000 integers for clauses
% 1.60/1.99 *** allocated 10000 integers for justifications
% 1.60/1.99 Bliksem 1.12
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 Automatic Strategy Selection
% 1.60/1.99
% 1.60/1.99 Clauses:
% 1.60/1.99 [
% 1.60/1.99 [ =( mult( X, ld( X, Y ) ), Y ) ],
% 1.60/1.99 [ =( ld( X, mult( X, Y ) ), Y ) ],
% 1.60/1.99 [ =( mult( rd( X, Y ), Y ), X ) ],
% 1.60/1.99 [ =( rd( mult( X, Y ), Y ), X ) ],
% 1.60/1.99 [ =( mult( X, unit ), X ) ],
% 1.60/1.99 [ =( mult( unit, X ), X ) ],
% 1.60/1.99 [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =( mult( X,
% 1.60/1.99 mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ],
% 1.60/1.99 [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =( mult( X,
% 1.60/1.99 mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ],
% 1.60/1.99 [ =( i( X ), ld( X, unit ) ) ],
% 1.60/1.99 [ ~( =( i( mult( a, b ) ), mult( i( b ), i( a ) ) ) ) ]
% 1.60/1.99 ] .
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 percentage equality = 1.000000, percentage horn = 0.800000
% 1.60/1.99 This is a pure equality problem
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 Options Used:
% 1.60/1.99
% 1.60/1.99 useres = 1
% 1.60/1.99 useparamod = 1
% 1.60/1.99 useeqrefl = 1
% 1.60/1.99 useeqfact = 1
% 1.60/1.99 usefactor = 1
% 1.60/1.99 usesimpsplitting = 0
% 1.60/1.99 usesimpdemod = 5
% 1.60/1.99 usesimpres = 3
% 1.60/1.99
% 1.60/1.99 resimpinuse = 1000
% 1.60/1.99 resimpclauses = 20000
% 1.60/1.99 substype = eqrewr
% 1.60/1.99 backwardsubs = 1
% 1.60/1.99 selectoldest = 5
% 1.60/1.99
% 1.60/1.99 litorderings [0] = split
% 1.60/1.99 litorderings [1] = extend the termordering, first sorting on arguments
% 1.60/1.99
% 1.60/1.99 termordering = kbo
% 1.60/1.99
% 1.60/1.99 litapriori = 0
% 1.60/1.99 termapriori = 1
% 1.60/1.99 litaposteriori = 0
% 1.60/1.99 termaposteriori = 0
% 1.60/1.99 demodaposteriori = 0
% 1.60/1.99 ordereqreflfact = 0
% 1.60/1.99
% 1.60/1.99 litselect = negord
% 1.60/1.99
% 1.60/1.99 maxweight = 15
% 1.60/1.99 maxdepth = 30000
% 1.60/1.99 maxlength = 115
% 1.60/1.99 maxnrvars = 195
% 1.60/1.99 excuselevel = 1
% 1.60/1.99 increasemaxweight = 1
% 1.60/1.99
% 1.60/1.99 maxselected = 10000000
% 1.60/1.99 maxnrclauses = 10000000
% 1.60/1.99
% 1.60/1.99 showgenerated = 0
% 1.60/1.99 showkept = 0
% 1.60/1.99 showselected = 0
% 1.60/1.99 showdeleted = 0
% 1.60/1.99 showresimp = 1
% 1.60/1.99 showstatus = 2000
% 1.60/1.99
% 1.60/1.99 prologoutput = 1
% 1.60/1.99 nrgoals = 5000000
% 1.60/1.99 totalproof = 1
% 1.60/1.99
% 1.60/1.99 Symbols occurring in the translation:
% 1.60/1.99
% 1.60/1.99 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.60/1.99 . [1, 2] (w:1, o:21, a:1, s:1, b:0),
% 1.60/1.99 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 1.60/1.99 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.60/1.99 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.60/1.99 ld [41, 2] (w:1, o:46, a:1, s:1, b:0),
% 1.60/1.99 mult [42, 2] (w:1, o:47, a:1, s:1, b:0),
% 1.60/1.99 rd [43, 2] (w:1, o:48, a:1, s:1, b:0),
% 1.60/1.99 unit [44, 0] (w:1, o:11, a:1, s:1, b:0),
% 1.60/1.99 i [46, 1] (w:1, o:20, a:1, s:1, b:0),
% 1.60/1.99 a [47, 0] (w:1, o:13, a:1, s:1, b:0),
% 1.60/1.99 b [48, 0] (w:1, o:14, a:1, s:1, b:0).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 Starting Search:
% 1.60/1.99
% 1.60/1.99 Resimplifying inuse:
% 1.60/1.99 Done
% 1.60/1.99
% 1.60/1.99 Failed to find proof!
% 1.60/1.99 maxweight = 15
% 1.60/1.99 maxnrclauses = 10000000
% 1.60/1.99 Generated: 22628
% 1.60/1.99 Kept: 130
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 The strategy used was not complete!
% 1.60/1.99
% 1.60/1.99 Increased maxweight to 16
% 1.60/1.99
% 1.60/1.99 Starting Search:
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 Bliksems!, er is een bewijs:
% 1.60/1.99 % SZS status Unsatisfiable
% 1.60/1.99 % SZS output start Refutation
% 1.60/1.99
% 1.60/1.99 clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 6, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =( mult(
% 1.60/1.99 X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 7, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =( mult(
% 1.60/1.99 X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 9, [ ~( =( mult( i( b ), i( a ) ), i( mult( a, b ) ) ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 10, [ =( mult( X, mult( Y, Y ) ), mult( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 11, [ ~( =( mult( mult( X, Y ), Z ), mult( mult( X, Z ), Y ) ) ),
% 1.60/1.99 =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 13, [ =( rd( X, X ), unit ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 14, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 18, [ =( rd( unit, i( X ) ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 19, [ =( ld( X, X ), unit ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 20, [ =( ld( rd( X, Y ), X ), Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 27, [ =( mult( mult( Y, X ), i( X ) ), Y ), =( mult( mult( Y, i( X
% 1.60/1.99 ) ), X ), Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 32, [ =( i( rd( unit, X ) ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 33, [ =( ld( X, mult( mult( X, Y ), Y ) ), mult( Y, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 47, [ =( mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ), X ), =( mult(
% 1.60/1.99 rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult( Y, Z ) )
% 1.60/1.99 , Z ), Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 49, [ =( ld( X, mult( mult( X, Y ), Z ) ), mult( Y, Z ) ), =( mult(
% 1.60/1.99 X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 55, [ =( ld( rd( X, Y ), mult( X, Y ) ), mult( Y, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 56, [ =( mult( i( X ), i( X ) ), ld( X, i( X ) ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 65, [ =( mult( mult( Y, i( X ) ), X ), Y ), ~( =( mult( mult( Y, i(
% 1.60/1.99 X ) ), X ), Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 66, [ ~( =( mult( X, Y ), mult( Y, X ) ) ), =( mult( X, Y ), mult(
% 1.60/1.99 Y, X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 68, [ =( rd( mult( X, Y ), mult( Y, Y ) ), rd( X, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 75, [ =( rd( mult( Y, i( X ) ), ld( X, i( X ) ) ), rd( Y, i( X ) )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 78, [ =( mult( Y, rd( X, Y ) ), X ), ~( =( mult( Y, rd( X, Y ) ), X
% 1.60/1.99 ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 80, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ), unit )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 87, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X ), i(
% 1.60/1.99 X ) ), Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 88, [ ~( =( mult( i( X ), X ), unit ) ), =( i( i( X ) ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 89, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( X ), X ), unit ) )
% 1.60/1.99 ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 90, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( rd( unit, X ), i(
% 1.60/1.99 X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 91, [ =( i( i( X ) ), X ), ~( =( mult( i( i( X ) ), i( X ) ), unit
% 1.60/1.99 ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 95, [ =( mult( i( X ), X ), unit ), ~( =( mult( X, rd( unit, X ) )
% 1.60/1.99 , unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 101, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( i( X ) ), i( X )
% 1.60/1.99 ), unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 104, [ ~( =( mult( i( Y ), Y ), unit ) ), =( mult( X, i( Y ) ), rd(
% 1.60/1.99 X, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 105, [ =( ld( mult( X, Y ), X ), i( Y ) ), ~( =( mult( i( Y ), Y )
% 1.60/1.99 , unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 106, [ =( rd( X, i( Y ) ), mult( X, Y ) ), ~( =( mult( i( Y ), Y )
% 1.60/1.99 , unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 112, [ ~( =( rd( i( b ), a ), i( mult( a, b ) ) ) ), ~( =( mult( i(
% 1.60/1.99 a ), a ), unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 113, [ =( ld( X, rd( X, Y ) ), i( Y ) ), ~( =( mult( i( Y ), Y ),
% 1.60/1.99 unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 114, [ =( ld( X, rd( X, Y ) ), i( Y ) ), ~( =( mult( Y, rd( unit, Y
% 1.60/1.99 ) ), unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 115, [ =( ld( mult( X, Y ), X ), i( Y ) ), ~( =( mult( Y, rd( unit
% 1.60/1.99 , Y ) ), unit ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 120, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( mult( X, rd( Y, X ) ), Y
% 1.60/1.99 ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 121, [ =( ld( ld( Y, X ), X ), Y ), ~( =( mult( Y, rd( X, Y ) ), X
% 1.60/1.99 ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 122, [ =( mult( ld( Y, X ), Y ), X ), ~( =( mult( Y, rd( X, Y ) ),
% 1.60/1.99 X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 128, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( mult( mult( X, Y ), i(
% 1.60/1.99 Y ) ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 133, [ =( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), mult( X, i( Y )
% 1.60/1.99 ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 176, [ =( rd( X, i( Y ) ), mult( X, Y ) ), =( mult( X, i( Y ) ), rd(
% 1.60/1.99 X, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 184, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( mult( i( X ), X )
% 1.60/1.99 , unit ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 186, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( i( i( X ) ), X ) ]
% 1.60/1.99 )
% 1.60/1.99 .
% 1.60/1.99 clause( 190, [ =( mult( ld( X, i( X ) ), X ), i( X ) ), =( i( i( X ) ), X )
% 1.60/1.99 ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 195, [ =( i( i( X ) ), X ), =( mult( mult( Y, i( X ) ), X ), Y ) ]
% 1.60/1.99 )
% 1.60/1.99 .
% 1.60/1.99 clause( 209, [ =( i( i( X ) ), X ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 225, [ =( rd( unit, X ), i( X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 229, [ =( mult( Y, i( X ) ), rd( Y, X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 234, [ =( ld( Y, rd( Y, X ) ), i( X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 235, [ =( ld( mult( Y, X ), Y ), i( X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 253, [ =( ld( X, ld( Y, X ) ), i( Y ) ), ~( =( mult( Y, rd( X, Y )
% 1.60/1.99 ), X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 254, [ =( i( ld( Y, X ) ), ld( X, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 275, [ =( mult( i( X ), Y ), ld( X, Y ) ), =( mult( X, rd( Y, X ) )
% 1.60/1.99 , Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 341, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( rd( Y, X ), ld( X, Y ) )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 342, [ =( ld( i( X ), ld( X, Y ) ), Y ), =( mult( X, rd( Y, X ) ),
% 1.60/1.99 Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 344, [ =( ld( ld( Y, X ), X ), Y ), ~( =( rd( X, Y ), ld( Y, X ) )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 345, [ =( ld( ld( Y, X ), X ), Y ), ~( =( ld( ld( Y, X ), X ), Y )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 350, [ =( ld( Y, mult( X, Y ) ), X ), ~( =( rd( mult( X, Y ), X ),
% 1.60/1.99 Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 357, [ =( mult( X, Y ), mult( Y, X ) ), ~( =( rd( mult( Y, X ), Y )
% 1.60/1.99 , X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 376, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( ld( ld( X, Y ), Y ), X )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 383, [ =( mult( Y, X ), mult( X, Y ) ), ~( =( ld( Y, mult( X, Y ) )
% 1.60/1.99 , X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 400, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( ld( i( X ), rd( Y, X ) )
% 1.60/1.99 , Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 407, [ =( ld( ld( Y, X ), X ), Y ), ~( =( ld( ld( X, Y ), Y ), X )
% 1.60/1.99 ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 431, [ =( ld( i( X ), ld( X, Y ) ), Y ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 454, [ =( rd( ld( X, Y ), Y ), i( X ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 456, [ =( mult( i( X ), Y ), ld( X, Y ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 470, [ =( rd( i( Y ), X ), i( mult( X, Y ) ) ) ] )
% 1.60/1.99 .
% 1.60/1.99 clause( 542, [] )
% 1.60/1.99 .
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 % SZS output end Refutation
% 1.60/1.99 found a proof!
% 1.60/1.99
% 1.60/1.99 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 1.60/1.99
% 1.60/1.99 initialclauses(
% 1.60/1.99 [ clause( 544, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/1.99 , clause( 545, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/1.99 , clause( 546, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/1.99 , clause( 547, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 , clause( 548, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 , clause( 549, [ =( mult( unit, X ), X ) ] )
% 1.60/1.99 , clause( 550, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , clause( 551, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/1.99 , clause( 552, [ =( i( X ), ld( X, unit ) ) ] )
% 1.60/1.99 , clause( 553, [ ~( =( i( mult( a, b ) ), mult( i( b ), i( a ) ) ) ) ] )
% 1.60/1.99 ] ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/1.99 , clause( 544, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/1.99 , clause( 545, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/1.99 , clause( 546, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 , clause( 547, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 , clause( 548, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/1.99 , clause( 549, [ =( mult( unit, X ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 6, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =( mult(
% 1.60/1.99 X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , clause( 550, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.60/1.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 7, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =( mult(
% 1.60/1.99 X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/1.99 , clause( 551, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.60/1.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 618, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/1.99 , clause( 552, [ =( i( X ), ld( X, unit ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/1.99 , clause( 618, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 636, [ ~( =( mult( i( b ), i( a ) ), i( mult( a, b ) ) ) ) ] )
% 1.60/1.99 , clause( 553, [ ~( =( i( mult( a, b ) ), mult( i( b ), i( a ) ) ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 9, [ ~( =( mult( i( b ), i( a ) ), i( mult( a, b ) ) ) ) ] )
% 1.60/1.99 , clause( 636, [ ~( =( mult( i( b ), i( a ) ), i( mult( a, b ) ) ) ) ] )
% 1.60/1.99 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 factor(
% 1.60/1.99 clause( 640, [ =( mult( X, mult( Y, Y ) ), mult( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , clause( 6, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 10, [ =( mult( X, mult( Y, Y ) ), mult( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , clause( 640, [ =( mult( X, mult( Y, Y ) ), mult( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqfact(
% 1.60/1.99 clause( 647, [ ~( =( mult( mult( X, Y ), Z ), mult( mult( X, Z ), Y ) ) ),
% 1.60/1.99 =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , clause( 6, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 11, [ ~( =( mult( mult( X, Y ), Z ), mult( mult( X, Z ), Y ) ) ),
% 1.60/1.99 =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , clause( 647, [ ~( =( mult( mult( X, Y ), Z ), mult( mult( X, Z ), Y ) ) )
% 1.60/1.99 , =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.60/1.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 656, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 657, [ =( unit, rd( X, X ) ) ] )
% 1.60/1.99 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/1.99 , 0, clause( 656, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, unit )
% 1.60/1.99 , :=( Y, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 658, [ =( rd( X, X ), unit ) ] )
% 1.60/1.99 , clause( 657, [ =( unit, rd( X, X ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 13, [ =( rd( X, X ), unit ) ] )
% 1.60/1.99 , clause( 658, [ =( rd( X, X ), unit ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 660, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 661, [ =( X, rd( Y, ld( X, Y ) ) ) ] )
% 1.60/1.99 , clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/1.99 , 0, clause( 660, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/1.99 :=( X, X ), :=( Y, ld( X, Y ) )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 662, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/1.99 , clause( 661, [ =( X, rd( Y, ld( X, Y ) ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 14, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/1.99 , clause( 662, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 664, [ =( Y, mult( X, ld( X, Y ) ) ) ] )
% 1.60/1.99 , clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 665, [ =( unit, mult( X, i( X ) ) ) ] )
% 1.60/1.99 , clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/1.99 , 0, clause( 664, [ =( Y, mult( X, ld( X, Y ) ) ) ] )
% 1.60/1.99 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, unit )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 666, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 , clause( 665, [ =( unit, mult( X, i( X ) ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 , clause( 666, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 668, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 669, [ =( X, rd( unit, i( X ) ) ) ] )
% 1.60/1.99 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 , 0, clause( 668, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/1.99 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, i( X ) )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 670, [ =( rd( unit, i( X ) ), X ) ] )
% 1.60/1.99 , clause( 669, [ =( X, rd( unit, i( X ) ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 18, [ =( rd( unit, i( X ) ), X ) ] )
% 1.60/1.99 , clause( 670, [ =( rd( unit, i( X ) ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 672, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/1.99 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 673, [ =( unit, ld( X, X ) ) ] )
% 1.60/1.99 , clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 , 0, clause( 672, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/1.99 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, unit )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 674, [ =( ld( X, X ), unit ) ] )
% 1.60/1.99 , clause( 673, [ =( unit, ld( X, X ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 19, [ =( ld( X, X ), unit ) ] )
% 1.60/1.99 , clause( 674, [ =( ld( X, X ), unit ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 676, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/1.99 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 677, [ =( X, ld( rd( Y, X ), Y ) ) ] )
% 1.60/1.99 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/1.99 , 0, clause( 676, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/1.99 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/1.99 :=( X, rd( Y, X ) ), :=( Y, X )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 678, [ =( ld( rd( Y, X ), Y ), X ) ] )
% 1.60/1.99 , clause( 677, [ =( X, ld( rd( Y, X ), Y ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 20, [ =( ld( rd( X, Y ), X ), Y ) ] )
% 1.60/1.99 , clause( 678, [ =( ld( rd( Y, X ), Y ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/1.99 )] ) ).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 680, [ =( mult( mult( X, Y ), Z ), mult( X, mult( Y, Z ) ) ), =(
% 1.60/1.99 mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , clause( 6, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/1.99 mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 688, [ =( mult( X, unit ), mult( mult( X, i( Y ) ), Y ) ), =( mult(
% 1.60/1.99 mult( X, Y ), i( Y ) ), mult( X, mult( Y, i( Y ) ) ) ) ] )
% 1.60/1.99 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 , 0, clause( 680, [ =( mult( mult( X, Y ), Z ), mult( X, mult( Y, Z ) ) ),
% 1.60/1.99 =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/1.99 , 1, 3, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, Y ), :=( Z, i( Y ) )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 691, [ =( mult( mult( X, Y ), i( Y ) ), mult( X, unit ) ), =( mult(
% 1.60/1.99 X, unit ), mult( mult( X, i( Y ) ), Y ) ) ] )
% 1.60/1.99 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/1.99 , 0, clause( 688, [ =( mult( X, unit ), mult( mult( X, i( Y ) ), Y ) ), =(
% 1.60/1.99 mult( mult( X, Y ), i( Y ) ), mult( X, mult( Y, i( Y ) ) ) ) ] )
% 1.60/1.99 , 1, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 694, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( mult( mult( X, Y )
% 1.60/1.99 , i( Y ) ), mult( X, unit ) ) ] )
% 1.60/1.99 , clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 , 0, clause( 691, [ =( mult( mult( X, Y ), i( Y ) ), mult( X, unit ) ), =(
% 1.60/1.99 mult( X, unit ), mult( mult( X, i( Y ) ), Y ) ) ] )
% 1.60/1.99 , 1, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 paramod(
% 1.60/1.99 clause( 696, [ =( mult( mult( X, Y ), i( Y ) ), X ), =( X, mult( mult( X, i(
% 1.60/1.99 Y ) ), Y ) ) ] )
% 1.60/1.99 , clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/1.99 , 0, clause( 694, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( mult( mult( X
% 1.60/1.99 , Y ), i( Y ) ), mult( X, unit ) ) ] )
% 1.60/1.99 , 1, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/1.99 :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 eqswap(
% 1.60/1.99 clause( 698, [ =( mult( mult( X, i( Y ) ), Y ), X ), =( mult( mult( X, Y )
% 1.60/1.99 , i( Y ) ), X ) ] )
% 1.60/1.99 , clause( 696, [ =( mult( mult( X, Y ), i( Y ) ), X ), =( X, mult( mult( X
% 1.60/1.99 , i( Y ) ), Y ) ) ] )
% 1.60/1.99 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/1.99
% 1.60/1.99
% 1.60/1.99 subsumption(
% 1.60/1.99 clause( 27, [ =( mult( mult( Y, X ), i( X ) ), Y ), =( mult( mult( Y, i( X
% 1.60/1.99 ) ), X ), Y ) ] )
% 1.60/1.99 , clause( 698, [ =( mult( mult( X, i( Y ) ), Y ), X ), =( mult( mult( X, Y
% 1.60/1.99 ), i( Y ) ), X ) ] )
% 1.60/1.99 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 1.60/2.00 ), ==>( 1, 0 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 700, [ =( Y, ld( rd( X, Y ), X ) ) ] )
% 1.60/2.00 , clause( 20, [ =( ld( rd( X, Y ), X ), Y ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 702, [ =( X, i( rd( unit, X ) ) ) ] )
% 1.60/2.00 , clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/2.00 , 0, clause( 700, [ =( Y, ld( rd( X, Y ), X ) ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, rd( unit, X ) )] ), substitution( 1, [
% 1.60/2.00 :=( X, unit ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 703, [ =( i( rd( unit, X ) ), X ) ] )
% 1.60/2.00 , clause( 702, [ =( X, i( rd( unit, X ) ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 32, [ =( i( rd( unit, X ) ), X ) ] )
% 1.60/2.00 , clause( 703, [ =( i( rd( unit, X ) ), X ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 705, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.00 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 706, [ =( mult( X, X ), ld( Y, mult( mult( Y, X ), X ) ) ) ] )
% 1.60/2.00 , clause( 10, [ =( mult( X, mult( Y, Y ) ), mult( mult( X, Y ), Y ) ) ] )
% 1.60/2.00 , 0, clause( 705, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.00 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.00 :=( X, Y ), :=( Y, mult( X, X ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 707, [ =( ld( Y, mult( mult( Y, X ), X ) ), mult( X, X ) ) ] )
% 1.60/2.00 , clause( 706, [ =( mult( X, X ), ld( Y, mult( mult( Y, X ), X ) ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 33, [ =( ld( X, mult( mult( X, Y ), Y ) ), mult( Y, Y ) ) ] )
% 1.60/2.00 , clause( 707, [ =( ld( Y, mult( mult( Y, X ), X ) ), mult( X, X ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 708, [ =( mult( mult( X, Y ), Z ), mult( X, mult( Y, Z ) ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , clause( 7, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 711, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.00 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 712, [ =( X, mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ) ), =( mult(
% 1.60/2.00 mult( rd( X, mult( Y, Z ) ), Z ), Y ), mult( rd( X, mult( Y, Z ) ), mult(
% 1.60/2.00 Z, Y ) ) ) ] )
% 1.60/2.00 , clause( 708, [ =( mult( mult( X, Y ), Z ), mult( X, mult( Y, Z ) ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , 1, clause( 711, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, rd( X, mult( Y, Z ) ) ), :=( Y, Z ), :=(
% 1.60/2.00 Z, Y )] ), substitution( 1, [ :=( X, X ), :=( Y, mult( Y, Z ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 742, [ =( mult( rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult(
% 1.60/2.00 rd( X, mult( Y, Z ) ), Z ), Y ) ), =( X, mult( mult( rd( X, mult( Y, Z )
% 1.60/2.00 ), Z ), Y ) ) ] )
% 1.60/2.00 , clause( 712, [ =( X, mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ) ), =(
% 1.60/2.00 mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ), mult( rd( X, mult( Y, Z ) )
% 1.60/2.00 , mult( Z, Y ) ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 743, [ =( mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ), X ), =( mult(
% 1.60/2.00 rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult( Y, Z ) )
% 1.60/2.00 , Z ), Y ) ) ] )
% 1.60/2.00 , clause( 742, [ =( mult( rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult(
% 1.60/2.00 rd( X, mult( Y, Z ) ), Z ), Y ) ), =( X, mult( mult( rd( X, mult( Y, Z )
% 1.60/2.00 ), Z ), Y ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 47, [ =( mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ), X ), =( mult(
% 1.60/2.00 rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult( Y, Z ) )
% 1.60/2.00 , Z ), Y ) ) ] )
% 1.60/2.00 , clause( 743, [ =( mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ), X ), =(
% 1.60/2.00 mult( rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult( Y,
% 1.60/2.00 Z ) ), Z ), Y ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.60/2.00 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 759, [ =( mult( mult( X, Z ), Y ), mult( X, mult( Y, Z ) ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , clause( 7, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 761, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.00 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 918, [ =( mult( X, Y ), ld( Z, mult( mult( Z, X ), Y ) ) ), =( mult(
% 1.60/2.00 mult( Z, X ), Y ), mult( Z, mult( Y, X ) ) ) ] )
% 1.60/2.00 , clause( 759, [ =( mult( mult( X, Z ), Y ), mult( X, mult( Y, Z ) ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , 1, clause( 761, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.00 , 0, 6, substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 1.60/2.00 substitution( 1, [ :=( X, Z ), :=( Y, mult( X, Y ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 964, [ =( mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/2.00 mult( Y, Z ), ld( X, mult( mult( X, Y ), Z ) ) ) ] )
% 1.60/2.00 , clause( 918, [ =( mult( X, Y ), ld( Z, mult( mult( Z, X ), Y ) ) ), =(
% 1.60/2.00 mult( mult( Z, X ), Y ), mult( Z, mult( Y, X ) ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 965, [ =( ld( Z, mult( mult( Z, X ), Y ) ), mult( X, Y ) ), =( mult(
% 1.60/2.00 Z, mult( Y, X ) ), mult( mult( Z, X ), Y ) ) ] )
% 1.60/2.00 , clause( 964, [ =( mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/2.00 mult( Y, Z ), ld( X, mult( mult( X, Y ), Z ) ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 49, [ =( ld( X, mult( mult( X, Y ), Z ) ), mult( Y, Z ) ), =( mult(
% 1.60/2.00 X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , clause( 965, [ =( ld( Z, mult( mult( Z, X ), Y ) ), mult( X, Y ) ), =(
% 1.60/2.00 mult( Z, mult( Y, X ) ), mult( mult( Z, X ), Y ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 1.60/2.00 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 997, [ =( mult( Y, Y ), ld( X, mult( mult( X, Y ), Y ) ) ) ] )
% 1.60/2.00 , clause( 33, [ =( ld( X, mult( mult( X, Y ), Y ) ), mult( Y, Y ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 998, [ =( mult( X, X ), ld( rd( Y, X ), mult( Y, X ) ) ) ] )
% 1.60/2.00 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.00 , 0, clause( 997, [ =( mult( Y, Y ), ld( X, mult( mult( X, Y ), Y ) ) ) ]
% 1.60/2.00 )
% 1.60/2.00 , 0, 9, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.00 :=( X, rd( Y, X ) ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 999, [ =( ld( rd( Y, X ), mult( Y, X ) ), mult( X, X ) ) ] )
% 1.60/2.00 , clause( 998, [ =( mult( X, X ), ld( rd( Y, X ), mult( Y, X ) ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 55, [ =( ld( rd( X, Y ), mult( X, Y ) ), mult( Y, Y ) ) ] )
% 1.60/2.00 , clause( 999, [ =( ld( rd( Y, X ), mult( Y, X ) ), mult( X, X ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1001, [ =( mult( Y, Y ), ld( X, mult( mult( X, Y ), Y ) ) ) ] )
% 1.60/2.00 , clause( 33, [ =( ld( X, mult( mult( X, Y ), Y ) ), mult( Y, Y ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1003, [ =( mult( i( X ), i( X ) ), ld( X, mult( unit, i( X ) ) ) )
% 1.60/2.00 ] )
% 1.60/2.00 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.00 , 0, clause( 1001, [ =( mult( Y, Y ), ld( X, mult( mult( X, Y ), Y ) ) ) ]
% 1.60/2.00 )
% 1.60/2.00 , 0, 9, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, i( X ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1004, [ =( mult( i( X ), i( X ) ), ld( X, i( X ) ) ) ] )
% 1.60/2.00 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/2.00 , 0, clause( 1003, [ =( mult( i( X ), i( X ) ), ld( X, mult( unit, i( X ) )
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , 0, 8, substitution( 0, [ :=( X, i( X ) )] ), substitution( 1, [ :=( X, X
% 1.60/2.00 )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 56, [ =( mult( i( X ), i( X ) ), ld( X, i( X ) ) ) ] )
% 1.60/2.00 , clause( 1004, [ =( mult( i( X ), i( X ) ), ld( X, i( X ) ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1007, [ ~( =( mult( mult( X, Z ), Y ), mult( mult( X, Y ), Z ) ) )
% 1.60/2.00 , =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , clause( 11, [ ~( =( mult( mult( X, Y ), Z ), mult( mult( X, Z ), Y ) ) )
% 1.60/2.00 , =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1018, [ =( mult( X, unit ), mult( mult( X, i( Y ) ), Y ) ), ~( =(
% 1.60/2.00 mult( mult( X, i( Y ) ), Y ), mult( mult( X, Y ), i( Y ) ) ) ) ] )
% 1.60/2.00 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.00 , 0, clause( 1007, [ ~( =( mult( mult( X, Z ), Y ), mult( mult( X, Y ), Z )
% 1.60/2.00 ) ), =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , 1, 3, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, Y ), :=( Z, i( Y ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1023, [ =( X, mult( mult( X, i( Y ) ), Y ) ), ~( =( mult( mult( X,
% 1.60/2.00 i( Y ) ), Y ), mult( mult( X, Y ), i( Y ) ) ) ) ] )
% 1.60/2.00 , clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/2.00 , 0, clause( 1018, [ =( mult( X, unit ), mult( mult( X, i( Y ) ), Y ) ),
% 1.60/2.00 ~( =( mult( mult( X, i( Y ) ), Y ), mult( mult( X, Y ), i( Y ) ) ) ) ] )
% 1.60/2.00 , 0, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1044, [ ~( =( mult( mult( X, i( Y ) ), Y ), X ) ), =( mult( mult( X
% 1.60/2.00 , i( Y ) ), Y ), X ), =( X, mult( mult( X, i( Y ) ), Y ) ) ] )
% 1.60/2.00 , clause( 27, [ =( mult( mult( Y, X ), i( X ) ), Y ), =( mult( mult( Y, i(
% 1.60/2.00 X ) ), X ), Y ) ] )
% 1.60/2.00 , 0, clause( 1023, [ =( X, mult( mult( X, i( Y ) ), Y ) ), ~( =( mult( mult(
% 1.60/2.00 X, i( Y ) ), Y ), mult( mult( X, Y ), i( Y ) ) ) ) ] )
% 1.60/2.00 , 1, 8, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.00 :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1066, [ =( mult( mult( X, i( Y ) ), Y ), X ), ~( =( mult( mult( X,
% 1.60/2.00 i( Y ) ), Y ), X ) ), =( mult( mult( X, i( Y ) ), Y ), X ) ] )
% 1.60/2.00 , clause( 1044, [ ~( =( mult( mult( X, i( Y ) ), Y ), X ) ), =( mult( mult(
% 1.60/2.00 X, i( Y ) ), Y ), X ), =( X, mult( mult( X, i( Y ) ), Y ) ) ] )
% 1.60/2.00 , 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 factor(
% 1.60/2.00 clause( 1158, [ =( mult( mult( X, i( Y ) ), Y ), X ), ~( =( mult( mult( X,
% 1.60/2.00 i( Y ) ), Y ), X ) ) ] )
% 1.60/2.00 , clause( 1066, [ =( mult( mult( X, i( Y ) ), Y ), X ), ~( =( mult( mult( X
% 1.60/2.00 , i( Y ) ), Y ), X ) ), =( mult( mult( X, i( Y ) ), Y ), X ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 65, [ =( mult( mult( Y, i( X ) ), X ), Y ), ~( =( mult( mult( Y, i(
% 1.60/2.00 X ) ), X ), Y ) ) ] )
% 1.60/2.00 , clause( 1158, [ =( mult( mult( X, i( Y ) ), Y ), X ), ~( =( mult( mult( X
% 1.60/2.00 , i( Y ) ), Y ), X ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 ), ==>( 1, 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1159, [ =( X, mult( unit, X ) ) ] )
% 1.60/2.00 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1160, [ ~( =( mult( mult( X, Z ), Y ), mult( mult( X, Y ), Z ) ) )
% 1.60/2.00 , =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , clause( 11, [ ~( =( mult( mult( X, Y ), Z ), mult( mult( X, Z ), Y ) ) )
% 1.60/2.00 , =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1166, [ =( mult( X, Y ), mult( mult( unit, Y ), X ) ), ~( =( mult(
% 1.60/2.00 mult( unit, Y ), X ), mult( mult( unit, X ), Y ) ) ) ] )
% 1.60/2.00 , clause( 1160, [ ~( =( mult( mult( X, Z ), Y ), mult( mult( X, Y ), Z ) )
% 1.60/2.00 ), =( mult( X, mult( Y, Z ) ), mult( mult( X, Z ), Y ) ) ] )
% 1.60/2.00 , 1, clause( 1159, [ =( X, mult( unit, X ) ) ] )
% 1.60/2.00 , 0, 4, substitution( 0, [ :=( X, unit ), :=( Y, X ), :=( Z, Y )] ),
% 1.60/2.00 substitution( 1, [ :=( X, mult( X, Y ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1169, [ ~( =( mult( mult( unit, X ), Y ), mult( Y, X ) ) ), =( mult(
% 1.60/2.00 Y, X ), mult( mult( unit, X ), Y ) ) ] )
% 1.60/2.00 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/2.00 , 0, clause( 1166, [ =( mult( X, Y ), mult( mult( unit, Y ), X ) ), ~( =(
% 1.60/2.00 mult( mult( unit, Y ), X ), mult( mult( unit, X ), Y ) ) ) ] )
% 1.60/2.00 , 1, 8, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.00 :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1175, [ =( mult( X, Y ), mult( Y, X ) ), ~( =( mult( mult( unit, Y
% 1.60/2.00 ), X ), mult( X, Y ) ) ) ] )
% 1.60/2.00 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/2.00 , 0, clause( 1169, [ ~( =( mult( mult( unit, X ), Y ), mult( Y, X ) ) ),
% 1.60/2.00 =( mult( Y, X ), mult( mult( unit, X ), Y ) ) ] )
% 1.60/2.00 , 1, 5, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.00 :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1177, [ ~( =( mult( X, Y ), mult( Y, X ) ) ), =( mult( Y, X ), mult(
% 1.60/2.00 X, Y ) ) ] )
% 1.60/2.00 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/2.00 , 0, clause( 1175, [ =( mult( X, Y ), mult( Y, X ) ), ~( =( mult( mult(
% 1.60/2.00 unit, Y ), X ), mult( X, Y ) ) ) ] )
% 1.60/2.00 , 1, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.00 :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1178, [ ~( =( mult( Y, X ), mult( X, Y ) ) ), =( mult( Y, X ), mult(
% 1.60/2.00 X, Y ) ) ] )
% 1.60/2.00 , clause( 1177, [ ~( =( mult( X, Y ), mult( Y, X ) ) ), =( mult( Y, X ),
% 1.60/2.00 mult( X, Y ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 66, [ ~( =( mult( X, Y ), mult( Y, X ) ) ), =( mult( X, Y ), mult(
% 1.60/2.00 Y, X ) ) ] )
% 1.60/2.00 , clause( 1178, [ ~( =( mult( Y, X ), mult( X, Y ) ) ), =( mult( Y, X ),
% 1.60/2.00 mult( X, Y ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 ), ==>( 1, 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1180, [ =( Y, rd( X, ld( Y, X ) ) ) ] )
% 1.60/2.00 , clause( 14, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1183, [ =( rd( X, Y ), rd( mult( X, Y ), mult( Y, Y ) ) ) ] )
% 1.60/2.00 , clause( 55, [ =( ld( rd( X, Y ), mult( X, Y ) ), mult( Y, Y ) ) ] )
% 1.60/2.00 , 0, clause( 1180, [ =( Y, rd( X, ld( Y, X ) ) ) ] )
% 1.60/2.00 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.00 :=( X, mult( X, Y ) ), :=( Y, rd( X, Y ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1184, [ =( rd( mult( X, Y ), mult( Y, Y ) ), rd( X, Y ) ) ] )
% 1.60/2.00 , clause( 1183, [ =( rd( X, Y ), rd( mult( X, Y ), mult( Y, Y ) ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 68, [ =( rd( mult( X, Y ), mult( Y, Y ) ), rd( X, Y ) ) ] )
% 1.60/2.00 , clause( 1184, [ =( rd( mult( X, Y ), mult( Y, Y ) ), rd( X, Y ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1186, [ =( rd( X, Y ), rd( mult( X, Y ), mult( Y, Y ) ) ) ] )
% 1.60/2.00 , clause( 68, [ =( rd( mult( X, Y ), mult( Y, Y ) ), rd( X, Y ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1189, [ =( rd( X, i( Y ) ), rd( mult( X, i( Y ) ), ld( Y, i( Y ) )
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , clause( 56, [ =( mult( i( X ), i( X ) ), ld( X, i( X ) ) ) ] )
% 1.60/2.00 , 0, clause( 1186, [ =( rd( X, Y ), rd( mult( X, Y ), mult( Y, Y ) ) ) ] )
% 1.60/2.00 , 0, 10, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, i( Y ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1194, [ =( rd( mult( X, i( Y ) ), ld( Y, i( Y ) ) ), rd( X, i( Y )
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , clause( 1189, [ =( rd( X, i( Y ) ), rd( mult( X, i( Y ) ), ld( Y, i( Y )
% 1.60/2.00 ) ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 75, [ =( rd( mult( Y, i( X ) ), ld( X, i( X ) ) ), rd( Y, i( X ) )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 1194, [ =( rd( mult( X, i( Y ) ), ld( Y, i( Y ) ) ), rd( X, i( Y
% 1.60/2.00 ) ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1195, [ ~( =( mult( Y, X ), mult( X, Y ) ) ), =( mult( X, Y ), mult(
% 1.60/2.00 Y, X ) ) ] )
% 1.60/2.00 , clause( 66, [ ~( =( mult( X, Y ), mult( Y, X ) ) ), =( mult( X, Y ), mult(
% 1.60/2.00 Y, X ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1196, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.00 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1198, [ =( X, mult( Y, rd( X, Y ) ) ), ~( =( mult( Y, rd( X, Y ) )
% 1.60/2.00 , mult( rd( X, Y ), Y ) ) ) ] )
% 1.60/2.00 , clause( 1195, [ ~( =( mult( Y, X ), mult( X, Y ) ) ), =( mult( X, Y ),
% 1.60/2.00 mult( Y, X ) ) ] )
% 1.60/2.00 , 1, clause( 1196, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, rd( X, Y ) ), :=( Y, Y )] ),
% 1.60/2.00 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1240, [ ~( =( mult( X, rd( Y, X ) ), Y ) ), =( Y, mult( X, rd( Y, X
% 1.60/2.00 ) ) ) ] )
% 1.60/2.00 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.00 , 0, clause( 1198, [ =( X, mult( Y, rd( X, Y ) ) ), ~( =( mult( Y, rd( X, Y
% 1.60/2.00 ) ), mult( rd( X, Y ), Y ) ) ) ] )
% 1.60/2.00 , 1, 7, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.00 :=( X, Y ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1242, [ =( mult( Y, rd( X, Y ) ), X ), ~( =( mult( Y, rd( X, Y ) )
% 1.60/2.00 , X ) ) ] )
% 1.60/2.00 , clause( 1240, [ ~( =( mult( X, rd( Y, X ) ), Y ) ), =( Y, mult( X, rd( Y
% 1.60/2.00 , X ) ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 78, [ =( mult( Y, rd( X, Y ) ), X ), ~( =( mult( Y, rd( X, Y ) ), X
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , clause( 1242, [ =( mult( Y, rd( X, Y ) ), X ), ~( =( mult( Y, rd( X, Y )
% 1.60/2.00 ), X ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.00 ), ==>( 1, 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1244, [ ~( =( mult( Y, X ), mult( X, Y ) ) ), =( mult( X, Y ), mult(
% 1.60/2.00 Y, X ) ) ] )
% 1.60/2.00 , clause( 66, [ ~( =( mult( X, Y ), mult( Y, X ) ) ), =( mult( X, Y ), mult(
% 1.60/2.00 Y, X ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1245, [ =( unit, mult( X, i( X ) ) ) ] )
% 1.60/2.00 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1247, [ =( unit, mult( i( X ), X ) ), ~( =( mult( i( X ), X ), mult(
% 1.60/2.00 X, i( X ) ) ) ) ] )
% 1.60/2.00 , clause( 1244, [ ~( =( mult( Y, X ), mult( X, Y ) ) ), =( mult( X, Y ),
% 1.60/2.00 mult( Y, X ) ) ] )
% 1.60/2.00 , 1, clause( 1245, [ =( unit, mult( X, i( X ) ) ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, i( X ) )] ), substitution( 1
% 1.60/2.00 , [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1296, [ ~( =( mult( i( X ), X ), unit ) ), =( unit, mult( i( X ), X
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.00 , 0, clause( 1247, [ =( unit, mult( i( X ), X ) ), ~( =( mult( i( X ), X )
% 1.60/2.00 , mult( X, i( X ) ) ) ) ] )
% 1.60/2.00 , 1, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.00 ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1298, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ), unit
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , clause( 1296, [ ~( =( mult( i( X ), X ), unit ) ), =( unit, mult( i( X )
% 1.60/2.00 , X ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 80, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ), unit )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 1298, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ),
% 1.60/2.00 unit ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 1.60/2.00 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1301, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( i( X ), X ),
% 1.60/2.00 unit ) ] )
% 1.60/2.00 , clause( 80, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ), unit
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1303, [ =( mult( mult( X, Y ), Z ), mult( X, mult( Y, Z ) ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , clause( 7, [ =( mult( X, mult( Y, Z ) ), mult( mult( X, Y ), Z ) ), =(
% 1.60/2.00 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1427, [ =( mult( X, unit ), mult( mult( X, Y ), i( Y ) ) ), ~( =(
% 1.60/2.00 unit, mult( i( Y ), Y ) ) ), =( mult( mult( X, Y ), i( Y ) ), mult( X,
% 1.60/2.00 mult( Y, i( Y ) ) ) ) ] )
% 1.60/2.00 , clause( 1301, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( i( X ), X ),
% 1.60/2.00 unit ) ] )
% 1.60/2.00 , 1, clause( 1303, [ =( mult( mult( X, Y ), Z ), mult( X, mult( Y, Z ) ) )
% 1.60/2.00 , =( mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.00 , 1, 3, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, Y ), :=( Z, i( Y ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1450, [ =( mult( mult( X, Y ), i( Y ) ), mult( X, unit ) ), =( mult(
% 1.60/2.00 X, unit ), mult( mult( X, Y ), i( Y ) ) ), ~( =( unit, mult( i( Y ), Y )
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.00 , 0, clause( 1427, [ =( mult( X, unit ), mult( mult( X, Y ), i( Y ) ) ),
% 1.60/2.00 ~( =( unit, mult( i( Y ), Y ) ) ), =( mult( mult( X, Y ), i( Y ) ), mult(
% 1.60/2.00 X, mult( Y, i( Y ) ) ) ) ] )
% 1.60/2.00 , 2, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1452, [ =( X, mult( mult( X, Y ), i( Y ) ) ), =( mult( mult( X, Y )
% 1.60/2.00 , i( Y ) ), mult( X, unit ) ), ~( =( unit, mult( i( Y ), Y ) ) ) ] )
% 1.60/2.00 , clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/2.00 , 0, clause( 1450, [ =( mult( mult( X, Y ), i( Y ) ), mult( X, unit ) ),
% 1.60/2.00 =( mult( X, unit ), mult( mult( X, Y ), i( Y ) ) ), ~( =( unit, mult( i(
% 1.60/2.00 Y ), Y ) ) ) ] )
% 1.60/2.00 , 1, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1454, [ =( mult( mult( X, Y ), i( Y ) ), X ), =( X, mult( mult( X,
% 1.60/2.00 Y ), i( Y ) ) ), ~( =( unit, mult( i( Y ), Y ) ) ) ] )
% 1.60/2.00 , clause( 4, [ =( mult( X, unit ), X ) ] )
% 1.60/2.00 , 0, clause( 1452, [ =( X, mult( mult( X, Y ), i( Y ) ) ), =( mult( mult( X
% 1.60/2.00 , Y ), i( Y ) ), mult( X, unit ) ), ~( =( unit, mult( i( Y ), Y ) ) ) ]
% 1.60/2.00 )
% 1.60/2.00 , 1, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.00 :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1457, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X ), i(
% 1.60/2.00 X ) ), Y ), =( Y, mult( mult( Y, X ), i( X ) ) ) ] )
% 1.60/2.00 , clause( 1454, [ =( mult( mult( X, Y ), i( Y ) ), X ), =( X, mult( mult( X
% 1.60/2.00 , Y ), i( Y ) ) ), ~( =( unit, mult( i( Y ), Y ) ) ) ] )
% 1.60/2.00 , 2, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1459, [ =( mult( mult( X, Y ), i( Y ) ), X ), ~( =( mult( i( Y ), Y
% 1.60/2.00 ), unit ) ), =( mult( mult( X, Y ), i( Y ) ), X ) ] )
% 1.60/2.00 , clause( 1457, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X )
% 1.60/2.00 , i( X ) ), Y ), =( Y, mult( mult( Y, X ), i( X ) ) ) ] )
% 1.60/2.00 , 2, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 factor(
% 1.60/2.00 clause( 1463, [ =( mult( mult( X, Y ), i( Y ) ), X ), ~( =( mult( i( Y ), Y
% 1.60/2.00 ), unit ) ) ] )
% 1.60/2.00 , clause( 1459, [ =( mult( mult( X, Y ), i( Y ) ), X ), ~( =( mult( i( Y )
% 1.60/2.00 , Y ), unit ) ), =( mult( mult( X, Y ), i( Y ) ), X ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 87, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X ), i(
% 1.60/2.00 X ) ), Y ) ] )
% 1.60/2.00 , clause( 1463, [ =( mult( mult( X, Y ), i( Y ) ), X ), ~( =( mult( i( Y )
% 1.60/2.00 , Y ), unit ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 1.60/2.00 ), ==>( 1, 0 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1465, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( i( X ), X ),
% 1.60/2.00 unit ) ] )
% 1.60/2.00 , clause( 80, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ), unit
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1467, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.00 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1469, [ =( X, ld( i( X ), unit ) ), ~( =( unit, mult( i( X ), X ) )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 1465, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( i( X ), X ),
% 1.60/2.00 unit ) ] )
% 1.60/2.00 , 1, clause( 1467, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.00 , 0, 5, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, i( X )
% 1.60/2.00 ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1480, [ =( X, i( i( X ) ) ), ~( =( unit, mult( i( X ), X ) ) ) ] )
% 1.60/2.00 , clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/2.00 , 0, clause( 1469, [ =( X, ld( i( X ), unit ) ), ~( =( unit, mult( i( X ),
% 1.60/2.00 X ) ) ) ] )
% 1.60/2.00 , 0, 2, substitution( 0, [ :=( X, i( X ) )] ), substitution( 1, [ :=( X, X
% 1.60/2.00 )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1482, [ ~( =( mult( i( X ), X ), unit ) ), =( X, i( i( X ) ) ) ] )
% 1.60/2.00 , clause( 1480, [ =( X, i( i( X ) ) ), ~( =( unit, mult( i( X ), X ) ) ) ]
% 1.60/2.00 )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1483, [ =( i( i( X ) ), X ), ~( =( mult( i( X ), X ), unit ) ) ] )
% 1.60/2.00 , clause( 1482, [ ~( =( mult( i( X ), X ), unit ) ), =( X, i( i( X ) ) ) ]
% 1.60/2.00 )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 88, [ ~( =( mult( i( X ), X ), unit ) ), =( i( i( X ) ), X ) ] )
% 1.60/2.00 , clause( 1483, [ =( i( i( X ) ), X ), ~( =( mult( i( X ), X ), unit ) ) ]
% 1.60/2.00 )
% 1.60/2.00 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 1.60/2.00 0 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1485, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( i( X ), X ),
% 1.60/2.00 unit ) ] )
% 1.60/2.00 , clause( 80, [ =( mult( i( X ), X ), unit ), ~( =( mult( i( X ), X ), unit
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1487, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.00 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1488, [ =( i( X ), rd( unit, X ) ), ~( =( unit, mult( i( X ), X ) )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 1485, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( i( X ), X ),
% 1.60/2.00 unit ) ] )
% 1.60/2.00 , 1, clause( 1487, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.00 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, i( X )
% 1.60/2.00 ), :=( Y, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1530, [ ~( =( mult( i( X ), X ), unit ) ), =( i( X ), rd( unit, X )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 1488, [ =( i( X ), rd( unit, X ) ), ~( =( unit, mult( i( X ), X )
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1531, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( X ), X ), unit )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 1530, [ ~( =( mult( i( X ), X ), unit ) ), =( i( X ), rd( unit, X
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 89, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( X ), X ), unit ) )
% 1.60/2.00 ] )
% 1.60/2.00 , clause( 1531, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( X ), X ), unit
% 1.60/2.00 ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 1.60/2.00 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1533, [ ~( =( unit, mult( i( X ), X ) ) ), =( i( i( X ) ), X ) ] )
% 1.60/2.00 , clause( 88, [ ~( =( mult( i( X ), X ), unit ) ), =( i( i( X ) ), X ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1537, [ =( i( X ), rd( unit, X ) ), ~( =( unit, mult( i( rd( unit,
% 1.60/2.00 X ) ), rd( unit, X ) ) ) ) ] )
% 1.60/2.00 , clause( 32, [ =( i( rd( unit, X ) ), X ) ] )
% 1.60/2.00 , 0, clause( 1533, [ ~( =( unit, mult( i( X ), X ) ) ), =( i( i( X ) ), X )
% 1.60/2.00 ] )
% 1.60/2.00 , 1, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, rd(
% 1.60/2.00 unit, X ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1538, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( i( X ), rd(
% 1.60/2.00 unit, X ) ) ] )
% 1.60/2.00 , clause( 32, [ =( i( rd( unit, X ) ), X ) ] )
% 1.60/2.00 , 0, clause( 1537, [ =( i( X ), rd( unit, X ) ), ~( =( unit, mult( i( rd(
% 1.60/2.00 unit, X ) ), rd( unit, X ) ) ) ) ] )
% 1.60/2.00 , 1, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.00 ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1543, [ =( rd( unit, X ), i( X ) ), ~( =( unit, mult( X, rd( unit,
% 1.60/2.00 X ) ) ) ) ] )
% 1.60/2.00 , clause( 1538, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( i( X ), rd(
% 1.60/2.00 unit, X ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1544, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( rd( unit, X )
% 1.60/2.00 , i( X ) ) ] )
% 1.60/2.00 , clause( 1543, [ =( rd( unit, X ), i( X ) ), ~( =( unit, mult( X, rd( unit
% 1.60/2.00 , X ) ) ) ) ] )
% 1.60/2.00 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 subsumption(
% 1.60/2.00 clause( 90, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( rd( unit, X ), i(
% 1.60/2.00 X ) ) ] )
% 1.60/2.00 , clause( 1544, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( rd( unit, X
% 1.60/2.00 ), i( X ) ) ] )
% 1.60/2.00 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 1.60/2.00 1 )] ) ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 eqswap(
% 1.60/2.00 clause( 1548, [ =( i( X ), rd( unit, X ) ), ~( =( mult( i( X ), X ), unit )
% 1.60/2.00 ) ] )
% 1.60/2.00 , clause( 89, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( X ), X ), unit )
% 1.60/2.00 ) ] )
% 1.60/2.00 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1554, [ =( i( ld( X, unit ) ), X ), ~( =( mult( i( ld( X, unit ) )
% 1.60/2.00 , ld( X, unit ) ), unit ) ) ] )
% 1.60/2.00 , clause( 14, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/2.00 , 0, clause( 1548, [ =( i( X ), rd( unit, X ) ), ~( =( mult( i( X ), X ),
% 1.60/2.00 unit ) ) ] )
% 1.60/2.00 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, unit )] ), substitution( 1, [
% 1.60/2.00 :=( X, ld( X, unit ) )] )).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1557, [ ~( =( mult( i( ld( X, unit ) ), i( X ) ), unit ) ), =( i(
% 1.60/2.00 ld( X, unit ) ), X ) ] )
% 1.60/2.00 , clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/2.00 , 0, clause( 1554, [ =( i( ld( X, unit ) ), X ), ~( =( mult( i( ld( X, unit
% 1.60/2.00 ) ), ld( X, unit ) ), unit ) ) ] )
% 1.60/2.00 , 1, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.00 ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1563, [ =( i( i( X ) ), X ), ~( =( mult( i( ld( X, unit ) ), i( X )
% 1.60/2.00 ), unit ) ) ] )
% 1.60/2.00 , clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/2.00 , 0, clause( 1557, [ ~( =( mult( i( ld( X, unit ) ), i( X ) ), unit ) ),
% 1.60/2.00 =( i( ld( X, unit ) ), X ) ] )
% 1.60/2.00 , 1, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.00 ).
% 1.60/2.00
% 1.60/2.00
% 1.60/2.00 paramod(
% 1.60/2.00 clause( 1564, [ ~( =( mult( i( i( X ) ), i( X ) ), unit ) ), =( i( i( X ) )
% 1.60/2.00 , X ) ] )
% 1.60/2.00 , clause( 8, [ =( ld( X, unit ), i( X ) ) ] )
% 1.60/2.00 , 0, clause( 1563, [ =( i( i( X ) ), X ), ~( =( mult( i( ld( X, unit ) ), i(
% 1.60/2.01 X ) ), unit ) ) ] )
% 1.60/2.01 , 1, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.01 ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 91, [ =( i( i( X ) ), X ), ~( =( mult( i( i( X ) ), i( X ) ), unit
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1564, [ ~( =( mult( i( i( X ) ), i( X ) ), unit ) ), =( i( i( X )
% 1.60/2.01 ), X ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 1.60/2.01 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1574, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( rd( unit, X )
% 1.60/2.01 , i( X ) ) ] )
% 1.60/2.01 , clause( 90, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( rd( unit, X )
% 1.60/2.01 , i( X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1577, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.01 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1578, [ =( unit, mult( i( X ), X ) ), ~( =( unit, mult( X, rd( unit
% 1.60/2.01 , X ) ) ) ) ] )
% 1.60/2.01 , clause( 1574, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( rd( unit, X
% 1.60/2.01 ), i( X ) ) ] )
% 1.60/2.01 , 1, clause( 1577, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.01 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, unit )
% 1.60/2.01 , :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1624, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( unit, mult( i(
% 1.60/2.01 X ), X ) ) ] )
% 1.60/2.01 , clause( 1578, [ =( unit, mult( i( X ), X ) ), ~( =( unit, mult( X, rd(
% 1.60/2.01 unit, X ) ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1625, [ =( mult( i( X ), X ), unit ), ~( =( mult( X, rd( unit, X )
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , clause( 1624, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( unit, mult(
% 1.60/2.01 i( X ), X ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 95, [ =( mult( i( X ), X ), unit ), ~( =( mult( X, rd( unit, X ) )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 1625, [ =( mult( i( X ), X ), unit ), ~( =( mult( X, rd( unit, X
% 1.60/2.01 ) ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 1.60/2.01 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1627, [ ~( =( unit, mult( i( i( X ) ), i( X ) ) ) ), =( i( i( X ) )
% 1.60/2.01 , X ) ] )
% 1.60/2.01 , clause( 91, [ =( i( i( X ) ), X ), ~( =( mult( i( i( X ) ), i( X ) ),
% 1.60/2.01 unit ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1629, [ =( X, rd( unit, i( X ) ) ) ] )
% 1.60/2.01 , clause( 18, [ =( rd( unit, i( X ) ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1630, [ =( i( X ), rd( unit, X ) ), ~( =( unit, mult( i( i( X ) ),
% 1.60/2.01 i( X ) ) ) ) ] )
% 1.60/2.01 , clause( 1627, [ ~( =( unit, mult( i( i( X ) ), i( X ) ) ) ), =( i( i( X )
% 1.60/2.01 ), X ) ] )
% 1.60/2.01 , 1, clause( 1629, [ =( X, rd( unit, i( X ) ) ) ] )
% 1.60/2.01 , 0, 5, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, i( X )
% 1.60/2.01 )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1676, [ ~( =( mult( i( i( X ) ), i( X ) ), unit ) ), =( i( X ), rd(
% 1.60/2.01 unit, X ) ) ] )
% 1.60/2.01 , clause( 1630, [ =( i( X ), rd( unit, X ) ), ~( =( unit, mult( i( i( X ) )
% 1.60/2.01 , i( X ) ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1677, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( i( X ) ), i( X )
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , clause( 1676, [ ~( =( mult( i( i( X ) ), i( X ) ), unit ) ), =( i( X ),
% 1.60/2.01 rd( unit, X ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 101, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( i( X ) ), i( X )
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , clause( 1677, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( i( X ) ), i( X
% 1.60/2.01 ) ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 1.60/2.01 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1679, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( mult( Y, X ), i(
% 1.60/2.01 X ) ), Y ) ] )
% 1.60/2.01 , clause( 87, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X ), i(
% 1.60/2.01 X ) ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1682, [ =( mult( X, i( Y ) ), rd( X, Y ) ), ~( =( unit, mult( i( Y
% 1.60/2.01 ), Y ) ) ) ] )
% 1.60/2.01 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, clause( 1679, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( mult( Y, X
% 1.60/2.01 ), i( X ) ), Y ) ] )
% 1.60/2.01 , 1, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, Y ), :=( Y, rd( X, Y ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1684, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( Y, i( X ) ), rd(
% 1.60/2.01 Y, X ) ) ] )
% 1.60/2.01 , clause( 1682, [ =( mult( X, i( Y ) ), rd( X, Y ) ), ~( =( unit, mult( i(
% 1.60/2.01 Y ), Y ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 104, [ ~( =( mult( i( Y ), Y ), unit ) ), =( mult( X, i( Y ) ), rd(
% 1.60/2.01 X, Y ) ) ] )
% 1.60/2.01 , clause( 1684, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( Y, i( X ) ),
% 1.60/2.01 rd( Y, X ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1686, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( mult( Y, X ), i(
% 1.60/2.01 X ) ), Y ) ] )
% 1.60/2.01 , clause( 87, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X ), i(
% 1.60/2.01 X ) ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1689, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.01 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1690, [ =( i( X ), ld( mult( Y, X ), Y ) ), ~( =( unit, mult( i( X
% 1.60/2.01 ), X ) ) ) ] )
% 1.60/2.01 , clause( 1686, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( mult( Y, X )
% 1.60/2.01 , i( X ) ), Y ) ] )
% 1.60/2.01 , 1, clause( 1689, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.01 , 0, 7, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, mult( Y, X ) ), :=( Y, i( X ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1692, [ ~( =( mult( i( X ), X ), unit ) ), =( i( X ), ld( mult( Y,
% 1.60/2.01 X ), Y ) ) ] )
% 1.60/2.01 , clause( 1690, [ =( i( X ), ld( mult( Y, X ), Y ) ), ~( =( unit, mult( i(
% 1.60/2.01 X ), X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1693, [ =( ld( mult( Y, X ), Y ), i( X ) ), ~( =( mult( i( X ), X )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 1692, [ ~( =( mult( i( X ), X ), unit ) ), =( i( X ), ld( mult( Y
% 1.60/2.01 , X ), Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 105, [ =( ld( mult( X, Y ), X ), i( Y ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 1693, [ =( ld( mult( Y, X ), Y ), i( X ) ), ~( =( mult( i( X ), X
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1694, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( mult( Y, X ), i(
% 1.60/2.01 X ) ), Y ) ] )
% 1.60/2.01 , clause( 87, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( mult( Y, X ), i(
% 1.60/2.01 X ) ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1697, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.01 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1698, [ =( mult( X, Y ), rd( X, i( Y ) ) ), ~( =( unit, mult( i( Y
% 1.60/2.01 ), Y ) ) ) ] )
% 1.60/2.01 , clause( 1694, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( mult( Y, X )
% 1.60/2.01 , i( X ) ), Y ) ] )
% 1.60/2.01 , 1, clause( 1697, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.01 , 0, 5, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.01 :=( X, mult( X, Y ) ), :=( Y, i( Y ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1700, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( Y, X ), rd( Y,
% 1.60/2.01 i( X ) ) ) ] )
% 1.60/2.01 , clause( 1698, [ =( mult( X, Y ), rd( X, i( Y ) ) ), ~( =( unit, mult( i(
% 1.60/2.01 Y ), Y ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1701, [ =( rd( X, i( Y ) ), mult( X, Y ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 1700, [ ~( =( mult( i( X ), X ), unit ) ), =( mult( Y, X ), rd( Y
% 1.60/2.01 , i( X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 106, [ =( rd( X, i( Y ) ), mult( X, Y ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 1701, [ =( rd( X, i( Y ) ), mult( X, Y ) ), ~( =( mult( i( Y ), Y
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1702, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( Y, i( X ) ), rd(
% 1.60/2.01 Y, X ) ) ] )
% 1.60/2.01 , clause( 104, [ ~( =( mult( i( Y ), Y ), unit ) ), =( mult( X, i( Y ) ),
% 1.60/2.01 rd( X, Y ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1705, [ ~( =( i( mult( a, b ) ), mult( i( b ), i( a ) ) ) ) ] )
% 1.60/2.01 , clause( 9, [ ~( =( mult( i( b ), i( a ) ), i( mult( a, b ) ) ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1706, [ ~( =( i( mult( a, b ) ), rd( i( b ), a ) ) ), ~( =( unit,
% 1.60/2.01 mult( i( a ), a ) ) ) ] )
% 1.60/2.01 , clause( 1702, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( Y, i( X ) ),
% 1.60/2.01 rd( Y, X ) ) ] )
% 1.60/2.01 , 1, clause( 1705, [ ~( =( i( mult( a, b ) ), mult( i( b ), i( a ) ) ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , 0, 6, substitution( 0, [ :=( X, a ), :=( Y, i( b ) )] ), substitution( 1
% 1.60/2.01 , [] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1708, [ ~( =( mult( i( a ), a ), unit ) ), ~( =( i( mult( a, b ) )
% 1.60/2.01 , rd( i( b ), a ) ) ) ] )
% 1.60/2.01 , clause( 1706, [ ~( =( i( mult( a, b ) ), rd( i( b ), a ) ) ), ~( =( unit
% 1.60/2.01 , mult( i( a ), a ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1709, [ ~( =( rd( i( b ), a ), i( mult( a, b ) ) ) ), ~( =( mult( i(
% 1.60/2.01 a ), a ), unit ) ) ] )
% 1.60/2.01 , clause( 1708, [ ~( =( mult( i( a ), a ), unit ) ), ~( =( i( mult( a, b )
% 1.60/2.01 ), rd( i( b ), a ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 112, [ ~( =( rd( i( b ), a ), i( mult( a, b ) ) ) ), ~( =( mult( i(
% 1.60/2.01 a ), a ), unit ) ) ] )
% 1.60/2.01 , clause( 1709, [ ~( =( rd( i( b ), a ), i( mult( a, b ) ) ) ), ~( =( mult(
% 1.60/2.01 i( a ), a ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 1.60/2.01 ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1710, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( Y, i( X ) ), rd(
% 1.60/2.01 Y, X ) ) ] )
% 1.60/2.01 , clause( 104, [ ~( =( mult( i( Y ), Y ), unit ) ), =( mult( X, i( Y ) ),
% 1.60/2.01 rd( X, Y ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1713, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.01 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1714, [ =( i( X ), ld( Y, rd( Y, X ) ) ), ~( =( unit, mult( i( X )
% 1.60/2.01 , X ) ) ) ] )
% 1.60/2.01 , clause( 1710, [ ~( =( unit, mult( i( X ), X ) ) ), =( mult( Y, i( X ) ),
% 1.60/2.01 rd( Y, X ) ) ] )
% 1.60/2.01 , 1, clause( 1713, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.01 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, Y ), :=( Y, i( X ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1716, [ ~( =( mult( i( X ), X ), unit ) ), =( i( X ), ld( Y, rd( Y
% 1.60/2.01 , X ) ) ) ] )
% 1.60/2.01 , clause( 1714, [ =( i( X ), ld( Y, rd( Y, X ) ) ), ~( =( unit, mult( i( X
% 1.60/2.01 ), X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1717, [ =( ld( Y, rd( Y, X ) ), i( X ) ), ~( =( mult( i( X ), X ),
% 1.60/2.01 unit ) ) ] )
% 1.60/2.01 , clause( 1716, [ ~( =( mult( i( X ), X ), unit ) ), =( i( X ), ld( Y, rd(
% 1.60/2.01 Y, X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 113, [ =( ld( X, rd( X, Y ) ), i( Y ) ), ~( =( mult( i( Y ), Y ),
% 1.60/2.01 unit ) ) ] )
% 1.60/2.01 , clause( 1717, [ =( ld( Y, rd( Y, X ) ), i( X ) ), ~( =( mult( i( X ), X )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1718, [ =( i( Y ), ld( X, rd( X, Y ) ) ), ~( =( mult( i( Y ), Y ),
% 1.60/2.01 unit ) ) ] )
% 1.60/2.01 , clause( 113, [ =( ld( X, rd( X, Y ) ), i( Y ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1722, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( mult( i( X ),
% 1.60/2.01 X ), unit ) ] )
% 1.60/2.01 , clause( 95, [ =( mult( i( X ), X ), unit ), ~( =( mult( X, rd( unit, X )
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 resolution(
% 1.60/2.01 clause( 1724, [ =( i( X ), ld( Y, rd( Y, X ) ) ), ~( =( unit, mult( X, rd(
% 1.60/2.01 unit, X ) ) ) ) ] )
% 1.60/2.01 , clause( 1718, [ =( i( Y ), ld( X, rd( X, Y ) ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , 1, clause( 1722, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( mult( i(
% 1.60/2.01 X ), X ), unit ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [ :=( X
% 1.60/2.01 , X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1726, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( i( X ), ld( Y
% 1.60/2.01 , rd( Y, X ) ) ) ] )
% 1.60/2.01 , clause( 1724, [ =( i( X ), ld( Y, rd( Y, X ) ) ), ~( =( unit, mult( X, rd(
% 1.60/2.01 unit, X ) ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1727, [ =( ld( Y, rd( Y, X ) ), i( X ) ), ~( =( mult( X, rd( unit,
% 1.60/2.01 X ) ), unit ) ) ] )
% 1.60/2.01 , clause( 1726, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( i( X ), ld(
% 1.60/2.01 Y, rd( Y, X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 114, [ =( ld( X, rd( X, Y ) ), i( Y ) ), ~( =( mult( Y, rd( unit, Y
% 1.60/2.01 ) ), unit ) ) ] )
% 1.60/2.01 , clause( 1727, [ =( ld( Y, rd( Y, X ) ), i( X ) ), ~( =( mult( X, rd( unit
% 1.60/2.01 , X ) ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1728, [ =( i( Y ), ld( mult( X, Y ), X ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 105, [ =( ld( mult( X, Y ), X ), i( Y ) ), ~( =( mult( i( Y ), Y
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1732, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( mult( i( X ),
% 1.60/2.01 X ), unit ) ] )
% 1.60/2.01 , clause( 95, [ =( mult( i( X ), X ), unit ), ~( =( mult( X, rd( unit, X )
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 resolution(
% 1.60/2.01 clause( 1734, [ =( i( X ), ld( mult( Y, X ), Y ) ), ~( =( unit, mult( X, rd(
% 1.60/2.01 unit, X ) ) ) ) ] )
% 1.60/2.01 , clause( 1728, [ =( i( Y ), ld( mult( X, Y ), X ) ), ~( =( mult( i( Y ), Y
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , 1, clause( 1732, [ ~( =( unit, mult( X, rd( unit, X ) ) ) ), =( mult( i(
% 1.60/2.01 X ), X ), unit ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [ :=( X
% 1.60/2.01 , X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1736, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( i( X ), ld(
% 1.60/2.01 mult( Y, X ), Y ) ) ] )
% 1.60/2.01 , clause( 1734, [ =( i( X ), ld( mult( Y, X ), Y ) ), ~( =( unit, mult( X,
% 1.60/2.01 rd( unit, X ) ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1737, [ =( ld( mult( Y, X ), Y ), i( X ) ), ~( =( mult( X, rd( unit
% 1.60/2.01 , X ) ), unit ) ) ] )
% 1.60/2.01 , clause( 1736, [ ~( =( mult( X, rd( unit, X ) ), unit ) ), =( i( X ), ld(
% 1.60/2.01 mult( Y, X ), Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 115, [ =( ld( mult( X, Y ), X ), i( Y ) ), ~( =( mult( Y, rd( unit
% 1.60/2.01 , Y ) ), unit ) ) ] )
% 1.60/2.01 , clause( 1737, [ =( ld( mult( Y, X ), Y ), i( X ) ), ~( =( mult( X, rd(
% 1.60/2.01 unit, X ) ), unit ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1739, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( mult( X, rd( Y, X )
% 1.60/2.01 ), Y ) ] )
% 1.60/2.01 , clause( 78, [ =( mult( Y, rd( X, Y ) ), X ), ~( =( mult( Y, rd( X, Y ) )
% 1.60/2.01 , X ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1741, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.01 , clause( 1, [ =( ld( X, mult( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1742, [ =( rd( X, Y ), ld( Y, X ) ), ~( =( X, mult( Y, rd( X, Y ) )
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1739, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( mult( X, rd( Y, X
% 1.60/2.01 ) ), Y ) ] )
% 1.60/2.01 , 1, clause( 1741, [ =( Y, ld( X, mult( X, Y ) ) ) ] )
% 1.60/2.01 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.01 :=( X, Y ), :=( Y, rd( X, Y ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1784, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( rd( X, Y ), ld( Y, X
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1742, [ =( rd( X, Y ), ld( Y, X ) ), ~( =( X, mult( Y, rd( X, Y )
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 120, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( mult( X, rd( Y, X ) ), Y
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1784, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( rd( X, Y ), ld( Y
% 1.60/2.01 , X ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 1.60/2.01 ), ==>( 1, 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1787, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( rd( Y, X ), ld( X, Y
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 120, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( mult( X, rd( Y, X ) ),
% 1.60/2.01 Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1789, [ =( Y, ld( rd( X, Y ), X ) ) ] )
% 1.60/2.01 , clause( 20, [ =( ld( rd( X, Y ), X ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1798, [ =( X, ld( ld( X, Y ), Y ) ), ~( =( Y, mult( X, rd( Y, X ) )
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1787, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( rd( Y, X ), ld( X
% 1.60/2.01 , Y ) ) ] )
% 1.60/2.01 , 1, clause( 1789, [ =( Y, ld( rd( X, Y ), X ) ) ] )
% 1.60/2.01 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1844, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( Y, ld( ld( Y, X ), X
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1798, [ =( X, ld( ld( X, Y ), Y ) ), ~( =( Y, mult( X, rd( Y, X )
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1845, [ =( ld( ld( X, Y ), Y ), X ), ~( =( mult( X, rd( Y, X ) ), Y
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1844, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( Y, ld( ld( Y, X )
% 1.60/2.01 , X ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 121, [ =( ld( ld( Y, X ), X ), Y ), ~( =( mult( Y, rd( X, Y ) ), X
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1845, [ =( ld( ld( X, Y ), Y ), X ), ~( =( mult( X, rd( Y, X ) )
% 1.60/2.01 , Y ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1847, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( rd( Y, X ), ld( X, Y
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 120, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( mult( X, rd( Y, X ) ),
% 1.60/2.01 Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1849, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.01 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1850, [ =( X, mult( ld( Y, X ), Y ) ), ~( =( X, mult( Y, rd( X, Y )
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , clause( 1847, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( rd( Y, X ), ld( X
% 1.60/2.01 , Y ) ) ] )
% 1.60/2.01 , 1, clause( 1849, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.01 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.01 :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1896, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( X, mult( ld( Y, X )
% 1.60/2.01 , Y ) ) ] )
% 1.60/2.01 , clause( 1850, [ =( X, mult( ld( Y, X ), Y ) ), ~( =( X, mult( Y, rd( X, Y
% 1.60/2.01 ) ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1897, [ =( mult( ld( Y, X ), Y ), X ), ~( =( mult( Y, rd( X, Y ) )
% 1.60/2.01 , X ) ) ] )
% 1.60/2.01 , clause( 1896, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( X, mult( ld( Y, X
% 1.60/2.01 ), Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 122, [ =( mult( ld( Y, X ), Y ), X ), ~( =( mult( Y, rd( X, Y ) ),
% 1.60/2.01 X ) ) ] )
% 1.60/2.01 , clause( 1897, [ =( mult( ld( Y, X ), Y ), X ), ~( =( mult( Y, rd( X, Y )
% 1.60/2.01 ), X ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1898, [ =( X, mult( mult( X, Y ), i( Y ) ) ), =( mult( mult( X, i(
% 1.60/2.01 Y ) ), Y ), X ) ] )
% 1.60/2.01 , clause( 27, [ =( mult( mult( Y, X ), i( X ) ), Y ), =( mult( mult( Y, i(
% 1.60/2.01 X ) ), X ), Y ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1901, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.01 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1902, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( X, mult( mult( X, Y
% 1.60/2.01 ), i( Y ) ) ) ] )
% 1.60/2.01 , clause( 1898, [ =( X, mult( mult( X, Y ), i( Y ) ) ), =( mult( mult( X, i(
% 1.60/2.01 Y ) ), Y ), X ) ] )
% 1.60/2.01 , 1, clause( 1901, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.01 , 0, 6, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, mult( X, i( Y ) ) ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1904, [ =( mult( mult( X, Y ), i( Y ) ), X ), =( mult( X, i( Y ) )
% 1.60/2.01 , rd( X, Y ) ) ] )
% 1.60/2.01 , clause( 1902, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( X, mult( mult( X,
% 1.60/2.01 Y ), i( Y ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 128, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( mult( mult( X, Y ), i(
% 1.60/2.01 Y ) ), X ) ] )
% 1.60/2.01 , clause( 1904, [ =( mult( mult( X, Y ), i( Y ) ), X ), =( mult( X, i( Y )
% 1.60/2.01 ), rd( X, Y ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 1
% 1.60/2.01 ), ==>( 1, 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1907, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.01 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1910, [ =( mult( X, i( Y ) ), mult( rd( X, i( Y ) ), ld( Y, i( Y )
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , clause( 75, [ =( rd( mult( Y, i( X ) ), ld( X, i( X ) ) ), rd( Y, i( X )
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , 0, clause( 1907, [ =( X, mult( rd( X, Y ), Y ) ) ] )
% 1.60/2.01 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 1.60/2.01 :=( X, mult( X, i( Y ) ) ), :=( Y, ld( Y, i( Y ) ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1911, [ =( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), mult( X, i( Y
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , clause( 1910, [ =( mult( X, i( Y ) ), mult( rd( X, i( Y ) ), ld( Y, i( Y
% 1.60/2.01 ) ) ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 133, [ =( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), mult( X, i( Y )
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 1911, [ =( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), mult( X, i(
% 1.60/2.01 Y ) ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1912, [ =( rd( X, Y ), mult( X, i( Y ) ) ), =( mult( mult( X, Y ),
% 1.60/2.01 i( Y ) ), X ) ] )
% 1.60/2.01 , clause( 128, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( mult( mult( X, Y )
% 1.60/2.01 , i( Y ) ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1915, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.01 , clause( 3, [ =( rd( mult( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1916, [ =( mult( X, Y ), rd( X, i( Y ) ) ), =( rd( X, Y ), mult( X
% 1.60/2.01 , i( Y ) ) ) ] )
% 1.60/2.01 , clause( 1912, [ =( rd( X, Y ), mult( X, i( Y ) ) ), =( mult( mult( X, Y )
% 1.60/2.01 , i( Y ) ), X ) ] )
% 1.60/2.01 , 1, clause( 1915, [ =( X, rd( mult( X, Y ), Y ) ) ] )
% 1.60/2.01 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, mult( X, Y ) ), :=( Y, i( Y ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1918, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( mult( X, Y ), rd( X
% 1.60/2.01 , i( Y ) ) ) ] )
% 1.60/2.01 , clause( 1916, [ =( mult( X, Y ), rd( X, i( Y ) ) ), =( rd( X, Y ), mult(
% 1.60/2.01 X, i( Y ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1919, [ =( rd( X, i( Y ) ), mult( X, Y ) ), =( mult( X, i( Y ) ),
% 1.60/2.01 rd( X, Y ) ) ] )
% 1.60/2.01 , clause( 1918, [ =( mult( X, i( Y ) ), rd( X, Y ) ), =( mult( X, Y ), rd(
% 1.60/2.01 X, i( Y ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 176, [ =( rd( X, i( Y ) ), mult( X, Y ) ), =( mult( X, i( Y ) ), rd(
% 1.60/2.01 X, Y ) ) ] )
% 1.60/2.01 , clause( 1919, [ =( rd( X, i( Y ) ), mult( X, Y ) ), =( mult( X, i( Y ) )
% 1.60/2.01 , rd( X, Y ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1920, [ =( mult( X, Y ), rd( X, i( Y ) ) ), =( mult( X, i( Y ) ),
% 1.60/2.01 rd( X, Y ) ) ] )
% 1.60/2.01 , clause( 176, [ =( rd( X, i( Y ) ), mult( X, Y ) ), =( mult( X, i( Y ) ),
% 1.60/2.01 rd( X, Y ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1923, [ =( ld( X, i( X ) ), mult( i( X ), i( X ) ) ) ] )
% 1.60/2.01 , clause( 56, [ =( mult( i( X ), i( X ) ), ld( X, i( X ) ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1925, [ =( ld( X, i( X ) ), rd( i( X ), X ) ), =( mult( i( X ), X )
% 1.60/2.01 , rd( i( X ), i( X ) ) ) ] )
% 1.60/2.01 , clause( 1920, [ =( mult( X, Y ), rd( X, i( Y ) ) ), =( mult( X, i( Y ) )
% 1.60/2.01 , rd( X, Y ) ) ] )
% 1.60/2.01 , 1, clause( 1923, [ =( ld( X, i( X ) ), mult( i( X ), i( X ) ) ) ] )
% 1.60/2.01 , 0, 5, substitution( 0, [ :=( X, i( X ) ), :=( Y, X )] ), substitution( 1
% 1.60/2.01 , [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1926, [ =( mult( i( X ), X ), unit ), =( ld( X, i( X ) ), rd( i( X
% 1.60/2.01 ), X ) ) ] )
% 1.60/2.01 , clause( 13, [ =( rd( X, X ), unit ) ] )
% 1.60/2.01 , 0, clause( 1925, [ =( ld( X, i( X ) ), rd( i( X ), X ) ), =( mult( i( X )
% 1.60/2.01 , X ), rd( i( X ), i( X ) ) ) ] )
% 1.60/2.01 , 1, 5, substitution( 0, [ :=( X, i( X ) )] ), substitution( 1, [ :=( X, X
% 1.60/2.01 )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1928, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( mult( i( X ), X )
% 1.60/2.01 , unit ) ] )
% 1.60/2.01 , clause( 1926, [ =( mult( i( X ), X ), unit ), =( ld( X, i( X ) ), rd( i(
% 1.60/2.01 X ), X ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 184, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( mult( i( X ), X )
% 1.60/2.01 , unit ) ] )
% 1.60/2.01 , clause( 1928, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( mult( i( X ), X
% 1.60/2.01 ), unit ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 1.60/2.01 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1930, [ =( ld( X, i( X ) ), rd( i( X ), X ) ), =( mult( i( X ), X )
% 1.60/2.01 , unit ) ] )
% 1.60/2.01 , clause( 184, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( mult( i( X ), X
% 1.60/2.01 ), unit ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1934, [ =( X, i( i( X ) ) ), ~( =( mult( i( X ), X ), unit ) ) ] )
% 1.60/2.01 , clause( 88, [ ~( =( mult( i( X ), X ), unit ) ), =( i( i( X ) ), X ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 resolution(
% 1.60/2.01 clause( 1936, [ =( X, i( i( X ) ) ), =( ld( X, i( X ) ), rd( i( X ), X ) )
% 1.60/2.01 ] )
% 1.60/2.01 , clause( 1934, [ =( X, i( i( X ) ) ), ~( =( mult( i( X ), X ), unit ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , 1, clause( 1930, [ =( ld( X, i( X ) ), rd( i( X ), X ) ), =( mult( i( X )
% 1.60/2.01 , X ), unit ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.01 ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1938, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( X, i( i( X ) ) )
% 1.60/2.01 ] )
% 1.60/2.01 , clause( 1936, [ =( X, i( i( X ) ) ), =( ld( X, i( X ) ), rd( i( X ), X )
% 1.60/2.01 ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1939, [ =( i( i( X ) ), X ), =( rd( i( X ), X ), ld( X, i( X ) ) )
% 1.60/2.01 ] )
% 1.60/2.01 , clause( 1938, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( X, i( i( X ) )
% 1.60/2.01 ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 186, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( i( i( X ) ), X ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 1939, [ =( i( i( X ) ), X ), =( rd( i( X ), X ), ld( X, i( X ) )
% 1.60/2.01 ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 1.60/2.01 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1941, [ =( X, i( i( X ) ) ), =( rd( i( X ), X ), ld( X, i( X ) ) )
% 1.60/2.01 ] )
% 1.60/2.01 , clause( 186, [ =( rd( i( X ), X ), ld( X, i( X ) ) ), =( i( i( X ) ), X )
% 1.60/2.01 ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1943, [ =( Y, mult( ld( X, Y ), X ) ), ~( =( mult( X, rd( Y, X ) )
% 1.60/2.01 , Y ) ) ] )
% 1.60/2.01 , clause( 122, [ =( mult( ld( Y, X ), Y ), X ), ~( =( mult( Y, rd( X, Y ) )
% 1.60/2.01 , X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1947, [ ~( =( mult( X, ld( X, i( X ) ) ), i( X ) ) ), =( X, i( i( X
% 1.60/2.01 ) ) ), =( i( X ), mult( ld( X, i( X ) ), X ) ) ] )
% 1.60/2.01 , clause( 1941, [ =( X, i( i( X ) ) ), =( rd( i( X ), X ), ld( X, i( X ) )
% 1.60/2.01 ) ] )
% 1.60/2.01 , 1, clause( 1943, [ =( Y, mult( ld( X, Y ), X ) ), ~( =( mult( X, rd( Y, X
% 1.60/2.01 ) ), Y ) ) ] )
% 1.60/2.01 , 1, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.01 :=( Y, i( X ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1948, [ ~( =( i( X ), i( X ) ) ), =( X, i( i( X ) ) ), =( i( X ),
% 1.60/2.01 mult( ld( X, i( X ) ), X ) ) ] )
% 1.60/2.01 , clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, clause( 1947, [ ~( =( mult( X, ld( X, i( X ) ) ), i( X ) ) ), =( X, i(
% 1.60/2.01 i( X ) ) ), =( i( X ), mult( ld( X, i( X ) ), X ) ) ] )
% 1.60/2.01 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, i( X ) )] ), substitution( 1
% 1.60/2.01 , [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqrefl(
% 1.60/2.01 clause( 1949, [ =( X, i( i( X ) ) ), =( i( X ), mult( ld( X, i( X ) ), X )
% 1.60/2.01 ) ] )
% 1.60/2.01 , clause( 1948, [ ~( =( i( X ), i( X ) ) ), =( X, i( i( X ) ) ), =( i( X )
% 1.60/2.01 , mult( ld( X, i( X ) ), X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1951, [ =( mult( ld( X, i( X ) ), X ), i( X ) ), =( X, i( i( X ) )
% 1.60/2.01 ) ] )
% 1.60/2.01 , clause( 1949, [ =( X, i( i( X ) ) ), =( i( X ), mult( ld( X, i( X ) ), X
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1952, [ =( i( i( X ) ), X ), =( mult( ld( X, i( X ) ), X ), i( X )
% 1.60/2.01 ) ] )
% 1.60/2.01 , clause( 1951, [ =( mult( ld( X, i( X ) ), X ), i( X ) ), =( X, i( i( X )
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 190, [ =( mult( ld( X, i( X ) ), X ), i( X ) ), =( i( i( X ) ), X )
% 1.60/2.01 ] )
% 1.60/2.01 , clause( 1952, [ =( i( i( X ) ), X ), =( mult( ld( X, i( X ) ), X ), i( X
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 1.60/2.01 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1954, [ =( X, i( i( X ) ) ), =( mult( ld( X, i( X ) ), X ), i( X )
% 1.60/2.01 ) ] )
% 1.60/2.01 , clause( 190, [ =( mult( ld( X, i( X ) ), X ), i( X ) ), =( i( i( X ) ), X
% 1.60/2.01 ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1956, [ =( X, mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ) ), =(
% 1.60/2.01 mult( rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult( Y,
% 1.60/2.01 Z ) ), Z ), Y ) ) ] )
% 1.60/2.01 , clause( 47, [ =( mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ), X ), =(
% 1.60/2.01 mult( rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult( Y,
% 1.60/2.01 Z ) ), Z ), Y ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1965, [ ~( =( X, mult( mult( X, i( Y ) ), Y ) ) ), =( mult( mult( X
% 1.60/2.01 , i( Y ) ), Y ), X ) ] )
% 1.60/2.01 , clause( 65, [ =( mult( mult( Y, i( X ) ), X ), Y ), ~( =( mult( mult( Y,
% 1.60/2.01 i( X ) ), X ), Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 1966, [ =( X, mult( mult( X, i( Y ) ), Y ) ), ~( =( X, mult( mult(
% 1.60/2.01 X, i( Y ) ), Y ) ) ) ] )
% 1.60/2.01 , clause( 1965, [ ~( =( X, mult( mult( X, i( Y ) ), Y ) ) ), =( mult( mult(
% 1.60/2.01 X, i( Y ) ), Y ), X ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1970, [ =( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), i( Y ) ),
% 1.60/2.01 mult( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), ld( Y, i( Y ) ) ), Y ) )
% 1.60/2.01 , =( Y, i( i( Y ) ) ), =( X, mult( mult( rd( X, mult( Y, ld( Y, i( Y ) )
% 1.60/2.01 ) ), ld( Y, i( Y ) ) ), Y ) ) ] )
% 1.60/2.01 , clause( 1954, [ =( X, i( i( X ) ) ), =( mult( ld( X, i( X ) ), X ), i( X
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , 1, clause( 1956, [ =( X, mult( mult( rd( X, mult( Y, Z ) ), Z ), Y ) ),
% 1.60/2.01 =( mult( rd( X, mult( Y, Z ) ), mult( Z, Y ) ), mult( mult( rd( X, mult(
% 1.60/2.01 Y, Z ) ), Z ), Y ) ) ] )
% 1.60/2.01 , 1, 10, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.01 :=( Y, Y ), :=( Z, ld( Y, i( Y ) ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1982, [ =( X, mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) )
% 1.60/2.01 , =( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), i( Y ) ), mult( mult( rd(
% 1.60/2.01 X, mult( Y, ld( Y, i( Y ) ) ) ), ld( Y, i( Y ) ) ), Y ) ), =( Y, i( i( Y
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, clause( 1970, [ =( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), i( Y ) )
% 1.60/2.01 , mult( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), ld( Y, i( Y ) ) ), Y )
% 1.60/2.01 ), =( Y, i( i( Y ) ) ), =( X, mult( mult( rd( X, mult( Y, ld( Y, i( Y )
% 1.60/2.01 ) ) ), ld( Y, i( Y ) ) ), Y ) ) ] )
% 1.60/2.01 , 2, 6, substitution( 0, [ :=( X, Y ), :=( Y, i( Y ) )] ), substitution( 1
% 1.60/2.01 , [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1988, [ =( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), i( Y ) ),
% 1.60/2.01 mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) ), =( X, mult( mult(
% 1.60/2.01 rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, clause( 1982, [ =( X, mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ),
% 1.60/2.01 Y ) ), =( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), i( Y ) ), mult( mult(
% 1.60/2.01 rd( X, mult( Y, ld( Y, i( Y ) ) ) ), ld( Y, i( Y ) ) ), Y ) ), =( Y, i( i(
% 1.60/2.01 Y ) ) ) ] )
% 1.60/2.01 , 1, 16, substitution( 0, [ :=( X, Y ), :=( Y, i( Y ) )] ), substitution( 1
% 1.60/2.01 , [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1989, [ =( mult( rd( X, i( Y ) ), i( Y ) ), mult( mult( rd( X, i( Y
% 1.60/2.01 ) ), ld( Y, i( Y ) ) ), Y ) ), =( X, mult( mult( rd( X, i( Y ) ), ld( Y
% 1.60/2.01 , i( Y ) ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , clause( 0, [ =( mult( X, ld( X, Y ) ), Y ) ] )
% 1.60/2.01 , 0, clause( 1988, [ =( mult( rd( X, mult( Y, ld( Y, i( Y ) ) ) ), i( Y ) )
% 1.60/2.01 , mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) ), =( X, mult( mult(
% 1.60/2.01 rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , 0, 4, substitution( 0, [ :=( X, Y ), :=( Y, i( Y ) )] ), substitution( 1
% 1.60/2.01 , [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1994, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( mult( rd( X, i( Y
% 1.60/2.01 ) ), i( Y ) ), mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) ),
% 1.60/2.01 =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , clause( 133, [ =( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), mult( X, i( Y
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , 0, clause( 1989, [ =( mult( rd( X, i( Y ) ), i( Y ) ), mult( mult( rd( X
% 1.60/2.01 , i( Y ) ), ld( Y, i( Y ) ) ), Y ) ), =( X, mult( mult( rd( X, i( Y ) ),
% 1.60/2.01 ld( Y, i( Y ) ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , 1, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1996, [ =( X, mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) )
% 1.60/2.01 , =( X, mult( mult( X, i( Y ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , clause( 2, [ =( mult( rd( X, Y ), Y ), X ) ] )
% 1.60/2.01 , 0, clause( 1994, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( mult( rd( X,
% 1.60/2.01 i( Y ) ), i( Y ) ), mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), Y ) )
% 1.60/2.01 , =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , 1, 1, substitution( 0, [ :=( X, X ), :=( Y, i( Y ) )] ), substitution( 1
% 1.60/2.01 , [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 1997, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( X, mult( mult( X,
% 1.60/2.01 i( Y ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , clause( 133, [ =( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ), mult( X, i( Y
% 1.60/2.01 ) ) ) ] )
% 1.60/2.01 , 0, clause( 1996, [ =( X, mult( mult( rd( X, i( Y ) ), ld( Y, i( Y ) ) ),
% 1.60/2.01 Y ) ), =( X, mult( mult( X, i( Y ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 factor(
% 1.60/2.01 clause( 1998, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( Y, i( i( Y ) ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 1997, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( X, mult( mult( X
% 1.60/2.01 , i( Y ) ), Y ) ), =( Y, i( i( Y ) ) ) ] )
% 1.60/2.01 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 resolution(
% 1.60/2.01 clause( 1999, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( Y, i( i( Y ) ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 1966, [ =( X, mult( mult( X, i( Y ) ), Y ) ), ~( =( X, mult( mult(
% 1.60/2.01 X, i( Y ) ), Y ) ) ) ] )
% 1.60/2.01 , 1, clause( 1998, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( Y, i( i( Y )
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 1.60/2.01 , X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2001, [ =( i( i( X ) ), X ), =( Y, mult( mult( Y, i( X ) ), X ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 1999, [ =( X, mult( mult( X, i( Y ) ), Y ) ), =( Y, i( i( Y ) ) )
% 1.60/2.01 ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2002, [ =( mult( mult( X, i( Y ) ), Y ), X ), =( i( i( Y ) ), Y ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 2001, [ =( i( i( X ) ), X ), =( Y, mult( mult( Y, i( X ) ), X ) )
% 1.60/2.01 ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 195, [ =( i( i( X ) ), X ), =( mult( mult( Y, i( X ) ), X ), Y ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 2002, [ =( mult( mult( X, i( Y ) ), Y ), X ), =( i( i( Y ) ), Y )
% 1.60/2.01 ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 1.60/2.01 ), ==>( 1, 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2004, [ =( X, i( i( X ) ) ), =( mult( mult( Y, i( X ) ), X ), Y ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 195, [ =( i( i( X ) ), X ), =( mult( mult( Y, i( X ) ), X ), Y )
% 1.60/2.01 ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2010, [ =( mult( i( X ), X ), unit ), =( X, i( i( X ) ) ) ] )
% 1.60/2.01 , clause( 5, [ =( mult( unit, X ), X ) ] )
% 1.60/2.01 , 0, clause( 2004, [ =( X, i( i( X ) ) ), =( mult( mult( Y, i( X ) ), X ),
% 1.60/2.01 Y ) ] )
% 1.60/2.01 , 1, 2, substitution( 0, [ :=( X, i( X ) )] ), substitution( 1, [ :=( X, X
% 1.60/2.01 ), :=( Y, unit )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 resolution(
% 1.60/2.01 clause( 2013, [ =( i( i( X ) ), X ), =( X, i( i( X ) ) ) ] )
% 1.60/2.01 , clause( 88, [ ~( =( mult( i( X ), X ), unit ) ), =( i( i( X ) ), X ) ] )
% 1.60/2.01 , 0, clause( 2010, [ =( mult( i( X ), X ), unit ), =( X, i( i( X ) ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.01 ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2015, [ =( i( i( X ) ), X ), =( i( i( X ) ), X ) ] )
% 1.60/2.01 , clause( 2013, [ =( i( i( X ) ), X ), =( X, i( i( X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 factor(
% 1.60/2.01 clause( 2017, [ =( i( i( X ) ), X ) ] )
% 1.60/2.01 , clause( 2015, [ =( i( i( X ) ), X ), =( i( i( X ) ), X ) ] )
% 1.60/2.01 , 0, 1, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 209, [ =( i( i( X ) ), X ) ] )
% 1.60/2.01 , clause( 2017, [ =( i( i( X ) ), X ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2019, [ =( i( X ), rd( unit, X ) ), ~( =( mult( i( i( X ) ), i( X )
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , clause( 101, [ =( rd( unit, X ), i( X ) ), ~( =( mult( i( i( X ) ), i( X
% 1.60/2.01 ) ), unit ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2024, [ ~( =( mult( X, i( X ) ), unit ) ), =( i( X ), rd( unit, X )
% 1.60/2.01 ) ] )
% 1.60/2.01 , clause( 209, [ =( i( i( X ) ), X ) ] )
% 1.60/2.01 , 0, clause( 2019, [ =( i( X ), rd( unit, X ) ), ~( =( mult( i( i( X ) ), i(
% 1.60/2.01 X ) ), unit ) ) ] )
% 1.60/2.01 , 1, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.01 ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2030, [ ~( =( unit, unit ) ), =( i( X ), rd( unit, X ) ) ] )
% 1.60/2.01 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.01 , 0, clause( 2024, [ ~( =( mult( X, i( X ) ), unit ) ), =( i( X ), rd( unit
% 1.60/2.01 , X ) ) ] )
% 1.60/2.01 , 0, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 1.60/2.01 ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqrefl(
% 1.60/2.01 clause( 2031, [ =( i( X ), rd( unit, X ) ) ] )
% 1.60/2.01 , clause( 2030, [ ~( =( unit, unit ) ), =( i( X ), rd( unit, X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2032, [ =( rd( unit, X ), i( X ) ) ] )
% 1.60/2.01 , clause( 2031, [ =( i( X ), rd( unit, X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 225, [ =( rd( unit, X ), i( X ) ) ] )
% 1.60/2.01 , clause( 2032, [ =( rd( unit, X ), i( X ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2034, [ =( mult( X, Y ), rd( X, i( Y ) ) ), ~( =( mult( i( Y ), Y )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 106, [ =( rd( X, i( Y ) ), mult( X, Y ) ), ~( =( mult( i( Y ), Y
% 1.60/2.01 ), unit ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2039, [ ~( =( mult( X, i( X ) ), unit ) ), =( mult( Y, i( X ) ), rd(
% 1.60/2.01 Y, i( i( X ) ) ) ) ] )
% 1.60/2.01 , clause( 209, [ =( i( i( X ) ), X ) ] )
% 1.60/2.01 , 0, clause( 2034, [ =( mult( X, Y ), rd( X, i( Y ) ) ), ~( =( mult( i( Y )
% 1.60/2.01 , Y ), unit ) ) ] )
% 1.60/2.01 , 1, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.01 :=( Y, i( X ) )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2040, [ =( mult( X, i( Y ) ), rd( X, Y ) ), ~( =( mult( Y, i( Y ) )
% 1.60/2.01 , unit ) ) ] )
% 1.60/2.01 , clause( 209, [ =( i( i( X ) ), X ) ] )
% 1.60/2.01 , 0, clause( 2039, [ ~( =( mult( X, i( X ) ), unit ) ), =( mult( Y, i( X )
% 1.60/2.01 ), rd( Y, i( i( X ) ) ) ) ] )
% 1.60/2.01 , 1, 7, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.01 :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2044, [ ~( =( unit, unit ) ), =( mult( Y, i( X ) ), rd( Y, X ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.01 , 0, clause( 2040, [ =( mult( X, i( Y ) ), rd( X, Y ) ), ~( =( mult( Y, i(
% 1.60/2.01 Y ) ), unit ) ) ] )
% 1.60/2.01 , 1, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.01 :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqrefl(
% 1.60/2.01 clause( 2045, [ =( mult( X, i( Y ) ), rd( X, Y ) ) ] )
% 1.60/2.01 , clause( 2044, [ ~( =( unit, unit ) ), =( mult( Y, i( X ) ), rd( Y, X ) )
% 1.60/2.01 ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 229, [ =( mult( Y, i( X ) ), rd( Y, X ) ) ] )
% 1.60/2.01 , clause( 2045, [ =( mult( X, i( Y ) ), rd( X, Y ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2048, [ =( i( Y ), ld( X, rd( X, Y ) ) ), ~( =( mult( Y, rd( unit,
% 1.60/2.01 Y ) ), unit ) ) ] )
% 1.60/2.01 , clause( 114, [ =( ld( X, rd( X, Y ) ), i( Y ) ), ~( =( mult( Y, rd( unit
% 1.60/2.01 , Y ) ), unit ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2053, [ ~( =( mult( X, i( X ) ), unit ) ), =( i( X ), ld( Y, rd( Y
% 1.60/2.01 , X ) ) ) ] )
% 1.60/2.01 , clause( 225, [ =( rd( unit, X ), i( X ) ) ] )
% 1.60/2.01 , 0, clause( 2048, [ =( i( Y ), ld( X, rd( X, Y ) ) ), ~( =( mult( Y, rd(
% 1.60/2.01 unit, Y ) ), unit ) ) ] )
% 1.60/2.01 , 1, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.01 :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2055, [ ~( =( unit, unit ) ), =( i( X ), ld( Y, rd( Y, X ) ) ) ] )
% 1.60/2.01 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.01 , 0, clause( 2053, [ ~( =( mult( X, i( X ) ), unit ) ), =( i( X ), ld( Y,
% 1.60/2.01 rd( Y, X ) ) ) ] )
% 1.60/2.01 , 0, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.01 :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqrefl(
% 1.60/2.01 clause( 2056, [ =( i( X ), ld( Y, rd( Y, X ) ) ) ] )
% 1.60/2.01 , clause( 2055, [ ~( =( unit, unit ) ), =( i( X ), ld( Y, rd( Y, X ) ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2057, [ =( ld( Y, rd( Y, X ) ), i( X ) ) ] )
% 1.60/2.01 , clause( 2056, [ =( i( X ), ld( Y, rd( Y, X ) ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 234, [ =( ld( Y, rd( Y, X ) ), i( X ) ) ] )
% 1.60/2.01 , clause( 2057, [ =( ld( Y, rd( Y, X ) ), i( X ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2059, [ =( i( Y ), ld( mult( X, Y ), X ) ), ~( =( mult( Y, rd( unit
% 1.60/2.01 , Y ) ), unit ) ) ] )
% 1.60/2.01 , clause( 115, [ =( ld( mult( X, Y ), X ), i( Y ) ), ~( =( mult( Y, rd(
% 1.60/2.01 unit, Y ) ), unit ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2063, [ ~( =( mult( X, i( X ) ), unit ) ), =( i( X ), ld( mult( Y,
% 1.60/2.01 X ), Y ) ) ] )
% 1.60/2.01 , clause( 225, [ =( rd( unit, X ), i( X ) ) ] )
% 1.60/2.01 , 0, clause( 2059, [ =( i( Y ), ld( mult( X, Y ), X ) ), ~( =( mult( Y, rd(
% 1.60/2.01 unit, Y ) ), unit ) ) ] )
% 1.60/2.01 , 1, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 1.60/2.01 :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2064, [ ~( =( unit, unit ) ), =( i( X ), ld( mult( Y, X ), Y ) ) ]
% 1.60/2.01 )
% 1.60/2.01 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.01 , 0, clause( 2063, [ ~( =( mult( X, i( X ) ), unit ) ), =( i( X ), ld( mult(
% 1.60/2.01 Y, X ), Y ) ) ] )
% 1.60/2.01 , 0, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 1.60/2.01 :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqrefl(
% 1.60/2.01 clause( 2065, [ =( i( X ), ld( mult( Y, X ), Y ) ) ] )
% 1.60/2.01 , clause( 2064, [ ~( =( unit, unit ) ), =( i( X ), ld( mult( Y, X ), Y ) )
% 1.60/2.01 ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2066, [ =( ld( mult( Y, X ), Y ), i( X ) ) ] )
% 1.60/2.01 , clause( 2065, [ =( i( X ), ld( mult( Y, X ), Y ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 235, [ =( ld( mult( Y, X ), Y ), i( X ) ) ] )
% 1.60/2.01 , clause( 2066, [ =( ld( mult( Y, X ), Y ), i( X ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2068, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( rd( Y, X ), ld( X, Y
% 1.60/2.01 ) ) ] )
% 1.60/2.01 , clause( 120, [ =( rd( Y, X ), ld( X, Y ) ), ~( =( mult( X, rd( Y, X ) ),
% 1.60/2.01 Y ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2070, [ =( i( Y ), ld( X, rd( X, Y ) ) ) ] )
% 1.60/2.01 , clause( 234, [ =( ld( Y, rd( Y, X ) ), i( X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2079, [ =( i( X ), ld( Y, ld( X, Y ) ) ), ~( =( Y, mult( X, rd( Y,
% 1.60/2.01 X ) ) ) ) ] )
% 1.60/2.01 , clause( 2068, [ ~( =( Y, mult( X, rd( Y, X ) ) ) ), =( rd( Y, X ), ld( X
% 1.60/2.01 , Y ) ) ] )
% 1.60/2.01 , 1, clause( 2070, [ =( i( Y ), ld( X, rd( X, Y ) ) ) ] )
% 1.60/2.01 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.01 :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2125, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( i( Y ), ld( X, ld( Y
% 1.60/2.01 , X ) ) ) ] )
% 1.60/2.01 , clause( 2079, [ =( i( X ), ld( Y, ld( X, Y ) ) ), ~( =( Y, mult( X, rd( Y
% 1.60/2.01 , X ) ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2126, [ =( ld( Y, ld( X, Y ) ), i( X ) ), ~( =( mult( X, rd( Y, X )
% 1.60/2.01 ), Y ) ) ] )
% 1.60/2.01 , clause( 2125, [ ~( =( mult( Y, rd( X, Y ) ), X ) ), =( i( Y ), ld( X, ld(
% 1.60/2.01 Y, X ) ) ) ] )
% 1.60/2.01 , 1, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 subsumption(
% 1.60/2.01 clause( 253, [ =( ld( X, ld( Y, X ) ), i( Y ) ), ~( =( mult( Y, rd( X, Y )
% 1.60/2.01 ), X ) ) ] )
% 1.60/2.01 , clause( 2126, [ =( ld( Y, ld( X, Y ) ), i( X ) ), ~( =( mult( X, rd( Y, X
% 1.60/2.01 ) ), Y ) ) ] )
% 1.60/2.01 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.01 ), ==>( 1, 1 )] ) ).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 eqswap(
% 1.60/2.01 clause( 2128, [ =( i( Y ), ld( X, rd( X, Y ) ) ) ] )
% 1.60/2.01 , clause( 234, [ =( ld( Y, rd( Y, X ) ), i( X ) ) ] )
% 1.60/2.01 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 1.60/2.01
% 1.60/2.01
% 1.60/2.01 paramod(
% 1.60/2.01 clause( 2131, [ =( i( ld( X, Y ) ), ld( Y, X ) ) ] )
% 1.60/2.01 , clause( 14, [ =( rd( Y, ld( X, Y ) ), X ) ] )
% 1.60/2.01 , 0, clause( 2128, [ =( i( Y ), ld( X, rd( X, Y ) ) ) ] )
% 1.60/2.02 , 0, 7, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.60/2.02 :=( X, Y ), :=( Y, ld( X, Y ) )] )).
% 1.60/2.02
% 1.60/2.02
% 1.60/2.02 subsumption(
% 1.60/2.02 clause( 254, [ =( i( ld( Y, X ) ), ld( X, Y ) ) ] )
% 1.60/2.02 , clause( 2131, [ =( i( ld( X, Y ) ), ld( Y, X ) ) ] )
% 1.60/2.02 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 1.60/2.02 )] ) ).
% 1.60/2.02
% 1.60/2.02
% 1.60/2.02 eqswap(
% 1.60/2.02 clause( 2134, [ =( mult( Y, Z ), ld( X, mult( mult( X, Y ), Z ) ) ), =(
% 1.60/2.02 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.02 , clause( 49, [ =( ld( X, mult( mult( X, Y ), Z ) ), mult( Y, Z ) ), =(
% 1.60/2.02 mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.02 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.60/2.02
% 1.60/2.02
% 1.60/2.02 paramod(
% 1.60/2.02 clause( 2145, [ =( mult( X, mult( Y, i( X ) ) ), mult( unit, Y ) ), =( mult(
% 1.60/2.02 i( X ), Y ), ld( X, mult( mult( X, i( X ) ), Y ) ) ) ] )
% 1.60/2.02 , clause( 15, [ =( mult( X, i( X ) ), unit ) ] )
% 1.60/2.02 , 0, clause( 2134, [ =( mult( Y, Z ), ld( X, mult( mult( X, Y ), Z ) ) ),
% 1.60/2.02 =( mult( X, mult( Z, Y ) ), mult( mult( X, Y ), Z ) ) ] )
% 1.60/2.02 , 1, 8, substitution( 0, [ :=Cputime limit exceeded (core dumped) (core dumped)
% 300.02/300.50 Bliksem ended
%------------------------------------------------------------------------------