%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n010.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:47 PM UTC 2026
% Result : Unsatisfiable 6.83s 7.26s
% Output : Refutation 6.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : bliksem %s
% 0.16/0.34 % Computer : n010.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % DateTime : Tue May 5 11:26:06 EDT 2026
% 0.16/0.34 % CPUTime :
% 5.13/5.55 *** allocated 10000 integers for termspace/termends
% 5.13/5.55 *** allocated 10000 integers for clauses
% 5.13/5.55 *** allocated 10000 integers for justifications
% 5.13/5.55 Bliksem 1.12
% 5.13/5.55
% 5.13/5.55
% 5.13/5.55 Automatic Strategy Selection
% 5.13/5.55
% 5.13/5.55 Clauses:
% 5.13/5.55 [
% 5.13/5.55 [ =( aux( X, Y, btrue ), bfalse ) ],
% 5.13/5.55 [ =( aux( X, Y, bfalse ), unique( Y ) ) ],
% 5.13/5.55 [ =( orb( btrue, X ), btrue ) ],
% 5.13/5.55 [ =( orb( bfalse, X ), X ) ],
% 5.13/5.55 [ =( leqNat( z, X ), btrue ) ],
% 5.13/5.55 [ =( leqNat( s( X ), z ), bfalse ) ],
% 5.13/5.55 [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ],
% 5.13/5.55 [ =( lengthNat( nil ), z ) ],
% 5.13/5.55 [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ],
% 5.13/5.55 [ =( impl( btrue, X ), X ) ],
% 5.13/5.55 [ =( impl( bfalse, X ), btrue ) ],
% 5.13/5.55 [ =( elemNat( X, nil ), bfalse ) ],
% 5.13/5.55 [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat( X, Z ) ) ) ]
% 5.13/5.55 ,
% 5.13/5.55 [ =( unique( nil ), btrue ) ],
% 5.13/5.55 [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) ) ],
% 5.13/5.55 [ =( append( nil, X ), X ) ],
% 5.13/5.55 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 5.13/5.55 [ =( rev( nil ), nil ) ],
% 5.13/5.55 [ =( rev( cons( X, Y ) ), append( rev( Y ), cons( X, nil ) ) ) ],
% 5.13/5.55 [ =( andb( btrue, X ), X ) ],
% 5.13/5.55 [ =( andb( bfalse, X ), bfalse ) ],
% 5.13/5.55 [ =( sorted( nil ), btrue ) ],
% 5.13/5.55 [ =( sorted( cons( X, nil ) ), btrue ) ],
% 5.13/5.55 [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y ), sorted(
% 5.13/5.55 cons( Y, Z ) ) ) ) ],
% 5.13/5.55 [ =( 'psorted_rev'( X ), impl( eq2( sorted( rev( X ) ), btrue ), impl(
% 5.13/5.55 eq2( unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s( z ) ) )
% 5.13/5.55 ), btrue ) ) ) ) ],
% 5.13/5.55 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 5.13/5.55 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 5.13/5.55 [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ],
% 5.13/5.55 [ =( eq( z, s( X ) ), bfalse ) ],
% 5.13/5.55 [ =( eq( s( X ), z ), bfalse ) ],
% 5.13/5.55 [ =( eq( X, X ), btrue ) ],
% 5.13/5.55 [ =( eq2( X, X ), btrue ) ],
% 5.13/5.55 [ ~( =( eq2( 'psorted_rev'( X ), bfalse ), btrue ) ) ]
% 5.13/5.55 ] .
% 5.13/5.55
% 5.13/5.55
% 5.13/5.55 percentage equality = 1.000000, percentage horn = 1.000000
% 5.13/5.55 This is a pure equality problem
% 5.13/5.55
% 5.13/5.55
% 5.13/5.55
% 5.13/5.55 Options Used:
% 5.13/5.55
% 5.13/5.55 useres = 1
% 5.13/5.55 useparamod = 1
% 5.13/5.55 useeqrefl = 1
% 5.13/5.55 useeqfact = 1
% 5.13/5.55 usefactor = 1
% 5.13/5.55 usesimpsplitting = 0
% 5.13/5.55 usesimpdemod = 5
% 5.13/5.55 usesimpres = 3
% 5.13/5.55
% 5.13/5.55 resimpinuse = 1000
% 5.13/5.55 resimpclauses = 20000
% 5.13/5.55 substype = eqrewr
% 5.13/5.55 backwardsubs = 1
% 5.13/5.55 selectoldest = 5
% 5.13/5.55
% 5.13/5.55 litorderings [0] = split
% 5.13/5.55 litorderings [1] = extend the termordering, first sorting on arguments
% 5.13/5.55
% 5.13/5.55 termordering = kbo
% 5.13/5.55
% 5.13/5.55 litapriori = 0
% 5.13/5.55 termapriori = 1
% 5.13/5.55 litaposteriori = 0
% 5.13/5.55 termaposteriori = 0
% 5.13/5.55 demodaposteriori = 0
% 5.13/5.55 ordereqreflfact = 0
% 5.13/5.55
% 5.13/5.55 litselect = negord
% 5.13/5.55
% 5.13/5.55 maxweight = 15
% 5.13/5.55 maxdepth = 30000
% 5.13/5.55 maxlength = 115
% 5.13/5.55 maxnrvars = 195
% 5.13/5.55 excuselevel = 1
% 5.13/5.55 increasemaxweight = 1
% 5.13/5.55
% 5.13/5.55 maxselected = 10000000
% 5.13/5.55 maxnrclauses = 10000000
% 5.13/5.55
% 5.13/5.55 showgenerated = 0
% 5.13/5.55 showkept = 0
% 5.13/5.55 showselected = 0
% 5.13/5.55 showdeleted = 0
% 5.13/5.55 showresimp = 1
% 5.13/5.55 showstatus = 2000
% 5.13/5.55
% 5.13/5.55 prologoutput = 1
% 5.13/5.55 nrgoals = 5000000
% 5.13/5.55 totalproof = 1
% 5.13/5.55
% 5.13/5.55 Symbols occurring in the translation:
% 5.13/5.55
% 5.13/5.55 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.13/5.55 . [1, 2] (w:1, o:31, a:1, s:1, b:0),
% 5.13/5.55 ! [4, 1] (w:0, o:20, a:1, s:1, b:0),
% 5.13/5.55 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.13/5.55 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.13/5.55 btrue [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 5.13/5.55 aux [42, 3] (w:1, o:65, a:1, s:1, b:0),
% 5.13/5.55 bfalse [43, 0] (w:1, o:13, a:1, s:1, b:0),
% 5.13/5.55 unique [44, 1] (w:1, o:25, a:1, s:1, b:0),
% 5.13/5.55 orb [46, 2] (w:1, o:56, a:1, s:1, b:0),
% 5.13/5.55 z [47, 0] (w:1, o:15, a:1, s:1, b:0),
% 5.13/5.55 leqNat [48, 2] (w:1, o:57, a:1, s:1, b:0),
% 5.13/5.55 s [50, 1] (w:1, o:27, a:1, s:1, b:0),
% 5.13/5.55 nil [52, 0] (w:1, o:19, a:1, s:1, b:0),
% 5.13/5.55 lengthNat [53, 1] (w:1, o:28, a:1, s:1, b:0),
% 5.13/5.55 cons [54, 2] (w:1, o:58, a:1, s:1, b:0),
% 5.13/5.55 impl [55, 2] (w:1, o:59, a:1, s:1, b:0),
% 5.13/5.55 elemNat [57, 2] (w:1, o:60, a:1, s:1, b:0),
% 5.13/5.55 eq [58, 2] (w:1, o:61, a:1, s:1, b:0),
% 5.13/5.55 append [59, 2] (w:1, o:62, a:1, s:1, b:0),
% 5.13/5.55 rev [60, 1] (w:1, o:26, a:1, s:1, b:0),
% 5.13/5.55 andb [61, 2] (w:1, o:63, a:1, s:1, b:0),
% 5.13/5.55 sorted [62, 1] (w:1, o:29, a:1, s:1, b:0),
% 5.13/5.55 'psorted_rev' [64, 1] (w:1, o:30, a:1, s:1, b:0),
% 6.83/7.26 eq2 [65, 2] (w:1, o:64, a:1, s:1, b:0).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 15
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 257
% 6.83/7.26 Kept: 57
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 16
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 16
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 272
% 6.83/7.26 Kept: 59
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 17
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 17
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 369
% 6.83/7.26 Kept: 72
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 18
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 18
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 444
% 6.83/7.26 Kept: 82
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 19
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 19
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 714
% 6.83/7.26 Kept: 95
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 20
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 20
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 811
% 6.83/7.26 Kept: 102
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 21
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 21
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 1257
% 6.83/7.26 Kept: 134
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 22
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 22
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 1650
% 6.83/7.26 Kept: 154
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 23
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 23
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 2568
% 6.83/7.26 Kept: 184
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 24
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 24
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 3170
% 6.83/7.26 Kept: 209
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 25
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 25
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 4579
% 6.83/7.26 Kept: 271
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 26
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 26
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 6299
% 6.83/7.26 Kept: 319
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 27
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 27
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 10321
% 6.83/7.26 Kept: 378
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 28
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 28
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 12245
% 6.83/7.26 Kept: 429
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 29
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 29
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 21228
% 6.83/7.26 Kept: 641
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 30
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 30
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 32902
% 6.83/7.26 Kept: 768
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 31
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 31
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 50081
% 6.83/7.26 Kept: 936
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 32
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 32
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 67454
% 6.83/7.26 Kept: 1116
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 33
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 33
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 107874
% 6.83/7.26 Kept: 1460
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 34
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26 Failed to find proof!
% 6.83/7.26 maxweight = 34
% 6.83/7.26 maxnrclauses = 10000000
% 6.83/7.26 Generated: 150965
% 6.83/7.26 Kept: 1698
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 The strategy used was not complete!
% 6.83/7.26
% 6.83/7.26 Increased maxweight to 35
% 6.83/7.26
% 6.83/7.26 Starting Search:
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 Intermediate Status:
% 6.83/7.26 Generated: 116726
% 6.83/7.26 Kept: 2000
% 6.83/7.26 Inuse: 1289
% 6.83/7.26 Deleted: 237
% 6.83/7.26 Deletedinuse: 4
% 6.83/7.26
% 6.83/7.26 Resimplifying inuse:
% 6.83/7.26 Done
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 Bliksems!, er is een bewijs:
% 6.83/7.26 % SZS status Unsatisfiable
% 6.83/7.26 % SZS output start Refutation
% 6.83/7.26
% 6.83/7.26 clause( 1, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 3, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 4, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 5, [ =( leqNat( s( X ), z ), bfalse ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 8, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 9, [ =( impl( btrue, X ), X ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 11, [ =( elemNat( X, nil ), bfalse ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y, Z
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 13, [ =( unique( nil ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 14, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 .
% 6.83/7.26 clause( 15, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 .
% 6.83/7.26 clause( 17, [ =( rev( nil ), nil ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 18, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 19, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 22, [ =( sorted( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 24, [ =( impl( eq2( sorted( rev( X ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s( z ) ) ) ), btrue ) )
% 6.83/7.26 ), 'psorted_rev'( X ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 25, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 27, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 29, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 31, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 32, [ ~( =( eq2( 'psorted_rev'( X ), bfalse ), btrue ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 33, [ =( rev( cons( X, nil ) ), cons( X, nil ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 34, [ =( rev( cons( Y, cons( X, nil ) ) ), cons( X, cons( Y, nil )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 37, [ =( elemNat( s( X ), cons( z, Y ) ), elemNat( s( X ), Y ) ) ]
% 6.83/7.26 )
% 6.83/7.26 .
% 6.83/7.26 clause( 38, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse ) )
% 6.83/7.26 ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 42, [ =( elemNat( s( X ), cons( Z, cons( z, Y ) ) ), elemNat( s( X
% 6.83/7.26 ), cons( Z, Y ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 43, [ =( orb( eq( X, Z ), orb( eq( X, Y ), bfalse ) ), elemNat( X,
% 6.83/7.26 cons( Z, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 44, [ =( aux( X, cons( Y, nil ), orb( eq( X, Y ), bfalse ) ),
% 6.83/7.26 unique( cons( X, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 48, [ =( unique( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 49, [ =( rev( cons( Z, cons( X, cons( Y, nil ) ) ) ), cons( Y, cons(
% 6.83/7.26 X, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 52, [ =( andb( leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ),
% 6.83/7.26 sorted( cons( s( X ), cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 53, [ =( sorted( cons( Y, cons( X, nil ) ) ), andb( leqNat( Y, X )
% 6.83/7.26 , btrue ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 58, [ =( andb( leqNat( Z, X ), andb( leqNat( X, Y ), btrue ) ),
% 6.83/7.26 sorted( cons( Z, cons( X, cons( Y, nil ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 64, [ =( impl( eq2( sorted( rev( cons( X, Y ) ) ), btrue ), impl(
% 6.83/7.26 eq2( unique( cons( X, Y ) ), btrue ), eq2( leqNat( lengthNat( Y ), s( s(
% 6.83/7.26 z ) ) ), btrue ) ) ), 'psorted_rev'( cons( X, Y ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 67, [ =( aux( s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ),
% 6.83/7.26 cons( Y, Z ) ) ), unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 .
% 6.83/7.26 clause( 68, [ =( elemNat( s( X ), cons( T, cons( Y, cons( z, Z ) ) ) ),
% 6.83/7.26 elemNat( s( X ), cons( T, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 82, [ =( rev( cons( T, cons( X, cons( Y, cons( Z, nil ) ) ) ) ),
% 6.83/7.26 cons( Z, cons( Y, cons( X, cons( T, nil ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 83, [ =( orb( eq( s( X ), Z ), orb( eq( X, Y ), bfalse ) ), elemNat(
% 6.83/7.26 s( X ), cons( Z, cons( s( Y ), nil ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 86, [ =( unique( cons( s( X ), cons( z, nil ) ) ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 125, [ =( andb( leqNat( Z, s( X ) ), andb( leqNat( X, Y ), btrue )
% 6.83/7.26 ), sorted( cons( Z, cons( s( X ), cons( s( Y ), nil ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 130, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), sorted( cons(
% 6.83/7.26 s( X ), Y ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 141, [ =( andb( leqNat( Z, s( z ) ), sorted( cons( s( X ), Y ) ) )
% 6.83/7.26 , sorted( cons( Z, cons( s( z ), cons( s( X ), Y ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 165, [ =( aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat(
% 6.83/7.26 s( X ), cons( Y, cons( Z, T ) ) ) ), unique( cons( s( X ), cons( Y, cons(
% 6.83/7.26 Z, cons( z, T ) ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 183, [ =( impl( eq2( sorted( rev( cons( Z, cons( X, Y ) ) ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( cons( Z, cons( X, Y ) ) ), btrue ), eq2(
% 6.83/7.26 leqNat( lengthNat( Y ), s( z ) ), btrue ) ) ), 'psorted_rev'( cons( Z,
% 6.83/7.26 cons( X, Y ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 205, [ =( aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X ),
% 6.83/7.26 Y ), bfalse ) ), unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 .
% 6.83/7.26 clause( 214, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil ) ) ),
% 6.83/7.26 elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 319, [ =( sorted( cons( Y, cons( s( z ), cons( s( X ), nil ) ) ) )
% 6.83/7.26 , andb( leqNat( Y, s( z ) ), btrue ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 364, [ =( andb( leqNat( Z, s( s( X ) ) ), andb( leqNat( X, Y ),
% 6.83/7.26 btrue ) ), sorted( cons( Z, cons( s( s( X ) ), cons( s( s( Y ) ), nil ) )
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 511, [ =( aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X,
% 6.83/7.26 Y ), bfalse ) ), unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 537, [ =( sorted( cons( Y, cons( s( s( z ) ), cons( s( s( X ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( Y, s( s( z ) ) ), btrue ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 540, [ =( sorted( cons( Z, cons( X, cons( s( s( z ) ), cons( s( s(
% 6.83/7.26 Y ) ), nil ) ) ) ) ), sorted( cons( Z, cons( X, cons( s( s( z ) ), nil )
% 6.83/7.26 ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 582, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil ) )
% 6.83/7.26 ) ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 764, [ =( aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil ) )
% 6.83/7.26 ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ), unique( cons( s( X ), cons(
% 6.83/7.26 s( Y ), cons( s( Z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 1833, [ =( aux( s( s( X ) ), cons( s( Y ), cons( s( z ), cons( z,
% 6.83/7.26 nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ), unique( cons( s( s( X ) ),
% 6.83/7.26 cons( s( Y ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 2018, [ =( aux( s( s( X ) ), cons( s( s( Y ) ), cons( s( z ), cons(
% 6.83/7.26 z, nil ) ) ), orb( eq( X, Y ), bfalse ) ), unique( cons( s( s( X ) ),
% 6.83/7.26 cons( s( s( Y ) ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 2072, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), btrue ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 2073, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), bfalse ) ] )
% 6.83/7.26 .
% 6.83/7.26 clause( 2074, [] )
% 6.83/7.26 .
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 % SZS output end Refutation
% 6.83/7.26 found a proof!
% 6.83/7.26
% 6.83/7.26 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 6.83/7.26
% 6.83/7.26 initialclauses(
% 6.83/7.26 [ clause( 2076, [ =( aux( X, Y, btrue ), bfalse ) ] )
% 6.83/7.26 , clause( 2077, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , clause( 2078, [ =( orb( btrue, X ), btrue ) ] )
% 6.83/7.26 , clause( 2079, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , clause( 2080, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 , clause( 2081, [ =( leqNat( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , clause( 2082, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , clause( 2083, [ =( lengthNat( nil ), z ) ] )
% 6.83/7.26 , clause( 2084, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.26 , clause( 2085, [ =( impl( btrue, X ), X ) ] )
% 6.83/7.26 , clause( 2086, [ =( impl( bfalse, X ), btrue ) ] )
% 6.83/7.26 , clause( 2087, [ =( elemNat( X, nil ), bfalse ) ] )
% 6.83/7.26 , clause( 2088, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat(
% 6.83/7.26 X, Z ) ) ) ] )
% 6.83/7.26 , clause( 2089, [ =( unique( nil ), btrue ) ] )
% 6.83/7.26 , clause( 2090, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , clause( 2091, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , clause( 2092, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , clause( 2093, [ =( rev( nil ), nil ) ] )
% 6.83/7.26 , clause( 2094, [ =( rev( cons( X, Y ) ), append( rev( Y ), cons( X, nil )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , clause( 2095, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 , clause( 2096, [ =( andb( bfalse, X ), bfalse ) ] )
% 6.83/7.26 , clause( 2097, [ =( sorted( nil ), btrue ) ] )
% 6.83/7.26 , clause( 2098, [ =( sorted( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , clause( 2099, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y
% 6.83/7.26 ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2100, [ =( 'psorted_rev'( X ), impl( eq2( sorted( rev( X ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s(
% 6.83/7.26 s( s( z ) ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 2101, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 6.83/7.26 , clause( 2102, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 6.83/7.26 , clause( 2103, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , clause( 2104, [ =( eq( z, s( X ) ), bfalse ) ] )
% 6.83/7.26 , clause( 2105, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , clause( 2106, [ =( eq( X, X ), btrue ) ] )
% 6.83/7.26 , clause( 2107, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.26 , clause( 2108, [ ~( =( eq2( 'psorted_rev'( X ), bfalse ), btrue ) ) ] )
% 6.83/7.26 ] ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 1, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , clause( 2077, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 3, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , clause( 2079, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 4, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 , clause( 2080, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 5, [ =( leqNat( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , clause( 2081, [ =( leqNat( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , clause( 2082, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 8, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.26 , clause( 2084, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 9, [ =( impl( btrue, X ), X ) ] )
% 6.83/7.26 , clause( 2085, [ =( impl( btrue, X ), X ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 11, [ =( elemNat( X, nil ), bfalse ) ] )
% 6.83/7.26 , clause( 2087, [ =( elemNat( X, nil ), bfalse ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2176, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , clause( 2088, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat(
% 6.83/7.26 X, Z ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y, Z
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , clause( 2176, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons(
% 6.83/7.26 Y, Z ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 13, [ =( unique( nil ), btrue ) ] )
% 6.83/7.26 , clause( 2089, [ =( unique( nil ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2205, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2090, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 14, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2205, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 15, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , clause( 2091, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2092, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 17, [ =( rev( nil ), nil ) ] )
% 6.83/7.26 , clause( 2093, [ =( rev( nil ), nil ) ] )
% 6.83/7.26 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2275, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 2094, [ =( rev( cons( X, Y ) ), append( rev( Y ), cons( X, nil )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 18, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , clause( 2275, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 19, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 , clause( 2095, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 22, [ =( sorted( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , clause( 2098, [ =( sorted( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2342, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2099, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y
% 6.83/7.26 ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2342, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2367, [ =( impl( eq2( sorted( rev( X ) ), btrue ), impl( eq2(
% 6.83/7.26 unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s( z ) ) ) ),
% 6.83/7.26 btrue ) ) ), 'psorted_rev'( X ) ) ] )
% 6.83/7.26 , clause( 2100, [ =( 'psorted_rev'( X ), impl( eq2( sorted( rev( X ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s(
% 6.83/7.26 s( s( z ) ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 24, [ =( impl( eq2( sorted( rev( X ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s( z ) ) ) ), btrue ) )
% 6.83/7.26 ), 'psorted_rev'( X ) ) ] )
% 6.83/7.26 , clause( 2367, [ =( impl( eq2( sorted( rev( X ) ), btrue ), impl( eq2(
% 6.83/7.26 unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s( z ) ) ) ),
% 6.83/7.26 btrue ) ) ), 'psorted_rev'( X ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 25, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 6.83/7.26 , clause( 2101, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 6.83/7.26 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 27, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , clause( 2103, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 29, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , clause( 2105, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 31, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.26 , clause( 2107, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 32, [ ~( =( eq2( 'psorted_rev'( X ), bfalse ), btrue ) ) ] )
% 6.83/7.26 , clause( 2108, [ ~( =( eq2( 'psorted_rev'( X ), bfalse ), btrue ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2518, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 18, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2520, [ =( rev( cons( X, nil ) ), append( nil, cons( X, nil ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 17, [ =( rev( nil ), nil ) ] )
% 6.83/7.26 , 0, clause( 2518, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, 6, substitution( 0, [] ), substitution( 1, [ :=( X, nil ), :=( Y, X )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2521, [ =( rev( cons( X, nil ) ), cons( X, nil ) ) ] )
% 6.83/7.26 , clause( 15, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2520, [ =( rev( cons( X, nil ) ), append( nil, cons( X, nil )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, 5, substitution( 0, [ :=( X, cons( X, nil ) )] ), substitution( 1, [
% 6.83/7.26 :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 33, [ =( rev( cons( X, nil ) ), cons( X, nil ) ) ] )
% 6.83/7.26 , clause( 2521, [ =( rev( cons( X, nil ) ), cons( X, nil ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2524, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 18, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2528, [ =( rev( cons( X, cons( Y, nil ) ) ), append( cons( Y, nil )
% 6.83/7.26 , cons( X, nil ) ) ) ] )
% 6.83/7.26 , clause( 33, [ =( rev( cons( X, nil ) ), cons( X, nil ) ) ] )
% 6.83/7.26 , 0, clause( 2524, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, 8, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, cons( Y
% 6.83/7.26 , nil ) ), :=( Y, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2529, [ =( rev( cons( X, cons( Y, nil ) ) ), cons( Y, append( nil,
% 6.83/7.26 cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, clause( 2528, [ =( rev( cons( X, cons( Y, nil ) ) ), append( cons( Y,
% 6.83/7.26 nil ), cons( X, nil ) ) ) ] )
% 6.83/7.26 , 0, 7, substitution( 0, [ :=( X, Y ), :=( Y, nil ), :=( Z, cons( X, nil )
% 6.83/7.26 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2530, [ =( rev( cons( X, cons( Y, nil ) ) ), cons( Y, cons( X, nil
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , clause( 15, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2529, [ =( rev( cons( X, cons( Y, nil ) ) ), cons( Y, append(
% 6.83/7.26 nil, cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , 0, 9, substitution( 0, [ :=( X, cons( X, nil ) )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 34, [ =( rev( cons( Y, cons( X, nil ) ) ), cons( X, cons( Y, nil )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , clause( 2530, [ =( rev( cons( X, cons( Y, nil ) ) ), cons( Y, cons( X,
% 6.83/7.26 nil ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2533, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat( X
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2535, [ =( elemNat( s( X ), cons( z, Y ) ), orb( bfalse, elemNat( s(
% 6.83/7.26 X ), Y ) ) ) ] )
% 6.83/7.26 , clause( 29, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , 0, clause( 2533, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ),
% 6.83/7.26 elemNat( X, Z ) ) ) ] )
% 6.83/7.26 , 0, 8, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, s( X )
% 6.83/7.26 ), :=( Y, z ), :=( Z, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2536, [ =( elemNat( s( X ), cons( z, Y ) ), elemNat( s( X ), Y ) )
% 6.83/7.26 ] )
% 6.83/7.26 , clause( 3, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2535, [ =( elemNat( s( X ), cons( z, Y ) ), orb( bfalse,
% 6.83/7.26 elemNat( s( X ), Y ) ) ) ] )
% 6.83/7.26 , 0, 7, substitution( 0, [ :=( X, elemNat( s( X ), Y ) )] ), substitution(
% 6.83/7.26 1, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 37, [ =( elemNat( s( X ), cons( z, Y ) ), elemNat( s( X ), Y ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2536, [ =( elemNat( s( X ), cons( z, Y ) ), elemNat( s( X ), Y )
% 6.83/7.26 ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2539, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat( X
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2540, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 11, [ =( elemNat( X, nil ), bfalse ) ] )
% 6.83/7.26 , 0, clause( 2539, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ),
% 6.83/7.26 elemNat( X, Z ) ) ) ] )
% 6.83/7.26 , 0, 10, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 6.83/7.26 :=( Y, Y ), :=( Z, nil )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 38, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse ) )
% 6.83/7.26 ] )
% 6.83/7.26 , clause( 2540, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2543, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat( X
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2546, [ =( elemNat( s( X ), cons( Y, cons( z, Z ) ) ), orb( eq( s(
% 6.83/7.26 X ), Y ), elemNat( s( X ), Z ) ) ) ] )
% 6.83/7.26 , clause( 37, [ =( elemNat( s( X ), cons( z, Y ) ), elemNat( s( X ), Y ) )
% 6.83/7.26 ] )
% 6.83/7.26 , 0, clause( 2543, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ),
% 6.83/7.26 elemNat( X, Z ) ) ) ] )
% 6.83/7.26 , 0, 14, substitution( 0, [ :=( X, X ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, s( X ) ), :=( Y, Y ), :=( Z, cons( z, Z ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2547, [ =( elemNat( s( X ), cons( Y, cons( z, Z ) ) ), elemNat( s(
% 6.83/7.26 X ), cons( Y, Z ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, clause( 2546, [ =( elemNat( s( X ), cons( Y, cons( z, Z ) ) ), orb( eq(
% 6.83/7.26 s( X ), Y ), elemNat( s( X ), Z ) ) ) ] )
% 6.83/7.26 , 0, 9, substitution( 0, [ :=( X, s( X ) ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 42, [ =( elemNat( s( X ), cons( Z, cons( z, Y ) ) ), elemNat( s( X
% 6.83/7.26 ), cons( Z, Y ) ) ) ] )
% 6.83/7.26 , clause( 2547, [ =( elemNat( s( X ), cons( Y, cons( z, Z ) ) ), elemNat( s(
% 6.83/7.26 X ), cons( Y, Z ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2550, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat( X
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2552, [ =( elemNat( X, cons( Y, cons( Z, nil ) ) ), orb( eq( X, Y )
% 6.83/7.26 , orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 38, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, clause( 2550, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ),
% 6.83/7.26 elemNat( X, Z ) ) ) ] )
% 6.83/7.26 , 0, 12, substitution( 0, [ :=( X, X ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, Y ), :=( Z, cons( Z, nil ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2554, [ =( orb( eq( X, Y ), orb( eq( X, Z ), bfalse ) ), elemNat( X
% 6.83/7.26 , cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2552, [ =( elemNat( X, cons( Y, cons( Z, nil ) ) ), orb( eq( X, Y
% 6.83/7.26 ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 43, [ =( orb( eq( X, Z ), orb( eq( X, Y ), bfalse ) ), elemNat( X,
% 6.83/7.26 cons( Z, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2554, [ =( orb( eq( X, Y ), orb( eq( X, Z ), bfalse ) ), elemNat(
% 6.83/7.26 X, cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2556, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 14, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2557, [ =( unique( cons( X, cons( Y, nil ) ) ), aux( X, cons( Y,
% 6.83/7.26 nil ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 38, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, clause( 2556, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, 12, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, cons( Y, nil ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2558, [ =( aux( X, cons( Y, nil ), orb( eq( X, Y ), bfalse ) ),
% 6.83/7.26 unique( cons( X, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2557, [ =( unique( cons( X, cons( Y, nil ) ) ), aux( X, cons( Y,
% 6.83/7.26 nil ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 44, [ =( aux( X, cons( Y, nil ), orb( eq( X, Y ), bfalse ) ),
% 6.83/7.26 unique( cons( X, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2558, [ =( aux( X, cons( Y, nil ), orb( eq( X, Y ), bfalse ) ),
% 6.83/7.26 unique( cons( X, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2560, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 14, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2563, [ =( unique( cons( X, nil ) ), aux( X, nil, bfalse ) ) ] )
% 6.83/7.26 , clause( 11, [ =( elemNat( X, nil ), bfalse ) ] )
% 6.83/7.26 , 0, clause( 2560, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, 8, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 6.83/7.26 :=( Y, nil )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2564, [ =( unique( cons( X, nil ) ), unique( nil ) ) ] )
% 6.83/7.26 , clause( 1, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , 0, clause( 2563, [ =( unique( cons( X, nil ) ), aux( X, nil, bfalse ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, nil )] ), substitution( 1, [
% 6.83/7.26 :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2565, [ =( unique( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , clause( 13, [ =( unique( nil ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2564, [ =( unique( cons( X, nil ) ), unique( nil ) ) ] )
% 6.83/7.26 , 0, 5, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 48, [ =( unique( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , clause( 2565, [ =( unique( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2568, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 18, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2573, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), append(
% 6.83/7.26 cons( Z, cons( Y, nil ) ), cons( X, nil ) ) ) ] )
% 6.83/7.26 , clause( 34, [ =( rev( cons( Y, cons( X, nil ) ) ), cons( X, cons( Y, nil
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, clause( 2568, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, 10, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, cons( Y, cons( Z, nil ) ) ), :=( Y, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2574, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), cons( Z,
% 6.83/7.26 append( cons( Y, nil ), cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, clause( 2573, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), append(
% 6.83/7.26 cons( Z, cons( Y, nil ) ), cons( X, nil ) ) ) ] )
% 6.83/7.26 , 0, 9, substitution( 0, [ :=( X, Z ), :=( Y, cons( Y, nil ) ), :=( Z, cons(
% 6.83/7.26 X, nil ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2576, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), cons( Z,
% 6.83/7.26 cons( Y, append( nil, cons( X, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, clause( 2574, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), cons(
% 6.83/7.26 Z, append( cons( Y, nil ), cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , 0, 11, substitution( 0, [ :=( X, Y ), :=( Y, nil ), :=( Z, cons( X, nil )
% 6.83/7.26 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2577, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), cons( Z,
% 6.83/7.26 cons( Y, cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 15, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2576, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), cons(
% 6.83/7.26 Z, cons( Y, append( nil, cons( X, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, 13, substitution( 0, [ :=( X, cons( X, nil ) )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 49, [ =( rev( cons( Z, cons( X, cons( Y, nil ) ) ) ), cons( Y, cons(
% 6.83/7.26 X, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2577, [ =( rev( cons( X, cons( Y, cons( Z, nil ) ) ) ), cons( Z,
% 6.83/7.26 cons( Y, cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2580, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y )
% 6.83/7.26 , sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2581, [ =( sorted( cons( s( X ), cons( s( Y ), Z ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2580, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X
% 6.83/7.26 , Y ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, 10, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, s( X ) ), :=( Y, s( Y ) ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2582, [ =( andb( leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ),
% 6.83/7.26 sorted( cons( s( X ), cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2581, [ =( sorted( cons( s( X ), cons( s( Y ), Z ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 52, [ =( andb( leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ),
% 6.83/7.26 sorted( cons( s( X ), cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2582, [ =( andb( leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ),
% 6.83/7.26 sorted( cons( s( X ), cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2584, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y )
% 6.83/7.26 , sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2585, [ =( sorted( cons( X, cons( Y, nil ) ) ), andb( leqNat( X, Y
% 6.83/7.26 ), btrue ) ) ] )
% 6.83/7.26 , clause( 22, [ =( sorted( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2584, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X
% 6.83/7.26 , Y ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, 11, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 6.83/7.26 :=( Y, Y ), :=( Z, nil )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 53, [ =( sorted( cons( Y, cons( X, nil ) ) ), andb( leqNat( Y, X )
% 6.83/7.26 , btrue ) ) ] )
% 6.83/7.26 , clause( 2585, [ =( sorted( cons( X, cons( Y, nil ) ) ), andb( leqNat( X,
% 6.83/7.26 Y ), btrue ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2588, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y )
% 6.83/7.26 , sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2590, [ =( sorted( cons( X, cons( Y, cons( Z, nil ) ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , clause( 53, [ =( sorted( cons( Y, cons( X, nil ) ) ), andb( leqNat( Y, X
% 6.83/7.26 ), btrue ) ) ] )
% 6.83/7.26 , 0, clause( 2588, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X
% 6.83/7.26 , Y ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, 13, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, Y ), :=( Z, cons( Z, nil ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2592, [ =( andb( leqNat( X, Y ), andb( leqNat( Y, Z ), btrue ) ),
% 6.83/7.26 sorted( cons( X, cons( Y, cons( Z, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2590, [ =( sorted( cons( X, cons( Y, cons( Z, nil ) ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 58, [ =( andb( leqNat( Z, X ), andb( leqNat( X, Y ), btrue ) ),
% 6.83/7.26 sorted( cons( Z, cons( X, cons( Y, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2592, [ =( andb( leqNat( X, Y ), andb( leqNat( Y, Z ), btrue ) )
% 6.83/7.26 , sorted( cons( X, cons( Y, cons( Z, nil ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2594, [ =( 'psorted_rev'( X ), impl( eq2( sorted( rev( X ) ), btrue
% 6.83/7.26 ), impl( eq2( unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s(
% 6.83/7.26 z ) ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 24, [ =( impl( eq2( sorted( rev( X ) ), btrue ), impl( eq2(
% 6.83/7.26 unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s( s( s( z ) ) ) ),
% 6.83/7.26 btrue ) ) ), 'psorted_rev'( X ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2596, [ =( 'psorted_rev'( cons( X, Y ) ), impl( eq2( sorted( rev(
% 6.83/7.26 cons( X, Y ) ) ), btrue ), impl( eq2( unique( cons( X, Y ) ), btrue ),
% 6.83/7.26 eq2( leqNat( s( lengthNat( Y ) ), s( s( s( z ) ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 8, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.26 , 0, clause( 2594, [ =( 'psorted_rev'( X ), impl( eq2( sorted( rev( X ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( X ), btrue ), eq2( leqNat( lengthNat( X ), s(
% 6.83/7.26 s( s( z ) ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 22, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, cons( X, Y ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2597, [ =( 'psorted_rev'( cons( X, Y ) ), impl( eq2( sorted( rev(
% 6.83/7.26 cons( X, Y ) ) ), btrue ), impl( eq2( unique( cons( X, Y ) ), btrue ),
% 6.83/7.26 eq2( leqNat( lengthNat( Y ), s( s( z ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2596, [ =( 'psorted_rev'( cons( X, Y ) ), impl( eq2( sorted(
% 6.83/7.26 rev( cons( X, Y ) ) ), btrue ), impl( eq2( unique( cons( X, Y ) ), btrue
% 6.83/7.26 ), eq2( leqNat( s( lengthNat( Y ) ), s( s( s( z ) ) ) ), btrue ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, 21, substitution( 0, [ :=( X, lengthNat( Y ) ), :=( Y, s( s( z ) ) )] )
% 6.83/7.26 , substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2598, [ =( impl( eq2( sorted( rev( cons( X, Y ) ) ), btrue ), impl(
% 6.83/7.26 eq2( unique( cons( X, Y ) ), btrue ), eq2( leqNat( lengthNat( Y ), s( s(
% 6.83/7.26 z ) ) ), btrue ) ) ), 'psorted_rev'( cons( X, Y ) ) ) ] )
% 6.83/7.26 , clause( 2597, [ =( 'psorted_rev'( cons( X, Y ) ), impl( eq2( sorted( rev(
% 6.83/7.26 cons( X, Y ) ) ), btrue ), impl( eq2( unique( cons( X, Y ) ), btrue ),
% 6.83/7.26 eq2( leqNat( lengthNat( Y ), s( s( z ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 64, [ =( impl( eq2( sorted( rev( cons( X, Y ) ) ), btrue ), impl(
% 6.83/7.26 eq2( unique( cons( X, Y ) ), btrue ), eq2( leqNat( lengthNat( Y ), s( s(
% 6.83/7.26 z ) ) ), btrue ) ) ), 'psorted_rev'( cons( X, Y ) ) ) ] )
% 6.83/7.26 , clause( 2598, [ =( impl( eq2( sorted( rev( cons( X, Y ) ) ), btrue ),
% 6.83/7.26 impl( eq2( unique( cons( X, Y ) ), btrue ), eq2( leqNat( lengthNat( Y ),
% 6.83/7.26 s( s( z ) ) ), btrue ) ) ), 'psorted_rev'( cons( X, Y ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2600, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 14, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2601, [ =( unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ), aux(
% 6.83/7.26 s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ), cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 42, [ =( elemNat( s( X ), cons( Z, cons( z, Y ) ) ), elemNat( s(
% 6.83/7.26 X ), cons( Z, Y ) ) ) ] )
% 6.83/7.26 , 0, clause( 2600, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, 18, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 6.83/7.26 substitution( 1, [ :=( X, s( X ) ), :=( Y, cons( Y, cons( z, Z ) ) )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2602, [ =( aux( s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ),
% 6.83/7.26 cons( Y, Z ) ) ), unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2601, [ =( unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ), aux(
% 6.83/7.26 s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ), cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 67, [ =( aux( s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ),
% 6.83/7.26 cons( Y, Z ) ) ), unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2602, [ =( aux( s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X )
% 6.83/7.26 , cons( Y, Z ) ) ), unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2604, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ), elemNat( X
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2607, [ =( elemNat( s( X ), cons( Y, cons( Z, cons( z, T ) ) ) ),
% 6.83/7.26 orb( eq( s( X ), Y ), elemNat( s( X ), cons( Z, T ) ) ) ) ] )
% 6.83/7.26 , clause( 42, [ =( elemNat( s( X ), cons( Z, cons( z, Y ) ) ), elemNat( s(
% 6.83/7.26 X ), cons( Z, Y ) ) ) ] )
% 6.83/7.26 , 0, clause( 2604, [ =( elemNat( X, cons( Y, Z ) ), orb( eq( X, Y ),
% 6.83/7.26 elemNat( X, Z ) ) ) ] )
% 6.83/7.26 , 0, 16, substitution( 0, [ :=( X, X ), :=( Y, T ), :=( Z, Z )] ),
% 6.83/7.26 substitution( 1, [ :=( X, s( X ) ), :=( Y, Y ), :=( Z, cons( Z, cons( z,
% 6.83/7.26 T ) ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2608, [ =( elemNat( s( X ), cons( Y, cons( Z, cons( z, T ) ) ) ),
% 6.83/7.26 elemNat( s( X ), cons( Y, cons( Z, T ) ) ) ) ] )
% 6.83/7.26 , clause( 12, [ =( orb( eq( X, Y ), elemNat( X, Z ) ), elemNat( X, cons( Y
% 6.83/7.26 , Z ) ) ) ] )
% 6.83/7.26 , 0, clause( 2607, [ =( elemNat( s( X ), cons( Y, cons( Z, cons( z, T ) ) )
% 6.83/7.26 ), orb( eq( s( X ), Y ), elemNat( s( X ), cons( Z, T ) ) ) ) ] )
% 6.83/7.26 , 0, 11, substitution( 0, [ :=( X, s( X ) ), :=( Y, Y ), :=( Z, cons( Z, T
% 6.83/7.26 ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 68, [ =( elemNat( s( X ), cons( T, cons( Y, cons( z, Z ) ) ) ),
% 6.83/7.26 elemNat( s( X ), cons( T, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2608, [ =( elemNat( s( X ), cons( Y, cons( Z, cons( z, T ) ) ) )
% 6.83/7.26 , elemNat( s( X ), cons( Y, cons( Z, T ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, T ), :=( Z, Y ), :=( T, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2611, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 18, [ =( append( rev( Y ), cons( X, nil ) ), rev( cons( X, Y ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2617, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) ) ) ),
% 6.83/7.26 append( cons( T, cons( Z, cons( Y, nil ) ) ), cons( X, nil ) ) ) ] )
% 6.83/7.26 , clause( 49, [ =( rev( cons( Z, cons( X, cons( Y, nil ) ) ) ), cons( Y,
% 6.83/7.26 cons( X, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2611, [ =( rev( cons( Y, X ) ), append( rev( X ), cons( Y, nil
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, 12, substitution( 0, [ :=( X, Z ), :=( Y, T ), :=( Z, Y )] ),
% 6.83/7.26 substitution( 1, [ :=( X, cons( Y, cons( Z, cons( T, nil ) ) ) ), :=( Y,
% 6.83/7.26 X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2618, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) ) ) ),
% 6.83/7.26 cons( T, append( cons( Z, cons( Y, nil ) ), cons( X, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, clause( 2617, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) )
% 6.83/7.26 ) ), append( cons( T, cons( Z, cons( Y, nil ) ) ), cons( X, nil ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, 11, substitution( 0, [ :=( X, T ), :=( Y, cons( Z, cons( Y, nil ) ) )
% 6.83/7.26 , :=( Z, cons( X, nil ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ),
% 6.83/7.26 :=( Z, Z ), :=( T, T )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2621, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) ) ) ),
% 6.83/7.26 cons( T, cons( Z, append( cons( Y, nil ), cons( X, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, clause( 2618, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) )
% 6.83/7.26 ) ), cons( T, append( cons( Z, cons( Y, nil ) ), cons( X, nil ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, 13, substitution( 0, [ :=( X, Z ), :=( Y, cons( Y, nil ) ), :=( Z,
% 6.83/7.26 cons( X, nil ) )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z
% 6.83/7.26 ), :=( T, T )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2623, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) ) ) ),
% 6.83/7.26 cons( T, cons( Z, cons( Y, append( nil, cons( X, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 16, [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, clause( 2621, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) )
% 6.83/7.26 ) ), cons( T, cons( Z, append( cons( Y, nil ), cons( X, nil ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, 15, substitution( 0, [ :=( X, Y ), :=( Y, nil ), :=( Z, cons( X, nil )
% 6.83/7.26 )] ), substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2624, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) ) ) ),
% 6.83/7.26 cons( T, cons( Z, cons( Y, cons( X, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 15, [ =( append( nil, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2623, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) )
% 6.83/7.26 ) ), cons( T, cons( Z, cons( Y, append( nil, cons( X, nil ) ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, 17, substitution( 0, [ :=( X, cons( X, nil ) )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 82, [ =( rev( cons( T, cons( X, cons( Y, cons( Z, nil ) ) ) ) ),
% 6.83/7.26 cons( Z, cons( Y, cons( X, cons( T, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2624, [ =( rev( cons( X, cons( Y, cons( Z, cons( T, nil ) ) ) ) )
% 6.83/7.26 , cons( T, cons( Z, cons( Y, cons( X, nil ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, T ), :=( Y, X ), :=( Z, Y ), :=( T, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2627, [ =( elemNat( X, cons( Y, cons( Z, nil ) ) ), orb( eq( X, Y )
% 6.83/7.26 , orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 43, [ =( orb( eq( X, Z ), orb( eq( X, Y ), bfalse ) ), elemNat( X
% 6.83/7.26 , cons( Z, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2629, [ =( elemNat( s( X ), cons( Y, cons( s( Z ), nil ) ) ), orb(
% 6.83/7.26 eq( s( X ), Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 27, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2627, [ =( elemNat( X, cons( Y, cons( Z, nil ) ) ), orb( eq( X
% 6.83/7.26 , Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, 16, substitution( 0, [ :=( X, X ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, s( X ) ), :=( Y, Y ), :=( Z, s( Z ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2631, [ =( orb( eq( s( X ), Y ), orb( eq( X, Z ), bfalse ) ),
% 6.83/7.26 elemNat( s( X ), cons( Y, cons( s( Z ), nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2629, [ =( elemNat( s( X ), cons( Y, cons( s( Z ), nil ) ) ), orb(
% 6.83/7.26 eq( s( X ), Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 83, [ =( orb( eq( s( X ), Z ), orb( eq( X, Y ), bfalse ) ), elemNat(
% 6.83/7.26 s( X ), cons( Z, cons( s( Y ), nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2631, [ =( orb( eq( s( X ), Y ), orb( eq( X, Z ), bfalse ) ),
% 6.83/7.26 elemNat( s( X ), cons( Y, cons( s( Z ), nil ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2633, [ =( unique( cons( X, cons( Y, nil ) ) ), aux( X, cons( Y,
% 6.83/7.26 nil ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 44, [ =( aux( X, cons( Y, nil ), orb( eq( X, Y ), bfalse ) ),
% 6.83/7.26 unique( cons( X, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2637, [ =( unique( cons( s( X ), cons( z, nil ) ) ), aux( s( X ),
% 6.83/7.26 cons( z, nil ), orb( bfalse, bfalse ) ) ) ] )
% 6.83/7.26 , clause( 29, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , 0, clause( 2633, [ =( unique( cons( X, cons( Y, nil ) ) ), aux( X, cons(
% 6.83/7.26 Y, nil ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, 15, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, s( X )
% 6.83/7.26 ), :=( Y, z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2638, [ =( unique( cons( s( X ), cons( z, nil ) ) ), aux( s( X ),
% 6.83/7.26 cons( z, nil ), bfalse ) ) ] )
% 6.83/7.26 , clause( 3, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2637, [ =( unique( cons( s( X ), cons( z, nil ) ) ), aux( s( X
% 6.83/7.26 ), cons( z, nil ), orb( bfalse, bfalse ) ) ) ] )
% 6.83/7.26 , 0, 14, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2639, [ =( unique( cons( s( X ), cons( z, nil ) ) ), unique( cons(
% 6.83/7.26 z, nil ) ) ) ] )
% 6.83/7.26 , clause( 1, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , 0, clause( 2638, [ =( unique( cons( s( X ), cons( z, nil ) ) ), aux( s( X
% 6.83/7.26 ), cons( z, nil ), bfalse ) ) ] )
% 6.83/7.26 , 0, 8, substitution( 0, [ :=( X, s( X ) ), :=( Y, cons( z, nil ) )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2640, [ =( unique( cons( s( X ), cons( z, nil ) ) ), btrue ) ] )
% 6.83/7.26 , clause( 48, [ =( unique( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2639, [ =( unique( cons( s( X ), cons( z, nil ) ) ), unique(
% 6.83/7.26 cons( z, nil ) ) ) ] )
% 6.83/7.26 , 0, 8, substitution( 0, [ :=( X, z )] ), substitution( 1, [ :=( X, X )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 86, [ =( unique( cons( s( X ), cons( z, nil ) ) ), btrue ) ] )
% 6.83/7.26 , clause( 2640, [ =( unique( cons( s( X ), cons( z, nil ) ) ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2643, [ =( sorted( cons( X, cons( Y, cons( Z, nil ) ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , clause( 58, [ =( andb( leqNat( Z, X ), andb( leqNat( X, Y ), btrue ) ),
% 6.83/7.26 sorted( cons( Z, cons( X, cons( Y, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2645, [ =( sorted( cons( X, cons( s( Y ), cons( s( Z ), nil ) ) ) )
% 6.83/7.26 , andb( leqNat( X, s( Y ) ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2643, [ =( sorted( cons( X, cons( Y, cons( Z, nil ) ) ) ),
% 6.83/7.26 andb( leqNat( X, Y ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , 0, 17, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, s( Y ) ), :=( Z, s( Z ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2647, [ =( andb( leqNat( X, s( Y ) ), andb( leqNat( Y, Z ), btrue )
% 6.83/7.26 ), sorted( cons( X, cons( s( Y ), cons( s( Z ), nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2645, [ =( sorted( cons( X, cons( s( Y ), cons( s( Z ), nil ) ) )
% 6.83/7.26 ), andb( leqNat( X, s( Y ) ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 125, [ =( andb( leqNat( Z, s( X ) ), andb( leqNat( X, Y ), btrue )
% 6.83/7.26 ), sorted( cons( Z, cons( s( X ), cons( s( Y ), nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2647, [ =( andb( leqNat( X, s( Y ) ), andb( leqNat( Y, Z ), btrue
% 6.83/7.26 ) ), sorted( cons( X, cons( s( Y ), cons( s( Z ), nil ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2649, [ =( sorted( cons( s( X ), cons( s( Y ), Z ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , clause( 52, [ =( andb( leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ),
% 6.83/7.26 sorted( cons( s( X ), cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2651, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), andb( btrue
% 6.83/7.26 , sorted( cons( s( X ), Y ) ) ) ) ] )
% 6.83/7.26 , clause( 4, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2649, [ =( sorted( cons( s( X ), cons( s( Y ), Z ) ) ), andb(
% 6.83/7.26 leqNat( X, Y ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , 0, 10, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, z ),
% 6.83/7.26 :=( Y, X ), :=( Z, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2652, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), sorted(
% 6.83/7.26 cons( s( X ), Y ) ) ) ] )
% 6.83/7.26 , clause( 19, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2651, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), andb(
% 6.83/7.26 btrue, sorted( cons( s( X ), Y ) ) ) ) ] )
% 6.83/7.26 , 0, 9, substitution( 0, [ :=( X, sorted( cons( s( X ), Y ) ) )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 130, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), sorted( cons(
% 6.83/7.26 s( X ), Y ) ) ) ] )
% 6.83/7.26 , clause( 2652, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), sorted(
% 6.83/7.26 cons( s( X ), Y ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2655, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y )
% 6.83/7.26 , sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2657, [ =( sorted( cons( X, cons( s( z ), cons( s( Y ), Z ) ) ) ),
% 6.83/7.26 andb( leqNat( X, s( z ) ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , clause( 130, [ =( sorted( cons( s( z ), cons( s( X ), Y ) ) ), sorted(
% 6.83/7.26 cons( s( X ), Y ) ) ) ] )
% 6.83/7.26 , 0, clause( 2655, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X
% 6.83/7.26 , Y ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, 16, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, s( z ) ), :=( Z, cons( s( Y ), Z ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2659, [ =( andb( leqNat( X, s( z ) ), sorted( cons( s( Y ), Z ) ) )
% 6.83/7.26 , sorted( cons( X, cons( s( z ), cons( s( Y ), Z ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2657, [ =( sorted( cons( X, cons( s( z ), cons( s( Y ), Z ) ) ) )
% 6.83/7.26 , andb( leqNat( X, s( z ) ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 141, [ =( andb( leqNat( Z, s( z ) ), sorted( cons( s( X ), Y ) ) )
% 6.83/7.26 , sorted( cons( Z, cons( s( z ), cons( s( X ), Y ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2659, [ =( andb( leqNat( X, s( z ) ), sorted( cons( s( Y ), Z ) )
% 6.83/7.26 ), sorted( cons( X, cons( s( z ), cons( s( Y ), Z ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2661, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 14, [ =( aux( X, Y, elemNat( X, Y ) ), unique( cons( X, Y ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2662, [ =( unique( cons( s( X ), cons( Y, cons( Z, cons( z, T ) ) )
% 6.83/7.26 ) ), aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat( s( X ),
% 6.83/7.26 cons( Y, cons( Z, T ) ) ) ) ) ] )
% 6.83/7.26 , clause( 68, [ =( elemNat( s( X ), cons( T, cons( Y, cons( z, Z ) ) ) ),
% 6.83/7.26 elemNat( s( X ), cons( T, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2661, [ =( unique( cons( X, Y ) ), aux( X, Y, elemNat( X, Y )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, 22, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, T ), :=( T, Y )] )
% 6.83/7.26 , substitution( 1, [ :=( X, s( X ) ), :=( Y, cons( Y, cons( Z, cons( z, T
% 6.83/7.26 ) ) ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2663, [ =( aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat(
% 6.83/7.26 s( X ), cons( Y, cons( Z, T ) ) ) ), unique( cons( s( X ), cons( Y, cons(
% 6.83/7.26 Z, cons( z, T ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2662, [ =( unique( cons( s( X ), cons( Y, cons( Z, cons( z, T ) )
% 6.83/7.26 ) ) ), aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat( s( X )
% 6.83/7.26 , cons( Y, cons( Z, T ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 165, [ =( aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat(
% 6.83/7.26 s( X ), cons( Y, cons( Z, T ) ) ) ), unique( cons( s( X ), cons( Y, cons(
% 6.83/7.26 Z, cons( z, T ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2663, [ =( aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ),
% 6.83/7.26 elemNat( s( X ), cons( Y, cons( Z, T ) ) ) ), unique( cons( s( X ), cons(
% 6.83/7.26 Y, cons( Z, cons( z, T ) ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2665, [ =( 'psorted_rev'( cons( X, Y ) ), impl( eq2( sorted( rev(
% 6.83/7.26 cons( X, Y ) ) ), btrue ), impl( eq2( unique( cons( X, Y ) ), btrue ),
% 6.83/7.26 eq2( leqNat( lengthNat( Y ), s( s( z ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 64, [ =( impl( eq2( sorted( rev( cons( X, Y ) ) ), btrue ), impl(
% 6.83/7.26 eq2( unique( cons( X, Y ) ), btrue ), eq2( leqNat( lengthNat( Y ), s( s(
% 6.83/7.26 z ) ) ), btrue ) ) ), 'psorted_rev'( cons( X, Y ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2667, [ =( 'psorted_rev'( cons( X, cons( Y, Z ) ) ), impl( eq2(
% 6.83/7.26 sorted( rev( cons( X, cons( Y, Z ) ) ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ), btrue ), eq2( leqNat( s( lengthNat( Z ) ), s(
% 6.83/7.26 s( z ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 8, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.26 , 0, clause( 2665, [ =( 'psorted_rev'( cons( X, Y ) ), impl( eq2( sorted(
% 6.83/7.26 rev( cons( X, Y ) ) ), btrue ), impl( eq2( unique( cons( X, Y ) ), btrue
% 6.83/7.26 ), eq2( leqNat( lengthNat( Y ), s( s( z ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 28, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, cons( Y, Z ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2668, [ =( 'psorted_rev'( cons( X, cons( Y, Z ) ) ), impl( eq2(
% 6.83/7.26 sorted( rev( cons( X, cons( Y, Z ) ) ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ), btrue ), eq2( leqNat( lengthNat( Z ), s( z ) )
% 6.83/7.26 , btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2667, [ =( 'psorted_rev'( cons( X, cons( Y, Z ) ) ), impl( eq2(
% 6.83/7.26 sorted( rev( cons( X, cons( Y, Z ) ) ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ), btrue ), eq2( leqNat( s( lengthNat( Z ) ), s(
% 6.83/7.26 s( z ) ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 27, substitution( 0, [ :=( X, lengthNat( Z ) ), :=( Y, s( z ) )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2669, [ =( impl( eq2( sorted( rev( cons( X, cons( Y, Z ) ) ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( cons( X, cons( Y, Z ) ) ), btrue ), eq2(
% 6.83/7.26 leqNat( lengthNat( Z ), s( z ) ), btrue ) ) ), 'psorted_rev'( cons( X,
% 6.83/7.26 cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 2668, [ =( 'psorted_rev'( cons( X, cons( Y, Z ) ) ), impl( eq2(
% 6.83/7.26 sorted( rev( cons( X, cons( Y, Z ) ) ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ), btrue ), eq2( leqNat( lengthNat( Z ), s( z ) )
% 6.83/7.26 , btrue ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 183, [ =( impl( eq2( sorted( rev( cons( Z, cons( X, Y ) ) ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( cons( Z, cons( X, Y ) ) ), btrue ), eq2(
% 6.83/7.26 leqNat( lengthNat( Y ), s( z ) ), btrue ) ) ), 'psorted_rev'( cons( Z,
% 6.83/7.26 cons( X, Y ) ) ) ) ] )
% 6.83/7.26 , clause( 2669, [ =( impl( eq2( sorted( rev( cons( X, cons( Y, Z ) ) ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( cons( X, cons( Y, Z ) ) ), btrue ), eq2(
% 6.83/7.26 leqNat( lengthNat( Z ), s( z ) ), btrue ) ) ), 'psorted_rev'( cons( X,
% 6.83/7.26 cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2671, [ =( unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ), aux(
% 6.83/7.26 s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ), cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 67, [ =( aux( s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ),
% 6.83/7.26 cons( Y, Z ) ) ), unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2672, [ =( unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ), aux(
% 6.83/7.26 s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X ), Y ), bfalse ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 38, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, clause( 2671, [ =( unique( cons( s( X ), cons( Y, cons( z, Z ) ) ) ),
% 6.83/7.26 aux( s( X ), cons( Y, cons( z, Z ) ), elemNat( s( X ), cons( Y, Z ) ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , 0, 18, substitution( 0, [ :=( X, s( X ) ), :=( Y, Y )] ), substitution( 1
% 6.83/7.26 , [ :=( X, X ), :=( Y, Y ), :=( Z, nil )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2673, [ =( aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X )
% 6.83/7.26 , Y ), bfalse ) ), unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , clause( 2672, [ =( unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ),
% 6.83/7.26 aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X ), Y ), bfalse ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 205, [ =( aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X ),
% 6.83/7.26 Y ), bfalse ) ), unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 2673, [ =( aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X
% 6.83/7.26 ), Y ), bfalse ) ), unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2675, [ =( elemNat( s( X ), cons( Y, cons( s( Z ), nil ) ) ), orb(
% 6.83/7.26 eq( s( X ), Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 83, [ =( orb( eq( s( X ), Z ), orb( eq( X, Y ), bfalse ) ),
% 6.83/7.26 elemNat( s( X ), cons( Z, cons( s( Y ), nil ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2677, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil ) ) ),
% 6.83/7.26 orb( eq( X, Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 27, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2675, [ =( elemNat( s( X ), cons( Y, cons( s( Z ), nil ) ) ),
% 6.83/7.26 orb( eq( s( X ), Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, 12, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, s( Y ) ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2679, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil ) ) ),
% 6.83/7.26 elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 43, [ =( orb( eq( X, Z ), orb( eq( X, Y ), bfalse ) ), elemNat( X
% 6.83/7.26 , cons( Z, cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2677, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil )
% 6.83/7.26 ) ), orb( eq( X, Y ), orb( eq( X, Z ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, 11, substitution( 0, [ :=( X, X ), :=( Y, Z ), :=( Z, Y )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 214, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil ) ) ),
% 6.83/7.26 elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 2679, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil ) ) )
% 6.83/7.26 , elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2682, [ =( sorted( cons( X, cons( s( z ), cons( s( Y ), Z ) ) ) ),
% 6.83/7.26 andb( leqNat( X, s( z ) ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , clause( 141, [ =( andb( leqNat( Z, s( z ) ), sorted( cons( s( X ), Y ) )
% 6.83/7.26 ), sorted( cons( Z, cons( s( z ), cons( s( X ), Y ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2683, [ =( sorted( cons( X, cons( s( z ), cons( s( Y ), nil ) ) ) )
% 6.83/7.26 , andb( leqNat( X, s( z ) ), btrue ) ) ] )
% 6.83/7.26 , clause( 22, [ =( sorted( cons( X, nil ) ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2682, [ =( sorted( cons( X, cons( s( z ), cons( s( Y ), Z ) )
% 6.83/7.26 ) ), andb( leqNat( X, s( z ) ), sorted( cons( s( Y ), Z ) ) ) ) ] )
% 6.83/7.26 , 0, 16, substitution( 0, [ :=( X, s( Y ) )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 ), :=( Y, Y ), :=( Z, nil )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 319, [ =( sorted( cons( Y, cons( s( z ), cons( s( X ), nil ) ) ) )
% 6.83/7.26 , andb( leqNat( Y, s( z ) ), btrue ) ) ] )
% 6.83/7.26 , clause( 2683, [ =( sorted( cons( X, cons( s( z ), cons( s( Y ), nil ) ) )
% 6.83/7.26 ), andb( leqNat( X, s( z ) ), btrue ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2686, [ =( sorted( cons( X, cons( s( Y ), cons( s( Z ), nil ) ) ) )
% 6.83/7.26 , andb( leqNat( X, s( Y ) ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , clause( 125, [ =( andb( leqNat( Z, s( X ) ), andb( leqNat( X, Y ), btrue
% 6.83/7.26 ) ), sorted( cons( Z, cons( s( X ), cons( s( Y ), nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2688, [ =( sorted( cons( X, cons( s( s( Y ) ), cons( s( s( Z ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( X, s( s( Y ) ) ), andb( leqNat( Y, Z ), btrue
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2686, [ =( sorted( cons( X, cons( s( Y ), cons( s( Z ), nil )
% 6.83/7.26 ) ) ), andb( leqNat( X, s( Y ) ), andb( leqNat( Y, Z ), btrue ) ) ) ] )
% 6.83/7.26 , 0, 20, substitution( 0, [ :=( X, Y ), :=( Y, Z )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, s( Y ) ), :=( Z, s( Z ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2690, [ =( andb( leqNat( X, s( s( Y ) ) ), andb( leqNat( Y, Z ),
% 6.83/7.26 btrue ) ), sorted( cons( X, cons( s( s( Y ) ), cons( s( s( Z ) ), nil ) )
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , clause( 2688, [ =( sorted( cons( X, cons( s( s( Y ) ), cons( s( s( Z ) )
% 6.83/7.26 , nil ) ) ) ), andb( leqNat( X, s( s( Y ) ) ), andb( leqNat( Y, Z ),
% 6.83/7.26 btrue ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 364, [ =( andb( leqNat( Z, s( s( X ) ) ), andb( leqNat( X, Y ),
% 6.83/7.26 btrue ) ), sorted( cons( Z, cons( s( s( X ) ), cons( s( s( Y ) ), nil ) )
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , clause( 2690, [ =( andb( leqNat( X, s( s( Y ) ) ), andb( leqNat( Y, Z ),
% 6.83/7.26 btrue ) ), sorted( cons( X, cons( s( s( Y ) ), cons( s( s( Z ) ), nil ) )
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2692, [ =( unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ), aux(
% 6.83/7.26 s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X ), Y ), bfalse ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 205, [ =( aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X )
% 6.83/7.26 , Y ), bfalse ) ), unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2693, [ =( unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) ) )
% 6.83/7.26 , aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , clause( 27, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2692, [ =( unique( cons( s( X ), cons( Y, cons( z, nil ) ) ) )
% 6.83/7.26 , aux( s( X ), cons( Y, cons( z, nil ) ), orb( eq( s( X ), Y ), bfalse )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, 21, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, s( Y ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2694, [ =( aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X
% 6.83/7.26 , Y ), bfalse ) ), unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , clause( 2693, [ =( unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) )
% 6.83/7.26 ), aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X, Y ), bfalse
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 511, [ =( aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X,
% 6.83/7.26 Y ), bfalse ) ), unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) ) )
% 6.83/7.26 ) ] )
% 6.83/7.26 , clause( 2694, [ =( aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq(
% 6.83/7.26 X, Y ), bfalse ) ), unique( cons( s( X ), cons( s( Y ), cons( z, nil ) )
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2696, [ =( sorted( cons( X, cons( s( s( Y ) ), cons( s( s( Z ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( X, s( s( Y ) ) ), andb( leqNat( Y, Z ), btrue
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , clause( 364, [ =( andb( leqNat( Z, s( s( X ) ) ), andb( leqNat( X, Y ),
% 6.83/7.26 btrue ) ), sorted( cons( Z, cons( s( s( X ) ), cons( s( s( Y ) ), nil ) )
% 6.83/7.26 ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2699, [ =( sorted( cons( X, cons( s( s( z ) ), cons( s( s( Y ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( X, s( s( z ) ) ), andb( btrue, btrue ) ) ) ]
% 6.83/7.26 )
% 6.83/7.26 , clause( 4, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2696, [ =( sorted( cons( X, cons( s( s( Y ) ), cons( s( s( Z )
% 6.83/7.26 ), nil ) ) ) ), andb( leqNat( X, s( s( Y ) ) ), andb( leqNat( Y, Z ),
% 6.83/7.26 btrue ) ) ) ] )
% 6.83/7.26 , 0, 20, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 6.83/7.26 :=( Y, z ), :=( Z, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2700, [ =( sorted( cons( X, cons( s( s( z ) ), cons( s( s( Y ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( X, s( s( z ) ) ), btrue ) ) ] )
% 6.83/7.26 , clause( 19, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2699, [ =( sorted( cons( X, cons( s( s( z ) ), cons( s( s( Y )
% 6.83/7.26 ), nil ) ) ) ), andb( leqNat( X, s( s( z ) ) ), andb( btrue, btrue ) ) )
% 6.83/7.26 ] )
% 6.83/7.26 , 0, 19, substitution( 0, [ :=( X, btrue )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 537, [ =( sorted( cons( Y, cons( s( s( z ) ), cons( s( s( X ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( Y, s( s( z ) ) ), btrue ) ) ] )
% 6.83/7.26 , clause( 2700, [ =( sorted( cons( X, cons( s( s( z ) ), cons( s( s( Y ) )
% 6.83/7.26 , nil ) ) ) ), andb( leqNat( X, s( s( z ) ) ), btrue ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2703, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X, Y )
% 6.83/7.26 , sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , clause( 23, [ =( andb( leqNat( X, Y ), sorted( cons( Y, Z ) ) ), sorted(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2706, [ =( sorted( cons( X, cons( Y, cons( s( s( z ) ), cons( s( s(
% 6.83/7.26 Z ) ), nil ) ) ) ) ), andb( leqNat( X, Y ), andb( leqNat( Y, s( s( z ) )
% 6.83/7.26 ), btrue ) ) ) ] )
% 6.83/7.26 , clause( 537, [ =( sorted( cons( Y, cons( s( s( z ) ), cons( s( s( X ) ),
% 6.83/7.26 nil ) ) ) ), andb( leqNat( Y, s( s( z ) ) ), btrue ) ) ] )
% 6.83/7.26 , 0, clause( 2703, [ =( sorted( cons( X, cons( Y, Z ) ) ), andb( leqNat( X
% 6.83/7.26 , Y ), sorted( cons( Y, Z ) ) ) ) ] )
% 6.83/7.26 , 0, 19, substitution( 0, [ :=( X, Z ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, Y ), :=( Z, cons( s( s( z ) ), cons( s( s( Z ) ), nil
% 6.83/7.26 ) ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2707, [ =( sorted( cons( X, cons( Y, cons( s( s( z ) ), cons( s( s(
% 6.83/7.26 Z ) ), nil ) ) ) ) ), sorted( cons( X, cons( Y, cons( s( s( z ) ), nil )
% 6.83/7.26 ) ) ) ) ] )
% 6.83/7.26 , clause( 58, [ =( andb( leqNat( Z, X ), andb( leqNat( X, Y ), btrue ) ),
% 6.83/7.26 sorted( cons( Z, cons( X, cons( Y, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2706, [ =( sorted( cons( X, cons( Y, cons( s( s( z ) ), cons(
% 6.83/7.26 s( s( Z ) ), nil ) ) ) ) ), andb( leqNat( X, Y ), andb( leqNat( Y, s( s(
% 6.83/7.26 z ) ) ), btrue ) ) ) ] )
% 6.83/7.26 , 0, 15, substitution( 0, [ :=( X, Y ), :=( Y, s( s( z ) ) ), :=( Z, X )] )
% 6.83/7.26 , substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 540, [ =( sorted( cons( Z, cons( X, cons( s( s( z ) ), cons( s( s(
% 6.83/7.26 Y ) ), nil ) ) ) ) ), sorted( cons( Z, cons( X, cons( s( s( z ) ), nil )
% 6.83/7.26 ) ) ) ) ] )
% 6.83/7.26 , clause( 2707, [ =( sorted( cons( X, cons( Y, cons( s( s( z ) ), cons( s(
% 6.83/7.26 s( Z ) ), nil ) ) ) ) ), sorted( cons( X, cons( Y, cons( s( s( z ) ), nil
% 6.83/7.26 ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, Z ), :=( Y, X ), :=( Z, Y )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2710, [ =( unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) ) )
% 6.83/7.26 , aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , clause( 511, [ =( aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X
% 6.83/7.26 , Y ), bfalse ) ), unique( cons( s( X ), cons( s( Y ), cons( z, nil ) ) )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2714, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil )
% 6.83/7.26 ) ) ), aux( s( s( X ) ), cons( s( z ), cons( z, nil ) ), orb( bfalse,
% 6.83/7.26 bfalse ) ) ) ] )
% 6.83/7.26 , clause( 29, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , 0, clause( 2710, [ =( unique( cons( s( X ), cons( s( Y ), cons( z, nil )
% 6.83/7.26 ) ) ), aux( s( X ), cons( s( Y ), cons( z, nil ) ), orb( eq( X, Y ),
% 6.83/7.26 bfalse ) ) ) ] )
% 6.83/7.26 , 0, 23, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, s( X )
% 6.83/7.26 ), :=( Y, z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2715, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil )
% 6.83/7.26 ) ) ), aux( s( s( X ) ), cons( s( z ), cons( z, nil ) ), bfalse ) ) ] )
% 6.83/7.26 , clause( 3, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2714, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z,
% 6.83/7.26 nil ) ) ) ), aux( s( s( X ) ), cons( s( z ), cons( z, nil ) ), orb(
% 6.83/7.26 bfalse, bfalse ) ) ) ] )
% 6.83/7.26 , 0, 22, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2716, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil )
% 6.83/7.26 ) ) ), unique( cons( s( z ), cons( z, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 1, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , 0, clause( 2715, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z,
% 6.83/7.26 nil ) ) ) ), aux( s( s( X ) ), cons( s( z ), cons( z, nil ) ), bfalse ) )
% 6.83/7.26 ] )
% 6.83/7.26 , 0, 12, substitution( 0, [ :=( X, s( s( X ) ) ), :=( Y, cons( s( z ), cons(
% 6.83/7.26 z, nil ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2717, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil )
% 6.83/7.26 ) ) ), btrue ) ] )
% 6.83/7.26 , clause( 86, [ =( unique( cons( s( X ), cons( z, nil ) ) ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2716, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z,
% 6.83/7.26 nil ) ) ) ), unique( cons( s( z ), cons( z, nil ) ) ) ) ] )
% 6.83/7.26 , 0, 12, substitution( 0, [ :=( X, z )] ), substitution( 1, [ :=( X, X )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 582, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil ) )
% 6.83/7.26 ) ), btrue ) ] )
% 6.83/7.26 , clause( 2717, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil
% 6.83/7.26 ) ) ) ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2720, [ =( unique( cons( s( X ), cons( Y, cons( Z, cons( z, T ) ) )
% 6.83/7.26 ) ), aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat( s( X ),
% 6.83/7.26 cons( Y, cons( Z, T ) ) ) ) ) ] )
% 6.83/7.26 , clause( 165, [ =( aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ),
% 6.83/7.26 elemNat( s( X ), cons( Y, cons( Z, T ) ) ) ), unique( cons( s( X ), cons(
% 6.83/7.26 Y, cons( Z, cons( z, T ) ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2721, [ =( unique( cons( s( X ), cons( s( Y ), cons( s( Z ), cons(
% 6.83/7.26 z, nil ) ) ) ) ), aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil )
% 6.83/7.26 ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 214, [ =( elemNat( s( X ), cons( s( Y ), cons( s( Z ), nil ) ) )
% 6.83/7.26 , elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2720, [ =( unique( cons( s( X ), cons( Y, cons( Z, cons( z, T
% 6.83/7.26 ) ) ) ) ), aux( s( X ), cons( Y, cons( Z, cons( z, T ) ) ), elemNat( s(
% 6.83/7.26 X ), cons( Y, cons( Z, T ) ) ) ) ) ] )
% 6.83/7.26 , 0, 26, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X ), :=( Y, s( Y ) ), :=( Z, s( Z ) ), :=( T,
% 6.83/7.26 nil )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2722, [ =( aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil )
% 6.83/7.26 ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ), unique( cons( s( X ),
% 6.83/7.26 cons( s( Y ), cons( s( Z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2721, [ =( unique( cons( s( X ), cons( s( Y ), cons( s( Z ), cons(
% 6.83/7.26 z, nil ) ) ) ) ), aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil )
% 6.83/7.26 ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 764, [ =( aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil ) )
% 6.83/7.26 ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ), unique( cons( s( X ), cons(
% 6.83/7.26 s( Y ), cons( s( Z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2722, [ =( aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil
% 6.83/7.26 ) ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ), unique( cons( s( X ),
% 6.83/7.26 cons( s( Y ), cons( s( Z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 6.83/7.26 permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2724, [ =( unique( cons( s( X ), cons( s( Y ), cons( s( Z ), cons(
% 6.83/7.26 z, nil ) ) ) ) ), aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil )
% 6.83/7.26 ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 764, [ =( aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z, nil )
% 6.83/7.26 ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ), unique( cons( s( X ),
% 6.83/7.26 cons( s( Y ), cons( s( Z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2726, [ =( unique( cons( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), elemNat( s( X ), cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , clause( 42, [ =( elemNat( s( X ), cons( Z, cons( z, Y ) ) ), elemNat( s(
% 6.83/7.26 X ), cons( Z, Y ) ) ) ] )
% 6.83/7.26 , 0, clause( 2724, [ =( unique( cons( s( X ), cons( s( Y ), cons( s( Z ),
% 6.83/7.26 cons( z, nil ) ) ) ) ), aux( s( X ), cons( s( Y ), cons( s( Z ), cons( z
% 6.83/7.26 , nil ) ) ), elemNat( X, cons( Y, cons( Z, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, 28, substitution( 0, [ :=( X, X ), :=( Y, nil ), :=( Z, Y )] ),
% 6.83/7.26 substitution( 1, [ :=( X, s( X ) ), :=( Y, Y ), :=( Z, z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2727, [ =( unique( cons( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 38, [ =( elemNat( X, cons( Y, nil ) ), orb( eq( X, Y ), bfalse )
% 6.83/7.26 ) ] )
% 6.83/7.26 , 0, clause( 2726, [ =( unique( cons( s( s( X ) ), cons( s( Y ), cons( s( z
% 6.83/7.26 ), cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( Y ), cons( s( z )
% 6.83/7.26 , cons( z, nil ) ) ), elemNat( s( X ), cons( Y, nil ) ) ) ) ] )
% 6.83/7.26 , 0, 28, substitution( 0, [ :=( X, s( X ) ), :=( Y, Y )] ), substitution( 1
% 6.83/7.26 , [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2728, [ =( aux( s( s( X ) ), cons( s( Y ), cons( s( z ), cons( z,
% 6.83/7.26 nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ), unique( cons( s( s( X ) ),
% 6.83/7.26 cons( s( Y ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2727, [ =( unique( cons( s( s( X ) ), cons( s( Y ), cons( s( z )
% 6.83/7.26 , cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 1833, [ =( aux( s( s( X ) ), cons( s( Y ), cons( s( z ), cons( z,
% 6.83/7.26 nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ), unique( cons( s( s( X ) ),
% 6.83/7.26 cons( s( Y ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2728, [ =( aux( s( s( X ) ), cons( s( Y ), cons( s( z ), cons( z
% 6.83/7.26 , nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ), unique( cons( s( s( X ) )
% 6.83/7.26 , cons( s( Y ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2730, [ =( unique( cons( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( Y ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 1833, [ =( aux( s( s( X ) ), cons( s( Y ), cons( s( z ), cons( z
% 6.83/7.26 , nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ), unique( cons( s( s( X ) )
% 6.83/7.26 , cons( s( Y ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2731, [ =( unique( cons( s( s( X ) ), cons( s( s( Y ) ), cons( s( z
% 6.83/7.26 ), cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( s( Y ) ), cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 27, [ =( eq( s( X ), s( Y ) ), eq( X, Y ) ) ] )
% 6.83/7.26 , 0, clause( 2730, [ =( unique( cons( s( s( X ) ), cons( s( Y ), cons( s( z
% 6.83/7.26 ), cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( Y ), cons( s( z )
% 6.83/7.26 , cons( z, nil ) ) ), orb( eq( s( X ), Y ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, 31, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 6.83/7.26 :=( X, X ), :=( Y, s( Y ) )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2732, [ =( aux( s( s( X ) ), cons( s( s( Y ) ), cons( s( z ), cons(
% 6.83/7.26 z, nil ) ) ), orb( eq( X, Y ), bfalse ) ), unique( cons( s( s( X ) ),
% 6.83/7.26 cons( s( s( Y ) ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2731, [ =( unique( cons( s( s( X ) ), cons( s( s( Y ) ), cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( s( Y ) ), cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 2018, [ =( aux( s( s( X ) ), cons( s( s( Y ) ), cons( s( z ), cons(
% 6.83/7.26 z, nil ) ) ), orb( eq( X, Y ), bfalse ) ), unique( cons( s( s( X ) ),
% 6.83/7.26 cons( s( s( Y ) ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , clause( 2732, [ =( aux( s( s( X ) ), cons( s( s( Y ) ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), orb( eq( X, Y ), bfalse ) ), unique( cons( s( s( X )
% 6.83/7.26 ), cons( s( s( Y ) ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 6.83/7.26 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2734, [ =( unique( cons( s( s( X ) ), cons( s( s( Y ) ), cons( s( z
% 6.83/7.26 ), cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( s( Y ) ), cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , clause( 2018, [ =( aux( s( s( X ) ), cons( s( s( Y ) ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), orb( eq( X, Y ), bfalse ) ), unique( cons( s( s( X )
% 6.83/7.26 ), cons( s( s( Y ) ), cons( s( z ), cons( z, nil ) ) ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2738, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), aux( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ), orb( bfalse, bfalse ) ) ) ] )
% 6.83/7.26 , clause( 29, [ =( eq( s( X ), z ), bfalse ) ] )
% 6.83/7.26 , 0, clause( 2734, [ =( unique( cons( s( s( X ) ), cons( s( s( Y ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), aux( s( s( X ) ), cons( s( s( Y ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ), orb( eq( X, Y ), bfalse ) ) ) ] )
% 6.83/7.26 , 0, 33, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, s( X )
% 6.83/7.26 ), :=( Y, z )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2739, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), aux( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ), bfalse ) ) ] )
% 6.83/7.26 , clause( 3, [ =( orb( bfalse, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2738, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ),
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ) ) ), aux( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ), orb( bfalse, bfalse ) ) ) ] )
% 6.83/7.26 , 0, 32, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2740, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), unique( cons( s( s( z ) ), cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ) ) ) ] )
% 6.83/7.26 , clause( 1, [ =( aux( X, Y, bfalse ), unique( Y ) ) ] )
% 6.83/7.26 , 0, clause( 2739, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ),
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ) ) ), aux( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ), bfalse ) ) ] )
% 6.83/7.26 , 0, 17, substitution( 0, [ :=( X, s( s( s( X ) ) ) ), :=( Y, cons( s( s( z
% 6.83/7.26 ) ), cons( s( z ), cons( z, nil ) ) ) )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2741, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), btrue ) ] )
% 6.83/7.26 , clause( 582, [ =( unique( cons( s( s( X ) ), cons( s( z ), cons( z, nil )
% 6.83/7.26 ) ) ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2740, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ),
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ) ) ), unique( cons( s( s( z ) ), cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, 17, substitution( 0, [ :=( X, z )] ), substitution( 1, [ :=( X, X )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 subsumption(
% 6.83/7.26 clause( 2072, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ), cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ) ) ), btrue ) ] )
% 6.83/7.26 , clause( 2741, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ),
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ) ) ), btrue ) ] )
% 6.83/7.26 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 eqswap(
% 6.83/7.26 clause( 2744, [ =( 'psorted_rev'( cons( X, cons( Y, Z ) ) ), impl( eq2(
% 6.83/7.26 sorted( rev( cons( X, cons( Y, Z ) ) ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ), btrue ), eq2( leqNat( lengthNat( Z ), s( z ) )
% 6.83/7.26 , btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 183, [ =( impl( eq2( sorted( rev( cons( Z, cons( X, Y ) ) ) ),
% 6.83/7.26 btrue ), impl( eq2( unique( cons( Z, cons( X, Y ) ) ), btrue ), eq2(
% 6.83/7.26 leqNat( lengthNat( Y ), s( z ) ), btrue ) ) ), 'psorted_rev'( cons( Z,
% 6.83/7.26 cons( X, Y ) ) ) ) ] )
% 6.83/7.26 , 0, substitution( 0, [ :=( X, Y ), :=( Y, Z ), :=( Z, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2758, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( sorted( rev( cons( s(
% 6.83/7.26 s( s( X ) ) ), cons( s( s( z ) ), cons( s( z ), cons( z, nil ) ) ) ) ) )
% 6.83/7.26 , btrue ), impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s( z
% 6.83/7.26 ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 2072, [ =( unique( cons( s( s( s( X ) ) ), cons( s( s( z ) ),
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ) ) ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2744, [ =( 'psorted_rev'( cons( X, cons( Y, Z ) ) ), impl( eq2(
% 6.83/7.26 sorted( rev( cons( X, cons( Y, Z ) ) ) ), btrue ), impl( eq2( unique(
% 6.83/7.26 cons( X, cons( Y, Z ) ) ), btrue ), eq2( leqNat( lengthNat( Z ), s( z ) )
% 6.83/7.26 , btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 39, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, s( s(
% 6.83/7.26 s( X ) ) ) ), :=( Y, s( s( z ) ) ), :=( Z, cons( s( z ), cons( z, nil ) )
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2759, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( sorted( cons( z, cons(
% 6.83/7.26 s( z ), cons( s( s( z ) ), cons( s( s( s( X ) ) ), nil ) ) ) ) ), btrue )
% 6.83/7.26 , impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s( z ), cons(
% 6.83/7.26 z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 82, [ =( rev( cons( T, cons( X, cons( Y, cons( Z, nil ) ) ) ) ),
% 6.83/7.26 cons( Z, cons( Y, cons( X, cons( T, nil ) ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2758, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( sorted( rev( cons(
% 6.83/7.26 s( s( s( X ) ) ), cons( s( s( z ) ), cons( s( z ), cons( z, nil ) ) ) ) )
% 6.83/7.26 ), btrue ), impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 20, substitution( 0, [ :=( X, s( s( z ) ) ), :=( Y, s( z ) ), :=( Z, z
% 6.83/7.26 ), :=( T, s( s( s( X ) ) ) )] ), substitution( 1, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2760, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( sorted( cons( z, cons(
% 6.83/7.26 s( z ), cons( s( s( z ) ), nil ) ) ) ), btrue ), impl( eq2( btrue, btrue
% 6.83/7.26 ), eq2( leqNat( lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) ),
% 6.83/7.26 btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 540, [ =( sorted( cons( Z, cons( X, cons( s( s( z ) ), cons( s( s(
% 6.83/7.26 Y ) ), nil ) ) ) ) ), sorted( cons( Z, cons( X, cons( s( s( z ) ), nil )
% 6.83/7.26 ) ) ) ) ] )
% 6.83/7.26 , 0, clause( 2759, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( sorted( cons( z,
% 6.83/7.26 cons( s( z ), cons( s( s( z ) ), cons( s( s( s( X ) ) ), nil ) ) ) ) ),
% 6.83/7.26 btrue ), impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s( z )
% 6.83/7.26 , cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 19, substitution( 0, [ :=( X, s( z ) ), :=( Y, s( X ) ), :=( Z, z )] )
% 6.83/7.26 , substitution( 1, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2761, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( andb( leqNat( z, s( z
% 6.83/7.26 ) ), btrue ), btrue ), impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat(
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 319, [ =( sorted( cons( Y, cons( s( z ), cons( s( X ), nil ) ) )
% 6.83/7.26 ), andb( leqNat( Y, s( z ) ), btrue ) ) ] )
% 6.83/7.26 , 0, clause( 2760, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( sorted( cons( z,
% 6.83/7.26 cons( s( z ), cons( s( s( z ) ), nil ) ) ) ), btrue ), impl( eq2( btrue,
% 6.83/7.26 btrue ), eq2( leqNat( lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z )
% 6.83/7.26 ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 19, substitution( 0, [ :=( X, s( z ) ), :=( Y, z )] ), substitution( 1
% 6.83/7.26 , [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2762, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( andb( btrue, btrue ),
% 6.83/7.26 btrue ), impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s( z )
% 6.83/7.26 , cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 4, [ =( leqNat( z, X ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2761, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( andb( leqNat( z,
% 6.83/7.26 s( z ) ), btrue ), btrue ), impl( eq2( btrue, btrue ), eq2( leqNat(
% 6.83/7.26 lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 20, substitution( 0, [ :=( X, s( z ) )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2763, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( btrue, btrue ), impl(
% 6.83/7.26 eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s( z ), cons( z, nil )
% 6.83/7.26 ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 19, [ =( andb( btrue, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2762, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( andb( btrue,
% 6.83/7.26 btrue ), btrue ), impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons(
% 6.83/7.26 s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 19, substitution( 0, [ :=( X, btrue )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2765, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( btrue, btrue ), impl(
% 6.83/7.26 btrue, eq2( leqNat( lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) )
% 6.83/7.26 , btrue ) ) ) ) ] )
% 6.83/7.26 , clause( 31, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2763, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( btrue, btrue ),
% 6.83/7.26 impl( eq2( btrue, btrue ), eq2( leqNat( lengthNat( cons( s( z ), cons( z
% 6.83/7.26 , nil ) ) ), s( z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 22, substitution( 0, [ :=( X, btrue )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2766, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( btrue, impl( btrue, eq2(
% 6.83/7.26 leqNat( lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) )
% 6.83/7.26 ) ) ] )
% 6.83/7.26 , clause( 31, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.26 , 0, clause( 2765, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( eq2( btrue, btrue ),
% 6.83/7.26 impl( btrue, eq2( leqNat( lengthNat( cons( s( z ), cons( z, nil ) ) ), s(
% 6.83/7.26 z ) ), btrue ) ) ) ) ] )
% 6.83/7.26 , 0, 18, substitution( 0, [ :=( X, btrue )] ), substitution( 1, [ :=( X, X
% 6.83/7.26 )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2768, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), impl( btrue, eq2( leqNat(
% 6.83/7.26 lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ] )
% 6.83/7.26 , clause( 9, [ =( impl( btrue, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2766, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( btrue, impl( btrue,
% 6.83/7.26 eq2( leqNat( lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue
% 6.83/7.26 ) ) ) ) ] )
% 6.83/7.26 , 0, 17, substitution( 0, [ :=( X, impl( btrue, eq2( leqNat( lengthNat(
% 6.83/7.26 cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) )] ),
% 6.83/7.26 substitution( 1, [ :=( X, X )] )).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2770, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( lengthNat( cons( s(
% 6.83/7.26 z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ] )
% 6.83/7.26 , clause( 9, [ =( impl( btrue, X ), X ) ] )
% 6.83/7.26 , 0, clause( 2768, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.26 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), impl( btrue, eq2( leqNat(
% 6.83/7.26 lengthNat( cons( s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ) ] )
% 6.83/7.26 , 0, 17, substitution( 0, [ :=( X, eq2( leqNat( lengthNat( cons( s( z ),
% 6.83/7.26 cons( z, nil ) ) ), s( z ) ), btrue ) )] ), substitution( 1, [ :=( X, X )] )
% 6.83/7.26 ).
% 6.83/7.26
% 6.83/7.26
% 6.83/7.26 paramod(
% 6.83/7.26 clause( 2771, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.26 , cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( s( lengthNat( cons(
% 6.83/7.27 z, nil ) ) ), s( z ) ), btrue ) ) ] )
% 6.83/7.27 , clause( 8, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.27 , 0, clause( 2770, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.27 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( lengthNat( cons(
% 6.83/7.27 s( z ), cons( z, nil ) ) ), s( z ) ), btrue ) ) ] )
% 6.83/7.27 , 0, 19, substitution( 0, [ :=( X, s( z ) ), :=( Y, cons( z, nil ) )] ),
% 6.83/7.27 substitution( 1, [ :=( X, X )] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 paramod(
% 6.83/7.27 clause( 2773, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.27 , cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( lengthNat( cons( z,
% 6.83/7.27 nil ) ), z ), btrue ) ) ] )
% 6.83/7.27 , clause( 6, [ =( leqNat( s( X ), s( Y ) ), leqNat( X, Y ) ) ] )
% 6.83/7.27 , 0, clause( 2771, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.27 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( s( lengthNat(
% 6.83/7.27 cons( z, nil ) ) ), s( z ) ), btrue ) ) ] )
% 6.83/7.27 , 0, 18, substitution( 0, [ :=( X, lengthNat( cons( z, nil ) ) ), :=( Y, z
% 6.83/7.27 )] ), substitution( 1, [ :=( X, X )] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 paramod(
% 6.83/7.27 clause( 2774, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.27 , cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( s( lengthNat( nil )
% 6.83/7.27 ), z ), btrue ) ) ] )
% 6.83/7.27 , clause( 8, [ =( lengthNat( cons( X, Y ) ), s( lengthNat( Y ) ) ) ] )
% 6.83/7.27 , 0, clause( 2773, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.27 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( lengthNat( cons(
% 6.83/7.27 z, nil ) ), z ), btrue ) ) ] )
% 6.83/7.27 , 0, 19, substitution( 0, [ :=( X, z ), :=( Y, nil )] ), substitution( 1, [
% 6.83/7.27 :=( X, X )] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 paramod(
% 6.83/7.27 clause( 2775, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.27 , cons( s( z ), cons( z, nil ) ) ) ) ), eq2( bfalse, btrue ) ) ] )
% 6.83/7.27 , clause( 5, [ =( leqNat( s( X ), z ), bfalse ) ] )
% 6.83/7.27 , 0, clause( 2774, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.27 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), eq2( leqNat( s( lengthNat(
% 6.83/7.27 nil ) ), z ), btrue ) ) ] )
% 6.83/7.27 , 0, 18, substitution( 0, [ :=( X, lengthNat( nil ) )] ), substitution( 1
% 6.83/7.27 , [ :=( X, X )] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 paramod(
% 6.83/7.27 clause( 2776, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.27 , cons( s( z ), cons( z, nil ) ) ) ) ), bfalse ) ] )
% 6.83/7.27 , clause( 25, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 6.83/7.27 , 0, clause( 2775, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s(
% 6.83/7.27 z ) ), cons( s( z ), cons( z, nil ) ) ) ) ), eq2( bfalse, btrue ) ) ] )
% 6.83/7.27 , 0, 17, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 subsumption(
% 6.83/7.27 clause( 2073, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z ) )
% 6.83/7.27 , cons( s( z ), cons( z, nil ) ) ) ) ), bfalse ) ] )
% 6.83/7.27 , clause( 2776, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z )
% 6.83/7.27 ), cons( s( z ), cons( z, nil ) ) ) ) ), bfalse ) ] )
% 6.83/7.27 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 eqswap(
% 6.83/7.27 clause( 2779, [ ~( =( btrue, eq2( 'psorted_rev'( X ), bfalse ) ) ) ] )
% 6.83/7.27 , clause( 32, [ ~( =( eq2( 'psorted_rev'( X ), bfalse ), btrue ) ) ] )
% 6.83/7.27 , 0, substitution( 0, [ :=( X, X )] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 paramod(
% 6.83/7.27 clause( 2781, [ ~( =( btrue, eq2( bfalse, bfalse ) ) ) ] )
% 6.83/7.27 , clause( 2073, [ =( 'psorted_rev'( cons( s( s( s( X ) ) ), cons( s( s( z )
% 6.83/7.27 ), cons( s( z ), cons( z, nil ) ) ) ) ), bfalse ) ] )
% 6.83/7.27 , 0, clause( 2779, [ ~( =( btrue, eq2( 'psorted_rev'( X ), bfalse ) ) ) ]
% 6.83/7.27 )
% 6.83/7.27 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, cons( s(
% 6.83/7.27 s( s( X ) ) ), cons( s( s( z ) ), cons( s( z ), cons( z, nil ) ) ) ) )] )
% 6.83/7.27 ).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 paramod(
% 6.83/7.27 clause( 2782, [ ~( =( btrue, btrue ) ) ] )
% 6.83/7.27 , clause( 31, [ =( eq2( X, X ), btrue ) ] )
% 6.83/7.27 , 0, clause( 2781, [ ~( =( btrue, eq2( bfalse, bfalse ) ) ) ] )
% 6.83/7.27 , 0, 3, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 eqrefl(
% 6.83/7.27 clause( 2783, [] )
% 6.83/7.27 , clause( 2782, [ ~( =( btrue, btrue ) ) ] )
% 6.83/7.27 , 0, substitution( 0, [] )).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 subsumption(
% 6.83/7.27 clause( 2074, [] )
% 6.83/7.27 , clause( 2783, [] )
% 6.83/7.27 , substitution( 0, [] ), permutation( 0, [] ) ).
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 end.
% 6.83/7.27
% 6.83/7.27 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 6.83/7.27
% 6.83/7.27 Memory use:
% 6.83/7.27
% 6.83/7.27 space for terms: 60376
% 6.83/7.27 space for clauses: 393723
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 clauses generated: 162706
% 6.83/7.27 clauses kept: 2075
% 6.83/7.27 clauses selected: 1482
% 6.83/7.27 clauses deleted: 350
% 6.83/7.27 clauses inuse deleted: 43
% 6.83/7.27
% 6.83/7.27 subsentry: 38040
% 6.83/7.27 literals s-matched: 36444
% 6.83/7.27 literals matched: 36444
% 6.83/7.27 full subsumption: 0
% 6.83/7.27
% 6.83/7.27 checksum: 404136934
% 6.83/7.27
% 6.83/7.27
% 6.83/7.27 Bliksem ended
%------------------------------------------------------------------------------