%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : CAT010-10 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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 1.15s 1.57s
% Output : Refutation 1.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : CAT010-10 : TPTP v8.1.0. Released v7.3.0.
% 0.00/0.07 % Command : bliksem %s
% 0.07/0.26 % Computer : n029.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % DateTime : Sun May 29 22:25:58 EDT 2022
% 0.07/0.26 % CPUTime :
% 1.15/1.57 *** allocated 10000 integers for termspace/termends
% 1.15/1.57 *** allocated 10000 integers for clauses
% 1.15/1.57 *** allocated 10000 integers for justifications
% 1.15/1.57 Bliksem 1.12
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 Automatic Strategy Selection
% 1.15/1.57
% 1.15/1.57 Clauses:
% 1.15/1.57 [
% 1.15/1.57 [ =( ifeq3( X, X, Y, Z ), Y ) ],
% 1.15/1.57 [ =( ifeq2( X, X, Y, Z ), Y ) ],
% 1.15/1.57 [ =( ifeq( X, X, Y, Z ), Y ) ],
% 1.15/1.57 [ =( ifeq( equivalent( X, Y ), true, 'there_exists'( X ), true ), true )
% 1.15/1.57 ],
% 1.15/1.57 [ =( ifeq2( equivalent( X, Y ), true, X, Y ), Y ) ],
% 1.15/1.57 [ =( ifeq( 'there_exists'( X ), true, equivalent( X, X ), true ), true )
% 1.15/1.57 ],
% 1.15/1.57 [ =( ifeq( 'there_exists'( domain( X ) ), true, 'there_exists'( X ),
% 1.15/1.57 true ), true ) ],
% 1.15/1.57 [ =( ifeq( 'there_exists'( codomain( X ) ), true, 'there_exists'( X ),
% 1.15/1.57 true ), true ) ],
% 1.15/1.57 [ =( ifeq( 'there_exists'( compose( X, Y ) ), true, 'there_exists'(
% 1.15/1.57 domain( X ) ), true ), true ) ],
% 1.15/1.57 [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain( X ),
% 1.15/1.57 codomain( Y ) ), codomain( Y ) ) ],
% 1.15/1.57 [ =( ifeq( 'there_exists'( domain( X ) ), true, ifeq3( domain( X ),
% 1.15/1.57 codomain( Y ), 'there_exists'( compose( X, Y ) ), true ), true ), true )
% 1.15/1.57 ],
% 1.15/1.57 [ =( compose( X, compose( Y, Z ) ), compose( compose( X, Y ), Z ) ) ]
% 1.15/1.57 ,
% 1.15/1.57 [ =( compose( X, domain( X ) ), X ) ],
% 1.15/1.57 [ =( compose( codomain( X ), X ), X ) ],
% 1.15/1.57 [ =( 'there_exists'( compose( a, b ) ), true ) ],
% 1.15/1.57 [ ~( =( codomain( compose( a, b ) ), codomain( a ) ) ) ]
% 1.15/1.57 ] .
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 percentage equality = 1.000000, percentage horn = 1.000000
% 1.15/1.57 This is a pure equality problem
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 Options Used:
% 1.15/1.57
% 1.15/1.57 useres = 1
% 1.15/1.57 useparamod = 1
% 1.15/1.57 useeqrefl = 1
% 1.15/1.57 useeqfact = 1
% 1.15/1.57 usefactor = 1
% 1.15/1.57 usesimpsplitting = 0
% 1.15/1.57 usesimpdemod = 5
% 1.15/1.57 usesimpres = 3
% 1.15/1.57
% 1.15/1.57 resimpinuse = 1000
% 1.15/1.57 resimpclauses = 20000
% 1.15/1.57 substype = eqrewr
% 1.15/1.57 backwardsubs = 1
% 1.15/1.57 selectoldest = 5
% 1.15/1.57
% 1.15/1.57 litorderings [0] = split
% 1.15/1.57 litorderings [1] = extend the termordering, first sorting on arguments
% 1.15/1.57
% 1.15/1.57 termordering = kbo
% 1.15/1.57
% 1.15/1.57 litapriori = 0
% 1.15/1.57 termapriori = 1
% 1.15/1.57 litaposteriori = 0
% 1.15/1.57 termaposteriori = 0
% 1.15/1.57 demodaposteriori = 0
% 1.15/1.57 ordereqreflfact = 0
% 1.15/1.57
% 1.15/1.57 litselect = negord
% 1.15/1.57
% 1.15/1.57 maxweight = 15
% 1.15/1.57 maxdepth = 30000
% 1.15/1.57 maxlength = 115
% 1.15/1.57 maxnrvars = 195
% 1.15/1.57 excuselevel = 1
% 1.15/1.57 increasemaxweight = 1
% 1.15/1.57
% 1.15/1.57 maxselected = 10000000
% 1.15/1.57 maxnrclauses = 10000000
% 1.15/1.57
% 1.15/1.57 showgenerated = 0
% 1.15/1.57 showkept = 0
% 1.15/1.57 showselected = 0
% 1.15/1.57 showdeleted = 0
% 1.15/1.57 showresimp = 1
% 1.15/1.57 showstatus = 2000
% 1.15/1.57
% 1.15/1.57 prologoutput = 1
% 1.15/1.57 nrgoals = 5000000
% 1.15/1.57 totalproof = 1
% 1.15/1.57
% 1.15/1.57 Symbols occurring in the translation:
% 1.15/1.57
% 1.15/1.57 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.15/1.57 . [1, 2] (w:1, o:26, a:1, s:1, b:0),
% 1.15/1.57 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 1.15/1.57 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.15/1.57 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.15/1.57 ifeq3 [42, 4] (w:1, o:54, a:1, s:1, b:0),
% 1.15/1.57 ifeq2 [43, 4] (w:1, o:53, a:1, s:1, b:0),
% 1.15/1.57 ifeq [44, 4] (w:1, o:55, a:1, s:1, b:0),
% 1.15/1.57 equivalent [47, 2] (w:1, o:51, a:1, s:1, b:0),
% 1.15/1.57 true [48, 0] (w:1, o:14, a:1, s:1, b:0),
% 1.15/1.57 'there_exists' [49, 1] (w:1, o:23, a:1, s:1, b:0),
% 1.15/1.57 domain [50, 1] (w:1, o:25, a:1, s:1, b:0),
% 1.15/1.57 codomain [51, 1] (w:1, o:24, a:1, s:1, b:0),
% 1.15/1.57 compose [52, 2] (w:1, o:52, a:1, s:1, b:0),
% 1.15/1.57 a [54, 0] (w:1, o:16, a:1, s:1, b:0),
% 1.15/1.57 b [55, 0] (w:1, o:17, a:1, s:1, b:0).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 Starting Search:
% 1.15/1.57
% 1.15/1.57 Resimplifying inuse:
% 1.15/1.57 Done
% 1.15/1.57
% 1.15/1.57 Failed to find proof!
% 1.15/1.57 maxweight = 15
% 1.15/1.57 maxnrclauses = 10000000
% 1.15/1.57 Generated: 14713
% 1.15/1.57 Kept: 484
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 The strategy used was not complete!
% 1.15/1.57
% 1.15/1.57 Increased maxweight to 16
% 1.15/1.57
% 1.15/1.57 Starting Search:
% 1.15/1.57
% 1.15/1.57 Resimplifying inuse:
% 1.15/1.57 Done
% 1.15/1.57
% 1.15/1.57 Resimplifying inuse:
% 1.15/1.57 Done
% 1.15/1.57
% 1.15/1.57 Failed to find proof!
% 1.15/1.57 maxweight = 16
% 1.15/1.57 maxnrclauses = 10000000
% 1.15/1.57 Generated: 119531
% 1.15/1.57 Kept: 1070
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 The strategy used was not complete!
% 1.15/1.57
% 1.15/1.57 Increased maxweight to 17
% 1.15/1.57
% 1.15/1.57 Starting Search:
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 Bliksems!, er is een bewijs:
% 1.15/1.57 % SZS status Unsatisfiable
% 1.15/1.57 % SZS output start Refutation
% 1.15/1.57
% 1.15/1.57 clause( 1, [ =( ifeq2( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 2, [ =( ifeq( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 6, [ =( ifeq( 'there_exists'( domain( X ) ), true, 'there_exists'(
% 1.15/1.57 X ), true ), true ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 8, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( X ) ), true ), true ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 9, [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain( X )
% 1.15/1.57 , codomain( Y ) ), codomain( Y ) ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 11, [ =( compose( X, compose( Y, Z ) ), compose( compose( X, Y ), Z
% 1.15/1.57 ) ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 13, [ =( compose( codomain( X ), X ), X ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 14, [ =( 'there_exists'( compose( a, b ) ), true ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 15, [ ~( =( codomain( compose( a, b ) ), codomain( a ) ) ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 21, [ =( compose( compose( codomain( compose( X, Y ) ), X ), Y ),
% 1.15/1.57 compose( X, Y ) ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 44, [ =( ifeq2( 'there_exists'( X ), true, domain( codomain( X ) )
% 1.15/1.57 , codomain( X ) ), codomain( X ) ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 85, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 359, [ =( domain( codomain( compose( a, b ) ) ), codomain( compose(
% 1.15/1.57 a, b ) ) ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 432, [ =( 'there_exists'( domain( compose( codomain( compose( a, b
% 1.15/1.57 ) ), a ) ) ), true ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 438, [ =( 'there_exists'( compose( codomain( compose( a, b ) ), a )
% 1.15/1.57 ), true ) ] )
% 1.15/1.57 .
% 1.15/1.57 clause( 446, [] )
% 1.15/1.57 .
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 % SZS output end Refutation
% 1.15/1.57 found a proof!
% 1.15/1.57
% 1.15/1.57 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 1.15/1.57
% 1.15/1.57 initialclauses(
% 1.15/1.57 [ clause( 448, [ =( ifeq3( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , clause( 449, [ =( ifeq2( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , clause( 450, [ =( ifeq( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , clause( 451, [ =( ifeq( equivalent( X, Y ), true, 'there_exists'( X ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , clause( 452, [ =( ifeq2( equivalent( X, Y ), true, X, Y ), Y ) ] )
% 1.15/1.57 , clause( 453, [ =( ifeq( 'there_exists'( X ), true, equivalent( X, X ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , clause( 454, [ =( ifeq( 'there_exists'( domain( X ) ), true,
% 1.15/1.57 'there_exists'( X ), true ), true ) ] )
% 1.15/1.57 , clause( 455, [ =( ifeq( 'there_exists'( codomain( X ) ), true,
% 1.15/1.57 'there_exists'( X ), true ), true ) ] )
% 1.15/1.57 , clause( 456, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( X ) ), true ), true ) ] )
% 1.15/1.57 , clause( 457, [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain(
% 1.15/1.57 X ), codomain( Y ) ), codomain( Y ) ) ] )
% 1.15/1.57 , clause( 458, [ =( ifeq( 'there_exists'( domain( X ) ), true, ifeq3(
% 1.15/1.57 domain( X ), codomain( Y ), 'there_exists'( compose( X, Y ) ), true ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , clause( 459, [ =( compose( X, compose( Y, Z ) ), compose( compose( X, Y )
% 1.15/1.57 , Z ) ) ] )
% 1.15/1.57 , clause( 460, [ =( compose( X, domain( X ) ), X ) ] )
% 1.15/1.57 , clause( 461, [ =( compose( codomain( X ), X ), X ) ] )
% 1.15/1.57 , clause( 462, [ =( 'there_exists'( compose( a, b ) ), true ) ] )
% 1.15/1.57 , clause( 463, [ ~( =( codomain( compose( a, b ) ), codomain( a ) ) ) ] )
% 1.15/1.57 ] ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 1, [ =( ifeq2( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , clause( 449, [ =( ifeq2( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.15/1.57 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 2, [ =( ifeq( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , clause( 450, [ =( ifeq( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.15/1.57 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 6, [ =( ifeq( 'there_exists'( domain( X ) ), true, 'there_exists'(
% 1.15/1.57 X ), true ), true ) ] )
% 1.15/1.57 , clause( 454, [ =( ifeq( 'there_exists'( domain( X ) ), true,
% 1.15/1.57 'there_exists'( X ), true ), true ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 8, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( X ) ), true ), true ) ] )
% 1.15/1.57 , clause( 456, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( X ) ), true ), true ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.15/1.57 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 9, [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain( X )
% 1.15/1.57 , codomain( Y ) ), codomain( Y ) ) ] )
% 1.15/1.57 , clause( 457, [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain(
% 1.15/1.57 X ), codomain( Y ) ), codomain( Y ) ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.15/1.57 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 11, [ =( compose( X, compose( Y, Z ) ), compose( compose( X, Y ), Z
% 1.15/1.57 ) ) ] )
% 1.15/1.57 , clause( 459, [ =( compose( X, compose( Y, Z ) ), compose( compose( X, Y )
% 1.15/1.57 , Z ) ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 1.15/1.57 permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 13, [ =( compose( codomain( X ), X ), X ) ] )
% 1.15/1.57 , clause( 461, [ =( compose( codomain( X ), X ), X ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 14, [ =( 'there_exists'( compose( a, b ) ), true ) ] )
% 1.15/1.57 , clause( 462, [ =( 'there_exists'( compose( a, b ) ), true ) ] )
% 1.15/1.57 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 15, [ ~( =( codomain( compose( a, b ) ), codomain( a ) ) ) ] )
% 1.15/1.57 , clause( 463, [ ~( =( codomain( compose( a, b ) ), codomain( a ) ) ) ] )
% 1.15/1.57 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 552, [ =( compose( compose( X, Y ), Z ), compose( X, compose( Y, Z
% 1.15/1.57 ) ) ) ] )
% 1.15/1.57 , clause( 11, [ =( compose( X, compose( Y, Z ) ), compose( compose( X, Y )
% 1.15/1.57 , Z ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 555, [ =( compose( compose( codomain( compose( X, Y ) ), X ), Y ),
% 1.15/1.57 compose( X, Y ) ) ] )
% 1.15/1.57 , clause( 13, [ =( compose( codomain( X ), X ), X ) ] )
% 1.15/1.57 , 0, clause( 552, [ =( compose( compose( X, Y ), Z ), compose( X, compose(
% 1.15/1.57 Y, Z ) ) ) ] )
% 1.15/1.57 , 0, 9, substitution( 0, [ :=( X, compose( X, Y ) )] ), substitution( 1, [
% 1.15/1.57 :=( X, codomain( compose( X, Y ) ) ), :=( Y, X ), :=( Z, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 21, [ =( compose( compose( codomain( compose( X, Y ) ), X ), Y ),
% 1.15/1.57 compose( X, Y ) ) ] )
% 1.15/1.57 , clause( 555, [ =( compose( compose( codomain( compose( X, Y ) ), X ), Y )
% 1.15/1.57 , compose( X, Y ) ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.15/1.57 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 561, [ =( codomain( Y ), ifeq2( 'there_exists'( compose( X, Y ) ),
% 1.15/1.57 true, domain( X ), codomain( Y ) ) ) ] )
% 1.15/1.57 , clause( 9, [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain( X
% 1.15/1.57 ), codomain( Y ) ), codomain( Y ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 562, [ =( codomain( X ), ifeq2( 'there_exists'( X ), true, domain(
% 1.15/1.57 codomain( X ) ), codomain( X ) ) ) ] )
% 1.15/1.57 , clause( 13, [ =( compose( codomain( X ), X ), X ) ] )
% 1.15/1.57 , 0, clause( 561, [ =( codomain( Y ), ifeq2( 'there_exists'( compose( X, Y
% 1.15/1.57 ) ), true, domain( X ), codomain( Y ) ) ) ] )
% 1.15/1.57 , 0, 5, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X,
% 1.15/1.57 codomain( X ) ), :=( Y, X )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 563, [ =( ifeq2( 'there_exists'( X ), true, domain( codomain( X ) )
% 1.15/1.57 , codomain( X ) ), codomain( X ) ) ] )
% 1.15/1.57 , clause( 562, [ =( codomain( X ), ifeq2( 'there_exists'( X ), true, domain(
% 1.15/1.57 codomain( X ) ), codomain( X ) ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 44, [ =( ifeq2( 'there_exists'( X ), true, domain( codomain( X ) )
% 1.15/1.57 , codomain( X ) ), codomain( X ) ) ] )
% 1.15/1.57 , clause( 563, [ =( ifeq2( 'there_exists'( X ), true, domain( codomain( X )
% 1.15/1.57 ), codomain( X ) ), codomain( X ) ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 565, [ =( true, ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( X ) ), true ) ) ] )
% 1.15/1.57 , clause( 8, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( X ) ), true ), true ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 566, [ =( true, ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ) ) ] )
% 1.15/1.57 , clause( 21, [ =( compose( compose( codomain( compose( X, Y ) ), X ), Y )
% 1.15/1.57 , compose( X, Y ) ) ] )
% 1.15/1.57 , 0, clause( 565, [ =( true, ifeq( 'there_exists'( compose( X, Y ) ), true
% 1.15/1.57 , 'there_exists'( domain( X ) ), true ) ) ] )
% 1.15/1.57 , 0, 4, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 1.15/1.57 :=( X, compose( codomain( compose( X, Y ) ), X ) ), :=( Y, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 567, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , clause( 566, [ =( true, ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 85, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , clause( 567, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 1.15/1.57 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 569, [ =( codomain( X ), ifeq2( 'there_exists'( X ), true, domain(
% 1.15/1.57 codomain( X ) ), codomain( X ) ) ) ] )
% 1.15/1.57 , clause( 44, [ =( ifeq2( 'there_exists'( X ), true, domain( codomain( X )
% 1.15/1.57 ), codomain( X ) ), codomain( X ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 571, [ =( codomain( compose( a, b ) ), ifeq2( true, true, domain(
% 1.15/1.57 codomain( compose( a, b ) ) ), codomain( compose( a, b ) ) ) ) ] )
% 1.15/1.57 , clause( 14, [ =( 'there_exists'( compose( a, b ) ), true ) ] )
% 1.15/1.57 , 0, clause( 569, [ =( codomain( X ), ifeq2( 'there_exists'( X ), true,
% 1.15/1.57 domain( codomain( X ) ), codomain( X ) ) ) ] )
% 1.15/1.57 , 0, 6, substitution( 0, [] ), substitution( 1, [ :=( X, compose( a, b ) )] )
% 1.15/1.57 ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 572, [ =( codomain( compose( a, b ) ), domain( codomain( compose( a
% 1.15/1.57 , b ) ) ) ) ] )
% 1.15/1.57 , clause( 1, [ =( ifeq2( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , 0, clause( 571, [ =( codomain( compose( a, b ) ), ifeq2( true, true,
% 1.15/1.57 domain( codomain( compose( a, b ) ) ), codomain( compose( a, b ) ) ) ) ]
% 1.15/1.57 )
% 1.15/1.57 , 0, 5, substitution( 0, [ :=( X, true ), :=( Y, domain( codomain( compose(
% 1.15/1.57 a, b ) ) ) ), :=( Z, codomain( compose( a, b ) ) )] ), substitution( 1, [] )
% 1.15/1.57 ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 573, [ =( domain( codomain( compose( a, b ) ) ), codomain( compose(
% 1.15/1.57 a, b ) ) ) ] )
% 1.15/1.57 , clause( 572, [ =( codomain( compose( a, b ) ), domain( codomain( compose(
% 1.15/1.57 a, b ) ) ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 359, [ =( domain( codomain( compose( a, b ) ) ), codomain( compose(
% 1.15/1.57 a, b ) ) ) ] )
% 1.15/1.57 , clause( 573, [ =( domain( codomain( compose( a, b ) ) ), codomain(
% 1.15/1.57 compose( a, b ) ) ) ] )
% 1.15/1.57 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 575, [ =( true, ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ) ) ] )
% 1.15/1.57 , clause( 85, [ =( ifeq( 'there_exists'( compose( X, Y ) ), true,
% 1.15/1.57 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ), true ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 577, [ =( true, ifeq( true, true, 'there_exists'( domain( compose(
% 1.15/1.57 codomain( compose( a, b ) ), a ) ) ), true ) ) ] )
% 1.15/1.57 , clause( 14, [ =( 'there_exists'( compose( a, b ) ), true ) ] )
% 1.15/1.57 , 0, clause( 575, [ =( true, ifeq( 'there_exists'( compose( X, Y ) ), true
% 1.15/1.57 , 'there_exists'( domain( compose( codomain( compose( X, Y ) ), X ) ) ),
% 1.15/1.57 true ) ) ] )
% 1.15/1.57 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, a ), :=( Y, b )] )
% 1.15/1.57 ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 578, [ =( true, 'there_exists'( domain( compose( codomain( compose(
% 1.15/1.57 a, b ) ), a ) ) ) ) ] )
% 1.15/1.57 , clause( 2, [ =( ifeq( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , 0, clause( 577, [ =( true, ifeq( true, true, 'there_exists'( domain(
% 1.15/1.57 compose( codomain( compose( a, b ) ), a ) ) ), true ) ) ] )
% 1.15/1.57 , 0, 2, substitution( 0, [ :=( X, true ), :=( Y, 'there_exists'( domain(
% 1.15/1.57 compose( codomain( compose( a, b ) ), a ) ) ) ), :=( Z, true )] ),
% 1.15/1.57 substitution( 1, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 579, [ =( 'there_exists'( domain( compose( codomain( compose( a, b
% 1.15/1.57 ) ), a ) ) ), true ) ] )
% 1.15/1.57 , clause( 578, [ =( true, 'there_exists'( domain( compose( codomain(
% 1.15/1.57 compose( a, b ) ), a ) ) ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 432, [ =( 'there_exists'( domain( compose( codomain( compose( a, b
% 1.15/1.57 ) ), a ) ) ), true ) ] )
% 1.15/1.57 , clause( 579, [ =( 'there_exists'( domain( compose( codomain( compose( a,
% 1.15/1.57 b ) ), a ) ) ), true ) ] )
% 1.15/1.57 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 581, [ =( true, ifeq( 'there_exists'( domain( X ) ), true,
% 1.15/1.57 'there_exists'( X ), true ) ) ] )
% 1.15/1.57 , clause( 6, [ =( ifeq( 'there_exists'( domain( X ) ), true, 'there_exists'(
% 1.15/1.57 X ), true ), true ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 583, [ =( true, ifeq( true, true, 'there_exists'( compose( codomain(
% 1.15/1.57 compose( a, b ) ), a ) ), true ) ) ] )
% 1.15/1.57 , clause( 432, [ =( 'there_exists'( domain( compose( codomain( compose( a,
% 1.15/1.57 b ) ), a ) ) ), true ) ] )
% 1.15/1.57 , 0, clause( 581, [ =( true, ifeq( 'there_exists'( domain( X ) ), true,
% 1.15/1.57 'there_exists'( X ), true ) ) ] )
% 1.15/1.57 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, compose( codomain(
% 1.15/1.57 compose( a, b ) ), a ) )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 585, [ =( true, 'there_exists'( compose( codomain( compose( a, b )
% 1.15/1.57 ), a ) ) ) ] )
% 1.15/1.57 , clause( 2, [ =( ifeq( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , 0, clause( 583, [ =( true, ifeq( true, true, 'there_exists'( compose(
% 1.15/1.57 codomain( compose( a, b ) ), a ) ), true ) ) ] )
% 1.15/1.57 , 0, 2, substitution( 0, [ :=( X, true ), :=( Y, 'there_exists'( compose(
% 1.15/1.57 codomain( compose( a, b ) ), a ) ) ), :=( Z, true )] ), substitution( 1
% 1.15/1.57 , [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 586, [ =( 'there_exists'( compose( codomain( compose( a, b ) ), a )
% 1.15/1.57 ), true ) ] )
% 1.15/1.57 , clause( 585, [ =( true, 'there_exists'( compose( codomain( compose( a, b
% 1.15/1.57 ) ), a ) ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 438, [ =( 'there_exists'( compose( codomain( compose( a, b ) ), a )
% 1.15/1.57 ), true ) ] )
% 1.15/1.57 , clause( 586, [ =( 'there_exists'( compose( codomain( compose( a, b ) ), a
% 1.15/1.57 ) ), true ) ] )
% 1.15/1.57 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 588, [ =( codomain( Y ), ifeq2( 'there_exists'( compose( X, Y ) ),
% 1.15/1.57 true, domain( X ), codomain( Y ) ) ) ] )
% 1.15/1.57 , clause( 9, [ =( ifeq2( 'there_exists'( compose( X, Y ) ), true, domain( X
% 1.15/1.57 ), codomain( Y ) ), codomain( Y ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 eqswap(
% 1.15/1.57 clause( 591, [ ~( =( codomain( a ), codomain( compose( a, b ) ) ) ) ] )
% 1.15/1.57 , clause( 15, [ ~( =( codomain( compose( a, b ) ), codomain( a ) ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 592, [ =( codomain( a ), ifeq2( true, true, domain( codomain(
% 1.15/1.57 compose( a, b ) ) ), codomain( a ) ) ) ] )
% 1.15/1.57 , clause( 438, [ =( 'there_exists'( compose( codomain( compose( a, b ) ), a
% 1.15/1.57 ) ), true ) ] )
% 1.15/1.57 , 0, clause( 588, [ =( codomain( Y ), ifeq2( 'there_exists'( compose( X, Y
% 1.15/1.57 ) ), true, domain( X ), codomain( Y ) ) ) ] )
% 1.15/1.57 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, codomain( compose(
% 1.15/1.57 a, b ) ) ), :=( Y, a )] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 593, [ =( codomain( a ), domain( codomain( compose( a, b ) ) ) ) ]
% 1.15/1.57 )
% 1.15/1.57 , clause( 1, [ =( ifeq2( X, X, Y, Z ), Y ) ] )
% 1.15/1.57 , 0, clause( 592, [ =( codomain( a ), ifeq2( true, true, domain( codomain(
% 1.15/1.57 compose( a, b ) ) ), codomain( a ) ) ) ] )
% 1.15/1.57 , 0, 3, substitution( 0, [ :=( X, true ), :=( Y, domain( codomain( compose(
% 1.15/1.57 a, b ) ) ) ), :=( Z, codomain( a ) )] ), substitution( 1, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 paramod(
% 1.15/1.57 clause( 594, [ =( codomain( a ), codomain( compose( a, b ) ) ) ] )
% 1.15/1.57 , clause( 359, [ =( domain( codomain( compose( a, b ) ) ), codomain(
% 1.15/1.57 compose( a, b ) ) ) ] )
% 1.15/1.57 , 0, clause( 593, [ =( codomain( a ), domain( codomain( compose( a, b ) ) )
% 1.15/1.57 ) ] )
% 1.15/1.57 , 0, 3, substitution( 0, [] ), substitution( 1, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 resolution(
% 1.15/1.57 clause( 595, [] )
% 1.15/1.57 , clause( 591, [ ~( =( codomain( a ), codomain( compose( a, b ) ) ) ) ] )
% 1.15/1.57 , 0, clause( 594, [ =( codomain( a ), codomain( compose( a, b ) ) ) ] )
% 1.15/1.57 , 0, substitution( 0, [] ), substitution( 1, [] )).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 subsumption(
% 1.15/1.57 clause( 446, [] )
% 1.15/1.57 , clause( 595, [] )
% 1.15/1.57 , substitution( 0, [] ), permutation( 0, [] ) ).
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 end.
% 1.15/1.57
% 1.15/1.57 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 1.15/1.57
% 1.15/1.57 Memory use:
% 1.15/1.57
% 1.15/1.57 space for terms: 5721
% 1.15/1.57 space for clauses: 50343
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 clauses generated: 2333
% 1.15/1.57 clauses kept: 447
% 1.15/1.57 clauses selected: 134
% 1.15/1.57 clauses deleted: 79
% 1.15/1.57 clauses inuse deleted: 0
% 1.15/1.57
% 1.15/1.57 subsentry: 629
% 1.15/1.57 literals s-matched: 293
% 1.15/1.57 literals matched: 293
% 1.15/1.57 full subsumption: 0
% 1.15/1.57
% 1.15/1.57 checksum: -725799127
% 1.15/1.57
% 1.15/1.57
% 1.15/1.57 Bliksem ended
%------------------------------------------------------------------------------