%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : COL081-2 : TPTP v8.1.0. Released v1.2.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 : Fri Jul 15 00:12:37 EDT 2022
% Result : Unsatisfiable 3.17s 3.53s
% Output : Refutation 3.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : COL081-2 : TPTP v8.1.0. Released v1.2.0.
% 0.10/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n029.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Tue May 31 05:54:44 EDT 2022
% 0.13/0.33 % CPUTime :
% 3.17/3.53 *** allocated 10000 integers for termspace/termends
% 3.17/3.53 *** allocated 10000 integers for clauses
% 3.17/3.53 *** allocated 10000 integers for justifications
% 3.17/3.53 Bliksem 1.12
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Automatic Strategy Selection
% 3.17/3.53
% 3.17/3.53 Clauses:
% 3.17/3.53 [
% 3.17/3.53 [ =( apply( k( X ), Y ), X ) ],
% 3.17/3.53 [ =( apply( apply( apply( abstraction, X ), Y ), Z ), apply( apply( X, k(
% 3.17/3.53 Z ) ), apply( Y, Z ) ) ) ],
% 3.17/3.53 [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y ) ) ) ) ]
% 3.17/3.53 ,
% 3.17/3.53 [ =( apply( identity, X ), X ) ],
% 3.17/3.53 [ ~( =( k( k( b ) ), apply( abstraction, k( k( b ) ) ) ) ) ]
% 3.17/3.53 ] .
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 percentage equality = 1.000000, percentage horn = 1.000000
% 3.17/3.53 This is a pure equality problem
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Options Used:
% 3.17/3.53
% 3.17/3.53 useres = 1
% 3.17/3.53 useparamod = 1
% 3.17/3.53 useeqrefl = 1
% 3.17/3.53 useeqfact = 1
% 3.17/3.53 usefactor = 1
% 3.17/3.53 usesimpsplitting = 0
% 3.17/3.53 usesimpdemod = 5
% 3.17/3.53 usesimpres = 3
% 3.17/3.53
% 3.17/3.53 resimpinuse = 1000
% 3.17/3.53 resimpclauses = 20000
% 3.17/3.53 substype = eqrewr
% 3.17/3.53 backwardsubs = 1
% 3.17/3.53 selectoldest = 5
% 3.17/3.53
% 3.17/3.53 litorderings [0] = split
% 3.17/3.53 litorderings [1] = extend the termordering, first sorting on arguments
% 3.17/3.53
% 3.17/3.53 termordering = kbo
% 3.17/3.53
% 3.17/3.53 litapriori = 0
% 3.17/3.53 termapriori = 1
% 3.17/3.53 litaposteriori = 0
% 3.17/3.53 termaposteriori = 0
% 3.17/3.53 demodaposteriori = 0
% 3.17/3.53 ordereqreflfact = 0
% 3.17/3.53
% 3.17/3.53 litselect = negord
% 3.17/3.53
% 3.17/3.53 maxweight = 15
% 3.17/3.53 maxdepth = 30000
% 3.17/3.53 maxlength = 115
% 3.17/3.53 maxnrvars = 195
% 3.17/3.53 excuselevel = 1
% 3.17/3.53 increasemaxweight = 1
% 3.17/3.53
% 3.17/3.53 maxselected = 10000000
% 3.17/3.53 maxnrclauses = 10000000
% 3.17/3.53
% 3.17/3.53 showgenerated = 0
% 3.17/3.53 showkept = 0
% 3.17/3.53 showselected = 0
% 3.17/3.53 showdeleted = 0
% 3.17/3.53 showresimp = 1
% 3.17/3.53 showstatus = 2000
% 3.17/3.53
% 3.17/3.53 prologoutput = 1
% 3.17/3.53 nrgoals = 5000000
% 3.17/3.53 totalproof = 1
% 3.17/3.53
% 3.17/3.53 Symbols occurring in the translation:
% 3.17/3.53
% 3.17/3.53 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.17/3.53 . [1, 2] (w:1, o:21, a:1, s:1, b:0),
% 3.17/3.53 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 3.17/3.53 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.17/3.53 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.17/3.53 k [40, 1] (w:1, o:20, a:1, s:1, b:0),
% 3.17/3.53 apply [42, 2] (w:1, o:46, a:1, s:1, b:0),
% 3.17/3.53 abstraction [43, 0] (w:1, o:11, a:1, s:1, b:0),
% 3.17/3.53 n [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 3.17/3.53 identity [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 3.17/3.53 b [47, 0] (w:1, o:14, a:1, s:1, b:0).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Starting Search:
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 46951
% 3.17/3.53 Kept: 2100
% 3.17/3.53 Inuse: 191
% 3.17/3.53 Deleted: 94
% 3.17/3.53 Deletedinuse: 11
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Intermediate Status:
% 3.17/3.53 Generated: 106910
% 3.17/3.53 Kept: 4109
% 3.17/3.53 Inuse: 316
% 3.17/3.53 Deleted: 142
% 3.17/3.53 Deletedinuse: 11
% 3.17/3.53
% 3.17/3.53 Resimplifying inuse:
% 3.17/3.53 Done
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 Bliksems!, er is een bewijs:
% 3.17/3.53 % SZS status Unsatisfiable
% 3.17/3.53 % SZS output start Refutation
% 3.17/3.53
% 3.17/3.53 clause( 0, [ =( apply( k( X ), Y ), X ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 1, [ =( apply( apply( X, k( Z ) ), apply( Y, Z ) ), apply( apply(
% 3.17/3.53 apply( abstraction, X ), Y ), Z ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 2, [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y ) )
% 3.17/3.53 ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 4, [ ~( =( apply( abstraction, k( k( b ) ) ), k( k( b ) ) ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 5, [ ~( =( apply( apply( X, n( X, Y ) ), n( apply( X, n( X, Y ) ),
% 3.17/3.53 apply( Y, n( X, Y ) ) ) ), apply( apply( Y, n( X, Y ) ), n( apply( X, n(
% 3.17/3.53 X, Y ) ), apply( Y, n( X, Y ) ) ) ) ) ), =( X, Y ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 16, [ ~( =( apply( abstraction, X ), X ) ), ~( =( apply( X, n( k( k(
% 3.17/3.53 b ) ), X ) ), k( b ) ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 24, [ =( k( X ), Y ), ~( =( apply( Y, n( k( X ), Y ) ), X ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 42, [ =( apply( apply( apply( abstraction, k( X ) ), Z ), Y ),
% 3.17/3.53 apply( X, apply( Z, Y ) ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 156, [ ~( =( apply( abstraction, k( X ) ), k( X ) ) ), ~( =( X, k(
% 3.17/3.53 b ) ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 157, [ ~( =( apply( abstraction, k( k( X ) ) ), k( k( X ) ) ) ),
% 3.17/3.53 ~( =( b, X ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 172, [ =( Y, X ), ~( =( X, Y ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 210, [ =( apply( Y, Z ), X ), ~( =( Y, k( X ) ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 273, [ ~( =( X, k( k( Y ) ) ) ), =( apply( apply( X, Z ), T ), Y )
% 3.17/3.53 ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 4687, [ ~( =( Y, k( k( X ) ) ) ), ~( =( b, X ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 4689, [ ~( =( X, k( k( b ) ) ) ) ] )
% 3.17/3.53 .
% 3.17/3.53 clause( 4690, [] )
% 3.17/3.53 .
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 % SZS output end Refutation
% 3.17/3.53 found a proof!
% 3.17/3.53
% 3.17/3.53 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 3.17/3.53
% 3.17/3.53 initialclauses(
% 3.17/3.53 [ clause( 4692, [ =( apply( k( X ), Y ), X ) ] )
% 3.17/3.53 , clause( 4693, [ =( apply( apply( apply( abstraction, X ), Y ), Z ), apply(
% 3.17/3.53 apply( X, k( Z ) ), apply( Y, Z ) ) ) ] )
% 3.17/3.53 , clause( 4694, [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y
% 3.17/3.53 ) ) ) ) ] )
% 3.17/3.53 , clause( 4695, [ =( apply( identity, X ), X ) ] )
% 3.17/3.53 , clause( 4696, [ ~( =( k( k( b ) ), apply( abstraction, k( k( b ) ) ) ) )
% 3.17/3.53 ] )
% 3.17/3.53 ] ).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 subsumption(
% 3.17/3.53 clause( 0, [ =( apply( k( X ), Y ), X ) ] )
% 3.17/3.53 , clause( 4692, [ =( apply( k( X ), Y ), X ) ] )
% 3.17/3.53 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 3.17/3.53 )] ) ).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 eqswap(
% 3.17/3.53 clause( 4699, [ =( apply( apply( X, k( Z ) ), apply( Y, Z ) ), apply( apply(
% 3.17/3.53 apply( abstraction, X ), Y ), Z ) ) ] )
% 3.17/3.53 , clause( 4693, [ =( apply( apply( apply( abstraction, X ), Y ), Z ), apply(
% 3.17/3.53 apply( X, k( Z ) ), apply( Y, Z ) ) ) ] )
% 3.17/3.53 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 subsumption(
% 3.17/3.53 clause( 1, [ =( apply( apply( X, k( Z ) ), apply( Y, Z ) ), apply( apply(
% 3.17/3.53 apply( abstraction, X ), Y ), Z ) ) ] )
% 3.17/3.53 , clause( 4699, [ =( apply( apply( X, k( Z ) ), apply( Y, Z ) ), apply(
% 3.17/3.53 apply( apply( abstraction, X ), Y ), Z ) ) ] )
% 3.17/3.53 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 3.17/3.53 permutation( 0, [ ==>( 0, 0 )] ) ).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 subsumption(
% 3.17/3.53 clause( 2, [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y ) )
% 3.17/3.53 ) ) ] )
% 3.17/3.53 , clause( 4694, [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y
% 3.17/3.53 ) ) ) ) ] )
% 3.17/3.53 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 3.17/3.53 ), ==>( 1, 1 )] ) ).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 eqswap(
% 3.17/3.53 clause( 4711, [ ~( =( apply( abstraction, k( k( b ) ) ), k( k( b ) ) ) ) ]
% 3.17/3.53 )
% 3.17/3.53 , clause( 4696, [ ~( =( k( k( b ) ), apply( abstraction, k( k( b ) ) ) ) )
% 3.17/3.53 ] )
% 3.17/3.53 , 0, substitution( 0, [] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 subsumption(
% 3.17/3.53 clause( 4, [ ~( =( apply( abstraction, k( k( b ) ) ), k( k( b ) ) ) ) ] )
% 3.17/3.53 , clause( 4711, [ ~( =( apply( abstraction, k( k( b ) ) ), k( k( b ) ) ) )
% 3.17/3.53 ] )
% 3.17/3.53 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 eqswap(
% 3.17/3.53 clause( 4712, [ =( Y, X ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y )
% 3.17/3.53 ) ) ) ] )
% 3.17/3.53 , clause( 2, [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y )
% 3.17/3.53 ) ) ) ] )
% 3.17/3.53 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 eqswap(
% 3.17/3.53 clause( 4716, [ ~( =( apply( Y, n( X, Y ) ), apply( X, n( X, Y ) ) ) ), =(
% 3.17/3.53 X, Y ) ] )
% 3.17/3.53 , clause( 2, [ =( X, Y ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X, Y )
% 3.17/3.53 ) ) ) ] )
% 3.17/3.53 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 eqswap(
% 3.17/3.53 clause( 4717, [ =( Y, X ), ~( =( apply( Y, n( X, Y ) ), apply( X, n( X, Y )
% 3.17/3.53 ) ) ) ] )
% 3.17/3.53 , clause( 4716, [ ~( =( apply( Y, n( X, Y ) ), apply( X, n( X, Y ) ) ) ),
% 3.17/3.53 =( X, Y ) ] )
% 3.17/3.53 , 1, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 resolution(
% 3.17/3.53 clause( 4730, [ =( X, Y ), ~( =( apply( apply( Y, n( Y, X ) ), n( apply( Y
% 3.17/3.53 , n( Y, X ) ), apply( X, n( Y, X ) ) ) ), apply( apply( X, n( Y, X ) ), n(
% 3.17/3.53 apply( Y, n( Y, X ) ), apply( X, n( Y, X ) ) ) ) ) ) ] )
% 3.17/3.53 , clause( 4717, [ =( Y, X ), ~( =( apply( Y, n( X, Y ) ), apply( X, n( X, Y
% 3.17/3.53 ) ) ) ) ] )
% 3.17/3.53 , 1, clause( 4712, [ =( Y, X ), ~( =( apply( X, n( X, Y ) ), apply( Y, n( X
% 3.17/3.53 , Y ) ) ) ) ] )
% 3.17/3.53 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [ :=( X
% 3.17/3.53 , apply( Y, n( Y, X ) ) ), :=( Y, apply( X, n( Y, X ) ) )] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 eqswap(
% 3.17/3.53 clause( 4731, [ =( Y, X ), ~( =( apply( apply( Y, n( Y, X ) ), n( apply( Y
% 3.17/3.53 , n( Y, X ) ), apply( X, n( Y, X ) ) ) ), apply( apply( X, n( Y, X ) ), n(
% 3.17/3.53 apply( Y, n( Y, X ) ), apply( X, n( Y, X ) ) ) ) ) ) ] )
% 3.17/3.53 , clause( 4730, [ =( X, Y ), ~( =( apply( apply( Y, n( Y, X ) ), n( apply(
% 3.17/3.53 Y, n( Y, X ) ), apply( X, n( Y, X ) ) ) ), apply( apply( X, n( Y, X ) ),
% 3.17/3.53 n( apply( Y, n( Y, X ) ), apply( X, n( Y, X ) ) ) ) ) ) ] )
% 3.17/3.53 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 3.17/3.53
% 3.17/3.53
% 3.17/3.53 subsumption(
% 3.17/3.53 clause( 5, [ ~( =( apply( apply( X, n( X, Y ) ), n( apply( X, n( X, Y ) ),
% 3.17/3.53 apply( Y, n( X, Y ) ) ) ), apply( apply( Y, n( X, Y ) ), n( apply( X, n(
% 3.17/3.53 X, Y ) ), apply( Y, n( X, Y ) ) ) ) ) ), =( X, Y ) ] )
% 3.17/3.53 , clause( 4731, [ =( Y, X ), ~( =( apply( apply( Y, n( Y, X ) ), n( apply(
% 3.17/3.53 Y, n( Y, X ) ), apply( X, n( Y, X ) ) ) ), apply( apply( X, n( Y, X ) ),
% 3.17/3.53 n( apply( Y, n( Y, X ) ), apply( X, n( Y, X ) ) ) ) ) ) ] )
% 4.46/4.85 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 1
% 4.46/4.85 ), ==>( 1, 0 )] ) ).
% 4.46/4.85
% 4.46/4.85
% 4.46/4.85
% 4.46/4.85 ==> clause( 16, [ ~( =( apply( abstraction, X ), X ) ), ~( =( apply( X, n(
% 4.46/4.85 k( k( b ) ), X ) ), k( b ) ) ) ] )
% 4.46/4.85
% 4.46/4.85
% 4.46/4.85
% 4.46/4.85 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 4.46/4.85
% 4.46/4.85 Bliksem ended
%------------------------------------------------------------------------------