%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX190-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n026.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 : Tue May 5 06:56:45 PM UTC 2026
% Result : Unsatisfiable 5.05s 5.49s
% Output : Refutation 5.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX190-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : bliksem %s
% 0.17/0.34 % Computer : n026.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % DateTime : Tue May 5 09:56:23 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.86/1.49 *** allocated 10000 integers for termspace/termends
% 0.86/1.49 *** allocated 10000 integers for clauses
% 0.86/1.49 *** allocated 10000 integers for justifications
% 0.86/1.49 Bliksem 1.12
% 0.86/1.49
% 0.86/1.49
% 0.86/1.49 Automatic Strategy Selection
% 0.86/1.49
% 0.86/1.49 Clauses:
% 0.86/1.49 [
% 0.86/1.49 [ =( aux( X, Y, btrue ), y( n( s( s( z ) ) ), opt( X ) ) ) ],
% 0.86/1.49 [ =( aux( x( X, Y ), Z, bfalse ), opt( x( X, x( Y, Z ) ) ) ) ],
% 0.86/1.49 [ =( aux( n( X ), Y, bfalse ), x( opt( n( X ) ), opt( Y ) ) ) ],
% 0.86/1.49 [ =( aux( y( X, Y ), Z, bfalse ), x( opt( y( X, Y ) ), opt( Z ) ) ) ]
% 0.86/1.49 ,
% 0.86/1.49 [ =( aux( x2, X, bfalse ), x( opt( x2 ), opt( X ) ) ) ],
% 0.86/1.49 [ =( fail2( X, Y ), aux( X, Y, eq2( X, Y ) ) ) ],
% 0.86/1.49 [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ],
% 0.86/1.49 [ =( fail1( n( X ), x( Y, Z ) ), fail2( n( X ), x( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail1( n( X ), y( Y, Z ) ), fail2( n( X ), y( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail1( n( X ), x2 ), fail2( n( X ), x2 ) ) ],
% 0.86/1.49 [ =( fail1( x( X, Y ), Z ), fail2( x( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( fail1( y( X, Y ), Z ), fail2( y( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( fail1( x2, X ), fail2( x2, X ) ) ],
% 0.86/1.49 [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ],
% 0.86/1.49 [ =( fail( X, n( z ) ), X ) ],
% 0.86/1.49 [ =( fail( X, x( Y, Z ) ), fail1( X, x( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail( X, y( Y, Z ) ), fail1( X, y( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail( X, x2 ), fail1( X, x2 ) ) ],
% 0.86/1.49 [ =( fail4( X, Y ), y( opt( X ), opt( Y ) ) ) ],
% 0.86/1.49 [ =( fail32( n( X ), n( Y ) ), n( mulNat( X, Y ) ) ) ],
% 0.86/1.49 [ =( fail32( n( X ), x( Y, Z ) ), fail4( n( X ), x( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail32( n( X ), y( Y, Z ) ), fail4( n( X ), y( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail32( n( X ), x2 ), fail4( n( X ), x2 ) ) ],
% 0.86/1.49 [ =( fail32( y( X, Y ), Z ), opt( y( X, y( Y, Z ) ) ) ) ],
% 0.86/1.49 [ =( fail32( x( X, Y ), Z ), fail4( x( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( fail32( x2, X ), fail4( x2, X ) ) ],
% 0.86/1.49 [ =( fail22( X, n( s( s( Y ) ) ) ), fail32( X, n( s( s( Y ) ) ) ) ) ]
% 0.86/1.49 ,
% 0.86/1.49 [ =( fail22( X, n( s( z ) ) ), X ) ],
% 0.86/1.49 [ =( fail22( X, n( z ) ), fail32( X, n( z ) ) ) ],
% 0.86/1.49 [ =( fail22( X, x( Y, Z ) ), fail32( X, x( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail22( X, y( Y, Z ) ), fail32( X, y( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail22( X, x2 ), fail32( X, x2 ) ) ],
% 0.86/1.49 [ =( fail12( n( s( s( X ) ) ), Y ), fail22( n( s( s( X ) ) ), Y ) ) ]
% 0.86/1.49 ,
% 0.86/1.49 [ =( fail12( n( s( z ) ), X ), X ) ],
% 0.86/1.49 [ =( fail12( n( z ), X ), fail22( n( z ), X ) ) ],
% 0.86/1.49 [ =( fail12( x( X, Y ), Z ), fail22( x( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( fail12( y( X, Y ), Z ), fail22( y( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( fail12( x2, X ), fail22( x2, X ) ) ],
% 0.86/1.49 [ =( fail3( X, n( s( Y ) ) ), fail12( X, n( s( Y ) ) ) ) ],
% 0.86/1.49 [ =( fail3( X, n( z ) ), n( z ) ) ],
% 0.86/1.49 [ =( fail3( X, x( Y, Z ) ), fail12( X, x( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail3( X, y( Y, Z ) ), fail12( X, y( Y, Z ) ) ) ],
% 0.86/1.49 [ =( fail3( X, x2 ), fail12( X, x2 ) ) ],
% 0.86/1.49 [ =( d( n( X ) ), n( z ) ) ],
% 0.86/1.49 [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ],
% 0.86/1.49 [ =( d( y( X, Y ) ), x( y( d( X ), Y ), y( X, d( Y ) ) ) ) ],
% 0.86/1.49 [ =( d( x2 ), n( s( z ) ) ) ],
% 0.86/1.49 [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ],
% 0.86/1.49 [ =( addNat( z, X ), X ) ],
% 0.86/1.49 [ =( mulNat( s( X ), Y ), addNat( Y, mulNat( X, Y ) ) ) ],
% 0.86/1.49 [ =( mulNat( z, X ), z ) ],
% 0.86/1.49 [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) ) ],
% 0.86/1.49 [ =( opt( x( n( z ), X ) ), X ) ],
% 0.86/1.49 [ =( opt( x( x( X, Y ), Z ) ), fail( x( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( opt( x( y( X, Y ), Z ) ), fail( y( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( opt( x( x2, X ) ), fail( x2, X ) ) ],
% 0.86/1.49 [ =( opt( y( n( s( X ) ), Y ) ), fail3( n( s( X ) ), Y ) ) ],
% 0.86/1.49 [ =( opt( y( n( z ), X ) ), n( z ) ) ],
% 0.86/1.49 [ =( opt( y( x( X, Y ), Z ) ), fail3( x( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( opt( y( y( X, Y ), Z ) ), fail3( y( X, Y ), Z ) ) ],
% 0.86/1.49 [ =( opt( y( x2, X ) ), fail3( x2, X ) ) ],
% 0.86/1.49 [ =( opt( n( X ) ), n( X ) ) ],
% 0.86/1.49 [ =( opt( x2 ), x2 ) ],
% 0.86/1.49 [ =( prop4( X ), eq2( opt( d( X ) ), opt( d( opt( X ) ) ) ) ) ],
% 0.86/1.49 [ =( eq3( bfalse, btrue ), bfalse ) ],
% 0.86/1.49 [ =( eq3( btrue, bfalse ), bfalse ) ],
% 0.86/1.49 [ =( eq2( n( X ), n( Y ) ), eq( X, Y ) ) ],
% 0.86/1.49 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( x( X, Z ), x( Y, T ) ), bfalse
% 0.86/1.49 ) ],
% 0.86/1.49 [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( x( X, Z ), x( Y, T ) ), eq2( Z,
% 0.86/1.49 T ) ) ],
% 0.86/1.49 [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( y( X, Z ), y( Y, T ) ), bfalse
% 0.86/1.49 ) ],
% 0.86/1.49 [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( y( X, Z ), y( Y, T ) ), eq2( Z,
% 5.05/5.49 T ) ) ],
% 5.05/5.49 [ =( eq2( n( X ), x( Y, Z ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( n( X ), y( Y, Z ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( n( X ), x2 ), bfalse ) ],
% 5.05/5.49 [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( x( X, Y ), y( Z, T ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( x( X, Y ), x2 ), bfalse ) ],
% 5.05/5.49 [ =( eq2( y( X, Y ), n( Z ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( y( X, Y ), x( Z, T ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( y( X, Y ), x2 ), bfalse ) ],
% 5.05/5.49 [ =( eq2( x2, n( X ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( x2, x( X, Y ) ), bfalse ) ],
% 5.05/5.49 [ =( eq2( x2, y( X, Y ) ), bfalse ) ],
% 5.05/5.49 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 5.05/5.49 [ =( eq( s( X ), z ), bfalse ) ],
% 5.05/5.49 [ =( eq( z, s( X ) ), bfalse ) ],
% 5.05/5.49 [ =( eq( X, X ), btrue ) ],
% 5.05/5.49 [ =( eq2( X, X ), btrue ) ],
% 5.05/5.49 [ =( eq3( X, X ), btrue ) ],
% 5.05/5.49 [ ~( =( eq3( prop4( X ), bfalse ), btrue ) ) ]
% 5.05/5.49 ] .
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 percentage equality = 1.000000, percentage horn = 1.000000
% 5.05/5.49 This is a pure equality problem
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Options Used:
% 5.05/5.49
% 5.05/5.49 useres = 1
% 5.05/5.49 useparamod = 1
% 5.05/5.49 useeqrefl = 1
% 5.05/5.49 useeqfact = 1
% 5.05/5.49 usefactor = 1
% 5.05/5.49 usesimpsplitting = 0
% 5.05/5.49 usesimpdemod = 5
% 5.05/5.49 usesimpres = 3
% 5.05/5.49
% 5.05/5.49 resimpinuse = 1000
% 5.05/5.49 resimpclauses = 20000
% 5.05/5.49 substype = eqrewr
% 5.05/5.49 backwardsubs = 1
% 5.05/5.49 selectoldest = 5
% 5.05/5.49
% 5.05/5.49 litorderings [0] = split
% 5.05/5.49 litorderings [1] = extend the termordering, first sorting on arguments
% 5.05/5.49
% 5.05/5.49 termordering = kbo
% 5.05/5.49
% 5.05/5.49 litapriori = 0
% 5.05/5.49 termapriori = 1
% 5.05/5.49 litaposteriori = 0
% 5.05/5.49 termaposteriori = 0
% 5.05/5.49 demodaposteriori = 0
% 5.05/5.49 ordereqreflfact = 0
% 5.05/5.49
% 5.05/5.49 litselect = negord
% 5.05/5.49
% 5.05/5.49 maxweight = 15
% 5.05/5.49 maxdepth = 30000
% 5.05/5.49 maxlength = 115
% 5.05/5.49 maxnrvars = 195
% 5.05/5.49 excuselevel = 1
% 5.05/5.49 increasemaxweight = 1
% 5.05/5.49
% 5.05/5.49 maxselected = 10000000
% 5.05/5.49 maxnrclauses = 10000000
% 5.05/5.49
% 5.05/5.49 showgenerated = 0
% 5.05/5.49 showkept = 0
% 5.05/5.49 showselected = 0
% 5.05/5.49 showdeleted = 0
% 5.05/5.49 showresimp = 1
% 5.05/5.49 showstatus = 2000
% 5.05/5.49
% 5.05/5.49 prologoutput = 1
% 5.05/5.49 nrgoals = 5000000
% 5.05/5.49 totalproof = 1
% 5.05/5.49
% 5.05/5.49 Symbols occurring in the translation:
% 5.05/5.49
% 5.05/5.49 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.05/5.49 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 5.05/5.49 ! [4, 1] (w:0, o:37, a:1, s:1, b:0),
% 5.05/5.49 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.05/5.49 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.05/5.49 btrue [41, 0] (w:1, o:19, a:1, s:1, b:0),
% 5.05/5.49 aux [42, 3] (w:1, o:87, a:1, s:1, b:0),
% 5.05/5.49 z [43, 0] (w:1, o:20, a:1, s:1, b:0),
% 5.05/5.49 s [44, 1] (w:1, o:42, a:1, s:1, b:0),
% 5.05/5.49 n [45, 1] (w:1, o:43, a:1, s:1, b:0),
% 5.05/5.49 opt [46, 1] (w:1, o:44, a:1, s:1, b:0),
% 5.05/5.49 y [47, 2] (w:1, o:73, a:1, s:1, b:0),
% 5.05/5.49 x [50, 2] (w:1, o:72, a:1, s:1, b:0),
% 5.05/5.49 bfalse [51, 0] (w:1, o:29, a:1, s:1, b:0),
% 5.05/5.49 x2 [54, 0] (w:1, o:30, a:1, s:1, b:0),
% 5.05/5.49 fail2 [55, 2] (w:1, o:79, a:1, s:1, b:0),
% 5.05/5.49 eq2 [56, 2] (w:1, o:74, a:1, s:1, b:0),
% 5.05/5.49 fail1 [59, 2] (w:1, o:77, a:1, s:1, b:0),
% 5.05/5.49 addNat [60, 2] (w:1, o:80, a:1, s:1, b:0),
% 5.05/5.49 fail [61, 2] (w:1, o:81, a:1, s:1, b:0),
% 5.05/5.49 fail4 [64, 2] (w:1, o:85, a:1, s:1, b:0),
% 5.05/5.49 fail32 [67, 2] (w:1, o:83, a:1, s:1, b:0),
% 5.05/5.49 mulNat [68, 2] (w:1, o:86, a:1, s:1, b:0),
% 5.05/5.49 fail22 [72, 2] (w:1, o:82, a:1, s:1, b:0),
% 5.05/5.49 fail12 [74, 2] (w:1, o:78, a:1, s:1, b:0),
% 5.05/5.49 fail3 [76, 2] (w:1, o:84, a:1, s:1, b:0),
% 5.05/5.49 d [77, 1] (w:1, o:45, a:1, s:1, b:0),
% 5.05/5.49 prop4 [85, 1] (w:1, o:46, a:1, s:1, b:0),
% 5.05/5.49 eq3 [86, 2] (w:1, o:75, a:1, s:1, b:0),
% 5.05/5.49 eq [87, 2] (w:1, o:76, a:1, s:1, b:0).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Starting Search:
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 4887
% 5.05/5.49 Kept: 2001
% 5.05/5.49 Inuse: 343
% 5.05/5.49 Deleted: 47
% 5.05/5.49 Deletedinuse: 8
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 11033
% 5.05/5.49 Kept: 4003
% 5.05/5.49 Inuse: 583
% 5.05/5.49 Deleted: 89
% 5.05/5.49 Deletedinuse: 10
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 16631
% 5.05/5.49 Kept: 6023
% 5.05/5.49 Inuse: 772
% 5.05/5.49 Deleted: 128
% 5.05/5.49 Deletedinuse: 19
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 21750
% 5.05/5.49 Kept: 8027
% 5.05/5.49 Inuse: 915
% 5.05/5.49 Deleted: 161
% 5.05/5.49 Deletedinuse: 21
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 27997
% 5.05/5.49 Kept: 10146
% 5.05/5.49 Inuse: 1056
% 5.05/5.49 Deleted: 171
% 5.05/5.49 Deletedinuse: 21
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 32947
% 5.05/5.49 Kept: 12146
% 5.05/5.49 Inuse: 1155
% 5.05/5.49 Deleted: 180
% 5.05/5.49 Deletedinuse: 27
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 43414
% 5.05/5.49 Kept: 14153
% 5.05/5.49 Inuse: 1345
% 5.05/5.49 Deleted: 191
% 5.05/5.49 Deletedinuse: 27
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 55212
% 5.05/5.49 Kept: 16169
% 5.05/5.49 Inuse: 1527
% 5.05/5.49 Deleted: 229
% 5.05/5.49 Deletedinuse: 29
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 63927
% 5.05/5.49 Kept: 18180
% 5.05/5.49 Inuse: 1660
% 5.05/5.49 Deleted: 269
% 5.05/5.49 Deletedinuse: 30
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying clauses:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 70309
% 5.05/5.49 Kept: 20183
% 5.05/5.49 Inuse: 1800
% 5.05/5.49 Deleted: 2651
% 5.05/5.49 Deletedinuse: 30
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 80312
% 5.05/5.49 Kept: 22187
% 5.05/5.49 Inuse: 1927
% 5.05/5.49 Deleted: 2687
% 5.05/5.49 Deletedinuse: 60
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 123430
% 5.05/5.49 Kept: 24190
% 5.05/5.49 Inuse: 2134
% 5.05/5.49 Deleted: 2701
% 5.05/5.49 Deletedinuse: 61
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 133019
% 5.05/5.49 Kept: 26192
% 5.05/5.49 Inuse: 2308
% 5.05/5.49 Deleted: 2707
% 5.05/5.49 Deletedinuse: 61
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 152096
% 5.05/5.49 Kept: 28222
% 5.05/5.49 Inuse: 2440
% 5.05/5.49 Deleted: 2721
% 5.05/5.49 Deletedinuse: 63
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 195884
% 5.05/5.49 Kept: 30246
% 5.05/5.49 Inuse: 2589
% 5.05/5.49 Deleted: 2733
% 5.05/5.49 Deletedinuse: 65
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 209453
% 5.05/5.49 Kept: 32262
% 5.05/5.49 Inuse: 2715
% 5.05/5.49 Deleted: 2741
% 5.05/5.49 Deletedinuse: 65
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 224164
% 5.05/5.49 Kept: 34262
% 5.05/5.49 Inuse: 2856
% 5.05/5.49 Deleted: 2745
% 5.05/5.49 Deletedinuse: 69
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 234266
% 5.05/5.49 Kept: 36367
% 5.05/5.49 Inuse: 2947
% 5.05/5.49 Deleted: 2745
% 5.05/5.49 Deletedinuse: 69
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 246758
% 5.05/5.49 Kept: 38488
% 5.05/5.49 Inuse: 3061
% 5.05/5.49 Deleted: 2753
% 5.05/5.49 Deletedinuse: 71
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying clauses:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 261150
% 5.05/5.49 Kept: 40530
% 5.05/5.49 Inuse: 3196
% 5.05/5.49 Deleted: 5166
% 5.05/5.49 Deletedinuse: 73
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 274956
% 5.05/5.49 Kept: 42537
% 5.05/5.49 Inuse: 3328
% 5.05/5.49 Deleted: 5168
% 5.05/5.49 Deletedinuse: 75
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 291826
% 5.05/5.49 Kept: 44540
% 5.05/5.49 Inuse: 3512
% 5.05/5.49 Deleted: 5168
% 5.05/5.49 Deletedinuse: 75
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 301872
% 5.05/5.49 Kept: 46544
% 5.05/5.49 Inuse: 3625
% 5.05/5.49 Deleted: 5168
% 5.05/5.49 Deletedinuse: 75
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Intermediate Status:
% 5.05/5.49 Generated: 308206
% 5.05/5.49 Kept: 48945
% 5.05/5.49 Inuse: 3666
% 5.05/5.49 Deleted: 5172
% 5.05/5.49 Deletedinuse: 79
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49 Resimplifying inuse:
% 5.05/5.49 Done
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Bliksems!, er is een bewijs:
% 5.05/5.49 % SZS status Unsatisfiable
% 5.05/5.49 % SZS output start Refutation
% 5.05/5.49
% 5.05/5.49 clause( 6, [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 13, [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 43, [ =( d( n( X ) ), n( z ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 44, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 47, [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 48, [ =( addNat( z, X ), X ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 51, [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 52, [ =( opt( x( n( z ), X ) ), X ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 63, [ =( eq2( opt( d( X ) ), opt( d( opt( X ) ) ) ), prop4( X ) ) ]
% 5.05/5.49 )
% 5.05/5.49 .
% 5.05/5.49 clause( 74, [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 88, [ =( eq3( X, X ), btrue ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 89, [ ~( =( eq3( prop4( X ), bfalse ), btrue ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 94, [ =( d( d( x2 ) ), n( z ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 114, [ =( fail1( d( x2 ), n( X ) ), n( s( X ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 167, [ =( fail( X, d( x2 ) ), fail1( X, d( x2 ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 368, [ =( fail1( d( x2 ), d( x2 ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 436, [ =( eq2( d( x( X, Y ) ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 440, [ =( x( n( z ), d( X ) ), d( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 442, [ =( d( x( d( x2 ), Y ) ), d( x( n( X ), Y ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 512, [ =( opt( x( d( x2 ), X ) ), fail( d( x2 ), X ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 622, [ =( eq2( opt( d( x( n( z ), X ) ) ), opt( d( X ) ) ), prop4(
% 5.05/5.49 x( n( z ), X ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 3315, [ =( fail( d( x2 ), d( X ) ), opt( d( x( x2, X ) ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 9628, [ =( opt( d( x( d( x2 ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 9699, [ =( opt( d( x( n( Y ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 15382, [ =( opt( d( x( x2, x2 ) ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 16270, [ =( eq2( d( X ), opt( d( X ) ) ), prop4( x( n( z ), X ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 50264, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), bfalse ) ] )
% 5.05/5.49 .
% 5.05/5.49 clause( 50272, [] )
% 5.05/5.49 .
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 % SZS output end Refutation
% 5.05/5.49 found a proof!
% 5.05/5.49
% 5.05/5.49 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 5.05/5.49
% 5.05/5.49 initialclauses(
% 5.05/5.49 [ clause( 50274, [ =( aux( X, Y, btrue ), y( n( s( s( z ) ) ), opt( X ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 50275, [ =( aux( x( X, Y ), Z, bfalse ), opt( x( X, x( Y, Z ) ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , clause( 50276, [ =( aux( n( X ), Y, bfalse ), x( opt( n( X ) ), opt( Y )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , clause( 50277, [ =( aux( y( X, Y ), Z, bfalse ), x( opt( y( X, Y ) ), opt(
% 5.05/5.49 Z ) ) ) ] )
% 5.05/5.49 , clause( 50278, [ =( aux( x2, X, bfalse ), x( opt( x2 ), opt( X ) ) ) ] )
% 5.05/5.49 , clause( 50279, [ =( fail2( X, Y ), aux( X, Y, eq2( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50280, [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50281, [ =( fail1( n( X ), x( Y, Z ) ), fail2( n( X ), x( Y, Z )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , clause( 50282, [ =( fail1( n( X ), y( Y, Z ) ), fail2( n( X ), y( Y, Z )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , clause( 50283, [ =( fail1( n( X ), x2 ), fail2( n( X ), x2 ) ) ] )
% 5.05/5.49 , clause( 50284, [ =( fail1( x( X, Y ), Z ), fail2( x( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50285, [ =( fail1( y( X, Y ), Z ), fail2( y( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50286, [ =( fail1( x2, X ), fail2( x2, X ) ) ] )
% 5.05/5.49 , clause( 50287, [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50288, [ =( fail( X, n( z ) ), X ) ] )
% 5.05/5.49 , clause( 50289, [ =( fail( X, x( Y, Z ) ), fail1( X, x( Y, Z ) ) ) ] )
% 5.05/5.49 , clause( 50290, [ =( fail( X, y( Y, Z ) ), fail1( X, y( Y, Z ) ) ) ] )
% 5.05/5.49 , clause( 50291, [ =( fail( X, x2 ), fail1( X, x2 ) ) ] )
% 5.05/5.49 , clause( 50292, [ =( fail4( X, Y ), y( opt( X ), opt( Y ) ) ) ] )
% 5.05/5.49 , clause( 50293, [ =( fail32( n( X ), n( Y ) ), n( mulNat( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50294, [ =( fail32( n( X ), x( Y, Z ) ), fail4( n( X ), x( Y, Z )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , clause( 50295, [ =( fail32( n( X ), y( Y, Z ) ), fail4( n( X ), y( Y, Z )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , clause( 50296, [ =( fail32( n( X ), x2 ), fail4( n( X ), x2 ) ) ] )
% 5.05/5.49 , clause( 50297, [ =( fail32( y( X, Y ), Z ), opt( y( X, y( Y, Z ) ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50298, [ =( fail32( x( X, Y ), Z ), fail4( x( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50299, [ =( fail32( x2, X ), fail4( x2, X ) ) ] )
% 5.05/5.49 , clause( 50300, [ =( fail22( X, n( s( s( Y ) ) ) ), fail32( X, n( s( s( Y
% 5.05/5.49 ) ) ) ) ) ] )
% 5.05/5.49 , clause( 50301, [ =( fail22( X, n( s( z ) ) ), X ) ] )
% 5.05/5.49 , clause( 50302, [ =( fail22( X, n( z ) ), fail32( X, n( z ) ) ) ] )
% 5.05/5.49 , clause( 50303, [ =( fail22( X, x( Y, Z ) ), fail32( X, x( Y, Z ) ) ) ] )
% 5.05/5.49 , clause( 50304, [ =( fail22( X, y( Y, Z ) ), fail32( X, y( Y, Z ) ) ) ] )
% 5.05/5.49 , clause( 50305, [ =( fail22( X, x2 ), fail32( X, x2 ) ) ] )
% 5.05/5.49 , clause( 50306, [ =( fail12( n( s( s( X ) ) ), Y ), fail22( n( s( s( X ) )
% 5.05/5.49 ), Y ) ) ] )
% 5.05/5.49 , clause( 50307, [ =( fail12( n( s( z ) ), X ), X ) ] )
% 5.05/5.49 , clause( 50308, [ =( fail12( n( z ), X ), fail22( n( z ), X ) ) ] )
% 5.05/5.49 , clause( 50309, [ =( fail12( x( X, Y ), Z ), fail22( x( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50310, [ =( fail12( y( X, Y ), Z ), fail22( y( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50311, [ =( fail12( x2, X ), fail22( x2, X ) ) ] )
% 5.05/5.49 , clause( 50312, [ =( fail3( X, n( s( Y ) ) ), fail12( X, n( s( Y ) ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50313, [ =( fail3( X, n( z ) ), n( z ) ) ] )
% 5.05/5.49 , clause( 50314, [ =( fail3( X, x( Y, Z ) ), fail12( X, x( Y, Z ) ) ) ] )
% 5.05/5.49 , clause( 50315, [ =( fail3( X, y( Y, Z ) ), fail12( X, y( Y, Z ) ) ) ] )
% 5.05/5.49 , clause( 50316, [ =( fail3( X, x2 ), fail12( X, x2 ) ) ] )
% 5.05/5.49 , clause( 50317, [ =( d( n( X ) ), n( z ) ) ] )
% 5.05/5.49 , clause( 50318, [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ] )
% 5.05/5.49 , clause( 50319, [ =( d( y( X, Y ) ), x( y( d( X ), Y ), y( X, d( Y ) ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 50320, [ =( d( x2 ), n( s( z ) ) ) ] )
% 5.05/5.49 , clause( 50321, [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50322, [ =( addNat( z, X ), X ) ] )
% 5.05/5.49 , clause( 50323, [ =( mulNat( s( X ), Y ), addNat( Y, mulNat( X, Y ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50324, [ =( mulNat( z, X ), z ) ] )
% 5.05/5.49 , clause( 50325, [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 50326, [ =( opt( x( n( z ), X ) ), X ) ] )
% 5.05/5.49 , clause( 50327, [ =( opt( x( x( X, Y ), Z ) ), fail( x( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50328, [ =( opt( x( y( X, Y ), Z ) ), fail( y( X, Y ), Z ) ) ] )
% 5.05/5.49 , clause( 50329, [ =( opt( x( x2, X ) ), fail( x2, X ) ) ] )
% 5.05/5.49 , clause( 50330, [ =( opt( y( n( s( X ) ), Y ) ), fail3( n( s( X ) ), Y ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 50331, [ =( opt( y( n( z ), X ) ), n( z ) ) ] )
% 5.05/5.49 , clause( 50332, [ =( opt( y( x( X, Y ), Z ) ), fail3( x( X, Y ), Z ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50333, [ =( opt( y( y( X, Y ), Z ) ), fail3( y( X, Y ), Z ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50334, [ =( opt( y( x2, X ) ), fail3( x2, X ) ) ] )
% 5.05/5.49 , clause( 50335, [ =( opt( n( X ) ), n( X ) ) ] )
% 5.05/5.49 , clause( 50336, [ =( opt( x2 ), x2 ) ] )
% 5.05/5.49 , clause( 50337, [ =( prop4( X ), eq2( opt( d( X ) ), opt( d( opt( X ) ) )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , clause( 50338, [ =( eq3( bfalse, btrue ), bfalse ) ] )
% 5.05/5.49 , clause( 50339, [ =( eq3( btrue, bfalse ), bfalse ) ] )
% 5.05/5.49 , clause( 50340, [ =( eq2( n( X ), n( Y ) ), eq( X, Y ) ) ] )
% 5.05/5.49 , clause( 50341, [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( x( X, Z ), x( Y,
% 5.05/5.49 T ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50342, [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( x( X, Z ), x( Y, T
% 5.05/5.49 ) ), eq2( Z, T ) ) ] )
% 5.05/5.49 , clause( 50343, [ ~( =( eq2( X, Y ), bfalse ) ), =( eq2( y( X, Z ), y( Y,
% 5.05/5.49 T ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50344, [ ~( =( eq2( X, Y ), btrue ) ), =( eq2( y( X, Z ), y( Y, T
% 5.05/5.49 ) ), eq2( Z, T ) ) ] )
% 5.05/5.49 , clause( 50345, [ =( eq2( n( X ), x( Y, Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50346, [ =( eq2( n( X ), y( Y, Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50347, [ =( eq2( n( X ), x2 ), bfalse ) ] )
% 5.05/5.49 , clause( 50348, [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50349, [ =( eq2( x( X, Y ), y( Z, T ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50350, [ =( eq2( x( X, Y ), x2 ), bfalse ) ] )
% 5.05/5.49 , clause( 50351, [ =( eq2( y( X, Y ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50352, [ =( eq2( y( X, Y ), x( Z, T ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50353, [ =( eq2( y( X, Y ), x2 ), bfalse ) ] )
% 5.05/5.49 , clause( 50354, [ =( eq2( x2, n( X ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50355, [ =( eq2( x2, x( X, Y ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50356, [ =( eq2( x2, y( X, Y ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50357, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 5.05/5.49 , clause( 50358, [ =( eq( s( X ), z ), bfalse ) ] )
% 5.05/5.49 , clause( 50359, [ =( eq( z, s( X ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50360, [ =( eq( X, X ), btrue ) ] )
% 5.05/5.49 , clause( 50361, [ =( eq2( X, X ), btrue ) ] )
% 5.05/5.49 , clause( 50362, [ =( eq3( X, X ), btrue ) ] )
% 5.05/5.49 , clause( 50363, [ ~( =( eq3( prop4( X ), bfalse ), btrue ) ) ] )
% 5.05/5.49 ] ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 6, [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50280, [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 13, [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ] )
% 5.05/5.49 , clause( 50287, [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 43, [ =( d( n( X ) ), n( z ) ) ] )
% 5.05/5.49 , clause( 50317, [ =( d( n( X ) ), n( z ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 50473, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50318, [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 44, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50473, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 50520, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , clause( 50320, [ =( d( x2 ), n( s( z ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , clause( 50520, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 47, [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , clause( 50321, [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 48, [ =( addNat( z, X ), X ) ] )
% 5.05/5.49 , clause( 50322, [ =( addNat( z, X ), X ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 51, [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) ) ] )
% 5.05/5.49 , clause( 50325, [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) )
% 5.05/5.49 ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 52, [ =( opt( x( n( z ), X ) ), X ) ] )
% 5.05/5.49 , clause( 50326, [ =( opt( x( n( z ), X ) ), X ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 50786, [ =( eq2( opt( d( X ) ), opt( d( opt( X ) ) ) ), prop4( X )
% 5.05/5.49 ) ] )
% 5.05/5.49 , clause( 50337, [ =( prop4( X ), eq2( opt( d( X ) ), opt( d( opt( X ) ) )
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 63, [ =( eq2( opt( d( X ) ), opt( d( opt( X ) ) ) ), prop4( X ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 50786, [ =( eq2( opt( d( X ) ), opt( d( opt( X ) ) ) ), prop4( X
% 5.05/5.49 ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 74, [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 50348, [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 5.05/5.49 permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 88, [ =( eq3( X, X ), btrue ) ] )
% 5.05/5.49 , clause( 50362, [ =( eq3( X, X ), btrue ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 89, [ ~( =( eq3( prop4( X ), bfalse ), btrue ) ) ] )
% 5.05/5.49 , clause( 50363, [ ~( =( eq3( prop4( X ), bfalse ), btrue ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51066, [ =( n( z ), d( n( X ) ) ) ] )
% 5.05/5.49 , clause( 43, [ =( d( n( X ) ), n( z ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51067, [ =( n( z ), d( d( x2 ) ) ) ] )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51066, [ =( n( z ), d( n( X ) ) ) ] )
% 5.05/5.49 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, s( z ) )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51068, [ =( d( d( x2 ) ), n( z ) ) ] )
% 5.05/5.49 , clause( 51067, [ =( n( z ), d( d( x2 ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 94, [ =( d( d( x2 ) ), n( z ) ) ] )
% 5.05/5.49 , clause( 51068, [ =( d( d( x2 ) ), n( z ) ) ] )
% 5.05/5.49 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51070, [ =( n( addNat( X, Y ) ), fail1( n( X ), n( Y ) ) ) ] )
% 5.05/5.49 , clause( 6, [ =( fail1( n( X ), n( Y ) ), n( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51073, [ =( n( addNat( s( z ), X ) ), fail1( d( x2 ), n( X ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51070, [ =( n( addNat( X, Y ) ), fail1( n( X ), n( Y ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, s( z ) ), :=( Y, X
% 5.05/5.49 )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51075, [ =( n( s( addNat( z, X ) ) ), fail1( d( x2 ), n( X ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 47, [ =( addNat( s( X ), Y ), s( addNat( X, Y ) ) ) ] )
% 5.05/5.49 , 0, clause( 51073, [ =( n( addNat( s( z ), X ) ), fail1( d( x2 ), n( X ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , 0, 2, substitution( 0, [ :=( X, z ), :=( Y, X )] ), substitution( 1, [
% 5.05/5.49 :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51076, [ =( n( s( X ) ), fail1( d( x2 ), n( X ) ) ) ] )
% 5.05/5.49 , clause( 48, [ =( addNat( z, X ), X ) ] )
% 5.05/5.49 , 0, clause( 51075, [ =( n( s( addNat( z, X ) ) ), fail1( d( x2 ), n( X ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 5.05/5.49 ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51077, [ =( fail1( d( x2 ), n( X ) ), n( s( X ) ) ) ] )
% 5.05/5.49 , clause( 51076, [ =( n( s( X ) ), fail1( d( x2 ), n( X ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 114, [ =( fail1( d( x2 ), n( X ) ), n( s( X ) ) ) ] )
% 5.05/5.49 , clause( 51077, [ =( fail1( d( x2 ), n( X ) ), n( s( X ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51079, [ =( fail1( X, n( s( Y ) ) ), fail( X, n( s( Y ) ) ) ) ] )
% 5.05/5.49 , clause( 13, [ =( fail( X, n( s( Y ) ) ), fail1( X, n( s( Y ) ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51081, [ =( fail1( X, n( s( z ) ) ), fail( X, d( x2 ) ) ) ] )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51079, [ =( fail1( X, n( s( Y ) ) ), fail( X, n( s( Y ) ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y, z )] )
% 5.05/5.49 ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51082, [ =( fail1( X, d( x2 ) ), fail( X, d( x2 ) ) ) ] )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51081, [ =( fail1( X, n( s( z ) ) ), fail( X, d( x2 ) ) ) ] )
% 5.05/5.49 , 0, 3, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51084, [ =( fail( X, d( x2 ) ), fail1( X, d( x2 ) ) ) ] )
% 5.05/5.49 , clause( 51082, [ =( fail1( X, d( x2 ) ), fail( X, d( x2 ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 167, [ =( fail( X, d( x2 ) ), fail1( X, d( x2 ) ) ) ] )
% 5.05/5.49 , clause( 51084, [ =( fail( X, d( x2 ) ), fail1( X, d( x2 ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51087, [ =( n( s( X ) ), fail1( d( x2 ), n( X ) ) ) ] )
% 5.05/5.49 , clause( 114, [ =( fail1( d( x2 ), n( X ) ), n( s( X ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51089, [ =( n( s( s( z ) ) ), fail1( d( x2 ), d( x2 ) ) ) ] )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51087, [ =( n( s( X ) ), fail1( d( x2 ), n( X ) ) ) ] )
% 5.05/5.49 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, s( z ) )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51091, [ =( fail1( d( x2 ), d( x2 ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , clause( 51089, [ =( n( s( s( z ) ) ), fail1( d( x2 ), d( x2 ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 368, [ =( fail1( d( x2 ), d( x2 ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , clause( 51091, [ =( fail1( d( x2 ), d( x2 ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51093, [ =( bfalse, eq2( x( X, Y ), n( Z ) ) ) ] )
% 5.05/5.49 , clause( 74, [ =( eq2( x( X, Y ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51094, [ =( bfalse, eq2( d( x( X, Y ) ), n( Z ) ) ) ] )
% 5.05/5.49 , clause( 44, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , 0, clause( 51093, [ =( bfalse, eq2( x( X, Y ), n( Z ) ) ) ] )
% 5.05/5.49 , 0, 3, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 5.05/5.49 :=( X, d( X ) ), :=( Y, d( Y ) ), :=( Z, Z )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51095, [ =( eq2( d( x( X, Y ) ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 51094, [ =( bfalse, eq2( d( x( X, Y ) ), n( Z ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 436, [ =( eq2( d( x( X, Y ) ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , clause( 51095, [ =( eq2( d( x( X, Y ) ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 5.05/5.49 permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51097, [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ] )
% 5.05/5.49 , clause( 44, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51098, [ =( d( x( d( x2 ), X ) ), x( n( z ), d( X ) ) ) ] )
% 5.05/5.49 , clause( 94, [ =( d( d( x2 ) ), n( z ) ) ] )
% 5.05/5.49 , 0, clause( 51097, [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ] )
% 5.05/5.49 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, d( x2 ) ), :=( Y,
% 5.05/5.49 X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51100, [ =( x( n( z ), d( X ) ), d( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , clause( 51098, [ =( d( x( d( x2 ), X ) ), x( n( z ), d( X ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 440, [ =( x( n( z ), d( X ) ), d( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , clause( 51100, [ =( x( n( z ), d( X ) ), d( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51103, [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ] )
% 5.05/5.49 , clause( 44, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51105, [ =( d( x( n( X ), Y ) ), x( n( z ), d( Y ) ) ) ] )
% 5.05/5.49 , clause( 43, [ =( d( n( X ) ), n( z ) ) ] )
% 5.05/5.49 , 0, clause( 51103, [ =( d( x( X, Y ) ), x( d( X ), d( Y ) ) ) ] )
% 5.05/5.49 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, n( X )
% 5.05/5.49 ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51107, [ =( d( x( n( X ), Y ) ), d( x( d( x2 ), Y ) ) ) ] )
% 5.05/5.49 , clause( 440, [ =( x( n( z ), d( X ) ), d( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , 0, clause( 51105, [ =( d( x( n( X ), Y ) ), x( n( z ), d( Y ) ) ) ] )
% 5.05/5.49 , 0, 6, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 5.05/5.49 :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51108, [ =( d( x( d( x2 ), Y ) ), d( x( n( X ), Y ) ) ) ] )
% 5.05/5.49 , clause( 51107, [ =( d( x( n( X ), Y ) ), d( x( d( x2 ), Y ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 442, [ =( d( x( d( x2 ), Y ) ), d( x( n( X ), Y ) ) ) ] )
% 5.05/5.49 , clause( 51108, [ =( d( x( d( x2 ), Y ) ), d( x( n( X ), Y ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51110, [ =( fail( n( s( X ) ), Y ), opt( x( n( s( X ) ), Y ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 51, [ =( opt( x( n( s( X ) ), Y ) ), fail( n( s( X ) ), Y ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51112, [ =( fail( n( s( z ) ), X ), opt( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51110, [ =( fail( n( s( X ) ), Y ), opt( x( n( s( X ) ), Y ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, z ), :=( Y, X )] )
% 5.05/5.49 ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51113, [ =( fail( d( x2 ), X ), opt( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , clause( 46, [ =( n( s( z ) ), d( x2 ) ) ] )
% 5.05/5.49 , 0, clause( 51112, [ =( fail( n( s( z ) ), X ), opt( x( d( x2 ), X ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , 0, 2, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51115, [ =( opt( x( d( x2 ), X ) ), fail( d( x2 ), X ) ) ] )
% 5.05/5.49 , clause( 51113, [ =( fail( d( x2 ), X ), opt( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 512, [ =( opt( x( d( x2 ), X ) ), fail( d( x2 ), X ) ) ] )
% 5.05/5.49 , clause( 51115, [ =( opt( x( d( x2 ), X ) ), fail( d( x2 ), X ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51118, [ =( prop4( X ), eq2( opt( d( X ) ), opt( d( opt( X ) ) ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , clause( 63, [ =( eq2( opt( d( X ) ), opt( d( opt( X ) ) ) ), prop4( X ) )
% 5.05/5.49 ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51119, [ =( prop4( x( n( z ), X ) ), eq2( opt( d( x( n( z ), X ) )
% 5.05/5.49 ), opt( d( X ) ) ) ) ] )
% 5.05/5.49 , clause( 52, [ =( opt( x( n( z ), X ) ), X ) ] )
% 5.05/5.49 , 0, clause( 51118, [ =( prop4( X ), eq2( opt( d( X ) ), opt( d( opt( X ) )
% 5.05/5.49 ) ) ) ] )
% 5.05/5.49 , 0, 15, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, x( n(
% 5.05/5.49 z ), X ) )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51120, [ =( eq2( opt( d( x( n( z ), X ) ) ), opt( d( X ) ) ), prop4(
% 5.05/5.49 x( n( z ), X ) ) ) ] )
% 5.05/5.49 , clause( 51119, [ =( prop4( x( n( z ), X ) ), eq2( opt( d( x( n( z ), X )
% 5.05/5.49 ) ), opt( d( X ) ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 622, [ =( eq2( opt( d( x( n( z ), X ) ) ), opt( d( X ) ) ), prop4(
% 5.05/5.49 x( n( z ), X ) ) ) ] )
% 5.05/5.49 , clause( 51120, [ =( eq2( opt( d( x( n( z ), X ) ) ), opt( d( X ) ) ),
% 5.05/5.49 prop4( x( n( z ), X ) ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51122, [ =( fail( d( x2 ), X ), opt( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , clause( 512, [ =( opt( x( d( x2 ), X ) ), fail( d( x2 ), X ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51123, [ =( fail( d( x2 ), d( X ) ), opt( d( x( x2, X ) ) ) ) ] )
% 5.05/5.49 , clause( 44, [ =( x( d( X ), d( Y ) ), d( x( X, Y ) ) ) ] )
% 5.05/5.49 , 0, clause( 51122, [ =( fail( d( x2 ), X ), opt( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , 0, 7, substitution( 0, [ :=( X, x2 ), :=( Y, X )] ), substitution( 1, [
% 5.05/5.49 :=( X, d( X ) )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 3315, [ =( fail( d( x2 ), d( X ) ), opt( d( x( x2, X ) ) ) ) ] )
% 5.05/5.49 , clause( 51123, [ =( fail( d( x2 ), d( X ) ), opt( d( x( x2, X ) ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51126, [ =( X, opt( x( n( z ), X ) ) ) ] )
% 5.05/5.49 , clause( 52, [ =( opt( x( n( z ), X ) ), X ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51127, [ =( d( X ), opt( d( x( d( x2 ), X ) ) ) ) ] )
% 5.05/5.49 , clause( 440, [ =( x( n( z ), d( X ) ), d( x( d( x2 ), X ) ) ) ] )
% 5.05/5.49 , 0, clause( 51126, [ =( X, opt( x( n( z ), X ) ) ) ] )
% 5.05/5.49 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, d( X )
% 5.05/5.49 )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51128, [ =( opt( d( x( d( x2 ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , clause( 51127, [ =( d( X ), opt( d( x( d( x2 ), X ) ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 9628, [ =( opt( d( x( d( x2 ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , clause( 51128, [ =( opt( d( x( d( x2 ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51130, [ =( d( X ), opt( d( x( d( x2 ), X ) ) ) ) ] )
% 5.05/5.49 , clause( 9628, [ =( opt( d( x( d( x2 ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51136, [ =( d( X ), opt( d( x( n( Y ), X ) ) ) ) ] )
% 5.05/5.49 , clause( 442, [ =( d( x( d( x2 ), Y ) ), d( x( n( X ), Y ) ) ) ] )
% 5.05/5.49 , 0, clause( 51130, [ =( d( X ), opt( d( x( d( x2 ), X ) ) ) ) ] )
% 5.05/5.49 , 0, 4, substitution( 0, [ :=( X, Y ), :=( Y, X )] ), substitution( 1, [
% 5.05/5.49 :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51140, [ =( opt( d( x( n( Y ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , clause( 51136, [ =( d( X ), opt( d( x( n( Y ), X ) ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 9699, [ =( opt( d( x( n( Y ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , clause( 51140, [ =( opt( d( x( n( Y ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 5.05/5.49 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51141, [ =( opt( d( x( x2, X ) ) ), fail( d( x2 ), d( X ) ) ) ] )
% 5.05/5.49 , clause( 3315, [ =( fail( d( x2 ), d( X ) ), opt( d( x( x2, X ) ) ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51144, [ =( opt( d( x( x2, x2 ) ) ), fail1( d( x2 ), d( x2 ) ) ) ]
% 5.05/5.49 )
% 5.05/5.49 , clause( 167, [ =( fail( X, d( x2 ) ), fail1( X, d( x2 ) ) ) ] )
% 5.05/5.49 , 0, clause( 51141, [ =( opt( d( x( x2, X ) ) ), fail( d( x2 ), d( X ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , 0, 6, substitution( 0, [ :=( X, d( x2 ) )] ), substitution( 1, [ :=( X,
% 5.05/5.49 x2 )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51145, [ =( opt( d( x( x2, x2 ) ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , clause( 368, [ =( fail1( d( x2 ), d( x2 ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , 0, clause( 51144, [ =( opt( d( x( x2, x2 ) ) ), fail1( d( x2 ), d( x2 ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 15382, [ =( opt( d( x( x2, x2 ) ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , clause( 51145, [ =( opt( d( x( x2, x2 ) ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51149, [ =( eq2( d( X ), opt( d( X ) ) ), prop4( x( n( z ), X ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 9699, [ =( opt( d( x( n( Y ), X ) ) ), d( X ) ) ] )
% 5.05/5.49 , 0, clause( 622, [ =( eq2( opt( d( x( n( z ), X ) ) ), opt( d( X ) ) ),
% 5.05/5.49 prop4( x( n( z ), X ) ) ) ] )
% 5.05/5.49 , 0, 2, substitution( 0, [ :=( X, X ), :=( Y, z )] ), substitution( 1, [
% 5.05/5.49 :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 16270, [ =( eq2( d( X ), opt( d( X ) ) ), prop4( x( n( z ), X ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 51149, [ =( eq2( d( X ), opt( d( X ) ) ), prop4( x( n( z ), X ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51152, [ =( prop4( x( n( z ), X ) ), eq2( d( X ), opt( d( X ) ) ) )
% 5.05/5.49 ] )
% 5.05/5.49 , clause( 16270, [ =( eq2( d( X ), opt( d( X ) ) ), prop4( x( n( z ), X ) )
% 5.05/5.49 ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51154, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), eq2( d( x( x2, x2 )
% 5.05/5.49 ), n( s( s( z ) ) ) ) ) ] )
% 5.05/5.49 , clause( 15382, [ =( opt( d( x( x2, x2 ) ) ), n( s( s( z ) ) ) ) ] )
% 5.05/5.49 , 0, clause( 51152, [ =( prop4( x( n( z ), X ) ), eq2( d( X ), opt( d( X )
% 5.05/5.49 ) ) ) ] )
% 5.05/5.49 , 0, 13, substitution( 0, [] ), substitution( 1, [ :=( X, x( x2, x2 ) )] )
% 5.05/5.49 ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51155, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), bfalse ) ] )
% 5.05/5.49 , clause( 436, [ =( eq2( d( x( X, Y ) ), n( Z ) ), bfalse ) ] )
% 5.05/5.49 , 0, clause( 51154, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), eq2( d( x( x2,
% 5.05/5.49 x2 ) ), n( s( s( z ) ) ) ) ) ] )
% 5.05/5.49 , 0, 8, substitution( 0, [ :=( X, x2 ), :=( Y, x2 ), :=( Z, s( s( z ) ) )] )
% 5.05/5.49 , substitution( 1, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 50264, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), bfalse ) ] )
% 5.05/5.49 , clause( 51155, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), bfalse ) ] )
% 5.05/5.49 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqswap(
% 5.05/5.49 clause( 51158, [ ~( =( btrue, eq3( prop4( X ), bfalse ) ) ) ] )
% 5.05/5.49 , clause( 89, [ ~( =( eq3( prop4( X ), bfalse ), btrue ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [ :=( X, X )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51160, [ ~( =( btrue, eq3( bfalse, bfalse ) ) ) ] )
% 5.05/5.49 , clause( 50264, [ =( prop4( x( n( z ), x( x2, x2 ) ) ), bfalse ) ] )
% 5.05/5.49 , 0, clause( 51158, [ ~( =( btrue, eq3( prop4( X ), bfalse ) ) ) ] )
% 5.05/5.49 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, x( n( z ), x( x2,
% 5.05/5.49 x2 ) ) )] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 paramod(
% 5.05/5.49 clause( 51161, [ ~( =( btrue, btrue ) ) ] )
% 5.05/5.49 , clause( 88, [ =( eq3( X, X ), btrue ) ] )
% 5.05/5.49 , 0, clause( 51160, [ ~( =( btrue, eq3( bfalse, bfalse ) ) ) ] )
% 5.05/5.49 , 0, 3, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 eqrefl(
% 5.05/5.49 clause( 51162, [] )
% 5.05/5.49 , clause( 51161, [ ~( =( btrue, btrue ) ) ] )
% 5.05/5.49 , 0, substitution( 0, [] )).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 subsumption(
% 5.05/5.49 clause( 50272, [] )
% 5.05/5.49 , clause( 51162, [] )
% 5.05/5.49 , substitution( 0, [] ), permutation( 0, [] ) ).
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 end.
% 5.05/5.49
% 5.05/5.49 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 5.05/5.49
% 5.05/5.49 Memory use:
% 5.05/5.49
% 5.05/5.49 space for terms: 694928
% 5.05/5.49 space for clauses: 5216754
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 clauses generated: 319579
% 5.05/5.49 clauses kept: 50273
% 5.05/5.49 clauses selected: 3795
% 5.05/5.49 clauses deleted: 5177
% 5.05/5.49 clauses inuse deleted: 79
% 5.05/5.49
% 5.05/5.49 subsentry: 30054
% 5.05/5.49 literals s-matched: 27539
% 5.05/5.49 literals matched: 27537
% 5.05/5.49 full subsumption: 103
% 5.05/5.49
% 5.05/5.49 checksum: -1834993217
% 5.05/5.49
% 5.05/5.49
% 5.05/5.49 Bliksem ended
%------------------------------------------------------------------------------