%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP179-3 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sat Jul 16 07:35:51 EDT 2022
% Result : Unsatisfiable 98.91s 99.31s
% Output : Refutation 98.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GRP179-3 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Tue Jun 14 03:41:24 EDT 2022
% 0.12/0.33 % CPUTime :
% 98.91/99.31 *** allocated 10000 integers for termspace/termends
% 98.91/99.31 *** allocated 10000 integers for clauses
% 98.91/99.31 *** allocated 10000 integers for justifications
% 98.91/99.31 Bliksem 1.12
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Automatic Strategy Selection
% 98.91/99.31
% 98.91/99.31 Clauses:
% 98.91/99.31 [
% 98.91/99.31 [ =( multiply( identity, X ), X ) ],
% 98.91/99.31 [ =( multiply( inverse( X ), X ), identity ) ],
% 98.91/99.31 [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply( Y, Z ) ) )
% 98.91/99.31 ],
% 98.91/99.31 [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y, X ) ) ]
% 98.91/99.31 ,
% 98.91/99.31 [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X ) ) ],
% 98.91/99.31 [ =( 'greatest_lower_bound'( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ) ) ],
% 98.91/99.31 [ =( 'least_upper_bound'( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( 'least_upper_bound'( X, Y ), Z ) ) ],
% 98.91/99.31 [ =( 'least_upper_bound'( X, X ), X ) ],
% 98.91/99.31 [ =( 'greatest_lower_bound'( X, X ), X ) ],
% 98.91/99.31 [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) ), X ) ]
% 98.91/99.31 ,
% 98.91/99.31 [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y ) ), X ) ]
% 98.91/99.31 ,
% 98.91/99.31 [ =( multiply( X, 'least_upper_bound'( Y, Z ) ), 'least_upper_bound'(
% 98.91/99.31 multiply( X, Y ), multiply( X, Z ) ) ) ],
% 98.91/99.31 [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ],
% 98.91/99.31 [ =( multiply( 'least_upper_bound'( X, Y ), Z ), 'least_upper_bound'(
% 98.91/99.31 multiply( X, Z ), multiply( Y, Z ) ) ) ],
% 98.91/99.31 [ =( multiply( 'greatest_lower_bound'( X, Y ), Z ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ],
% 98.91/99.31 [ =( inverse( identity ), identity ) ],
% 98.91/99.31 [ =( inverse( inverse( X ) ), X ) ],
% 98.91/99.31 [ =( inverse( multiply( X, Y ) ), multiply( inverse( Y ), inverse( X ) )
% 98.91/99.31 ) ],
% 98.91/99.31 [ ~( =( 'least_upper_bound'( inverse( a ), identity ), inverse(
% 98.91/99.31 'greatest_lower_bound'( a, identity ) ) ) ) ]
% 98.91/99.31 ] .
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 percentage equality = 1.000000, percentage horn = 1.000000
% 98.91/99.31 This is a pure equality problem
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Options Used:
% 98.91/99.31
% 98.91/99.31 useres = 1
% 98.91/99.31 useparamod = 1
% 98.91/99.31 useeqrefl = 1
% 98.91/99.31 useeqfact = 1
% 98.91/99.31 usefactor = 1
% 98.91/99.31 usesimpsplitting = 0
% 98.91/99.31 usesimpdemod = 5
% 98.91/99.31 usesimpres = 3
% 98.91/99.31
% 98.91/99.31 resimpinuse = 1000
% 98.91/99.31 resimpclauses = 20000
% 98.91/99.31 substype = eqrewr
% 98.91/99.31 backwardsubs = 1
% 98.91/99.31 selectoldest = 5
% 98.91/99.31
% 98.91/99.31 litorderings [0] = split
% 98.91/99.31 litorderings [1] = extend the termordering, first sorting on arguments
% 98.91/99.31
% 98.91/99.31 termordering = kbo
% 98.91/99.31
% 98.91/99.31 litapriori = 0
% 98.91/99.31 termapriori = 1
% 98.91/99.31 litaposteriori = 0
% 98.91/99.31 termaposteriori = 0
% 98.91/99.31 demodaposteriori = 0
% 98.91/99.31 ordereqreflfact = 0
% 98.91/99.31
% 98.91/99.31 litselect = negord
% 98.91/99.31
% 98.91/99.31 maxweight = 15
% 98.91/99.31 maxdepth = 30000
% 98.91/99.31 maxlength = 115
% 98.91/99.31 maxnrvars = 195
% 98.91/99.31 excuselevel = 1
% 98.91/99.31 increasemaxweight = 1
% 98.91/99.31
% 98.91/99.31 maxselected = 10000000
% 98.91/99.31 maxnrclauses = 10000000
% 98.91/99.31
% 98.91/99.31 showgenerated = 0
% 98.91/99.31 showkept = 0
% 98.91/99.31 showselected = 0
% 98.91/99.31 showdeleted = 0
% 98.91/99.31 showresimp = 1
% 98.91/99.31 showstatus = 2000
% 98.91/99.31
% 98.91/99.31 prologoutput = 1
% 98.91/99.31 nrgoals = 5000000
% 98.91/99.31 totalproof = 1
% 98.91/99.31
% 98.91/99.31 Symbols occurring in the translation:
% 98.91/99.31
% 98.91/99.31 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 98.91/99.31 . [1, 2] (w:1, o:20, a:1, s:1, b:0),
% 98.91/99.31 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 98.91/99.31 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 98.91/99.31 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 98.91/99.31 identity [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 98.91/99.31 multiply [41, 2] (w:1, o:46, a:1, s:1, b:0),
% 98.91/99.31 inverse [42, 1] (w:1, o:19, a:1, s:1, b:0),
% 98.91/99.31 'greatest_lower_bound' [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 98.91/99.31 'least_upper_bound' [46, 2] (w:1, o:45, a:1, s:1, b:0),
% 98.91/99.31 a [47, 0] (w:1, o:13, a:1, s:1, b:0).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Starting Search:
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 24260
% 98.91/99.31 Kept: 2004
% 98.91/99.31 Inuse: 195
% 98.91/99.31 Deleted: 12
% 98.91/99.31 Deletedinuse: 4
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 87874
% 98.91/99.31 Kept: 4009
% 98.91/99.31 Inuse: 398
% 98.91/99.31 Deleted: 26
% 98.91/99.31 Deletedinuse: 4
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 183571
% 98.91/99.31 Kept: 6021
% 98.91/99.31 Inuse: 623
% 98.91/99.31 Deleted: 73
% 98.91/99.31 Deletedinuse: 36
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 306632
% 98.91/99.31 Kept: 8027
% 98.91/99.31 Inuse: 783
% 98.91/99.31 Deleted: 107
% 98.91/99.31 Deletedinuse: 68
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 733417
% 98.91/99.31 Kept: 10031
% 98.91/99.31 Inuse: 1159
% 98.91/99.31 Deleted: 163
% 98.91/99.31 Deletedinuse: 68
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 1811454
% 98.91/99.31 Kept: 12067
% 98.91/99.31 Inuse: 1707
% 98.91/99.31 Deleted: 254
% 98.91/99.31 Deletedinuse: 68
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 2002702
% 98.91/99.31 Kept: 14219
% 98.91/99.31 Inuse: 1830
% 98.91/99.31 Deleted: 278
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 2080852
% 98.91/99.31 Kept: 16300
% 98.91/99.31 Inuse: 1874
% 98.91/99.31 Deleted: 280
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 2230059
% 98.91/99.31 Kept: 18345
% 98.91/99.31 Inuse: 1947
% 98.91/99.31 Deleted: 280
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying clauses:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 2420427
% 98.91/99.31 Kept: 20349
% 98.91/99.31 Inuse: 2020
% 98.91/99.31 Deleted: 2043
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 2795071
% 98.91/99.31 Kept: 22390
% 98.91/99.31 Inuse: 2156
% 98.91/99.31 Deleted: 2043
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 3257663
% 98.91/99.31 Kept: 24393
% 98.91/99.31 Inuse: 2330
% 98.91/99.31 Deleted: 2043
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 3912775
% 98.91/99.31 Kept: 26396
% 98.91/99.31 Inuse: 2573
% 98.91/99.31 Deleted: 2047
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 4840360
% 98.91/99.31 Kept: 28398
% 98.91/99.31 Inuse: 2887
% 98.91/99.31 Deleted: 2052
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 6615355
% 98.91/99.31 Kept: 30411
% 98.91/99.31 Inuse: 3369
% 98.91/99.31 Deleted: 2076
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 9869528
% 98.91/99.31 Kept: 32411
% 98.91/99.31 Inuse: 4069
% 98.91/99.31 Deleted: 2076
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 14125658
% 98.91/99.31 Kept: 34415
% 98.91/99.31 Inuse: 4943
% 98.91/99.31 Deleted: 2111
% 98.91/99.31 Deletedinuse: 69
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 18388683
% 98.91/99.31 Kept: 36415
% 98.91/99.31 Inuse: 5704
% 98.91/99.31 Deleted: 2173
% 98.91/99.31 Deletedinuse: 118
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Intermediate Status:
% 98.91/99.31 Generated: 27046263
% 98.91/99.31 Kept: 38420
% 98.91/99.31 Inuse: 6771
% 98.91/99.31 Deleted: 2211
% 98.91/99.31 Deletedinuse: 134
% 98.91/99.31
% 98.91/99.31 Resimplifying inuse:
% 98.91/99.31 Done
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 Bliksems!, er is een bewijs:
% 98.91/99.31 % SZS status Unsatisfiable
% 98.91/99.31 % SZS output start Refutation
% 98.91/99.31
% 98.91/99.31 clause( 0, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 98.91/99.31 , Z ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 3, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y,
% 98.91/99.31 X ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X ) )
% 98.91/99.31 ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 5, [ =( 'greatest_lower_bound'( X, 'greatest_lower_bound'( Y, Z ) )
% 98.91/99.31 , 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 6, [ =( 'least_upper_bound'( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 9, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) ), X
% 98.91/99.31 ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 10, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y ) ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 11, [ =( 'least_upper_bound'( multiply( X, Y ), multiply( X, Z ) )
% 98.91/99.31 , multiply( X, 'least_upper_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 12, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z )
% 98.91/99.31 ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 13, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z ) )
% 98.91/99.31 , multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 14, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z )
% 98.91/99.31 ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 17, [ =( multiply( inverse( Y ), inverse( X ) ), inverse( multiply(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 18, [ ~( =( 'least_upper_bound'( inverse( a ), identity ), inverse(
% 98.91/99.31 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 19, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 20, [ =( 'greatest_lower_bound'( 'least_upper_bound'( X, Y ), X ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 21, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X ) ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply( Y,
% 98.91/99.31 identity ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 23, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y )
% 98.91/99.31 , identity ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 27, [ =( 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), X
% 98.91/99.31 ), 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 29, [ =( 'least_upper_bound'( 'least_upper_bound'( X, Y ), X ),
% 98.91/99.31 'least_upper_bound'( X, Y ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 30, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 31, [ =( 'least_upper_bound'( 'greatest_lower_bound'( X, Y ), X ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 43, [ =( 'least_upper_bound'( 'greatest_lower_bound'( Y, X ), X ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 44, [ =( 'least_upper_bound'( 'greatest_lower_bound'(
% 98.91/99.31 'greatest_lower_bound'( X, Y ), Z ), 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( Y, Z ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 73, [ =( 'least_upper_bound'( identity, multiply( inverse( X ), Y )
% 98.91/99.31 ), multiply( inverse( X ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 78, [ ~( =( 'least_upper_bound'( identity, inverse( a ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 90, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ), multiply( X
% 98.91/99.31 , 'greatest_lower_bound'( Z, Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 125, [ =( multiply( 'least_upper_bound'( X, Z ), Y ), multiply(
% 98.91/99.31 'least_upper_bound'( Z, X ), Y ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 153, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y ), Z ),
% 98.91/99.31 inverse( Y ) ), 'greatest_lower_bound'( X, multiply( Z, inverse( Y ) ) )
% 98.91/99.31 ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 162, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ), multiply(
% 98.91/99.31 'greatest_lower_bound'( Z, X ), Y ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 166, [ =( 'greatest_lower_bound'( multiply( Y, X ), X ), multiply(
% 98.91/99.31 'greatest_lower_bound'( Y, identity ), X ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 167, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ), multiply(
% 98.91/99.31 X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 180, [ =( inverse( multiply( Y, inverse( X ) ) ), multiply( X,
% 98.91/99.31 inverse( Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X )
% 98.91/99.31 ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 184, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse( Y )
% 98.91/99.31 ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 195, [ =( multiply( X, 'greatest_lower_bound'( Z, inverse( multiply(
% 98.91/99.31 Y, X ) ) ) ), 'greatest_lower_bound'( multiply( X, Z ), inverse( Y ) ) )
% 98.91/99.31 ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 213, [ =( inverse( 'greatest_lower_bound'( Y, X ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 229, [ =( multiply( inverse( 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ), identity ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 289, [ =( inverse( 'least_upper_bound'( Y, X ) ), inverse(
% 98.91/99.31 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 305, [ =( multiply( inverse( 'least_upper_bound'( Y, X ) ),
% 98.91/99.31 'least_upper_bound'( X, Y ) ), identity ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 457, [ =( multiply( inverse( Y ), 'greatest_lower_bound'( identity
% 98.91/99.31 , Y ) ), 'greatest_lower_bound'( inverse( Y ), identity ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 472, [ =( 'least_upper_bound'( multiply( X, 'greatest_lower_bound'(
% 98.91/99.31 identity, Y ) ), X ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 475, [ =( 'greatest_lower_bound'( Y, multiply( Y,
% 98.91/99.31 'least_upper_bound'( X, identity ) ) ), Y ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 483, [ =( 'least_upper_bound'( multiply( X, 'greatest_lower_bound'(
% 98.91/99.31 Y, identity ) ), X ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 513, [ =( 'least_upper_bound'( X, multiply( X,
% 98.91/99.31 'greatest_lower_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 522, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.31 identity, X ) ), identity ), inverse( 'greatest_lower_bound'( identity, X
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 546, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.31 identity, X ) ), identity ), inverse( 'least_upper_bound'( identity, X )
% 98.91/99.31 ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 1007, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 1009, [ =( multiply( 'least_upper_bound'( Z, multiply( X, Y ) ),
% 98.91/99.31 inverse( Y ) ), 'least_upper_bound'( multiply( Z, inverse( Y ) ), X ) ) ]
% 98.91/99.31 )
% 98.91/99.31 .
% 98.91/99.31 clause( 1741, [ =( multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.31 inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ), inverse( X
% 98.91/99.31 ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 2160, [ =( multiply( 'greatest_lower_bound'( identity, X ), inverse(
% 98.91/99.31 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 2575, [ =( 'least_upper_bound'( 'greatest_lower_bound'( inverse(
% 98.91/99.31 'least_upper_bound'( identity, X ) ), Y ), 'greatest_lower_bound'(
% 98.91/99.31 identity, Y ) ), 'greatest_lower_bound'( identity, Y ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 3198, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.31 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 3227, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.31 'greatest_lower_bound'( identity, inverse( X ) ) ) ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 4702, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.31 'greatest_lower_bound'( Y, inverse( X ) ) ) ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 4745, [ =( 'greatest_lower_bound'( inverse( X ), inverse(
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ) ), inverse( X ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 4830, [ =( 'least_upper_bound'( inverse( X ), inverse(
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ) ), inverse( 'greatest_lower_bound'( Y, X
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 4831, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ), inverse( X ) ), inverse( 'greatest_lower_bound'( Y, X ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 5295, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y, X
% 98.91/99.31 ) ), inverse( X ) ), inverse( X ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 5310, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y,
% 98.91/99.31 inverse( X ) ) ), X ), X ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 5364, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'( X
% 98.91/99.31 , inverse( Y ) ) ), Y ), inverse( 'least_upper_bound'( X, inverse( Y ) )
% 98.91/99.31 ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 38541, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'(
% 98.91/99.31 identity, inverse( X ) ) ), 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.31 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 38556, [ =( 'least_upper_bound'( identity, inverse( X ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 38696, [ ~( =( inverse( 'greatest_lower_bound'( identity, a ) ),
% 98.91/99.31 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 .
% 98.91/99.31 clause( 39291, [] )
% 98.91/99.31 .
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 % SZS output end Refutation
% 98.91/99.31 found a proof!
% 98.91/99.31
% 98.91/99.31 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 98.91/99.31
% 98.91/99.31 initialclauses(
% 98.91/99.31 [ clause( 39293, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 , clause( 39294, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , clause( 39295, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 98.91/99.31 multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39296, [ =( 'greatest_lower_bound'( X, Y ),
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ) ] )
% 98.91/99.31 , clause( 39297, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y,
% 98.91/99.31 X ) ) ] )
% 98.91/99.31 , clause( 39298, [ =( 'greatest_lower_bound'( X, 'greatest_lower_bound'( Y
% 98.91/99.31 , Z ) ), 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ) ) ]
% 98.91/99.31 )
% 98.91/99.31 , clause( 39299, [ =( 'least_upper_bound'( X, 'least_upper_bound'( Y, Z ) )
% 98.91/99.31 , 'least_upper_bound'( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39300, [ =( 'least_upper_bound'( X, X ), X ) ] )
% 98.91/99.31 , clause( 39301, [ =( 'greatest_lower_bound'( X, X ), X ) ] )
% 98.91/99.31 , clause( 39302, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y
% 98.91/99.31 ) ), X ) ] )
% 98.91/99.31 , clause( 39303, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y
% 98.91/99.31 ) ), X ) ] )
% 98.91/99.31 , clause( 39304, [ =( multiply( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 39305, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 39306, [ =( multiply( 'least_upper_bound'( X, Y ), Z ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39307, [ =( multiply( 'greatest_lower_bound'( X, Y ), Z ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39308, [ =( inverse( identity ), identity ) ] )
% 98.91/99.31 , clause( 39309, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 , clause( 39310, [ =( inverse( multiply( X, Y ) ), multiply( inverse( Y ),
% 98.91/99.31 inverse( X ) ) ) ] )
% 98.91/99.31 , clause( 39311, [ ~( =( 'least_upper_bound'( inverse( a ), identity ),
% 98.91/99.31 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 ] ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 0, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 , clause( 39293, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , clause( 39294, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39317, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X
% 98.91/99.31 , Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39295, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 98.91/99.31 multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y )
% 98.91/99.31 , Z ) ) ] )
% 98.91/99.31 , clause( 39317, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply(
% 98.91/99.31 X, Y ), Z ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 3, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y,
% 98.91/99.31 X ) ) ] )
% 98.91/99.31 , clause( 39296, [ =( 'greatest_lower_bound'( X, Y ),
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X ) )
% 98.91/99.31 ] )
% 98.91/99.31 , clause( 39297, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y,
% 98.91/99.31 X ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 5, [ =( 'greatest_lower_bound'( X, 'greatest_lower_bound'( Y, Z ) )
% 98.91/99.31 , 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39298, [ =( 'greatest_lower_bound'( X, 'greatest_lower_bound'( Y
% 98.91/99.31 , Z ) ), 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ) ) ]
% 98.91/99.31 )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 6, [ =( 'least_upper_bound'( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39299, [ =( 'least_upper_bound'( X, 'least_upper_bound'( Y, Z ) )
% 98.91/99.31 , 'least_upper_bound'( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 9, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) ), X
% 98.91/99.31 ) ] )
% 98.91/99.31 , clause( 39302, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y
% 98.91/99.31 ) ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 10, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y ) ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 , clause( 39303, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y
% 98.91/99.31 ) ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39359, [ =( 'least_upper_bound'( multiply( X, Y ), multiply( X, Z )
% 98.91/99.31 ), multiply( X, 'least_upper_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39304, [ =( multiply( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 11, [ =( 'least_upper_bound'( multiply( X, Y ), multiply( X, Z ) )
% 98.91/99.31 , multiply( X, 'least_upper_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39359, [ =( 'least_upper_bound'( multiply( X, Y ), multiply( X, Z
% 98.91/99.31 ) ), multiply( X, 'least_upper_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39370, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X,
% 98.91/99.31 Z ) ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39305, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 12, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z )
% 98.91/99.31 ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 39370, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X
% 98.91/99.31 , Z ) ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39382, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z )
% 98.91/99.31 ), multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39306, [ =( multiply( 'least_upper_bound'( X, Y ), Z ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 13, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z ) )
% 98.91/99.31 , multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39382, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z
% 98.91/99.31 ) ), multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39395, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y,
% 98.91/99.31 Z ) ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39307, [ =( multiply( 'greatest_lower_bound'( X, Y ), Z ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 14, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z )
% 98.91/99.31 ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , clause( 39395, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y
% 98.91/99.31 , Z ) ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 , clause( 39309, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39426, [ =( multiply( inverse( Y ), inverse( X ) ), inverse(
% 98.91/99.31 multiply( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 39310, [ =( inverse( multiply( X, Y ) ), multiply( inverse( Y ),
% 98.91/99.31 inverse( X ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 17, [ =( multiply( inverse( Y ), inverse( X ) ), inverse( multiply(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 , clause( 39426, [ =( multiply( inverse( Y ), inverse( X ) ), inverse(
% 98.91/99.31 multiply( X, Y ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 18, [ ~( =( 'least_upper_bound'( inverse( a ), identity ), inverse(
% 98.91/99.31 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 , clause( 39311, [ ~( =( 'least_upper_bound'( inverse( a ), identity ),
% 98.91/99.31 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39445, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 98.91/99.31 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39446, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 98.91/99.31 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 , 0, clause( 39445, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 98.91/99.31 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, inverse(
% 98.91/99.31 X ) )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39447, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 98.91/99.31 , clause( 39446, [ =( identity, multiply( X, inverse( X ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 19, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 98.91/99.31 , clause( 39447, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39448, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 10, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39449, [ =( X, 'greatest_lower_bound'( 'least_upper_bound'( X, Y )
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , clause( 3, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , 0, clause( 39448, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, 'least_upper_bound'( X, Y ) )] )
% 98.91/99.31 , substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39452, [ =( 'greatest_lower_bound'( 'least_upper_bound'( X, Y ), X
% 98.91/99.31 ), X ) ] )
% 98.91/99.31 , clause( 39449, [ =( X, 'greatest_lower_bound'( 'least_upper_bound'( X, Y
% 98.91/99.31 ), X ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 20, [ =( 'greatest_lower_bound'( 'least_upper_bound'( X, Y ), X ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 , clause( 39452, [ =( 'greatest_lower_bound'( 'least_upper_bound'( X, Y ),
% 98.91/99.31 X ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39453, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 10, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39454, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X )
% 98.91/99.31 ) ] )
% 98.91/99.31 , 0, clause( 39453, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39457, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X )
% 98.91/99.31 ), X ) ] )
% 98.91/99.31 , clause( 39454, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'( Y
% 98.91/99.31 , X ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 21, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X ) ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 , clause( 39457, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X
% 98.91/99.31 ) ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39459, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 98.91/99.31 Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 98.91/99.31 ), Z ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39462, [ =( multiply( multiply( X, Y ), inverse( Y ) ), multiply( X
% 98.91/99.31 , identity ) ) ] )
% 98.91/99.31 , clause( 19, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 98.91/99.31 , 0, clause( 39459, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 98.91/99.31 multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.31 :=( Y, Y ), :=( Z, inverse( Y ) )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply( Y,
% 98.91/99.31 identity ) ) ] )
% 98.91/99.31 , clause( 39462, [ =( multiply( multiply( X, Y ), inverse( Y ) ), multiply(
% 98.91/99.31 X, identity ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39466, [ =( multiply( multiply( X, Y ), Z ), multiply( X, multiply(
% 98.91/99.31 Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 2, [ =( multiply( X, multiply( Y, Z ) ), multiply( multiply( X, Y
% 98.91/99.31 ), Z ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39469, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y
% 98.91/99.31 ), identity ) ] )
% 98.91/99.31 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , 0, clause( 39466, [ =( multiply( multiply( X, Y ), Z ), multiply( X,
% 98.91/99.31 multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, 9, substitution( 0, [ :=( X, multiply( X, Y ) )] ), substitution( 1, [
% 98.91/99.31 :=( X, inverse( multiply( X, Y ) ) ), :=( Y, X ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 23, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y )
% 98.91/99.31 , identity ) ] )
% 98.91/99.31 , clause( 39469, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X )
% 98.91/99.31 , Y ), identity ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39475, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 21, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39478, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'(
% 98.91/99.31 'greatest_lower_bound'( X, Y ), X ) ) ] )
% 98.91/99.31 , clause( 9, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, clause( 39475, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'(
% 98.91/99.31 Y, X ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, 'greatest_lower_bound'( X, Y ) ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39479, [ =( 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y )
% 98.91/99.31 , X ), 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.31 , clause( 39478, [ =( 'greatest_lower_bound'( X, Y ),
% 98.91/99.31 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), X ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 27, [ =( 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), X
% 98.91/99.31 ), 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.31 , clause( 39479, [ =( 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y
% 98.91/99.31 ), X ), 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39481, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 9, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39484, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'(
% 98.91/99.31 'least_upper_bound'( X, Y ), X ) ) ] )
% 98.91/99.31 , clause( 20, [ =( 'greatest_lower_bound'( 'least_upper_bound'( X, Y ), X )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, clause( 39481, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, 'least_upper_bound'( X, Y ) ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39485, [ =( 'least_upper_bound'( 'least_upper_bound'( X, Y ), X ),
% 98.91/99.31 'least_upper_bound'( X, Y ) ) ] )
% 98.91/99.31 , clause( 39484, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'(
% 98.91/99.31 'least_upper_bound'( X, Y ), X ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 29, [ =( 'least_upper_bound'( 'least_upper_bound'( X, Y ), X ),
% 98.91/99.31 'least_upper_bound'( X, Y ) ) ] )
% 98.91/99.31 , clause( 39485, [ =( 'least_upper_bound'( 'least_upper_bound'( X, Y ), X )
% 98.91/99.31 , 'least_upper_bound'( X, Y ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39486, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 9, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39487, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 3, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , 0, clause( 39486, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39490, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X )
% 98.91/99.31 ), X ) ] )
% 98.91/99.31 , clause( 39487, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 30, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 , clause( 39490, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X
% 98.91/99.31 ) ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39491, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 9, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( X, Y ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39492, [ =( X, 'least_upper_bound'( 'greatest_lower_bound'( X, Y )
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X )
% 98.91/99.31 ) ] )
% 98.91/99.31 , 0, clause( 39491, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'(
% 98.91/99.31 X, Y ) ) ) ] )
% 98.91/99.31 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, 'greatest_lower_bound'( X, Y
% 98.91/99.31 ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39495, [ =( 'least_upper_bound'( 'greatest_lower_bound'( X, Y ), X
% 98.91/99.31 ), X ) ] )
% 98.91/99.31 , clause( 39492, [ =( X, 'least_upper_bound'( 'greatest_lower_bound'( X, Y
% 98.91/99.31 ), X ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 31, [ =( 'least_upper_bound'( 'greatest_lower_bound'( X, Y ), X ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 , clause( 39495, [ =( 'least_upper_bound'( 'greatest_lower_bound'( X, Y ),
% 98.91/99.31 X ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39496, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , clause( 30, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X ) )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39497, [ =( X, 'least_upper_bound'( 'greatest_lower_bound'( Y, X )
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X )
% 98.91/99.31 ) ] )
% 98.91/99.31 , 0, clause( 39496, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'(
% 98.91/99.31 Y, X ) ) ) ] )
% 98.91/99.31 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, 'greatest_lower_bound'( Y, X
% 98.91/99.31 ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39500, [ =( 'least_upper_bound'( 'greatest_lower_bound'( Y, X ), X
% 98.91/99.31 ), X ) ] )
% 98.91/99.31 , clause( 39497, [ =( X, 'least_upper_bound'( 'greatest_lower_bound'( Y, X
% 98.91/99.31 ), X ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 43, [ =( 'least_upper_bound'( 'greatest_lower_bound'( Y, X ), X ),
% 98.91/99.31 X ) ] )
% 98.91/99.31 , clause( 39500, [ =( 'least_upper_bound'( 'greatest_lower_bound'( Y, X ),
% 98.91/99.31 X ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39502, [ =( Y, 'least_upper_bound'( 'greatest_lower_bound'( X, Y )
% 98.91/99.31 , Y ) ) ] )
% 98.91/99.31 , clause( 43, [ =( 'least_upper_bound'( 'greatest_lower_bound'( Y, X ), X )
% 98.91/99.31 , X ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39503, [ =( 'greatest_lower_bound'( X, Y ), 'least_upper_bound'(
% 98.91/99.31 'greatest_lower_bound'( 'greatest_lower_bound'( Z, X ), Y ),
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 5, [ =( 'greatest_lower_bound'( X, 'greatest_lower_bound'( Y, Z )
% 98.91/99.31 ), 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, clause( 39502, [ =( Y, 'least_upper_bound'( 'greatest_lower_bound'( X
% 98.91/99.31 , Y ), Y ) ) ] )
% 98.91/99.31 , 0, 5, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 98.91/99.31 substitution( 1, [ :=( X, Z ), :=( Y, 'greatest_lower_bound'( X, Y ) )] )
% 98.91/99.31 ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39504, [ =( 'least_upper_bound'( 'greatest_lower_bound'(
% 98.91/99.31 'greatest_lower_bound'( Z, X ), Y ), 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.31 , clause( 39503, [ =( 'greatest_lower_bound'( X, Y ), 'least_upper_bound'(
% 98.91/99.31 'greatest_lower_bound'( 'greatest_lower_bound'( Z, X ), Y ),
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 44, [ =( 'least_upper_bound'( 'greatest_lower_bound'(
% 98.91/99.31 'greatest_lower_bound'( X, Y ), Z ), 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( Y, Z ) ) ] )
% 98.91/99.31 , clause( 39504, [ =( 'least_upper_bound'( 'greatest_lower_bound'(
% 98.91/99.31 'greatest_lower_bound'( Z, X ), Y ), 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39506, [ =( multiply( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 11, [ =( 'least_upper_bound'( multiply( X, Y ), multiply( X, Z )
% 98.91/99.31 ), multiply( X, 'least_upper_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39508, [ =( multiply( inverse( X ), 'least_upper_bound'( X, Y ) ),
% 98.91/99.31 'least_upper_bound'( identity, multiply( inverse( X ), Y ) ) ) ] )
% 98.91/99.31 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , 0, clause( 39506, [ =( multiply( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, inverse(
% 98.91/99.31 X ) ), :=( Y, X ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39511, [ =( 'least_upper_bound'( identity, multiply( inverse( X ),
% 98.91/99.31 Y ) ), multiply( inverse( X ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 39508, [ =( multiply( inverse( X ), 'least_upper_bound'( X, Y ) )
% 98.91/99.31 , 'least_upper_bound'( identity, multiply( inverse( X ), Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 73, [ =( 'least_upper_bound'( identity, multiply( inverse( X ), Y )
% 98.91/99.31 ), multiply( inverse( X ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 39511, [ =( 'least_upper_bound'( identity, multiply( inverse( X )
% 98.91/99.31 , Y ) ), multiply( inverse( X ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39513, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.31 'least_upper_bound'( inverse( a ), identity ) ) ) ] )
% 98.91/99.31 , clause( 18, [ ~( =( 'least_upper_bound'( inverse( a ), identity ),
% 98.91/99.31 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39514, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.31 'least_upper_bound'( identity, inverse( a ) ) ) ) ] )
% 98.91/99.31 , clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X )
% 98.91/99.31 ) ] )
% 98.91/99.31 , 0, clause( 39513, [ ~( =( inverse( 'greatest_lower_bound'( a, identity )
% 98.91/99.31 ), 'least_upper_bound'( inverse( a ), identity ) ) ) ] )
% 98.91/99.31 , 0, 6, substitution( 0, [ :=( X, inverse( a ) ), :=( Y, identity )] ),
% 98.91/99.31 substitution( 1, [] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39517, [ ~( =( 'least_upper_bound'( identity, inverse( a ) ),
% 98.91/99.31 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 , clause( 39514, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.31 'least_upper_bound'( identity, inverse( a ) ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 78, [ ~( =( 'least_upper_bound'( identity, inverse( a ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 , clause( 39517, [ ~( =( 'least_upper_bound'( identity, inverse( a ) ),
% 98.91/99.31 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.31 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39518, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 12, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z
% 98.91/99.31 ) ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39520, [ =( multiply( X, 'greatest_lower_bound'( Z, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 3, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , 0, clause( 39518, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39522, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ), multiply(
% 98.91/99.31 X, 'greatest_lower_bound'( Z, Y ) ) ) ] )
% 98.91/99.31 , clause( 12, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z
% 98.91/99.31 ) ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, clause( 39520, [ =( multiply( X, 'greatest_lower_bound'( Z, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, 6, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 98.91/99.31 substitution( 1, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 90, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ), multiply( X
% 98.91/99.31 , 'greatest_lower_bound'( Z, Y ) ) ) ] )
% 98.91/99.31 , clause( 39522, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 multiply( X, 'greatest_lower_bound'( Z, Y ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39523, [ =( multiply( 'least_upper_bound'( X, Z ), Y ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , clause( 13, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z )
% 98.91/99.31 ), multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39525, [ =( multiply( 'least_upper_bound'( Y, X ), Z ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 4, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'( Y, X )
% 98.91/99.31 ) ] )
% 98.91/99.31 , 0, clause( 39523, [ =( multiply( 'least_upper_bound'( X, Z ), Y ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39527, [ =( multiply( 'least_upper_bound'( X, Y ), Z ), multiply(
% 98.91/99.31 'least_upper_bound'( Y, X ), Z ) ) ] )
% 98.91/99.31 , clause( 13, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z )
% 98.91/99.31 ), multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, clause( 39525, [ =( multiply( 'least_upper_bound'( Y, X ), Z ),
% 98.91/99.31 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 98.91/99.31 substitution( 1, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 125, [ =( multiply( 'least_upper_bound'( X, Z ), Y ), multiply(
% 98.91/99.31 'least_upper_bound'( Z, X ), Y ) ) ] )
% 98.91/99.31 , clause( 39527, [ =( multiply( 'least_upper_bound'( X, Y ), Z ), multiply(
% 98.91/99.31 'least_upper_bound'( Y, X ), Z ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39529, [ =( multiply( X, identity ), multiply( multiply( X, Y ),
% 98.91/99.31 inverse( Y ) ) ) ] )
% 98.91/99.31 , clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply( Y
% 98.91/99.31 , identity ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39532, [ =( multiply( X, identity ), multiply( identity, inverse(
% 98.91/99.31 inverse( X ) ) ) ) ] )
% 98.91/99.31 , clause( 19, [ =( multiply( X, inverse( X ) ), identity ) ] )
% 98.91/99.31 , 0, clause( 39529, [ =( multiply( X, identity ), multiply( multiply( X, Y
% 98.91/99.31 ), inverse( Y ) ) ) ] )
% 98.91/99.31 , 0, 5, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.31 :=( Y, inverse( X ) )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39533, [ =( multiply( X, identity ), inverse( inverse( X ) ) ) ] )
% 98.91/99.31 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 , 0, clause( 39532, [ =( multiply( X, identity ), multiply( identity,
% 98.91/99.31 inverse( inverse( X ) ) ) ) ] )
% 98.91/99.31 , 0, 4, substitution( 0, [ :=( X, inverse( inverse( X ) ) )] ),
% 98.91/99.31 substitution( 1, [ :=( X, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39534, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 , 0, clause( 39533, [ =( multiply( X, identity ), inverse( inverse( X ) ) )
% 98.91/99.31 ] )
% 98.91/99.31 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 98.91/99.31 ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , clause( 39534, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39537, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , clause( 14, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z
% 98.91/99.31 ) ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39539, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y ), Z )
% 98.91/99.31 , inverse( Y ) ), 'greatest_lower_bound'( multiply( X, identity ),
% 98.91/99.31 multiply( Z, inverse( Y ) ) ) ) ] )
% 98.91/99.31 , clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply( Y
% 98.91/99.31 , identity ) ) ] )
% 98.91/99.31 , 0, clause( 39537, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , 0, 10, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.31 :=( X, multiply( X, Y ) ), :=( Y, inverse( Y ) ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39543, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y ), Z )
% 98.91/99.31 , inverse( Y ) ), 'greatest_lower_bound'( X, multiply( Z, inverse( Y ) )
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , 0, clause( 39539, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y )
% 98.91/99.31 , Z ), inverse( Y ) ), 'greatest_lower_bound'( multiply( X, identity ),
% 98.91/99.31 multiply( Z, inverse( Y ) ) ) ) ] )
% 98.91/99.31 , 0, 10, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.31 :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 153, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y ), Z ),
% 98.91/99.31 inverse( Y ) ), 'greatest_lower_bound'( X, multiply( Z, inverse( Y ) ) )
% 98.91/99.31 ) ] )
% 98.91/99.31 , clause( 39543, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y ), Z
% 98.91/99.31 ), inverse( Y ) ), 'greatest_lower_bound'( X, multiply( Z, inverse( Y )
% 98.91/99.31 ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39545, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , clause( 14, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z
% 98.91/99.31 ) ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39547, [ =( multiply( 'greatest_lower_bound'( Y, X ), Z ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , clause( 3, [ =( 'greatest_lower_bound'( X, Y ), 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ) ] )
% 98.91/99.31 , 0, clause( 39545, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39549, [ =( multiply( 'greatest_lower_bound'( X, Y ), Z ), multiply(
% 98.91/99.31 'greatest_lower_bound'( Y, X ), Z ) ) ] )
% 98.91/99.31 , clause( 14, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z
% 98.91/99.31 ) ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, clause( 39547, [ =( multiply( 'greatest_lower_bound'( Y, X ), Z ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] ),
% 98.91/99.31 substitution( 1, [ :=( X, Y ), :=( Y, X ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 162, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ), multiply(
% 98.91/99.31 'greatest_lower_bound'( Z, X ), Y ) ) ] )
% 98.91/99.31 , clause( 39549, [ =( multiply( 'greatest_lower_bound'( X, Y ), Z ),
% 98.91/99.31 multiply( 'greatest_lower_bound'( Y, X ), Z ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39551, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , clause( 14, [ =( 'greatest_lower_bound'( multiply( X, Z ), multiply( Y, Z
% 98.91/99.31 ) ), multiply( 'greatest_lower_bound'( X, Y ), Z ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39553, [ =( multiply( 'greatest_lower_bound'( X, identity ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), Y ) ) ] )
% 98.91/99.31 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 , 0, clause( 39551, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.31 , 0, 10, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.31 :=( Y, Y ), :=( Z, identity )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39555, [ =( 'greatest_lower_bound'( multiply( X, Y ), Y ), multiply(
% 98.91/99.31 'greatest_lower_bound'( X, identity ), Y ) ) ] )
% 98.91/99.31 , clause( 39553, [ =( multiply( 'greatest_lower_bound'( X, identity ), Y )
% 98.91/99.31 , 'greatest_lower_bound'( multiply( X, Y ), Y ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 166, [ =( 'greatest_lower_bound'( multiply( Y, X ), X ), multiply(
% 98.91/99.31 'greatest_lower_bound'( Y, identity ), X ) ) ] )
% 98.91/99.31 , clause( 39555, [ =( 'greatest_lower_bound'( multiply( X, Y ), Y ),
% 98.91/99.31 multiply( 'greatest_lower_bound'( X, identity ), Y ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39557, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 12, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z
% 98.91/99.31 ) ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39558, [ =( multiply( X, 'greatest_lower_bound'( identity, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( X, multiply( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , 0, clause( 39557, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.31 :=( Y, identity ), :=( Z, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39560, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ), multiply(
% 98.91/99.31 X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.31 , clause( 39558, [ =( multiply( X, 'greatest_lower_bound'( identity, Y ) )
% 98.91/99.31 , 'greatest_lower_bound'( X, multiply( X, Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 167, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ), multiply(
% 98.91/99.31 X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.31 , clause( 39560, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ),
% 98.91/99.31 multiply( X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39563, [ =( inverse( multiply( Y, X ) ), multiply( inverse( X ),
% 98.91/99.31 inverse( Y ) ) ) ] )
% 98.91/99.31 , clause( 17, [ =( multiply( inverse( Y ), inverse( X ) ), inverse(
% 98.91/99.31 multiply( X, Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39564, [ =( inverse( multiply( X, inverse( Y ) ) ), multiply( Y,
% 98.91/99.31 inverse( X ) ) ) ] )
% 98.91/99.31 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.31 , 0, clause( 39563, [ =( inverse( multiply( Y, X ) ), multiply( inverse( X
% 98.91/99.31 ), inverse( Y ) ) ) ] )
% 98.91/99.31 , 0, 7, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, inverse(
% 98.91/99.31 Y ) ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 180, [ =( inverse( multiply( Y, inverse( X ) ) ), multiply( X,
% 98.91/99.31 inverse( Y ) ) ) ] )
% 98.91/99.31 , clause( 39564, [ =( inverse( multiply( X, inverse( Y ) ) ), multiply( Y,
% 98.91/99.31 inverse( X ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39569, [ =( multiply( Y, inverse( X ) ), inverse( multiply( X,
% 98.91/99.31 inverse( Y ) ) ) ) ] )
% 98.91/99.31 , clause( 180, [ =( inverse( multiply( Y, inverse( X ) ) ), multiply( X,
% 98.91/99.31 inverse( Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39575, [ =( multiply( X, inverse( multiply( Y, X ) ) ), inverse(
% 98.91/99.31 multiply( Y, identity ) ) ) ] )
% 98.91/99.31 , clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply( Y
% 98.91/99.31 , identity ) ) ] )
% 98.91/99.31 , 0, clause( 39569, [ =( multiply( Y, inverse( X ) ), inverse( multiply( X
% 98.91/99.31 , inverse( Y ) ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, multiply( Y, X ) ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39576, [ =( multiply( X, inverse( multiply( Y, X ) ) ), inverse( Y
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , 0, clause( 39575, [ =( multiply( X, inverse( multiply( Y, X ) ) ),
% 98.91/99.31 inverse( multiply( Y, identity ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.31 :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X )
% 98.91/99.31 ) ] )
% 98.91/99.31 , clause( 39576, [ =( multiply( X, inverse( multiply( Y, X ) ) ), inverse(
% 98.91/99.31 Y ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39579, [ =( multiply( X, identity ), multiply( multiply( X, Y ),
% 98.91/99.31 inverse( Y ) ) ) ] )
% 98.91/99.31 , clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply( Y
% 98.91/99.31 , identity ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39586, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ),
% 98.91/99.31 identity ), multiply( identity, inverse( Y ) ) ) ] )
% 98.91/99.31 , clause( 23, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y
% 98.91/99.31 ), identity ) ] )
% 98.91/99.31 , 0, clause( 39579, [ =( multiply( X, identity ), multiply( multiply( X, Y
% 98.91/99.31 ), inverse( Y ) ) ) ] )
% 98.91/99.31 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, multiply( inverse( multiply( X, Y ) ), X ) ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39587, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ),
% 98.91/99.31 identity ), inverse( Y ) ) ] )
% 98.91/99.31 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.31 , 0, clause( 39586, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X
% 98.91/99.31 ), identity ), multiply( identity, inverse( Y ) ) ) ] )
% 98.91/99.31 , 0, 9, substitution( 0, [ :=( X, inverse( Y ) )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39588, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse( Y
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.31 , 0, clause( 39587, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X
% 98.91/99.31 ), identity ), inverse( Y ) ) ] )
% 98.91/99.31 , 0, 1, substitution( 0, [ :=( X, multiply( inverse( multiply( X, Y ) ), X
% 98.91/99.31 ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 184, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse( Y )
% 98.91/99.31 ) ] )
% 98.91/99.31 , clause( 39588, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse(
% 98.91/99.31 Y ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39591, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , clause( 12, [ =( 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z
% 98.91/99.31 ) ), multiply( X, 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39593, [ =( multiply( X, 'greatest_lower_bound'( Y, inverse(
% 98.91/99.31 multiply( Z, X ) ) ) ), 'greatest_lower_bound'( multiply( X, Y ), inverse(
% 98.91/99.31 Z ) ) ) ] )
% 98.91/99.31 , clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , 0, clause( 39591, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.31 'greatest_lower_bound'( multiply( X, Y ), multiply( X, Z ) ) ) ] )
% 98.91/99.31 , 0, 13, substitution( 0, [ :=( X, Z ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.31 :=( X, X ), :=( Y, Y ), :=( Z, inverse( multiply( Z, X ) ) )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 195, [ =( multiply( X, 'greatest_lower_bound'( Z, inverse( multiply(
% 98.91/99.31 Y, X ) ) ) ), 'greatest_lower_bound'( multiply( X, Z ), inverse( Y ) ) )
% 98.91/99.31 ] )
% 98.91/99.31 , clause( 39593, [ =( multiply( X, 'greatest_lower_bound'( Y, inverse(
% 98.91/99.31 multiply( Z, X ) ) ) ), 'greatest_lower_bound'( multiply( X, Y ), inverse(
% 98.91/99.31 Z ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 98.91/99.31 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39596, [ =( inverse( Y ), multiply( X, inverse( multiply( Y, X ) )
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39599, [ =( inverse( 'greatest_lower_bound'( X, Y ) ), multiply( Z
% 98.91/99.31 , inverse( multiply( 'greatest_lower_bound'( Y, X ), Z ) ) ) ) ] )
% 98.91/99.31 , clause( 162, [ =( multiply( 'greatest_lower_bound'( X, Z ), Y ), multiply(
% 98.91/99.31 'greatest_lower_bound'( Z, X ), Y ) ) ] )
% 98.91/99.31 , 0, clause( 39596, [ =( inverse( Y ), multiply( X, inverse( multiply( Y, X
% 98.91/99.31 ) ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 98.91/99.31 substitution( 1, [ :=( X, Z ), :=( Y, 'greatest_lower_bound'( X, Y ) )] )
% 98.91/99.31 ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39602, [ =( inverse( 'greatest_lower_bound'( X, Y ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ) ) ] )
% 98.91/99.31 , clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , 0, clause( 39599, [ =( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.31 multiply( Z, inverse( multiply( 'greatest_lower_bound'( Y, X ), Z ) ) ) )
% 98.91/99.31 ] )
% 98.91/99.31 , 0, 5, substitution( 0, [ :=( X, 'greatest_lower_bound'( Y, X ) ), :=( Y,
% 98.91/99.31 Z )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 213, [ =( inverse( 'greatest_lower_bound'( Y, X ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 39602, [ =( inverse( 'greatest_lower_bound'( X, Y ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39603, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 98.91/99.31 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39604, [ =( identity, multiply( inverse( 'greatest_lower_bound'( Y
% 98.91/99.31 , X ) ), 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 213, [ =( inverse( 'greatest_lower_bound'( Y, X ) ), inverse(
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , 0, clause( 39603, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 98.91/99.31 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.31 :=( X, 'greatest_lower_bound'( X, Y ) )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39607, [ =( multiply( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ), identity ) ] )
% 98.91/99.31 , clause( 39604, [ =( identity, multiply( inverse( 'greatest_lower_bound'(
% 98.91/99.31 Y, X ) ), 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 229, [ =( multiply( inverse( 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.31 'greatest_lower_bound'( X, Y ) ), identity ) ] )
% 98.91/99.31 , clause( 39607, [ =( multiply( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( Y, X ) ), identity ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39608, [ =( inverse( Y ), multiply( X, inverse( multiply( Y, X ) )
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39611, [ =( inverse( 'least_upper_bound'( X, Y ) ), multiply( Z,
% 98.91/99.31 inverse( multiply( 'least_upper_bound'( Y, X ), Z ) ) ) ) ] )
% 98.91/99.31 , clause( 125, [ =( multiply( 'least_upper_bound'( X, Z ), Y ), multiply(
% 98.91/99.31 'least_upper_bound'( Z, X ), Y ) ) ] )
% 98.91/99.31 , 0, clause( 39608, [ =( inverse( Y ), multiply( X, inverse( multiply( Y, X
% 98.91/99.31 ) ) ) ) ] )
% 98.91/99.31 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 98.91/99.31 substitution( 1, [ :=( X, Z ), :=( Y, 'least_upper_bound'( X, Y ) )] )
% 98.91/99.31 ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39614, [ =( inverse( 'least_upper_bound'( X, Y ) ), inverse(
% 98.91/99.31 'least_upper_bound'( Y, X ) ) ) ] )
% 98.91/99.31 , clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , 0, clause( 39611, [ =( inverse( 'least_upper_bound'( X, Y ) ), multiply(
% 98.91/99.31 Z, inverse( multiply( 'least_upper_bound'( Y, X ), Z ) ) ) ) ] )
% 98.91/99.31 , 0, 5, substitution( 0, [ :=( X, 'least_upper_bound'( Y, X ) ), :=( Y, Z )] )
% 98.91/99.31 , substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 289, [ =( inverse( 'least_upper_bound'( Y, X ) ), inverse(
% 98.91/99.31 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 39614, [ =( inverse( 'least_upper_bound'( X, Y ) ), inverse(
% 98.91/99.31 'least_upper_bound'( Y, X ) ) ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39615, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 98.91/99.31 , clause( 1, [ =( multiply( inverse( X ), X ), identity ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39616, [ =( identity, multiply( inverse( 'least_upper_bound'( Y, X
% 98.91/99.31 ) ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 289, [ =( inverse( 'least_upper_bound'( Y, X ) ), inverse(
% 98.91/99.31 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , 0, clause( 39615, [ =( identity, multiply( inverse( X ), X ) ) ] )
% 98.91/99.31 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.31 :=( X, 'least_upper_bound'( X, Y ) )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39619, [ =( multiply( inverse( 'least_upper_bound'( X, Y ) ),
% 98.91/99.31 'least_upper_bound'( Y, X ) ), identity ) ] )
% 98.91/99.31 , clause( 39616, [ =( identity, multiply( inverse( 'least_upper_bound'( Y,
% 98.91/99.31 X ) ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 subsumption(
% 98.91/99.31 clause( 305, [ =( multiply( inverse( 'least_upper_bound'( Y, X ) ),
% 98.91/99.31 'least_upper_bound'( X, Y ) ), identity ) ] )
% 98.91/99.31 , clause( 39619, [ =( multiply( inverse( 'least_upper_bound'( X, Y ) ),
% 98.91/99.31 'least_upper_bound'( Y, X ) ), identity ) ] )
% 98.91/99.31 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.31 )] ) ).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 eqswap(
% 98.91/99.31 clause( 39621, [ =( multiply( X, 'greatest_lower_bound'( identity, Y ) ),
% 98.91/99.31 'greatest_lower_bound'( X, multiply( X, Y ) ) ) ] )
% 98.91/99.31 , clause( 167, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ), multiply(
% 98.91/99.31 X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.31 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39640, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ),
% 98.91/99.31 'greatest_lower_bound'( identity, Y ) ), 'greatest_lower_bound'( multiply(
% 98.91/99.31 inverse( multiply( X, Y ) ), X ), identity ) ) ] )
% 98.91/99.31 , clause( 23, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ), Y
% 98.91/99.31 ), identity ) ] )
% 98.91/99.31 , 0, clause( 39621, [ =( multiply( X, 'greatest_lower_bound'( identity, Y )
% 98.91/99.31 ), 'greatest_lower_bound'( X, multiply( X, Y ) ) ) ] )
% 98.91/99.31 , 0, 18, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.31 :=( X, multiply( inverse( multiply( X, Y ) ), X ) ), :=( Y, Y )] )).
% 98.91/99.31
% 98.91/99.31
% 98.91/99.31 paramod(
% 98.91/99.31 clause( 39642, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X ),
% 98.91/99.31 'greatest_lower_bound'( identity, Y ) ), 'greatest_lower_bound'( inverse(
% 98.91/99.31 Y ), identity ) ) ] )
% 98.91/99.31 , clause( 184, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse( Y
% 98.91/99.31 ) ) ] )
% 98.91/99.31 , 0, clause( 39640, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X
% 98.91/99.31 ), 'greatest_lower_bound'( identity, Y ) ), 'greatest_lower_bound'(
% 98.91/99.31 multiply( inverse( multiply( X, Y ) ), X ), identity ) ) ] )
% 98.91/99.32 , 0, 12, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39643, [ =( multiply( inverse( Y ), 'greatest_lower_bound'(
% 98.91/99.32 identity, Y ) ), 'greatest_lower_bound'( inverse( Y ), identity ) ) ] )
% 98.91/99.32 , clause( 184, [ =( multiply( inverse( multiply( X, Y ) ), X ), inverse( Y
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , 0, clause( 39642, [ =( multiply( multiply( inverse( multiply( X, Y ) ), X
% 98.91/99.32 ), 'greatest_lower_bound'( identity, Y ) ), 'greatest_lower_bound'(
% 98.91/99.32 inverse( Y ), identity ) ) ] )
% 98.91/99.32 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 457, [ =( multiply( inverse( Y ), 'greatest_lower_bound'( identity
% 98.91/99.32 , Y ) ), 'greatest_lower_bound'( inverse( Y ), identity ) ) ] )
% 98.91/99.32 , clause( 39643, [ =( multiply( inverse( Y ), 'greatest_lower_bound'(
% 98.91/99.32 identity, Y ) ), 'greatest_lower_bound'( inverse( Y ), identity ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39648, [ =( X, 'least_upper_bound'( 'greatest_lower_bound'( X, Y )
% 98.91/99.32 , X ) ) ] )
% 98.91/99.32 , clause( 31, [ =( 'least_upper_bound'( 'greatest_lower_bound'( X, Y ), X )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39649, [ =( X, 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ) ) ] )
% 98.91/99.32 , clause( 167, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ), multiply(
% 98.91/99.32 X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39648, [ =( X, 'least_upper_bound'( 'greatest_lower_bound'( X
% 98.91/99.32 , Y ), X ) ) ] )
% 98.91/99.32 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, multiply( X, Y ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39650, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ), X ) ] )
% 98.91/99.32 , clause( 39649, [ =( X, 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 472, [ =( 'least_upper_bound'( multiply( X, 'greatest_lower_bound'(
% 98.91/99.32 identity, Y ) ), X ), X ) ] )
% 98.91/99.32 , clause( 39650, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39652, [ =( multiply( X, 'greatest_lower_bound'( identity, Y ) ),
% 98.91/99.32 'greatest_lower_bound'( X, multiply( X, Y ) ) ) ] )
% 98.91/99.32 , clause( 167, [ =( 'greatest_lower_bound'( X, multiply( X, Y ) ), multiply(
% 98.91/99.32 X, 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39654, [ =( multiply( X, identity ), 'greatest_lower_bound'( X,
% 98.91/99.32 multiply( X, 'least_upper_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 21, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X ) )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, clause( 39652, [ =( multiply( X, 'greatest_lower_bound'( identity, Y )
% 98.91/99.32 ), 'greatest_lower_bound'( X, multiply( X, Y ) ) ) ] )
% 98.91/99.32 , 0, 3, substitution( 0, [ :=( X, identity ), :=( Y, Y )] ), substitution(
% 98.91/99.32 1, [ :=( X, X ), :=( Y, 'least_upper_bound'( Y, identity ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39655, [ =( X, 'greatest_lower_bound'( X, multiply( X,
% 98.91/99.32 'least_upper_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.32 , 0, clause( 39654, [ =( multiply( X, identity ), 'greatest_lower_bound'( X
% 98.91/99.32 , multiply( X, 'least_upper_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , 0, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.32 :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39656, [ =( 'greatest_lower_bound'( X, multiply( X,
% 98.91/99.32 'least_upper_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39655, [ =( X, 'greatest_lower_bound'( X, multiply( X,
% 98.91/99.32 'least_upper_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 475, [ =( 'greatest_lower_bound'( Y, multiply( Y,
% 98.91/99.32 'least_upper_bound'( X, identity ) ) ), Y ) ] )
% 98.91/99.32 , clause( 39656, [ =( 'greatest_lower_bound'( X, multiply( X,
% 98.91/99.32 'least_upper_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39657, [ =( X, 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ) ) ] )
% 98.91/99.32 , clause( 472, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ), X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39658, [ =( X, 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ) ) ] )
% 98.91/99.32 , clause( 90, [ =( multiply( X, 'greatest_lower_bound'( Y, Z ) ), multiply(
% 98.91/99.32 X, 'greatest_lower_bound'( Z, Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39657, [ =( X, 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( identity, Y ) ), X ) ) ] )
% 98.91/99.32 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, identity ), :=( Z, Y )] ),
% 98.91/99.32 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39661, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ), X ) ] )
% 98.91/99.32 , clause( 39658, [ =( X, 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 483, [ =( 'least_upper_bound'( multiply( X, 'greatest_lower_bound'(
% 98.91/99.32 Y, identity ) ), X ), X ) ] )
% 98.91/99.32 , clause( 39661, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39663, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'(
% 98.91/99.32 'least_upper_bound'( X, Y ), X ) ) ] )
% 98.91/99.32 , clause( 29, [ =( 'least_upper_bound'( 'least_upper_bound'( X, Y ), X ),
% 98.91/99.32 'least_upper_bound'( X, Y ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39665, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ), 'least_upper_bound'( X,
% 98.91/99.32 multiply( X, 'greatest_lower_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 483, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ), X ) ] )
% 98.91/99.32 , 0, clause( 39663, [ =( 'least_upper_bound'( X, Y ), 'least_upper_bound'(
% 98.91/99.32 'least_upper_bound'( X, Y ), X ) ) ] )
% 98.91/99.32 , 0, 9, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, multiply( X, 'greatest_lower_bound'( Y, identity ) ) ), :=( Y, X )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39666, [ =( X, 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 483, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ), X ) ] )
% 98.91/99.32 , 0, clause( 39665, [ =( 'least_upper_bound'( multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ), X ), 'least_upper_bound'( X,
% 98.91/99.32 multiply( X, 'greatest_lower_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , 0, 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39668, [ =( 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39666, [ =( X, 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 513, [ =( 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39668, [ =( 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39671, [ =( X, 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 513, [ =( 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ), X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39672, [ =( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 identity ) ) ] )
% 98.91/99.32 , clause( 229, [ =( multiply( inverse( 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.32 'greatest_lower_bound'( X, Y ) ), identity ) ] )
% 98.91/99.32 , 0, clause( 39671, [ =( X, 'least_upper_bound'( X, multiply( X,
% 98.91/99.32 'greatest_lower_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, identity )] ),
% 98.91/99.32 substitution( 1, [ :=( X, inverse( 'greatest_lower_bound'( identity, X )
% 98.91/99.32 ) ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39673, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'greatest_lower_bound'( identity, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , clause( 39672, [ =( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 identity ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 522, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'greatest_lower_bound'( identity, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , clause( 39673, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'greatest_lower_bound'( identity, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39675, [ =( X, 'greatest_lower_bound'( X, multiply( X,
% 98.91/99.32 'least_upper_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 475, [ =( 'greatest_lower_bound'( Y, multiply( Y,
% 98.91/99.32 'least_upper_bound'( X, identity ) ) ), Y ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39676, [ =( inverse( 'least_upper_bound'( identity, X ) ),
% 98.91/99.32 'greatest_lower_bound'( inverse( 'least_upper_bound'( identity, X ) ),
% 98.91/99.32 identity ) ) ] )
% 98.91/99.32 , clause( 305, [ =( multiply( inverse( 'least_upper_bound'( Y, X ) ),
% 98.91/99.32 'least_upper_bound'( X, Y ) ), identity ) ] )
% 98.91/99.32 , 0, clause( 39675, [ =( X, 'greatest_lower_bound'( X, multiply( X,
% 98.91/99.32 'least_upper_bound'( Y, identity ) ) ) ) ] )
% 98.91/99.32 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, identity )] ),
% 98.91/99.32 substitution( 1, [ :=( X, inverse( 'least_upper_bound'( identity, X ) ) )
% 98.91/99.32 , :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39677, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'least_upper_bound'( identity, X )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 39676, [ =( inverse( 'least_upper_bound'( identity, X ) ),
% 98.91/99.32 'greatest_lower_bound'( inverse( 'least_upper_bound'( identity, X ) ),
% 98.91/99.32 identity ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 546, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'least_upper_bound'( identity, X )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 39677, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'least_upper_bound'( identity, X )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39680, [ =( multiply( multiply( X, Y ), inverse( Y ) ), X ) ] )
% 98.91/99.32 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.32 , 0, clause( 22, [ =( multiply( multiply( Y, X ), inverse( X ) ), multiply(
% 98.91/99.32 Y, identity ) ) ] )
% 98.91/99.32 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 98.91/99.32 :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 1007, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 98.91/99.32 , clause( 39680, [ =( multiply( multiply( X, Y ), inverse( Y ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39683, [ =( multiply( 'least_upper_bound'( X, Z ), Y ),
% 98.91/99.32 'least_upper_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.32 , clause( 13, [ =( 'least_upper_bound'( multiply( X, Z ), multiply( Y, Z )
% 98.91/99.32 ), multiply( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39685, [ =( multiply( 'least_upper_bound'( X, multiply( Y, Z ) ),
% 98.91/99.32 inverse( Z ) ), 'least_upper_bound'( multiply( X, inverse( Z ) ), Y ) ) ]
% 98.91/99.32 )
% 98.91/99.32 , clause( 1007, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 98.91/99.32 , 0, clause( 39683, [ =( multiply( 'least_upper_bound'( X, Z ), Y ),
% 98.91/99.32 'least_upper_bound'( multiply( X, Y ), multiply( Z, Y ) ) ) ] )
% 98.91/99.32 , 0, 14, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, inverse( Z ) ), :=( Z, multiply( Y, Z ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 1009, [ =( multiply( 'least_upper_bound'( Z, multiply( X, Y ) ),
% 98.91/99.32 inverse( Y ) ), 'least_upper_bound'( multiply( Z, inverse( Y ) ), X ) ) ]
% 98.91/99.32 )
% 98.91/99.32 , clause( 39685, [ =( multiply( 'least_upper_bound'( X, multiply( Y, Z ) )
% 98.91/99.32 , inverse( Z ) ), 'least_upper_bound'( multiply( X, inverse( Z ) ), Y ) )
% 98.91/99.32 ] )
% 98.91/99.32 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 98.91/99.32 permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39688, [ =( multiply( inverse( X ), 'least_upper_bound'( X, Y ) ),
% 98.91/99.32 'least_upper_bound'( identity, multiply( inverse( X ), Y ) ) ) ] )
% 98.91/99.32 , clause( 73, [ =( 'least_upper_bound'( identity, multiply( inverse( X ), Y
% 98.91/99.32 ) ), multiply( inverse( X ), 'least_upper_bound'( X, Y ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39689, [ =( X, multiply( multiply( X, Y ), inverse( Y ) ) ) ] )
% 98.91/99.32 , clause( 1007, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39690, [ =( inverse( X ), multiply( 'least_upper_bound'( identity,
% 98.91/99.32 multiply( inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ) )
% 98.91/99.32 ] )
% 98.91/99.32 , clause( 39688, [ =( multiply( inverse( X ), 'least_upper_bound'( X, Y ) )
% 98.91/99.32 , 'least_upper_bound'( identity, multiply( inverse( X ), Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39689, [ =( X, multiply( multiply( X, Y ), inverse( Y ) ) ) ]
% 98.91/99.32 )
% 98.91/99.32 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, inverse( X ) ), :=( Y, 'least_upper_bound'( X, Y ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39691, [ =( multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.32 inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ), inverse( X
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 39690, [ =( inverse( X ), multiply( 'least_upper_bound'( identity
% 98.91/99.32 , multiply( inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) )
% 98.91/99.32 ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 1741, [ =( multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.32 inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ), inverse( X
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 39691, [ =( multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.32 inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ), inverse( X
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39693, [ =( inverse( Y ), multiply( X, inverse( multiply( Y, X ) )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 183, [ =( multiply( Y, inverse( multiply( X, Y ) ) ), inverse( X
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39695, [ =( inverse( inverse( X ) ), multiply(
% 98.91/99.32 'greatest_lower_bound'( identity, X ), inverse( 'greatest_lower_bound'(
% 98.91/99.32 inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , clause( 457, [ =( multiply( inverse( Y ), 'greatest_lower_bound'(
% 98.91/99.32 identity, Y ) ), 'greatest_lower_bound'( inverse( Y ), identity ) ) ] )
% 98.91/99.32 , 0, clause( 39693, [ =( inverse( Y ), multiply( X, inverse( multiply( Y, X
% 98.91/99.32 ) ) ) ) ] )
% 98.91/99.32 , 0, 9, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.32 :=( X, 'greatest_lower_bound'( identity, X ) ), :=( Y, inverse( X ) )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39696, [ =( X, multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39695, [ =( inverse( inverse( X ) ), multiply(
% 98.91/99.32 'greatest_lower_bound'( identity, X ), inverse( 'greatest_lower_bound'(
% 98.91/99.32 inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , 0, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39697, [ =( multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39696, [ =( X, multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 2160, [ =( multiply( 'greatest_lower_bound'( identity, X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39697, [ =( multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39699, [ =( 'greatest_lower_bound'( Y, Z ), 'least_upper_bound'(
% 98.91/99.32 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ), Z ),
% 98.91/99.32 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.32 , clause( 44, [ =( 'least_upper_bound'( 'greatest_lower_bound'(
% 98.91/99.32 'greatest_lower_bound'( X, Y ), Z ), 'greatest_lower_bound'( Y, Z ) ),
% 98.91/99.32 'greatest_lower_bound'( Y, Z ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39702, [ =( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 'least_upper_bound'( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, Y ) ), X ), 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , clause( 546, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'least_upper_bound'( identity, X )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , 0, clause( 39699, [ =( 'greatest_lower_bound'( Y, Z ),
% 98.91/99.32 'least_upper_bound'( 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y
% 98.91/99.32 ), Z ), 'greatest_lower_bound'( Y, Z ) ) ) ] )
% 98.91/99.32 , 0, 6, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, inverse(
% 98.91/99.32 'least_upper_bound'( identity, Y ) ) ), :=( Y, identity ), :=( Z, X )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39707, [ =( 'least_upper_bound'( 'greatest_lower_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( identity, Y ) ), X ), 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.32 , clause( 39702, [ =( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 'least_upper_bound'( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, Y ) ), X ), 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 2575, [ =( 'least_upper_bound'( 'greatest_lower_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( identity, X ) ), Y ), 'greatest_lower_bound'(
% 98.91/99.32 identity, Y ) ), 'greatest_lower_bound'( identity, Y ) ) ] )
% 98.91/99.32 , clause( 39707, [ =( 'least_upper_bound'( 'greatest_lower_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( identity, Y ) ), X ), 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39709, [ =( multiply( 'greatest_lower_bound'( X, identity ), Y ),
% 98.91/99.32 'greatest_lower_bound'( multiply( X, Y ), Y ) ) ] )
% 98.91/99.32 , clause( 166, [ =( 'greatest_lower_bound'( multiply( Y, X ), X ), multiply(
% 98.91/99.32 'greatest_lower_bound'( Y, identity ), X ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39714, [ =( multiply( 'greatest_lower_bound'(
% 98.91/99.32 'greatest_lower_bound'( identity, X ), identity ), inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ),
% 98.91/99.32 'greatest_lower_bound'( X, inverse( 'greatest_lower_bound'( inverse( X )
% 98.91/99.32 , identity ) ) ) ) ] )
% 98.91/99.32 , clause( 2160, [ =( multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39709, [ =( multiply( 'greatest_lower_bound'( X, identity ), Y
% 98.91/99.32 ), 'greatest_lower_bound'( multiply( X, Y ), Y ) ) ] )
% 98.91/99.32 , 0, 13, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X,
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ), :=( Y, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39715, [ =( multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ),
% 98.91/99.32 'greatest_lower_bound'( X, inverse( 'greatest_lower_bound'( inverse( X )
% 98.91/99.32 , identity ) ) ) ) ] )
% 98.91/99.32 , clause( 27, [ =( 'greatest_lower_bound'( 'greatest_lower_bound'( X, Y ),
% 98.91/99.32 X ), 'greatest_lower_bound'( X, Y ) ) ] )
% 98.91/99.32 , 0, clause( 39714, [ =( multiply( 'greatest_lower_bound'(
% 98.91/99.32 'greatest_lower_bound'( identity, X ), identity ), inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ),
% 98.91/99.32 'greatest_lower_bound'( X, inverse( 'greatest_lower_bound'( inverse( X )
% 98.91/99.32 , identity ) ) ) ) ] )
% 98.91/99.32 , 0, 2, substitution( 0, [ :=( X, identity ), :=( Y, X )] ), substitution(
% 98.91/99.32 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39716, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , clause( 2160, [ =( multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39715, [ =( multiply( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( inverse( X ), identity ) ) ),
% 98.91/99.32 'greatest_lower_bound'( X, inverse( 'greatest_lower_bound'( inverse( X )
% 98.91/99.32 , identity ) ) ) ) ] )
% 98.91/99.32 , 0, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39717, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39716, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 3198, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , clause( 39717, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39718, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , clause( 3198, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ), X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39719, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( X ) ) ) ) ) ] )
% 98.91/99.32 , clause( 213, [ =( inverse( 'greatest_lower_bound'( Y, X ) ), inverse(
% 98.91/99.32 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39718, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( inverse( X ), identity ) ) ) ) ] )
% 98.91/99.32 , 0, 4, substitution( 0, [ :=( X, identity ), :=( Y, inverse( X ) )] ),
% 98.91/99.32 substitution( 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39725, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , clause( 39719, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( X ) ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 3227, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , clause( 39725, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39729, [ =( 'greatest_lower_bound'( X, multiply( Z, inverse( Y ) )
% 98.91/99.32 ), multiply( 'greatest_lower_bound'( multiply( X, Y ), Z ), inverse( Y )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 153, [ =( multiply( 'greatest_lower_bound'( multiply( X, Y ), Z )
% 98.91/99.32 , inverse( Y ) ), 'greatest_lower_bound'( X, multiply( Z, inverse( Y ) )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39734, [ =( 'greatest_lower_bound'( X, multiply( inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( multiply( X, Y ) ) ) ),
% 98.91/99.32 inverse( Y ) ) ), multiply( multiply( X, Y ), inverse( Y ) ) ) ] )
% 98.91/99.32 , clause( 3227, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39729, [ =( 'greatest_lower_bound'( X, multiply( Z, inverse( Y
% 98.91/99.32 ) ) ), multiply( 'greatest_lower_bound'( multiply( X, Y ), Z ), inverse(
% 98.91/99.32 Y ) ) ) ] )
% 98.91/99.32 , 0, 14, substitution( 0, [ :=( X, multiply( X, Y ) )] ), substitution( 1
% 98.91/99.32 , [ :=( X, X ), :=( Y, Y ), :=( Z, inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, inverse( multiply( X, Y ) ) ) ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39735, [ =( 'greatest_lower_bound'( X, multiply( inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( multiply( X, Y ) ) ) ),
% 98.91/99.32 inverse( Y ) ) ), X ) ] )
% 98.91/99.32 , clause( 1007, [ =( multiply( multiply( Y, X ), inverse( X ) ), Y ) ] )
% 98.91/99.32 , 0, clause( 39734, [ =( 'greatest_lower_bound'( X, multiply( inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( multiply( X, Y ) ) ) ),
% 98.91/99.32 inverse( Y ) ) ), multiply( multiply( X, Y ), inverse( Y ) ) ) ] )
% 98.91/99.32 , 0, 13, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39736, [ =( 'greatest_lower_bound'( X, inverse( multiply( Y,
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( multiply( X, Y ) ) ) ) ) ), X
% 98.91/99.32 ) ] )
% 98.91/99.32 , clause( 17, [ =( multiply( inverse( Y ), inverse( X ) ), inverse(
% 98.91/99.32 multiply( X, Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39735, [ =( 'greatest_lower_bound'( X, multiply( inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( multiply( X, Y ) ) ) ),
% 98.91/99.32 inverse( Y ) ) ), X ) ] )
% 98.91/99.32 , 0, 3, substitution( 0, [ :=( X, Y ), :=( Y, 'greatest_lower_bound'(
% 98.91/99.32 identity, inverse( multiply( X, Y ) ) ) )] ), substitution( 1, [ :=( X, X
% 98.91/99.32 ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39737, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( multiply( Y, identity ), inverse( X ) ) ) ), X )
% 98.91/99.32 ] )
% 98.91/99.32 , clause( 195, [ =( multiply( X, 'greatest_lower_bound'( Z, inverse(
% 98.91/99.32 multiply( Y, X ) ) ) ), 'greatest_lower_bound'( multiply( X, Z ), inverse(
% 98.91/99.32 Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39736, [ =( 'greatest_lower_bound'( X, inverse( multiply( Y,
% 98.91/99.32 'greatest_lower_bound'( identity, inverse( multiply( X, Y ) ) ) ) ) ), X
% 98.91/99.32 ) ] )
% 98.91/99.32 , 0, 4, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, identity )] ),
% 98.91/99.32 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39738, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , clause( 152, [ =( multiply( X, identity ), X ) ] )
% 98.91/99.32 , 0, clause( 39737, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( multiply( Y, identity ), inverse( X ) ) ) ), X )
% 98.91/99.32 ] )
% 98.91/99.32 , 0, 5, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.32 :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 4702, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , clause( 39738, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39741, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, inverse( X ) ) ) ) ) ] )
% 98.91/99.32 , clause( 4702, [ =( 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, inverse( X ) ) ) ), X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39742, [ =( inverse( X ), 'greatest_lower_bound'( inverse( X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( Y, X ) ) ) ) ] )
% 98.91/99.32 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39741, [ =( X, 'greatest_lower_bound'( X, inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, inverse( X ) ) ) ) ) ] )
% 98.91/99.32 , 0, 9, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, inverse(
% 98.91/99.32 X ) ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39743, [ =( 'greatest_lower_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( X ) ) ] )
% 98.91/99.32 , clause( 39742, [ =( inverse( X ), 'greatest_lower_bound'( inverse( X ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( Y, X ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 4745, [ =( 'greatest_lower_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( X ) ) ] )
% 98.91/99.32 , clause( 39743, [ =( 'greatest_lower_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( X ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39745, [ =( Y, 'least_upper_bound'( 'greatest_lower_bound'( X, Y )
% 98.91/99.32 , Y ) ) ] )
% 98.91/99.32 , clause( 43, [ =( 'least_upper_bound'( 'greatest_lower_bound'( Y, X ), X )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39746, [ =( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.32 'least_upper_bound'( inverse( Y ), inverse( 'greatest_lower_bound'( X, Y
% 98.91/99.32 ) ) ) ) ] )
% 98.91/99.32 , clause( 4745, [ =( 'greatest_lower_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( X ) ) ] )
% 98.91/99.32 , 0, clause( 39745, [ =( Y, 'least_upper_bound'( 'greatest_lower_bound'( X
% 98.91/99.32 , Y ), Y ) ) ] )
% 98.91/99.32 , 0, 6, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.32 :=( X, inverse( Y ) ), :=( Y, inverse( 'greatest_lower_bound'( X, Y ) ) )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39747, [ =( 'least_upper_bound'( inverse( Y ), inverse(
% 98.91/99.32 'greatest_lower_bound'( X, Y ) ) ), inverse( 'greatest_lower_bound'( X, Y
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , clause( 39746, [ =( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.32 'least_upper_bound'( inverse( Y ), inverse( 'greatest_lower_bound'( X, Y
% 98.91/99.32 ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 4830, [ =( 'least_upper_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( 'greatest_lower_bound'( Y, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , clause( 39747, [ =( 'least_upper_bound'( inverse( Y ), inverse(
% 98.91/99.32 'greatest_lower_bound'( X, Y ) ) ), inverse( 'greatest_lower_bound'( X, Y
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39749, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , clause( 30, [ =( 'least_upper_bound'( X, 'greatest_lower_bound'( Y, X ) )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39750, [ =( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( X, Y ) ), inverse(
% 98.91/99.32 Y ) ) ) ] )
% 98.91/99.32 , clause( 4745, [ =( 'greatest_lower_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( X ) ) ] )
% 98.91/99.32 , 0, clause( 39749, [ =( X, 'least_upper_bound'( X, 'greatest_lower_bound'(
% 98.91/99.32 Y, X ) ) ) ] )
% 98.91/99.32 , 0, 10, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.32 :=( X, inverse( 'greatest_lower_bound'( X, Y ) ) ), :=( Y, inverse( Y ) )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39751, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'( X
% 98.91/99.32 , Y ) ), inverse( Y ) ), inverse( 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.32 , clause( 39750, [ =( inverse( 'greatest_lower_bound'( X, Y ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( X, Y ) ), inverse(
% 98.91/99.32 Y ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 4831, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'( Y
% 98.91/99.32 , X ) ), inverse( X ) ), inverse( 'greatest_lower_bound'( Y, X ) ) ) ] )
% 98.91/99.32 , clause( 39751, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 X, Y ) ), inverse( Y ) ), inverse( 'greatest_lower_bound'( X, Y ) ) ) ]
% 98.91/99.32 )
% 98.91/99.32 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39753, [ =( inverse( 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( X ), inverse( 'greatest_lower_bound'( Y, X
% 98.91/99.32 ) ) ) ) ] )
% 98.91/99.32 , clause( 4830, [ =( 'least_upper_bound'( inverse( X ), inverse(
% 98.91/99.32 'greatest_lower_bound'( Y, X ) ) ), inverse( 'greatest_lower_bound'( Y, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39757, [ =( inverse( 'greatest_lower_bound'( X, 'least_upper_bound'(
% 98.91/99.32 Y, X ) ) ), 'least_upper_bound'( inverse( 'least_upper_bound'( Y, X ) ),
% 98.91/99.32 inverse( X ) ) ) ] )
% 98.91/99.32 , clause( 21, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X ) )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, clause( 39753, [ =( inverse( 'greatest_lower_bound'( Y, X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( X ), inverse( 'greatest_lower_bound'( Y, X
% 98.91/99.32 ) ) ) ) ] )
% 98.91/99.32 , 0, 13, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, 'least_upper_bound'( Y, X ) ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39758, [ =( inverse( X ), 'least_upper_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( Y, X ) ), inverse( X ) ) ) ] )
% 98.91/99.32 , clause( 21, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( Y, X ) )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, clause( 39757, [ =( inverse( 'greatest_lower_bound'( X,
% 98.91/99.32 'least_upper_bound'( Y, X ) ) ), 'least_upper_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( Y, X ) ), inverse( X ) ) ) ] )
% 98.91/99.32 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 98.91/99.32 :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39760, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y, X
% 98.91/99.32 ) ), inverse( X ) ), inverse( X ) ) ] )
% 98.91/99.32 , clause( 39758, [ =( inverse( X ), 'least_upper_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( Y, X ) ), inverse( X ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 5295, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y, X
% 98.91/99.32 ) ), inverse( X ) ), inverse( X ) ) ] )
% 98.91/99.32 , clause( 39760, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y
% 98.91/99.32 , X ) ), inverse( X ) ), inverse( X ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39763, [ =( inverse( Y ), 'least_upper_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( X, Y ) ), inverse( Y ) ) ) ] )
% 98.91/99.32 , clause( 5295, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y,
% 98.91/99.32 X ) ), inverse( X ) ), inverse( X ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39765, [ =( inverse( inverse( X ) ), 'least_upper_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( Y, inverse( X ) ) ), X ) ) ] )
% 98.91/99.32 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39763, [ =( inverse( Y ), 'least_upper_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( X, Y ) ), inverse( Y ) ) ) ] )
% 98.91/99.32 , 0, 10, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 98.91/99.32 :=( Y, inverse( X ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39766, [ =( X, 'least_upper_bound'( inverse( 'least_upper_bound'( Y
% 98.91/99.32 , inverse( X ) ) ), X ) ) ] )
% 98.91/99.32 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39765, [ =( inverse( inverse( X ) ), 'least_upper_bound'(
% 98.91/99.32 inverse( 'least_upper_bound'( Y, inverse( X ) ) ), X ) ) ] )
% 98.91/99.32 , 0, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 98.91/99.32 :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39768, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y,
% 98.91/99.32 inverse( X ) ) ), X ), X ) ] )
% 98.91/99.32 , clause( 39766, [ =( X, 'least_upper_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 Y, inverse( X ) ) ), X ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 5310, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y,
% 98.91/99.32 inverse( X ) ) ), X ), X ) ] )
% 98.91/99.32 , clause( 39768, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y
% 98.91/99.32 , inverse( X ) ) ), X ), X ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39771, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , clause( 10, [ =( 'greatest_lower_bound'( X, 'least_upper_bound'( X, Y ) )
% 98.91/99.32 , X ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39772, [ =( inverse( 'least_upper_bound'( X, inverse( Y ) ) ),
% 98.91/99.32 'greatest_lower_bound'( inverse( 'least_upper_bound'( X, inverse( Y ) ) )
% 98.91/99.32 , Y ) ) ] )
% 98.91/99.32 , clause( 5310, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'( Y,
% 98.91/99.32 inverse( X ) ) ), X ), X ) ] )
% 98.91/99.32 , 0, clause( 39771, [ =( X, 'greatest_lower_bound'( X, 'least_upper_bound'(
% 98.91/99.32 X, Y ) ) ) ] )
% 98.91/99.32 , 0, 12, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 98.91/99.32 :=( X, inverse( 'least_upper_bound'( X, inverse( Y ) ) ) ), :=( Y, Y )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39773, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'( X
% 98.91/99.32 , inverse( Y ) ) ), Y ), inverse( 'least_upper_bound'( X, inverse( Y ) )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 39772, [ =( inverse( 'least_upper_bound'( X, inverse( Y ) ) ),
% 98.91/99.32 'greatest_lower_bound'( inverse( 'least_upper_bound'( X, inverse( Y ) ) )
% 98.91/99.32 , Y ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 5364, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'( X
% 98.91/99.32 , inverse( Y ) ) ), Y ), inverse( 'least_upper_bound'( X, inverse( Y ) )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , clause( 39773, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 X, inverse( Y ) ) ), Y ), inverse( 'least_upper_bound'( X, inverse( Y ) )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 98.91/99.32 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39775, [ =( 'greatest_lower_bound'( identity, Y ),
% 98.91/99.32 'least_upper_bound'( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, X ) ), Y ), 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.32 , clause( 2575, [ =( 'least_upper_bound'( 'greatest_lower_bound'( inverse(
% 98.91/99.32 'least_upper_bound'( identity, X ) ), Y ), 'greatest_lower_bound'(
% 98.91/99.32 identity, Y ) ), 'greatest_lower_bound'( identity, Y ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39776, [ =( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 'least_upper_bound'( inverse( 'least_upper_bound'( identity, inverse( X )
% 98.91/99.32 ) ), 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , clause( 5364, [ =( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 X, inverse( Y ) ) ), Y ), inverse( 'least_upper_bound'( X, inverse( Y ) )
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , 0, clause( 39775, [ =( 'greatest_lower_bound'( identity, Y ),
% 98.91/99.32 'least_upper_bound'( 'greatest_lower_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, X ) ), Y ), 'greatest_lower_bound'( identity, Y ) ) ) ] )
% 98.91/99.32 , 0, 5, substitution( 0, [ :=( X, identity ), :=( Y, X )] ), substitution(
% 98.91/99.32 1, [ :=( X, inverse( X ) ), :=( Y, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39777, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, inverse( X ) ) ), 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.32 , clause( 39776, [ =( 'greatest_lower_bound'( identity, X ),
% 98.91/99.32 'least_upper_bound'( inverse( 'least_upper_bound'( identity, inverse( X )
% 98.91/99.32 ) ), 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 38541, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, inverse( X ) ) ), 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.32 , clause( 39777, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, inverse( X ) ) ), 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39779, [ =( inverse( X ), multiply( 'least_upper_bound'( identity,
% 98.91/99.32 multiply( inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ) )
% 98.91/99.32 ] )
% 98.91/99.32 , clause( 1741, [ =( multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.32 inverse( X ), Y ) ), inverse( 'least_upper_bound'( X, Y ) ) ), inverse( X
% 98.91/99.32 ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39786, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.32 inverse( inverse( 'least_upper_bound'( identity, inverse( X ) ) ) ),
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ), inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ) ) ] )
% 98.91/99.32 , clause( 38541, [ =( 'least_upper_bound'( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, inverse( X ) ) ), 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ] )
% 98.91/99.32 , 0, clause( 39779, [ =( inverse( X ), multiply( 'least_upper_bound'(
% 98.91/99.32 identity, multiply( inverse( X ), Y ) ), inverse( 'least_upper_bound'( X
% 98.91/99.32 , Y ) ) ) ) ] )
% 98.91/99.32 , 0, 21, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X,
% 98.91/99.32 inverse( 'least_upper_bound'( identity, inverse( X ) ) ) ), :=( Y,
% 98.91/99.32 'greatest_lower_bound'( identity, X ) )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39787, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), 'least_upper_bound'( multiply( identity, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ), inverse( inverse(
% 98.91/99.32 'least_upper_bound'( identity, inverse( X ) ) ) ) ) ) ] )
% 98.91/99.32 , clause( 1009, [ =( multiply( 'least_upper_bound'( Z, multiply( X, Y ) ),
% 98.91/99.32 inverse( Y ) ), 'least_upper_bound'( multiply( Z, inverse( Y ) ), X ) ) ]
% 98.91/99.32 )
% 98.91/99.32 , 0, clause( 39786, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), multiply( 'least_upper_bound'( identity, multiply(
% 98.91/99.32 inverse( inverse( 'least_upper_bound'( identity, inverse( X ) ) ) ),
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ), inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ) ) ] )
% 98.91/99.32 , 0, 7, substitution( 0, [ :=( X, inverse( inverse( 'least_upper_bound'(
% 98.91/99.32 identity, inverse( X ) ) ) ) ), :=( Y, 'greatest_lower_bound'( identity,
% 98.91/99.32 X ) ), :=( Z, identity )] ), substitution( 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39788, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), inverse( inverse( 'least_upper_bound'( identity, inverse(
% 98.91/99.32 X ) ) ) ) ) ) ] )
% 98.91/99.32 , clause( 0, [ =( multiply( identity, X ), X ) ] )
% 98.91/99.32 , 0, clause( 39787, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), 'least_upper_bound'( multiply( identity, inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ), inverse( inverse(
% 98.91/99.32 'least_upper_bound'( identity, inverse( X ) ) ) ) ) ) ] )
% 98.91/99.32 , 0, 8, substitution( 0, [ :=( X, inverse( 'greatest_lower_bound'( identity
% 98.91/99.32 , X ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39790, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), 'least_upper_bound'( identity, inverse( X ) ) ) ) ] )
% 98.91/99.32 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39788, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), inverse( inverse( 'least_upper_bound'( identity, inverse(
% 98.91/99.32 X ) ) ) ) ) ) ] )
% 98.91/99.32 , 0, 12, substitution( 0, [ :=( X, 'least_upper_bound'( identity, inverse(
% 98.91/99.32 X ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39791, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'least_upper_bound'( identity, inverse( X ) ) ) ) ] )
% 98.91/99.32 , clause( 16, [ =( inverse( inverse( X ) ), X ) ] )
% 98.91/99.32 , 0, clause( 39790, [ =( inverse( inverse( 'least_upper_bound'( identity,
% 98.91/99.32 inverse( X ) ) ) ), 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), 'least_upper_bound'( identity, inverse( X ) ) ) ) ] )
% 98.91/99.32 , 0, 1, substitution( 0, [ :=( X, 'least_upper_bound'( identity, inverse( X
% 98.91/99.32 ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39796, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 'least_upper_bound'( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( X ) ) ) ] )
% 98.91/99.32 , clause( 6, [ =( 'least_upper_bound'( X, 'least_upper_bound'( Y, Z ) ),
% 98.91/99.32 'least_upper_bound'( 'least_upper_bound'( X, Y ), Z ) ) ] )
% 98.91/99.32 , 0, clause( 39791, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 'least_upper_bound'( identity, inverse( X ) ) ) ) ] )
% 98.91/99.32 , 0, 5, substitution( 0, [ :=( X, inverse( 'greatest_lower_bound'( identity
% 98.91/99.32 , X ) ) ), :=( Y, identity ), :=( Z, inverse( X ) )] ), substitution( 1
% 98.91/99.32 , [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39797, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 inverse( X ) ) ) ] )
% 98.91/99.32 , clause( 522, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( 'greatest_lower_bound'( identity, X
% 98.91/99.32 ) ) ) ] )
% 98.91/99.32 , 0, clause( 39796, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 'least_upper_bound'( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 identity, X ) ), identity ), inverse( X ) ) ) ] )
% 98.91/99.32 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 98.91/99.32 ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39798, [ =( 'least_upper_bound'( identity, inverse( X ) ), inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , clause( 4831, [ =( 'least_upper_bound'( inverse( 'greatest_lower_bound'(
% 98.91/99.32 Y, X ) ), inverse( X ) ), inverse( 'greatest_lower_bound'( Y, X ) ) ) ]
% 98.91/99.32 )
% 98.91/99.32 , 0, clause( 39797, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 'least_upper_bound'( inverse( 'greatest_lower_bound'( identity, X ) ),
% 98.91/99.32 inverse( X ) ) ) ] )
% 98.91/99.32 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, identity )] ), substitution(
% 98.91/99.32 1, [ :=( X, X )] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 38556, [ =( 'least_upper_bound'( identity, inverse( X ) ), inverse(
% 98.91/99.32 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , clause( 39798, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39801, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.32 'least_upper_bound'( identity, inverse( a ) ) ) ) ] )
% 98.91/99.32 , clause( 78, [ ~( =( 'least_upper_bound'( identity, inverse( a ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39802, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( identity, a ) ) ) ) ] )
% 98.91/99.32 , clause( 38556, [ =( 'least_upper_bound'( identity, inverse( X ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( identity, X ) ) ) ] )
% 98.91/99.32 , 0, clause( 39801, [ ~( =( inverse( 'greatest_lower_bound'( a, identity )
% 98.91/99.32 ), 'least_upper_bound'( identity, inverse( a ) ) ) ) ] )
% 98.91/99.32 , 0, 6, substitution( 0, [ :=( X, a )] ), substitution( 1, [] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39803, [ ~( =( inverse( 'greatest_lower_bound'( identity, a ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 39802, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( identity, a ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 38696, [ ~( =( inverse( 'greatest_lower_bound'( identity, a ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 39803, [ ~( =( inverse( 'greatest_lower_bound'( identity, a ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqswap(
% 98.91/99.32 clause( 39804, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( identity, a ) ) ) ) ] )
% 98.91/99.32 , clause( 38696, [ ~( =( inverse( 'greatest_lower_bound'( identity, a ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 paramod(
% 98.91/99.32 clause( 39806, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , clause( 213, [ =( inverse( 'greatest_lower_bound'( Y, X ) ), inverse(
% 98.91/99.32 'greatest_lower_bound'( X, Y ) ) ) ] )
% 98.91/99.32 , 0, clause( 39804, [ ~( =( inverse( 'greatest_lower_bound'( a, identity )
% 98.91/99.32 ), inverse( 'greatest_lower_bound'( identity, a ) ) ) ) ] )
% 98.91/99.32 , 0, 6, substitution( 0, [ :=( X, a ), :=( Y, identity )] ), substitution(
% 98.91/99.32 1, [] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 eqrefl(
% 98.91/99.32 clause( 39809, [] )
% 98.91/99.32 , clause( 39806, [ ~( =( inverse( 'greatest_lower_bound'( a, identity ) ),
% 98.91/99.32 inverse( 'greatest_lower_bound'( a, identity ) ) ) ) ] )
% 98.91/99.32 , 0, substitution( 0, [] )).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 subsumption(
% 98.91/99.32 clause( 39291, [] )
% 98.91/99.32 , clause( 39809, [] )
% 98.91/99.32 , substitution( 0, [] ), permutation( 0, [] ) ).
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 end.
% 98.91/99.32
% 98.91/99.32 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 98.91/99.32
% 98.91/99.32 Memory use:
% 98.91/99.32
% 98.91/99.32 space for terms: 565288
% 98.91/99.32 space for clauses: 4112088
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 clauses generated: 28834930
% 98.91/99.32 clauses kept: 39292
% 98.91/99.32 clauses selected: 6985
% 98.91/99.32 clauses deleted: 2227
% 98.91/99.32 clauses inuse deleted: 134
% 98.91/99.32
% 98.91/99.32 subsentry: 1206780
% 98.91/99.32 literals s-matched: 1205622
% 98.91/99.32 literals matched: 1205572
% 98.91/99.32 full subsumption: 0
% 98.91/99.32
% 98.91/99.32 checksum: 1607774239
% 98.91/99.32
% 98.91/99.32
% 98.91/99.32 Bliksem ended
%------------------------------------------------------------------------------