%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CAT003-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n028.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:08 EDT 2022
% Result : Unsatisfiable 219.64s 220.09s
% Output : Refutation 219.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CAT003-2 : TPTP v8.1.0. Released v1.0.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n028.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 : Sun May 29 17:25:03 EDT 2022
% 0.12/0.33 % CPUTime :
% 219.64/220.09 *** allocated 10000 integers for termspace/termends
% 219.64/220.09 *** allocated 10000 integers for clauses
% 219.64/220.09 *** allocated 10000 integers for justifications
% 219.64/220.09 Bliksem 1.12
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Automatic Strategy Selection
% 219.64/220.09
% 219.64/220.09 Clauses:
% 219.64/220.09 [
% 219.64/220.09 [ =( codomain( domain( X ) ), domain( X ) ) ],
% 219.64/220.09 [ =( domain( codomain( X ) ), codomain( X ) ) ],
% 219.64/220.09 [ =( compose( domain( X ), X ), X ) ],
% 219.64/220.09 [ =( compose( X, codomain( X ) ), X ) ],
% 219.64/220.09 [ ~( =( codomain( X ), domain( Y ) ) ), =( domain( compose( X, Y ) ),
% 219.64/220.09 domain( X ) ) ],
% 219.64/220.09 [ ~( =( codomain( X ), domain( Y ) ) ), =( codomain( compose( X, Y ) ),
% 219.64/220.09 codomain( Y ) ) ],
% 219.64/220.09 [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ), domain( Z )
% 219.64/220.09 ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y ), Z ) ) ]
% 219.64/220.09 ,
% 219.64/220.09 [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~( =( compose(
% 219.64/220.09 compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b ) ), domain( Z
% 219.64/220.09 ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z ) ],
% 219.64/220.09 [ =( codomain( a ), domain( b ) ) ],
% 219.64/220.09 [ =( codomain( b ), domain( h ) ) ],
% 219.64/220.09 [ =( codomain( b ), domain( g ) ) ],
% 219.64/220.09 [ =( compose( b, h ), compose( b, g ) ) ],
% 219.64/220.09 [ ~( =( g, h ) ) ]
% 219.64/220.09 ] .
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 percentage equality = 1.000000, percentage horn = 1.000000
% 219.64/220.09 This is a pure equality problem
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Options Used:
% 219.64/220.09
% 219.64/220.09 useres = 1
% 219.64/220.09 useparamod = 1
% 219.64/220.09 useeqrefl = 1
% 219.64/220.09 useeqfact = 1
% 219.64/220.09 usefactor = 1
% 219.64/220.09 usesimpsplitting = 0
% 219.64/220.09 usesimpdemod = 5
% 219.64/220.09 usesimpres = 3
% 219.64/220.09
% 219.64/220.09 resimpinuse = 1000
% 219.64/220.09 resimpclauses = 20000
% 219.64/220.09 substype = eqrewr
% 219.64/220.09 backwardsubs = 1
% 219.64/220.09 selectoldest = 5
% 219.64/220.09
% 219.64/220.09 litorderings [0] = split
% 219.64/220.09 litorderings [1] = extend the termordering, first sorting on arguments
% 219.64/220.09
% 219.64/220.09 termordering = kbo
% 219.64/220.09
% 219.64/220.09 litapriori = 0
% 219.64/220.09 termapriori = 1
% 219.64/220.09 litaposteriori = 0
% 219.64/220.09 termaposteriori = 0
% 219.64/220.09 demodaposteriori = 0
% 219.64/220.09 ordereqreflfact = 0
% 219.64/220.09
% 219.64/220.09 litselect = negord
% 219.64/220.09
% 219.64/220.09 maxweight = 15
% 219.64/220.09 maxdepth = 30000
% 219.64/220.09 maxlength = 115
% 219.64/220.09 maxnrvars = 195
% 219.64/220.09 excuselevel = 1
% 219.64/220.09 increasemaxweight = 1
% 219.64/220.09
% 219.64/220.09 maxselected = 10000000
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09
% 219.64/220.09 showgenerated = 0
% 219.64/220.09 showkept = 0
% 219.64/220.09 showselected = 0
% 219.64/220.09 showdeleted = 0
% 219.64/220.09 showresimp = 1
% 219.64/220.09 showstatus = 2000
% 219.64/220.09
% 219.64/220.09 prologoutput = 1
% 219.64/220.09 nrgoals = 5000000
% 219.64/220.09 totalproof = 1
% 219.64/220.09
% 219.64/220.09 Symbols occurring in the translation:
% 219.64/220.09
% 219.64/220.09 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 219.64/220.09 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 219.64/220.09 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 219.64/220.09 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 219.64/220.09 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 219.64/220.09 domain [40, 1] (w:1, o:22, a:1, s:1, b:0),
% 219.64/220.09 codomain [41, 1] (w:1, o:21, a:1, s:1, b:0),
% 219.64/220.09 compose [42, 2] (w:1, o:48, a:1, s:1, b:0),
% 219.64/220.09 a [45, 0] (w:1, o:12, a:1, s:1, b:0),
% 219.64/220.09 b [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 219.64/220.09 h [47, 0] (w:1, o:15, a:1, s:1, b:0),
% 219.64/220.09 g [48, 0] (w:1, o:14, a:1, s:1, b:0).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 15
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 19683
% 219.64/220.09 Kept: 200
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 16
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 16
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 27289
% 219.64/220.09 Kept: 262
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 17
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 17
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 48554
% 219.64/220.09 Kept: 327
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 18
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 18
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 54006
% 219.64/220.09 Kept: 388
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 19
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 19
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 134042
% 219.64/220.09 Kept: 651
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 20
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 20
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 1048848
% 219.64/220.09 Kept: 1653
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 21
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 117891
% 219.64/220.09 Kept: 2000
% 219.64/220.09 Inuse: 493
% 219.64/220.09 Deleted: 106
% 219.64/220.09 Deletedinuse: 0
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 21
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 3574746
% 219.64/220.09 Kept: 3159
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 22
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 21315
% 219.64/220.09 Kept: 2035
% 219.64/220.09 Inuse: 203
% 219.64/220.09 Deleted: 26
% 219.64/220.09 Deletedinuse: 0
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 396778
% 219.64/220.09 Kept: 4036
% 219.64/220.09 Inuse: 939
% 219.64/220.09 Deleted: 139
% 219.64/220.09 Deletedinuse: 3
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 8316433
% 219.64/220.09 Kept: 6041
% 219.64/220.09 Inuse: 4266
% 219.64/220.09 Deleted: 486
% 219.64/220.09 Deletedinuse: 120
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 22
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 16244260
% 219.64/220.09 Kept: 6890
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 23
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 17082
% 219.64/220.09 Kept: 2011
% 219.64/220.09 Inuse: 173
% 219.64/220.09 Deleted: 25
% 219.64/220.09 Deletedinuse: 0
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 69665
% 219.64/220.09 Kept: 4012
% 219.64/220.09 Inuse: 396
% 219.64/220.09 Deleted: 133
% 219.64/220.09 Deletedinuse: 0
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 1339172
% 219.64/220.09 Kept: 6015
% 219.64/220.09 Inuse: 1808
% 219.64/220.09 Deleted: 279
% 219.64/220.09 Deletedinuse: 4
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 13087704
% 219.64/220.09 Kept: 8018
% 219.64/220.09 Inuse: 5476
% 219.64/220.09 Deleted: 1038
% 219.64/220.09 Deletedinuse: 208
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09 Failed to find proof!
% 219.64/220.09 maxweight = 23
% 219.64/220.09 maxnrclauses = 10000000
% 219.64/220.09 Generated: 19441004
% 219.64/220.09 Kept: 8219
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 The strategy used was not complete!
% 219.64/220.09
% 219.64/220.09 Increased maxweight to 24
% 219.64/220.09
% 219.64/220.09 Starting Search:
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Intermediate Status:
% 219.64/220.09 Generated: 12701
% 219.64/220.09 Kept: 2004
% 219.64/220.09 Inuse: 140
% 219.64/220.09 Deleted: 19
% 219.64/220.09 Deletedinuse: 0
% 219.64/220.09
% 219.64/220.09 Resimplifying inuse:
% 219.64/220.09 Done
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 Bliksems!, er is een bewijs:
% 219.64/220.09 % SZS status Unsatisfiable
% 219.64/220.09 % SZS output start Refutation
% 219.64/220.09
% 219.64/220.09 clause( 5, [ ~( =( codomain( X ), domain( Y ) ) ), =( codomain( compose( X
% 219.64/220.09 , Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 6, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y
% 219.64/220.09 ), Z ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 7, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~( =(
% 219.64/220.09 compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b ) ),
% 219.64/220.09 domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z ) ]
% 219.64/220.09 )
% 219.64/220.09 .
% 219.64/220.09 clause( 8, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 9, [ =( domain( h ), codomain( b ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 10, [ =( domain( g ), codomain( b ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 11, [ =( compose( b, h ), compose( b, g ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 12, [ ~( =( h, g ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 14, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~( =(
% 219.64/220.09 codomain( compose( a, b ) ), domain( Y ) ) ), ~( =( compose( compose( a,
% 219.64/220.09 b ), Y ), compose( compose( a, b ), X ) ) ), =( X, Y ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 42, [ ~( =( codomain( X ), codomain( a ) ) ), =( codomain( compose(
% 219.64/220.09 X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 47, [ =( codomain( compose( a, b ) ), codomain( b ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 53, [ =( compose( X, compose( b, g ) ), compose( compose( X, b ), h
% 219.64/220.09 ) ), ~( =( codomain( X ), codomain( a ) ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 72, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 codomain( b ) ) ), =( compose( X, compose( Y, g ) ), compose( compose( X
% 219.64/220.09 , Y ), g ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 73, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( compose(
% 219.64/220.09 X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 74, [ =( compose( compose( a, b ), h ), compose( compose( a, b ), g
% 219.64/220.09 ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 113, [ ~( =( compose( compose( a, b ), Y ), compose( compose( a, b
% 219.64/220.09 ), X ) ) ), =( X, Y ), ~( =( codomain( b ), domain( X ) ) ), ~( =(
% 219.64/220.09 codomain( b ), domain( Y ) ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 2999, [ ~( =( X, g ) ), ~( =( codomain( b ), domain( X ) ) ), ~(
% 219.64/220.09 =( compose( compose( a, b ), X ), compose( compose( a, b ), g ) ) ) ] )
% 219.64/220.09 .
% 219.64/220.09 clause( 3000, [] )
% 219.64/220.09 .
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 % SZS output end Refutation
% 219.64/220.09 found a proof!
% 219.64/220.09
% 219.64/220.09 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 219.64/220.09
% 219.64/220.09 initialclauses(
% 219.64/220.09 [ clause( 3002, [ =( codomain( domain( X ) ), domain( X ) ) ] )
% 219.64/220.09 , clause( 3003, [ =( domain( codomain( X ) ), codomain( X ) ) ] )
% 219.64/220.09 , clause( 3004, [ =( compose( domain( X ), X ), X ) ] )
% 219.64/220.09 , clause( 3005, [ =( compose( X, codomain( X ) ), X ) ] )
% 219.64/220.09 , clause( 3006, [ ~( =( codomain( X ), domain( Y ) ) ), =( domain( compose(
% 219.64/220.09 X, Y ) ), domain( X ) ) ] )
% 219.64/220.09 , clause( 3007, [ ~( =( codomain( X ), domain( Y ) ) ), =( codomain(
% 219.64/220.09 compose( X, Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 , clause( 3008, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y )
% 219.64/220.09 , domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X
% 219.64/220.09 , Y ), Z ) ) ] )
% 219.64/220.09 , clause( 3009, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~(
% 219.64/220.09 =( compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b )
% 219.64/220.09 ), domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z
% 219.64/220.09 ) ] )
% 219.64/220.09 , clause( 3010, [ =( codomain( a ), domain( b ) ) ] )
% 219.64/220.09 , clause( 3011, [ =( codomain( b ), domain( h ) ) ] )
% 219.64/220.09 , clause( 3012, [ =( codomain( b ), domain( g ) ) ] )
% 219.64/220.09 , clause( 3013, [ =( compose( b, h ), compose( b, g ) ) ] )
% 219.64/220.09 , clause( 3014, [ ~( =( g, h ) ) ] )
% 219.64/220.09 ] ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 5, [ ~( =( codomain( X ), domain( Y ) ) ), =( codomain( compose( X
% 219.64/220.09 , Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 , clause( 3007, [ ~( =( codomain( X ), domain( Y ) ) ), =( codomain(
% 219.64/220.09 compose( X, Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 219.64/220.09 ), ==>( 1, 1 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 6, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y
% 219.64/220.09 ), Z ) ) ] )
% 219.64/220.09 , clause( 3008, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y )
% 219.64/220.09 , domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X
% 219.64/220.09 , Y ), Z ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 219.64/220.09 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 7, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~( =(
% 219.64/220.09 compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b ) ),
% 219.64/220.09 domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z ) ]
% 219.64/220.09 )
% 219.64/220.09 , clause( 3009, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~(
% 219.64/220.09 =( compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b )
% 219.64/220.09 ), domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z
% 219.64/220.09 ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 219.64/220.09 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 ),
% 219.64/220.09 ==>( 4, 4 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3136, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 , clause( 3010, [ =( codomain( a ), domain( b ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 8, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 , clause( 3136, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3183, [ =( domain( h ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3011, [ =( codomain( b ), domain( h ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 9, [ =( domain( h ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3183, [ =( domain( h ), codomain( b ) ) ] )
% 219.64/220.09 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3231, [ =( domain( g ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3012, [ =( codomain( b ), domain( g ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 10, [ =( domain( g ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3231, [ =( domain( g ), codomain( b ) ) ] )
% 219.64/220.09 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 11, [ =( compose( b, h ), compose( b, g ) ) ] )
% 219.64/220.09 , clause( 3013, [ =( compose( b, h ), compose( b, g ) ) ] )
% 219.64/220.09 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3330, [ ~( =( h, g ) ) ] )
% 219.64/220.09 , clause( 3014, [ ~( =( g, h ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 12, [ ~( =( h, g ) ) ] )
% 219.64/220.09 , clause( 3330, [ ~( =( h, g ) ) ] )
% 219.64/220.09 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3331, [ ~( =( domain( X ), codomain( compose( a, b ) ) ) ), ~( =(
% 219.64/220.09 compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b ) ),
% 219.64/220.09 domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z ) ]
% 219.64/220.09 )
% 219.64/220.09 , clause( 7, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~( =(
% 219.64/220.09 compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b ) ),
% 219.64/220.09 domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z ) ]
% 219.64/220.09 )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqrefl(
% 219.64/220.09 clause( 3347, [ ~( =( domain( X ), codomain( compose( a, b ) ) ) ), ~( =(
% 219.64/220.09 compose( compose( a, b ), X ), compose( compose( a, b ), Y ) ) ), ~( =(
% 219.64/220.09 codomain( compose( a, b ) ), domain( Y ) ) ), =( X, Y ) ] )
% 219.64/220.09 , clause( 3331, [ ~( =( domain( X ), codomain( compose( a, b ) ) ) ), ~(
% 219.64/220.09 =( compose( compose( a, b ), X ), Y ) ), ~( =( codomain( compose( a, b )
% 219.64/220.09 ), domain( Z ) ) ), ~( =( compose( compose( a, b ), Z ), Y ) ), =( X, Z
% 219.64/220.09 ) ] )
% 219.64/220.09 , 3, substitution( 0, [ :=( X, X ), :=( Y, compose( compose( a, b ), Y ) )
% 219.64/220.09 , :=( Z, Y )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3350, [ =( Y, X ), ~( =( domain( X ), codomain( compose( a, b ) ) )
% 219.64/220.09 ), ~( =( compose( compose( a, b ), X ), compose( compose( a, b ), Y ) )
% 219.64/220.09 ), ~( =( codomain( compose( a, b ) ), domain( Y ) ) ) ] )
% 219.64/220.09 , clause( 3347, [ ~( =( domain( X ), codomain( compose( a, b ) ) ) ), ~(
% 219.64/220.09 =( compose( compose( a, b ), X ), compose( compose( a, b ), Y ) ) ), ~(
% 219.64/220.09 =( codomain( compose( a, b ) ), domain( Y ) ) ), =( X, Y ) ] )
% 219.64/220.09 , 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3351, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), =( Y, X
% 219.64/220.09 ), ~( =( compose( compose( a, b ), X ), compose( compose( a, b ), Y ) )
% 219.64/220.09 ), ~( =( codomain( compose( a, b ) ), domain( Y ) ) ) ] )
% 219.64/220.09 , clause( 3350, [ =( Y, X ), ~( =( domain( X ), codomain( compose( a, b ) )
% 219.64/220.09 ) ), ~( =( compose( compose( a, b ), X ), compose( compose( a, b ), Y )
% 219.64/220.09 ) ), ~( =( codomain( compose( a, b ) ), domain( Y ) ) ) ] )
% 219.64/220.09 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 14, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~( =(
% 219.64/220.09 codomain( compose( a, b ) ), domain( Y ) ) ), ~( =( compose( compose( a,
% 219.64/220.09 b ), Y ), compose( compose( a, b ), X ) ) ), =( X, Y ) ] )
% 219.64/220.09 , clause( 3351, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), =( Y
% 219.64/220.09 , X ), ~( =( compose( compose( a, b ), X ), compose( compose( a, b ), Y )
% 219.64/220.09 ) ), ~( =( codomain( compose( a, b ) ), domain( Y ) ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 219.64/220.09 ), ==>( 1, 3 ), ==>( 2, 2 ), ==>( 3, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3357, [ ~( =( domain( Y ), codomain( X ) ) ), =( codomain( compose(
% 219.64/220.09 X, Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 , clause( 5, [ ~( =( codomain( X ), domain( Y ) ) ), =( codomain( compose(
% 219.64/220.09 X, Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3360, [ ~( =( codomain( a ), codomain( X ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 8, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 , 0, clause( 3357, [ ~( =( domain( Y ), codomain( X ) ) ), =( codomain(
% 219.64/220.09 compose( X, Y ) ), codomain( Y ) ) ] )
% 219.64/220.09 , 0, 2, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y, b )] )
% 219.64/220.09 ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3361, [ ~( =( codomain( X ), codomain( a ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3360, [ ~( =( codomain( a ), codomain( X ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 42, [ ~( =( codomain( X ), codomain( a ) ) ), =( codomain( compose(
% 219.64/220.09 X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3361, [ ~( =( codomain( X ), codomain( a ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 219.64/220.09 1 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3364, [ ~( =( codomain( a ), codomain( X ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 42, [ ~( =( codomain( X ), codomain( a ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqrefl(
% 219.64/220.09 clause( 3367, [ =( codomain( compose( a, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3364, [ ~( =( codomain( a ), codomain( X ) ) ), =( codomain(
% 219.64/220.09 compose( X, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, a )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 47, [ =( codomain( compose( a, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , clause( 3367, [ =( codomain( compose( a, b ) ), codomain( b ) ) ] )
% 219.64/220.09 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3370, [ ~( =( domain( Y ), codomain( X ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y
% 219.64/220.09 ), Z ) ) ] )
% 219.64/220.09 , clause( 6, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y
% 219.64/220.09 ), Z ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3379, [ =( compose( X, compose( b, g ) ), compose( compose( X, b )
% 219.64/220.09 , h ) ), ~( =( domain( b ), codomain( X ) ) ), ~( =( codomain( b ),
% 219.64/220.09 domain( h ) ) ) ] )
% 219.64/220.09 , clause( 11, [ =( compose( b, h ), compose( b, g ) ) ] )
% 219.64/220.09 , 0, clause( 3370, [ ~( =( domain( Y ), codomain( X ) ) ), ~( =( codomain(
% 219.64/220.09 Y ), domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose(
% 219.64/220.09 X, Y ), Z ) ) ] )
% 219.64/220.09 , 2, 3, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y, b ),
% 219.64/220.09 :=( Z, h )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3381, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), h ) ), ~( =( codomain( b ),
% 219.64/220.09 domain( h ) ) ) ] )
% 219.64/220.09 , clause( 8, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 , 0, clause( 3379, [ =( compose( X, compose( b, g ) ), compose( compose( X
% 219.64/220.09 , b ), h ) ), ~( =( domain( b ), codomain( X ) ) ), ~( =( codomain( b ),
% 219.64/220.09 domain( h ) ) ) ] )
% 219.64/220.09 , 1, 2, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3382, [ ~( =( codomain( b ), codomain( b ) ) ), ~( =( codomain( a )
% 219.64/220.09 , codomain( X ) ) ), =( compose( X, compose( b, g ) ), compose( compose(
% 219.64/220.09 X, b ), h ) ) ] )
% 219.64/220.09 , clause( 9, [ =( domain( h ), codomain( b ) ) ] )
% 219.64/220.09 , 0, clause( 3381, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( X
% 219.64/220.09 , compose( b, g ) ), compose( compose( X, b ), h ) ), ~( =( codomain( b )
% 219.64/220.09 , domain( h ) ) ) ] )
% 219.64/220.09 , 2, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqrefl(
% 219.64/220.09 clause( 3383, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), h ) ) ] )
% 219.64/220.09 , clause( 3382, [ ~( =( codomain( b ), codomain( b ) ) ), ~( =( codomain( a
% 219.64/220.09 ), codomain( X ) ) ), =( compose( X, compose( b, g ) ), compose( compose(
% 219.64/220.09 X, b ), h ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3384, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), h ) ) ] )
% 219.64/220.09 , clause( 3383, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), h ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 53, [ =( compose( X, compose( b, g ) ), compose( compose( X, b ), h
% 219.64/220.09 ) ), ~( =( codomain( X ), codomain( a ) ) ) ] )
% 219.64/220.09 , clause( 3384, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), h ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 219.64/220.09 0 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3388, [ ~( =( domain( Y ), codomain( X ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y
% 219.64/220.09 ), Z ) ) ] )
% 219.64/220.09 , clause( 6, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose( X, Y
% 219.64/220.09 ), Z ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3396, [ ~( =( codomain( X ), codomain( b ) ) ), ~( =( domain( X ),
% 219.64/220.09 codomain( Y ) ) ), =( compose( Y, compose( X, g ) ), compose( compose( Y
% 219.64/220.09 , X ), g ) ) ] )
% 219.64/220.09 , clause( 10, [ =( domain( g ), codomain( b ) ) ] )
% 219.64/220.09 , 0, clause( 3388, [ ~( =( domain( Y ), codomain( X ) ) ), ~( =( codomain(
% 219.64/220.09 Y ), domain( Z ) ) ), =( compose( X, compose( Y, Z ) ), compose( compose(
% 219.64/220.09 X, Y ), Z ) ) ] )
% 219.64/220.09 , 1, 4, substitution( 0, [] ), substitution( 1, [ :=( X, Y ), :=( Y, X ),
% 219.64/220.09 :=( Z, g )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3405, [ ~( =( codomain( Y ), domain( X ) ) ), ~( =( codomain( X ),
% 219.64/220.09 codomain( b ) ) ), =( compose( Y, compose( X, g ) ), compose( compose( Y
% 219.64/220.09 , X ), g ) ) ] )
% 219.64/220.09 , clause( 3396, [ ~( =( codomain( X ), codomain( b ) ) ), ~( =( domain( X )
% 219.64/220.09 , codomain( Y ) ) ), =( compose( Y, compose( X, g ) ), compose( compose(
% 219.64/220.09 Y, X ), g ) ) ] )
% 219.64/220.09 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 72, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 codomain( b ) ) ), =( compose( X, compose( Y, g ) ), compose( compose( X
% 219.64/220.09 , Y ), g ) ) ] )
% 219.64/220.09 , clause( 3405, [ ~( =( codomain( Y ), domain( X ) ) ), ~( =( codomain( X )
% 219.64/220.09 , codomain( b ) ) ), =( compose( Y, compose( X, g ) ), compose( compose(
% 219.64/220.09 Y, X ), g ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 219.64/220.09 ), ==>( 1, 1 ), ==>( 2, 2 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3411, [ ~( =( domain( Y ), codomain( X ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 codomain( b ) ) ), =( compose( X, compose( Y, g ) ), compose( compose( X
% 219.64/220.09 , Y ), g ) ) ] )
% 219.64/220.09 , clause( 72, [ ~( =( codomain( X ), domain( Y ) ) ), ~( =( codomain( Y ),
% 219.64/220.09 codomain( b ) ) ), =( compose( X, compose( Y, g ) ), compose( compose( X
% 219.64/220.09 , Y ), g ) ) ] )
% 219.64/220.09 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqrefl(
% 219.64/220.09 clause( 3422, [ ~( =( domain( b ), codomain( X ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , clause( 3411, [ ~( =( domain( Y ), codomain( X ) ) ), ~( =( codomain( Y )
% 219.64/220.09 , codomain( b ) ) ), =( compose( X, compose( Y, g ) ), compose( compose(
% 219.64/220.09 X, Y ), g ) ) ] )
% 219.64/220.09 , 1, substitution( 0, [ :=( X, X ), :=( Y, b )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3423, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , clause( 8, [ =( domain( b ), codomain( a ) ) ] )
% 219.64/220.09 , 0, clause( 3422, [ ~( =( domain( b ), codomain( X ) ) ), =( compose( X,
% 219.64/220.09 compose( b, g ) ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , 0, 2, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 paramod(
% 219.64/220.09 clause( 3428, [ =( compose( compose( X, b ), h ), compose( compose( X, b )
% 219.64/220.09 , g ) ), ~( =( codomain( X ), codomain( a ) ) ), ~( =( codomain( a ),
% 219.64/220.09 codomain( X ) ) ) ] )
% 219.64/220.09 , clause( 53, [ =( compose( X, compose( b, g ) ), compose( compose( X, b )
% 219.64/220.09 , h ) ), ~( =( codomain( X ), codomain( a ) ) ) ] )
% 219.64/220.09 , 0, clause( 3423, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( X
% 219.64/220.09 , compose( b, g ) ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , 1, 1, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 219.64/220.09 ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3431, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( compose(
% 219.64/220.09 X, b ), h ), compose( compose( X, b ), g ) ), ~( =( codomain( X ),
% 219.64/220.09 codomain( a ) ) ) ] )
% 219.64/220.09 , clause( 3428, [ =( compose( compose( X, b ), h ), compose( compose( X, b
% 219.64/220.09 ), g ) ), ~( =( codomain( X ), codomain( a ) ) ), ~( =( codomain( a ),
% 219.64/220.09 codomain( X ) ) ) ] )
% 219.64/220.09 , 2, substitution( 0, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 factor(
% 219.64/220.09 clause( 3438, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( compose(
% 219.64/220.09 X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , clause( 3431, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose(
% 219.64/220.09 compose( X, b ), h ), compose( compose( X, b ), g ) ), ~( =( codomain( X
% 219.64/220.09 ), codomain( a ) ) ) ] )
% 219.64/220.09 , 0, 2, substitution( 0, [ :=( X, X )] )).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 subsumption(
% 219.64/220.09 clause( 73, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( compose(
% 219.64/220.09 X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , clause( 3438, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose(
% 219.64/220.09 compose( X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 219.64/220.09 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 219.64/220.09 1 )] ) ).
% 219.64/220.09
% 219.64/220.09
% 219.64/220.09 eqswap(
% 219.64/220.09 clause( 3439, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose( compose(
% 220.15/220.52 X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 220.15/220.52 , clause( 73, [ ~( =( codomain( X ), codomain( a ) ) ), =( compose( compose(
% 220.15/220.52 X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqrefl(
% 220.15/220.52 clause( 3442, [ =( compose( compose( a, b ), h ), compose( compose( a, b )
% 220.15/220.52 , g ) ) ] )
% 220.15/220.52 , clause( 3439, [ ~( =( codomain( a ), codomain( X ) ) ), =( compose(
% 220.15/220.52 compose( X, b ), h ), compose( compose( X, b ), g ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [ :=( X, a )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 subsumption(
% 220.15/220.52 clause( 74, [ =( compose( compose( a, b ), h ), compose( compose( a, b ), g
% 220.15/220.52 ) ) ] )
% 220.15/220.52 , clause( 3442, [ =( compose( compose( a, b ), h ), compose( compose( a, b
% 220.15/220.52 ), g ) ) ] )
% 220.15/220.52 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 paramod(
% 220.15/220.52 clause( 3456, [ ~( =( codomain( b ), domain( X ) ) ), ~( =( codomain(
% 220.15/220.52 compose( a, b ) ), domain( Y ) ) ), ~( =( compose( compose( a, b ), X ),
% 220.15/220.52 compose( compose( a, b ), Y ) ) ), =( Y, X ) ] )
% 220.15/220.52 , clause( 47, [ =( codomain( compose( a, b ) ), codomain( b ) ) ] )
% 220.15/220.52 , 0, clause( 14, [ ~( =( codomain( compose( a, b ) ), domain( X ) ) ), ~(
% 220.15/220.52 =( codomain( compose( a, b ) ), domain( Y ) ) ), ~( =( compose( compose(
% 220.15/220.52 a, b ), Y ), compose( compose( a, b ), X ) ) ), =( X, Y ) ] )
% 220.15/220.52 , 1, 2, substitution( 0, [] ), substitution( 1, [ :=( X, Y ), :=( Y, X )] )
% 220.15/220.52 ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 paramod(
% 220.15/220.52 clause( 3459, [ ~( =( codomain( b ), domain( X ) ) ), ~( =( codomain( b ),
% 220.15/220.52 domain( Y ) ) ), ~( =( compose( compose( a, b ), Y ), compose( compose( a
% 220.15/220.52 , b ), X ) ) ), =( X, Y ) ] )
% 220.15/220.52 , clause( 47, [ =( codomain( compose( a, b ) ), codomain( b ) ) ] )
% 220.15/220.52 , 0, clause( 3456, [ ~( =( codomain( b ), domain( X ) ) ), ~( =( codomain(
% 220.15/220.52 compose( a, b ) ), domain( Y ) ) ), ~( =( compose( compose( a, b ), X ),
% 220.15/220.52 compose( compose( a, b ), Y ) ) ), =( Y, X ) ] )
% 220.15/220.52 , 1, 2, substitution( 0, [] ), substitution( 1, [ :=( X, Y ), :=( Y, X )] )
% 220.15/220.52 ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 subsumption(
% 220.15/220.52 clause( 113, [ ~( =( compose( compose( a, b ), Y ), compose( compose( a, b
% 220.15/220.52 ), X ) ) ), =( X, Y ), ~( =( codomain( b ), domain( X ) ) ), ~( =(
% 220.15/220.52 codomain( b ), domain( Y ) ) ) ] )
% 220.15/220.52 , clause( 3459, [ ~( =( codomain( b ), domain( X ) ) ), ~( =( codomain( b )
% 220.15/220.52 , domain( Y ) ) ), ~( =( compose( compose( a, b ), Y ), compose( compose(
% 220.15/220.52 a, b ), X ) ) ), =( X, Y ) ] )
% 220.15/220.52 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 2
% 220.15/220.52 ), ==>( 1, 3 ), ==>( 2, 0 ), ==>( 3, 1 )] ) ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 3469, [ ~( =( compose( compose( a, b ), Y ), compose( compose( a, b
% 220.15/220.52 ), X ) ) ), =( Y, X ), ~( =( codomain( b ), domain( Y ) ) ), ~( =(
% 220.15/220.52 codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , clause( 113, [ ~( =( compose( compose( a, b ), Y ), compose( compose( a,
% 220.15/220.52 b ), X ) ) ), =( X, Y ), ~( =( codomain( b ), domain( X ) ) ), ~( =(
% 220.15/220.52 codomain( b ), domain( Y ) ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 3476, [ ~( =( g, h ) ) ] )
% 220.15/220.52 , clause( 12, [ ~( =( h, g ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 paramod(
% 220.15/220.52 clause( 3480, [ ~( =( g, X ) ), ~( =( compose( compose( a, b ), h ),
% 220.15/220.52 compose( compose( a, b ), X ) ) ), ~( =( codomain( b ), domain( h ) ) ),
% 220.15/220.52 ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , clause( 3469, [ ~( =( compose( compose( a, b ), Y ), compose( compose( a
% 220.15/220.52 , b ), X ) ) ), =( Y, X ), ~( =( codomain( b ), domain( Y ) ) ), ~( =(
% 220.15/220.52 codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , 1, clause( 3476, [ ~( =( g, h ) ) ] )
% 220.15/220.52 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, h )] ), substitution( 1, [] )
% 220.15/220.52 ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 paramod(
% 220.15/220.52 clause( 6275, [ ~( =( compose( compose( a, b ), g ), compose( compose( a, b
% 220.15/220.52 ), X ) ) ), ~( =( g, X ) ), ~( =( codomain( b ), domain( h ) ) ), ~( =(
% 220.15/220.52 codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , clause( 74, [ =( compose( compose( a, b ), h ), compose( compose( a, b )
% 220.15/220.52 , g ) ) ] )
% 220.15/220.52 , 0, clause( 3480, [ ~( =( g, X ) ), ~( =( compose( compose( a, b ), h ),
% 220.15/220.52 compose( compose( a, b ), X ) ) ), ~( =( codomain( b ), domain( h ) ) ),
% 220.15/220.52 ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , 1, 2, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 paramod(
% 220.15/220.52 clause( 6282, [ ~( =( codomain( b ), codomain( b ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), g ), compose( compose( a, b ), X ) ) ), ~( =( g, X ) ),
% 220.15/220.52 ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , clause( 9, [ =( domain( h ), codomain( b ) ) ] )
% 220.15/220.52 , 0, clause( 6275, [ ~( =( compose( compose( a, b ), g ), compose( compose(
% 220.15/220.52 a, b ), X ) ) ), ~( =( g, X ) ), ~( =( codomain( b ), domain( h ) ) ),
% 220.15/220.52 ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , 2, 4, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqrefl(
% 220.15/220.52 clause( 6283, [ ~( =( compose( compose( a, b ), g ), compose( compose( a, b
% 220.15/220.52 ), X ) ) ), ~( =( g, X ) ), ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , clause( 6282, [ ~( =( codomain( b ), codomain( b ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), g ), compose( compose( a, b ), X ) ) ), ~( =( g, X ) ),
% 220.15/220.52 ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 6286, [ ~( =( domain( X ), codomain( b ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), g ), compose( compose( a, b ), X ) ) ), ~( =( g, X ) ) ]
% 220.15/220.52 )
% 220.15/220.52 , clause( 6283, [ ~( =( compose( compose( a, b ), g ), compose( compose( a
% 220.15/220.52 , b ), X ) ) ), ~( =( g, X ) ), ~( =( codomain( b ), domain( X ) ) ) ] )
% 220.15/220.52 , 2, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 6288, [ ~( =( X, g ) ), ~( =( domain( X ), codomain( b ) ) ), ~(
% 220.15/220.52 =( compose( compose( a, b ), g ), compose( compose( a, b ), X ) ) ) ] )
% 220.15/220.52 , clause( 6286, [ ~( =( domain( X ), codomain( b ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), g ), compose( compose( a, b ), X ) ) ), ~( =( g, X ) ) ]
% 220.15/220.52 )
% 220.15/220.52 , 2, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 6289, [ ~( =( compose( compose( a, b ), X ), compose( compose( a, b
% 220.15/220.52 ), g ) ) ), ~( =( X, g ) ), ~( =( domain( X ), codomain( b ) ) ) ] )
% 220.15/220.52 , clause( 6288, [ ~( =( X, g ) ), ~( =( domain( X ), codomain( b ) ) ), ~(
% 220.15/220.52 =( compose( compose( a, b ), g ), compose( compose( a, b ), X ) ) ) ] )
% 220.15/220.52 , 2, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 6290, [ ~( =( codomain( b ), domain( X ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), X ), compose( compose( a, b ), g ) ) ), ~( =( X, g ) ) ]
% 220.15/220.52 )
% 220.15/220.52 , clause( 6289, [ ~( =( compose( compose( a, b ), X ), compose( compose( a
% 220.15/220.52 , b ), g ) ) ), ~( =( X, g ) ), ~( =( domain( X ), codomain( b ) ) ) ] )
% 220.15/220.52 , 2, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 subsumption(
% 220.15/220.52 clause( 2999, [ ~( =( X, g ) ), ~( =( codomain( b ), domain( X ) ) ), ~(
% 220.15/220.52 =( compose( compose( a, b ), X ), compose( compose( a, b ), g ) ) ) ] )
% 220.15/220.52 , clause( 6290, [ ~( =( codomain( b ), domain( X ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), X ), compose( compose( a, b ), g ) ) ), ~( =( X, g ) ) ]
% 220.15/220.52 )
% 220.15/220.52 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 1 ), ==>( 1,
% 220.15/220.52 2 ), ==>( 2, 0 )] ) ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqswap(
% 220.15/220.52 clause( 6291, [ ~( =( g, X ) ), ~( =( codomain( b ), domain( X ) ) ), ~(
% 220.15/220.52 =( compose( compose( a, b ), X ), compose( compose( a, b ), g ) ) ) ] )
% 220.15/220.52 , clause( 2999, [ ~( =( X, g ) ), ~( =( codomain( b ), domain( X ) ) ), ~(
% 220.15/220.52 =( compose( compose( a, b ), X ), compose( compose( a, b ), g ) ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [ :=( X, X )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqrefl(
% 220.15/220.52 clause( 6299, [ ~( =( codomain( b ), domain( g ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), g ), compose( compose( a, b ), g ) ) ) ] )
% 220.15/220.52 , clause( 6291, [ ~( =( g, X ) ), ~( =( codomain( b ), domain( X ) ) ), ~(
% 220.15/220.52 =( compose( compose( a, b ), X ), compose( compose( a, b ), g ) ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [ :=( X, g )] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqrefl(
% 220.15/220.52 clause( 6301, [ ~( =( codomain( b ), domain( g ) ) ) ] )
% 220.15/220.52 , clause( 6299, [ ~( =( codomain( b ), domain( g ) ) ), ~( =( compose(
% 220.15/220.52 compose( a, b ), g ), compose( compose( a, b ), g ) ) ) ] )
% 220.15/220.52 , 1, substitution( 0, [] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 paramod(
% 220.15/220.52 clause( 6302, [ ~( =( codomain( b ), codomain( b ) ) ) ] )
% 220.15/220.52 , clause( 10, [ =( domain( g ), codomain( b ) ) ] )
% 220.15/220.52 , 0, clause( 6301, [ ~( =( codomain( b ), domain( g ) ) ) ] )
% 220.15/220.52 , 0, 4, substitution( 0, [] ), substitution( 1, [] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 eqrefl(
% 220.15/220.52 clause( 6303, [] )
% 220.15/220.52 , clause( 6302, [ ~( =( codomain( b ), codomain( b ) ) ) ] )
% 220.15/220.52 , 0, substitution( 0, [] )).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 subsumption(
% 220.15/220.52 clause( 3000, [] )
% 220.15/220.52 , clause( 6303, [] )
% 220.15/220.52 , substitution( 0, [] ), permutation( 0, [] ) ).
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 end.
% 220.15/220.52
% 220.15/220.52 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 220.15/220.52
% 220.15/220.52 Memory use:
% 220.15/220.52
% 220.15/220.52 space for terms: 66162
% 220.15/220.52 space for clauses: 285459
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 clauses generated: 30107
% 220.15/220.52 clauses kept: 3001
% 220.15/220.52 clauses selected: 233
% 220.15/220.52 clauses deleted: 63
% 220.15/220.52 clauses inuse deleted: 0
% 220.15/220.52
% 220.15/220.52 subsentry: 1824141
% 220.15/220.52 literals s-matched: 101242
% 220.15/220.52 literals matched: 82901
% 220.15/220.52 full subsumption: 76733
% 220.15/220.52
% 220.15/220.52 checksum: -699919011
% 220.15/220.52
% 220.15/220.52
% 220.15/220.52 Bliksem ended
%------------------------------------------------------------------------------