%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP351-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n003.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:36 EDT 2022
% Result : Unsatisfiable 0.73s 1.21s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP351-1 : TPTP v8.1.0. Released v2.5.0.
% 0.06/0.13 % Command : bliksem %s
% 0.12/0.33 % Computer : n003.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.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Tue Jun 14 03:59:10 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.73/1.21 *** allocated 10000 integers for termspace/termends
% 0.73/1.21 *** allocated 10000 integers for clauses
% 0.73/1.21 *** allocated 10000 integers for justifications
% 0.73/1.21 Bliksem 1.12
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 Automatic Strategy Selection
% 0.73/1.21
% 0.73/1.21 Clauses:
% 0.73/1.21 [
% 0.73/1.21 [ =( multiply( identity, X ), X ) ],
% 0.73/1.21 [ =( multiply( inverse( X ), X ), identity ) ],
% 0.73/1.21 [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply( Y, Z ) ) )
% 0.73/1.21 ],
% 0.73/1.21 [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ],
% 0.73/1.21 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c6', 'sk_c7' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3', 'sk_c6' ),
% 0.73/1.21 'sk_c7' ) ],
% 0.73/1.21 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ), 'sk_c6' ) ]
% 0.73/1.21 ,
% 0.73/1.21 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ), 'sk_c5' ) ]
% 0.73/1.21 ,
% 0.73/1.21 [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4', 'sk_c6' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ],
% 0.73/1.21 [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c6', 'sk_c7' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c6' ),
% 0.73/1.21 'sk_c7' ) ],
% 0.73/1.21 [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ), 'sk_c6' ) ]
% 0.73/1.21 ,
% 0.73/1.21 [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ), 'sk_c5' ) ]
% 0.73/1.21 ,
% 0.73/1.21 [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4', 'sk_c6' ),
% 0.73/1.21 'sk_c5' ) ],
% 0.73/1.21 [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =( multiply( X,
% 0.73/1.21 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~( =( multiply(
% 0.73/1.21 Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ), ~( =(
% 0.73/1.21 multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z, 'sk_c6' ),
% 0.73/1.21 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( T ), 'sk_c5'
% 0.73/1.21 ) ), ~( =( multiply( T, 'sk_c6' ), 'sk_c5' ) ) ]
% 0.73/1.21 ] .
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 percentage equality = 1.000000, percentage horn = 0.137931
% 0.73/1.21 This is a pure equality problem
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 Options Used:
% 0.73/1.21
% 0.73/1.21 useres = 1
% 0.73/1.21 useparamod = 1
% 0.73/1.21 useeqrefl = 1
% 0.73/1.21 useeqfact = 1
% 0.73/1.21 usefactor = 1
% 0.73/1.21 usesimpsplitting = 0
% 0.73/1.21 usesimpdemod = 5
% 0.73/1.21 usesimpres = 3
% 0.73/1.21
% 0.73/1.21 resimpinuse = 1000
% 0.73/1.21 resimpclauses = 20000
% 0.73/1.21 substype = eqrewr
% 0.73/1.21 backwardsubs = 1
% 0.73/1.21 selectoldest = 5
% 0.73/1.21
% 0.73/1.21 litorderings [0] = split
% 0.73/1.21 litorderings [1] = extend the termordering, first sorting on arguments
% 0.73/1.21
% 0.73/1.21 termordering = kbo
% 0.73/1.21
% 0.73/1.21 litapriori = 0
% 0.73/1.21 termapriori = 1
% 0.73/1.21 litaposteriori = 0
% 0.73/1.21 termaposteriori = 0
% 0.73/1.21 demodaposteriori = 0
% 0.73/1.21 ordereqreflfact = 0
% 0.73/1.21
% 0.73/1.21 litselect = negord
% 0.73/1.21
% 0.73/1.21 maxweight = 15
% 0.73/1.21 maxdepth = 30000
% 0.73/1.21 maxlength = 115
% 0.73/1.21 maxnrvars = 195
% 0.73/1.21 excuselevel = 1
% 0.73/1.21 increasemaxweight = 1
% 0.73/1.21
% 0.73/1.21 maxselected = 10000000
% 0.73/1.21 maxnrclauses = 10000000
% 0.73/1.21
% 0.73/1.21 showgenerated = 0
% 0.73/1.21 showkept = 0
% 0.73/1.21 showselected = 0
% 0.73/1.21 showdeleted = 0
% 0.73/1.21 showresimp = 1
% 0.73/1.21 showstatus = 2000
% 0.73/1.21
% 0.73/1.21 prologoutput = 1
% 0.73/1.21 nrgoals = 5000000
% 0.73/1.21 totalproof = 1
% 0.73/1.21
% 0.73/1.21 Symbols occurring in the translation:
% 0.73/1.21
% 0.73/1.21 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.21 . [1, 2] (w:1, o:30, a:1, s:1, b:0),
% 0.73/1.21 ! [4, 1] (w:0, o:24, a:1, s:1, b:0),
% 0.73/1.21 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.21 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.21 identity [39, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.73/1.21 multiply [41, 2] (w:1, o:55, a:1, s:1, b:0),
% 0.73/1.21 inverse [42, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.73/1.21 'sk_c6' [45, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.73/1.21 'sk_c5' [46, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.73/1.21 'sk_c7' [47, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.73/1.21 'sk_c3' [48, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.73/1.21 'sk_c4' [49, 0] (w:1, o:5, a:1, s:1, b:0),
% 0.73/1.21 'sk_c1' [50, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.73/1.21 'sk_c2' [51, 0] (w:1, o:9, a:1, s:1, b:0).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 Starting Search:
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 Bliksems!, er is een bewijs:
% 0.73/1.21 % SZS status Unsatisfiable
% 0.73/1.21 % SZS output start Refutation
% 0.73/1.21
% 0.73/1.21 clause( 0, [ =( multiply( identity, X ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 0.73/1.21 , Z ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 3, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 4, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 5, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 7, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 8, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 9, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 10, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 11, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 12, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 13, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 14, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 15, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 16, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 17, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 18, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 19, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 20, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 21, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 23, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 24, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 25, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 26, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 27, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 28, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 0.73/1.21 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 0.73/1.21 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 0.73/1.21 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( T
% 0.73/1.21 ), 'sk_c5' ) ), ~( =( multiply( T, 'sk_c6' ), 'sk_c5' ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 30, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 0.73/1.21 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 0.73/1.21 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 0.73/1.21 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( Y
% 0.73/1.21 ), 'sk_c5' ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 35, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 37, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y )
% 0.73/1.21 , identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 38, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y,
% 0.73/1.21 identity ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 39, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X ) )
% 0.73/1.21 ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 40, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 43, [ =( multiply( 'sk_c6', 'sk_c3' ), identity ), =( multiply(
% 0.73/1.21 'sk_c7', 'sk_c1' ), identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 46, [ =( multiply( 'sk_c5', 'sk_c4' ), identity ), =( multiply(
% 0.73/1.21 'sk_c7', 'sk_c1' ), identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 59, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 61, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 63, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 82, [ =( multiply( inverse( identity ), X ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 85, [ =( multiply( multiply( Y, inverse( identity ) ), X ),
% 0.73/1.21 multiply( Y, X ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 130, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 194, [ =( inverse( identity ), identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 197, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y )
% 0.73/1.21 ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 227, [ =( multiply( X, identity ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 248, [ =( multiply( inverse( 'sk_c7' ), X ), multiply( 'sk_c1', X )
% 0.73/1.21 ), =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 252, [ =( multiply( inverse( 'sk_c5' ), X ), multiply( 'sk_c4', X )
% 0.73/1.21 ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 258, [ =( inverse( inverse( X ) ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 288, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 0.73/1.21 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 292, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 298, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( 'sk_c6',
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 308, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 309, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 310, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 312, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 313, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( identity, 'sk_c7' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 314, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 316, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 318, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 319, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 323, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c6' ),
% 0.73/1.21 'sk_c3' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 325, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( 'sk_c6' ),
% 0.73/1.21 'sk_c3' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 326, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( multiply( 'sk_c5', X )
% 0.73/1.21 , X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 327, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 328, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( identity, 'sk_c7' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 329, [ =( multiply( X, 'sk_c7' ), X ), =( inverse( 'sk_c1' ),
% 0.73/1.21 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 333, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( identity, 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 334, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c7', 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 336, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 337, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c1', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 340, [ =( multiply( X, 'sk_c6' ), X ), ~( =( 'sk_c7', 'sk_c6' ) ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 341, [ =( inverse( 'sk_c6' ), 'sk_c6' ), ~( =( 'sk_c7', 'sk_c6' ) )
% 0.73/1.21 ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 342, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( multiply( 'sk_c6', X ), X ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 344, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c2', 'sk_c5' ), =(
% 0.73/1.21 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 347, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c6', 'sk_c5' ), =(
% 0.73/1.21 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 351, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 382, [ =( multiply( X, 'sk_c6' ), X ), =( identity, 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 384, [ =( inverse( 'sk_c6' ), 'sk_c6' ), =( identity, 'sk_c7' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 386, [ =( identity, 'sk_c7' ), =( multiply( 'sk_c6', X ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 391, [ =( 'sk_c3', 'sk_c6' ), =( identity, 'sk_c7' ), =( 'sk_c6',
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 395, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( inverse( 'sk_c5' ), 'sk_c5' )
% 0.73/1.21 ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 403, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 427, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( 'sk_c1', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 431, [ =( 'sk_c7', 'sk_c5' ), =( inverse( 'sk_c6' ), 'sk_c3' ), =(
% 0.73/1.21 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 435, [ =( identity, 'sk_c7' ), =( 'sk_c3', 'sk_c6' ), =( 'sk_c3',
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 436, [ =( identity, 'sk_c7' ), =( 'sk_c3', 'sk_c6' ), =( 'sk_c5',
% 0.73/1.21 'sk_c4' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 446, [ =( identity, 'sk_c7' ), =( 'sk_c3', 'sk_c6' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 447, [ =( 'sk_c7', 'sk_c5' ), =( inverse( 'sk_c6' ), 'sk_c3' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 465, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( 'sk_c6', 'sk_c5' ), =(
% 0.73/1.21 inverse( 'sk_c6' ), 'sk_c3' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 469, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 477, [ =( 'sk_c6', 'sk_c5' ), =( identity, 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 481, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( identity, 'sk_c7' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 498, [ =( multiply( X, 'sk_c7' ), X ), =( inverse( 'sk_c5' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 500, [ =( inverse( 'sk_c7' ), 'sk_c7' ), =( inverse( 'sk_c5' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 534, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( identity, 'sk_c5' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 538, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( 'sk_c1', 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 546, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 577, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c5' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 579, [ =( multiply( 'sk_c4', 'sk_c5' ), identity ), =( identity,
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 580, [ =( inverse( 'sk_c5' ), 'sk_c4' ), =( identity, 'sk_c5' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 619, [ =( identity, 'sk_c7' ), =( inverse( 'sk_c2' ), 'sk_c5' ) ]
% 0.73/1.21 )
% 0.73/1.21 .
% 0.73/1.21 clause( 622, [ =( identity, 'sk_c7' ), =( 'sk_c2', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 632, [ =( identity, 'sk_c7' ), =( 'sk_c5', 'sk_c4' ), =( 'sk_c7',
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 633, [ =( identity, 'sk_c7' ), =( 'sk_c7', 'sk_c5' ), =( 'sk_c7',
% 0.73/1.21 'sk_c4' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 635, [ =( identity, 'sk_c7' ), =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 636, [ =( inverse( 'sk_c5' ), 'sk_c4' ), =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 638, [ =( multiply( X, 'sk_c7' ), X ), =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 639, [ =( 'sk_c7', 'sk_c5' ), =( 'sk_c1', 'sk_c7' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 656, [ =( 'sk_c7', 'sk_c5' ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 666, [ =( 'sk_c7', 'sk_c5' ), =( 'sk_c3', 'sk_c4' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 667, [ ~( =( 'sk_c6', 'sk_c5' ) ), =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 672, [ =( multiply( 'sk_c4', 'sk_c5' ), 'sk_c5' ), =( 'sk_c7',
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 675, [ =( 'sk_c7', 'sk_c5' ), =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 677, [ =( 'sk_c7', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 681, [ =( inverse( 'sk_c5' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 695, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 696, [ =( 'sk_c5', 'sk_c4' ), =( identity, 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 697, [ =( multiply( 'sk_c5', 'sk_c5' ), identity ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 728, [ =( identity, 'sk_c5' ), =( identity, 'sk_c4' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 739, [ =( identity, 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 740, [ =( multiply( X, 'sk_c5' ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 741, [ =( multiply( 'sk_c5', X ), X ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 743, [ =( 'sk_c6', 'sk_c5' ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 750, [ ~( =( inverse( X ), 'sk_c5' ) ), ~( =( X, 'sk_c5' ) ), ~(
% 0.73/1.21 =( inverse( Y ), 'sk_c5' ) ), ~( =( Y, 'sk_c5' ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 751, [ ~( =( inverse( X ), 'sk_c5' ) ), ~( =( X, 'sk_c5' ) ) ] )
% 0.73/1.21 .
% 0.73/1.21 clause( 752, [] )
% 0.73/1.21 .
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 % SZS output end Refutation
% 0.73/1.21 found a proof!
% 0.73/1.21
% 0.73/1.21 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 0.73/1.21
% 0.73/1.21 initialclauses(
% 0.73/1.21 [ clause( 754, [ =( multiply( identity, X ), X ) ] )
% 0.73/1.21 , clause( 755, [ =( multiply( inverse( X ), X ), identity ) ] )
% 0.73/1.21 , clause( 756, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 0.73/1.21 Y, Z ) ) ) ] )
% 0.73/1.21 , clause( 757, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 758, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 759, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , clause( 760, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 761, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 762, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 763, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 764, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , clause( 765, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 766, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 767, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 768, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 769, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 , clause( 770, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 , clause( 771, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 772, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 773, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 774, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , clause( 775, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 776, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 777, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 778, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 779, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 , clause( 780, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 , clause( 781, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 0.73/1.21 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 782, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 0.73/1.21 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 0.73/1.21 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 0.73/1.21 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( T
% 0.73/1.21 ), 'sk_c5' ) ), ~( =( multiply( T, 'sk_c6' ), 'sk_c5' ) ) ] )
% 0.73/1.21 ] ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 0, [ =( multiply( identity, X ), X ) ] )
% 0.73/1.21 , clause( 754, [ =( multiply( identity, X ), X ) ] )
% 0.73/1.21 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 0.73/1.21 , clause( 755, [ =( multiply( inverse( X ), X ), identity ) ] )
% 0.73/1.21 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 eqswap(
% 0.73/1.21 clause( 788, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 0.73/1.21 ), Z ) ) ] )
% 0.73/1.21 , clause( 756, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 0.73/1.21 Y, Z ) ) ) ] )
% 0.73/1.21 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 0.73/1.21 , Z ) ) ] )
% 0.73/1.21 , clause( 788, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X
% 0.73/1.21 , Y ), Z ) ) ] )
% 0.73/1.21 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 0.73/1.21 permutation( 0, [ ==>( 0, 0 )] ) ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 3, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 757, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 4, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 758, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 5, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , clause( 759, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 7, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 761, [ =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 8, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 762, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 9, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 763, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 10, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , clause( 764, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c3' ), 'sk_c6' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 11, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 765, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 0.73/1.21 'sk_c4' ), 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 12, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 766, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 0.73/1.21 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 13, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , clause( 767, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c6',
% 0.73/1.21 'sk_c7' ), 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 14, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , clause( 768, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 0.73/1.21 'sk_c6' ), 'sk_c7' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 15, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 , clause( 769, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 0.73/1.21 'sk_c6' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 16, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 , clause( 770, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 0.73/1.21 'sk_c5' ) ] )
% 0.73/1.21 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 0.73/1.21 ).
% 0.73/1.21
% 0.73/1.21
% 0.73/1.21 subsumption(
% 0.73/1.21 clause( 17, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 5.28/5.68 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.68 , clause( 771, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 5.28/5.68 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 18, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 5.28/5.68 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.68 , clause( 772, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 5.28/5.68 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 19, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 5.28/5.68 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.68 , clause( 773, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 5.28/5.68 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 20, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 5.28/5.68 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.68 , clause( 774, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 5.28/5.68 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 21, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 5.28/5.68 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.68 , clause( 775, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 5.28/5.68 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 23, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c6',
% 5.28/5.68 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.68 , clause( 777, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c6',
% 5.28/5.68 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 24, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.68 , clause( 778, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 25, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 5.28/5.68 'sk_c6' ) ] )
% 5.28/5.68 , clause( 779, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 5.28/5.68 'sk_c6' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 26, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 5.28/5.68 'sk_c5' ) ] )
% 5.28/5.68 , clause( 780, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 5.28/5.68 'sk_c5' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 27, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 5.28/5.68 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.68 , clause( 781, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 5.28/5.68 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.68 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 28, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 5.28/5.68 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 5.28/5.68 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 5.28/5.68 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( T
% 5.28/5.68 ), 'sk_c5' ) ), ~( =( multiply( T, 'sk_c6' ), 'sk_c5' ) ) ] )
% 5.28/5.68 , clause( 782, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 5.28/5.68 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 5.28/5.68 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 5.28/5.68 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( T
% 5.28/5.68 ), 'sk_c5' ) ), ~( =( multiply( T, 'sk_c6' ), 'sk_c5' ) ) ] )
% 5.28/5.68 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 5.28/5.68 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 ),
% 5.28/5.68 ==>( 4, 4 ), ==>( 5, 5 ), ==>( 6, 6 ), ==>( 7, 7 ), ==>( 8, 8 ), ==>( 9,
% 5.28/5.68 9 )] ) ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 factor(
% 5.28/5.68 clause( 5165, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 5.28/5.68 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 5.28/5.68 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 5.28/5.68 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( Y
% 5.28/5.68 ), 'sk_c5' ) ) ] )
% 5.28/5.68 , clause( 28, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 5.28/5.68 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 5.28/5.68 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 5.28/5.68 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( T
% 5.28/5.68 ), 'sk_c5' ) ), ~( =( multiply( T, 'sk_c6' ), 'sk_c5' ) ) ] )
% 5.28/5.68 , 3, 9, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, Y )] )
% 5.28/5.68 ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 subsumption(
% 5.28/5.68 clause( 30, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 5.28/5.68 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 5.28/5.68 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 5.28/5.68 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( Y
% 5.28/5.68 ), 'sk_c5' ) ) ] )
% 5.28/5.68 , clause( 5165, [ ~( =( multiply( 'sk_c6', 'sk_c5' ), 'sk_c7' ) ), ~( =(
% 5.28/5.68 multiply( X, 'sk_c7' ), 'sk_c6' ) ), ~( =( inverse( X ), 'sk_c7' ) ), ~(
% 5.28/5.68 =( multiply( Y, 'sk_c6' ), 'sk_c5' ) ), ~( =( inverse( Y ), 'sk_c6' ) ),
% 5.28/5.68 ~( =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ) ), ~( =( multiply( Z,
% 5.28/5.68 'sk_c6' ), 'sk_c7' ) ), ~( =( inverse( Z ), 'sk_c6' ) ), ~( =( inverse( Y
% 5.28/5.68 ), 'sk_c5' ) ) ] )
% 5.28/5.68 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 5.28/5.68 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 ),
% 5.28/5.68 ==>( 4, 4 ), ==>( 5, 5 ), ==>( 6, 6 ), ==>( 7, 7 ), ==>( 8, 8 )] ) ).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 eqswap(
% 5.28/5.68 clause( 6446, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 5.28/5.68 'sk_c7' ) ] )
% 5.28/5.68 , clause( 16, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 5.28/5.68 'sk_c5' ) ] )
% 5.28/5.68 , 1, substitution( 0, [] )).
% 5.28/5.68
% 5.28/5.68
% 5.28/5.68 eqswap(
% 5.28/5.68 clause( 6448, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6457, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c5',
% 5.28/5.69 inverse( 'sk_c4' ) ) ] )
% 5.28/5.69 , clause( 6446, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , 1, clause( 6448, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6459, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , clause( 6457, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c5',
% 5.28/5.69 inverse( 'sk_c4' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6460, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 6459, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 35, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 6460, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6461, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 5.28/5.69 Y, Z ) ) ) ] )
% 5.28/5.69 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 5.28/5.69 ), Z ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6464, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y
% 5.28/5.69 ), identity ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6461, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 5.28/5.69 multiply( Y, Z ) ) ) ] )
% 5.28/5.69 , 0, 9, substitution( 0, [ :=( X, multiply( X, Y ) )] ), substitution( 1, [
% 5.28/5.69 :=( X, inverse( multiply( X, Y ) ) ), :=( Y, X ), :=( Z, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 37, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y )
% 5.28/5.69 , identity ) ] )
% 5.28/5.69 , clause( 6464, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ),
% 5.28/5.69 Y ), identity ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.28/5.69 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6470, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 5.28/5.69 Y, Z ) ) ) ] )
% 5.28/5.69 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 5.28/5.69 ), Z ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6475, [ =( multiply( multiply( X, inverse( Y ) ), Y ), multiply( X
% 5.28/5.69 , identity ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6470, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 5.28/5.69 multiply( Y, Z ) ) ) ] )
% 5.28/5.69 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 5.28/5.69 :=( Y, inverse( Y ) ), :=( Z, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 38, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y,
% 5.28/5.69 identity ) ) ] )
% 5.28/5.69 , clause( 6475, [ =( multiply( multiply( X, inverse( Y ) ), Y ), multiply(
% 5.28/5.69 X, identity ) ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 5.28/5.69 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6480, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 5.28/5.69 Y, Z ) ) ) ] )
% 5.28/5.69 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 5.28/5.69 ), Z ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6485, [ =( multiply( multiply( X, identity ), Y ), multiply( X, Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 5.28/5.69 , 0, clause( 6480, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 5.28/5.69 multiply( Y, Z ) ) ) ] )
% 5.28/5.69 , 0, 8, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 5.28/5.69 :=( Y, identity ), :=( Z, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 39, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X ) )
% 5.28/5.69 ] )
% 5.28/5.69 , clause( 6485, [ =( multiply( multiply( X, identity ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 5.28/5.69 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6491, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , clause( 15, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 5.28/5.69 'sk_c6' ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6493, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6502, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c6',
% 5.28/5.69 inverse( 'sk_c3' ) ) ] )
% 5.28/5.69 , clause( 6491, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , 1, clause( 6493, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6504, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , clause( 6502, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( 'sk_c6',
% 5.28/5.69 inverse( 'sk_c3' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6505, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 6504, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 40, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 6505, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6506, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 40, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , 0, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6509, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6510, [ =( identity, multiply( 'sk_c6', 'sk_c3' ) ), =( identity,
% 5.28/5.69 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , clause( 6506, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , 1, clause( 6509, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6512, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c3' ) ) ] )
% 5.28/5.69 , clause( 6510, [ =( identity, multiply( 'sk_c6', 'sk_c3' ) ), =( identity
% 5.28/5.69 , multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6513, [ =( multiply( 'sk_c6', 'sk_c3' ), identity ), =( multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ), identity ) ] )
% 5.28/5.69 , clause( 6512, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity
% 5.28/5.69 , multiply( 'sk_c6', 'sk_c3' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 43, [ =( multiply( 'sk_c6', 'sk_c3' ), identity ), =( multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ), identity ) ] )
% 5.28/5.69 , clause( 6513, [ =( multiply( 'sk_c6', 'sk_c3' ), identity ), =( multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ), identity ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6514, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 5.28/5.69 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 35, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( inverse(
% 5.28/5.69 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.69 , 0, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6517, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6518, [ =( identity, multiply( 'sk_c5', 'sk_c4' ) ), =( identity,
% 5.28/5.69 multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , clause( 6514, [ =( identity, multiply( 'sk_c7', 'sk_c1' ) ), =( inverse(
% 5.28/5.69 'sk_c4' ), 'sk_c5' ) ] )
% 5.28/5.69 , 1, clause( 6517, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6520, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity,
% 5.28/5.69 multiply( 'sk_c5', 'sk_c4' ) ) ] )
% 5.28/5.69 , clause( 6518, [ =( identity, multiply( 'sk_c5', 'sk_c4' ) ), =( identity
% 5.28/5.69 , multiply( 'sk_c7', 'sk_c1' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6521, [ =( multiply( 'sk_c5', 'sk_c4' ), identity ), =( multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ), identity ) ] )
% 5.28/5.69 , clause( 6520, [ =( multiply( 'sk_c7', 'sk_c1' ), identity ), =( identity
% 5.28/5.69 , multiply( 'sk_c5', 'sk_c4' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 46, [ =( multiply( 'sk_c5', 'sk_c4' ), identity ), =( multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ), identity ) ] )
% 5.28/5.69 , clause( 6521, [ =( multiply( 'sk_c5', 'sk_c4' ), identity ), =( multiply(
% 5.28/5.69 'sk_c7', 'sk_c1' ), identity ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6523, [ =( 'sk_c5', multiply( 'sk_c4', 'sk_c6' ) ), =( inverse(
% 5.28/5.69 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 27, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c4',
% 5.28/5.69 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6525, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6526, [ =( identity, multiply( 'sk_c6', 'sk_c2' ) ), =( 'sk_c5',
% 5.28/5.69 multiply( 'sk_c4', 'sk_c6' ) ) ] )
% 5.28/5.69 , clause( 6523, [ =( 'sk_c5', multiply( 'sk_c4', 'sk_c6' ) ), =( inverse(
% 5.28/5.69 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.69 , 1, clause( 6525, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c2' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6528, [ =( multiply( 'sk_c4', 'sk_c6' ), 'sk_c5' ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c2' ) ) ] )
% 5.28/5.69 , clause( 6526, [ =( identity, multiply( 'sk_c6', 'sk_c2' ) ), =( 'sk_c5',
% 5.28/5.69 multiply( 'sk_c4', 'sk_c6' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6529, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 6528, [ =( multiply( 'sk_c4', 'sk_c6' ), 'sk_c5' ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c2' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 59, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 6529, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c4', 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6531, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( inverse(
% 5.28/5.69 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 24, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 5.28/5.69 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6533, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6534, [ =( identity, multiply( 'sk_c6', 'sk_c2' ) ), =( 'sk_c7',
% 5.28/5.69 multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.28/5.69 , clause( 6531, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( inverse(
% 5.28/5.69 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.69 , 1, clause( 6533, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c2' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6536, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c2' ) ) ] )
% 5.28/5.69 , clause( 6534, [ =( identity, multiply( 'sk_c6', 'sk_c2' ) ), =( 'sk_c7',
% 5.28/5.69 multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6537, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.69 , clause( 6536, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c2' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 61, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.69 , clause( 6537, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6539, [ =( 'sk_c5', multiply( 'sk_c6', 'sk_c7' ) ), =( inverse(
% 5.28/5.69 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 23, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c6',
% 5.28/5.69 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6541, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6542, [ =( identity, multiply( 'sk_c6', 'sk_c2' ) ), =( 'sk_c5',
% 5.28/5.69 multiply( 'sk_c6', 'sk_c7' ) ) ] )
% 5.28/5.69 , clause( 6539, [ =( 'sk_c5', multiply( 'sk_c6', 'sk_c7' ) ), =( inverse(
% 5.28/5.69 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.69 , 1, clause( 6541, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 5.28/5.69 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c2' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6544, [ =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c2' ) ) ] )
% 5.28/5.69 , clause( 6542, [ =( identity, multiply( 'sk_c6', 'sk_c2' ) ), =( 'sk_c5',
% 5.28/5.69 multiply( 'sk_c6', 'sk_c7' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6545, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 6544, [ =( multiply( 'sk_c6', 'sk_c7' ), 'sk_c5' ), =( identity,
% 5.28/5.69 multiply( 'sk_c6', 'sk_c2' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 63, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.69 , clause( 6545, [ =( multiply( 'sk_c6', 'sk_c2' ), identity ), =( multiply(
% 5.28/5.69 'sk_c6', 'sk_c7' ), 'sk_c5' ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6547, [ =( multiply( X, Y ), multiply( multiply( X, identity ), Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 39, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X )
% 5.28/5.69 ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6550, [ =( multiply( inverse( identity ), X ), multiply( identity,
% 5.28/5.69 X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6547, [ =( multiply( X, Y ), multiply( multiply( X, identity )
% 5.28/5.69 , Y ) ) ] )
% 5.28/5.69 , 0, 6, substitution( 0, [ :=( X, identity )] ), substitution( 1, [ :=( X,
% 5.28/5.69 inverse( identity ) ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6551, [ =( multiply( inverse( identity ), X ), X ) ] )
% 5.28/5.69 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 5.28/5.69 , 0, clause( 6550, [ =( multiply( inverse( identity ), X ), multiply(
% 5.28/5.69 identity, X ) ) ] )
% 5.28/5.69 , 0, 5, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 82, [ =( multiply( inverse( identity ), X ), X ) ] )
% 5.28/5.69 , clause( 6551, [ =( multiply( inverse( identity ), X ), X ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6554, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 5.28/5.69 Y, Z ) ) ) ] )
% 5.28/5.69 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 5.28/5.69 ), Z ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6559, [ =( multiply( multiply( X, inverse( identity ) ), Y ),
% 5.28/5.69 multiply( X, Y ) ) ] )
% 5.28/5.69 , clause( 82, [ =( multiply( inverse( identity ), X ), X ) ] )
% 5.28/5.69 , 0, clause( 6554, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 5.28/5.69 multiply( Y, Z ) ) ) ] )
% 5.28/5.69 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 5.28/5.69 :=( Y, inverse( identity ) ), :=( Z, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 85, [ =( multiply( multiply( Y, inverse( identity ) ), X ),
% 5.28/5.69 multiply( Y, X ) ) ] )
% 5.28/5.69 , clause( 6559, [ =( multiply( multiply( X, inverse( identity ) ), Y ),
% 5.28/5.69 multiply( X, Y ) ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 5.28/5.69 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6565, [ =( multiply( X, Y ), multiply( multiply( X, inverse(
% 5.28/5.69 identity ) ), Y ) ) ] )
% 5.28/5.69 , clause( 85, [ =( multiply( multiply( Y, inverse( identity ) ), X ),
% 5.28/5.69 multiply( Y, X ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6568, [ =( multiply( inverse( inverse( identity ) ), X ), multiply(
% 5.28/5.69 identity, X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6565, [ =( multiply( X, Y ), multiply( multiply( X, inverse(
% 5.28/5.69 identity ) ), Y ) ) ] )
% 5.28/5.69 , 0, 7, substitution( 0, [ :=( X, inverse( identity ) )] ), substitution( 1
% 5.28/5.69 , [ :=( X, inverse( inverse( identity ) ) ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6569, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 5.28/5.69 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 5.28/5.69 , 0, clause( 6568, [ =( multiply( inverse( inverse( identity ) ), X ),
% 5.28/5.69 multiply( identity, X ) ) ] )
% 5.28/5.69 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 130, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 5.28/5.69 , clause( 6569, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ]
% 5.28/5.69 )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6571, [ =( X, multiply( inverse( inverse( identity ) ), X ) ) ] )
% 5.28/5.69 , clause( 130, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6573, [ =( inverse( identity ), identity ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6571, [ =( X, multiply( inverse( inverse( identity ) ), X ) )
% 5.28/5.69 ] )
% 5.28/5.69 , 0, 3, substitution( 0, [ :=( X, inverse( identity ) )] ), substitution( 1
% 5.28/5.69 , [ :=( X, inverse( identity ) )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 194, [ =( inverse( identity ), identity ) ] )
% 5.28/5.69 , clause( 6573, [ =( inverse( identity ), identity ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6576, [ =( multiply( X, identity ), multiply( multiply( X, inverse(
% 5.28/5.69 Y ) ), Y ) ) ] )
% 5.28/5.69 , clause( 38, [ =( multiply( multiply( Y, inverse( X ) ), X ), multiply( Y
% 5.28/5.69 , identity ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6579, [ =( multiply( inverse( inverse( X ) ), identity ), multiply(
% 5.28/5.69 identity, X ) ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6576, [ =( multiply( X, identity ), multiply( multiply( X,
% 5.28/5.69 inverse( Y ) ), Y ) ) ] )
% 5.28/5.69 , 0, 7, substitution( 0, [ :=( X, inverse( X ) )] ), substitution( 1, [
% 5.28/5.69 :=( X, inverse( inverse( X ) ) ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6580, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 5.28/5.69 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 5.28/5.69 , 0, clause( 6579, [ =( multiply( inverse( inverse( X ) ), identity ),
% 5.28/5.69 multiply( identity, X ) ) ] )
% 5.28/5.69 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 197, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 5.28/5.69 , clause( 6580, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ]
% 5.28/5.69 )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6583, [ =( multiply( X, Y ), multiply( multiply( X, identity ), Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 39, [ =( multiply( multiply( Y, identity ), X ), multiply( Y, X )
% 5.28/5.69 ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6586, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 197, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 5.28/5.69 , 0, clause( 6583, [ =( multiply( X, Y ), multiply( multiply( X, identity )
% 5.28/5.69 , Y ) ) ] )
% 5.28/5.69 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, inverse(
% 5.28/5.69 inverse( X ) ) ), :=( Y, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 6586, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.28/5.69 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6592, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) ), Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6595, [ =( multiply( X, identity ), X ) ] )
% 5.28/5.69 , clause( 197, [ =( multiply( inverse( inverse( X ) ), identity ), X ) ] )
% 5.28/5.69 , 0, clause( 6592, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) )
% 5.28/5.69 , Y ) ) ] )
% 5.28/5.69 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 5.28/5.69 :=( Y, identity )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 227, [ =( multiply( X, identity ), X ) ] )
% 5.28/5.69 , clause( 6595, [ =( multiply( X, identity ), X ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6601, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , clause( 15, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 5.28/5.69 'sk_c6' ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6603, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) ), Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6612, [ =( multiply( 'sk_c1', X ), multiply( inverse( 'sk_c7' ), X
% 5.28/5.69 ) ), =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.28/5.69 , clause( 6601, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , 1, clause( 6603, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) )
% 5.28/5.69 , Y ) ) ] )
% 5.28/5.69 , 0, 6, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' ), :=( Y,
% 5.28/5.69 X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6614, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( multiply( 'sk_c1', X )
% 5.28/5.69 , multiply( inverse( 'sk_c7' ), X ) ) ] )
% 5.28/5.69 , clause( 6612, [ =( multiply( 'sk_c1', X ), multiply( inverse( 'sk_c7' ),
% 5.28/5.69 X ) ), =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6615, [ =( multiply( inverse( 'sk_c7' ), X ), multiply( 'sk_c1', X
% 5.28/5.69 ) ), =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 6614, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( multiply( 'sk_c1', X
% 5.28/5.69 ), multiply( inverse( 'sk_c7' ), X ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 248, [ =( multiply( inverse( 'sk_c7' ), X ), multiply( 'sk_c1', X )
% 5.28/5.69 ), =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 6615, [ =( multiply( inverse( 'sk_c7' ), X ), multiply( 'sk_c1',
% 5.28/5.69 X ) ), =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 5.28/5.69 1 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6616, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c4' ),
% 5.28/5.69 'sk_c5' ) ] )
% 5.28/5.69 , clause( 16, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 5.28/5.69 'sk_c5' ) ] )
% 5.28/5.69 , 0, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6619, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) ), Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6620, [ =( multiply( 'sk_c4', X ), multiply( inverse( 'sk_c5' ), X
% 5.28/5.69 ) ), =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 5.28/5.69 , clause( 6616, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c4' ),
% 5.28/5.69 'sk_c5' ) ] )
% 5.28/5.69 , 1, clause( 6619, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) )
% 5.28/5.69 , Y ) ) ] )
% 5.28/5.69 , 0, 6, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c4' ), :=( Y,
% 5.28/5.69 X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6622, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4', X )
% 5.28/5.69 , multiply( inverse( 'sk_c5' ), X ) ) ] )
% 5.28/5.69 , clause( 6620, [ =( multiply( 'sk_c4', X ), multiply( inverse( 'sk_c5' ),
% 5.28/5.69 X ) ), =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6623, [ =( multiply( inverse( 'sk_c5' ), X ), multiply( 'sk_c4', X
% 5.28/5.69 ) ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 5.28/5.69 , clause( 6622, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4', X
% 5.28/5.69 ), multiply( inverse( 'sk_c5' ), X ) ) ] )
% 5.28/5.69 , 1, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 252, [ =( multiply( inverse( 'sk_c5' ), X ), multiply( 'sk_c4', X )
% 5.28/5.69 ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 5.28/5.69 , clause( 6623, [ =( multiply( inverse( 'sk_c5' ), X ), multiply( 'sk_c4',
% 5.28/5.69 X ) ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 5.28/5.69 1 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6624, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) ), Y )
% 5.28/5.69 ) ] )
% 5.28/5.69 , clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6627, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.28/5.69 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 5.28/5.69 , 0, clause( 6624, [ =( multiply( X, Y ), multiply( inverse( inverse( X ) )
% 5.28/5.69 , Y ) ) ] )
% 5.28/5.69 , 0, 5, substitution( 0, [ :=( X, inverse( X ) )] ), substitution( 1, [
% 5.28/5.69 :=( X, X ), :=( Y, inverse( X ) )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.28/5.69 , clause( 6627, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6630, [ =( X, multiply( X, identity ) ) ] )
% 5.28/5.69 , clause( 227, [ =( multiply( X, identity ), X ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6633, [ =( inverse( inverse( X ) ), multiply( X, identity ) ) ] )
% 5.28/5.69 , clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.28/5.69 ) ) ] )
% 5.28/5.69 , 0, clause( 6630, [ =( X, multiply( X, identity ) ) ] )
% 5.28/5.69 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, identity )] ), substitution(
% 5.28/5.69 1, [ :=( X, inverse( inverse( X ) ) )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6634, [ =( inverse( inverse( X ) ), X ) ] )
% 5.28/5.69 , clause( 227, [ =( multiply( X, identity ), X ) ] )
% 5.28/5.69 , 0, clause( 6633, [ =( inverse( inverse( X ) ), multiply( X, identity ) )
% 5.28/5.69 ] )
% 5.28/5.69 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 258, [ =( inverse( inverse( X ) ), X ) ] )
% 5.28/5.69 , clause( 6634, [ =( inverse( inverse( X ) ), X ) ] )
% 5.28/5.69 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6636, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 10, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , 0, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6639, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.28/5.69 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6643, [ =( identity, multiply( 'sk_c3', 'sk_c6' ) ), =( 'sk_c6',
% 5.28/5.69 multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 5.28/5.69 , clause( 6636, [ =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ), =( inverse(
% 5.28/5.69 'sk_c3' ), 'sk_c6' ) ] )
% 5.28/5.69 , 1, clause( 6639, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.28/5.69 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6653, [ =( identity, 'sk_c7' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 5.28/5.69 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 5.28/5.69 , clause( 9, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 5.28/5.69 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.69 , 1, clause( 6643, [ =( identity, multiply( 'sk_c3', 'sk_c6' ) ), =(
% 5.28/5.69 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 5.28/5.69 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6719, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 5.28/5.69 'sk_c7' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 5.28/5.69 , clause( 6653, [ =( identity, 'sk_c7' ), =( multiply( 'sk_c1', 'sk_c7' ),
% 5.28/5.69 'sk_c6' ), =( 'sk_c6', multiply( 'sk_c1', 'sk_c7' ) ) ] )
% 5.28/5.69 , 2, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 factor(
% 5.28/5.69 clause( 6725, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , clause( 6719, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 5.28/5.69 'sk_c7' ), =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ) ] )
% 5.28/5.69 , 0, 2, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 subsumption(
% 5.28/5.69 clause( 288, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , clause( 6725, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 5.28/5.69 'sk_c7' ) ] )
% 5.28/5.69 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.69 ).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6787, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( inverse(
% 5.28/5.69 'sk_c1' ), 'sk_c7' ) ] )
% 5.28/5.69 , clause( 14, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 5.28/5.69 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.69 , 1, substitution( 0, [] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 eqswap(
% 5.28/5.69 clause( 6789, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.28/5.69 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.28/5.69 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.69 clause( 6793, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c7',
% 5.28/5.69 multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.28/5.69 , clause( 6787, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( inverse(
% 5.28/5.69 'sk_c1' ), 'sk_c7' ) ] )
% 5.28/5.69 , 1, clause( 6789, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.28/5.69 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.28/5.69
% 5.28/5.69
% 5.28/5.69 paramod(
% 5.28/5.70 clause( 6802, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c6' ),
% 5.28/5.70 'sk_c7' ), =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.28/5.70 , clause( 9, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( multiply(
% 5.28/5.70 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.70 , 0, clause( 6793, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 5.28/5.70 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.28/5.70 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 eqswap(
% 5.28/5.70 clause( 6822, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.70 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.70 , clause( 6802, [ =( identity, 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c6' ),
% 5.28/5.70 'sk_c7' ), =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.28/5.70 , 2, substitution( 0, [] )).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 factor(
% 5.28/5.70 clause( 6937, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.70 'sk_c6' ) ] )
% 5.28/5.70 , clause( 6822, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.70 'sk_c6' ), =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.70 , 0, 2, substitution( 0, [] )).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 subsumption(
% 5.28/5.70 clause( 292, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.70 'sk_c6' ) ] )
% 5.28/5.70 , clause( 6937, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.28/5.70 'sk_c6' ) ] )
% 5.28/5.70 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.28/5.70 ).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 eqswap(
% 5.28/5.70 clause( 6939, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( inverse(
% 5.28/5.70 'sk_c2' ), 'sk_c6' ) ] )
% 5.28/5.70 , clause( 24, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 5.28/5.70 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.70 , 1, substitution( 0, [] )).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 eqswap(
% 5.28/5.70 clause( 6941, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.28/5.70 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.28/5.70 , 0, substitution( 0, [ :=( X, X )] )).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 eqswap(
% 5.28/5.70 clause( 6943, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( multiply(
% 5.28/5.70 'sk_c2', 'sk_c6' ), 'sk_c5' ) ] )
% 5.28/5.70 , clause( 19, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( multiply(
% 5.28/5.70 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.28/5.70 , 1, substitution( 0, [] )).
% 5.28/5.70
% 5.28/5.70
% 5.28/5.70 paramod(
% 5.28/5.70 clause( 6948, [ =( identity, multiply( 'sk_c2', 'sk_c6' ) ), =( 'sk_c7',
% 5.28/5.70 multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.35/5.70 , clause( 6939, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( inverse(
% 5.35/5.70 'sk_c2' ), 'sk_c6' ) ] )
% 5.35/5.70 , 1, clause( 6941, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.70 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c2' )] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 paramod(
% 5.35/5.70 clause( 7126, [ =( identity, 'sk_c5' ), =( 'sk_c7', multiply( 'sk_c3',
% 5.35/5.70 'sk_c6' ) ), =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.35/5.70 , clause( 6943, [ =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ), =( multiply(
% 5.35/5.70 'sk_c2', 'sk_c6' ), 'sk_c5' ) ] )
% 5.35/5.70 , 1, clause( 6948, [ =( identity, multiply( 'sk_c2', 'sk_c6' ) ), =(
% 5.35/5.70 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.35/5.70 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 factor(
% 5.35/5.70 clause( 7127, [ =( identity, 'sk_c5' ), =( 'sk_c7', multiply( 'sk_c3',
% 5.35/5.70 'sk_c6' ) ) ] )
% 5.35/5.70 , clause( 7126, [ =( identity, 'sk_c5' ), =( 'sk_c7', multiply( 'sk_c3',
% 5.35/5.70 'sk_c6' ) ), =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.35/5.70 , 1, 2, substitution( 0, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 paramod(
% 5.35/5.70 clause( 7137, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c3', 'sk_c6' ),
% 5.35/5.70 'sk_c7' ), =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.35/5.70 , clause( 292, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( identity,
% 5.35/5.70 'sk_c6' ) ] )
% 5.35/5.70 , 1, clause( 7127, [ =( identity, 'sk_c5' ), =( 'sk_c7', multiply( 'sk_c3'
% 5.35/5.70 , 'sk_c6' ) ) ] )
% 5.35/5.70 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 eqswap(
% 5.35/5.70 clause( 7203, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( 'sk_c6',
% 5.35/5.70 'sk_c5' ), =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.35/5.70 , clause( 7137, [ =( 'sk_c6', 'sk_c5' ), =( multiply( 'sk_c3', 'sk_c6' ),
% 5.35/5.70 'sk_c7' ), =( 'sk_c7', multiply( 'sk_c3', 'sk_c6' ) ) ] )
% 5.35/5.70 , 2, substitution( 0, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 factor(
% 5.35/5.70 clause( 7209, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( 'sk_c6',
% 5.35/5.70 'sk_c5' ) ] )
% 5.35/5.70 , clause( 7203, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( 'sk_c6',
% 5.35/5.70 'sk_c5' ), =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ) ] )
% 5.35/5.70 , 0, 2, substitution( 0, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 subsumption(
% 5.35/5.70 clause( 298, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( 'sk_c6',
% 5.35/5.70 'sk_c5' ) ] )
% 5.35/5.70 , clause( 7209, [ =( multiply( 'sk_c3', 'sk_c6' ), 'sk_c7' ), =( 'sk_c6',
% 5.35/5.70 'sk_c5' ) ] )
% 5.35/5.70 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.70 ).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 eqswap(
% 5.35/5.70 clause( 7265, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 5.35/5.70 'sk_c7' ) ] )
% 5.35/5.70 , clause( 15, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 5.35/5.70 'sk_c6' ) ] )
% 5.35/5.70 , 1, substitution( 0, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 eqswap(
% 5.35/5.70 clause( 7267, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.70 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.70 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 paramod(
% 5.35/5.70 clause( 7273, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c6',
% 5.35/5.70 inverse( 'sk_c3' ) ) ] )
% 5.35/5.70 , clause( 7265, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c1' ),
% 5.35/5.70 'sk_c7' ) ] )
% 5.35/5.70 , 1, clause( 7267, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.70 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 paramod(
% 5.35/5.70 clause( 7282, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c3' ), 'sk_c6' ),
% 5.35/5.70 =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.70 , clause( 10, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 5.35/5.70 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.70 , 0, clause( 7273, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 5.35/5.70 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.70 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 eqswap(
% 5.35/5.70 clause( 7302, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' ),
% 5.35/5.70 =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.70 , clause( 7282, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c3' ), 'sk_c6' )
% 5.35/5.70 , =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.70 , 2, substitution( 0, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 factor(
% 5.35/5.70 clause( 7431, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' ) ]
% 5.35/5.70 )
% 5.35/5.70 , clause( 7302, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' )
% 5.35/5.70 , =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.70 , 0, 2, substitution( 0, [] )).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 subsumption(
% 5.35/5.70 clause( 308, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' ) ]
% 5.35/5.70 )
% 5.35/5.70 , clause( 7431, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' )
% 5.35/5.70 ] )
% 5.35/5.70 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.70 ).
% 5.35/5.70
% 5.35/5.70
% 5.35/5.70 eqswap(
% 5.35/5.70 clause( 7432, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , clause( 15, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , 0, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7435, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.71 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7439, [ =( identity, multiply( 'sk_c3', 'sk_c6' ) ), =( 'sk_c7',
% 5.35/5.71 inverse( 'sk_c1' ) ) ] )
% 5.35/5.71 , clause( 7432, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , 1, clause( 7435, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7449, [ =( identity, 'sk_c7' ), =( inverse( 'sk_c1' ), 'sk_c7' ),
% 5.35/5.71 =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 5.35/5.71 , clause( 14, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c3',
% 5.35/5.71 'sk_c6' ), 'sk_c7' ) ] )
% 5.35/5.71 , 1, clause( 7439, [ =( identity, multiply( 'sk_c3', 'sk_c6' ) ), =(
% 5.35/5.71 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7515, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ),
% 5.35/5.71 =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 5.35/5.71 , clause( 7449, [ =( identity, 'sk_c7' ), =( inverse( 'sk_c1' ), 'sk_c7' )
% 5.35/5.71 , =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 5.35/5.71 , 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 factor(
% 5.35/5.71 clause( 7521, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 7515, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' )
% 5.35/5.71 , =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 subsumption(
% 5.35/5.71 clause( 309, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 7521, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' )
% 5.35/5.71 ] )
% 5.35/5.71 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.71 ).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7591, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 5.35/5.71 'sk_c7' ) ] )
% 5.35/5.71 , clause( 16, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( inverse( 'sk_c4' ),
% 5.35/5.71 'sk_c5' ) ] )
% 5.35/5.71 , 1, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7593, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.71 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7599, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c5',
% 5.35/5.71 inverse( 'sk_c4' ) ) ] )
% 5.35/5.71 , clause( 7591, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c1' ),
% 5.35/5.71 'sk_c7' ) ] )
% 5.35/5.71 , 1, clause( 7593, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7608, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c4' ), 'sk_c5' ),
% 5.35/5.71 =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.71 , clause( 11, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( inverse(
% 5.35/5.71 'sk_c4' ), 'sk_c5' ) ] )
% 5.35/5.71 , 0, clause( 7599, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 5.35/5.71 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7628, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ),
% 5.35/5.71 =( inverse( 'sk_c4' ), 'sk_c5' ) ] )
% 5.35/5.71 , clause( 7608, [ =( identity, 'sk_c6' ), =( inverse( 'sk_c4' ), 'sk_c5' )
% 5.35/5.71 , =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.71 , 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 factor(
% 5.35/5.71 clause( 7751, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 7628, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' )
% 5.35/5.71 , =( inverse( 'sk_c4' ), 'sk_c5' ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 subsumption(
% 5.35/5.71 clause( 310, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 7751, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' )
% 5.35/5.71 ] )
% 5.35/5.71 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.71 ).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7753, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c2' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , clause( 25, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , 1, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7755, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.71 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 7757, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( multiply( 'sk_c2',
% 5.35/5.71 'sk_c6' ), 'sk_c5' ) ] )
% 5.35/5.71 , clause( 20, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 5.35/5.71 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.71 , 1, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7764, [ =( identity, multiply( 'sk_c2', 'sk_c6' ) ), =( 'sk_c6',
% 5.35/5.71 inverse( 'sk_c3' ) ) ] )
% 5.35/5.71 , clause( 7753, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( inverse( 'sk_c2' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , 1, clause( 7755, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c2' )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7942, [ =( identity, 'sk_c5' ), =( 'sk_c6', inverse( 'sk_c3' ) ),
% 5.35/5.71 =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.71 , clause( 7757, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( multiply( 'sk_c2',
% 5.35/5.71 'sk_c6' ), 'sk_c5' ) ] )
% 5.35/5.71 , 1, clause( 7764, [ =( identity, multiply( 'sk_c2', 'sk_c6' ) ), =(
% 5.35/5.71 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 factor(
% 5.35/5.71 clause( 7943, [ =( identity, 'sk_c5' ), =( 'sk_c6', inverse( 'sk_c3' ) ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 7942, [ =( identity, 'sk_c5' ), =( 'sk_c6', inverse( 'sk_c3' ) )
% 5.35/5.71 , =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.71 , 1, 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 7953, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c3' ), 'sk_c6' ),
% 5.35/5.71 =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.71 , clause( 308, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6' ) ]
% 5.35/5.71 )
% 5.35/5.71 , 1, clause( 7943, [ =( identity, 'sk_c5' ), =( 'sk_c6', inverse( 'sk_c3' )
% 5.35/5.71 ) ] )
% 5.35/5.71 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 8019, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ),
% 5.35/5.71 =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.71 , clause( 7953, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c3' ), 'sk_c6' ),
% 5.35/5.71 =( 'sk_c6', inverse( 'sk_c3' ) ) ] )
% 5.35/5.71 , 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 factor(
% 5.35/5.71 clause( 8025, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 8019, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ),
% 5.35/5.71 =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 subsumption(
% 5.35/5.71 clause( 312, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ) ] )
% 5.35/5.71 , clause( 8025, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.71 )
% 5.35/5.71 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.71 ).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 8084, [ =( 'sk_c6', inverse( 'sk_c2' ) ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , clause( 25, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , 0, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 8087, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.71 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 8091, [ =( identity, multiply( 'sk_c3', 'sk_c6' ) ), =( 'sk_c6',
% 5.35/5.71 inverse( 'sk_c2' ) ) ] )
% 5.35/5.71 , clause( 8084, [ =( 'sk_c6', inverse( 'sk_c2' ) ), =( inverse( 'sk_c3' ),
% 5.35/5.71 'sk_c6' ) ] )
% 5.35/5.71 , 1, clause( 8087, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.71 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 paramod(
% 5.35/5.71 clause( 8101, [ =( identity, 'sk_c7' ), =( inverse( 'sk_c2' ), 'sk_c6' ),
% 5.35/5.71 =( 'sk_c6', inverse( 'sk_c2' ) ) ] )
% 5.35/5.71 , clause( 24, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( multiply( 'sk_c3',
% 5.35/5.71 'sk_c6' ), 'sk_c7' ) ] )
% 5.35/5.71 , 1, clause( 8091, [ =( identity, multiply( 'sk_c3', 'sk_c6' ) ), =(
% 5.35/5.71 'sk_c6', inverse( 'sk_c2' ) ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 eqswap(
% 5.35/5.71 clause( 8167, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( identity, 'sk_c7' ),
% 5.35/5.71 =( inverse( 'sk_c2' ), 'sk_c6' ) ] )
% 5.35/5.71 , clause( 8101, [ =( identity, 'sk_c7' ), =( inverse( 'sk_c2' ), 'sk_c6' )
% 5.35/5.71 , =( 'sk_c6', inverse( 'sk_c2' ) ) ] )
% 5.35/5.71 , 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 factor(
% 5.35/5.71 clause( 8173, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( identity, 'sk_c7' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 8167, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( identity, 'sk_c7' )
% 5.35/5.71 , =( inverse( 'sk_c2' ), 'sk_c6' ) ] )
% 5.35/5.71 , 0, 2, substitution( 0, [] )).
% 5.35/5.71
% 5.35/5.71
% 5.35/5.71 subsumption(
% 5.35/5.71 clause( 313, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( identity, 'sk_c7' ) ]
% 5.35/5.71 )
% 5.35/5.71 , clause( 8173, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( identity, 'sk_c7' )
% 5.35/5.72 ] )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8243, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c2' ),
% 5.35/5.72 'sk_c6' ) ] )
% 5.35/5.72 , clause( 26, [ =( inverse( 'sk_c2' ), 'sk_c6' ), =( inverse( 'sk_c4' ),
% 5.35/5.72 'sk_c5' ) ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8245, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.72 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8247, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( multiply( 'sk_c2',
% 5.35/5.72 'sk_c6' ), 'sk_c5' ) ] )
% 5.35/5.72 , clause( 21, [ =( multiply( 'sk_c2', 'sk_c6' ), 'sk_c5' ), =( inverse(
% 5.35/5.72 'sk_c4' ), 'sk_c5' ) ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8254, [ =( identity, multiply( 'sk_c2', 'sk_c6' ) ), =( 'sk_c5',
% 5.35/5.72 inverse( 'sk_c4' ) ) ] )
% 5.35/5.72 , clause( 8243, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( inverse( 'sk_c2' ),
% 5.35/5.72 'sk_c6' ) ] )
% 5.35/5.72 , 1, clause( 8245, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.72 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c2' )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8432, [ =( identity, 'sk_c5' ), =( 'sk_c5', inverse( 'sk_c4' ) ),
% 5.35/5.72 =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.72 , clause( 8247, [ =( 'sk_c5', inverse( 'sk_c4' ) ), =( multiply( 'sk_c2',
% 5.35/5.72 'sk_c6' ), 'sk_c5' ) ] )
% 5.35/5.72 , 1, clause( 8254, [ =( identity, multiply( 'sk_c2', 'sk_c6' ) ), =(
% 5.35/5.72 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.72 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 factor(
% 5.35/5.72 clause( 8433, [ =( identity, 'sk_c5' ), =( 'sk_c5', inverse( 'sk_c4' ) ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8432, [ =( identity, 'sk_c5' ), =( 'sk_c5', inverse( 'sk_c4' ) )
% 5.35/5.72 , =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.72 , 1, 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8443, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c4' ), 'sk_c5' ),
% 5.35/5.72 =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.72 , clause( 310, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( identity, 'sk_c6' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, clause( 8433, [ =( identity, 'sk_c5' ), =( 'sk_c5', inverse( 'sk_c4' )
% 5.35/5.72 ) ] )
% 5.35/5.72 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8509, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ),
% 5.35/5.72 =( inverse( 'sk_c4' ), 'sk_c5' ) ] )
% 5.35/5.72 , clause( 8443, [ =( 'sk_c6', 'sk_c5' ), =( inverse( 'sk_c4' ), 'sk_c5' ),
% 5.35/5.72 =( 'sk_c5', inverse( 'sk_c4' ) ) ] )
% 5.35/5.72 , 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 factor(
% 5.35/5.72 clause( 8515, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8509, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ),
% 5.35/5.72 =( inverse( 'sk_c4' ), 'sk_c5' ) ] )
% 5.35/5.72 , 0, 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 314, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ) ] )
% 5.35/5.72 , clause( 8515, [ =( inverse( 'sk_c4' ), 'sk_c5' ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8573, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 312, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8577, [ =( identity, 'sk_c5' ), =( 'sk_c6', inverse( 'sk_c3' ) ),
% 5.35/5.72 =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.72 , clause( 8573, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( 'sk_c6', 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, clause( 308, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c6'
% 5.35/5.72 ) ] )
% 5.35/5.72 , 1, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8634, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' ),
% 5.35/5.72 =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.72 , clause( 8577, [ =( identity, 'sk_c5' ), =( 'sk_c6', inverse( 'sk_c3' ) )
% 5.35/5.72 , =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 factor(
% 5.35/5.72 clause( 8639, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8634, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' )
% 5.35/5.72 , =( inverse( 'sk_c3' ), 'sk_c6' ) ] )
% 5.35/5.72 , 0, 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 316, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8639, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' )
% 5.35/5.72 ] )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8643, [ =( 'sk_c5', identity ), =( inverse( 'sk_c3' ), 'sk_c6' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 316, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8645, [ =( X, inverse( inverse( X ) ) ) ] )
% 5.35/5.72 , clause( 258, [ =( inverse( inverse( X ) ), X ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8646, [ =( 'sk_c3', inverse( 'sk_c6' ) ), =( 'sk_c5', identity ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8643, [ =( 'sk_c5', identity ), =( inverse( 'sk_c3' ), 'sk_c6' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 8645, [ =( X, inverse( inverse( X ) ) ) ] )
% 5.35/5.72 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c3' )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8648, [ =( identity, 'sk_c5' ), =( 'sk_c3', inverse( 'sk_c6' ) ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8646, [ =( 'sk_c3', inverse( 'sk_c6' ) ), =( 'sk_c5', identity )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8649, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8648, [ =( identity, 'sk_c5' ), =( 'sk_c3', inverse( 'sk_c6' ) )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 318, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 8649, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' )
% 5.35/5.72 ] )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8650, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 316, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8653, [ =( X, multiply( X, identity ) ) ] )
% 5.35/5.72 , clause( 227, [ =( multiply( X, identity ), X ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8654, [ =( X, multiply( X, 'sk_c5' ) ), =( 'sk_c6', inverse(
% 5.35/5.72 'sk_c3' ) ) ] )
% 5.35/5.72 , clause( 8650, [ =( 'sk_c6', inverse( 'sk_c3' ) ), =( identity, 'sk_c5' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 8653, [ =( X, multiply( X, identity ) ) ] )
% 5.35/5.72 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8656, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( X, multiply( X,
% 5.35/5.72 'sk_c5' ) ) ] )
% 5.35/5.72 , clause( 8654, [ =( X, multiply( X, 'sk_c5' ) ), =( 'sk_c6', inverse(
% 5.35/5.72 'sk_c3' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8657, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c3' ),
% 5.35/5.72 'sk_c6' ) ] )
% 5.35/5.72 , clause( 8656, [ =( inverse( 'sk_c3' ), 'sk_c6' ), =( X, multiply( X,
% 5.35/5.72 'sk_c5' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 319, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c3' ),
% 5.35/5.72 'sk_c6' ) ] )
% 5.35/5.72 , clause( 8657, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c3' ),
% 5.35/5.72 'sk_c6' ) ] )
% 5.35/5.72 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 5.35/5.72 1 )] ) ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8658, [ =( 'sk_c3', inverse( 'sk_c6' ) ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 318, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8661, [ =( X, multiply( X, identity ) ) ] )
% 5.35/5.72 , clause( 227, [ =( multiply( X, identity ), X ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8662, [ =( X, multiply( X, 'sk_c5' ) ), =( 'sk_c3', inverse(
% 5.35/5.72 'sk_c6' ) ) ] )
% 5.35/5.72 , clause( 8658, [ =( 'sk_c3', inverse( 'sk_c6' ) ), =( identity, 'sk_c5' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 8661, [ =( X, multiply( X, identity ) ) ] )
% 5.35/5.72 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8664, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( X, multiply( X,
% 5.35/5.72 'sk_c5' ) ) ] )
% 5.35/5.72 , clause( 8662, [ =( X, multiply( X, 'sk_c5' ) ), =( 'sk_c3', inverse(
% 5.35/5.72 'sk_c6' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8665, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , clause( 8664, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( X, multiply( X,
% 5.35/5.72 'sk_c5' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 323, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , clause( 8665, [ =( multiply( X, 'sk_c5' ), X ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 5.35/5.72 1 )] ) ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8669, [ =( identity, inverse( identity ) ) ] )
% 5.35/5.72 , clause( 194, [ =( inverse( identity ), identity ) ] )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8695, [ =( identity, inverse( 'sk_c5' ) ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , clause( 318, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, clause( 8669, [ =( identity, inverse( identity ) ) ] )
% 5.35/5.72 , 0, 3, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8697, [ =( 'sk_c5', inverse( 'sk_c5' ) ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ), =( inverse( 'sk_c6' ), 'sk_c3' ) ] )
% 5.35/5.72 , clause( 318, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, clause( 8695, [ =( identity, inverse( 'sk_c5' ) ), =( inverse( 'sk_c6'
% 5.35/5.72 ), 'sk_c3' ) ] )
% 5.35/5.72 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8760, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ), =( inverse( 'sk_c6' ), 'sk_c3' ) ] )
% 5.35/5.72 , clause( 8697, [ =( 'sk_c5', inverse( 'sk_c5' ) ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ), =( inverse( 'sk_c6' ), 'sk_c3' ) ] )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 factor(
% 5.35/5.72 clause( 8764, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , clause( 8760, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ), =( inverse( 'sk_c6' ), 'sk_c3' ) ] )
% 5.35/5.72 , 1, 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 325, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , clause( 8764, [ =( inverse( 'sk_c5' ), 'sk_c5' ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8812, [ =( 'sk_c3', inverse( 'sk_c6' ) ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 318, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( identity, 'sk_c5' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8815, [ =( X, multiply( inverse( inverse( identity ) ), X ) ) ] )
% 5.35/5.72 , clause( 130, [ =( multiply( inverse( inverse( identity ) ), X ), X ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8817, [ =( X, multiply( inverse( inverse( 'sk_c5' ) ), X ) ), =(
% 5.35/5.72 'sk_c3', inverse( 'sk_c6' ) ) ] )
% 5.35/5.72 , clause( 8812, [ =( 'sk_c3', inverse( 'sk_c6' ) ), =( identity, 'sk_c5' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 8815, [ =( X, multiply( inverse( inverse( identity ) ), X ) )
% 5.35/5.72 ] )
% 5.35/5.72 , 0, 5, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8818, [ =( X, multiply( 'sk_c5', X ) ), =( 'sk_c3', inverse(
% 5.35/5.72 'sk_c6' ) ) ] )
% 5.35/5.72 , clause( 198, [ =( multiply( inverse( inverse( X ) ), Y ), multiply( X, Y
% 5.35/5.72 ) ) ] )
% 5.35/5.72 , 0, clause( 8817, [ =( X, multiply( inverse( inverse( 'sk_c5' ) ), X ) ),
% 5.35/5.72 =( 'sk_c3', inverse( 'sk_c6' ) ) ] )
% 5.35/5.72 , 0, 2, substitution( 0, [ :=( X, 'sk_c5' ), :=( Y, X )] ), substitution( 1
% 5.35/5.72 , [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8820, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( X, multiply( 'sk_c5',
% 5.35/5.72 X ) ) ] )
% 5.35/5.72 , clause( 8818, [ =( X, multiply( 'sk_c5', X ) ), =( 'sk_c3', inverse(
% 5.35/5.72 'sk_c6' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8821, [ =( multiply( 'sk_c5', X ), X ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , clause( 8820, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( X, multiply( 'sk_c5'
% 5.35/5.72 , X ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 326, [ =( inverse( 'sk_c6' ), 'sk_c3' ), =( multiply( 'sk_c5', X )
% 5.35/5.72 , X ) ] )
% 5.35/5.72 , clause( 8821, [ =( multiply( 'sk_c5', X ), X ), =( inverse( 'sk_c6' ),
% 5.35/5.72 'sk_c3' ) ] )
% 5.35/5.72 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 5.35/5.72 0 )] ) ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8823, [ =( 'sk_c7', identity ), =( inverse( 'sk_c1' ), 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 309, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8825, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.72 , clause( 257, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8831, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =( 'sk_c7',
% 5.35/5.72 identity ) ] )
% 5.35/5.72 , clause( 8823, [ =( 'sk_c7', identity ), =( inverse( 'sk_c1' ), 'sk_c7' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 8825, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 5.35/5.72 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 8852, [ =( identity, 'sk_c6' ), =( identity, 'sk_c7' ), =( 'sk_c7'
% 5.35/5.72 , identity ) ] )
% 5.35/5.72 , clause( 288, [ =( multiply( 'sk_c1', 'sk_c7' ), 'sk_c6' ), =( identity,
% 5.35/5.72 'sk_c7' ) ] )
% 5.35/5.72 , 0, clause( 8831, [ =( identity, multiply( 'sk_c1', 'sk_c7' ) ), =(
% 5.35/5.72 'sk_c7', identity ) ] )
% 5.35/5.72 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 8876, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ), =( identity
% 5.35/5.72 , 'sk_c7' ) ] )
% 5.35/5.72 , clause( 8852, [ =( identity, 'sk_c6' ), =( identity, 'sk_c7' ), =(
% 5.35/5.72 'sk_c7', identity ) ] )
% 5.35/5.72 , 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 factor(
% 5.35/5.72 clause( 9035, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ) ] )
% 5.35/5.72 , clause( 8876, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ), =(
% 5.35/5.72 identity, 'sk_c7' ) ] )
% 5.35/5.72 , 0, 2, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 327, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ) ] )
% 5.35/5.72 , clause( 9035, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ) ] )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9037, [ =( 'sk_c7', identity ), =( inverse( 'sk_c1' ), 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 309, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9039, [ =( X, inverse( inverse( X ) ) ) ] )
% 5.35/5.72 , clause( 258, [ =( inverse( inverse( X ) ), X ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 9040, [ =( 'sk_c1', inverse( 'sk_c7' ) ), =( 'sk_c7', identity ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 9037, [ =( 'sk_c7', identity ), =( inverse( 'sk_c1' ), 'sk_c7' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 9039, [ =( X, inverse( inverse( X ) ) ) ] )
% 5.35/5.72 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c1' )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9042, [ =( identity, 'sk_c7' ), =( 'sk_c1', inverse( 'sk_c7' ) ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 9040, [ =( 'sk_c1', inverse( 'sk_c7' ) ), =( 'sk_c7', identity )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9043, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( identity, 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 9042, [ =( identity, 'sk_c7' ), =( 'sk_c1', inverse( 'sk_c7' ) )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 328, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( identity, 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 9043, [ =( inverse( 'sk_c7' ), 'sk_c1' ), =( identity, 'sk_c7' )
% 5.35/5.72 ] )
% 5.35/5.72 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 5.35/5.72 ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9044, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( identity, 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , clause( 309, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( identity, 'sk_c7' ) ]
% 5.35/5.72 )
% 5.35/5.72 , 0, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9047, [ =( X, multiply( X, identity ) ) ] )
% 5.35/5.72 , clause( 227, [ =( multiply( X, identity ), X ) ] )
% 5.35/5.72 , 0, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 paramod(
% 5.35/5.72 clause( 9048, [ =( X, multiply( X, 'sk_c7' ) ), =( 'sk_c7', inverse(
% 5.35/5.72 'sk_c1' ) ) ] )
% 5.35/5.72 , clause( 9044, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( identity, 'sk_c7' )
% 5.35/5.72 ] )
% 5.35/5.72 , 1, clause( 9047, [ =( X, multiply( X, identity ) ) ] )
% 5.35/5.72 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9050, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( X, multiply( X,
% 5.35/5.72 'sk_c7' ) ) ] )
% 5.35/5.72 , clause( 9048, [ =( X, multiply( X, 'sk_c7' ) ), =( 'sk_c7', inverse(
% 5.35/5.72 'sk_c1' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqswap(
% 5.35/5.72 clause( 9051, [ =( multiply( X, 'sk_c7' ), X ), =( inverse( 'sk_c1' ),
% 5.35/5.72 'sk_c7' ) ] )
% 5.35/5.72 , clause( 9050, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( X, multiply( X,
% 5.35/5.72 'sk_c7' ) ) ] )
% 5.35/5.72 , 1, substitution( 0, [ :=( X, X )] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 329, [ =( multiply( X, 'sk_c7' ), X ), =( inverse( 'sk_c1' ),
% 5.35/5.72 'sk_c7' ) ] )
% 5.35/5.72 , clause( 9051, [ =( multiply( X, 'sk_c7' ), X ), =( inverse( 'sk_c1' ),
% 5.35/5.72 'sk_c7' ) ] )
% 5.35/5.72 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 5.35/5.72 1 )] ) ).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 eqfact(
% 5.35/5.72 clause( 9055, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( identity, 'sk_c6' ) ] )
% 5.35/5.72 , clause( 327, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ) ] )
% 5.35/5.72 , 0, 1, substitution( 0, [] )).
% 5.35/5.72
% 5.35/5.72
% 5.35/5.72 subsumption(
% 5.35/5.72 clause( 333, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( identity, 'sk_c6' ) ] )
% 293.99/294.35 , clause( 9055, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( identity, 'sk_c6' ) ] )
% 293.99/294.35 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] )
% 293.99/294.35 ).
% 293.99/294.35
% 293.99/294.35
% 293.99/294.35 eqswap(
% 293.99/294.35 clause( 9066, [ ~( =( 'sk_c6', 'sk_c7' ) ), =( identity, 'sk_c6' ) ] )
% 293.99/294.35 , clause( 333, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( identity, 'sk_c6' ) ] )
% 293.99/294.35 , 0, substitution( 0, [] )).
% 293.99/294.35
% 293.99/294.35
% 293.99/294.35 eqfact(
% 293.99/294.35 clause( 9070, [ ~( =( 'sk_c6', 'sk_c7' ) ), =( identity, 'sk_c7' ) ] )
% 293.99/294.35 , clause( 327, [ =( identity, 'sk_c7' ), =( identity, 'sk_c6' ) ] )
% 293.99/294.35 , 1, 0, substitution( 0, [] )).
% 293.99/294.35
% 293.99/294.35
% 293.99/294.35 paramod(
% 293.99/294.35 clause( 9083, [ =( 'sk_c6', 'sk_c7' ), ~( =( 'sk_c6', 'sk_c7' ) ), ~( =(
% 293.99/294.35 'sk_c6', 'sk_c7' ) ) ] )
% 293.99/294.35 , clause( 9066, [ ~( =( 'sk_c6', 'sk_c7' ) ), =( identity, 'sk_c6' ) ] )
% 293.99/294.35 , 1, clause( 9070, [ ~( =( 'sk_c6', 'sk_c7' ) ), =( identity, 'sk_c7' ) ]
% 293.99/294.35 )
% 293.99/294.35 , 1, 1, substitution( 0, [] ), substitution( 1, [] )).
% 293.99/294.35
% 293.99/294.35
% 293.99/294.35 eqswap(
% 293.99/294.35 clause( 9086, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c6', 'sk_c7' ), ~( =(
% 293.99/294.35 'sk_c6', 'sk_c7' ) ) ] )
% 293.99/294.35 , clause( 9083, [ =( 'sk_c6', 'sk_c7' ), ~( =( 'sk_c6', 'sk_c7' ) ), ~( =(
% 293.99/294.36 'sk_c6', 'sk_c7' ) ) ] )
% 293.99/294.36 , 2, substitution( 0, [] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9088, [ ~( =( 'sk_c7', 'sk_c6' ) ), ~( =( 'sk_c7', 'sk_c6' ) ), =(
% 293.99/294.36 'sk_c6', 'sk_c7' ) ] )
% 293.99/294.36 , clause( 9086, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c6', 'sk_c7' ), ~( =(
% 293.99/294.36 'sk_c6', 'sk_c7' ) ) ] )
% 293.99/294.36 , 2, substitution( 0, [] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9089, [ =( 'sk_c7', 'sk_c6' ), ~( =( 'sk_c7', 'sk_c6' ) ), ~( =(
% 293.99/294.36 'sk_c7', 'sk_c6' ) ) ] )
% 293.99/294.36 , clause( 9088, [ ~( =( 'sk_c7', 'sk_c6' ) ), ~( =( 'sk_c7', 'sk_c6' ) ),
% 293.99/294.36 =( 'sk_c6', 'sk_c7' ) ] )
% 293.99/294.36 , 2, substitution( 0, [] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 factor(
% 293.99/294.36 clause( 9092, [ =( 'sk_c7', 'sk_c6' ), ~( =( 'sk_c7', 'sk_c6' ) ) ] )
% 293.99/294.36 , clause( 9089, [ =( 'sk_c7', 'sk_c6' ), ~( =( 'sk_c7', 'sk_c6' ) ), ~( =(
% 293.99/294.36 'sk_c7', 'sk_c6' ) ) ] )
% 293.99/294.36 , 1, 2, substitution( 0, [] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 subsumption(
% 293.99/294.36 clause( 334, [ ~( =( 'sk_c7', 'sk_c6' ) ), =( 'sk_c7', 'sk_c6' ) ] )
% 293.99/294.36 , clause( 9092, [ =( 'sk_c7', 'sk_c6' ), ~( =( 'sk_c7', 'sk_c6' ) ) ] )
% 293.99/294.36 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] )
% 293.99/294.36 ).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9095, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c6',
% 293.99/294.36 'sk_c7' ), 'sk_c5' ) ] )
% 293.99/294.36 , clause( 13, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c6',
% 293.99/294.36 'sk_c7' ), 'sk_c5' ) ] )
% 293.99/294.36 , 0, substitution( 0, [] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9098, [ =( identity, multiply( multiply( inverse( multiply( X, Y )
% 293.99/294.36 ), X ), Y ) ) ] )
% 293.99/294.36 , clause( 37, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y
% 293.99/294.36 ), identity ) ] )
% 293.99/294.36 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9100, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( X, 'sk_c7' )
% 293.99/294.36 , X ) ] )
% 293.99/294.36 , clause( 329, [ =( multiply( X, 'sk_c7' ), X ), =( inverse( 'sk_c1' ),
% 293.99/294.36 'sk_c7' ) ] )
% 293.99/294.36 , 1, substitution( 0, [ :=( X, X )] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9103, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( inverse(
% 293.99/294.36 'sk_c5' ), X ), multiply( 'sk_c4', X ) ) ] )
% 293.99/294.36 , clause( 252, [ =( multiply( inverse( 'sk_c5' ), X ), multiply( 'sk_c4', X
% 293.99/294.36 ) ), =( inverse( 'sk_c1' ), 'sk_c7' ) ] )
% 293.99/294.36 , 1, substitution( 0, [ :=( X, X )] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 eqswap(
% 293.99/294.36 clause( 9105, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c4',
% 293.99/294.36 'sk_c6' ), 'sk_c5' ) ] )
% 293.99/294.36 , clause( 17, [ =( inverse( 'sk_c1' ), 'sk_c7' ), =( multiply( 'sk_c4',
% 293.99/294.36 'sk_c6' ), 'sk_c5' ) ] )
% 293.99/294.36 , 0, substitution( 0, [] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 paramod(
% 293.99/294.36 clause( 9111, [ =( identity, multiply( multiply( inverse( 'sk_c5' ),
% 293.99/294.36 'sk_c6' ), 'sk_c7' ) ), =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 293.99/294.36 , clause( 9095, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( 'sk_c6',
% 293.99/294.36 'sk_c7' ), 'sk_c5' ) ] )
% 293.99/294.36 , 1, clause( 9098, [ =( identity, multiply( multiply( inverse( multiply( X
% 293.99/294.36 , Y ) ), X ), Y ) ) ] )
% 293.99/294.36 , 0, 5, substitution( 0, [] ), substitution( 1, [ :=( X, 'sk_c6' ), :=( Y,
% 293.99/294.36 'sk_c7' )] )).
% 293.99/294.36
% 293.99/294.36
% 293.99/294.36 paramod(
% 293.99/294.36 clause( 2046609, [ =( identity, multiply( inverse( 'sk_c5' ), 'sk_c6' ) ),
% 293.99/294.36 =( 'sk_c7', inverse( 'sk_c1' ) ), =( 'sk_c7', inverse( 'sk_c1' ) ) ] )
% 293.99/294.36 , clause( 9100, [ =( 'sk_c7', inverse( 'sk_c1' ) ), =( multiply( X, 'sk_c7'
% 293.99/294.36 ), X ) ] )
% 293.99/294.36 , 1, clause( 9111, [ =( identity, multiply( multiply( inverse( 'sk_c5' ),
% 293.99/294.36 'sk_c6' ),Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------