%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX217-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:49 PM UTC 2026
% Result : Unsatisfiable 8.54s 8.93s
% Output : Refutation 8.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.16/0.33 % Computer : n026.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % DateTime : Tue May 5 12:16:08 EDT 2026
% 0.16/0.33 % CPUTime :
% 8.54/8.93 *** allocated 10000 integers for termspace/termends
% 8.54/8.93 *** allocated 10000 integers for clauses
% 8.54/8.93 *** allocated 10000 integers for justifications
% 8.54/8.93 Bliksem 1.12
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Automatic Strategy Selection
% 8.54/8.93
% 8.54/8.93 Clauses:
% 8.54/8.93 [
% 8.54/8.93 [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) ) ) ],
% 8.54/8.93 [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) ) ) ) ],
% 8.54/8.93 [ =( notb( btrue ), bfalse ) ],
% 8.54/8.93 [ =( notb( bfalse ), btrue ) ],
% 8.54/8.93 [ =( half( zero ), zero ) ],
% 8.54/8.93 [ =( half( suc( zero ) ), zero ) ],
% 8.54/8.93 [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ],
% 8.54/8.93 [ =( evenNat( zero ), btrue ) ],
% 8.54/8.93 [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ],
% 8.54/8.93 [ =( shw( zero ), nil ) ],
% 8.54/8.93 [ =( shw( suc( X ) ), aux( X, evenNat( suc( X ) ) ) ) ],
% 8.54/8.93 [ =( append( nil, X ), X ) ],
% 8.54/8.93 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 8.54/8.93 [ =( addNat( zero, X ), X ) ],
% 8.54/8.93 [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ],
% 8.54/8.93 [ =( double( X ), addNat( X, X ) ) ],
% 8.54/8.93 [ =( rd( nil ), zero ) ],
% 8.54/8.93 [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ],
% 8.54/8.93 [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ],
% 8.54/8.93 [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ],
% 8.54/8.93 [ =( 'sat_comm'( X, Y ), eq( x( X, Y ), x( Y, X ) ) ) ],
% 8.54/8.93 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 8.54/8.93 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 8.54/8.93 [ =( eq3( i, o ), bfalse ) ],
% 8.54/8.93 [ =( eq3( o, i ), bfalse ) ],
% 8.54/8.93 [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ],
% 8.54/8.93 [ =( eq( zero, suc( X ) ), bfalse ) ],
% 8.54/8.93 [ =( eq( suc( X ), zero ), bfalse ) ],
% 8.54/8.93 [ =( eq( X, X ), btrue ) ],
% 8.54/8.93 [ =( eq2( X, X ), btrue ) ],
% 8.54/8.93 [ =( eq3( X, X ), btrue ) ],
% 8.54/8.93 [ ~( =( eq2( 'sat_comm'( X, Y ), bfalse ), btrue ) ) ]
% 8.54/8.93 ] .
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 percentage equality = 1.000000, percentage horn = 1.000000
% 8.54/8.93 This is a pure equality problem
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Options Used:
% 8.54/8.93
% 8.54/8.93 useres = 1
% 8.54/8.93 useparamod = 1
% 8.54/8.93 useeqrefl = 1
% 8.54/8.93 useeqfact = 1
% 8.54/8.93 usefactor = 1
% 8.54/8.93 usesimpsplitting = 0
% 8.54/8.93 usesimpdemod = 5
% 8.54/8.93 usesimpres = 3
% 8.54/8.93
% 8.54/8.93 resimpinuse = 1000
% 8.54/8.93 resimpclauses = 20000
% 8.54/8.93 substype = eqrewr
% 8.54/8.93 backwardsubs = 1
% 8.54/8.93 selectoldest = 5
% 8.54/8.93
% 8.54/8.93 litorderings [0] = split
% 8.54/8.93 litorderings [1] = extend the termordering, first sorting on arguments
% 8.54/8.93
% 8.54/8.93 termordering = kbo
% 8.54/8.93
% 8.54/8.93 litapriori = 0
% 8.54/8.93 termapriori = 1
% 8.54/8.93 litaposteriori = 0
% 8.54/8.93 termaposteriori = 0
% 8.54/8.93 demodaposteriori = 0
% 8.54/8.93 ordereqreflfact = 0
% 8.54/8.93
% 8.54/8.93 litselect = negord
% 8.54/8.93
% 8.54/8.93 maxweight = 15
% 8.54/8.93 maxdepth = 30000
% 8.54/8.93 maxlength = 115
% 8.54/8.93 maxnrvars = 195
% 8.54/8.93 excuselevel = 1
% 8.54/8.93 increasemaxweight = 1
% 8.54/8.93
% 8.54/8.93 maxselected = 10000000
% 8.54/8.93 maxnrclauses = 10000000
% 8.54/8.93
% 8.54/8.93 showgenerated = 0
% 8.54/8.93 showkept = 0
% 8.54/8.93 showselected = 0
% 8.54/8.93 showdeleted = 0
% 8.54/8.93 showresimp = 1
% 8.54/8.93 showstatus = 2000
% 8.54/8.93
% 8.54/8.93 prologoutput = 1
% 8.54/8.93 nrgoals = 5000000
% 8.54/8.93 totalproof = 1
% 8.54/8.93
% 8.54/8.93 Symbols occurring in the translation:
% 8.54/8.93
% 8.54/8.93 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 8.54/8.93 . [1, 2] (w:1, o:32, a:1, s:1, b:0),
% 8.54/8.93 ! [4, 1] (w:0, o:20, a:1, s:1, b:0),
% 8.54/8.93 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.54/8.93 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 8.54/8.93 btrue [40, 0] (w:1, o:14, a:1, s:1, b:0),
% 8.54/8.93 aux [41, 2] (w:1, o:57, a:1, s:1, b:0),
% 8.54/8.93 o [42, 0] (w:1, o:8, a:1, s:1, b:0),
% 8.54/8.93 suc [43, 1] (w:1, o:26, a:1, s:1, b:0),
% 8.54/8.93 half [44, 1] (w:1, o:27, a:1, s:1, b:0),
% 8.54/8.93 shw [45, 1] (w:1, o:28, a:1, s:1, b:0),
% 8.54/8.93 cons [46, 2] (w:1, o:58, a:1, s:1, b:0),
% 8.54/8.93 bfalse [47, 0] (w:1, o:15, a:1, s:1, b:0),
% 8.54/8.93 i [48, 0] (w:1, o:16, a:1, s:1, b:0),
% 8.54/8.93 notb [49, 1] (w:1, o:29, a:1, s:1, b:0),
% 8.54/8.93 zero [50, 0] (w:1, o:17, a:1, s:1, b:0),
% 8.54/8.93 evenNat [52, 1] (w:1, o:31, a:1, s:1, b:0),
% 8.54/8.93 nil [53, 0] (w:1, o:7, a:1, s:1, b:0),
% 8.54/8.93 append [54, 2] (w:1, o:59, a:1, s:1, b:0),
% 8.54/8.93 addNat [57, 2] (w:1, o:60, a:1, s:1, b:0),
% 8.54/8.93 double [59, 1] (w:1, o:30, a:1, s:1, b:0),
% 8.54/8.93 rd [60, 1] (w:1, o:25, a:1, s:1, b:0),
% 8.54/8.93 x [61, 2] (w:1, o:61, a:1, s:1, b:0),
% 8.54/8.93 'sat_comm' [62, 2] (w:1, o:62, a:1, s:1, b:0),
% 8.54/8.93 eq [63, 2] (w:1, o:63, a:1, s:1, b:0),
% 8.54/8.93 eq2 [64, 2] (w:1, o:64, a:1, s:1, b:0),
% 8.54/8.93 eq3 [65, 2] (w:1, o:65, a:1, s:1, b:0).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Starting Search:
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 8295
% 8.54/8.93 Kept: 2022
% 8.54/8.93 Inuse: 523
% 8.54/8.93 Deleted: 71
% 8.54/8.93 Deletedinuse: 3
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Failed to find proof!
% 8.54/8.93 maxweight = 15
% 8.54/8.93 maxnrclauses = 10000000
% 8.54/8.93 Generated: 47102
% 8.54/8.93 Kept: 2999
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 The strategy used was not complete!
% 8.54/8.93
% 8.54/8.93 Increased maxweight to 16
% 8.54/8.93
% 8.54/8.93 Starting Search:
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 6298
% 8.54/8.93 Kept: 2002
% 8.54/8.93 Inuse: 407
% 8.54/8.93 Deleted: 49
% 8.54/8.93 Deletedinuse: 7
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 12751
% 8.54/8.93 Kept: 4010
% 8.54/8.93 Inuse: 677
% 8.54/8.93 Deleted: 107
% 8.54/8.93 Deletedinuse: 9
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 29276
% 8.54/8.93 Kept: 6010
% 8.54/8.93 Inuse: 1298
% 8.54/8.93 Deleted: 281
% 8.54/8.93 Deletedinuse: 11
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 57915
% 8.54/8.93 Kept: 8011
% 8.54/8.93 Inuse: 2324
% 8.54/8.93 Deleted: 611
% 8.54/8.93 Deletedinuse: 14
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Failed to find proof!
% 8.54/8.93 maxweight = 16
% 8.54/8.93 maxnrclauses = 10000000
% 8.54/8.93 Generated: 200851
% 8.54/8.93 Kept: 9587
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 The strategy used was not complete!
% 8.54/8.93
% 8.54/8.93 Increased maxweight to 17
% 8.54/8.93
% 8.54/8.93 Starting Search:
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 6553
% 8.54/8.93 Kept: 2017
% 8.54/8.93 Inuse: 392
% 8.54/8.93 Deleted: 33
% 8.54/8.93 Deletedinuse: 5
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 11663
% 8.54/8.93 Kept: 4034
% 8.54/8.93 Inuse: 578
% 8.54/8.93 Deleted: 112
% 8.54/8.93 Deletedinuse: 25
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Intermediate Status:
% 8.54/8.93 Generated: 17730
% 8.54/8.93 Kept: 6036
% 8.54/8.93 Inuse: 843
% 8.54/8.93 Deleted: 177
% 8.54/8.93 Deletedinuse: 27
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93 Resimplifying inuse:
% 8.54/8.93 Done
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 Bliksems!, er is een bewijs:
% 8.54/8.93 % SZS status Unsatisfiable
% 8.54/8.93 % SZS output start Refutation
% 8.54/8.93
% 8.54/8.93 clause( 0, [ =( cons( o, shw( half( suc( X ) ) ) ), aux( X, btrue ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 1, [ =( cons( i, shw( half( suc( X ) ) ) ), aux( X, bfalse ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 2, [ =( notb( btrue ), bfalse ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 3, [ =( notb( bfalse ), btrue ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 4, [ =( half( zero ), zero ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 5, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 6, [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 7, [ =( evenNat( zero ), btrue ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 8, [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 9, [ =( shw( zero ), nil ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 10, [ =( aux( X, notb( evenNat( X ) ) ), shw( suc( X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 11, [ =( append( nil, X ), X ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 12, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 .
% 8.54/8.93 clause( 13, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 14, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 15, [ =( addNat( X, X ), double( X ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 16, [ =( rd( nil ), zero ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 18, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 19, [ =( rd( append( shw( X ), shw( Y ) ) ), x( X, Y ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 20, [ =( eq( x( X, Y ), x( Y, X ) ), 'sat_comm'( X, Y ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 27, [ =( eq( suc( X ), zero ), bfalse ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 29, [ =( eq2( X, X ), btrue ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 31, [ ~( =( eq2( 'sat_comm'( X, Y ), bfalse ), btrue ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 32, [ =( cons( i, nil ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 33, [ =( cons( o, nil ), aux( zero, btrue ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 34, [ =( double( zero ), zero ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 35, [ =( cons( i, shw( suc( half( X ) ) ) ), aux( suc( X ), bfalse
% 8.54/8.93 ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 36, [ =( cons( o, shw( suc( half( X ) ) ) ), aux( suc( X ), btrue )
% 8.54/8.93 ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 37, [ =( rd( aux( zero, btrue ) ), zero ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 39, [ =( aux( suc( X ), notb( notb( evenNat( X ) ) ) ), shw( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 40, [ =( aux( zero, bfalse ), shw( suc( zero ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 41, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 44, [ =( suc( suc( addNat( X, suc( suc( X ) ) ) ) ), double( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 51, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 55, [ =( append( shw( suc( zero ) ), X ), cons( i, X ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 66, [ =( suc( addNat( double( rd( X ) ), rd( cons( i, X ) ) ) ),
% 8.54/8.93 double( rd( cons( i, X ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 70, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( zero ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 78, [ =( rd( shw( suc( zero ) ) ), suc( zero ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 79, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( suc( suc( zero )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 91, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 96, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 97, [ =( aux( suc( suc( zero ) ), bfalse ), aux( suc( zero ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 98, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc( suc(
% 8.54/8.93 suc( zero ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 104, [ =( cons( o, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 105, [ =( aux( suc( suc( zero ) ), btrue ), aux( suc( zero ), btrue
% 8.54/8.93 ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 123, [ =( aux( suc( zero ), btrue ), shw( suc( suc( zero ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 .
% 8.54/8.93 clause( 138, [ =( aux( suc( suc( zero ) ), btrue ), shw( suc( suc( zero ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 176, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 184, [ =( eq( double( suc( suc( zero ) ) ), suc( X ) ), eq( suc(
% 8.54/8.93 suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 185, [ =( eq( suc( X ), double( suc( suc( zero ) ) ) ), eq( X, suc(
% 8.54/8.93 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 317, [ =( cons( o, shw( suc( zero ) ) ), shw( suc( suc( zero ) ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 318, [ =( append( shw( suc( suc( zero ) ) ), X ), cons( o, cons( i
% 8.54/8.93 , X ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 319, [ =( rd( shw( suc( suc( zero ) ) ) ), suc( suc( zero ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 .
% 8.54/8.93 clause( 324, [ =( x( suc( zero ), suc( suc( zero ) ) ), suc( double( suc(
% 8.54/8.93 suc( zero ) ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 325, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( zero ), bfalse )
% 8.54/8.93 ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 326, [ =( x( suc( zero ), suc( zero ) ), rd( aux( suc( zero ),
% 8.54/8.93 bfalse ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 342, [ =( suc( suc( double( suc( suc( zero ) ) ) ) ), double( suc(
% 8.54/8.93 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 348, [ =( rd( aux( suc( zero ), bfalse ) ), suc( suc( suc( zero ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 498, [ =( x( suc( suc( zero ) ), X ), double( x( suc( zero ), X ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 501, [ =( eq( double( x( suc( zero ), X ) ), x( X, suc( suc( zero )
% 8.54/8.93 ) ) ), 'sat_comm'( suc( suc( zero ) ), X ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 523, [ =( eq( double( suc( suc( suc( zero ) ) ) ), suc( X ) ), eq(
% 8.54/8.93 suc( double( suc( suc( zero ) ) ) ), X ) ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 1002, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero ) ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 7495, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), bfalse )
% 8.54/8.93 ] )
% 8.54/8.93 .
% 8.54/8.93 clause( 7496, [] )
% 8.54/8.93 .
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 % SZS output end Refutation
% 8.54/8.93 found a proof!
% 8.54/8.93
% 8.54/8.93 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 8.54/8.93
% 8.54/8.93 initialclauses(
% 8.54/8.93 [ clause( 7498, [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , clause( 7499, [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , clause( 7500, [ =( notb( btrue ), bfalse ) ] )
% 8.54/8.93 , clause( 7501, [ =( notb( bfalse ), btrue ) ] )
% 8.54/8.93 , clause( 7502, [ =( half( zero ), zero ) ] )
% 8.54/8.93 , clause( 7503, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , clause( 7504, [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ] )
% 8.54/8.93 , clause( 7505, [ =( evenNat( zero ), btrue ) ] )
% 8.54/8.93 , clause( 7506, [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ] )
% 8.54/8.93 , clause( 7507, [ =( shw( zero ), nil ) ] )
% 8.54/8.93 , clause( 7508, [ =( shw( suc( X ) ), aux( X, evenNat( suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 7509, [ =( append( nil, X ), X ) ] )
% 8.54/8.93 , clause( 7510, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , clause( 7511, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 , clause( 7512, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.93 , clause( 7513, [ =( double( X ), addNat( X, X ) ) ] )
% 8.54/8.93 , clause( 7514, [ =( rd( nil ), zero ) ] )
% 8.54/8.93 , clause( 7515, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , clause( 7516, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.93 , clause( 7517, [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ] )
% 8.54/8.93 , clause( 7518, [ =( 'sat_comm'( X, Y ), eq( x( X, Y ), x( Y, X ) ) ) ] )
% 8.54/8.93 , clause( 7519, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 8.54/8.93 , clause( 7520, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 8.54/8.93 , clause( 7521, [ =( eq3( i, o ), bfalse ) ] )
% 8.54/8.93 , clause( 7522, [ =( eq3( o, i ), bfalse ) ] )
% 8.54/8.93 , clause( 7523, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.93 , clause( 7524, [ =( eq( zero, suc( X ) ), bfalse ) ] )
% 8.54/8.93 , clause( 7525, [ =( eq( suc( X ), zero ), bfalse ) ] )
% 8.54/8.93 , clause( 7526, [ =( eq( X, X ), btrue ) ] )
% 8.54/8.93 , clause( 7527, [ =( eq2( X, X ), btrue ) ] )
% 8.54/8.93 , clause( 7528, [ =( eq3( X, X ), btrue ) ] )
% 8.54/8.93 , clause( 7529, [ ~( =( eq2( 'sat_comm'( X, Y ), bfalse ), btrue ) ) ] )
% 8.54/8.93 ] ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7530, [ =( cons( o, shw( half( suc( X ) ) ) ), aux( X, btrue ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 7498, [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 0, [ =( cons( o, shw( half( suc( X ) ) ) ), aux( X, btrue ) ) ] )
% 8.54/8.93 , clause( 7530, [ =( cons( o, shw( half( suc( X ) ) ) ), aux( X, btrue ) )
% 8.54/8.93 ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7532, [ =( cons( i, shw( half( suc( X ) ) ) ), aux( X, bfalse ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 7499, [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 1, [ =( cons( i, shw( half( suc( X ) ) ) ), aux( X, bfalse ) ) ] )
% 8.54/8.93 , clause( 7532, [ =( cons( i, shw( half( suc( X ) ) ) ), aux( X, bfalse ) )
% 8.54/8.93 ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 2, [ =( notb( btrue ), bfalse ) ] )
% 8.54/8.93 , clause( 7500, [ =( notb( btrue ), bfalse ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 3, [ =( notb( bfalse ), btrue ) ] )
% 8.54/8.93 , clause( 7501, [ =( notb( bfalse ), btrue ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 4, [ =( half( zero ), zero ) ] )
% 8.54/8.93 , clause( 7502, [ =( half( zero ), zero ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 5, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , clause( 7503, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 6, [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ] )
% 8.54/8.93 , clause( 7504, [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 7, [ =( evenNat( zero ), btrue ) ] )
% 8.54/8.93 , clause( 7505, [ =( evenNat( zero ), btrue ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 8, [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ] )
% 8.54/8.93 , clause( 7506, [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 9, [ =( shw( zero ), nil ) ] )
% 8.54/8.93 , clause( 7507, [ =( shw( zero ), nil ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7609, [ =( shw( suc( X ) ), aux( X, notb( evenNat( X ) ) ) ) ] )
% 8.54/8.93 , clause( 8, [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ] )
% 8.54/8.93 , 0, clause( 7508, [ =( shw( suc( X ) ), aux( X, evenNat( suc( X ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 8.54/8.93 ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7610, [ =( aux( X, notb( evenNat( X ) ) ), shw( suc( X ) ) ) ] )
% 8.54/8.93 , clause( 7609, [ =( shw( suc( X ) ), aux( X, notb( evenNat( X ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 10, [ =( aux( X, notb( evenNat( X ) ) ), shw( suc( X ) ) ) ] )
% 8.54/8.93 , clause( 7610, [ =( aux( X, notb( evenNat( X ) ) ), shw( suc( X ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 11, [ =( append( nil, X ), X ) ] )
% 8.54/8.93 , clause( 7509, [ =( append( nil, X ), X ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 12, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 7510, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 8.54/8.93 permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 13, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 , clause( 7511, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 14, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.93 , clause( 7512, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 8.54/8.93 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7680, [ =( addNat( X, X ), double( X ) ) ] )
% 8.54/8.93 , clause( 7513, [ =( double( X ), addNat( X, X ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 15, [ =( addNat( X, X ), double( X ) ) ] )
% 8.54/8.93 , clause( 7680, [ =( addNat( X, X ), double( X ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 16, [ =( rd( nil ), zero ) ] )
% 8.54/8.93 , clause( 7514, [ =( rd( nil ), zero ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7715, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , clause( 7515, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , clause( 7715, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 18, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.93 , clause( 7516, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7754, [ =( rd( append( shw( X ), shw( Y ) ) ), x( X, Y ) ) ] )
% 8.54/8.93 , clause( 7517, [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 19, [ =( rd( append( shw( X ), shw( Y ) ) ), x( X, Y ) ) ] )
% 8.54/8.93 , clause( 7754, [ =( rd( append( shw( X ), shw( Y ) ) ), x( X, Y ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 8.54/8.93 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7775, [ =( eq( x( X, Y ), x( Y, X ) ), 'sat_comm'( X, Y ) ) ] )
% 8.54/8.93 , clause( 7518, [ =( 'sat_comm'( X, Y ), eq( x( X, Y ), x( Y, X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 20, [ =( eq( x( X, Y ), x( Y, X ) ), 'sat_comm'( X, Y ) ) ] )
% 8.54/8.93 , clause( 7775, [ =( eq( x( X, Y ), x( Y, X ) ), 'sat_comm'( X, Y ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 8.54/8.93 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.93 , clause( 7523, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 8.54/8.93 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 27, [ =( eq( suc( X ), zero ), bfalse ) ] )
% 8.54/8.93 , clause( 7525, [ =( eq( suc( X ), zero ), bfalse ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 29, [ =( eq2( X, X ), btrue ) ] )
% 8.54/8.93 , clause( 7527, [ =( eq2( X, X ), btrue ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 31, [ ~( =( eq2( 'sat_comm'( X, Y ), bfalse ), btrue ) ) ] )
% 8.54/8.93 , clause( 7529, [ ~( =( eq2( 'sat_comm'( X, Y ), bfalse ), btrue ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 8.54/8.93 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7893, [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 1, [ =( cons( i, shw( half( suc( X ) ) ) ), aux( X, bfalse ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7895, [ =( aux( zero, bfalse ), cons( i, shw( zero ) ) ) ] )
% 8.54/8.93 , clause( 5, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , 0, clause( 7893, [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7896, [ =( aux( zero, bfalse ), cons( i, nil ) ) ] )
% 8.54/8.93 , clause( 9, [ =( shw( zero ), nil ) ] )
% 8.54/8.93 , 0, clause( 7895, [ =( aux( zero, bfalse ), cons( i, shw( zero ) ) ) ] )
% 8.54/8.93 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7897, [ =( cons( i, nil ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , clause( 7896, [ =( aux( zero, bfalse ), cons( i, nil ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 32, [ =( cons( i, nil ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , clause( 7897, [ =( cons( i, nil ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7899, [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 0, [ =( cons( o, shw( half( suc( X ) ) ) ), aux( X, btrue ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7901, [ =( aux( zero, btrue ), cons( o, shw( zero ) ) ) ] )
% 8.54/8.93 , clause( 5, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , 0, clause( 7899, [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7902, [ =( aux( zero, btrue ), cons( o, nil ) ) ] )
% 8.54/8.93 , clause( 9, [ =( shw( zero ), nil ) ] )
% 8.54/8.93 , 0, clause( 7901, [ =( aux( zero, btrue ), cons( o, shw( zero ) ) ) ] )
% 8.54/8.93 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7903, [ =( cons( o, nil ), aux( zero, btrue ) ) ] )
% 8.54/8.93 , clause( 7902, [ =( aux( zero, btrue ), cons( o, nil ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 33, [ =( cons( o, nil ), aux( zero, btrue ) ) ] )
% 8.54/8.93 , clause( 7903, [ =( cons( o, nil ), aux( zero, btrue ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7904, [ =( double( X ), addNat( X, X ) ) ] )
% 8.54/8.93 , clause( 15, [ =( addNat( X, X ), double( X ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7906, [ =( double( zero ), zero ) ] )
% 8.54/8.93 , clause( 13, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 , 0, clause( 7904, [ =( double( X ), addNat( X, X ) ) ] )
% 8.54/8.93 , 0, 3, substitution( 0, [ :=( X, zero )] ), substitution( 1, [ :=( X, zero
% 8.54/8.93 )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 34, [ =( double( zero ), zero ) ] )
% 8.54/8.93 , clause( 7906, [ =( double( zero ), zero ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7909, [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 1, [ =( cons( i, shw( half( suc( X ) ) ) ), aux( X, bfalse ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7910, [ =( aux( suc( X ), bfalse ), cons( i, shw( suc( half( X ) )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , clause( 6, [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ] )
% 8.54/8.93 , 0, clause( 7909, [ =( aux( X, bfalse ), cons( i, shw( half( suc( X ) ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , 0, 8, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, suc( X
% 8.54/8.93 ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7911, [ =( cons( i, shw( suc( half( X ) ) ) ), aux( suc( X ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , clause( 7910, [ =( aux( suc( X ), bfalse ), cons( i, shw( suc( half( X )
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 35, [ =( cons( i, shw( suc( half( X ) ) ) ), aux( suc( X ), bfalse
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 7911, [ =( cons( i, shw( suc( half( X ) ) ) ), aux( suc( X ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7913, [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 0, [ =( cons( o, shw( half( suc( X ) ) ) ), aux( X, btrue ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7914, [ =( aux( suc( X ), btrue ), cons( o, shw( suc( half( X ) ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 6, [ =( half( suc( suc( X ) ) ), suc( half( X ) ) ) ] )
% 8.54/8.93 , 0, clause( 7913, [ =( aux( X, btrue ), cons( o, shw( half( suc( X ) ) ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 , 0, 8, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, suc( X
% 8.54/8.93 ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7915, [ =( cons( o, shw( suc( half( X ) ) ) ), aux( suc( X ), btrue
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 7914, [ =( aux( suc( X ), btrue ), cons( o, shw( suc( half( X ) )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 36, [ =( cons( o, shw( suc( half( X ) ) ) ), aux( suc( X ), btrue )
% 8.54/8.93 ) ] )
% 8.54/8.93 , clause( 7915, [ =( cons( o, shw( suc( half( X ) ) ) ), aux( suc( X ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7917, [ =( double( rd( X ) ), rd( cons( o, X ) ) ) ] )
% 8.54/8.93 , clause( 18, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7920, [ =( double( rd( nil ) ), rd( aux( zero, btrue ) ) ) ] )
% 8.54/8.93 , clause( 33, [ =( cons( o, nil ), aux( zero, btrue ) ) ] )
% 8.54/8.93 , 0, clause( 7917, [ =( double( rd( X ) ), rd( cons( o, X ) ) ) ] )
% 8.54/8.93 , 0, 5, substitution( 0, [] ), substitution( 1, [ :=( X, nil )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7921, [ =( double( zero ), rd( aux( zero, btrue ) ) ) ] )
% 8.54/8.93 , clause( 16, [ =( rd( nil ), zero ) ] )
% 8.54/8.93 , 0, clause( 7920, [ =( double( rd( nil ) ), rd( aux( zero, btrue ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7922, [ =( zero, rd( aux( zero, btrue ) ) ) ] )
% 8.54/8.93 , clause( 34, [ =( double( zero ), zero ) ] )
% 8.54/8.93 , 0, clause( 7921, [ =( double( zero ), rd( aux( zero, btrue ) ) ) ] )
% 8.54/8.93 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7923, [ =( rd( aux( zero, btrue ) ), zero ) ] )
% 8.54/8.93 , clause( 7922, [ =( zero, rd( aux( zero, btrue ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 37, [ =( rd( aux( zero, btrue ) ), zero ) ] )
% 8.54/8.93 , clause( 7923, [ =( rd( aux( zero, btrue ) ), zero ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7925, [ =( shw( suc( X ) ), aux( X, notb( evenNat( X ) ) ) ) ] )
% 8.54/8.93 , clause( 10, [ =( aux( X, notb( evenNat( X ) ) ), shw( suc( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7926, [ =( shw( suc( suc( X ) ) ), aux( suc( X ), notb( notb(
% 8.54/8.93 evenNat( X ) ) ) ) ) ] )
% 8.54/8.93 , clause( 8, [ =( evenNat( suc( X ) ), notb( evenNat( X ) ) ) ] )
% 8.54/8.93 , 0, clause( 7925, [ =( shw( suc( X ) ), aux( X, notb( evenNat( X ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, 9, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, suc( X
% 8.54/8.93 ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7927, [ =( aux( suc( X ), notb( notb( evenNat( X ) ) ) ), shw( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 7926, [ =( shw( suc( suc( X ) ) ), aux( suc( X ), notb( notb(
% 8.54/8.93 evenNat( X ) ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 39, [ =( aux( suc( X ), notb( notb( evenNat( X ) ) ) ), shw( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 7927, [ =( aux( suc( X ), notb( notb( evenNat( X ) ) ) ), shw(
% 8.54/8.93 suc( suc( X ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7929, [ =( shw( suc( X ) ), aux( X, notb( evenNat( X ) ) ) ) ] )
% 8.54/8.93 , clause( 10, [ =( aux( X, notb( evenNat( X ) ) ), shw( suc( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7931, [ =( shw( suc( zero ) ), aux( zero, notb( btrue ) ) ) ] )
% 8.54/8.93 , clause( 7, [ =( evenNat( zero ), btrue ) ] )
% 8.54/8.93 , 0, clause( 7929, [ =( shw( suc( X ) ), aux( X, notb( evenNat( X ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7932, [ =( shw( suc( zero ) ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , clause( 2, [ =( notb( btrue ), bfalse ) ] )
% 8.54/8.93 , 0, clause( 7931, [ =( shw( suc( zero ) ), aux( zero, notb( btrue ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7933, [ =( aux( zero, bfalse ), shw( suc( zero ) ) ) ] )
% 8.54/8.93 , clause( 7932, [ =( shw( suc( zero ) ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 40, [ =( aux( zero, bfalse ), shw( suc( zero ) ) ) ] )
% 8.54/8.93 , clause( 7933, [ =( aux( zero, bfalse ), shw( suc( zero ) ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7934, [ =( suc( addNat( X, Y ) ), addNat( suc( X ), Y ) ) ] )
% 8.54/8.93 , clause( 14, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7937, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ] )
% 8.54/8.93 , clause( 15, [ =( addNat( X, X ), double( X ) ) ] )
% 8.54/8.93 , 0, clause( 7934, [ =( suc( addNat( X, Y ) ), addNat( suc( X ), Y ) ) ] )
% 8.54/8.93 , 0, 6, substitution( 0, [ :=( X, suc( X ) )] ), substitution( 1, [ :=( X,
% 8.54/8.93 X ), :=( Y, suc( X ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 41, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ] )
% 8.54/8.93 , clause( 7937, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7941, [ =( double( suc( X ) ), suc( addNat( X, suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 41, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7946, [ =( double( suc( suc( X ) ) ), suc( suc( addNat( X, suc( suc(
% 8.54/8.93 X ) ) ) ) ) ) ] )
% 8.54/8.93 , clause( 14, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.93 , 0, clause( 7941, [ =( double( suc( X ) ), suc( addNat( X, suc( X ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, 6, substitution( 0, [ :=( X, X ), :=( Y, suc( suc( X ) ) )] ),
% 8.54/8.93 substitution( 1, [ :=( X, suc( X ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7947, [ =( suc( suc( addNat( X, suc( suc( X ) ) ) ) ), double( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 7946, [ =( double( suc( suc( X ) ) ), suc( suc( addNat( X, suc(
% 8.54/8.93 suc( X ) ) ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 44, [ =( suc( suc( addNat( X, suc( suc( X ) ) ) ) ), double( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 7947, [ =( suc( suc( addNat( X, suc( suc( X ) ) ) ) ), double(
% 8.54/8.93 suc( suc( X ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7949, [ =( double( suc( X ) ), suc( addNat( X, suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 41, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7950, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.93 , clause( 13, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 , 0, clause( 7949, [ =( double( suc( X ) ), suc( addNat( X, suc( X ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, 5, substitution( 0, [ :=( X, suc( zero ) )] ), substitution( 1, [ :=(
% 8.54/8.93 X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 51, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.93 , clause( 7950, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7953, [ =( cons( X, append( Y, Z ) ), append( cons( X, Y ), Z ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 12, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7956, [ =( cons( i, append( nil, X ) ), append( aux( zero, bfalse )
% 8.54/8.93 , X ) ) ] )
% 8.54/8.93 , clause( 32, [ =( cons( i, nil ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , 0, clause( 7953, [ =( cons( X, append( Y, Z ) ), append( cons( X, Y ), Z
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, i ), :=( Y, nil )
% 8.54/8.93 , :=( Z, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7957, [ =( cons( i, append( nil, X ) ), append( shw( suc( zero ) )
% 8.54/8.93 , X ) ) ] )
% 8.54/8.93 , clause( 40, [ =( aux( zero, bfalse ), shw( suc( zero ) ) ) ] )
% 8.54/8.93 , 0, clause( 7956, [ =( cons( i, append( nil, X ) ), append( aux( zero,
% 8.54/8.93 bfalse ), X ) ) ] )
% 8.54/8.93 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7958, [ =( cons( i, X ), append( shw( suc( zero ) ), X ) ) ] )
% 8.54/8.93 , clause( 11, [ =( append( nil, X ), X ) ] )
% 8.54/8.93 , 0, clause( 7957, [ =( cons( i, append( nil, X ) ), append( shw( suc( zero
% 8.54/8.93 ) ), X ) ) ] )
% 8.54/8.93 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 8.54/8.93 ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7959, [ =( append( shw( suc( zero ) ), X ), cons( i, X ) ) ] )
% 8.54/8.93 , clause( 7958, [ =( cons( i, X ), append( shw( suc( zero ) ), X ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 55, [ =( append( shw( suc( zero ) ), X ), cons( i, X ) ) ] )
% 8.54/8.93 , clause( 7959, [ =( append( shw( suc( zero ) ), X ), cons( i, X ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7961, [ =( double( suc( X ) ), suc( addNat( X, suc( X ) ) ) ) ] )
% 8.54/8.93 , clause( 41, [ =( suc( addNat( X, suc( X ) ) ), double( suc( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7963, [ =( double( suc( double( rd( X ) ) ) ), suc( addNat( double(
% 8.54/8.93 rd( X ) ), rd( cons( i, X ) ) ) ) ) ] )
% 8.54/8.93 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , 0, clause( 7961, [ =( double( suc( X ) ), suc( addNat( X, suc( X ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, 11, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, double(
% 8.54/8.93 rd( X ) ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7964, [ =( double( rd( cons( i, X ) ) ), suc( addNat( double( rd( X
% 8.54/8.93 ) ), rd( cons( i, X ) ) ) ) ) ] )
% 8.54/8.93 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , 0, clause( 7963, [ =( double( suc( double( rd( X ) ) ) ), suc( addNat(
% 8.54/8.93 double( rd( X ) ), rd( cons( i, X ) ) ) ) ) ] )
% 8.54/8.93 , 0, 2, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 8.54/8.93 ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7966, [ =( suc( addNat( double( rd( X ) ), rd( cons( i, X ) ) ) ),
% 8.54/8.93 double( rd( cons( i, X ) ) ) ) ] )
% 8.54/8.93 , clause( 7964, [ =( double( rd( cons( i, X ) ) ), suc( addNat( double( rd(
% 8.54/8.93 X ) ), rd( cons( i, X ) ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 66, [ =( suc( addNat( double( rd( X ) ), rd( cons( i, X ) ) ) ),
% 8.54/8.93 double( rd( cons( i, X ) ) ) ) ] )
% 8.54/8.93 , clause( 7966, [ =( suc( addNat( double( rd( X ) ), rd( cons( i, X ) ) ) )
% 8.54/8.93 , double( rd( cons( i, X ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7969, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7971, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( double( zero )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 37, [ =( rd( aux( zero, btrue ) ), zero ) ] )
% 8.54/8.93 , 0, clause( 7969, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, aux( zero, btrue )
% 8.54/8.93 )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7972, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , clause( 34, [ =( double( zero ), zero ) ] )
% 8.54/8.93 , 0, clause( 7971, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( double(
% 8.54/8.93 zero ) ) ) ] )
% 8.54/8.93 , 0, 8, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 70, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , clause( 7972, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( zero ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7975, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7979, [ =( rd( cons( i, nil ) ), suc( double( zero ) ) ) ] )
% 8.54/8.93 , clause( 16, [ =( rd( nil ), zero ) ] )
% 8.54/8.93 , 0, clause( 7975, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, nil )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7980, [ =( rd( cons( i, nil ) ), suc( zero ) ) ] )
% 8.54/8.93 , clause( 34, [ =( double( zero ), zero ) ] )
% 8.54/8.93 , 0, clause( 7979, [ =( rd( cons( i, nil ) ), suc( double( zero ) ) ) ] )
% 8.54/8.93 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7981, [ =( rd( aux( zero, bfalse ) ), suc( zero ) ) ] )
% 8.54/8.93 , clause( 32, [ =( cons( i, nil ), aux( zero, bfalse ) ) ] )
% 8.54/8.93 , 0, clause( 7980, [ =( rd( cons( i, nil ) ), suc( zero ) ) ] )
% 8.54/8.93 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7982, [ =( rd( shw( suc( zero ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , clause( 40, [ =( aux( zero, bfalse ), shw( suc( zero ) ) ) ] )
% 8.54/8.93 , 0, clause( 7981, [ =( rd( aux( zero, bfalse ) ), suc( zero ) ) ] )
% 8.54/8.93 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 78, [ =( rd( shw( suc( zero ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , clause( 7982, [ =( rd( shw( suc( zero ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7985, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7987, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( double( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , clause( 78, [ =( rd( shw( suc( zero ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , 0, clause( 7985, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, shw( suc( zero ) )
% 8.54/8.93 )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7988, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( suc( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , clause( 51, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.93 , 0, clause( 7987, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( double(
% 8.54/8.93 suc( zero ) ) ) ) ] )
% 8.54/8.93 , 0, 8, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 79, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( suc( suc( zero )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , clause( 7988, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( suc( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7991, [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ] )
% 8.54/8.93 , clause( 19, [ =( rd( append( shw( X ), shw( Y ) ) ), x( X, Y ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7992, [ =( x( suc( zero ), X ), rd( cons( i, shw( X ) ) ) ) ] )
% 8.54/8.93 , clause( 55, [ =( append( shw( suc( zero ) ), X ), cons( i, X ) ) ] )
% 8.54/8.93 , 0, clause( 7991, [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , 0, 6, substitution( 0, [ :=( X, shw( X ) )] ), substitution( 1, [ :=( X,
% 8.54/8.93 suc( zero ) ), :=( Y, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7993, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.93 , clause( 7992, [ =( x( suc( zero ), X ), rd( cons( i, shw( X ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 91, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.93 , clause( 7993, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7995, [ =( aux( suc( X ), bfalse ), cons( i, shw( suc( half( X ) )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , clause( 35, [ =( cons( i, shw( suc( half( X ) ) ) ), aux( suc( X ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 7996, [ =( aux( suc( suc( zero ) ), bfalse ), cons( i, shw( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , clause( 5, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , 0, clause( 7995, [ =( aux( suc( X ), bfalse ), cons( i, shw( suc( half( X
% 8.54/8.93 ) ) ) ) ) ] )
% 8.54/8.93 , 0, 10, substitution( 0, [] ), substitution( 1, [ :=( X, suc( zero ) )] )
% 8.54/8.93 ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7997, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , clause( 7996, [ =( aux( suc( suc( zero ) ), bfalse ), cons( i, shw( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 96, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , clause( 7997, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( suc( zero ) )
% 8.54/8.93 , bfalse ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 7999, [ =( aux( suc( X ), bfalse ), cons( i, shw( suc( half( X ) )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , clause( 35, [ =( cons( i, shw( suc( half( X ) ) ) ), aux( suc( X ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8001, [ =( aux( suc( zero ), bfalse ), cons( i, shw( suc( zero ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 4, [ =( half( zero ), zero ) ] )
% 8.54/8.93 , 0, clause( 7999, [ =( aux( suc( X ), bfalse ), cons( i, shw( suc( half( X
% 8.54/8.93 ) ) ) ) ) ] )
% 8.54/8.93 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8002, [ =( aux( suc( zero ), bfalse ), aux( suc( suc( zero ) ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , clause( 96, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , 0, clause( 8001, [ =( aux( suc( zero ), bfalse ), cons( i, shw( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , 0, 5, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8003, [ =( aux( suc( suc( zero ) ), bfalse ), aux( suc( zero ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , clause( 8002, [ =( aux( suc( zero ), bfalse ), aux( suc( suc( zero ) ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 97, [ =( aux( suc( suc( zero ) ), bfalse ), aux( suc( zero ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , clause( 8003, [ =( aux( suc( suc( zero ) ), bfalse ), aux( suc( zero ),
% 8.54/8.93 bfalse ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8005, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8008, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc(
% 8.54/8.93 double( suc( zero ) ) ) ) ] )
% 8.54/8.93 , clause( 70, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( zero ) ) ] )
% 8.54/8.93 , 0, clause( 8005, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.93 , 0, 11, substitution( 0, [] ), substitution( 1, [ :=( X, cons( i, aux(
% 8.54/8.93 zero, btrue ) ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8009, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc( suc(
% 8.54/8.93 suc( zero ) ) ) ) ] )
% 8.54/8.93 , clause( 51, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.93 , 0, clause( 8008, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc(
% 8.54/8.93 double( suc( zero ) ) ) ) ] )
% 8.54/8.93 , 0, 10, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 98, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc( suc(
% 8.54/8.93 suc( zero ) ) ) ) ] )
% 8.54/8.93 , clause( 8009, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc(
% 8.54/8.93 suc( suc( zero ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8012, [ =( aux( suc( X ), btrue ), cons( o, shw( suc( half( X ) ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 36, [ =( cons( o, shw( suc( half( X ) ) ) ), aux( suc( X ), btrue
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8013, [ =( aux( suc( suc( zero ) ), btrue ), cons( o, shw( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , clause( 5, [ =( half( suc( zero ) ), zero ) ] )
% 8.54/8.93 , 0, clause( 8012, [ =( aux( suc( X ), btrue ), cons( o, shw( suc( half( X
% 8.54/8.93 ) ) ) ) ) ] )
% 8.54/8.93 , 0, 10, substitution( 0, [] ), substitution( 1, [ :=( X, suc( zero ) )] )
% 8.54/8.93 ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8014, [ =( cons( o, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , clause( 8013, [ =( aux( suc( suc( zero ) ), btrue ), cons( o, shw( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 104, [ =( cons( o, shw( suc( zero ) ) ), aux( suc( suc( zero ) ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , clause( 8014, [ =( cons( o, shw( suc( zero ) ) ), aux( suc( suc( zero ) )
% 8.54/8.93 , btrue ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8016, [ =( aux( suc( X ), btrue ), cons( o, shw( suc( half( X ) ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 36, [ =( cons( o, shw( suc( half( X ) ) ) ), aux( suc( X ), btrue
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8018, [ =( aux( suc( zero ), btrue ), cons( o, shw( suc( zero ) ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 , clause( 4, [ =( half( zero ), zero ) ] )
% 8.54/8.93 , 0, clause( 8016, [ =( aux( suc( X ), btrue ), cons( o, shw( suc( half( X
% 8.54/8.93 ) ) ) ) ) ] )
% 8.54/8.93 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8019, [ =( aux( suc( zero ), btrue ), aux( suc( suc( zero ) ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , clause( 104, [ =( cons( o, shw( suc( zero ) ) ), aux( suc( suc( zero ) )
% 8.54/8.93 , btrue ) ) ] )
% 8.54/8.93 , 0, clause( 8018, [ =( aux( suc( zero ), btrue ), cons( o, shw( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , 0, 5, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8020, [ =( aux( suc( suc( zero ) ), btrue ), aux( suc( zero ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , clause( 8019, [ =( aux( suc( zero ), btrue ), aux( suc( suc( zero ) ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 105, [ =( aux( suc( suc( zero ) ), btrue ), aux( suc( zero ), btrue
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 8020, [ =( aux( suc( suc( zero ) ), btrue ), aux( suc( zero ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8022, [ =( shw( suc( suc( X ) ) ), aux( suc( X ), notb( notb(
% 8.54/8.93 evenNat( X ) ) ) ) ) ] )
% 8.54/8.93 , clause( 39, [ =( aux( suc( X ), notb( notb( evenNat( X ) ) ) ), shw( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8025, [ =( shw( suc( suc( zero ) ) ), aux( suc( zero ), notb( notb(
% 8.54/8.93 btrue ) ) ) ) ] )
% 8.54/8.93 , clause( 7, [ =( evenNat( zero ), btrue ) ] )
% 8.54/8.93 , 0, clause( 8022, [ =( shw( suc( suc( X ) ) ), aux( suc( X ), notb( notb(
% 8.54/8.93 evenNat( X ) ) ) ) ) ] )
% 8.54/8.93 , 0, 10, substitution( 0, [] ), substitution( 1, [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8026, [ =( shw( suc( suc( zero ) ) ), aux( suc( zero ), notb(
% 8.54/8.93 bfalse ) ) ) ] )
% 8.54/8.93 , clause( 2, [ =( notb( btrue ), bfalse ) ] )
% 8.54/8.93 , 0, clause( 8025, [ =( shw( suc( suc( zero ) ) ), aux( suc( zero ), notb(
% 8.54/8.93 notb( btrue ) ) ) ) ] )
% 8.54/8.93 , 0, 9, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8027, [ =( shw( suc( suc( zero ) ) ), aux( suc( zero ), btrue ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 3, [ =( notb( bfalse ), btrue ) ] )
% 8.54/8.93 , 0, clause( 8026, [ =( shw( suc( suc( zero ) ) ), aux( suc( zero ), notb(
% 8.54/8.93 bfalse ) ) ) ] )
% 8.54/8.93 , 0, 8, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8028, [ =( aux( suc( zero ), btrue ), shw( suc( suc( zero ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 8027, [ =( shw( suc( suc( zero ) ) ), aux( suc( zero ), btrue ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 123, [ =( aux( suc( zero ), btrue ), shw( suc( suc( zero ) ) ) ) ]
% 8.54/8.93 )
% 8.54/8.93 , clause( 8028, [ =( aux( suc( zero ), btrue ), shw( suc( suc( zero ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8031, [ =( aux( suc( suc( zero ) ), btrue ), shw( suc( suc( zero )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , clause( 123, [ =( aux( suc( zero ), btrue ), shw( suc( suc( zero ) ) ) )
% 8.54/8.93 ] )
% 8.54/8.93 , 0, clause( 105, [ =( aux( suc( suc( zero ) ), btrue ), aux( suc( zero ),
% 8.54/8.93 btrue ) ) ] )
% 8.54/8.93 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 138, [ =( aux( suc( suc( zero ) ), btrue ), shw( suc( suc( zero ) )
% 8.54/8.93 ) ) ] )
% 8.54/8.93 , clause( 8031, [ =( aux( suc( suc( zero ) ), btrue ), shw( suc( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8034, [ =( double( suc( suc( X ) ) ), suc( suc( addNat( X, suc( suc(
% 8.54/8.93 X ) ) ) ) ) ) ] )
% 8.54/8.93 , clause( 44, [ =( suc( suc( addNat( X, suc( suc( X ) ) ) ) ), double( suc(
% 8.54/8.93 suc( X ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8035, [ =( double( suc( suc( zero ) ) ), suc( suc( suc( suc( zero )
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , clause( 13, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.93 , 0, clause( 8034, [ =( double( suc( suc( X ) ) ), suc( suc( addNat( X, suc(
% 8.54/8.93 suc( X ) ) ) ) ) ) ] )
% 8.54/8.93 , 0, 7, substitution( 0, [ :=( X, suc( suc( zero ) ) )] ), substitution( 1
% 8.54/8.93 , [ :=( X, zero )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8036, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , clause( 8035, [ =( double( suc( suc( zero ) ) ), suc( suc( suc( suc( zero
% 8.54/8.93 ) ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 176, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc( zero
% 8.54/8.93 ) ) ) ) ] )
% 8.54/8.93 , clause( 8036, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8038, [ =( eq( X, Y ), eq( suc( X ), suc( Y ) ) ) ] )
% 8.54/8.93 , clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8039, [ =( eq( suc( suc( suc( zero ) ) ), X ), eq( double( suc( suc(
% 8.54/8.93 zero ) ) ), suc( X ) ) ) ] )
% 8.54/8.93 , clause( 176, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , 0, clause( 8038, [ =( eq( X, Y ), eq( suc( X ), suc( Y ) ) ) ] )
% 8.54/8.93 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, suc( suc( suc(
% 8.54/8.93 zero ) ) ) ), :=( Y, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8041, [ =( eq( double( suc( suc( zero ) ) ), suc( X ) ), eq( suc(
% 8.54/8.93 suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.93 , clause( 8039, [ =( eq( suc( suc( suc( zero ) ) ), X ), eq( double( suc(
% 8.54/8.93 suc( zero ) ) ), suc( X ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 184, [ =( eq( double( suc( suc( zero ) ) ), suc( X ) ), eq( suc(
% 8.54/8.93 suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.93 , clause( 8041, [ =( eq( double( suc( suc( zero ) ) ), suc( X ) ), eq( suc(
% 8.54/8.93 suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8044, [ =( eq( X, Y ), eq( suc( X ), suc( Y ) ) ) ] )
% 8.54/8.93 , clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8046, [ =( eq( X, suc( suc( suc( zero ) ) ) ), eq( suc( X ), double(
% 8.54/8.93 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 , clause( 176, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc(
% 8.54/8.93 zero ) ) ) ) ] )
% 8.54/8.93 , 0, clause( 8044, [ =( eq( X, Y ), eq( suc( X ), suc( Y ) ) ) ] )
% 8.54/8.93 , 0, 10, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y, suc(
% 8.54/8.93 suc( suc( zero ) ) ) )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 eqswap(
% 8.54/8.93 clause( 8048, [ =( eq( suc( X ), double( suc( suc( zero ) ) ) ), eq( X, suc(
% 8.54/8.93 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 , clause( 8046, [ =( eq( X, suc( suc( suc( zero ) ) ) ), eq( suc( X ),
% 8.54/8.93 double( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 subsumption(
% 8.54/8.93 clause( 185, [ =( eq( suc( X ), double( suc( suc( zero ) ) ) ), eq( X, suc(
% 8.54/8.93 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 , clause( 8048, [ =( eq( suc( X ), double( suc( suc( zero ) ) ) ), eq( X,
% 8.54/8.93 suc( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.93 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.93
% 8.54/8.93
% 8.54/8.93 paramod(
% 8.54/8.93 clause( 8051, [ =( cons( o, shw( suc( zero ) ) ), shw( suc( suc( zero ) ) )
% 8.54/8.93 ) ] )
% 8.54/8.93 , clause( 138, [ =( aux( suc( suc( zero ) ), btrue ), shw( suc( suc( zero )
% 8.54/8.93 ) ) ) ] )
% 8.54/8.93 , 0, clause( 104, [ =( cons( o, shw( suc( zero ) ) ), aux( suc( suc( zero )
% 8.54/8.93 ), btrue ) ) ] )
% 8.54/8.93 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 317, [ =( cons( o, shw( suc( zero ) ) ), shw( suc( suc( zero ) ) )
% 8.54/8.94 ) ] )
% 8.54/8.94 , clause( 8051, [ =( cons( o, shw( suc( zero ) ) ), shw( suc( suc( zero ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8054, [ =( cons( X, append( Y, Z ) ), append( cons( X, Y ), Z ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , clause( 12, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8056, [ =( cons( o, append( shw( suc( zero ) ), X ) ), append( shw(
% 8.54/8.94 suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.94 , clause( 317, [ =( cons( o, shw( suc( zero ) ) ), shw( suc( suc( zero ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, clause( 8054, [ =( cons( X, append( Y, Z ) ), append( cons( X, Y ), Z
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, o ), :=( Y, shw(
% 8.54/8.94 suc( zero ) ) ), :=( Z, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8057, [ =( cons( o, cons( i, X ) ), append( shw( suc( suc( zero ) )
% 8.54/8.94 ), X ) ) ] )
% 8.54/8.94 , clause( 55, [ =( append( shw( suc( zero ) ), X ), cons( i, X ) ) ] )
% 8.54/8.94 , 0, clause( 8056, [ =( cons( o, append( shw( suc( zero ) ), X ) ), append(
% 8.54/8.94 shw( suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.94 , 0, 3, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 8.54/8.94 ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8058, [ =( append( shw( suc( suc( zero ) ) ), X ), cons( o, cons( i
% 8.54/8.94 , X ) ) ) ] )
% 8.54/8.94 , clause( 8057, [ =( cons( o, cons( i, X ) ), append( shw( suc( suc( zero )
% 8.54/8.94 ) ), X ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 318, [ =( append( shw( suc( suc( zero ) ) ), X ), cons( o, cons( i
% 8.54/8.94 , X ) ) ) ] )
% 8.54/8.94 , clause( 8058, [ =( append( shw( suc( suc( zero ) ) ), X ), cons( o, cons(
% 8.54/8.94 i, X ) ) ) ] )
% 8.54/8.94 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8060, [ =( double( rd( X ) ), rd( cons( o, X ) ) ) ] )
% 8.54/8.94 , clause( 18, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8063, [ =( double( rd( shw( suc( zero ) ) ) ), rd( shw( suc( suc(
% 8.54/8.94 zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 317, [ =( cons( o, shw( suc( zero ) ) ), shw( suc( suc( zero ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, clause( 8060, [ =( double( rd( X ) ), rd( cons( o, X ) ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, shw( suc( zero ) )
% 8.54/8.94 )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8064, [ =( double( suc( zero ) ), rd( shw( suc( suc( zero ) ) ) ) )
% 8.54/8.94 ] )
% 8.54/8.94 , clause( 78, [ =( rd( shw( suc( zero ) ) ), suc( zero ) ) ] )
% 8.54/8.94 , 0, clause( 8063, [ =( double( rd( shw( suc( zero ) ) ) ), rd( shw( suc(
% 8.54/8.94 suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8065, [ =( suc( suc( zero ) ), rd( shw( suc( suc( zero ) ) ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , clause( 51, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.94 , 0, clause( 8064, [ =( double( suc( zero ) ), rd( shw( suc( suc( zero ) )
% 8.54/8.94 ) ) ) ] )
% 8.54/8.94 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8066, [ =( rd( shw( suc( suc( zero ) ) ) ), suc( suc( zero ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , clause( 8065, [ =( suc( suc( zero ) ), rd( shw( suc( suc( zero ) ) ) ) )
% 8.54/8.94 ] )
% 8.54/8.94 , 0, substitution( 0, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 319, [ =( rd( shw( suc( suc( zero ) ) ) ), suc( suc( zero ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , clause( 8066, [ =( rd( shw( suc( suc( zero ) ) ) ), suc( suc( zero ) ) )
% 8.54/8.94 ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8068, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.94 , clause( 17, [ =( suc( double( rd( X ) ) ), rd( cons( i, X ) ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8070, [ =( rd( cons( i, shw( suc( suc( zero ) ) ) ) ), suc( double(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 319, [ =( rd( shw( suc( suc( zero ) ) ) ), suc( suc( zero ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, clause( 8068, [ =( rd( cons( i, X ) ), suc( double( rd( X ) ) ) ) ] )
% 8.54/8.94 , 0, 10, substitution( 0, [] ), substitution( 1, [ :=( X, shw( suc( suc(
% 8.54/8.94 zero ) ) ) )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8071, [ =( x( suc( zero ), suc( suc( zero ) ) ), suc( double( suc(
% 8.54/8.94 suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 91, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.94 , 0, clause( 8070, [ =( rd( cons( i, shw( suc( suc( zero ) ) ) ) ), suc(
% 8.54/8.94 double( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, 1, substitution( 0, [ :=( X, suc( suc( zero ) ) )] ), substitution( 1
% 8.54/8.94 , [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 324, [ =( x( suc( zero ), suc( suc( zero ) ) ), suc( double( suc(
% 8.54/8.94 suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 8071, [ =( x( suc( zero ), suc( suc( zero ) ) ), suc( double( suc(
% 8.54/8.94 suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8075, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( zero ), bfalse
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , clause( 97, [ =( aux( suc( suc( zero ) ), bfalse ), aux( suc( zero ),
% 8.54/8.94 bfalse ) ) ] )
% 8.54/8.94 , 0, clause( 96, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( suc( zero )
% 8.54/8.94 ), bfalse ) ) ] )
% 8.54/8.94 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 325, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( zero ), bfalse )
% 8.54/8.94 ) ] )
% 8.54/8.94 , clause( 8075, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( zero ),
% 8.54/8.94 bfalse ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8078, [ =( x( suc( zero ), X ), rd( cons( i, shw( X ) ) ) ) ] )
% 8.54/8.94 , clause( 91, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8079, [ =( x( suc( zero ), suc( zero ) ), rd( aux( suc( zero ),
% 8.54/8.94 bfalse ) ) ) ] )
% 8.54/8.94 , clause( 325, [ =( cons( i, shw( suc( zero ) ) ), aux( suc( zero ), bfalse
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, clause( 8078, [ =( x( suc( zero ), X ), rd( cons( i, shw( X ) ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, 7, substitution( 0, [] ), substitution( 1, [ :=( X, suc( zero ) )] )
% 8.54/8.94 ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 326, [ =( x( suc( zero ), suc( zero ) ), rd( aux( suc( zero ),
% 8.54/8.94 bfalse ) ) ) ] )
% 8.54/8.94 , clause( 8079, [ =( x( suc( zero ), suc( zero ) ), rd( aux( suc( zero ),
% 8.54/8.94 bfalse ) ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8082, [ =( double( rd( cons( i, X ) ) ), suc( addNat( double( rd( X
% 8.54/8.94 ) ), rd( cons( i, X ) ) ) ) ) ] )
% 8.54/8.94 , clause( 66, [ =( suc( addNat( double( rd( X ) ), rd( cons( i, X ) ) ) ),
% 8.54/8.94 double( rd( cons( i, X ) ) ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8091, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) )
% 8.54/8.94 , suc( addNat( double( suc( zero ) ), rd( cons( i, cons( i, aux( zero,
% 8.54/8.94 btrue ) ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 70, [ =( rd( cons( i, aux( zero, btrue ) ) ), suc( zero ) ) ] )
% 8.54/8.94 , 0, clause( 8082, [ =( double( rd( cons( i, X ) ) ), suc( addNat( double(
% 8.54/8.94 rd( X ) ), rd( cons( i, X ) ) ) ) ) ] )
% 8.54/8.94 , 0, 13, substitution( 0, [] ), substitution( 1, [ :=( X, cons( i, aux(
% 8.54/8.94 zero, btrue ) ) )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8093, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) )
% 8.54/8.94 , suc( addNat( suc( suc( zero ) ), rd( cons( i, cons( i, aux( zero, btrue
% 8.54/8.94 ) ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 51, [ =( double( suc( zero ) ), suc( suc( zero ) ) ) ] )
% 8.54/8.94 , 0, clause( 8091, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ), suc( addNat( double( suc( zero ) ), rd( cons( i, cons( i, aux(
% 8.54/8.94 zero, btrue ) ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, 12, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8094, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) )
% 8.54/8.94 , suc( suc( addNat( suc( zero ), rd( cons( i, cons( i, aux( zero, btrue )
% 8.54/8.94 ) ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 14, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.94 , 0, clause( 8093, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ), suc( addNat( suc( suc( zero ) ), rd( cons( i, cons( i, aux( zero
% 8.54/8.94 , btrue ) ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, 11, substitution( 0, [ :=( X, suc( zero ) ), :=( Y, rd( cons( i, cons(
% 8.54/8.94 i, aux( zero, btrue ) ) ) ) )] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8096, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) )
% 8.54/8.94 , suc( suc( suc( addNat( zero, rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 14, [ =( addNat( suc( X ), Y ), suc( addNat( X, Y ) ) ) ] )
% 8.54/8.94 , 0, clause( 8094, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ), suc( suc( addNat( suc( zero ), rd( cons( i, cons( i, aux( zero,
% 8.54/8.94 btrue ) ) ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, 12, substitution( 0, [ :=( X, zero ), :=( Y, rd( cons( i, cons( i, aux(
% 8.54/8.94 zero, btrue ) ) ) ) )] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8097, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) )
% 8.54/8.94 , suc( suc( suc( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) ) ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , clause( 13, [ =( addNat( zero, X ), X ) ] )
% 8.54/8.94 , 0, clause( 8096, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ), suc( suc( suc( addNat( zero, rd( cons( i, cons( i, aux( zero,
% 8.54/8.94 btrue ) ) ) ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, 13, substitution( 0, [ :=( X, rd( cons( i, cons( i, aux( zero, btrue )
% 8.54/8.94 ) ) ) )] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8099, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) )
% 8.54/8.94 , suc( suc( suc( suc( suc( suc( zero ) ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 98, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc( suc(
% 8.54/8.94 suc( zero ) ) ) ) ] )
% 8.54/8.94 , 0, clause( 8097, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ), suc( suc( suc( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ) ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, 13, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8100, [ =( double( suc( suc( suc( zero ) ) ) ), suc( suc( suc( suc(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 98, [ =( rd( cons( i, cons( i, aux( zero, btrue ) ) ) ), suc( suc(
% 8.54/8.94 suc( zero ) ) ) ) ] )
% 8.54/8.94 , 0, clause( 8099, [ =( double( rd( cons( i, cons( i, aux( zero, btrue ) )
% 8.54/8.94 ) ) ), suc( suc( suc( suc( suc( suc( zero ) ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, 2, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8103, [ =( double( suc( suc( suc( zero ) ) ) ), suc( suc( double(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ) ] )
% 8.54/8.94 , clause( 176, [ =( suc( suc( suc( suc( zero ) ) ) ), double( suc( suc(
% 8.54/8.94 zero ) ) ) ) ] )
% 8.54/8.94 , 0, clause( 8100, [ =( double( suc( suc( suc( zero ) ) ) ), suc( suc( suc(
% 8.54/8.94 suc( suc( suc( zero ) ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, 8, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8104, [ =( suc( suc( double( suc( suc( zero ) ) ) ) ), double( suc(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 8103, [ =( double( suc( suc( suc( zero ) ) ) ), suc( suc( double(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 342, [ =( suc( suc( double( suc( suc( zero ) ) ) ) ), double( suc(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 8104, [ =( suc( suc( double( suc( suc( zero ) ) ) ) ), double(
% 8.54/8.94 suc( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8108, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero ) ) )
% 8.54/8.94 ) ] )
% 8.54/8.94 , clause( 91, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.94 , 0, clause( 79, [ =( rd( cons( i, shw( suc( zero ) ) ) ), suc( suc( suc(
% 8.54/8.94 zero ) ) ) ) ] )
% 8.54/8.94 , 0, 1, substitution( 0, [ :=( X, suc( zero ) )] ), substitution( 1, [] )
% 8.54/8.94 ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8109, [ =( rd( aux( suc( zero ), bfalse ) ), suc( suc( suc( zero )
% 8.54/8.94 ) ) ) ] )
% 8.54/8.94 , clause( 326, [ =( x( suc( zero ), suc( zero ) ), rd( aux( suc( zero ),
% 8.54/8.94 bfalse ) ) ) ] )
% 8.54/8.94 , 0, clause( 8108, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero
% 8.54/8.94 ) ) ) ) ] )
% 8.54/8.94 , 0, 1, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 348, [ =( rd( aux( suc( zero ), bfalse ) ), suc( suc( suc( zero ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , clause( 8109, [ =( rd( aux( suc( zero ), bfalse ) ), suc( suc( suc( zero
% 8.54/8.94 ) ) ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8112, [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ] )
% 8.54/8.94 , clause( 19, [ =( rd( append( shw( X ), shw( Y ) ) ), x( X, Y ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8115, [ =( x( suc( suc( zero ) ), X ), rd( cons( o, cons( i, shw( X
% 8.54/8.94 ) ) ) ) ) ] )
% 8.54/8.94 , clause( 318, [ =( append( shw( suc( suc( zero ) ) ), X ), cons( o, cons(
% 8.54/8.94 i, X ) ) ) ] )
% 8.54/8.94 , 0, clause( 8112, [ =( x( X, Y ), rd( append( shw( X ), shw( Y ) ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, shw( X ) )] ), substitution( 1, [ :=( X,
% 8.54/8.94 suc( suc( zero ) ) ), :=( Y, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8116, [ =( x( suc( suc( zero ) ), X ), double( rd( cons( i, shw( X
% 8.54/8.94 ) ) ) ) ) ] )
% 8.54/8.94 , clause( 18, [ =( rd( cons( o, X ) ), double( rd( X ) ) ) ] )
% 8.54/8.94 , 0, clause( 8115, [ =( x( suc( suc( zero ) ), X ), rd( cons( o, cons( i,
% 8.54/8.94 shw( X ) ) ) ) ) ] )
% 8.54/8.94 , 0, 6, substitution( 0, [ :=( X, cons( i, shw( X ) ) )] ), substitution( 1
% 8.54/8.94 , [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8117, [ =( x( suc( suc( zero ) ), X ), double( x( suc( zero ), X )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , clause( 91, [ =( rd( cons( i, shw( X ) ) ), x( suc( zero ), X ) ) ] )
% 8.54/8.94 , 0, clause( 8116, [ =( x( suc( suc( zero ) ), X ), double( rd( cons( i,
% 8.54/8.94 shw( X ) ) ) ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 8.54/8.94 ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 498, [ =( x( suc( suc( zero ) ), X ), double( x( suc( zero ), X ) )
% 8.54/8.94 ) ] )
% 8.54/8.94 , clause( 8117, [ =( x( suc( suc( zero ) ), X ), double( x( suc( zero ), X
% 8.54/8.94 ) ) ) ] )
% 8.54/8.94 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8120, [ =( 'sat_comm'( X, Y ), eq( x( X, Y ), x( Y, X ) ) ) ] )
% 8.54/8.94 , clause( 20, [ =( eq( x( X, Y ), x( Y, X ) ), 'sat_comm'( X, Y ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8121, [ =( 'sat_comm'( suc( suc( zero ) ), X ), eq( double( x( suc(
% 8.54/8.94 zero ), X ) ), x( X, suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 498, [ =( x( suc( suc( zero ) ), X ), double( x( suc( zero ), X )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, clause( 8120, [ =( 'sat_comm'( X, Y ), eq( x( X, Y ), x( Y, X ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, suc(
% 8.54/8.94 suc( zero ) ) ), :=( Y, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8123, [ =( eq( double( x( suc( zero ), X ) ), x( X, suc( suc( zero
% 8.54/8.94 ) ) ) ), 'sat_comm'( suc( suc( zero ) ), X ) ) ] )
% 8.54/8.94 , clause( 8121, [ =( 'sat_comm'( suc( suc( zero ) ), X ), eq( double( x(
% 8.54/8.94 suc( zero ), X ) ), x( X, suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 501, [ =( eq( double( x( suc( zero ), X ) ), x( X, suc( suc( zero )
% 8.54/8.94 ) ) ), 'sat_comm'( suc( suc( zero ) ), X ) ) ] )
% 8.54/8.94 , clause( 8123, [ =( eq( double( x( suc( zero ), X ) ), x( X, suc( suc(
% 8.54/8.94 zero ) ) ) ), 'sat_comm'( suc( suc( zero ) ), X ) ) ] )
% 8.54/8.94 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8126, [ =( eq( X, Y ), eq( suc( X ), suc( Y ) ) ) ] )
% 8.54/8.94 , clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8127, [ =( eq( suc( double( suc( suc( zero ) ) ) ), X ), eq( double(
% 8.54/8.94 suc( suc( suc( zero ) ) ) ), suc( X ) ) ) ] )
% 8.54/8.94 , clause( 342, [ =( suc( suc( double( suc( suc( zero ) ) ) ) ), double( suc(
% 8.54/8.94 suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, clause( 8126, [ =( eq( X, Y ), eq( suc( X ), suc( Y ) ) ) ] )
% 8.54/8.94 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, suc( double( suc(
% 8.54/8.94 suc( zero ) ) ) ) ), :=( Y, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8129, [ =( eq( double( suc( suc( suc( zero ) ) ) ), suc( X ) ), eq(
% 8.54/8.94 suc( double( suc( suc( zero ) ) ) ), X ) ) ] )
% 8.54/8.94 , clause( 8127, [ =( eq( suc( double( suc( suc( zero ) ) ) ), X ), eq(
% 8.54/8.94 double( suc( suc( suc( zero ) ) ) ), suc( X ) ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 523, [ =( eq( double( suc( suc( suc( zero ) ) ) ), suc( X ) ), eq(
% 8.54/8.94 suc( double( suc( suc( zero ) ) ) ), X ) ) ] )
% 8.54/8.94 , clause( 8129, [ =( eq( double( suc( suc( suc( zero ) ) ) ), suc( X ) ),
% 8.54/8.94 eq( suc( double( suc( suc( zero ) ) ) ), X ) ) ] )
% 8.54/8.94 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8133, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero ) ) )
% 8.54/8.94 ) ] )
% 8.54/8.94 , clause( 348, [ =( rd( aux( suc( zero ), bfalse ) ), suc( suc( suc( zero )
% 8.54/8.94 ) ) ) ] )
% 8.54/8.94 , 0, clause( 326, [ =( x( suc( zero ), suc( zero ) ), rd( aux( suc( zero )
% 8.54/8.94 , bfalse ) ) ) ] )
% 8.54/8.94 , 0, 6, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 1002, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero ) ) )
% 8.54/8.94 ) ] )
% 8.54/8.94 , clause( 8133, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8136, [ =( 'sat_comm'( suc( suc( zero ) ), X ), eq( double( x( suc(
% 8.54/8.94 zero ), X ) ), x( X, suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 501, [ =( eq( double( x( suc( zero ), X ) ), x( X, suc( suc( zero
% 8.54/8.94 ) ) ) ), 'sat_comm'( suc( suc( zero ) ), X ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8144, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 double( suc( suc( suc( zero ) ) ) ), x( suc( zero ), suc( suc( zero ) ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , clause( 1002, [ =( x( suc( zero ), suc( zero ) ), suc( suc( suc( zero ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, clause( 8136, [ =( 'sat_comm'( suc( suc( zero ) ), X ), eq( double( x(
% 8.54/8.94 suc( zero ), X ) ), x( X, suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, suc( zero ) )] )
% 8.54/8.94 ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8145, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 double( suc( suc( suc( zero ) ) ) ), suc( double( suc( suc( zero ) ) ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , clause( 324, [ =( x( suc( zero ), suc( suc( zero ) ) ), suc( double( suc(
% 8.54/8.94 suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, clause( 8144, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 double( suc( suc( suc( zero ) ) ) ), x( suc( zero ), suc( suc( zero ) ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, 13, substitution( 0, [] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8146, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq( suc(
% 8.54/8.94 double( suc( suc( zero ) ) ) ), double( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 523, [ =( eq( double( suc( suc( suc( zero ) ) ) ), suc( X ) ), eq(
% 8.54/8.94 suc( double( suc( suc( zero ) ) ) ), X ) ) ] )
% 8.54/8.94 , 0, clause( 8145, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 double( suc( suc( suc( zero ) ) ) ), suc( double( suc( suc( zero ) ) ) )
% 8.54/8.94 ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, double( suc( suc( zero ) ) ) )] ),
% 8.54/8.94 substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8147, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 double( suc( suc( zero ) ) ), suc( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , clause( 185, [ =( eq( suc( X ), double( suc( suc( zero ) ) ) ), eq( X,
% 8.54/8.94 suc( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, clause( 8146, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 suc( double( suc( suc( zero ) ) ) ), double( suc( suc( zero ) ) ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, double( suc( suc( zero ) ) ) )] ),
% 8.54/8.94 substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8148, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq( suc(
% 8.54/8.94 suc( suc( zero ) ) ), suc( suc( zero ) ) ) ) ] )
% 8.54/8.94 , clause( 184, [ =( eq( double( suc( suc( zero ) ) ), suc( X ) ), eq( suc(
% 8.54/8.94 suc( suc( zero ) ) ), X ) ) ] )
% 8.54/8.94 , 0, clause( 8147, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 double( suc( suc( zero ) ) ), suc( suc( suc( zero ) ) ) ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, suc( suc( zero ) ) )] ), substitution( 1
% 8.54/8.94 , [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8149, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq( suc(
% 8.54/8.94 suc( zero ) ), suc( zero ) ) ) ] )
% 8.54/8.94 , clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.94 , 0, clause( 8148, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 suc( suc( suc( zero ) ) ), suc( suc( zero ) ) ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, suc( suc( zero ) ) ), :=( Y, suc( zero )
% 8.54/8.94 )] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8151, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq( suc(
% 8.54/8.94 zero ), zero ) ) ] )
% 8.54/8.94 , clause( 25, [ =( eq( suc( X ), suc( Y ) ), eq( X, Y ) ) ] )
% 8.54/8.94 , 0, clause( 8149, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 suc( suc( zero ) ), suc( zero ) ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, suc( zero ) ), :=( Y, zero )] ),
% 8.54/8.94 substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8152, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), bfalse )
% 8.54/8.94 ] )
% 8.54/8.94 , clause( 27, [ =( eq( suc( X ), zero ), bfalse ) ] )
% 8.54/8.94 , 0, clause( 8151, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), eq(
% 8.54/8.94 suc( zero ), zero ) ) ] )
% 8.54/8.94 , 0, 7, substitution( 0, [ :=( X, zero )] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 7495, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), bfalse )
% 8.54/8.94 ] )
% 8.54/8.94 , clause( 8152, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), bfalse
% 8.54/8.94 ) ] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqswap(
% 8.54/8.94 clause( 8155, [ ~( =( btrue, eq2( 'sat_comm'( X, Y ), bfalse ) ) ) ] )
% 8.54/8.94 , clause( 31, [ ~( =( eq2( 'sat_comm'( X, Y ), bfalse ), btrue ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8157, [ ~( =( btrue, eq2( bfalse, bfalse ) ) ) ] )
% 8.54/8.94 , clause( 7495, [ =( 'sat_comm'( suc( suc( zero ) ), suc( zero ) ), bfalse
% 8.54/8.94 ) ] )
% 8.54/8.94 , 0, clause( 8155, [ ~( =( btrue, eq2( 'sat_comm'( X, Y ), bfalse ) ) ) ]
% 8.54/8.94 )
% 8.54/8.94 , 0, 4, substitution( 0, [] ), substitution( 1, [ :=( X, suc( suc( zero ) )
% 8.54/8.94 ), :=( Y, suc( zero ) )] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 paramod(
% 8.54/8.94 clause( 8158, [ ~( =( btrue, btrue ) ) ] )
% 8.54/8.94 , clause( 29, [ =( eq2( X, X ), btrue ) ] )
% 8.54/8.94 , 0, clause( 8157, [ ~( =( btrue, eq2( bfalse, bfalse ) ) ) ] )
% 8.54/8.94 , 0, 3, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 eqrefl(
% 8.54/8.94 clause( 8159, [] )
% 8.54/8.94 , clause( 8158, [ ~( =( btrue, btrue ) ) ] )
% 8.54/8.94 , 0, substitution( 0, [] )).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 subsumption(
% 8.54/8.94 clause( 7496, [] )
% 8.54/8.94 , clause( 8159, [] )
% 8.54/8.94 , substitution( 0, [] ), permutation( 0, [] ) ).
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 end.
% 8.54/8.94
% 8.54/8.94 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 8.54/8.94
% 8.54/8.94 Memory use:
% 8.54/8.94
% 8.54/8.94 space for terms: 114682
% 8.54/8.94 space for clauses: 837512
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 clauses generated: 23263
% 8.54/8.94 clauses kept: 7497
% 8.54/8.94 clauses selected: 986
% 8.54/8.94 clauses deleted: 233
% 8.54/8.94 clauses inuse deleted: 27
% 8.54/8.94
% 8.54/8.94 subsentry: 2908
% 8.54/8.94 literals s-matched: 1449
% 8.54/8.94 literals matched: 1449
% 8.54/8.94 full subsumption: 0
% 8.54/8.94
% 8.54/8.94 checksum: 596542013
% 8.54/8.94
% 8.54/8.94
% 8.54/8.94 Bliksem ended
%------------------------------------------------------------------------------