%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Tue May 5 06:56:53 PM UTC 2026
% Result : Unsatisfiable 67.84s 68.29s
% Output : Refutation 67.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.17/0.33 % Computer : n026.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % DateTime : Tue May 5 13:19:08 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.77/1.13 *** allocated 10000 integers for termspace/termends
% 0.77/1.13 *** allocated 10000 integers for clauses
% 0.77/1.13 *** allocated 10000 integers for justifications
% 0.77/1.13 Bliksem 1.12
% 0.77/1.13
% 0.77/1.13
% 0.77/1.13 Automatic Strategy Selection
% 0.77/1.13
% 0.77/1.13 Clauses:
% 0.77/1.13 [
% 0.77/1.13 [ =( aux( X, Y, btrue ), eps ) ],
% 0.77/1.13 [ =( aux( X, Y, bfalse ), nil4 ) ],
% 0.77/1.13 [ =( aux2( X, Y, Z, btrue ), x( y( step( Y, X ), Z ), step( Z, X ) ) ) ]
% 0.77/1.13 ,
% 0.77/1.13 [ =( aux2( X, Y, Z, bfalse ), x( y( step( Y, X ), Z ), nil4 ) ) ],
% 0.77/1.13 [ =( aux3( X, Y, Z, btrue ), rec( y( X, star( X ) ), cons2( Y, Z ) ) ) ]
% 0.77/1.13 ,
% 0.77/1.13 [ =( aux3( X, Y, Z, bfalse ), bfalse ) ],
% 0.77/1.13 [ =( z( nil4, X ), nil4 ) ],
% 0.77/1.13 [ =( z( eps, X ), X ) ],
% 0.77/1.13 [ =( z( atom( X ), nil4 ), nil4 ) ],
% 0.77/1.13 [ =( z( atom( X ), eps ), atom( X ) ) ],
% 0.77/1.13 [ =( z( atom( X ), atom( Y ) ), y( atom( X ), atom( Y ) ) ) ],
% 0.77/1.13 [ =( z( atom( X ), x( Y, Z ) ), y( atom( X ), x( Y, Z ) ) ) ],
% 0.77/1.13 [ =( z( atom( X ), y( Y, Z ) ), y( atom( X ), y( Y, Z ) ) ) ],
% 0.77/1.13 [ =( z( atom( X ), star( Y ) ), y( atom( X ), star( Y ) ) ) ],
% 0.77/1.13 [ =( z( x( X, Y ), nil4 ), nil4 ) ],
% 0.77/1.13 [ =( z( x( X, Y ), eps ), x( X, Y ) ) ],
% 0.77/1.13 [ =( z( x( X, Y ), atom( Z ) ), y( x( X, Y ), atom( Z ) ) ) ],
% 0.77/1.13 [ =( z( x( X, Y ), x( Z, T ) ), y( x( X, Y ), x( Z, T ) ) ) ],
% 0.77/1.13 [ =( z( x( X, Y ), y( Z, T ) ), y( x( X, Y ), y( Z, T ) ) ) ],
% 0.77/1.13 [ =( z( x( X, Y ), star( Z ) ), y( x( X, Y ), star( Z ) ) ) ],
% 0.77/1.13 [ =( z( y( X, Y ), nil4 ), nil4 ) ],
% 0.77/1.13 [ =( z( y( X, Y ), eps ), y( X, Y ) ) ],
% 0.77/1.13 [ =( z( y( X, Y ), atom( Z ) ), y( y( X, Y ), atom( Z ) ) ) ],
% 0.77/1.13 [ =( z( y( X, Y ), x( Z, T ) ), y( y( X, Y ), x( Z, T ) ) ) ],
% 0.77/1.13 [ =( z( y( X, Y ), y( Z, T ) ), y( y( X, Y ), y( Z, T ) ) ) ],
% 0.77/1.13 [ =( z( y( X, Y ), star( Z ) ), y( y( X, Y ), star( Z ) ) ) ],
% 0.77/1.13 [ =( z( star( X ), nil4 ), nil4 ) ],
% 0.77/1.13 [ =( z( star( X ), eps ), star( X ) ) ],
% 0.77/1.13 [ =( z( star( X ), atom( Y ) ), y( star( X ), atom( Y ) ) ) ],
% 0.77/1.13 [ =( z( star( X ), x( Y, Z ) ), y( star( X ), x( Y, Z ) ) ) ],
% 0.77/1.13 [ =( z( star( X ), y( Y, Z ) ), y( star( X ), y( Y, Z ) ) ) ],
% 0.77/1.13 [ =( z( star( X ), star( Y ) ), y( star( X ), star( Y ) ) ) ],
% 0.77/1.13 [ =( x2( nil4, X ), X ) ],
% 0.77/1.13 [ =( x2( eps, nil4 ), eps ) ],
% 0.77/1.13 [ =( x2( eps, eps ), x( eps, eps ) ) ],
% 0.77/1.13 [ =( x2( eps, atom( X ) ), x( eps, atom( X ) ) ) ],
% 0.77/1.13 [ =( x2( eps, x( X, Y ) ), x( eps, x( X, Y ) ) ) ],
% 0.77/1.13 [ =( x2( eps, y( X, Y ) ), x( eps, y( X, Y ) ) ) ],
% 0.77/1.13 [ =( x2( eps, star( X ) ), x( eps, star( X ) ) ) ],
% 0.77/1.13 [ =( x2( atom( X ), nil4 ), atom( X ) ) ],
% 0.77/1.13 [ =( x2( atom( X ), eps ), x( atom( X ), eps ) ) ],
% 0.77/1.13 [ =( x2( atom( X ), atom( Y ) ), x( atom( X ), atom( Y ) ) ) ],
% 0.77/1.13 [ =( x2( atom( X ), x( Y, Z ) ), x( atom( X ), x( Y, Z ) ) ) ],
% 0.77/1.13 [ =( x2( atom( X ), y( Y, Z ) ), x( atom( X ), y( Y, Z ) ) ) ],
% 0.77/1.13 [ =( x2( atom( X ), star( Y ) ), x( atom( X ), star( Y ) ) ) ],
% 0.77/1.13 [ =( x2( x( X, Y ), nil4 ), x( X, Y ) ) ],
% 0.77/1.13 [ =( x2( x( X, Y ), eps ), x( x( X, Y ), eps ) ) ],
% 0.77/1.13 [ =( x2( x( X, Y ), atom( Z ) ), x( x( X, Y ), atom( Z ) ) ) ],
% 0.77/1.13 [ =( x2( x( X, Y ), x( Z, T ) ), x( x( X, Y ), x( Z, T ) ) ) ],
% 0.77/1.13 [ =( x2( x( X, Y ), y( Z, T ) ), x( x( X, Y ), y( Z, T ) ) ) ],
% 0.77/1.13 [ =( x2( x( X, Y ), star( Z ) ), x( x( X, Y ), star( Z ) ) ) ],
% 0.77/1.13 [ =( x2( y( X, Y ), nil4 ), y( X, Y ) ) ],
% 0.77/1.13 [ =( x2( y( X, Y ), eps ), x( y( X, Y ), eps ) ) ],
% 0.77/1.13 [ =( x2( y( X, Y ), atom( Z ) ), x( y( X, Y ), atom( Z ) ) ) ],
% 0.77/1.13 [ =( x2( y( X, Y ), x( Z, T ) ), x( y( X, Y ), x( Z, T ) ) ) ],
% 0.77/1.13 [ =( x2( y( X, Y ), y( Z, T ) ), x( y( X, Y ), y( Z, T ) ) ) ],
% 0.77/1.13 [ =( x2( y( X, Y ), star( Z ) ), x( y( X, Y ), star( Z ) ) ) ],
% 0.77/1.13 [ =( x2( star( X ), nil4 ), star( X ) ) ],
% 0.77/1.13 [ =( x2( star( X ), eps ), x( star( X ), eps ) ) ],
% 0.77/1.13 [ =( x2( star( X ), atom( Y ) ), x( star( X ), atom( Y ) ) ) ],
% 0.77/1.13 [ =( x2( star( X ), x( Y, Z ) ), x( star( X ), x( Y, Z ) ) ) ],
% 0.77/1.13 [ =( x2( star( X ), y( Y, Z ) ), x( star( X ), y( Y, Z ) ) ) ],
% 0.77/1.13 [ =( x2( star( X ), star( Y ) ), x( star( X ), star( Y ) ) ) ],
% 0.77/1.13 [ =( splits( X, nil ), nil ) ],
% 0.77/1.13 [ =( splits( X, cons( pair2( Y, Z ), T ) ), cons( pair2( cons2( X, Y ),
% 0.77/1.13 Z ), splits( X, T ) ) ) ],
% 0.77/1.13 [ =( splits2( nil2 ), cons( pair2( nil2, nil2 ), nil ) ) ],
% 0.77/1.13 [ =( splits2( cons2( X, Y ) ), cons( pair2( nil2, cons2( X, Y ) ),
% 0.77/1.13 splits( X, splits2( Y ) ) ) ) ],
% 60.54/60.95 [ =( orb( btrue, X ), btrue ) ],
% 60.54/60.95 [ =( orb( bfalse, X ), X ) ],
% 60.54/60.95 [ =( or2( nil3 ), bfalse ) ],
% 60.54/60.95 [ =( or2( cons3( X, Y ) ), orb( X, or2( Y ) ) ) ],
% 60.54/60.95 [ =( notb( btrue ), bfalse ) ],
% 60.54/60.95 [ =( notb( bfalse ), btrue ) ],
% 60.54/60.95 [ =( andb( btrue, X ), X ) ],
% 60.54/60.95 [ =( andb( bfalse, X ), bfalse ) ],
% 60.54/60.95 [ =( eps2( eps ), btrue ) ],
% 60.54/60.95 [ =( eps2( x( X, Y ) ), orb( eps2( X ), eps2( Y ) ) ) ],
% 60.54/60.95 [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ],
% 60.54/60.95 [ =( eps2( star( X ) ), btrue ) ],
% 60.54/60.95 [ =( eps2( nil4 ), bfalse ) ],
% 60.54/60.95 [ =( eps2( atom( X ) ), bfalse ) ],
% 60.54/60.95 [ =( step( atom( X ), Y ), aux( Y, X, eq( X, Y ) ) ) ],
% 60.54/60.95 [ =( step( x( X, Y ), Z ), x( step( X, Z ), step( Y, Z ) ) ) ],
% 60.54/60.95 [ =( step( y( X, Y ), Z ), aux2( Z, X, Y, eps2( X ) ) ) ],
% 60.54/60.95 [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) ) ) ],
% 60.54/60.95 [ =( step( nil4, X ), nil4 ) ],
% 60.54/60.95 [ =( step( eps, X ), nil4 ) ],
% 60.54/60.95 [ =( rec( X, nil2 ), eps2( X ) ) ],
% 60.54/60.95 [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ],
% 60.54/60.95 [ =( reck( X, Y, nil ), nil3 ) ],
% 60.54/60.95 [ =( reck( X, Y, cons( pair2( Z, T ), U ) ), cons3( andb( reck2( X, Z )
% 60.54/60.95 , rec( Y, T ) ), reck( X, Y, U ) ) ) ],
% 60.54/60.95 [ =( reck2( nil4, X ), bfalse ) ],
% 60.54/60.95 [ =( reck2( eps, nil2 ), btrue ) ],
% 60.54/60.95 [ =( reck2( eps, cons2( X, Y ) ), bfalse ) ],
% 60.54/60.95 [ =( reck2( atom( X ), nil2 ), bfalse ) ],
% 60.54/60.95 [ =( reck2( atom( X ), cons2( Y, nil2 ) ), eq( X, Y ) ) ],
% 60.54/60.95 [ =( reck2( atom( X ), cons2( Y, cons2( Z, T ) ) ), bfalse ) ],
% 60.54/60.95 [ =( reck2( x( X, Y ), Z ), orb( reck2( X, Z ), reck2( Y, Z ) ) ) ],
% 60.54/60.95 [ =( reck2( y( X, Y ), Z ), or2( reck( X, Y, splits2( Z ) ) ) ) ],
% 60.54/60.95 [ =( reck2( star( X ), nil2 ), btrue ) ],
% 60.54/60.95 [ =( reck2( star( X ), cons2( Y, Z ) ), aux3( X, Y, Z, notb( eps2( X ) )
% 60.54/60.95 ) ) ],
% 60.54/60.95 [ =( 'prop_same'( X, Y ), eq2( rec( X, Y ), reck2( X, Y ) ) ) ],
% 60.54/60.95 [ =( eq( a, b ), bfalse ) ],
% 60.54/60.95 [ =( eq( a, c ), bfalse ) ],
% 60.54/60.95 [ =( eq( b, a ), bfalse ) ],
% 60.54/60.95 [ =( eq( b, c ), bfalse ) ],
% 60.54/60.95 [ =( eq( c, a ), bfalse ) ],
% 60.54/60.95 [ =( eq( c, b ), bfalse ) ],
% 60.54/60.95 [ =( eq2( bfalse, btrue ), bfalse ) ],
% 60.54/60.95 [ =( eq2( btrue, bfalse ), bfalse ) ],
% 60.54/60.95 [ =( eq( X, X ), btrue ) ],
% 60.54/60.95 [ =( eq2( X, X ), btrue ) ],
% 60.54/60.95 [ ~( =( eq2( 'prop_same'( X, Y ), bfalse ), btrue ) ) ]
% 60.54/60.95 ] .
% 60.54/60.95
% 60.54/60.95
% 60.54/60.95 percentage equality = 1.000000, percentage horn = 1.000000
% 60.54/60.95 This is a pure equality problem
% 60.54/60.95
% 60.54/60.95
% 60.54/60.95
% 60.54/60.95 Options Used:
% 60.54/60.95
% 60.54/60.95 useres = 1
% 60.54/60.95 useparamod = 1
% 60.54/60.95 useeqrefl = 1
% 60.54/60.95 useeqfact = 1
% 60.54/60.95 usefactor = 1
% 60.54/60.95 usesimpsplitting = 0
% 60.54/60.95 usesimpdemod = 5
% 60.54/60.95 usesimpres = 3
% 60.54/60.95
% 60.54/60.95 resimpinuse = 1000
% 60.54/60.95 resimpclauses = 20000
% 60.54/60.95 substype = eqrewr
% 60.54/60.95 backwardsubs = 1
% 60.54/60.95 selectoldest = 5
% 60.54/60.95
% 60.54/60.95 litorderings [0] = split
% 60.54/60.95 litorderings [1] = extend the termordering, first sorting on arguments
% 60.54/60.95
% 60.54/60.95 termordering = kbo
% 60.54/60.95
% 60.54/60.95 litapriori = 0
% 60.54/60.95 termapriori = 1
% 60.54/60.95 litaposteriori = 0
% 60.54/60.95 termaposteriori = 0
% 60.54/60.95 demodaposteriori = 0
% 60.54/60.95 ordereqreflfact = 0
% 60.54/60.95
% 60.54/60.95 litselect = negord
% 60.54/60.95
% 60.54/60.95 maxweight = 15
% 60.54/60.95 maxdepth = 30000
% 60.54/60.95 maxlength = 115
% 60.54/60.95 maxnrvars = 195
% 60.54/60.95 excuselevel = 1
% 60.54/60.95 increasemaxweight = 1
% 60.54/60.95
% 60.54/60.95 maxselected = 10000000
% 60.54/60.95 maxnrclauses = 10000000
% 60.54/60.95
% 60.54/60.95 showgenerated = 0
% 60.54/60.95 showkept = 0
% 60.54/60.95 showselected = 0
% 60.54/60.95 showdeleted = 0
% 60.54/60.95 showresimp = 1
% 60.54/60.95 showstatus = 2000
% 60.54/60.95
% 60.54/60.95 prologoutput = 1
% 60.54/60.95 nrgoals = 5000000
% 60.54/60.95 totalproof = 1
% 60.54/60.95
% 60.54/60.95 Symbols occurring in the translation:
% 60.54/60.95
% 60.54/60.95 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 60.54/60.95 . [1, 2] (w:1, o:51, a:1, s:1, b:0),
% 60.54/60.95 ! [4, 1] (w:0, o:40, a:1, s:1, b:0),
% 60.54/60.95 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 60.54/60.95 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 60.54/60.95 btrue [41, 0] (w:1, o:20, a:1, s:1, b:0),
% 60.54/60.95 aux [42, 3] (w:1, o:93, a:1, s:1, b:0),
% 60.54/60.95 eps [43, 0] (w:1, o:21, a:1, s:1, b:0),
% 60.54/60.95 bfalse [44, 0] (w:1, o:22, a:1, s:1, b:0),
% 60.54/60.95 nil4 [45, 0] (w:1, o:24, a:1, s:1, b:0),
% 60.54/60.95 aux2 [48, 4] (w:1, o:95, a:1, s:1, b:0),
% 60.54/60.95 step [49, 2] (w:1, o:78, a:1, s:1, b:0),
% 60.54/60.95 y [50, 2] (w:1, o:81, a:1, s:1, b:0),
% 60.54/60.95 x [51, 2] (w:1, o:79, a:1, s:1, b:0),
% 60.54/60.95 aux3 [55, 4] (w:1, o:96, a:1, s:1, b:0),
% 60.54/60.95 star [56, 1] (w:1, o:45, a:1, s:1, b:0),
% 60.54/60.95 cons2 [57, 2] (w:1, o:82, a:1, s:1, b:0),
% 67.84/68.29 rec [58, 2] (w:1, o:76, a:1, s:1, b:0),
% 67.84/68.29 z [59, 2] (w:1, o:83, a:1, s:1, b:0),
% 67.84/68.29 atom [61, 1] (w:1, o:46, a:1, s:1, b:0),
% 67.84/68.29 x2 [65, 2] (w:1, o:80, a:1, s:1, b:0),
% 67.84/68.29 nil [66, 0] (w:1, o:30, a:1, s:1, b:0),
% 67.84/68.29 splits [67, 2] (w:1, o:84, a:1, s:1, b:0),
% 67.84/68.29 pair2 [70, 2] (w:1, o:86, a:1, s:1, b:0),
% 67.84/68.29 cons [71, 2] (w:1, o:87, a:1, s:1, b:0),
% 67.84/68.29 nil2 [72, 0] (w:1, o:34, a:1, s:1, b:0),
% 67.84/68.29 splits2 [73, 1] (w:1, o:47, a:1, s:1, b:0),
% 67.84/68.29 orb [76, 2] (w:1, o:85, a:1, s:1, b:0),
% 67.84/68.29 nil3 [77, 0] (w:1, o:23, a:1, s:1, b:0),
% 67.84/68.29 or2 [78, 1] (w:1, o:49, a:1, s:1, b:0),
% 67.84/68.29 cons3 [79, 2] (w:1, o:88, a:1, s:1, b:0),
% 67.84/68.29 notb [80, 1] (w:1, o:48, a:1, s:1, b:0),
% 67.84/68.29 andb [81, 2] (w:1, o:89, a:1, s:1, b:0),
% 67.84/68.29 eps2 [82, 1] (w:1, o:50, a:1, s:1, b:0),
% 67.84/68.29 eq [84, 2] (w:1, o:90, a:1, s:1, b:0),
% 67.84/68.29 reck [86, 3] (w:1, o:94, a:1, s:1, b:0),
% 67.84/68.29 reck2 [88, 2] (w:1, o:77, a:1, s:1, b:0),
% 67.84/68.29 'prop_same' [92, 2] (w:1, o:91, a:1, s:1, b:0),
% 67.84/68.29 eq2 [93, 2] (w:1, o:92, a:1, s:1, b:0),
% 67.84/68.29 a [94, 0] (w:1, o:19, a:1, s:1, b:0),
% 67.84/68.29 b [95, 0] (w:1, o:38, a:1, s:1, b:0),
% 67.84/68.29 c [96, 0] (w:1, o:39, a:1, s:1, b:0).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Starting Search:
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 6541
% 67.84/68.29 Kept: 2004
% 67.84/68.29 Inuse: 432
% 67.84/68.29 Deleted: 119
% 67.84/68.29 Deletedinuse: 22
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 22068
% 67.84/68.29 Kept: 4009
% 67.84/68.29 Inuse: 891
% 67.84/68.29 Deleted: 413
% 67.84/68.29 Deletedinuse: 41
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 35742
% 67.84/68.29 Kept: 6013
% 67.84/68.29 Inuse: 1224
% 67.84/68.29 Deleted: 529
% 67.84/68.29 Deletedinuse: 51
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 62999
% 67.84/68.29 Kept: 8459
% 67.84/68.29 Inuse: 1719
% 67.84/68.29 Deleted: 648
% 67.84/68.29 Deletedinuse: 89
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 107109
% 67.84/68.29 Kept: 10460
% 67.84/68.29 Inuse: 2243
% 67.84/68.29 Deleted: 937
% 67.84/68.29 Deletedinuse: 178
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 169192
% 67.84/68.29 Kept: 12468
% 67.84/68.29 Inuse: 2753
% 67.84/68.29 Deleted: 1234
% 67.84/68.29 Deletedinuse: 204
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 216105
% 67.84/68.29 Kept: 14469
% 67.84/68.29 Inuse: 3240
% 67.84/68.29 Deleted: 1408
% 67.84/68.29 Deletedinuse: 235
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 259986
% 67.84/68.29 Kept: 16471
% 67.84/68.29 Inuse: 3649
% 67.84/68.29 Deleted: 1551
% 67.84/68.29 Deletedinuse: 291
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 304570
% 67.84/68.29 Kept: 18474
% 67.84/68.29 Inuse: 4210
% 67.84/68.29 Deleted: 1786
% 67.84/68.29 Deletedinuse: 319
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying clauses:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 506738
% 67.84/68.29 Kept: 20474
% 67.84/68.29 Inuse: 5673
% 67.84/68.29 Deleted: 6751
% 67.84/68.29 Deletedinuse: 585
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 735837
% 67.84/68.29 Kept: 22475
% 67.84/68.29 Inuse: 7759
% 67.84/68.29 Deleted: 6894
% 67.84/68.29 Deletedinuse: 678
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 948859
% 67.84/68.29 Kept: 24476
% 67.84/68.29 Inuse: 9416
% 67.84/68.29 Deleted: 7086
% 67.84/68.29 Deletedinuse: 789
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 1223118
% 67.84/68.29 Kept: 26476
% 67.84/68.29 Inuse: 12382
% 67.84/68.29 Deleted: 7517
% 67.84/68.29 Deletedinuse: 887
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 1817155
% 67.84/68.29 Kept: 28476
% 67.84/68.29 Inuse: 18636
% 67.84/68.29 Deleted: 7850
% 67.84/68.29 Deletedinuse: 961
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Failed to find proof!
% 67.84/68.29 maxweight = 15
% 67.84/68.29 maxnrclauses = 10000000
% 67.84/68.29 Generated: 2014887
% 67.84/68.29 Kept: 29312
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 The strategy used was not complete!
% 67.84/68.29
% 67.84/68.29 Increased maxweight to 16
% 67.84/68.29
% 67.84/68.29 Starting Search:
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 6031
% 67.84/68.29 Kept: 2003
% 67.84/68.29 Inuse: 410
% 67.84/68.29 Deleted: 113
% 67.84/68.29 Deletedinuse: 22
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 17953
% 67.84/68.29 Kept: 4005
% 67.84/68.29 Inuse: 736
% 67.84/68.29 Deleted: 358
% 67.84/68.29 Deletedinuse: 25
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 31282
% 67.84/68.29 Kept: 6005
% 67.84/68.29 Inuse: 1117
% 67.84/68.29 Deleted: 505
% 67.84/68.29 Deletedinuse: 47
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 54584
% 67.84/68.29 Kept: 8007
% 67.84/68.29 Inuse: 1532
% 67.84/68.29 Deleted: 596
% 67.84/68.29 Deletedinuse: 81
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 73794
% 67.84/68.29 Kept: 10008
% 67.84/68.29 Inuse: 1904
% 67.84/68.29 Deleted: 790
% 67.84/68.29 Deletedinuse: 154
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 110934
% 67.84/68.29 Kept: 12008
% 67.84/68.29 Inuse: 2336
% 67.84/68.29 Deleted: 1119
% 67.84/68.29 Deletedinuse: 246
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 156547
% 67.84/68.29 Kept: 14018
% 67.84/68.29 Inuse: 2765
% 67.84/68.29 Deleted: 1301
% 67.84/68.29 Deletedinuse: 278
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 197464
% 67.84/68.29 Kept: 16020
% 67.84/68.29 Inuse: 3146
% 67.84/68.29 Deleted: 1400
% 67.84/68.29 Deletedinuse: 287
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 241919
% 67.84/68.29 Kept: 18026
% 67.84/68.29 Inuse: 3499
% 67.84/68.29 Deleted: 1494
% 67.84/68.29 Deletedinuse: 290
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying clauses:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 305148
% 67.84/68.29 Kept: 20026
% 67.84/68.29 Inuse: 3967
% 67.84/68.29 Deleted: 7435
% 67.84/68.29 Deletedinuse: 318
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 444596
% 67.84/68.29 Kept: 22030
% 67.84/68.29 Inuse: 4583
% 67.84/68.29 Deleted: 7973
% 67.84/68.29 Deletedinuse: 724
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 613376
% 67.84/68.29 Kept: 24033
% 67.84/68.29 Inuse: 5099
% 67.84/68.29 Deleted: 8417
% 67.84/68.29 Deletedinuse: 838
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 756001
% 67.84/68.29 Kept: 26041
% 67.84/68.29 Inuse: 5642
% 67.84/68.29 Deleted: 8511
% 67.84/68.29 Deletedinuse: 878
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 916693
% 67.84/68.29 Kept: 28043
% 67.84/68.29 Inuse: 6205
% 67.84/68.29 Deleted: 8793
% 67.84/68.29 Deletedinuse: 936
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29 Resimplifying inuse:
% 67.84/68.29 Done
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Intermediate Status:
% 67.84/68.29 Generated: 1006238
% 67.84/68.29 Kept: 30045
% 67.84/68.29 Inuse: 6565
% 67.84/68.29 Deleted: 8854
% 67.84/68.29 Deletedinuse: 965
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Bliksems!, er is een bewijs:
% 67.84/68.29 % SZS status Unsatisfiable
% 67.84/68.29 % SZS output start Refutation
% 67.84/68.29
% 67.84/68.29 clause( 0, [ =( aux( X, Y, btrue ), eps ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 5, [ =( aux3( X, Y, Z, bfalse ), bfalse ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 71, [ =( notb( btrue ), bfalse ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 73, [ =( andb( btrue, X ), X ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 75, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 77, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 78, [ =( eps2( star( X ) ), btrue ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 81, [ =( aux( Y, X, eq( X, Y ) ), step( atom( X ), Y ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 84, [ =( y( step( X, Y ), star( X ) ), step( star( X ), Y ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 87, [ =( rec( X, nil2 ), eps2( X ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 88, [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 100, [ =( aux3( X, Y, Z, notb( eps2( X ) ) ), reck2( star( X ),
% 67.84/68.29 cons2( Y, Z ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 101, [ =( eq2( rec( X, Y ), reck2( X, Y ) ), 'prop_same'( X, Y ) )
% 67.84/68.29 ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 109, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 110, [ =( eq( X, X ), btrue ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 111, [ =( eq2( X, X ), btrue ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 112, [ ~( =( eq2( 'prop_same'( X, Y ), bfalse ), btrue ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 137, [ =( eps2( y( Y, star( X ) ) ), andb( eps2( Y ), btrue ) ) ]
% 67.84/68.29 )
% 67.84/68.29 .
% 67.84/68.29 clause( 140, [ =( eps2( y( eps, X ) ), eps2( X ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 141, [ =( andb( eps2( X ), btrue ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 260, [ =( eps2( y( Y, star( X ) ) ), eps2( y( Y, eps ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 399, [ =( eq2( rec( step( X, Y ), Z ), reck2( X, cons2( Y, Z ) ) )
% 67.84/68.29 , 'prop_same'( X, cons2( Y, Z ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 430, [ =( eps2( y( step( X, Y ), eps ) ), eps2( step( star( X ), Y
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 695, [ =( step( atom( X ), X ), eps ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 696, [ =( y( eps, star( atom( X ) ) ), step( star( atom( X ) ), X )
% 67.84/68.29 ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 887, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), bfalse ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 1426, [ =( eps2( step( star( atom( X ) ), X ) ), btrue ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 1436, [ =( eps2( step( star( star( atom( X ) ) ), X ) ), btrue ) ]
% 67.84/68.29 )
% 67.84/68.29 .
% 67.84/68.29 clause( 4067, [ =( eq2( eps2( step( X, Y ) ), reck2( X, cons2( Y, nil2 ) )
% 67.84/68.29 ), 'prop_same'( X, cons2( Y, nil2 ) ) ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 30037, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X, nil2
% 67.84/68.29 ) ), bfalse ) ] )
% 67.84/68.29 .
% 67.84/68.29 clause( 30051, [] )
% 67.84/68.29 .
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 % SZS output end Refutation
% 67.84/68.29 found a proof!
% 67.84/68.29
% 67.84/68.29 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 67.84/68.29
% 67.84/68.29 initialclauses(
% 67.84/68.29 [ clause( 30053, [ =( aux( X, Y, btrue ), eps ) ] )
% 67.84/68.29 , clause( 30054, [ =( aux( X, Y, bfalse ), nil4 ) ] )
% 67.84/68.29 , clause( 30055, [ =( aux2( X, Y, Z, btrue ), x( y( step( Y, X ), Z ), step(
% 67.84/68.29 Z, X ) ) ) ] )
% 67.84/68.29 , clause( 30056, [ =( aux2( X, Y, Z, bfalse ), x( y( step( Y, X ), Z ),
% 67.84/68.29 nil4 ) ) ] )
% 67.84/68.29 , clause( 30057, [ =( aux3( X, Y, Z, btrue ), rec( y( X, star( X ) ), cons2(
% 67.84/68.29 Y, Z ) ) ) ] )
% 67.84/68.29 , clause( 30058, [ =( aux3( X, Y, Z, bfalse ), bfalse ) ] )
% 67.84/68.29 , clause( 30059, [ =( z( nil4, X ), nil4 ) ] )
% 67.84/68.29 , clause( 30060, [ =( z( eps, X ), X ) ] )
% 67.84/68.29 , clause( 30061, [ =( z( atom( X ), nil4 ), nil4 ) ] )
% 67.84/68.29 , clause( 30062, [ =( z( atom( X ), eps ), atom( X ) ) ] )
% 67.84/68.29 , clause( 30063, [ =( z( atom( X ), atom( Y ) ), y( atom( X ), atom( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30064, [ =( z( atom( X ), x( Y, Z ) ), y( atom( X ), x( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30065, [ =( z( atom( X ), y( Y, Z ) ), y( atom( X ), y( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30066, [ =( z( atom( X ), star( Y ) ), y( atom( X ), star( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30067, [ =( z( x( X, Y ), nil4 ), nil4 ) ] )
% 67.84/68.29 , clause( 30068, [ =( z( x( X, Y ), eps ), x( X, Y ) ) ] )
% 67.84/68.29 , clause( 30069, [ =( z( x( X, Y ), atom( Z ) ), y( x( X, Y ), atom( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30070, [ =( z( x( X, Y ), x( Z, T ) ), y( x( X, Y ), x( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30071, [ =( z( x( X, Y ), y( Z, T ) ), y( x( X, Y ), y( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30072, [ =( z( x( X, Y ), star( Z ) ), y( x( X, Y ), star( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30073, [ =( z( y( X, Y ), nil4 ), nil4 ) ] )
% 67.84/68.29 , clause( 30074, [ =( z( y( X, Y ), eps ), y( X, Y ) ) ] )
% 67.84/68.29 , clause( 30075, [ =( z( y( X, Y ), atom( Z ) ), y( y( X, Y ), atom( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30076, [ =( z( y( X, Y ), x( Z, T ) ), y( y( X, Y ), x( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30077, [ =( z( y( X, Y ), y( Z, T ) ), y( y( X, Y ), y( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30078, [ =( z( y( X, Y ), star( Z ) ), y( y( X, Y ), star( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30079, [ =( z( star( X ), nil4 ), nil4 ) ] )
% 67.84/68.29 , clause( 30080, [ =( z( star( X ), eps ), star( X ) ) ] )
% 67.84/68.29 , clause( 30081, [ =( z( star( X ), atom( Y ) ), y( star( X ), atom( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30082, [ =( z( star( X ), x( Y, Z ) ), y( star( X ), x( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30083, [ =( z( star( X ), y( Y, Z ) ), y( star( X ), y( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30084, [ =( z( star( X ), star( Y ) ), y( star( X ), star( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30085, [ =( x2( nil4, X ), X ) ] )
% 67.84/68.29 , clause( 30086, [ =( x2( eps, nil4 ), eps ) ] )
% 67.84/68.29 , clause( 30087, [ =( x2( eps, eps ), x( eps, eps ) ) ] )
% 67.84/68.29 , clause( 30088, [ =( x2( eps, atom( X ) ), x( eps, atom( X ) ) ) ] )
% 67.84/68.29 , clause( 30089, [ =( x2( eps, x( X, Y ) ), x( eps, x( X, Y ) ) ) ] )
% 67.84/68.29 , clause( 30090, [ =( x2( eps, y( X, Y ) ), x( eps, y( X, Y ) ) ) ] )
% 67.84/68.29 , clause( 30091, [ =( x2( eps, star( X ) ), x( eps, star( X ) ) ) ] )
% 67.84/68.29 , clause( 30092, [ =( x2( atom( X ), nil4 ), atom( X ) ) ] )
% 67.84/68.29 , clause( 30093, [ =( x2( atom( X ), eps ), x( atom( X ), eps ) ) ] )
% 67.84/68.29 , clause( 30094, [ =( x2( atom( X ), atom( Y ) ), x( atom( X ), atom( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30095, [ =( x2( atom( X ), x( Y, Z ) ), x( atom( X ), x( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30096, [ =( x2( atom( X ), y( Y, Z ) ), x( atom( X ), y( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30097, [ =( x2( atom( X ), star( Y ) ), x( atom( X ), star( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30098, [ =( x2( x( X, Y ), nil4 ), x( X, Y ) ) ] )
% 67.84/68.29 , clause( 30099, [ =( x2( x( X, Y ), eps ), x( x( X, Y ), eps ) ) ] )
% 67.84/68.29 , clause( 30100, [ =( x2( x( X, Y ), atom( Z ) ), x( x( X, Y ), atom( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30101, [ =( x2( x( X, Y ), x( Z, T ) ), x( x( X, Y ), x( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30102, [ =( x2( x( X, Y ), y( Z, T ) ), x( x( X, Y ), y( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30103, [ =( x2( x( X, Y ), star( Z ) ), x( x( X, Y ), star( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30104, [ =( x2( y( X, Y ), nil4 ), y( X, Y ) ) ] )
% 67.84/68.29 , clause( 30105, [ =( x2( y( X, Y ), eps ), x( y( X, Y ), eps ) ) ] )
% 67.84/68.29 , clause( 30106, [ =( x2( y( X, Y ), atom( Z ) ), x( y( X, Y ), atom( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30107, [ =( x2( y( X, Y ), x( Z, T ) ), x( y( X, Y ), x( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30108, [ =( x2( y( X, Y ), y( Z, T ) ), x( y( X, Y ), y( Z, T ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30109, [ =( x2( y( X, Y ), star( Z ) ), x( y( X, Y ), star( Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30110, [ =( x2( star( X ), nil4 ), star( X ) ) ] )
% 67.84/68.29 , clause( 30111, [ =( x2( star( X ), eps ), x( star( X ), eps ) ) ] )
% 67.84/68.29 , clause( 30112, [ =( x2( star( X ), atom( Y ) ), x( star( X ), atom( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30113, [ =( x2( star( X ), x( Y, Z ) ), x( star( X ), x( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30114, [ =( x2( star( X ), y( Y, Z ) ), x( star( X ), y( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30115, [ =( x2( star( X ), star( Y ) ), x( star( X ), star( Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30116, [ =( splits( X, nil ), nil ) ] )
% 67.84/68.29 , clause( 30117, [ =( splits( X, cons( pair2( Y, Z ), T ) ), cons( pair2(
% 67.84/68.29 cons2( X, Y ), Z ), splits( X, T ) ) ) ] )
% 67.84/68.29 , clause( 30118, [ =( splits2( nil2 ), cons( pair2( nil2, nil2 ), nil ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 30119, [ =( splits2( cons2( X, Y ) ), cons( pair2( nil2, cons2( X
% 67.84/68.29 , Y ) ), splits( X, splits2( Y ) ) ) ) ] )
% 67.84/68.29 , clause( 30120, [ =( orb( btrue, X ), btrue ) ] )
% 67.84/68.29 , clause( 30121, [ =( orb( bfalse, X ), X ) ] )
% 67.84/68.29 , clause( 30122, [ =( or2( nil3 ), bfalse ) ] )
% 67.84/68.29 , clause( 30123, [ =( or2( cons3( X, Y ) ), orb( X, or2( Y ) ) ) ] )
% 67.84/68.29 , clause( 30124, [ =( notb( btrue ), bfalse ) ] )
% 67.84/68.29 , clause( 30125, [ =( notb( bfalse ), btrue ) ] )
% 67.84/68.29 , clause( 30126, [ =( andb( btrue, X ), X ) ] )
% 67.84/68.29 , clause( 30127, [ =( andb( bfalse, X ), bfalse ) ] )
% 67.84/68.29 , clause( 30128, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 , clause( 30129, [ =( eps2( x( X, Y ) ), orb( eps2( X ), eps2( Y ) ) ) ] )
% 67.84/68.29 , clause( 30130, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 30131, [ =( eps2( star( X ) ), btrue ) ] )
% 67.84/68.29 , clause( 30132, [ =( eps2( nil4 ), bfalse ) ] )
% 67.84/68.29 , clause( 30133, [ =( eps2( atom( X ) ), bfalse ) ] )
% 67.84/68.29 , clause( 30134, [ =( step( atom( X ), Y ), aux( Y, X, eq( X, Y ) ) ) ] )
% 67.84/68.29 , clause( 30135, [ =( step( x( X, Y ), Z ), x( step( X, Z ), step( Y, Z ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30136, [ =( step( y( X, Y ), Z ), aux2( Z, X, Y, eps2( X ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 30137, [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) ) )
% 67.84/68.29 ] )
% 67.84/68.29 , clause( 30138, [ =( step( nil4, X ), nil4 ) ] )
% 67.84/68.29 , clause( 30139, [ =( step( eps, X ), nil4 ) ] )
% 67.84/68.29 , clause( 30140, [ =( rec( X, nil2 ), eps2( X ) ) ] )
% 67.84/68.29 , clause( 30141, [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 30142, [ =( reck( X, Y, nil ), nil3 ) ] )
% 67.84/68.29 , clause( 30143, [ =( reck( X, Y, cons( pair2( Z, T ), U ) ), cons3( andb(
% 67.84/68.29 reck2( X, Z ), rec( Y, T ) ), reck( X, Y, U ) ) ) ] )
% 67.84/68.29 , clause( 30144, [ =( reck2( nil4, X ), bfalse ) ] )
% 67.84/68.29 , clause( 30145, [ =( reck2( eps, nil2 ), btrue ) ] )
% 67.84/68.29 , clause( 30146, [ =( reck2( eps, cons2( X, Y ) ), bfalse ) ] )
% 67.84/68.29 , clause( 30147, [ =( reck2( atom( X ), nil2 ), bfalse ) ] )
% 67.84/68.29 , clause( 30148, [ =( reck2( atom( X ), cons2( Y, nil2 ) ), eq( X, Y ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 30149, [ =( reck2( atom( X ), cons2( Y, cons2( Z, T ) ) ), bfalse
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30150, [ =( reck2( x( X, Y ), Z ), orb( reck2( X, Z ), reck2( Y,
% 67.84/68.29 Z ) ) ) ] )
% 67.84/68.29 , clause( 30151, [ =( reck2( y( X, Y ), Z ), or2( reck( X, Y, splits2( Z )
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 , clause( 30152, [ =( reck2( star( X ), nil2 ), btrue ) ] )
% 67.84/68.29 , clause( 30153, [ =( reck2( star( X ), cons2( Y, Z ) ), aux3( X, Y, Z,
% 67.84/68.29 notb( eps2( X ) ) ) ) ] )
% 67.84/68.29 , clause( 30154, [ =( 'prop_same'( X, Y ), eq2( rec( X, Y ), reck2( X, Y )
% 67.84/68.29 ) ) ] )
% 67.84/68.29 , clause( 30155, [ =( eq( a, b ), bfalse ) ] )
% 67.84/68.29 , clause( 30156, [ =( eq( a, c ), bfalse ) ] )
% 67.84/68.29 , clause( 30157, [ =( eq( b, a ), bfalse ) ] )
% 67.84/68.29 , clause( 30158, [ =( eq( b, c ), bfalse ) ] )
% 67.84/68.29 , clause( 30159, [ =( eq( c, a ), bfalse ) ] )
% 67.84/68.29 , clause( 30160, [ =( eq( c, b ), bfalse ) ] )
% 67.84/68.29 , clause( 30161, [ =( eq2( bfalse, btrue ), bfalse ) ] )
% 67.84/68.29 , clause( 30162, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 67.84/68.29 , clause( 30163, [ =( eq( X, X ), btrue ) ] )
% 67.84/68.29 , clause( 30164, [ =( eq2( X, X ), btrue ) ] )
% 67.84/68.29 , clause( 30165, [ ~( =( eq2( 'prop_same'( X, Y ), bfalse ), btrue ) ) ] )
% 67.84/68.29 ] ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 0, [ =( aux( X, Y, btrue ), eps ) ] )
% 67.84/68.29 , clause( 30053, [ =( aux( X, Y, btrue ), eps ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 5, [ =( aux3( X, Y, Z, bfalse ), bfalse ) ] )
% 67.84/68.29 , clause( 30058, [ =( aux3( X, Y, Z, bfalse ), bfalse ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 71, [ =( notb( btrue ), bfalse ) ] )
% 67.84/68.29 , clause( 30124, [ =( notb( btrue ), bfalse ) ] )
% 67.84/68.29 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 73, [ =( andb( btrue, X ), X ) ] )
% 67.84/68.29 , clause( 30126, [ =( andb( btrue, X ), X ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 75, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 , clause( 30128, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 30472, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ] )
% 67.84/68.29 , clause( 30130, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 77, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ] )
% 67.84/68.29 , clause( 30472, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 78, [ =( eps2( star( X ) ), btrue ) ] )
% 67.84/68.29 , clause( 30131, [ =( eps2( star( X ) ), btrue ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 30633, [ =( aux( Y, X, eq( X, Y ) ), step( atom( X ), Y ) ) ] )
% 67.84/68.29 , clause( 30134, [ =( step( atom( X ), Y ), aux( Y, X, eq( X, Y ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 81, [ =( aux( Y, X, eq( X, Y ) ), step( atom( X ), Y ) ) ] )
% 67.84/68.29 , clause( 30633, [ =( aux( Y, X, eq( X, Y ) ), step( atom( X ), Y ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 30718, [ =( y( step( X, Y ), star( X ) ), step( star( X ), Y ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 30137, [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) ) )
% 67.84/68.29 ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 84, [ =( y( step( X, Y ), star( X ) ), step( star( X ), Y ) ) ] )
% 67.84/68.29 , clause( 30718, [ =( y( step( X, Y ), star( X ) ), step( star( X ), Y ) )
% 67.84/68.29 ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 87, [ =( rec( X, nil2 ), eps2( X ) ) ] )
% 67.84/68.29 , clause( 30140, [ =( rec( X, nil2 ), eps2( X ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 88, [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ] )
% 67.84/68.29 , clause( 30141, [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 30996, [ =( aux3( X, Y, Z, notb( eps2( X ) ) ), reck2( star( X ),
% 67.84/68.29 cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , clause( 30153, [ =( reck2( star( X ), cons2( Y, Z ) ), aux3( X, Y, Z,
% 67.84/68.29 notb( eps2( X ) ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 100, [ =( aux3( X, Y, Z, notb( eps2( X ) ) ), reck2( star( X ),
% 67.84/68.29 cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , clause( 30996, [ =( aux3( X, Y, Z, notb( eps2( X ) ) ), reck2( star( X )
% 67.84/68.29 , cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31098, [ =( eq2( rec( X, Y ), reck2( X, Y ) ), 'prop_same'( X, Y )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 30154, [ =( 'prop_same'( X, Y ), eq2( rec( X, Y ), reck2( X, Y )
% 67.84/68.29 ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 101, [ =( eq2( rec( X, Y ), reck2( X, Y ) ), 'prop_same'( X, Y ) )
% 67.84/68.29 ] )
% 67.84/68.29 , clause( 31098, [ =( eq2( rec( X, Y ), reck2( X, Y ) ), 'prop_same'( X, Y
% 67.84/68.29 ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 109, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 67.84/68.29 , clause( 30162, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 67.84/68.29 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 110, [ =( eq( X, X ), btrue ) ] )
% 67.84/68.29 , clause( 30163, [ =( eq( X, X ), btrue ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 111, [ =( eq2( X, X ), btrue ) ] )
% 67.84/68.29 , clause( 30164, [ =( eq2( X, X ), btrue ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 112, [ ~( =( eq2( 'prop_same'( X, Y ), bfalse ), btrue ) ) ] )
% 67.84/68.29 , clause( 30165, [ ~( =( eq2( 'prop_same'( X, Y ), bfalse ), btrue ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31546, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ] )
% 67.84/68.29 , clause( 77, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31548, [ =( eps2( y( X, star( Y ) ) ), andb( eps2( X ), btrue ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 78, [ =( eps2( star( X ) ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31546, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) )
% 67.84/68.29 ] )
% 67.84/68.29 , 0, 9, substitution( 0, [ :=( X, Y )] ), substitution( 1, [ :=( X, X ),
% 67.84/68.29 :=( Y, star( Y ) )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 137, [ =( eps2( y( Y, star( X ) ) ), andb( eps2( Y ), btrue ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 31548, [ =( eps2( y( X, star( Y ) ) ), andb( eps2( X ), btrue ) )
% 67.84/68.29 ] )
% 67.84/68.29 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31552, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ] )
% 67.84/68.29 , clause( 77, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31554, [ =( eps2( y( eps, X ) ), andb( btrue, eps2( X ) ) ) ] )
% 67.84/68.29 , clause( 75, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31552, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) )
% 67.84/68.29 ] )
% 67.84/68.29 , 0, 6, substitution( 0, [] ), substitution( 1, [ :=( X, eps ), :=( Y, X )] )
% 67.84/68.29 ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31556, [ =( eps2( y( eps, X ) ), eps2( X ) ) ] )
% 67.84/68.29 , clause( 73, [ =( andb( btrue, X ), X ) ] )
% 67.84/68.29 , 0, clause( 31554, [ =( eps2( y( eps, X ) ), andb( btrue, eps2( X ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, 5, substitution( 0, [ :=( X, eps2( X ) )] ), substitution( 1, [ :=( X
% 67.84/68.29 , X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 140, [ =( eps2( y( eps, X ) ), eps2( X ) ) ] )
% 67.84/68.29 , clause( 31556, [ =( eps2( y( eps, X ) ), eps2( X ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31559, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) ) ] )
% 67.84/68.29 , clause( 77, [ =( andb( eps2( X ), eps2( Y ) ), eps2( y( X, Y ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31561, [ =( eps2( y( X, eps ) ), andb( eps2( X ), btrue ) ) ] )
% 67.84/68.29 , clause( 75, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31559, [ =( eps2( y( X, Y ) ), andb( eps2( X ), eps2( Y ) ) )
% 67.84/68.29 ] )
% 67.84/68.29 , 0, 8, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y, eps )] )
% 67.84/68.29 ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31563, [ =( andb( eps2( X ), btrue ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , clause( 31561, [ =( eps2( y( X, eps ) ), andb( eps2( X ), btrue ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 141, [ =( andb( eps2( X ), btrue ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , clause( 31563, [ =( andb( eps2( X ), btrue ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31566, [ =( eps2( y( X, star( Y ) ) ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , clause( 141, [ =( andb( eps2( X ), btrue ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , 0, clause( 137, [ =( eps2( y( Y, star( X ) ) ), andb( eps2( Y ), btrue )
% 67.84/68.29 ) ] )
% 67.84/68.29 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, Y ),
% 67.84/68.29 :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 260, [ =( eps2( y( Y, star( X ) ) ), eps2( y( Y, eps ) ) ) ] )
% 67.84/68.29 , clause( 31566, [ =( eps2( y( X, star( Y ) ) ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, Y ), :=( Y, X )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31569, [ =( 'prop_same'( X, Y ), eq2( rec( X, Y ), reck2( X, Y ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 101, [ =( eq2( rec( X, Y ), reck2( X, Y ) ), 'prop_same'( X, Y )
% 67.84/68.29 ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31570, [ =( 'prop_same'( X, cons2( Y, Z ) ), eq2( rec( step( X, Y )
% 67.84/68.29 , Z ), reck2( X, cons2( Y, Z ) ) ) ) ] )
% 67.84/68.29 , clause( 88, [ =( rec( X, cons2( Y, Z ) ), rec( step( X, Y ), Z ) ) ] )
% 67.84/68.29 , 0, clause( 31569, [ =( 'prop_same'( X, Y ), eq2( rec( X, Y ), reck2( X, Y
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 , 0, 7, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 substitution( 1, [ :=( X, X ), :=( Y, cons2( Y, Z ) )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31571, [ =( eq2( rec( step( X, Y ), Z ), reck2( X, cons2( Y, Z ) )
% 67.84/68.29 ), 'prop_same'( X, cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , clause( 31570, [ =( 'prop_same'( X, cons2( Y, Z ) ), eq2( rec( step( X, Y
% 67.84/68.29 ), Z ), reck2( X, cons2( Y, Z ) ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 399, [ =( eq2( rec( step( X, Y ), Z ), reck2( X, cons2( Y, Z ) ) )
% 67.84/68.29 , 'prop_same'( X, cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , clause( 31571, [ =( eq2( rec( step( X, Y ), Z ), reck2( X, cons2( Y, Z )
% 67.84/68.29 ) ), 'prop_same'( X, cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31573, [ =( eps2( y( X, eps ) ), eps2( y( X, star( Y ) ) ) ) ] )
% 67.84/68.29 , clause( 260, [ =( eps2( y( Y, star( X ) ) ), eps2( y( Y, eps ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31574, [ =( eps2( y( step( X, Y ), eps ) ), eps2( step( star( X ),
% 67.84/68.29 Y ) ) ) ] )
% 67.84/68.29 , clause( 84, [ =( y( step( X, Y ), star( X ) ), step( star( X ), Y ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, clause( 31573, [ =( eps2( y( X, eps ) ), eps2( y( X, star( Y ) ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, 8, substitution( 0, [ :=( X, X ), :=( Y, Y )] ), substitution( 1, [
% 67.84/68.29 :=( X, step( X, Y ) ), :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 430, [ =( eps2( y( step( X, Y ), eps ) ), eps2( step( star( X ), Y
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 , clause( 31574, [ =( eps2( y( step( X, Y ), eps ) ), eps2( step( star( X )
% 67.84/68.29 , Y ) ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31577, [ =( step( atom( Y ), X ), aux( X, Y, eq( Y, X ) ) ) ] )
% 67.84/68.29 , clause( 81, [ =( aux( Y, X, eq( X, Y ) ), step( atom( X ), Y ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31579, [ =( step( atom( X ), X ), aux( X, X, btrue ) ) ] )
% 67.84/68.29 , clause( 110, [ =( eq( X, X ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31577, [ =( step( atom( Y ), X ), aux( X, Y, eq( Y, X ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, 8, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X ),
% 67.84/68.29 :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31580, [ =( step( atom( X ), X ), eps ) ] )
% 67.84/68.29 , clause( 0, [ =( aux( X, Y, btrue ), eps ) ] )
% 67.84/68.29 , 0, clause( 31579, [ =( step( atom( X ), X ), aux( X, X, btrue ) ) ] )
% 67.84/68.29 , 0, 5, substitution( 0, [ :=( X, X ), :=( Y, X )] ), substitution( 1, [
% 67.84/68.29 :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 695, [ =( step( atom( X ), X ), eps ) ] )
% 67.84/68.29 , clause( 31580, [ =( step( atom( X ), X ), eps ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31583, [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 84, [ =( y( step( X, Y ), star( X ) ), step( star( X ), Y ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31584, [ =( step( star( atom( X ) ), X ), y( eps, star( atom( X ) )
% 67.84/68.29 ) ) ] )
% 67.84/68.29 , clause( 695, [ =( step( atom( X ), X ), eps ) ] )
% 67.84/68.29 , 0, clause( 31583, [ =( step( star( X ), Y ), y( step( X, Y ), star( X ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , 0, 7, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, atom( X
% 67.84/68.29 ) ), :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31585, [ =( y( eps, star( atom( X ) ) ), step( star( atom( X ) ), X
% 67.84/68.29 ) ) ] )
% 67.84/68.29 , clause( 31584, [ =( step( star( atom( X ) ), X ), y( eps, star( atom( X )
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 696, [ =( y( eps, star( atom( X ) ) ), step( star( atom( X ) ), X )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 31585, [ =( y( eps, star( atom( X ) ) ), step( star( atom( X ) )
% 67.84/68.29 , X ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31587, [ =( reck2( star( X ), cons2( Y, Z ) ), aux3( X, Y, Z, notb(
% 67.84/68.29 eps2( X ) ) ) ) ] )
% 67.84/68.29 , clause( 100, [ =( aux3( X, Y, Z, notb( eps2( X ) ) ), reck2( star( X ),
% 67.84/68.29 cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31590, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), aux3( star(
% 67.84/68.29 X ), Y, Z, notb( btrue ) ) ) ] )
% 67.84/68.29 , clause( 78, [ =( eps2( star( X ) ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31587, [ =( reck2( star( X ), cons2( Y, Z ) ), aux3( X, Y, Z,
% 67.84/68.29 notb( eps2( X ) ) ) ) ] )
% 67.84/68.29 , 0, 14, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, star(
% 67.84/68.29 X ) ), :=( Y, Y ), :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31591, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), aux3( star(
% 67.84/68.29 X ), Y, Z, bfalse ) ) ] )
% 67.84/68.29 , clause( 71, [ =( notb( btrue ), bfalse ) ] )
% 67.84/68.29 , 0, clause( 31590, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), aux3(
% 67.84/68.29 star( X ), Y, Z, notb( btrue ) ) ) ] )
% 67.84/68.29 , 0, 13, substitution( 0, [] ), substitution( 1, [ :=( X, X ), :=( Y, Y ),
% 67.84/68.29 :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31592, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), bfalse ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 5, [ =( aux3( X, Y, Z, bfalse ), bfalse ) ] )
% 67.84/68.29 , 0, clause( 31591, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), aux3(
% 67.84/68.29 star( X ), Y, Z, bfalse ) ) ] )
% 67.84/68.29 , 0, 8, substitution( 0, [ :=( X, star( X ) ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 substitution( 1, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 887, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), bfalse ) ] )
% 67.84/68.29 , clause( 31592, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), bfalse ) ]
% 67.84/68.29 )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] ),
% 67.84/68.29 permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31595, [ =( eps2( y( X, eps ) ), eps2( y( X, star( Y ) ) ) ) ] )
% 67.84/68.29 , clause( 260, [ =( eps2( y( Y, star( X ) ) ), eps2( y( Y, eps ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, Y ), :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31598, [ =( eps2( y( eps, eps ) ), eps2( step( star( atom( X ) ), X
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 , clause( 696, [ =( y( eps, star( atom( X ) ) ), step( star( atom( X ) ), X
% 67.84/68.29 ) ) ] )
% 67.84/68.29 , 0, clause( 31595, [ =( eps2( y( X, eps ) ), eps2( y( X, star( Y ) ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, 6, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, eps ),
% 67.84/68.29 :=( Y, atom( X ) )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31599, [ =( eps2( eps ), eps2( step( star( atom( X ) ), X ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 140, [ =( eps2( y( eps, X ) ), eps2( X ) ) ] )
% 67.84/68.29 , 0, clause( 31598, [ =( eps2( y( eps, eps ) ), eps2( step( star( atom( X )
% 67.84/68.29 ), X ) ) ) ] )
% 67.84/68.29 , 0, 1, substitution( 0, [ :=( X, eps )] ), substitution( 1, [ :=( X, X )] )
% 67.84/68.29 ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31600, [ =( btrue, eps2( step( star( atom( X ) ), X ) ) ) ] )
% 67.84/68.29 , clause( 75, [ =( eps2( eps ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31599, [ =( eps2( eps ), eps2( step( star( atom( X ) ), X ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , 0, 1, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31601, [ =( eps2( step( star( atom( X ) ), X ) ), btrue ) ] )
% 67.84/68.29 , clause( 31600, [ =( btrue, eps2( step( star( atom( X ) ), X ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 1426, [ =( eps2( step( star( atom( X ) ), X ) ), btrue ) ] )
% 67.84/68.29 , clause( 31601, [ =( eps2( step( star( atom( X ) ), X ) ), btrue ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31603, [ =( eps2( y( X, eps ) ), andb( eps2( X ), btrue ) ) ] )
% 67.84/68.29 , clause( 141, [ =( andb( eps2( X ), btrue ), eps2( y( X, eps ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31606, [ =( eps2( y( step( star( atom( X ) ), X ), eps ) ), andb(
% 67.84/68.29 btrue, btrue ) ) ] )
% 67.84/68.29 , clause( 1426, [ =( eps2( step( star( atom( X ) ), X ) ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31603, [ =( eps2( y( X, eps ) ), andb( eps2( X ), btrue ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, 10, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, step(
% 67.84/68.29 star( atom( X ) ), X ) )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31607, [ =( eps2( y( step( star( atom( X ) ), X ), eps ) ), btrue )
% 67.84/68.29 ] )
% 67.84/68.29 , clause( 73, [ =( andb( btrue, X ), X ) ] )
% 67.84/68.29 , 0, clause( 31606, [ =( eps2( y( step( star( atom( X ) ), X ), eps ) ),
% 67.84/68.29 andb( btrue, btrue ) ) ] )
% 67.84/68.29 , 0, 9, substitution( 0, [ :=( X, btrue )] ), substitution( 1, [ :=( X, X )] )
% 67.84/68.29 ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31608, [ =( eps2( step( star( star( atom( X ) ) ), X ) ), btrue ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 430, [ =( eps2( y( step( X, Y ), eps ) ), eps2( step( star( X ),
% 67.84/68.29 Y ) ) ) ] )
% 67.84/68.29 , 0, clause( 31607, [ =( eps2( y( step( star( atom( X ) ), X ), eps ) ),
% 67.84/68.29 btrue ) ] )
% 67.84/68.29 , 0, 1, substitution( 0, [ :=( X, star( atom( X ) ) ), :=( Y, X )] ),
% 67.84/68.29 substitution( 1, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 1436, [ =( eps2( step( star( star( atom( X ) ) ), X ) ), btrue ) ]
% 67.84/68.29 )
% 67.84/68.29 , clause( 31608, [ =( eps2( step( star( star( atom( X ) ) ), X ) ), btrue )
% 67.84/68.29 ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31611, [ =( 'prop_same'( X, cons2( Y, Z ) ), eq2( rec( step( X, Y )
% 67.84/68.29 , Z ), reck2( X, cons2( Y, Z ) ) ) ) ] )
% 67.84/68.29 , clause( 399, [ =( eq2( rec( step( X, Y ), Z ), reck2( X, cons2( Y, Z ) )
% 67.84/68.29 ), 'prop_same'( X, cons2( Y, Z ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31612, [ =( 'prop_same'( X, cons2( Y, nil2 ) ), eq2( eps2( step( X
% 67.84/68.29 , Y ) ), reck2( X, cons2( Y, nil2 ) ) ) ) ] )
% 67.84/68.29 , clause( 87, [ =( rec( X, nil2 ), eps2( X ) ) ] )
% 67.84/68.29 , 0, clause( 31611, [ =( 'prop_same'( X, cons2( Y, Z ) ), eq2( rec( step( X
% 67.84/68.29 , Y ), Z ), reck2( X, cons2( Y, Z ) ) ) ) ] )
% 67.84/68.29 , 0, 7, substitution( 0, [ :=( X, step( X, Y ) )] ), substitution( 1, [
% 67.84/68.29 :=( X, X ), :=( Y, Y ), :=( Z, nil2 )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31613, [ =( eq2( eps2( step( X, Y ) ), reck2( X, cons2( Y, nil2 ) )
% 67.84/68.29 ), 'prop_same'( X, cons2( Y, nil2 ) ) ) ] )
% 67.84/68.29 , clause( 31612, [ =( 'prop_same'( X, cons2( Y, nil2 ) ), eq2( eps2( step(
% 67.84/68.29 X, Y ) ), reck2( X, cons2( Y, nil2 ) ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 4067, [ =( eq2( eps2( step( X, Y ) ), reck2( X, cons2( Y, nil2 ) )
% 67.84/68.29 ), 'prop_same'( X, cons2( Y, nil2 ) ) ) ] )
% 67.84/68.29 , clause( 31613, [ =( eq2( eps2( step( X, Y ) ), reck2( X, cons2( Y, nil2 )
% 67.84/68.29 ) ), 'prop_same'( X, cons2( Y, nil2 ) ) ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X ), :=( Y, Y )] ), permutation( 0, [ ==>( 0, 0
% 67.84/68.29 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31615, [ =( 'prop_same'( X, cons2( Y, nil2 ) ), eq2( eps2( step( X
% 67.84/68.29 , Y ) ), reck2( X, cons2( Y, nil2 ) ) ) ) ] )
% 67.84/68.29 , clause( 4067, [ =( eq2( eps2( step( X, Y ) ), reck2( X, cons2( Y, nil2 )
% 67.84/68.29 ) ), 'prop_same'( X, cons2( Y, nil2 ) ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31618, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X, nil2
% 67.84/68.29 ) ), eq2( btrue, reck2( star( star( atom( X ) ) ), cons2( X, nil2 ) ) )
% 67.84/68.29 ) ] )
% 67.84/68.29 , clause( 1436, [ =( eps2( step( star( star( atom( X ) ) ), X ) ), btrue )
% 67.84/68.29 ] )
% 67.84/68.29 , 0, clause( 31615, [ =( 'prop_same'( X, cons2( Y, nil2 ) ), eq2( eps2(
% 67.84/68.29 step( X, Y ) ), reck2( X, cons2( Y, nil2 ) ) ) ) ] )
% 67.84/68.29 , 0, 10, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, star(
% 67.84/68.29 star( atom( X ) ) ) ), :=( Y, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31619, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X, nil2
% 67.84/68.29 ) ), eq2( btrue, bfalse ) ) ] )
% 67.84/68.29 , clause( 887, [ =( reck2( star( star( X ) ), cons2( Y, Z ) ), bfalse ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, clause( 31618, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X,
% 67.84/68.29 nil2 ) ), eq2( btrue, reck2( star( star( atom( X ) ) ), cons2( X, nil2 )
% 67.84/68.29 ) ) ) ] )
% 67.84/68.29 , 0, 11, substitution( 0, [ :=( X, atom( X ) ), :=( Y, X ), :=( Z, nil2 )] )
% 67.84/68.29 , substitution( 1, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31620, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X, nil2
% 67.84/68.29 ) ), bfalse ) ] )
% 67.84/68.29 , clause( 109, [ =( eq2( btrue, bfalse ), bfalse ) ] )
% 67.84/68.29 , 0, clause( 31619, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X,
% 67.84/68.29 nil2 ) ), eq2( btrue, bfalse ) ) ] )
% 67.84/68.29 , 0, 9, substitution( 0, [] ), substitution( 1, [ :=( X, X )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 30037, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X, nil2
% 67.84/68.29 ) ), bfalse ) ] )
% 67.84/68.29 , clause( 31620, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X,
% 67.84/68.29 nil2 ) ), bfalse ) ] )
% 67.84/68.29 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqswap(
% 67.84/68.29 clause( 31623, [ ~( =( btrue, eq2( 'prop_same'( X, Y ), bfalse ) ) ) ] )
% 67.84/68.29 , clause( 112, [ ~( =( eq2( 'prop_same'( X, Y ), bfalse ), btrue ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [ :=( X, X ), :=( Y, Y )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31625, [ ~( =( btrue, eq2( bfalse, bfalse ) ) ) ] )
% 67.84/68.29 , clause( 30037, [ =( 'prop_same'( star( star( atom( X ) ) ), cons2( X,
% 67.84/68.29 nil2 ) ), bfalse ) ] )
% 67.84/68.29 , 0, clause( 31623, [ ~( =( btrue, eq2( 'prop_same'( X, Y ), bfalse ) ) ) ]
% 67.84/68.29 )
% 67.84/68.29 , 0, 4, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, star(
% 67.84/68.29 star( atom( X ) ) ) ), :=( Y, cons2( X, nil2 ) )] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 paramod(
% 67.84/68.29 clause( 31626, [ ~( =( btrue, btrue ) ) ] )
% 67.84/68.29 , clause( 111, [ =( eq2( X, X ), btrue ) ] )
% 67.84/68.29 , 0, clause( 31625, [ ~( =( btrue, eq2( bfalse, bfalse ) ) ) ] )
% 67.84/68.29 , 0, 3, substitution( 0, [ :=( X, bfalse )] ), substitution( 1, [] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 eqrefl(
% 67.84/68.29 clause( 31627, [] )
% 67.84/68.29 , clause( 31626, [ ~( =( btrue, btrue ) ) ] )
% 67.84/68.29 , 0, substitution( 0, [] )).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 subsumption(
% 67.84/68.29 clause( 30051, [] )
% 67.84/68.29 , clause( 31627, [] )
% 67.84/68.29 , substitution( 0, [] ), permutation( 0, [] ) ).
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 end.
% 67.84/68.29
% 67.84/68.29 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 67.84/68.29
% 67.84/68.29 Memory use:
% 67.84/68.29
% 67.84/68.29 space for terms: 441607
% 67.84/68.29 space for clauses: 2794376
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 clauses generated: 1008629
% 67.84/68.29 clauses kept: 30052
% 67.84/68.29 clauses selected: 6583
% 67.84/68.29 clauses deleted: 8855
% 67.84/68.29 clauses inuse deleted: 965
% 67.84/68.29
% 67.84/68.29 subsentry: 14993
% 67.84/68.29 literals s-matched: 10737
% 67.84/68.29 literals matched: 10737
% 67.84/68.29 full subsumption: 0
% 67.84/68.29
% 67.84/68.29 checksum: 846637632
% 67.84/68.29
% 67.84/68.29
% 67.84/68.29 Bliksem ended
%------------------------------------------------------------------------------