%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP214-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sat Jul 16 07:36:09 EDT 2022
% Result : Unsatisfiable 33.88s 34.30s
% Output : Refutation 33.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : GRP214-1 : TPTP v8.1.0. Released v2.5.0.
% 0.07/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Mon Jun 13 07:56:27 EDT 2022
% 0.12/0.33 % CPUTime :
% 33.88/34.30 *** allocated 10000 integers for termspace/termends
% 33.88/34.30 *** allocated 10000 integers for clauses
% 33.88/34.30 *** allocated 10000 integers for justifications
% 33.88/34.30 Bliksem 1.12
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 Automatic Strategy Selection
% 33.88/34.30
% 33.88/34.30 Clauses:
% 33.88/34.30 [
% 33.88/34.30 [ =( multiply( identity, X ), X ) ],
% 33.88/34.30 [ =( multiply( inverse( X ), X ), identity ) ],
% 33.88/34.30 [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply( Y, Z ) ) )
% 33.88/34.30 ],
% 33.88/34.30 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 33.88/34.30 'sk_c7' ), 'sk_c5' ) ],
% 33.88/34.30 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ],
% 33.88/34.30 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ],
% 33.88/34.30 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ],
% 33.88/34.30 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3', 'sk_c7' ),
% 33.88/34.30 'sk_c5' ) ],
% 33.88/34.30 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ), 'sk_c7' ) ]
% 33.88/34.30 ,
% 33.88/34.30 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4', 'sk_c5' ),
% 33.88/34.30 'sk_c6' ) ],
% 33.88/34.30 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ), 'sk_c5' ) ]
% 33.88/34.30 ,
% 33.88/34.30 [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 33.88/34.30 'sk_c7' ), 'sk_c5' ) ],
% 33.88/34.30 [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ],
% 33.88/34.30 [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ],
% 33.88/34.30 [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ],
% 33.88/34.30 [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7'
% 33.88/34.30 ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =( multiply( Z,
% 33.88/34.30 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =( multiply( U, T )
% 33.88/34.30 , 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ]
% 33.88/34.30 ] .
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 percentage equality = 1.000000, percentage horn = 0.250000
% 33.88/34.30 This is a pure equality problem
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 Options Used:
% 33.88/34.30
% 33.88/34.30 useres = 1
% 33.88/34.30 useparamod = 1
% 33.88/34.30 useeqrefl = 1
% 33.88/34.30 useeqfact = 1
% 33.88/34.30 usefactor = 1
% 33.88/34.30 usesimpsplitting = 0
% 33.88/34.30 usesimpdemod = 5
% 33.88/34.30 usesimpres = 3
% 33.88/34.30
% 33.88/34.30 resimpinuse = 1000
% 33.88/34.30 resimpclauses = 20000
% 33.88/34.30 substype = eqrewr
% 33.88/34.30 backwardsubs = 1
% 33.88/34.30 selectoldest = 5
% 33.88/34.30
% 33.88/34.30 litorderings [0] = split
% 33.88/34.30 litorderings [1] = extend the termordering, first sorting on arguments
% 33.88/34.30
% 33.88/34.30 termordering = kbo
% 33.88/34.30
% 33.88/34.30 litapriori = 0
% 33.88/34.30 termapriori = 1
% 33.88/34.30 litaposteriori = 0
% 33.88/34.30 termaposteriori = 0
% 33.88/34.30 demodaposteriori = 0
% 33.88/34.30 ordereqreflfact = 0
% 33.88/34.30
% 33.88/34.30 litselect = negord
% 33.88/34.30
% 33.88/34.30 maxweight = 15
% 33.88/34.30 maxdepth = 30000
% 33.88/34.30 maxlength = 115
% 33.88/34.30 maxnrvars = 195
% 33.88/34.30 excuselevel = 1
% 33.88/34.30 increasemaxweight = 1
% 33.88/34.30
% 33.88/34.30 maxselected = 10000000
% 33.88/34.30 maxnrclauses = 10000000
% 33.88/34.30
% 33.88/34.30 showgenerated = 0
% 33.88/34.30 showkept = 0
% 33.88/34.30 showselected = 0
% 33.88/34.30 showdeleted = 0
% 33.88/34.30 showresimp = 1
% 33.88/34.30 showstatus = 2000
% 33.88/34.30
% 33.88/34.30 prologoutput = 1
% 33.88/34.30 nrgoals = 5000000
% 33.88/34.30 totalproof = 1
% 33.88/34.30
% 33.88/34.30 Symbols occurring in the translation:
% 33.88/34.30
% 33.88/34.30 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 33.88/34.30 . [1, 2] (w:1, o:31, a:1, s:1, b:0),
% 33.88/34.30 ! [4, 1] (w:0, o:25, a:1, s:1, b:0),
% 33.88/34.30 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 33.88/34.30 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 33.88/34.30 identity [39, 0] (w:1, o:16, a:1, s:1, b:0),
% 33.88/34.30 multiply [41, 2] (w:1, o:56, a:1, s:1, b:0),
% 33.88/34.30 inverse [42, 1] (w:1, o:30, a:1, s:1, b:0),
% 33.88/34.30 'sk_c1' [45, 0] (w:1, o:5, a:1, s:1, b:0),
% 33.88/34.30 'sk_c7' [46, 0] (w:1, o:9, a:1, s:1, b:0),
% 33.88/34.30 'sk_c6' [47, 0] (w:1, o:8, a:1, s:1, b:0),
% 33.88/34.30 'sk_c3' [48, 0] (w:1, o:11, a:1, s:1, b:0),
% 33.88/34.30 'sk_c5' [49, 0] (w:1, o:7, a:1, s:1, b:0),
% 33.88/34.30 'sk_c4' [50, 0] (w:1, o:6, a:1, s:1, b:0),
% 33.88/34.30 'sk_c2' [51, 0] (w:1, o:10, a:1, s:1, b:0).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 Starting Search:
% 33.88/34.30
% 33.88/34.30 Resimplifying inuse:
% 33.88/34.30 Done
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 Intermediate Status:
% 33.88/34.30 Generated: 117916
% 33.88/34.30 Kept: 2001
% 33.88/34.30 Inuse: 548
% 33.88/34.30 Deleted: 500
% 33.88/34.30 Deletedinuse: 108
% 33.88/34.30
% 33.88/34.30 Resimplifying inuse:
% 33.88/34.30 Done
% 33.88/34.30
% 33.88/34.30 Resimplifying inuse:
% 33.88/34.30 Done
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 Intermediate Status:
% 33.88/34.30 Generated: 387940
% 33.88/34.30 Kept: 4004
% 33.88/34.30 Inuse: 1072
% 33.88/34.30 Deleted: 679
% 33.88/34.30 Deletedinuse: 194
% 33.88/34.30
% 33.88/34.30 Resimplifying inuse:
% 33.88/34.30 Done
% 33.88/34.30
% 33.88/34.30 Resimplifying inuse:
% 33.88/34.30 Done
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 Bliksems!, er is een bewijs:
% 33.88/34.30 % SZS status Unsatisfiable
% 33.88/34.30 % SZS output start Refutation
% 33.88/34.30
% 33.88/34.30 clause( 0, [ =( multiply( identity, X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 33.88/34.30 , Z ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 3, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 4, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 5, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 6, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 7, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.88/34.30 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 9, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 10, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 11, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 12, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 13, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 14, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 15, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X )
% 33.88/34.30 , 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =( multiply(
% 33.88/34.30 Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =( multiply( U,
% 33.88/34.30 T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 20, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X )
% 33.88/34.30 , 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =( inverse(
% 33.88/34.30 Z ), 'sk_c7' ) ), ~( =( inverse( T ), multiply( Z, 'sk_c7' ) ) ), ~( =(
% 33.88/34.30 multiply( multiply( T, Z ), 'sk_c7' ), 'sk_c6' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 22, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 24, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 25, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( inverse(
% 33.88/34.30 'sk_c1' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 28, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y )
% 33.88/34.30 , identity ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 29, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y,
% 33.88/34.30 identity ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 30, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X ) )
% 33.88/34.30 ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 31, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c3' ), multiply( X,
% 33.88/34.30 identity ) ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 40, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( multiply(
% 33.88/34.30 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 42, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 44, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 49, [ =( multiply( inverse( identity ), X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 50, [ =( multiply( multiply( Y, inverse( identity ) ), X ),
% 33.88/34.30 multiply( Y, X ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 55, [ =( multiply( multiply( X, 'sk_c1' ), 'sk_c7' ), multiply( X,
% 33.88/34.30 'sk_c6' ) ), =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 73, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 122, [ =( inverse( identity ), identity ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 125, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y )
% 33.88/34.30 ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 159, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 169, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( multiply( 'sk_c7',
% 33.88/34.30 'sk_c1' ), identity ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 170, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 171, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( inverse( 'sk_c1' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 173, [ =( inverse( 'sk_c5' ), 'sk_c4' ), =( inverse( 'sk_c1' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 174, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 175, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( 'sk_c6',
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 176, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.88/34.30 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 178, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 179, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( 'sk_c6',
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 181, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 33.88/34.30 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 183, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c6',
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 184, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 185, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 186, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 187, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c6', 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 188, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 189, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( identity, 'sk_c6' ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 193, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( multiply( 'sk_c6', X )
% 33.88/34.30 , X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 194, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 196, [ =( multiply( X, 'sk_c5' ), X ), ~( =( 'sk_c6', 'sk_c5' ) ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 197, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( 'sk_c6', 'sk_c5' ) )
% 33.88/34.30 ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 198, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( multiply( 'sk_c5', X ), X ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 199, [ =( multiply( X, 'sk_c6' ), X ), =( identity, 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 200, [ =( multiply( X, 'sk_c5' ), X ), =( identity, 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 201, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( identity, 'sk_c5' ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 202, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 204, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c5', X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 218, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c5', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 221, [ =( identity, 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c1' ),
% 33.88/34.30 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 230, [ =( multiply( 'sk_c1', 'sk_c7' ), identity ), =( 'sk_c5',
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 233, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c5',
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 240, [ =( identity, 'sk_c6' ), =( 'sk_c5', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 242, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c4', X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 243, [ =( identity, 'sk_c6' ), =( multiply( X, 'sk_c4' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 244, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 247, [ =( multiply( X, 'sk_c6' ), X ), =( 'sk_c5', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 248, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( 'sk_c5', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 252, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c6', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 253, [ =( multiply( 'sk_c1', 'sk_c7' ), identity ), =( 'sk_c6',
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 254, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( 'sk_c6', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 269, [ =( multiply( X, 'sk_c6' ), X ), =( multiply( 'sk_c4', Y ), Y
% 33.88/34.30 ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 275, [ ~( =( 'sk_c6', 'sk_c4' ) ), =( multiply( 'sk_c4', 'sk_c6' )
% 33.88/34.30 , 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 276, [ ~( =( 'sk_c6', 'sk_c4' ) ), =( 'sk_c6', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 288, [ =( multiply( inverse( 'sk_c6' ), X ), X ), =( multiply( Y,
% 33.88/34.30 'sk_c4' ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 290, [ ~( =( inverse( 'sk_c6' ), 'sk_c4' ) ), =( multiply( inverse(
% 33.88/34.30 'sk_c6' ), 'sk_c4' ), inverse( 'sk_c6' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 291, [ ~( =( inverse( 'sk_c6' ), 'sk_c4' ) ), =( inverse( 'sk_c6' )
% 33.88/34.30 , 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 297, [ =( multiply( inverse( 'sk_c5' ), X ), X ), =( multiply( Y,
% 33.88/34.30 'sk_c6' ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 299, [ ~( =( inverse( 'sk_c5' ), 'sk_c6' ) ), =( multiply( inverse(
% 33.88/34.30 'sk_c5' ), 'sk_c6' ), inverse( 'sk_c5' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 300, [ ~( =( inverse( 'sk_c5' ), 'sk_c6' ) ), =( inverse( 'sk_c5' )
% 33.88/34.30 , 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 311, [ =( multiply( X, 'sk_c4' ), X ), ~( =( 'sk_c6', 'sk_c4' ) ),
% 33.88/34.30 =( multiply( Y, 'sk_c4' ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 315, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( 'sk_c5',
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 316, [ =( multiply( X, 'sk_c4' ), X ), ~( =( 'sk_c6', 'sk_c4' ) ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 317, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( multiply( X,
% 33.88/34.30 'sk_c7' ), 'sk_c3' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 321, [ ~( =( 'sk_c6', 'sk_c4' ) ), =( identity, 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 323, [ ~( =( 'sk_c6', 'sk_c4' ) ), =( multiply( 'sk_c4', X ), X ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 333, [ =( inverse( 'sk_c6' ), 'sk_c5' ), ~( =( inverse( 'sk_c5' ),
% 33.88/34.30 'sk_c6' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 339, [ =( 'sk_c6', 'sk_c5' ), =( 'sk_c5', 'sk_c4' ), ~( =( inverse(
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 343, [ =( inverse( 'sk_c4' ), 'sk_c6' ), ~( =( inverse( 'sk_c6' ),
% 33.88/34.30 'sk_c4' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 355, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 356, [ =( 'sk_c6', 'sk_c4' ), ~( =( inverse( 'sk_c6' ), 'sk_c4' ) )
% 33.88/34.30 ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 367, [ ~( =( inverse( 'sk_c6' ), 'sk_c4' ) ), =( multiply( 'sk_c4'
% 33.88/34.30 , X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 374, [ =( 'sk_c5', 'sk_c4' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.88/34.30 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 375, [ =( multiply( 'sk_c4', X ), X ), =( multiply( 'sk_c1',
% 33.88/34.30 'sk_c7' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 377, [ =( 'sk_c6', 'sk_c4' ), =( identity, 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 381, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( 'sk_c6', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 383, [ =( 'sk_c6', 'sk_c4' ), =( multiply( 'sk_c6', X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 386, [ =( 'sk_c6', 'sk_c5' ), ~( =( inverse( 'sk_c5' ), 'sk_c6' ) )
% 33.88/34.30 , =( 'sk_c6', 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 387, [ =( 'sk_c6', 'sk_c5' ), ~( =( inverse( 'sk_c5' ), 'sk_c6' ) )
% 33.88/34.30 ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 388, [ ~( =( inverse( 'sk_c5' ), 'sk_c6' ) ), =( multiply( 'sk_c5'
% 33.88/34.30 , X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 389, [ ~( =( inverse( 'sk_c5' ), 'sk_c6' ) ), =( multiply( X,
% 33.88/34.30 'sk_c5' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 431, [ =( 'sk_c5', 'sk_c4' ), =( multiply( 'sk_c7', 'sk_c1' ),
% 33.88/34.30 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 434, [ =( multiply( 'sk_c7', 'sk_c1' ), 'sk_c6' ), =( identity,
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 457, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( 'sk_c6',
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 477, [ =( 'sk_c6', 'sk_c5' ), =( multiply( multiply( X, 'sk_c7' ),
% 33.88/34.30 'sk_c1' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 478, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( inverse( 'sk_c7' ),
% 33.88/34.30 'sk_c1' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 480, [ ~( =( 'sk_c3', 'sk_c1' ) ), =( inverse( 'sk_c7' ), 'sk_c1' )
% 33.88/34.30 ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 481, [ ~( =( 'sk_c3', 'sk_c1' ) ), =( 'sk_c3', 'sk_c1' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 489, [ =( inverse( 'sk_c1' ), 'sk_c7' ), ~( =( 'sk_c3', 'sk_c1' ) )
% 33.88/34.30 ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 501, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( multiply( multiply( X,
% 33.88/34.30 'sk_c7' ), 'sk_c1' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 510, [ =( 'sk_c6', 'sk_c4' ), =( inverse( 'sk_c2' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 516, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse( Y )
% 33.88/34.30 ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 527, [ =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ), =( multiply( X,
% 33.88/34.30 'sk_c6' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 528, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( inverse( 'sk_c2' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 535, [ =( inverse( 'sk_c2' ), 'sk_c7' ), =( multiply( 'sk_c4', X )
% 33.88/34.30 , X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 539, [ =( 'sk_c6', 'sk_c4' ), =( 'sk_c2', 'sk_c1' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 542, [ =( 'sk_c2', 'sk_c1' ), =( identity, 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 559, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( 'sk_c2', 'sk_c1' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 566, [ =( 'sk_c2', 'sk_c1' ), =( multiply( 'sk_c7', 'sk_c3' ),
% 33.88/34.30 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 569, [ =( multiply( 'sk_c7', 'sk_c1' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c7', 'sk_c3' ), 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 574, [ =( inverse( 'sk_c7' ), 'sk_c2' ), =( multiply( 'sk_c4', X )
% 33.88/34.30 , X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 618, [ =( identity, 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 621, [ =( multiply( X, 'sk_c6' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 622, [ =( inverse( 'sk_c6' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 623, [ =( multiply( 'sk_c6', X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 653, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( multiply( 'sk_c7',
% 33.88/34.30 'sk_c1' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 656, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X )
% 33.88/34.30 ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 657, [ =( multiply( inverse( Y ), inverse( X ) ), inverse( multiply(
% 33.88/34.30 X, Y ) ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 664, [ =( inverse( multiply( inverse( X ), Y ) ), multiply( inverse(
% 33.88/34.30 Y ), X ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 673, [ =( inverse( multiply( X, inverse( Y ) ) ), multiply( Y,
% 33.88/34.30 inverse( X ) ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 674, [ =( inverse( 'sk_c7' ), 'sk_c2' ), =( 'sk_c6', 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 679, [ =( inverse( 'sk_c7' ), 'sk_c2' ), =( multiply( X, 'sk_c5' )
% 33.88/34.30 , X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 680, [ =( inverse( 'sk_c7' ), 'sk_c2' ), =( inverse( 'sk_c5' ),
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 681, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c2' ), X ), =(
% 33.88/34.30 'sk_c6', 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 683, [ =( 'sk_c6', 'sk_c5' ), =( multiply( multiply( X, 'sk_c2' ),
% 33.88/34.30 'sk_c7' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 684, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c2', 'sk_c7' ),
% 33.88/34.30 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 689, [ =( multiply( 'sk_c2', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c5', X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 695, [ =( multiply( inverse( 'sk_c2' ), X ), multiply( 'sk_c7', X )
% 33.88/34.30 ), =( multiply( Y, 'sk_c5' ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 697, [ ~( =( multiply( 'sk_c7', 'sk_c5' ), inverse( 'sk_c2' ) ) ),
% 33.88/34.30 =( multiply( inverse( 'sk_c2' ), 'sk_c5' ), inverse( 'sk_c2' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 698, [ ~( =( multiply( 'sk_c7', 'sk_c5' ), inverse( 'sk_c2' ) ) ),
% 33.88/34.30 =( multiply( 'sk_c7', 'sk_c5' ), inverse( 'sk_c2' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 720, [ =( multiply( inverse( X ), 'sk_c2' ), inverse( multiply(
% 33.88/34.30 'sk_c7', X ) ) ), =( inverse( 'sk_c5' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 772, [ =( multiply( inverse( X ), 'sk_c1' ), inverse( multiply(
% 33.88/34.30 'sk_c7', X ) ) ), =( inverse( 'sk_c7' ), 'sk_c3' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 788, [ =( multiply( inverse( X ), 'sk_c7' ), inverse( multiply(
% 33.88/34.30 'sk_c1', X ) ) ), =( 'sk_c6', 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 845, [ =( 'sk_c6', 'sk_c5' ), =( inverse( multiply( 'sk_c2', X ) )
% 33.88/34.30 , inverse( multiply( 'sk_c1', X ) ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 848, [ =( 'sk_c6', 'sk_c5' ), =( inverse( multiply( 'sk_c1',
% 33.88/34.30 'sk_c7' ) ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 856, [ =( 'sk_c6', 'sk_c5' ), =( multiply( multiply( X, 'sk_c1' ),
% 33.88/34.30 'sk_c7' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 858, [ =( 'sk_c6', 'sk_c5' ), =( multiply( multiply( 'sk_c1',
% 33.88/34.30 'sk_c7' ), X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 863, [ =( multiply( X, 'sk_c2' ), multiply( X, 'sk_c1' ) ), =(
% 33.88/34.30 'sk_c6', 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 864, [ =( 'sk_c6', 'sk_c5' ), =( multiply( X, inverse( 'sk_c1' ) )
% 33.88/34.30 , multiply( X, 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 868, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c2' ), inverse(
% 33.88/34.30 'sk_c1' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 879, [ =( inverse( 'sk_c2' ), inverse( 'sk_c1' ) ), =( inverse(
% 33.88/34.30 'sk_c5' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 885, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( multiply(
% 33.88/34.30 'sk_c7', 'sk_c1' ) ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 945, [ =( multiply( multiply( 'sk_c1', 'sk_c7' ), X ), X ), =(
% 33.88/34.30 multiply( Y, 'sk_c5' ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 952, [ ~( =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c5' ) ), =( multiply(
% 33.88/34.30 multiply( 'sk_c1', 'sk_c7' ), 'sk_c5' ), multiply( 'sk_c1', 'sk_c7' ) ) ]
% 33.88/34.30 )
% 33.88/34.30 .
% 33.88/34.30 clause( 953, [ ~( =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c5' ) ), =( multiply(
% 33.88/34.30 'sk_c1', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 955, [ =( 'sk_c6', 'sk_c5' ), ~( =( multiply( 'sk_c1', 'sk_c7' ),
% 33.88/34.30 'sk_c5' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 961, [ ~( =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c5' ) ), =( multiply(
% 33.88/34.30 'sk_c5', X ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 969, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c1' ), X ), =(
% 33.88/34.30 inverse( 'sk_c5' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 995, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( multiply( inverse( X )
% 33.88/34.30 , 'sk_c1' ), inverse( multiply( 'sk_c7', X ) ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1023, [ =( multiply( X, inverse( X ) ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1024, [ =( multiply( multiply( Y, inverse( X ) ), X ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1025, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c7', 'sk_c3' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1030, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c7',
% 33.88/34.30 'sk_c3' ), 'sk_c4' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1033, [ =( multiply( inverse( X ), X ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1035, [ =( multiply( 'sk_c2', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1045, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X
% 33.88/34.30 ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1078, [ =( inverse( 'sk_c5' ), 'sk_c6' ), =( inverse( 'sk_c2' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1080, [ =( inverse( 'sk_c2' ), 'sk_c7' ), =( multiply( X, 'sk_c5' )
% 33.88/34.30 , X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1081, [ =( inverse( 'sk_c2' ), 'sk_c7' ), =( multiply( 'sk_c5', X )
% 33.88/34.30 , X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1082, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c2' ), X ), =(
% 33.88/34.30 inverse( 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1095, [ =( multiply( 'sk_c7', 'sk_c3' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c2' ), 'sk_c7' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1150, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.88/34.30 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1311, [ =( multiply( X, inverse( 'sk_c1' ) ), multiply( X, 'sk_c7'
% 33.88/34.30 ) ), =( multiply( 'sk_c5', Y ), Y ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1314, [ ~( =( multiply( 'sk_c5', 'sk_c7' ), inverse( 'sk_c1' ) ) )
% 33.88/34.30 , =( multiply( 'sk_c5', inverse( 'sk_c1' ) ), inverse( 'sk_c1' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1315, [ ~( =( multiply( 'sk_c5', 'sk_c7' ), inverse( 'sk_c1' ) ) )
% 33.88/34.30 , =( multiply( 'sk_c5', 'sk_c7' ), inverse( 'sk_c1' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1411, [ =( inverse( 'sk_c1' ), 'sk_c7' ), ~( =( multiply( 'sk_c1',
% 33.88/34.30 'sk_c7' ), 'sk_c4' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1413, [ =( multiply( 'sk_c7', 'sk_c1' ), 'sk_c6' ), ~( =( multiply(
% 33.88/34.30 'sk_c1', 'sk_c7' ), 'sk_c4' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1616, [ ~( =( multiply( 'sk_c5', 'sk_c7' ), 'sk_c7' ) ), =( 'sk_c6'
% 33.88/34.30 , 'sk_c5' ), =( 'sk_c3', 'sk_c2' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1620, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( multiply( 'sk_c5',
% 33.88/34.30 'sk_c7' ), inverse( 'sk_c1' ) ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1625, [ ~( =( multiply( 'sk_c5', 'sk_c7' ), inverse( 'sk_c1' ) ) )
% 33.88/34.30 , =( multiply( 'sk_c7', 'sk_c1' ), 'sk_c5' ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1655, [ =( 'sk_c6', 'sk_c5' ), ~( =( multiply( 'sk_c5', 'sk_c7' ),
% 33.88/34.30 'sk_c7' ) ), ~( =( multiply( 'sk_c7', 'sk_c1' ), 'sk_c4' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1657, [ =( 'sk_c6', 'sk_c5' ), ~( =( multiply( 'sk_c5', 'sk_c7' ),
% 33.88/34.30 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1662, [ ~( =( multiply( 'sk_c5', 'sk_c7' ), 'sk_c7' ) ), =(
% 33.88/34.30 multiply( X, 'sk_c5' ), X ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1726, [ =( inverse( 'sk_c2' ), 'sk_c7' ), ~( =( inverse( 'sk_c2' )
% 33.88/34.30 , 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1730, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), ~( =( inverse(
% 33.88/34.30 'sk_c2' ), 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 1731, [ =( multiply( 'sk_c2', 'sk_c7' ), 'sk_c6' ), ~( =( inverse(
% 33.88/34.30 'sk_c2' ), 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 5596, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X
% 33.88/34.30 ), 'sk_c7' ) ), ~( =( inverse( 'sk_c2' ), 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 5617, [ ~( =( multiply( 'sk_c7', X ), 'sk_c6' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 5656, [ ~( =( inverse( 'sk_c2' ), 'sk_c7' ) ) ] )
% 33.88/34.30 .
% 33.88/34.30 clause( 5683, [] )
% 33.88/34.30 .
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 % SZS output end Refutation
% 33.88/34.30 found a proof!
% 33.88/34.30
% 33.88/34.30 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 33.88/34.30
% 33.88/34.30 initialclauses(
% 33.88/34.30 [ clause( 5685, [ =( multiply( identity, X ), X ) ] )
% 33.88/34.30 , clause( 5686, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.88/34.30 , clause( 5687, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.88/34.30 Y, Z ) ) ) ] )
% 33.88/34.30 , clause( 5688, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5689, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 , clause( 5690, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , clause( 5691, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5692, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.88/34.30 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5693, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 , clause( 5694, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , clause( 5695, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5696, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5697, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 , clause( 5698, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , clause( 5699, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5700, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse(
% 33.88/34.30 X ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =(
% 33.88/34.30 multiply( Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =(
% 33.88/34.30 multiply( U, T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.88/34.30 ] ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 0, [ =( multiply( identity, X ), X ) ] )
% 33.88/34.30 , clause( 5685, [ =( multiply( identity, X ), X ) ] )
% 33.88/34.30 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.88/34.30 , clause( 5686, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.88/34.30 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 eqswap(
% 33.88/34.30 clause( 5706, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X,
% 33.88/34.30 Y ), Z ) ) ] )
% 33.88/34.30 , clause( 5687, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.88/34.30 Y, Z ) ) ) ] )
% 33.88/34.30 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 33.88/34.30 , Z ) ) ] )
% 33.88/34.30 , clause( 5706, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X
% 33.88/34.30 , Y ), Z ) ) ] )
% 33.88/34.30 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 33.88/34.30 permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 3, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5688, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 4, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 , clause( 5689, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 5, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , clause( 5690, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 6, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5691, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c4' ), 'sk_c5' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 7, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.88/34.30 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5692, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.88/34.30 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 , clause( 5693, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.88/34.30 'sk_c7' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 9, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , clause( 5694, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 33.88/34.30 'sk_c5' ), 'sk_c6' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 10, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5695, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.88/34.30 'sk_c5' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 11, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , clause( 5696, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.88/34.30 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 12, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 , clause( 5697, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.88/34.30 'sk_c3' ), 'sk_c7' ) ] )
% 33.88/34.30 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.88/34.30 ).
% 33.88/34.30
% 33.88/34.30
% 33.88/34.30 subsumption(
% 33.88/34.30 clause( 13, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.98/34.36 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.36 , clause( 5698, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.98/34.36 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.36 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.36 ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 14, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.98/34.36 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.36 , clause( 5699, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.98/34.36 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.36 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.36 ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 15, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X )
% 33.98/34.36 , 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =( multiply(
% 33.98/34.36 Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =( multiply( U,
% 33.98/34.36 T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.98/34.36 , clause( 5700, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse(
% 33.98/34.36 X ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =(
% 33.98/34.36 multiply( Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =(
% 33.98/34.36 multiply( U, T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.98/34.36 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ), :=( U
% 33.98/34.36 , U )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3
% 33.98/34.36 , 3 ), ==>( 4, 4 ), ==>( 5, 5 ), ==>( 6, 6 )] ) ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 6770, [ ~( =( 'sk_c6', multiply( X, 'sk_c7' ) ) ), ~( =( inverse( X
% 33.98/34.36 ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =(
% 33.98/34.36 multiply( Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =(
% 33.98/34.36 multiply( U, T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.98/34.36 , clause( 15, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X
% 33.98/34.36 ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =(
% 33.98/34.36 multiply( Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =(
% 33.98/34.36 multiply( U, T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T ),
% 33.98/34.36 :=( U, U )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqrefl(
% 33.98/34.36 clause( 6898, [ ~( =( 'sk_c6', multiply( X, 'sk_c7' ) ) ), ~( =( inverse( X
% 33.98/34.36 ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =( inverse(
% 33.98/34.36 Z ), 'sk_c7' ) ), ~( =( multiply( T, multiply( Z, 'sk_c7' ) ), 'sk_c6' )
% 33.98/34.36 ), ~( =( inverse( T ), multiply( Z, 'sk_c7' ) ) ) ] )
% 33.98/34.36 , clause( 6770, [ ~( =( 'sk_c6', multiply( X, 'sk_c7' ) ) ), ~( =( inverse(
% 33.98/34.36 X ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =(
% 33.98/34.36 multiply( Z, 'sk_c7' ), T ) ), ~( =( inverse( Z ), 'sk_c7' ) ), ~( =(
% 33.98/34.36 multiply( U, T ), 'sk_c6' ) ), ~( =( inverse( U ), T ) ) ] )
% 33.98/34.36 , 3, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, multiply(
% 33.98/34.36 Z, 'sk_c7' ) ), :=( U, T )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7034, [ ~( =( multiply( multiply( X, Y ), 'sk_c7' ), 'sk_c6' ) ),
% 33.98/34.36 ~( =( 'sk_c6', multiply( Z, 'sk_c7' ) ) ), ~( =( inverse( Z ), 'sk_c7' )
% 33.98/34.36 ), ~( =( multiply( 'sk_c7', T ), 'sk_c6' ) ), ~( =( inverse( Y ),
% 33.98/34.36 'sk_c7' ) ), ~( =( inverse( X ), multiply( Y, 'sk_c7' ) ) ) ] )
% 33.98/34.36 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.36 ), Z ) ) ] )
% 33.98/34.36 , 0, clause( 6898, [ ~( =( 'sk_c6', multiply( X, 'sk_c7' ) ) ), ~( =(
% 33.98/34.36 inverse( X ), 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~(
% 33.98/34.36 =( inverse( Z ), 'sk_c7' ) ), ~( =( multiply( T, multiply( Z, 'sk_c7' ) )
% 33.98/34.36 , 'sk_c6' ) ), ~( =( inverse( T ), multiply( Z, 'sk_c7' ) ) ) ] )
% 33.98/34.36 , 4, 2, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, 'sk_c7' )] ),
% 33.98/34.36 substitution( 1, [ :=( X, Z ), :=( Y, T ), :=( Z, Y ), :=( T, X )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7036, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( multiply(
% 33.98/34.36 multiply( Y, Z ), 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) )
% 33.98/34.36 , ~( =( multiply( 'sk_c7', T ), 'sk_c6' ) ), ~( =( inverse( Z ), 'sk_c7'
% 33.98/34.36 ) ), ~( =( inverse( Y ), multiply( Z, 'sk_c7' ) ) ) ] )
% 33.98/34.36 , clause( 7034, [ ~( =( multiply( multiply( X, Y ), 'sk_c7' ), 'sk_c6' ) )
% 33.98/34.36 , ~( =( 'sk_c6', multiply( Z, 'sk_c7' ) ) ), ~( =( inverse( Z ), 'sk_c7'
% 33.98/34.36 ) ), ~( =( multiply( 'sk_c7', T ), 'sk_c6' ) ), ~( =( inverse( Y ),
% 33.98/34.36 'sk_c7' ) ), ~( =( inverse( X ), multiply( Y, 'sk_c7' ) ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X ), :=( T, T )] )
% 33.98/34.36 ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 20, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X )
% 33.98/34.36 , 'sk_c7' ) ), ~( =( multiply( 'sk_c7', Y ), 'sk_c6' ) ), ~( =( inverse(
% 33.98/34.36 Z ), 'sk_c7' ) ), ~( =( inverse( T ), multiply( Z, 'sk_c7' ) ) ), ~( =(
% 33.98/34.36 multiply( multiply( T, Z ), 'sk_c7' ), 'sk_c6' ) ) ] )
% 33.98/34.36 , clause( 7036, [ ~( =( multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( multiply(
% 33.98/34.36 multiply( Y, Z ), 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) )
% 33.98/34.36 , ~( =( multiply( 'sk_c7', T ), 'sk_c6' ) ), ~( =( inverse( Z ), 'sk_c7'
% 33.98/34.36 ) ), ~( =( inverse( Y ), multiply( Z, 'sk_c7' ) ) ) ] )
% 33.98/34.36 , substitution( 0, [ :=( X, X ), :=( Y, T ), :=( Z, Z ), :=( T, Y )] ),
% 33.98/34.36 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 5 ), ==>( 2, 1 ), ==>( 3, 2 ),
% 33.98/34.36 ==>( 4, 3 ), ==>( 5, 4 )] ) ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7211, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , clause( 10, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.98/34.36 'sk_c5' ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7213, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.36 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7222, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c5',
% 33.98/34.36 inverse( 'sk_c4' ) ) ] )
% 33.98/34.36 , clause( 7211, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , 1, clause( 7213, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.36 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7224, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, multiply(
% 33.98/34.36 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.36 , clause( 7222, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c5',
% 33.98/34.36 inverse( 'sk_c4' ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7225, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.36 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.36 , clause( 7224, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, multiply(
% 33.98/34.36 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 22, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.36 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.36 , clause( 7225, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.36 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.36 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.36 ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7227, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7229, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.36 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7238, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c7',
% 33.98/34.36 inverse( 'sk_c3' ) ) ] )
% 33.98/34.36 , clause( 7227, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , 1, clause( 7229, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.36 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7240, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, multiply(
% 33.98/34.36 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.36 , clause( 7238, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c7',
% 33.98/34.36 inverse( 'sk_c3' ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7241, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.36 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.36 , clause( 7240, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, multiply(
% 33.98/34.36 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 24, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.36 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.36 , clause( 7241, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.36 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.36 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.36 ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7242, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , 0, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7245, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.36 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7246, [ =( identity, multiply( 'sk_c7', 'sk_c3' ) ), =( 'sk_c7',
% 33.98/34.36 inverse( 'sk_c1' ) ) ] )
% 33.98/34.36 , clause( 7242, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 33.98/34.36 'sk_c7' ) ] )
% 33.98/34.36 , 1, clause( 7245, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.36 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7248, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, multiply(
% 33.98/34.36 'sk_c7', 'sk_c3' ) ) ] )
% 33.98/34.36 , clause( 7246, [ =( identity, multiply( 'sk_c7', 'sk_c3' ) ), =( 'sk_c7',
% 33.98/34.36 inverse( 'sk_c1' ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7249, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( inverse(
% 33.98/34.36 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.36 , clause( 7248, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, multiply(
% 33.98/34.36 'sk_c7', 'sk_c3' ) ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 25, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( inverse(
% 33.98/34.36 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.36 , clause( 7249, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( inverse(
% 33.98/34.36 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.36 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.36 ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7250, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.98/34.36 Y, Z ) ) ) ] )
% 33.98/34.36 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.36 ), Z ) ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7253, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y
% 33.98/34.36 ), identity ) ] )
% 33.98/34.36 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.36 , 0, clause( 7250, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 33.98/34.36 multiply( Y, Z ) ) ) ] )
% 33.98/34.36 , 0, 9, substitution( 0, [ :=( X, multiply( X, Y ) )] ), substitution( 1, [
% 33.98/34.36 :=( X, inverse( multiply( X, Y ) ) ), :=( Y, X ), :=( Z, Y )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 28, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y )
% 33.98/34.36 , identity ) ] )
% 33.98/34.36 , clause( 7253, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ),
% 33.98/34.36 Y ), identity ) ] )
% 33.98/34.36 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 33.98/34.36 )] ) ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7259, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.98/34.36 Y, Z ) ) ) ] )
% 33.98/34.36 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.36 ), Z ) ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7264, [ =( multiply( multiply( X, inverse( Y ) ), Y ), multiply( X
% 33.98/34.36 , identity ) ) ] )
% 33.98/34.36 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.36 , 0, clause( 7259, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 33.98/34.36 multiply( Y, Z ) ) ) ] )
% 33.98/34.36 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 33.98/34.36 :=( Y, inverse( Y ) ), :=( Z, Y )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 29, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y,
% 33.98/34.36 identity ) ) ] )
% 33.98/34.36 , clause( 7264, [ =( multiply( multiply( X, inverse( Y ) ), Y ), multiply(
% 33.98/34.36 X, identity ) ) ] )
% 33.98/34.36 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 33.98/34.36 )] ) ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7269, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.98/34.36 Y, Z ) ) ) ] )
% 33.98/34.36 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.36 ), Z ) ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7274, [ =( multiply( multiply( X, identity ), Y ), multiply( X, Y )
% 33.98/34.36 ) ] )
% 33.98/34.36 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 33.98/34.36 , 0, clause( 7269, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 33.98/34.36 multiply( Y, Z ) ) ) ] )
% 33.98/34.36 , 0, 8, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 33.98/34.36 :=( Y, identity ), :=( Z, Y )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 subsumption(
% 33.98/34.36 clause( 30, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X ) )
% 33.98/34.36 ] )
% 33.98/34.36 , clause( 7274, [ =( multiply( multiply( X, identity ), Y ), multiply( X, Y
% 33.98/34.36 ) ) ] )
% 33.98/34.36 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 33.98/34.36 )] ) ).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7280, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c7',
% 33.98/34.36 'sk_c3' ), identity ) ] )
% 33.98/34.36 , clause( 25, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( inverse(
% 33.98/34.36 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.36 , 1, substitution( 0, [] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7282, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.98/34.36 Y, Z ) ) ) ] )
% 33.98/34.36 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.36 ), Z ) ) ] )
% 33.98/34.36 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 paramod(
% 33.98/34.36 clause( 7284, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c3' ), multiply( X
% 33.98/34.36 , identity ) ), =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.36 , clause( 7280, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c7',
% 33.98/34.36 'sk_c3' ), identity ) ] )
% 33.98/34.36 , 1, clause( 7282, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 33.98/34.36 multiply( Y, Z ) ) ) ] )
% 33.98/34.36 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y,
% 33.98/34.36 'sk_c7' ), :=( Z, 'sk_c3' )] )).
% 33.98/34.36
% 33.98/34.36
% 33.98/34.36 eqswap(
% 33.98/34.36 clause( 7289, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( multiply( X
% 33.98/34.37 , 'sk_c7' ), 'sk_c3' ), multiply( X, identity ) ) ] )
% 33.98/34.37 , clause( 7284, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c3' ), multiply(
% 33.98/34.37 X, identity ) ), =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 31, [ =( multiply( multiply( X, 'sk_c7' ), 'sk_c3' ), multiply( X,
% 33.98/34.37 identity ) ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7289, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( multiply(
% 33.98/34.37 X, 'sk_c7' ), 'sk_c3' ), multiply( X, identity ) ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 33.98/34.37 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7291, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 12, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7294, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7295, [ =( identity, multiply( 'sk_c7', 'sk_c3' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.37 , clause( 7291, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7294, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7297, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.37 multiply( 'sk_c7', 'sk_c3' ) ) ] )
% 33.98/34.37 , clause( 7295, [ =( identity, multiply( 'sk_c7', 'sk_c3' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7298, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( multiply(
% 33.98/34.37 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7297, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.37 multiply( 'sk_c7', 'sk_c3' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 40, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( multiply(
% 33.98/34.37 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7298, [ =( multiply( 'sk_c7', 'sk_c3' ), identity ), =( multiply(
% 33.98/34.37 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7300, [ =( 'sk_c6', multiply( 'sk_c4', 'sk_c5' ) ), =( inverse(
% 33.98/34.37 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 9, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 33.98/34.37 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7302, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7303, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c4', 'sk_c5' ) ) ] )
% 33.98/34.37 , clause( 7300, [ =( 'sk_c6', multiply( 'sk_c4', 'sk_c5' ) ), =( inverse(
% 33.98/34.37 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7302, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7305, [ =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ), =( identity,
% 33.98/34.37 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.37 , clause( 7303, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c4', 'sk_c5' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7306, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7305, [ =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ), =( identity,
% 33.98/34.37 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 42, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7306, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7308, [ =( 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.98/34.37 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7310, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7311, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c5',
% 33.98/34.37 multiply( 'sk_c3', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7308, [ =( 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7310, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7313, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.37 , clause( 7311, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c5',
% 33.98/34.37 multiply( 'sk_c3', 'sk_c7' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7314, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.37 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , clause( 7313, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 44, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.37 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , clause( 7314, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.37 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7316, [ =( multiply( X, Y ), multiply( multiply( X, identity ), Y )
% 33.98/34.37 ) ] )
% 33.98/34.37 , clause( 30, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X )
% 33.98/34.37 ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7319, [ =( multiply( inverse( identity ), X ), multiply( identity,
% 33.98/34.37 X ) ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, clause( 7316, [ =( multiply( X, Y ), multiply( multiply( X, identity )
% 33.98/34.37 , Y ) ) ] )
% 33.98/34.37 , 0, 6, substitution( 0, [ :=( X, identity )] ), substitution( 1, [ :=( X,
% 33.98/34.37 inverse( identity ) ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7320, [ =( multiply( inverse( identity ), X ), X ) ] )
% 33.98/34.37 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 33.98/34.37 , 0, clause( 7319, [ =( multiply( inverse( identity ), X ), multiply(
% 33.98/34.37 identity, X ) ) ] )
% 33.98/34.37 , 0, 5, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 49, [ =( multiply( inverse( identity ), X ), X ) ] )
% 33.98/34.37 , clause( 7320, [ =( multiply( inverse( identity ), X ), X ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7323, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.98/34.37 Y, Z ) ) ) ] )
% 33.98/34.37 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.37 ), Z ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7328, [ =( multiply( multiply( X, inverse( identity ) ), Y ),
% 33.98/34.37 multiply( X, Y ) ) ] )
% 33.98/34.37 , clause( 49, [ =( multiply( inverse( identity ), X ), X ) ] )
% 33.98/34.37 , 0, clause( 7323, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 33.98/34.37 multiply( Y, Z ) ) ) ] )
% 33.98/34.37 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 33.98/34.37 :=( Y, inverse( identity ) ), :=( Z, Y )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 50, [ =( multiply( multiply( Y, inverse( identity ) ), X ),
% 33.98/34.37 multiply( Y, X ) ) ] )
% 33.98/34.37 , clause( 7328, [ =( multiply( multiply( X, inverse( identity ) ), Y ),
% 33.98/34.37 multiply( X, Y ) ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 33.98/34.37 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7334, [ =( 'sk_c6', multiply( 'sk_c4', 'sk_c5' ) ), =( multiply(
% 33.98/34.37 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 5, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7336, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 33.98/34.37 Y, Z ) ) ) ] )
% 33.98/34.37 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 33.98/34.37 ), Z ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7354, [ =( multiply( multiply( X, 'sk_c1' ), 'sk_c7' ), multiply( X
% 33.98/34.37 , 'sk_c6' ) ), =( 'sk_c6', multiply( 'sk_c4', 'sk_c5' ) ) ] )
% 33.98/34.37 , clause( 7334, [ =( 'sk_c6', multiply( 'sk_c4', 'sk_c5' ) ), =( multiply(
% 33.98/34.37 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , 1, clause( 7336, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 33.98/34.37 multiply( Y, Z ) ) ) ] )
% 33.98/34.37 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y,
% 33.98/34.37 'sk_c1' ), :=( Z, 'sk_c7' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7359, [ =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 multiply( X, 'sk_c1' ), 'sk_c7' ), multiply( X, 'sk_c6' ) ) ] )
% 33.98/34.37 , clause( 7354, [ =( multiply( multiply( X, 'sk_c1' ), 'sk_c7' ), multiply(
% 33.98/34.37 X, 'sk_c6' ) ), =( 'sk_c6', multiply( 'sk_c4', 'sk_c5' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 55, [ =( multiply( multiply( X, 'sk_c1' ), 'sk_c7' ), multiply( X,
% 33.98/34.37 'sk_c6' ) ), =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7359, [ =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 multiply( X, 'sk_c1' ), 'sk_c7' ), multiply( X, 'sk_c6' ) ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 33.98/34.37 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7362, [ =( multiply( X, Y ), multiply( multiply( X, inverse(
% 33.98/34.37 identity ) ), Y ) ) ] )
% 33.98/34.37 , clause( 50, [ =( multiply( multiply( Y, inverse( identity ) ), X ),
% 33.98/34.37 multiply( Y, X ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7365, [ =( multiply( inverse( inverse( identity ) ), X ), multiply(
% 33.98/34.37 identity, X ) ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, clause( 7362, [ =( multiply( X, Y ), multiply( multiply( X, inverse(
% 33.98/34.37 identity ) ), Y ) ) ] )
% 33.98/34.37 , 0, 7, substitution( 0, [ :=( X, inverse( identity ) )] ), substitution( 1
% 33.98/34.37 , [ :=( X, inverse( inverse( identity ) ) ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7366, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 33.98/34.37 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 33.98/34.37 , 0, clause( 7365, [ =( multiply( inverse( inverse( identity ) ), X ),
% 33.98/34.37 multiply( identity, X ) ) ] )
% 33.98/34.37 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 73, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 33.98/34.37 , clause( 7366, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ]
% 33.98/34.37 )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7368, [ =( X, multiply( inverse( inverse( identity ) ), X ) ) ] )
% 33.98/34.37 , clause( 73, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7370, [ =( inverse( identity ), identity ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, clause( 7368, [ =( X, multiply( inverse( inverse( identity ) ), X ) )
% 33.98/34.37 ] )
% 33.98/34.37 , 0, 3, substitution( 0, [ :=( X, inverse( identity ) )] ), substitution( 1
% 33.98/34.37 , [ :=( X, inverse( identity ) )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 122, [ =( inverse( identity ), identity ) ] )
% 33.98/34.37 , clause( 7370, [ =( inverse( identity ), identity ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7373, [ =( multiply( X, identity ), multiply( multiply( X, inverse(
% 33.98/34.37 Y ) ), Y ) ) ] )
% 33.98/34.37 , clause( 29, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y
% 33.98/34.37 , identity ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7376, [ =( multiply( inverse( inverse( X ) ), identity ), multiply(
% 33.98/34.37 identity, X ) ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, clause( 7373, [ =( multiply( X, identity ), multiply( multiply( X,
% 33.98/34.37 inverse( Y ) ), Y ) ) ] )
% 33.98/34.37 , 0, 7, substitution( 0, [ :=( X, inverse( X ) )] ), substitution( 1, [
% 33.98/34.37 :=( X, inverse( inverse( X ) ) ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7377, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 33.98/34.37 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 33.98/34.37 , 0, clause( 7376, [ =( multiply( inverse( inverse( X ) ), identity ),
% 33.98/34.37 multiply( identity, X ) ) ] )
% 33.98/34.37 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 125, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 33.98/34.37 , clause( 7377, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ]
% 33.98/34.37 )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7380, [ =( multiply( X, Y ), multiply( multiply( X, identity ), Y )
% 33.98/34.37 ) ] )
% 33.98/34.37 , clause( 30, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X )
% 33.98/34.37 ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7383, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y )
% 33.98/34.37 ) ] )
% 33.98/34.37 , clause( 125, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 33.98/34.37 , 0, clause( 7380, [ =( multiply( X, Y ), multiply( multiply( X, identity )
% 33.98/34.37 , Y ) ) ] )
% 33.98/34.37 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, inverse(
% 33.98/34.37 inverse( X ) ) ), :=( Y, Y )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y )
% 33.98/34.37 ) ] )
% 33.98/34.37 , clause( 7383, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 33.98/34.37 ) ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 33.98/34.37 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7389, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) ), Y )
% 33.98/34.37 ) ] )
% 33.98/34.37 , clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 33.98/34.37 ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7392, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.37 , clause( 125, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 33.98/34.37 , 0, clause( 7389, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) )
% 33.98/34.37 , Y ) ) ] )
% 33.98/34.37 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 33.98/34.37 :=( Y, identity )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.37 , clause( 7392, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7397, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) ), Y )
% 33.98/34.37 ) ] )
% 33.98/34.37 , clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 33.98/34.37 ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7400, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 33.98/34.37 , 0, clause( 7397, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) )
% 33.98/34.37 , Y ) ) ] )
% 33.98/34.37 , 0, 5, substitution( 0, [ :=( X, inverse( X ) )] ), substitution( 1, [
% 33.98/34.37 :=( X, X ), :=( Y, inverse( X ) )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , clause( 7400, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7403, [ =( X, multiply( X, identity ) ) ] )
% 33.98/34.37 , clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7406, [ =( inverse( inverse( X ) ), multiply( X, identity ) ) ] )
% 33.98/34.37 , clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 33.98/34.37 ) ) ] )
% 33.98/34.37 , 0, clause( 7403, [ =( X, multiply( X, identity ) ) ] )
% 33.98/34.37 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, identity )] ), substitution(
% 33.98/34.37 1, [ :=( X, inverse( inverse( X ) ) )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7407, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.37 , 0, clause( 7406, [ =( inverse( inverse( X ) ), multiply( X, identity ) )
% 33.98/34.37 ] )
% 33.98/34.37 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , clause( 7407, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7410, [ =( multiply( X, identity ), multiply( multiply( X, inverse(
% 33.98/34.37 Y ) ), Y ) ) ] )
% 33.98/34.37 , clause( 29, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y
% 33.98/34.37 , identity ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7412, [ =( multiply( X, identity ), multiply( multiply( X, Y ),
% 33.98/34.37 inverse( Y ) ) ) ] )
% 33.98/34.37 , clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , 0, clause( 7410, [ =( multiply( X, identity ), multiply( multiply( X,
% 33.98/34.37 inverse( Y ) ), Y ) ) ] )
% 33.98/34.37 , 0, 7, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 33.98/34.37 :=( Y, inverse( Y ) )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7413, [ =( X, multiply( multiply( X, Y ), inverse( Y ) ) ) ] )
% 33.98/34.37 , clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.37 , 0, clause( 7412, [ =( multiply( X, identity ), multiply( multiply( X, Y )
% 33.98/34.37 , inverse( Y ) ) ) ] )
% 33.98/34.37 , 0, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 33.98/34.37 :=( Y, Y )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7414, [ =( multiply( multiply( X, Y ), inverse( Y ) ), X ) ] )
% 33.98/34.37 , clause( 7413, [ =( X, multiply( multiply( X, Y ), inverse( Y ) ) ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 159, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 33.98/34.37 , clause( 7414, [ =( multiply( multiply( X, Y ), inverse( Y ) ), X ) ] )
% 33.98/34.37 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 33.98/34.37 )] ) ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7415, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 24, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7418, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7419, [ =( 'sk_c3', inverse( 'sk_c7' ) ), =( identity, multiply(
% 33.98/34.37 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.37 , clause( 7415, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7418, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7421, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c3',
% 33.98/34.37 inverse( 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7419, [ =( 'sk_c3', inverse( 'sk_c7' ) ), =( identity, multiply(
% 33.98/34.37 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7422, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( multiply( 'sk_c7',
% 33.98/34.37 'sk_c1' ), identity ) ] )
% 33.98/34.37 , clause( 7421, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c3',
% 33.98/34.37 inverse( 'sk_c7' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 169, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( multiply( 'sk_c7',
% 33.98/34.37 'sk_c1' ), identity ) ] )
% 33.98/34.37 , clause( 7422, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( multiply( 'sk_c7',
% 33.98/34.37 'sk_c1' ), identity ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7424, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7426, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7435, [ =( 'sk_c1', inverse( 'sk_c7' ) ), =( 'sk_c7', inverse(
% 33.98/34.37 'sk_c3' ) ) ] )
% 33.98/34.37 , clause( 7424, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7426, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7437, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( 'sk_c1', inverse(
% 33.98/34.37 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7435, [ =( 'sk_c1', inverse( 'sk_c7' ) ), =( 'sk_c7', inverse(
% 33.98/34.37 'sk_c3' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7438, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7437, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( 'sk_c1', inverse(
% 33.98/34.37 'sk_c7' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 170, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7438, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7439, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7442, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7443, [ =( 'sk_c3', inverse( 'sk_c7' ) ), =( 'sk_c7', inverse(
% 33.98/34.37 'sk_c1' ) ) ] )
% 33.98/34.37 , clause( 7439, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7442, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7445, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c3', inverse(
% 33.98/34.37 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7443, [ =( 'sk_c3', inverse( 'sk_c7' ) ), =( 'sk_c7', inverse(
% 33.98/34.37 'sk_c1' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7446, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7445, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c3', inverse(
% 33.98/34.37 'sk_c7' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 171, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7446, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7447, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c4' ),
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , clause( 10, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7450, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7451, [ =( 'sk_c4', inverse( 'sk_c5' ) ), =( 'sk_c7', inverse(
% 33.98/34.37 'sk_c1' ) ) ] )
% 33.98/34.37 , clause( 7447, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c4' ),
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , 1, clause( 7450, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7453, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c4', inverse(
% 33.98/34.37 'sk_c5' ) ) ] )
% 33.98/34.37 , clause( 7451, [ =( 'sk_c4', inverse( 'sk_c5' ) ), =( 'sk_c7', inverse(
% 33.98/34.37 'sk_c1' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7454, [ =( inverse( 'sk_c5' ), 'sk_c4' ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7453, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c4', inverse(
% 33.98/34.37 'sk_c5' ) ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 173, [ =( inverse( 'sk_c5' ), 'sk_c4' ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7454, [ =( inverse( 'sk_c5' ), 'sk_c4' ), =( inverse( 'sk_c1' ),
% 33.98/34.37 'sk_c7' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7455, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 4, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7458, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7462, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7455, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7458, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7472, [ =( identity, 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 3, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , 1, clause( 7462, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =(
% 33.98/34.37 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7538, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7472, [ =( identity, 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 factor(
% 33.98/34.37 clause( 7544, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , clause( 7538, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , 0, 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 174, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , clause( 7544, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7605, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.37 , clause( 6, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.98/34.37 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7608, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7609, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 5, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7615, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7605, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.37 , 1, clause( 7608, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7616, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1',
% 33.98/34.37 'sk_c7' ) ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7609, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( multiply(
% 33.98/34.37 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.37 , 1, clause( 7615, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =(
% 33.98/34.37 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 factor(
% 33.98/34.37 clause( 7617, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1',
% 33.98/34.37 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7616, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1',
% 33.98/34.37 'sk_c7' ) ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , 1, 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7627, [ =( 'sk_c5', 'sk_c6' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 174, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , 1, clause( 7617, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1'
% 33.98/34.37 , 'sk_c7' ) ) ] )
% 33.98/34.37 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7693, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( 'sk_c5',
% 33.98/34.37 'sk_c6' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7627, [ =( 'sk_c5', 'sk_c6' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 33.98/34.37 , 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7694, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7693, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( 'sk_c5',
% 33.98/34.37 'sk_c6' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 factor(
% 33.98/34.37 clause( 7698, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7694, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 33.98/34.37 , 1, 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 175, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( 'sk_c6',
% 33.98/34.37 'sk_c5' ) ] )
% 33.98/34.37 , clause( 7698, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 33.98/34.37 'sk_c6' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7755, [ =( 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 7, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.98/34.37 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , 1, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7757, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7761, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c5',
% 33.98/34.37 multiply( 'sk_c3', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 7755, [ =( 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ), =( inverse(
% 33.98/34.37 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7757, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7770, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c7' ),
% 33.98/34.37 'sk_c5' ), =( 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ) ] )
% 33.98/34.37 , clause( 3, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , 0, clause( 7761, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 33.98/34.37 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ) ] )
% 33.98/34.37 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7790, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , clause( 7770, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c7' ),
% 33.98/34.37 'sk_c5' ), =( 'sk_c5', multiply( 'sk_c3', 'sk_c7' ) ) ] )
% 33.98/34.37 , 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 factor(
% 33.98/34.37 clause( 7905, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7790, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , 0, 2, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 subsumption(
% 33.98/34.37 clause( 176, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7905, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.37 'sk_c6' ) ] )
% 33.98/34.37 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.37 ).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7906, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , clause( 12, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 0, substitution( 0, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7909, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.37 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7913, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =( 'sk_c6',
% 33.98/34.37 multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.37 , clause( 7906, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( inverse(
% 33.98/34.37 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.37 , 1, clause( 7909, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.37 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 paramod(
% 33.98/34.37 clause( 7923, [ =( identity, 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.37 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.37 , clause( 11, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.98/34.37 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.37 , 1, clause( 7913, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =(
% 33.98/34.37 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.37 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.37
% 33.98/34.37
% 33.98/34.37 eqswap(
% 33.98/34.37 clause( 7989, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.37 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.37 , clause( 7923, [ =( identity, 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.37 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 7995, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , clause( 7989, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.38 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 subsumption(
% 33.98/34.38 clause( 178, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , clause( 7995, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.38 ).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8056, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( inverse(
% 33.98/34.38 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.38 , clause( 14, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( inverse(
% 33.98/34.38 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.38 , 0, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8059, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.38 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8060, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( multiply(
% 33.98/34.38 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.38 , clause( 13, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( multiply(
% 33.98/34.38 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.38 , 0, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8066, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =( 'sk_c6',
% 33.98/34.38 multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , clause( 8056, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( inverse(
% 33.98/34.38 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.38 , 1, clause( 8059, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8067, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7',
% 33.98/34.38 'sk_c2' ) ), =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , clause( 8060, [ =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ), =( multiply(
% 33.98/34.38 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.38 , 1, clause( 8066, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =(
% 33.98/34.38 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8068, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7',
% 33.98/34.38 'sk_c2' ) ) ] )
% 33.98/34.38 , clause( 8067, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7',
% 33.98/34.38 'sk_c2' ) ), =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , 1, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8078, [ =( 'sk_c5', 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.38 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , clause( 178, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( identity,
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , 1, clause( 8068, [ =( identity, 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7'
% 33.98/34.38 , 'sk_c2' ) ) ] )
% 33.98/34.38 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8144, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( 'sk_c5',
% 33.98/34.38 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.38 , clause( 8078, [ =( 'sk_c5', 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.38 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c7', 'sk_c2' ) ) ] )
% 33.98/34.38 , 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8145, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.38 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.38 , clause( 8144, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( 'sk_c5',
% 33.98/34.38 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.38 , 1, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8149, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.38 'sk_c6' ) ] )
% 33.98/34.38 , clause( 8145, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.38 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ) ] )
% 33.98/34.38 , 1, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 subsumption(
% 33.98/34.38 clause( 179, [ =( multiply( 'sk_c7', 'sk_c2' ), 'sk_c6' ), =( 'sk_c6',
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , clause( 8149, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c2' ),
% 33.98/34.38 'sk_c6' ) ] )
% 33.98/34.38 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 33.98/34.38 ).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8205, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 33.98/34.38 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.38 , clause( 22, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.38 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.38 , 0, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8208, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.38 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8212, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =( identity,
% 33.98/34.38 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 8205, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 33.98/34.38 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.38 , 1, clause( 8208, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8222, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c1' ),
% 33.98/34.38 identity ), =( identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 42, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.38 'sk_c4', 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.38 , 1, clause( 8212, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =(
% 33.98/34.38 identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8288, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 33.98/34.38 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c1' ), identity ) ] )
% 33.98/34.38 , clause( 8222, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c1' ),
% 33.98/34.38 identity ), =( identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8294, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 33.98/34.38 'sk_c6' ) ] )
% 33.98/34.38 , clause( 8288, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity
% 33.98/34.38 , 'sk_c6' ), =( multiply( 'sk_c7', 'sk_c1' ), identity ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 subsumption(
% 33.98/34.38 clause( 181, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 33.98/34.38 'sk_c6' ) ] )
% 33.98/34.38 , clause( 8294, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity
% 33.98/34.38 , 'sk_c6' ) ] )
% 33.98/34.38 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.38 ).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8355, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 33.98/34.38 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.38 , clause( 24, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 33.98/34.38 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.38 , 0, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8358, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.38 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8359, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( multiply(
% 33.98/34.38 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.38 , clause( 44, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( multiply(
% 33.98/34.38 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.38 , 0, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8365, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =( identity,
% 33.98/34.38 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 8355, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 33.98/34.38 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.38 , 1, clause( 8358, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8366, [ =( identity, 'sk_c5' ), =( identity, multiply( 'sk_c7',
% 33.98/34.38 'sk_c1' ) ), =( identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 8359, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( multiply(
% 33.98/34.38 'sk_c3', 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.38 , 1, clause( 8365, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =(
% 33.98/34.38 identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8367, [ =( identity, 'sk_c5' ), =( identity, multiply( 'sk_c7',
% 33.98/34.38 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 8366, [ =( identity, 'sk_c5' ), =( identity, multiply( 'sk_c7',
% 33.98/34.38 'sk_c1' ) ), =( identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , 1, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8411, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c1' ),
% 33.98/34.38 identity ), =( identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 181, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 33.98/34.38 'sk_c6' ) ] )
% 33.98/34.38 , 1, clause( 8367, [ =( identity, 'sk_c5' ), =( identity, multiply( 'sk_c7'
% 33.98/34.38 , 'sk_c1' ) ) ] )
% 33.98/34.38 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8449, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c6',
% 33.98/34.38 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c1' ), identity ) ] )
% 33.98/34.38 , clause( 8411, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c1' ),
% 33.98/34.38 identity ), =( identity, multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 33.98/34.38 , 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8607, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c6',
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , clause( 8449, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c6',
% 33.98/34.38 'sk_c5' ), =( multiply( 'sk_c7', 'sk_c1' ), identity ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 subsumption(
% 33.98/34.38 clause( 183, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c6',
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , clause( 8607, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( 'sk_c6',
% 33.98/34.38 'sk_c5' ) ] )
% 33.98/34.38 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.38 ).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8609, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.38 'sk_c7' ) ] )
% 33.98/34.38 , clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.98/34.38 'sk_c7' ) ] )
% 33.98/34.38 , 1, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8611, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.38 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8617, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c7',
% 33.98/34.38 inverse( 'sk_c3' ) ) ] )
% 33.98/34.38 , clause( 8609, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.38 'sk_c7' ) ] )
% 33.98/34.38 , 1, clause( 8611, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8626, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c3' ), 'sk_c7' ),
% 33.98/34.38 =( 'sk_c7', inverse( 'sk_c3' ) ) ] )
% 33.98/34.38 , clause( 4, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.98/34.38 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.38 , 0, clause( 8617, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 33.98/34.38 'sk_c7', inverse( 'sk_c3' ) ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8646, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ),
% 33.98/34.38 =( inverse( 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.38 , clause( 8626, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c3' ), 'sk_c7' )
% 33.98/34.38 , =( 'sk_c7', inverse( 'sk_c3' ) ) ] )
% 33.98/34.38 , 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8769, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ) ]
% 33.98/34.38 )
% 33.98/34.38 , clause( 8646, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' )
% 33.98/34.38 , =( inverse( 'sk_c3' ), 'sk_c7' ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 subsumption(
% 33.98/34.38 clause( 184, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ) ]
% 33.98/34.38 )
% 33.98/34.38 , clause( 8769, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' )
% 33.98/34.38 ] )
% 33.98/34.38 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.38 ).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8770, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 33.98/34.38 'sk_c7' ) ] )
% 33.98/34.38 , clause( 8, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 33.98/34.38 'sk_c7' ) ] )
% 33.98/34.38 , 0, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8773, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.38 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8777, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =( 'sk_c7',
% 33.98/34.38 inverse( 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 8770, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 33.98/34.38 'sk_c7' ) ] )
% 33.98/34.38 , 1, clause( 8773, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.38 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 paramod(
% 33.98/34.38 clause( 8787, [ =( identity, 'sk_c5' ), =( inverse( 'sk_c1' ), 'sk_c7' ),
% 33.98/34.38 =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.38 , clause( 7, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 33.98/34.38 'sk_c7' ), 'sk_c5' ) ] )
% 33.98/34.38 , 1, clause( 8777, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =(
% 33.98/34.38 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.38 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 eqswap(
% 33.98/34.38 clause( 8853, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' ),
% 33.98/34.38 =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.38 , clause( 8787, [ =( identity, 'sk_c5' ), =( inverse( 'sk_c1' ), 'sk_c7' )
% 33.98/34.38 , =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.38 , 2, substitution( 0, [] )).
% 33.98/34.38
% 33.98/34.38
% 33.98/34.38 factor(
% 33.98/34.38 clause( 8859, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' ) ]
% 33.98/34.38 )
% 33.98/34.38 , clause( 8853, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' )
% 33.98/34.39 , =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 185, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 8859, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' )
% 33.98/34.39 ] )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 8929, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.39 'sk_c7' ) ] )
% 33.98/34.39 , clause( 10, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.98/34.39 'sk_c5' ) ] )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 8931, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.39 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 8937, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c5',
% 33.98/34.39 inverse( 'sk_c4' ) ) ] )
% 33.98/34.39 , clause( 8929, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 33.98/34.39 'sk_c7' ) ] )
% 33.98/34.39 , 1, clause( 8931, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.39 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 8946, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c4' ), 'sk_c5' ),
% 33.98/34.39 =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 33.98/34.39 , clause( 6, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 33.98/34.39 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.39 , 0, clause( 8937, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 33.98/34.39 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 8966, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ),
% 33.98/34.39 =( inverse( 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.39 , clause( 8946, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c4' ), 'sk_c5' )
% 33.98/34.39 , =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 33.98/34.39 , 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 factor(
% 33.98/34.39 clause( 9089, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 8966, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' )
% 33.98/34.39 , =( inverse( 'sk_c4' ), 'sk_c5' ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 186, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9089, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' )
% 33.98/34.39 ] )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9090, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c4' ),
% 33.98/34.39 'sk_c5' ) ] )
% 33.98/34.39 , clause( 10, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 33.98/34.39 'sk_c5' ) ] )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9093, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.39 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9094, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c4',
% 33.98/34.39 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.39 , clause( 9, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 33.98/34.39 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9100, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =( 'sk_c7',
% 33.98/34.39 inverse( 'sk_c1' ) ) ] )
% 33.98/34.39 , clause( 9090, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c4' ),
% 33.98/34.39 'sk_c5' ) ] )
% 33.98/34.39 , 1, clause( 9093, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.39 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9101, [ =( identity, 'sk_c6' ), =( 'sk_c7', inverse( 'sk_c1' ) ),
% 33.98/34.39 =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.39 , clause( 9094, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c4',
% 33.98/34.39 'sk_c5' ), 'sk_c6' ) ] )
% 33.98/34.39 , 1, clause( 9100, [ =( identity, multiply( 'sk_c4', 'sk_c5' ) ), =(
% 33.98/34.39 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 factor(
% 33.98/34.39 clause( 9102, [ =( identity, 'sk_c6' ), =( 'sk_c7', inverse( 'sk_c1' ) ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9101, [ =( identity, 'sk_c6' ), =( 'sk_c7', inverse( 'sk_c1' ) )
% 33.98/34.39 , =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.39 , 1, 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9112, [ =( 'sk_c5', 'sk_c6' ), =( inverse( 'sk_c1' ), 'sk_c7' ),
% 33.98/34.39 =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.39 , clause( 185, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c5' ) ]
% 33.98/34.39 )
% 33.98/34.39 , 1, clause( 9102, [ =( identity, 'sk_c6' ), =( 'sk_c7', inverse( 'sk_c1' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9178, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c5', 'sk_c6' ),
% 33.98/34.39 =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.39 , clause( 9112, [ =( 'sk_c5', 'sk_c6' ), =( inverse( 'sk_c1' ), 'sk_c7' ),
% 33.98/34.39 =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 33.98/34.39 , 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9179, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c1' ), 'sk_c7' ),
% 33.98/34.39 =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.39 , clause( 9178, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c5', 'sk_c6' ),
% 33.98/34.39 =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 factor(
% 33.98/34.39 clause( 9183, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c1' ), 'sk_c7' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9179, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c1' ), 'sk_c7' ),
% 33.98/34.39 =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 33.98/34.39 , 1, 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 187, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c6', 'sk_c5' ) ] )
% 33.98/34.39 , clause( 9183, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c1' ), 'sk_c7' ) ]
% 33.98/34.39 )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9240, [ =( 'sk_c6', identity ), =( inverse( 'sk_c3' ), 'sk_c7' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 184, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9242, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.39 , clause( 157, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9248, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =( 'sk_c6',
% 33.98/34.39 identity ) ] )
% 33.98/34.39 , clause( 9240, [ =( 'sk_c6', identity ), =( inverse( 'sk_c3' ), 'sk_c7' )
% 33.98/34.39 ] )
% 33.98/34.39 , 1, clause( 9242, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 33.98/34.39 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9269, [ =( identity, 'sk_c5' ), =( identity, 'sk_c6' ), =( 'sk_c6'
% 33.98/34.39 , identity ) ] )
% 33.98/34.39 , clause( 176, [ =( multiply( 'sk_c3', 'sk_c7' ), 'sk_c5' ), =( identity,
% 33.98/34.39 'sk_c6' ) ] )
% 33.98/34.39 , 0, clause( 9248, [ =( identity, multiply( 'sk_c3', 'sk_c7' ) ), =(
% 33.98/34.39 'sk_c6', identity ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9293, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ), =( identity
% 33.98/34.39 , 'sk_c6' ) ] )
% 33.98/34.39 , clause( 9269, [ =( identity, 'sk_c5' ), =( identity, 'sk_c6' ), =(
% 33.98/34.39 'sk_c6', identity ) ] )
% 33.98/34.39 , 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 factor(
% 33.98/34.39 clause( 9452, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 9293, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ), =(
% 33.98/34.39 identity, 'sk_c6' ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 188, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 9452, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9454, [ =( 'sk_c6', identity ), =( inverse( 'sk_c3' ), 'sk_c7' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 184, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9456, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.39 , clause( 158, [ =( inverse( inverse( X ) ), X ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9457, [ =( 'sk_c3', inverse( 'sk_c7' ) ), =( 'sk_c6', identity ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9454, [ =( 'sk_c6', identity ), =( inverse( 'sk_c3' ), 'sk_c7' )
% 33.98/34.39 ] )
% 33.98/34.39 , 1, clause( 9456, [ =( X, inverse( inverse( X ) ) ) ] )
% 33.98/34.39 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9459, [ =( identity, 'sk_c6' ), =( 'sk_c3', inverse( 'sk_c7' ) ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9457, [ =( 'sk_c3', inverse( 'sk_c7' ) ), =( 'sk_c6', identity )
% 33.98/34.39 ] )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9460, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9459, [ =( identity, 'sk_c6' ), =( 'sk_c3', inverse( 'sk_c7' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 189, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9460, [ =( inverse( 'sk_c7' ), 'sk_c3' ), =( identity, 'sk_c6' )
% 33.98/34.39 ] )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9461, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 184, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( identity, 'sk_c6' ) ]
% 33.98/34.39 )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9464, [ =( X, multiply( inverse( inverse( identity ) ), X ) ) ] )
% 33.98/34.39 , clause( 73, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9466, [ =( X, multiply( inverse( inverse( 'sk_c6' ) ), X ) ), =(
% 33.98/34.39 'sk_c7', inverse( 'sk_c3' ) ) ] )
% 33.98/34.39 , clause( 9461, [ =( 'sk_c7', inverse( 'sk_c3' ) ), =( identity, 'sk_c6' )
% 33.98/34.39 ] )
% 33.98/34.39 , 1, clause( 9464, [ =( X, multiply( inverse( inverse( identity ) ), X ) )
% 33.98/34.39 ] )
% 33.98/34.39 , 0, 5, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9467, [ =( X, multiply( 'sk_c6', X ) ), =( 'sk_c7', inverse(
% 33.98/34.39 'sk_c3' ) ) ] )
% 33.98/34.39 , clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 33.98/34.39 ) ) ] )
% 33.98/34.39 , 0, clause( 9466, [ =( X, multiply( inverse( inverse( 'sk_c6' ) ), X ) ),
% 33.98/34.39 =( 'sk_c7', inverse( 'sk_c3' ) ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [ :=( X, 'sk_c6' ), :=( Y, X )] ), substitution( 1
% 33.98/34.39 , [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9469, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( X, multiply( 'sk_c6',
% 33.98/34.39 X ) ) ] )
% 33.98/34.39 , clause( 9467, [ =( X, multiply( 'sk_c6', X ) ), =( 'sk_c7', inverse(
% 33.98/34.39 'sk_c3' ) ) ] )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9470, [ =( multiply( 'sk_c6', X ), X ), =( inverse( 'sk_c3' ),
% 33.98/34.39 'sk_c7' ) ] )
% 33.98/34.39 , clause( 9469, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( X, multiply( 'sk_c6'
% 33.98/34.39 , X ) ) ] )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 193, [ =( inverse( 'sk_c3' ), 'sk_c7' ), =( multiply( 'sk_c6', X )
% 33.98/34.39 , X ) ] )
% 33.98/34.39 , clause( 9470, [ =( multiply( 'sk_c6', X ), X ), =( inverse( 'sk_c3' ),
% 33.98/34.39 'sk_c7' ) ] )
% 33.98/34.39 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 33.98/34.39 0 )] ) ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqfact(
% 33.98/34.39 clause( 9474, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 188, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 0, 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 194, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 9474, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9482, [ ~( =( 'sk_c5', 'sk_c6' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 194, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9485, [ =( X, multiply( X, identity ) ) ] )
% 33.98/34.39 , clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9486, [ =( X, multiply( X, 'sk_c5' ) ), ~( =( 'sk_c5', 'sk_c6' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 9482, [ ~( =( 'sk_c5', 'sk_c6' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 1, clause( 9485, [ =( X, multiply( X, identity ) ) ] )
% 33.98/34.39 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9488, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( X, multiply( X, 'sk_c5' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 9486, [ =( X, multiply( X, 'sk_c5' ) ), ~( =( 'sk_c5', 'sk_c6' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9489, [ =( multiply( X, 'sk_c5' ), X ), ~( =( 'sk_c6', 'sk_c5' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 9488, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( X, multiply( X, 'sk_c5' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 196, [ =( multiply( X, 'sk_c5' ), X ), ~( =( 'sk_c6', 'sk_c5' ) ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9489, [ =( multiply( X, 'sk_c5' ), X ), ~( =( 'sk_c6', 'sk_c5' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 33.98/34.39 1 )] ) ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9493, [ =( identity, inverse( identity ) ) ] )
% 33.98/34.39 , clause( 122, [ =( inverse( identity ), identity ) ] )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9519, [ =( identity, inverse( 'sk_c5' ) ), ~( =( 'sk_c6', 'sk_c5' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , clause( 194, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 1, clause( 9493, [ =( identity, inverse( identity ) ) ] )
% 33.98/34.39 , 0, 3, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9520, [ =( 'sk_c5', inverse( 'sk_c5' ) ), ~( =( 'sk_c6', 'sk_c5' )
% 33.98/34.39 ), ~( =( 'sk_c6', 'sk_c5' ) ) ] )
% 33.98/34.39 , clause( 194, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 1, clause( 9519, [ =( identity, inverse( 'sk_c5' ) ), ~( =( 'sk_c6',
% 33.98/34.39 'sk_c5' ) ) ] )
% 33.98/34.39 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9524, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( 'sk_c6', 'sk_c5' )
% 33.98/34.39 ), ~( =( 'sk_c6', 'sk_c5' ) ) ] )
% 33.98/34.39 , clause( 9520, [ =( 'sk_c5', inverse( 'sk_c5' ) ), ~( =( 'sk_c6', 'sk_c5'
% 33.98/34.39 ) ), ~( =( 'sk_c6', 'sk_c5' ) ) ] )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 factor(
% 33.98/34.39 clause( 9528, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( 'sk_c6', 'sk_c5' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , clause( 9524, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( 'sk_c6', 'sk_c5'
% 33.98/34.39 ) ), ~( =( 'sk_c6', 'sk_c5' ) ) ] )
% 33.98/34.39 , 1, 2, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 197, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( 'sk_c6', 'sk_c5' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 9528, [ =( inverse( 'sk_c5' ), 'sk_c5' ), ~( =( 'sk_c6', 'sk_c5'
% 33.98/34.39 ) ) ] )
% 33.98/34.39 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 33.98/34.39 ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9530, [ ~( =( 'sk_c5', 'sk_c6' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 194, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 0, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9533, [ =( X, multiply( inverse( inverse( identity ) ), X ) ) ] )
% 33.98/34.39 , clause( 73, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9535, [ =( X, multiply( inverse( inverse( 'sk_c5' ) ), X ) ), ~(
% 33.98/34.39 =( 'sk_c5', 'sk_c6' ) ) ] )
% 33.98/34.39 , clause( 9530, [ ~( =( 'sk_c5', 'sk_c6' ) ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 1, clause( 9533, [ =( X, multiply( inverse( inverse( identity ) ), X ) )
% 33.98/34.39 ] )
% 33.98/34.39 , 0, 5, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9536, [ =( X, multiply( 'sk_c5', X ) ), ~( =( 'sk_c5', 'sk_c6' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 126, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 33.98/34.39 ) ) ] )
% 33.98/34.39 , 0, clause( 9535, [ =( X, multiply( inverse( inverse( 'sk_c5' ) ), X ) ),
% 33.98/34.39 ~( =( 'sk_c5', 'sk_c6' ) ) ] )
% 33.98/34.39 , 0, 2, substitution( 0, [ :=( X, 'sk_c5' ), :=( Y, X )] ), substitution( 1
% 33.98/34.39 , [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9538, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( X, multiply( 'sk_c5', X ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 9536, [ =( X, multiply( 'sk_c5', X ) ), ~( =( 'sk_c5', 'sk_c6' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9539, [ =( multiply( 'sk_c5', X ), X ), ~( =( 'sk_c6', 'sk_c5' ) )
% 33.98/34.39 ] )
% 33.98/34.39 , clause( 9538, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( X, multiply( 'sk_c5', X )
% 33.98/34.39 ) ] )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 198, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( multiply( 'sk_c5', X ), X ) ]
% 33.98/34.39 )
% 33.98/34.39 , clause( 9539, [ =( multiply( 'sk_c5', X ), X ), ~( =( 'sk_c6', 'sk_c5' )
% 33.98/34.39 ) ] )
% 33.98/34.39 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 33.98/34.39 0 )] ) ).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9541, [ =( 'sk_c5', identity ), =( identity, 'sk_c6' ) ] )
% 33.98/34.39 , clause( 188, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , 1, substitution( 0, [] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9543, [ =( X, multiply( X, identity ) ) ] )
% 33.98/34.39 , clause( 141, [ =( multiply( X, identity ), X ) ] )
% 33.98/34.39 , 0, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 paramod(
% 33.98/34.39 clause( 9640, [ =( X, multiply( X, 'sk_c6' ) ), =( 'sk_c5', identity ) ] )
% 33.98/34.39 , clause( 9541, [ =( 'sk_c5', identity ), =( identity, 'sk_c6' ) ] )
% 33.98/34.39 , 1, clause( 9543, [ =( X, multiply( X, identity ) ) ] )
% 33.98/34.39 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9686, [ =( identity, 'sk_c5' ), =( X, multiply( X, 'sk_c6' ) ) ] )
% 33.98/34.39 , clause( 9640, [ =( X, multiply( X, 'sk_c6' ) ), =( 'sk_c5', identity ) ]
% 33.98/34.39 )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 eqswap(
% 33.98/34.39 clause( 9687, [ =( multiply( X, 'sk_c6' ), X ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 9686, [ =( identity, 'sk_c5' ), =( X, multiply( X, 'sk_c6' ) ) ]
% 33.98/34.39 )
% 33.98/34.39 , 1, substitution( 0, [ :=( X, X )] )).
% 33.98/34.39
% 33.98/34.39
% 33.98/34.39 subsumption(
% 33.98/34.39 clause( 199, [ =( multiply( X, 'sk_c6' ), X ), =( identity, 'sk_c5' ) ] )
% 33.98/34.39 , clause( 9687, [ =( multiply( X, 'sk_c6' ), X ), =( identity, 'sk_c5' ) ]
% 34.05/34.40 )
% 34.05/34.40 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 34.05/34.40 1 )] ) ).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 eqswap(
% 34.05/34.40 clause( 9688, [ =( 'sk_c6', identity ), =( identity, 'sk_c5' ) ] )
% 34.05/34.40 , clause( 188, [ =( identity, 'sk_c6' ), =( identity, 'sk_c5' ) ] )
% 34.05/34.40 , 0, substitution( 0, [] )).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 eqswap(
% 34.05/34.40 clause( 9691, [ =( X, multiply( X, identity ) ) ] )
% 34.05/34.40 , clause( 141, [ =( multiply( X, identity ), X ) ] )
% 34.05/34.40 , 0, substitution( 0, [ :=( X, X )] )).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 paramod(
% 34.05/34.40 clause( 9692, [ =( X, multiply( X, 'sk_c5' ) ), =( 'sk_c6', identity ) ] )
% 34.05/34.40 , clause( 9688, [ =( 'sk_c6', identity ), =( identity, 'sk_c5' ) ] )
% 34.05/34.40 , 1, clause( 9691, [ =( X, multiply( X, identity ) ) ] )
% 34.05/34.40 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 eqswap(
% 34.05/34.40 clause( 9738, [ =( identity, 'sk_c6' ), =( X, multiply( X, 'sk_c5' ) ) ] )
% 34.05/34.40 , clause( 9692, [ =( X, multiply( X, 'sk_c5' ) ), =( 'sk_c6', identity ) ]
% 34.05/34.40 )
% 34.05/34.40 , 1, substitution( 0, [ :=( X, X )] )).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 eqswap(
% 34.05/34.40 clause( 9739, [ =( multiply( X, 'sk_c5' ), X ), =( identity, 'sk_c6' ) ] )
% 34.05/34.40 , clause( 9738, [ =( identity, 'sk_c6' ), =( X, multiply( X, 'sk_c5' ) ) ]
% 34.05/34.40 )
% 34.05/34.40 , 1, substitution( 0, [ :=( X, X )] )).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 subsumption(
% 34.05/34.40 clause( 200, [ =( multiply( X, 'sk_c5' ), X ), =( identity, 'sk_c6' ) ] )
% 34.05/34.40 , clause( 9739, [ =( multiply( X, 'sk_c5' ), X ), =( identity, 'sk_c6' ) ]
% 34.05/34.40 )
% 34.05/34.40 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 34.05/34.40 1 )] ) ).
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 ==> clause( 201, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( identity, 'sk_c5' )
% 34.05/34.40 ] )
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40
% 34.05/34.40 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 34.05/34.40
% 34.05/34.40 Bliksem ended
%------------------------------------------------------------------------------