%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CAT010-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 14 23:54:11 EDT 2022
% Result : Unsatisfiable 34.52s 34.99s
% Output : Refutation 34.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : CAT010-1 : TPTP v8.1.0. Released v1.0.0.
% 0.02/0.09 % Command : bliksem %s
% 0.08/0.29 % Computer : n032.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % DateTime : Sun May 29 16:41:56 EDT 2022
% 0.08/0.29 % CPUTime :
% 34.52/34.99 *** allocated 10000 integers for termspace/termends
% 34.52/34.99 *** allocated 10000 integers for clauses
% 34.52/34.99 *** allocated 10000 integers for justifications
% 34.52/34.99 Bliksem 1.12
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Automatic Strategy Selection
% 34.52/34.99
% 34.52/34.99 Clauses:
% 34.52/34.99 [
% 34.52/34.99 [ ~( defined( X, Y ) ), product( X, Y, compose( X, Y ) ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), defined( X, Y ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( defined( Z, T ) ), defined( Y, T ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( product( Y, T, U ) ), ~( defined( Z, T ) )
% 34.52/34.99 , defined( X, U ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( product( Z, T, U ) ), ~( product( Y, T, W
% 34.52/34.99 ) ), product( X, W, U ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined( T, X ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( product( T, X, U ) ), ~( defined( T, Z ) )
% 34.52/34.99 , defined( U, Y ) ],
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( product( T, Z, U ) ), ~( product( T, X, W
% 34.52/34.99 ) ), product( W, Y, U ) ],
% 34.52/34.99 [ ~( defined( X, Y ) ), ~( defined( Y, Z ) ), ~( 'identity_map'( Y ) ),
% 34.52/34.99 defined( X, Z ) ],
% 34.52/34.99 [ 'identity_map'( domain( X ) ) ],
% 34.52/34.99 [ 'identity_map'( codomain( X ) ) ],
% 34.52/34.99 [ defined( X, domain( X ) ) ],
% 34.52/34.99 [ defined( codomain( X ), X ) ],
% 34.52/34.99 [ product( X, domain( X ), X ) ],
% 34.52/34.99 [ product( codomain( X ), X, X ) ],
% 34.52/34.99 [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product( X, Y, Y ) ]
% 34.52/34.99 ,
% 34.52/34.99 [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product( X, Y, X ) ]
% 34.52/34.99 ,
% 34.52/34.99 [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T ) ],
% 34.52/34.99 [ defined( b, a ) ],
% 34.52/34.99 [ ~( =( codomain( compose( b, a ) ), codomain( b ) ) ) ]
% 34.52/34.99 ] .
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 percentage equality = 0.042553, percentage horn = 1.000000
% 34.52/34.99 This is a problem with some equality
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Options Used:
% 34.52/34.99
% 34.52/34.99 useres = 1
% 34.52/34.99 useparamod = 1
% 34.52/34.99 useeqrefl = 1
% 34.52/34.99 useeqfact = 1
% 34.52/34.99 usefactor = 1
% 34.52/34.99 usesimpsplitting = 0
% 34.52/34.99 usesimpdemod = 5
% 34.52/34.99 usesimpres = 3
% 34.52/34.99
% 34.52/34.99 resimpinuse = 1000
% 34.52/34.99 resimpclauses = 20000
% 34.52/34.99 substype = eqrewr
% 34.52/34.99 backwardsubs = 1
% 34.52/34.99 selectoldest = 5
% 34.52/34.99
% 34.52/34.99 litorderings [0] = split
% 34.52/34.99 litorderings [1] = extend the termordering, first sorting on arguments
% 34.52/34.99
% 34.52/34.99 termordering = kbo
% 34.52/34.99
% 34.52/34.99 litapriori = 0
% 34.52/34.99 termapriori = 1
% 34.52/34.99 litaposteriori = 0
% 34.52/34.99 termaposteriori = 0
% 34.52/34.99 demodaposteriori = 0
% 34.52/34.99 ordereqreflfact = 0
% 34.52/34.99
% 34.52/34.99 litselect = negord
% 34.52/34.99
% 34.52/34.99 maxweight = 15
% 34.52/34.99 maxdepth = 30000
% 34.52/34.99 maxlength = 115
% 34.52/34.99 maxnrvars = 195
% 34.52/34.99 excuselevel = 1
% 34.52/34.99 increasemaxweight = 1
% 34.52/34.99
% 34.52/34.99 maxselected = 10000000
% 34.52/34.99 maxnrclauses = 10000000
% 34.52/34.99
% 34.52/34.99 showgenerated = 0
% 34.52/34.99 showkept = 0
% 34.52/34.99 showselected = 0
% 34.52/34.99 showdeleted = 0
% 34.52/34.99 showresimp = 1
% 34.52/34.99 showstatus = 2000
% 34.52/34.99
% 34.52/34.99 prologoutput = 1
% 34.52/34.99 nrgoals = 5000000
% 34.52/34.99 totalproof = 1
% 34.52/34.99
% 34.52/34.99 Symbols occurring in the translation:
% 34.52/34.99
% 34.52/34.99 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 34.52/34.99 . [1, 2] (w:1, o:26, a:1, s:1, b:0),
% 34.52/34.99 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 34.52/34.99 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 34.52/34.99 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 34.52/34.99 defined [41, 2] (w:1, o:52, a:1, s:1, b:0),
% 34.52/34.99 compose [42, 2] (w:1, o:51, a:1, s:1, b:0),
% 34.52/34.99 product [43, 3] (w:1, o:53, a:1, s:1, b:0),
% 34.52/34.99 'identity_map' [48, 1] (w:1, o:23, a:1, s:1, b:0),
% 34.52/34.99 domain [49, 1] (w:1, o:25, a:1, s:1, b:0),
% 34.52/34.99 codomain [50, 1] (w:1, o:24, a:1, s:1, b:0),
% 34.52/34.99 b [52, 0] (w:1, o:17, a:1, s:1, b:0),
% 34.52/34.99 a [53, 0] (w:1, o:16, a:1, s:1, b:0).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Starting Search:
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 4742
% 34.52/34.99 Kept: 2002
% 34.52/34.99 Inuse: 130
% 34.52/34.99 Deleted: 0
% 34.52/34.99 Deletedinuse: 0
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 10673
% 34.52/34.99 Kept: 4058
% 34.52/34.99 Inuse: 224
% 34.52/34.99 Deleted: 8
% 34.52/34.99 Deletedinuse: 6
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 17007
% 34.52/34.99 Kept: 6081
% 34.52/34.99 Inuse: 302
% 34.52/34.99 Deleted: 15
% 34.52/34.99 Deletedinuse: 6
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 23728
% 34.52/34.99 Kept: 8087
% 34.52/34.99 Inuse: 363
% 34.52/34.99 Deleted: 41
% 34.52/34.99 Deletedinuse: 29
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 32056
% 34.52/34.99 Kept: 11373
% 34.52/34.99 Inuse: 408
% 34.52/34.99 Deleted: 59
% 34.52/34.99 Deletedinuse: 45
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 41047
% 34.52/34.99 Kept: 13392
% 34.52/34.99 Inuse: 451
% 34.52/34.99 Deleted: 207
% 34.52/34.99 Deletedinuse: 186
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 50352
% 34.52/34.99 Kept: 15424
% 34.52/34.99 Inuse: 513
% 34.52/34.99 Deleted: 268
% 34.52/34.99 Deletedinuse: 238
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 59593
% 34.52/34.99 Kept: 17429
% 34.52/34.99 Inuse: 559
% 34.52/34.99 Deleted: 283
% 34.52/34.99 Deletedinuse: 243
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 69153
% 34.52/34.99 Kept: 19549
% 34.52/34.99 Inuse: 603
% 34.52/34.99 Deleted: 400
% 34.52/34.99 Deletedinuse: 267
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying clauses:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 87662
% 34.52/34.99 Kept: 21585
% 34.52/34.99 Inuse: 651
% 34.52/34.99 Deleted: 10151
% 34.52/34.99 Deletedinuse: 271
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 103193
% 34.52/34.99 Kept: 23588
% 34.52/34.99 Inuse: 711
% 34.52/34.99 Deleted: 10164
% 34.52/34.99 Deletedinuse: 284
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 112134
% 34.52/34.99 Kept: 25617
% 34.52/34.99 Inuse: 750
% 34.52/34.99 Deleted: 10220
% 34.52/34.99 Deletedinuse: 337
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 121940
% 34.52/34.99 Kept: 27662
% 34.52/34.99 Inuse: 808
% 34.52/34.99 Deleted: 10247
% 34.52/34.99 Deletedinuse: 348
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 134603
% 34.52/34.99 Kept: 29671
% 34.52/34.99 Inuse: 869
% 34.52/34.99 Deleted: 10270
% 34.52/34.99 Deletedinuse: 362
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 155204
% 34.52/34.99 Kept: 31678
% 34.52/34.99 Inuse: 916
% 34.52/34.99 Deleted: 10301
% 34.52/34.99 Deletedinuse: 362
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 173047
% 34.52/34.99 Kept: 33712
% 34.52/34.99 Inuse: 959
% 34.52/34.99 Deleted: 10313
% 34.52/34.99 Deletedinuse: 363
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 186370
% 34.52/34.99 Kept: 35867
% 34.52/34.99 Inuse: 991
% 34.52/34.99 Deleted: 10333
% 34.52/34.99 Deletedinuse: 363
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 198525
% 34.52/34.99 Kept: 37886
% 34.52/34.99 Inuse: 1025
% 34.52/34.99 Deleted: 10345
% 34.52/34.99 Deletedinuse: 363
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 210034
% 34.52/34.99 Kept: 39997
% 34.52/34.99 Inuse: 1055
% 34.52/34.99 Deleted: 10351
% 34.52/34.99 Deletedinuse: 365
% 34.52/34.99
% 34.52/34.99 Resimplifying clauses:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 227919
% 34.52/34.99 Kept: 42143
% 34.52/34.99 Inuse: 1092
% 34.52/34.99 Deleted: 16981
% 34.52/34.99 Deletedinuse: 374
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 243712
% 34.52/34.99 Kept: 44336
% 34.52/34.99 Inuse: 1129
% 34.52/34.99 Deleted: 16986
% 34.52/34.99 Deletedinuse: 376
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 256577
% 34.52/34.99 Kept: 46336
% 34.52/34.99 Inuse: 1158
% 34.52/34.99 Deleted: 16996
% 34.52/34.99 Deletedinuse: 383
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 275442
% 34.52/34.99 Kept: 48350
% 34.52/34.99 Inuse: 1193
% 34.52/34.99 Deleted: 16996
% 34.52/34.99 Deletedinuse: 383
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 296688
% 34.52/34.99 Kept: 52615
% 34.52/34.99 Inuse: 1222
% 34.52/34.99 Deleted: 16996
% 34.52/34.99 Deletedinuse: 383
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 301493
% 34.52/34.99 Kept: 55241
% 34.52/34.99 Inuse: 1223
% 34.52/34.99 Deleted: 17000
% 34.52/34.99 Deletedinuse: 387
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Intermediate Status:
% 34.52/34.99 Generated: 315859
% 34.52/34.99 Kept: 58658
% 34.52/34.99 Inuse: 1240
% 34.52/34.99 Deleted: 17017
% 34.52/34.99 Deletedinuse: 402
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99 Resimplifying inuse:
% 34.52/34.99 Done
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 Bliksems!, er is een bewijs:
% 34.52/34.99 % SZS status Unsatisfiable
% 34.52/34.99 % SZS output start Refutation
% 34.52/34.99
% 34.52/34.99 clause( 0, [ ~( defined( X, Y ) ), product( X, Y, compose( X, Y ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 1, [ ~( product( X, Y, Z ) ), defined( X, Y ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 5, [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined( T, X )
% 34.52/34.99 ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 8, [ ~( defined( X, Y ) ), ~( defined( Y, Z ) ), ~( 'identity_map'(
% 34.52/34.99 Y ) ), defined( X, Z ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 9, [ 'identity_map'( domain( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 10, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 11, [ defined( X, domain( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 12, [ defined( codomain( X ), X ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 13, [ product( X, domain( X ), X ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 14, [ product( codomain( X ), X, X ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 15, [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product( X, Y
% 34.52/34.99 , Y ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 16, [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product( X, Y
% 34.52/34.99 , X ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 17, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T ) ]
% 34.52/34.99 )
% 34.52/34.99 .
% 34.52/34.99 clause( 18, [ defined( b, a ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 19, [ ~( =( codomain( compose( b, a ) ), codomain( b ) ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 30, [ product( b, a, compose( b, a ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 172, [ ~( defined( X, Y ) ), defined( X, codomain( Y ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 176, [ ~( product( X, Y, Z ) ), defined( codomain( Z ), X ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 437, [ ~( defined( domain( X ), Y ) ), defined( X, Y ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 525, [ ~( 'identity_map'( X ) ), product( X, Y, Y ), ~( product( X
% 34.52/34.99 , Y, Z ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 680, [ ~( product( X, domain( X ), Y ) ), =( X, Y ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 681, [ ~( product( codomain( X ), X, Y ) ), =( X, Y ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 1233, [ defined( X, codomain( Y ) ), ~( defined( domain( X ), Y ) )
% 34.52/34.99 ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 8084, [ defined( codomain( compose( b, a ) ), b ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 8098, [ defined( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 9666, [ ~( defined( domain( X ), Y ) ), product( X, codomain( Y ),
% 34.52/34.99 X ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 9758, [ =( domain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 11374, [ =( domain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 11576, [ =( codomain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 12491, [ =( codomain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 49842, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), ~(
% 34.52/34.99 product( X, Y, T ) ), =( Y, T ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 49843, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), =( Y, Z
% 34.52/34.99 ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 49890, [ ~( product( codomain( X ), Y, Z ) ), =( Y, Z ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 56333, [ =( codomain( X ), codomain( Y ) ), ~( defined( codomain( Y
% 34.52/34.99 ), X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 59963, [ =( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 60294, [ ~( =( codomain( X ), codomain( b ) ) ), ~( defined(
% 34.52/34.99 codomain( b ), X ) ) ] )
% 34.52/34.99 .
% 34.52/34.99 clause( 60295, [] )
% 34.52/34.99 .
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 % SZS output end Refutation
% 34.52/34.99 found a proof!
% 34.52/34.99
% 34.52/34.99 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 34.52/34.99
% 34.52/34.99 initialclauses(
% 34.52/34.99 [ clause( 60297, [ ~( defined( X, Y ) ), product( X, Y, compose( X, Y ) ) ]
% 34.52/34.99 )
% 34.52/34.99 , clause( 60298, [ ~( product( X, Y, Z ) ), defined( X, Y ) ] )
% 34.52/34.99 , clause( 60299, [ ~( product( X, Y, Z ) ), ~( defined( Z, T ) ), defined(
% 34.52/34.99 Y, T ) ] )
% 34.52/34.99 , clause( 60300, [ ~( product( X, Y, Z ) ), ~( product( Y, T, U ) ), ~(
% 34.52/34.99 defined( Z, T ) ), defined( X, U ) ] )
% 34.52/34.99 , clause( 60301, [ ~( product( X, Y, Z ) ), ~( product( Z, T, U ) ), ~(
% 34.52/34.99 product( Y, T, W ) ), product( X, W, U ) ] )
% 34.52/34.99 , clause( 60302, [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined(
% 34.52/34.99 T, X ) ] )
% 34.52/34.99 , clause( 60303, [ ~( product( X, Y, Z ) ), ~( product( T, X, U ) ), ~(
% 34.52/34.99 defined( T, Z ) ), defined( U, Y ) ] )
% 34.52/34.99 , clause( 60304, [ ~( product( X, Y, Z ) ), ~( product( T, Z, U ) ), ~(
% 34.52/34.99 product( T, X, W ) ), product( W, Y, U ) ] )
% 34.52/34.99 , clause( 60305, [ ~( defined( X, Y ) ), ~( defined( Y, Z ) ), ~(
% 34.52/34.99 'identity_map'( Y ) ), defined( X, Z ) ] )
% 34.52/34.99 , clause( 60306, [ 'identity_map'( domain( X ) ) ] )
% 34.52/34.99 , clause( 60307, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 , clause( 60308, [ defined( X, domain( X ) ) ] )
% 34.52/34.99 , clause( 60309, [ defined( codomain( X ), X ) ] )
% 34.52/34.99 , clause( 60310, [ product( X, domain( X ), X ) ] )
% 34.52/34.99 , clause( 60311, [ product( codomain( X ), X, X ) ] )
% 34.52/34.99 , clause( 60312, [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product(
% 34.52/34.99 X, Y, Y ) ] )
% 34.52/34.99 , clause( 60313, [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product(
% 34.52/34.99 X, Y, X ) ] )
% 34.52/34.99 , clause( 60314, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z,
% 34.52/34.99 T ) ] )
% 34.52/34.99 , clause( 60315, [ defined( b, a ) ] )
% 34.52/34.99 , clause( 60316, [ ~( =( codomain( compose( b, a ) ), codomain( b ) ) ) ]
% 34.52/34.99 )
% 34.52/34.99 ] ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 0, [ ~( defined( X, Y ) ), product( X, Y, compose( X, Y ) ) ] )
% 34.52/34.99 , clause( 60297, [ ~( defined( X, Y ) ), product( X, Y, compose( X, Y ) ) ]
% 34.52/34.99 )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 1, [ ~( product( X, Y, Z ) ), defined( X, Y ) ] )
% 34.52/34.99 , clause( 60298, [ ~( product( X, Y, Z ) ), defined( X, Y ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 5, [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined( T, X )
% 34.52/34.99 ] )
% 34.52/34.99 , clause( 60302, [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined(
% 34.52/34.99 T, X ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 8, [ ~( defined( X, Y ) ), ~( defined( Y, Z ) ), ~( 'identity_map'(
% 34.52/34.99 Y ) ), defined( X, Z ) ] )
% 34.52/34.99 , clause( 60305, [ ~( defined( X, Y ) ), ~( defined( Y, Z ) ), ~(
% 34.52/34.99 'identity_map'( Y ) ), defined( X, Z ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 )] )
% 34.52/34.99 ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 9, [ 'identity_map'( domain( X ) ) ] )
% 34.52/34.99 , clause( 60306, [ 'identity_map'( domain( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 10, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 , clause( 60307, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 11, [ defined( X, domain( X ) ) ] )
% 34.52/34.99 , clause( 60308, [ defined( X, domain( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 12, [ defined( codomain( X ), X ) ] )
% 34.52/34.99 , clause( 60309, [ defined( codomain( X ), X ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 13, [ product( X, domain( X ), X ) ] )
% 34.52/34.99 , clause( 60310, [ product( X, domain( X ), X ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 14, [ product( codomain( X ), X, X ) ] )
% 34.52/34.99 , clause( 60311, [ product( codomain( X ), X, X ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 15, [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product( X, Y
% 34.52/34.99 , Y ) ] )
% 34.52/34.99 , clause( 60312, [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product(
% 34.52/34.99 X, Y, Y ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 16, [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product( X, Y
% 34.52/34.99 , X ) ] )
% 34.52/34.99 , clause( 60313, [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product(
% 34.52/34.99 X, Y, X ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 17, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T ) ]
% 34.52/34.99 )
% 34.52/34.99 , clause( 60314, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z,
% 34.52/34.99 T ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 18, [ defined( b, a ) ] )
% 34.52/34.99 , clause( 60315, [ defined( b, a ) ] )
% 34.52/34.99 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 19, [ ~( =( codomain( compose( b, a ) ), codomain( b ) ) ) ] )
% 34.52/34.99 , clause( 60316, [ ~( =( codomain( compose( b, a ) ), codomain( b ) ) ) ]
% 34.52/34.99 )
% 34.52/34.99 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60458, [ product( b, a, compose( b, a ) ) ] )
% 34.52/34.99 , clause( 0, [ ~( defined( X, Y ) ), product( X, Y, compose( X, Y ) ) ] )
% 34.52/34.99 , 0, clause( 18, [ defined( b, a ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, b ), :=( Y, a )] ), substitution( 1, [] )
% 34.52/34.99 ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 30, [ product( b, a, compose( b, a ) ) ] )
% 34.52/34.99 , clause( 60458, [ product( b, a, compose( b, a ) ) ] )
% 34.52/34.99 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60459, [ ~( defined( Y, X ) ), defined( Y, codomain( X ) ) ] )
% 34.52/34.99 , clause( 5, [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined( T, X
% 34.52/34.99 ) ] )
% 34.52/34.99 , 0, clause( 14, [ product( codomain( X ), X, X ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, codomain( X ) ), :=( Y, X ), :=( Z, X ),
% 34.52/34.99 :=( T, Y )] ), substitution( 1, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 172, [ ~( defined( X, Y ) ), defined( X, codomain( Y ) ) ] )
% 34.52/34.99 , clause( 60459, [ ~( defined( Y, X ) ), defined( Y, codomain( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60460, [ ~( product( X, Y, Z ) ), defined( codomain( Z ), X ) ] )
% 34.52/34.99 , clause( 5, [ ~( product( X, Y, Z ) ), ~( defined( T, Z ) ), defined( T, X
% 34.52/34.99 ) ] )
% 34.52/34.99 , 1, clause( 12, [ defined( codomain( X ), X ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, codomain(
% 34.52/34.99 Z ) )] ), substitution( 1, [ :=( X, Z )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 176, [ ~( product( X, Y, Z ) ), defined( codomain( Z ), X ) ] )
% 34.52/34.99 , clause( 60460, [ ~( product( X, Y, Z ) ), defined( codomain( Z ), X ) ]
% 34.52/34.99 )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60461, [ ~( defined( domain( X ), Y ) ), ~( 'identity_map'( domain(
% 34.52/34.99 X ) ) ), defined( X, Y ) ] )
% 34.52/34.99 , clause( 8, [ ~( defined( X, Y ) ), ~( defined( Y, Z ) ), ~(
% 34.52/34.99 'identity_map'( Y ) ), defined( X, Z ) ] )
% 34.52/34.99 , 0, clause( 11, [ defined( X, domain( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, domain( X ) ), :=( Z, Y )] ),
% 34.52/34.99 substitution( 1, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60463, [ ~( defined( domain( X ), Y ) ), defined( X, Y ) ] )
% 34.52/34.99 , clause( 60461, [ ~( defined( domain( X ), Y ) ), ~( 'identity_map'(
% 34.52/34.99 domain( X ) ) ), defined( X, Y ) ] )
% 34.52/34.99 , 1, clause( 9, [ 'identity_map'( domain( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 34.52/34.99 , X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 437, [ ~( defined( domain( X ), Y ) ), defined( X, Y ) ] )
% 34.52/34.99 , clause( 60463, [ ~( defined( domain( X ), Y ) ), defined( X, Y ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60464, [ ~( 'identity_map'( X ) ), product( X, Y, Y ), ~( product(
% 34.52/34.99 X, Y, Z ) ) ] )
% 34.52/34.99 , clause( 15, [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product( X
% 34.52/34.99 , Y, Y ) ] )
% 34.52/34.99 , 0, clause( 1, [ ~( product( X, Y, Z ) ), defined( X, Y ) ] )
% 34.52/34.99 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [ :=( X
% 34.52/34.99 , X ), :=( Y, Y ), :=( Z, Z )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 525, [ ~( 'identity_map'( X ) ), product( X, Y, Y ), ~( product( X
% 34.52/34.99 , Y, Z ) ) ] )
% 34.52/34.99 , clause( 60464, [ ~( 'identity_map'( X ) ), product( X, Y, Y ), ~( product(
% 34.52/34.99 X, Y, Z ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60465, [ ~( product( X, domain( X ), Y ) ), =( X, Y ) ] )
% 34.52/34.99 , clause( 17, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T )
% 34.52/34.99 ] )
% 34.52/34.99 , 0, clause( 13, [ product( X, domain( X ), X ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, domain( X ) ), :=( Z, X ), :=( T
% 34.52/34.99 , Y )] ), substitution( 1, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 680, [ ~( product( X, domain( X ), Y ) ), =( X, Y ) ] )
% 34.52/34.99 , clause( 60465, [ ~( product( X, domain( X ), Y ) ), =( X, Y ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60467, [ ~( product( codomain( X ), X, Y ) ), =( X, Y ) ] )
% 34.52/34.99 , clause( 17, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T )
% 34.52/34.99 ] )
% 34.52/34.99 , 0, clause( 14, [ product( codomain( X ), X, X ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, codomain( X ) ), :=( Y, X ), :=( Z, X ),
% 34.52/34.99 :=( T, Y )] ), substitution( 1, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 681, [ ~( product( codomain( X ), X, Y ) ), =( X, Y ) ] )
% 34.52/34.99 , clause( 60467, [ ~( product( codomain( X ), X, Y ) ), =( X, Y ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60469, [ defined( X, codomain( Y ) ), ~( defined( domain( X ), Y )
% 34.52/34.99 ) ] )
% 34.52/34.99 , clause( 437, [ ~( defined( domain( X ), Y ) ), defined( X, Y ) ] )
% 34.52/34.99 , 0, clause( 172, [ ~( defined( X, Y ) ), defined( X, codomain( Y ) ) ] )
% 34.52/34.99 , 1, substitution( 0, [ :=( X, X ), :=( Y, codomain( Y ) )] ),
% 34.52/34.99 substitution( 1, [ :=( X, domain( X ) ), :=( Y, Y )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 1233, [ defined( X, codomain( Y ) ), ~( defined( domain( X ), Y ) )
% 34.52/34.99 ] )
% 34.52/34.99 , clause( 60469, [ defined( X, codomain( Y ) ), ~( defined( domain( X ), Y
% 34.52/34.99 ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 34.52/34.99 ), ==>( 1, 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60470, [ defined( codomain( compose( b, a ) ), b ) ] )
% 34.52/34.99 , clause( 176, [ ~( product( X, Y, Z ) ), defined( codomain( Z ), X ) ] )
% 34.52/34.99 , 0, clause( 30, [ product( b, a, compose( b, a ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, b ), :=( Y, a ), :=( Z, compose( b, a ) )] )
% 34.52/34.99 , substitution( 1, [] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 8084, [ defined( codomain( compose( b, a ) ), b ) ] )
% 34.52/34.99 , clause( 60470, [ defined( codomain( compose( b, a ) ), b ) ] )
% 34.52/34.99 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60471, [ defined( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 34.52/34.99 , clause( 172, [ ~( defined( X, Y ) ), defined( X, codomain( Y ) ) ] )
% 34.52/34.99 , 0, clause( 8084, [ defined( codomain( compose( b, a ) ), b ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, codomain( compose( b, a ) ) ), :=( Y, b )] )
% 34.52/34.99 , substitution( 1, [] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 8098, [ defined( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 34.52/34.99 , clause( 60471, [ defined( codomain( compose( b, a ) ), codomain( b ) ) ]
% 34.52/34.99 )
% 34.52/34.99 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60472, [ ~( 'identity_map'( codomain( Y ) ) ), product( X, codomain(
% 34.52/34.99 Y ), X ), ~( defined( domain( X ), Y ) ) ] )
% 34.52/34.99 , clause( 16, [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product( X
% 34.52/34.99 , Y, X ) ] )
% 34.52/34.99 , 0, clause( 1233, [ defined( X, codomain( Y ) ), ~( defined( domain( X ),
% 34.52/34.99 Y ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X ), :=( Y, codomain( Y ) )] ),
% 34.52/34.99 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60473, [ product( Y, codomain( X ), Y ), ~( defined( domain( Y ), X
% 34.52/34.99 ) ) ] )
% 34.52/34.99 , clause( 60472, [ ~( 'identity_map'( codomain( Y ) ) ), product( X,
% 34.52/34.99 codomain( Y ), X ), ~( defined( domain( X ), Y ) ) ] )
% 34.52/34.99 , 0, clause( 10, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [ :=( X
% 34.52/34.99 , X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 9666, [ ~( defined( domain( X ), Y ) ), product( X, codomain( Y ),
% 34.52/34.99 X ) ] )
% 34.52/34.99 , clause( 60473, [ product( Y, codomain( X ), Y ), ~( defined( domain( Y )
% 34.52/34.99 , X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 34.52/34.99 ), ==>( 1, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 eqswap(
% 34.52/34.99 clause( 60474, [ =( Y, X ), ~( product( X, domain( X ), Y ) ) ] )
% 34.52/34.99 , clause( 680, [ ~( product( X, domain( X ), Y ) ), =( X, Y ) ] )
% 34.52/34.99 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60475, [ =( domain( X ), X ), ~( defined( X, domain( X ) ) ), ~(
% 34.52/34.99 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 60474, [ =( Y, X ), ~( product( X, domain( X ), Y ) ) ] )
% 34.52/34.99 , 1, clause( 15, [ ~( defined( X, Y ) ), ~( 'identity_map'( X ) ), product(
% 34.52/34.99 X, Y, Y ) ] )
% 34.52/34.99 , 2, substitution( 0, [ :=( X, X ), :=( Y, domain( X ) )] ), substitution(
% 34.52/34.99 1, [ :=( X, X ), :=( Y, domain( X ) )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60476, [ =( domain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 60475, [ =( domain( X ), X ), ~( defined( X, domain( X ) ) ), ~(
% 34.52/34.99 'identity_map'( X ) ) ] )
% 34.52/34.99 , 1, clause( 11, [ defined( X, domain( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 34.52/34.99 ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 9758, [ =( domain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 60476, [ =( domain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 34.52/34.99 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 eqswap(
% 34.52/34.99 clause( 60478, [ =( X, domain( X ) ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 9758, [ =( domain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60479, [ =( codomain( X ), domain( codomain( X ) ) ) ] )
% 34.52/34.99 , clause( 60478, [ =( X, domain( X ) ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , 1, clause( 10, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, codomain( X ) )] ), substitution( 1, [ :=( X
% 34.52/34.99 , X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 eqswap(
% 34.52/34.99 clause( 60480, [ =( domain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 , clause( 60479, [ =( codomain( X ), domain( codomain( X ) ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 11374, [ =( domain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 , clause( 60480, [ =( domain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 eqswap(
% 34.52/34.99 clause( 60481, [ =( Y, X ), ~( product( codomain( X ), X, Y ) ) ] )
% 34.52/34.99 , clause( 681, [ ~( product( codomain( X ), X, Y ) ), =( X, Y ) ] )
% 34.52/34.99 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60482, [ =( codomain( X ), X ), ~( defined( codomain( X ), X ) ),
% 34.52/34.99 ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 60481, [ =( Y, X ), ~( product( codomain( X ), X, Y ) ) ] )
% 34.52/34.99 , 1, clause( 16, [ ~( defined( X, Y ) ), ~( 'identity_map'( Y ) ), product(
% 34.52/34.99 X, Y, X ) ] )
% 34.52/34.99 , 2, substitution( 0, [ :=( X, X ), :=( Y, codomain( X ) )] ),
% 34.52/34.99 substitution( 1, [ :=( X, codomain( X ) ), :=( Y, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60483, [ =( codomain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 60482, [ =( codomain( X ), X ), ~( defined( codomain( X ), X ) )
% 34.52/34.99 , ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , 1, clause( 12, [ defined( codomain( X ), X ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 34.52/34.99 ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 11576, [ =( codomain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 60483, [ =( codomain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 34.52/34.99 1 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 eqswap(
% 34.52/34.99 clause( 60485, [ =( X, codomain( X ) ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , clause( 11576, [ =( codomain( X ), X ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60486, [ =( codomain( X ), codomain( codomain( X ) ) ) ] )
% 34.52/34.99 , clause( 60485, [ =( X, codomain( X ) ), ~( 'identity_map'( X ) ) ] )
% 34.52/34.99 , 1, clause( 10, [ 'identity_map'( codomain( X ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, codomain( X ) )] ), substitution( 1, [ :=( X
% 34.52/34.99 , X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 eqswap(
% 34.52/34.99 clause( 60487, [ =( codomain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 , clause( 60486, [ =( codomain( X ), codomain( codomain( X ) ) ) ] )
% 34.52/34.99 , 0, substitution( 0, [ :=( X, X )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 12491, [ =( codomain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 , clause( 60487, [ =( codomain( codomain( X ) ), codomain( X ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 resolution(
% 34.52/34.99 clause( 60488, [ ~( product( X, Y, Z ) ), =( Y, Z ), ~( 'identity_map'( X )
% 34.52/34.99 ), ~( product( X, Y, T ) ) ] )
% 34.52/34.99 , clause( 17, [ ~( product( X, Y, Z ) ), ~( product( X, Y, T ) ), =( Z, T )
% 34.52/34.99 ] )
% 34.52/34.99 , 0, clause( 525, [ ~( 'identity_map'( X ) ), product( X, Y, Y ), ~(
% 34.52/34.99 product( X, Y, Z ) ) ] )
% 34.52/34.99 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Y ), :=( T, Z )] ),
% 34.52/34.99 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, T )] )).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 49842, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), ~(
% 34.52/34.99 product( X, Y, T ) ), =( Y, T ) ] )
% 34.52/34.99 , clause( 60488, [ ~( product( X, Y, Z ) ), =( Y, Z ), ~( 'identity_map'( X
% 34.52/34.99 ) ), ~( product( X, Y, T ) ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, T ), :=( T, Z )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 2 ), ==>( 1, 3 ), ==>( 2, 0 ), ==>( 3, 1 )] )
% 34.52/34.99 ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 factor(
% 34.52/34.99 clause( 60493, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), =( Y, Z
% 34.52/34.99 ) ] )
% 34.52/34.99 , clause( 49842, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), ~(
% 34.52/34.99 product( X, Y, T ) ), =( Y, T ) ] )
% 34.52/34.99 , 1, 2, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, Z )] )
% 34.52/34.99 ).
% 34.52/34.99
% 34.52/34.99
% 34.52/34.99 subsumption(
% 34.52/34.99 clause( 49843, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), =( Y, Z
% 34.52/34.99 ) ] )
% 34.52/34.99 , clause( 60493, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), =( Y
% 34.52/34.99 , Z ) ] )
% 34.52/34.99 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 34.52/34.99 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60495, [ =( Y, X ), ~( 'identity_map'( Z ) ), ~( product( Z, X, Y )
% 37.90/38.32 ) ] )
% 37.90/38.32 , clause( 49843, [ ~( 'identity_map'( X ) ), ~( product( X, Y, Z ) ), =( Y
% 37.90/38.32 , Z ) ] )
% 37.90/38.32 , 2, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 resolution(
% 37.90/38.32 clause( 60496, [ =( X, Y ), ~( product( codomain( Z ), Y, X ) ) ] )
% 37.90/38.32 , clause( 60495, [ =( Y, X ), ~( 'identity_map'( Z ) ), ~( product( Z, X, Y
% 37.90/38.32 ) ) ] )
% 37.90/38.32 , 1, clause( 10, [ 'identity_map'( codomain( X ) ) ] )
% 37.90/38.32 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X ), :=( Z, codomain( Z ) )] ),
% 37.90/38.32 substitution( 1, [ :=( X, Z )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60497, [ =( Y, X ), ~( product( codomain( Z ), Y, X ) ) ] )
% 37.90/38.32 , clause( 60496, [ =( X, Y ), ~( product( codomain( Z ), Y, X ) ) ] )
% 37.90/38.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 subsumption(
% 37.90/38.32 clause( 49890, [ ~( product( codomain( X ), Y, Z ) ), =( Y, Z ) ] )
% 37.90/38.32 , clause( 60497, [ =( Y, X ), ~( product( codomain( Z ), Y, X ) ) ] )
% 37.90/38.32 , substitution( 0, [ :=( X, Z ), :=( Y, Y ), :=( Z, X )] ),
% 37.90/38.32 permutation( 0, [ ==>( 0, 1 ), ==>( 1, 0 )] ) ).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60498, [ =( Y, X ), ~( product( codomain( Z ), X, Y ) ) ] )
% 37.90/38.32 , clause( 49890, [ ~( product( codomain( X ), Y, Z ) ), =( Y, Z ) ] )
% 37.90/38.32 , 1, substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 resolution(
% 37.90/38.32 clause( 60500, [ =( codomain( X ), codomain( Y ) ), ~( defined( domain(
% 37.90/38.32 codomain( X ) ), Y ) ) ] )
% 37.90/38.32 , clause( 60498, [ =( Y, X ), ~( product( codomain( Z ), X, Y ) ) ] )
% 37.90/38.32 , 1, clause( 9666, [ ~( defined( domain( X ), Y ) ), product( X, codomain(
% 37.90/38.32 Y ), X ) ] )
% 37.90/38.32 , 1, substitution( 0, [ :=( X, codomain( Y ) ), :=( Y, codomain( X ) ),
% 37.90/38.32 :=( Z, X )] ), substitution( 1, [ :=( X, codomain( X ) ), :=( Y, Y )] )
% 37.90/38.32 ).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 paramod(
% 37.90/38.32 clause( 60501, [ ~( defined( codomain( X ), Y ) ), =( codomain( X ),
% 37.90/38.32 codomain( Y ) ) ] )
% 37.90/38.32 , clause( 11374, [ =( domain( codomain( X ) ), codomain( X ) ) ] )
% 37.90/38.32 , 0, clause( 60500, [ =( codomain( X ), codomain( Y ) ), ~( defined( domain(
% 37.90/38.32 codomain( X ) ), Y ) ) ] )
% 37.90/38.32 , 1, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 37.90/38.32 :=( Y, Y )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60502, [ =( codomain( Y ), codomain( X ) ), ~( defined( codomain( X
% 37.90/38.32 ), Y ) ) ] )
% 37.90/38.32 , clause( 60501, [ ~( defined( codomain( X ), Y ) ), =( codomain( X ),
% 37.90/38.32 codomain( Y ) ) ] )
% 37.90/38.32 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 subsumption(
% 37.90/38.32 clause( 56333, [ =( codomain( X ), codomain( Y ) ), ~( defined( codomain( Y
% 37.90/38.32 ), X ) ) ] )
% 37.90/38.32 , clause( 60502, [ =( codomain( Y ), codomain( X ) ), ~( defined( codomain(
% 37.90/38.32 X ), Y ) ) ] )
% 37.90/38.32 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 37.90/38.32 ), ==>( 1, 1 )] ) ).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60503, [ =( codomain( Y ), codomain( X ) ), ~( defined( codomain( Y
% 37.90/38.32 ), X ) ) ] )
% 37.90/38.32 , clause( 56333, [ =( codomain( X ), codomain( Y ) ), ~( defined( codomain(
% 37.90/38.32 Y ), X ) ) ] )
% 37.90/38.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 resolution(
% 37.90/38.32 clause( 60505, [ =( codomain( compose( b, a ) ), codomain( codomain( b ) )
% 37.90/38.32 ) ] )
% 37.90/38.32 , clause( 60503, [ =( codomain( Y ), codomain( X ) ), ~( defined( codomain(
% 37.90/38.32 Y ), X ) ) ] )
% 37.90/38.32 , 1, clause( 8098, [ defined( codomain( compose( b, a ) ), codomain( b ) )
% 37.90/38.32 ] )
% 37.90/38.32 , 0, substitution( 0, [ :=( X, codomain( b ) ), :=( Y, compose( b, a ) )] )
% 37.90/38.32 , substitution( 1, [] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 paramod(
% 37.90/38.32 clause( 60506, [ =( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 37.90/38.32 , clause( 12491, [ =( codomain( codomain( X ) ), codomain( X ) ) ] )
% 37.90/38.32 , 0, clause( 60505, [ =( codomain( compose( b, a ) ), codomain( codomain( b
% 37.90/38.32 ) ) ) ] )
% 37.90/38.32 , 0, 5, substitution( 0, [ :=( X, b )] ), substitution( 1, [] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 subsumption(
% 37.90/38.32 clause( 59963, [ =( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 37.90/38.32 , clause( 60506, [ =( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 37.90/38.32 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60508, [ =( codomain( Y ), codomain( X ) ), ~( defined( codomain( Y
% 37.90/38.32 ), X ) ) ] )
% 37.90/38.32 , clause( 56333, [ =( codomain( X ), codomain( Y ) ), ~( defined( codomain(
% 37.90/38.32 Y ), X ) ) ] )
% 37.90/38.32 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 37.90/38.32
% 37.90/38.32
% 37.90/38.32 eqswap(
% 37.90/38.32 clause( 60509, [ ~( =( codomain( b ), codomain( compose( b, a ) ) ) ) ] )
% 37.90/38.33 , clause( 19, [ ~( =( codomain( compose( b, a ) ), codomain( b ) ) ) ] )
% 37.90/38.33 , 0, substitution( 0, [] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 paramod(
% 37.90/38.33 clause( 60512, [ ~( =( codomain( b ), codomain( X ) ) ), ~( defined(
% 37.90/38.33 codomain( compose( b, a ) ), X ) ) ] )
% 37.90/38.33 , clause( 60508, [ =( codomain( Y ), codomain( X ) ), ~( defined( codomain(
% 37.90/38.33 Y ), X ) ) ] )
% 37.90/38.33 , 0, clause( 60509, [ ~( =( codomain( b ), codomain( compose( b, a ) ) ) )
% 37.90/38.33 ] )
% 37.90/38.33 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, compose( b, a ) )] ),
% 37.90/38.33 substitution( 1, [] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 paramod(
% 37.90/38.33 clause( 62524, [ ~( defined( codomain( b ), X ) ), ~( =( codomain( b ),
% 37.90/38.33 codomain( X ) ) ) ] )
% 37.90/38.33 , clause( 59963, [ =( codomain( compose( b, a ) ), codomain( b ) ) ] )
% 37.90/38.33 , 0, clause( 60512, [ ~( =( codomain( b ), codomain( X ) ) ), ~( defined(
% 37.90/38.33 codomain( compose( b, a ) ), X ) ) ] )
% 37.90/38.33 , 1, 2, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 eqswap(
% 37.90/38.33 clause( 62525, [ ~( =( codomain( X ), codomain( b ) ) ), ~( defined(
% 37.90/38.33 codomain( b ), X ) ) ] )
% 37.90/38.33 , clause( 62524, [ ~( defined( codomain( b ), X ) ), ~( =( codomain( b ),
% 37.90/38.33 codomain( X ) ) ) ] )
% 37.90/38.33 , 1, substitution( 0, [ :=( X, X )] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 subsumption(
% 37.90/38.33 clause( 60294, [ ~( =( codomain( X ), codomain( b ) ) ), ~( defined(
% 37.90/38.33 codomain( b ), X ) ) ] )
% 37.90/38.33 , clause( 62525, [ ~( =( codomain( X ), codomain( b ) ) ), ~( defined(
% 37.90/38.33 codomain( b ), X ) ) ] )
% 37.90/38.33 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 37.90/38.33 1 )] ) ).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 eqswap(
% 37.90/38.33 clause( 62526, [ ~( =( codomain( b ), codomain( X ) ) ), ~( defined(
% 37.90/38.33 codomain( b ), X ) ) ] )
% 37.90/38.33 , clause( 60294, [ ~( =( codomain( X ), codomain( b ) ) ), ~( defined(
% 37.90/38.33 codomain( b ), X ) ) ] )
% 37.90/38.33 , 0, substitution( 0, [ :=( X, X )] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 eqrefl(
% 37.90/38.33 clause( 62527, [ ~( defined( codomain( b ), b ) ) ] )
% 37.90/38.33 , clause( 62526, [ ~( =( codomain( b ), codomain( X ) ) ), ~( defined(
% 37.90/38.33 codomain( b ), X ) ) ] )
% 37.90/38.33 , 0, substitution( 0, [ :=( X, b )] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 resolution(
% 37.90/38.33 clause( 62528, [] )
% 37.90/38.33 , clause( 62527, [ ~( defined( codomain( b ), b ) ) ] )
% 37.90/38.33 , 0, clause( 12, [ defined( codomain( X ), X ) ] )
% 37.90/38.33 , 0, substitution( 0, [] ), substitution( 1, [ :=( X, b )] )).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 subsumption(
% 37.90/38.33 clause( 60295, [] )
% 37.90/38.33 , clause( 62528, [] )
% 37.90/38.33 , substitution( 0, [] ), permutation( 0, [] ) ).
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 end.
% 37.90/38.33
% 37.90/38.33 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 37.90/38.33
% 37.90/38.33 Memory use:
% 37.90/38.33
% 37.90/38.33 space for terms: 902424
% 37.90/38.33 space for clauses: 2366862
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 clauses generated: 332835
% 37.90/38.33 clauses kept: 60296
% 37.90/38.33 clauses selected: 1266
% 37.90/38.33 clauses deleted: 17022
% 37.90/38.33 clauses inuse deleted: 403
% 37.90/38.33
% 37.90/38.33 subsentry: 19300721
% 37.90/38.33 literals s-matched: 8277465
% 37.90/38.33 literals matched: 6181852
% 37.90/38.33 full subsumption: 4209201
% 37.90/38.33
% 37.90/38.33 checksum: 302223572
% 37.90/38.33
% 37.90/38.33
% 37.90/38.33 Bliksem ended
%------------------------------------------------------------------------------