%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX208-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n011.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:48 PM UTC 2026
% Result : Timeout 299.44s 300.04s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX208-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : bliksem %s
% 0.16/0.33 % Computer : n011.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % DateTime : Tue May 5 11:39:02 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.73/1.14 *** allocated 10000 integers for termspace/termends
% 0.73/1.14 *** allocated 10000 integers for clauses
% 0.73/1.14 *** allocated 10000 integers for justifications
% 0.73/1.14 Bliksem 1.12
% 0.73/1.14
% 0.73/1.14
% 0.73/1.14 Automatic Strategy Selection
% 0.73/1.14
% 0.73/1.14 Clauses:
% 0.73/1.14 [
% 0.73/1.14 [ =( aux( X, pair2( Y, Z ) ), pair2( Y, s( Z ) ) ) ],
% 0.73/1.14 [ =( aux2( X, left( Y ) ), pair2( Y, z ) ) ],
% 0.73/1.14 [ =( aux2( X, right( Y ) ), aux( Y, mod10( Y ) ) ) ],
% 0.73/1.14 [ =( aux3( X, Y, pair2( Z, T ) ), showNumnum( cons( Z, X ), T ) ) ],
% 0.73/1.14 [ =( impl( btrue, X ), X ) ],
% 0.73/1.14 [ =( impl( bfalse, X ), btrue ) ],
% 0.73/1.14 [ =( append( nil, X ), X ) ],
% 0.73/1.14 [ =( append( cons( X, Y ), Z ), cons( X, append( Y, Z ) ) ) ],
% 0.73/1.14 [ =( x2( z, z ), z ) ],
% 0.73/1.14 [ =( x2( z, s( X ) ), z ) ],
% 0.73/1.14 [ =( x2( s( X ), z ), s( X ) ) ],
% 0.73/1.14 [ =( x2( s( X ), s( Y ) ), x2( X, Y ) ) ],
% 0.73/1.14 [ =( min10( z ), left( dIG0 ) ) ],
% 0.73/1.14 [ =( min10( s( z ) ), left( dIG1 ) ) ],
% 0.73/1.14 [ =( min10( s( s( z ) ) ), left( dIG2 ) ) ],
% 0.73/1.14 [ =( min10( s( s( s( z ) ) ) ), left( dIG3 ) ) ],
% 0.73/1.14 [ =( min10( s( s( s( s( z ) ) ) ) ), left( dIG4 ) ) ],
% 0.73/1.14 [ =( min10( s( s( s( s( s( z ) ) ) ) ) ), left( dIG5 ) ) ],
% 0.73/1.14 [ =( min10( s( s( s( s( s( s( z ) ) ) ) ) ) ), left( dIG6 ) ) ],
% 0.73/1.14 [ =( min10( s( s( s( s( s( s( s( z ) ) ) ) ) ) ) ), left( dIG7 ) ) ]
% 0.73/1.14 ,
% 0.73/1.14 [ =( min10( s( s( s( s( s( s( s( s( z ) ) ) ) ) ) ) ) ), left( dIG8 ) )
% 0.73/1.14 ],
% 0.73/1.14 [ =( min10( s( s( s( s( s( s( s( s( s( z ) ) ) ) ) ) ) ) ) ), left( dIG9
% 0.73/1.14 ) ) ],
% 0.73/1.14 [ =( min10( s( s( s( s( s( s( s( s( s( s( X ) ) ) ) ) ) ) ) ) ) ), right(
% 0.73/1.14 x2( s( s( s( s( s( s( s( s( s( s( X ) ) ) ) ) ) ) ) ) ), s( s( s( s( s( s(
% 0.73/1.14 s( s( s( s( z ) ) ) ) ) ) ) ) ) ) ) ) ) ],
% 0.73/1.14 [ =( mod10( X ), aux2( X, min10( X ) ) ) ],
% 0.73/1.14 [ =( showNumnum( X, z ), X ) ],
% 0.73/1.14 [ =( showNumnum( X, s( Y ) ), aux3( X, Y, mod10( s( Y ) ) ) ) ],
% 0.73/1.14 [ =( showNum( z ), cons( dIG0, nil ) ) ],
% 0.73/1.14 [ =( showNum( s( X ) ), showNumnum( nil, s( X ) ) ) ],
% 0.73/1.14 [ =( show( x ), cons( cHARX, nil ) ) ],
% 0.73/1.14 [ =( show( add( X, Y ) ), append( show( X ), append( cons( pLUS, nil ),
% 0.73/1.14 show( Y ) ) ) ) ],
% 0.73/1.14 [ =( show( mul( X, Y ) ), append( showF( X ), append( cons( mULT, nil )
% 0.73/1.14 , showF( Y ) ) ) ) ],
% 0.73/1.14 [ =( show( num( X ) ), showNum( X ) ) ],
% 0.73/1.14 [ =( showF( add( X, Y ) ), cons( pAR1, append( show( add( X, Y ) ), cons(
% 0.73/1.14 pAR2, nil ) ) ) ) ],
% 0.73/1.14 [ =( showF( x ), show( x ) ) ],
% 0.73/1.14 [ =( showF( mul( X, Y ) ), show( mul( X, Y ) ) ) ],
% 0.73/1.14 [ =( showF( num( X ) ), show( num( X ) ) ) ],
% 0.73/1.14 [ =( prop3( X ), impl( eq( show( X ), cons( pAR1, cons( pAR1, cons(
% 0.73/1.14 cHARX, cons( pLUS, cons( dIG5, cons( pAR2, cons( pLUS, cons( dIG7, cons(
% 0.73/1.14 pAR2, cons( mULT, cons( cHARX, nil ) ) ) ) ) ) ) ) ) ) ) ), eq5( btrue,
% 0.73/1.14 bfalse ) ) ) ],
% 0.73/1.14 [ =( eq4( pAR1, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR1, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pAR2, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( pLUS, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( mULT, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( cHARX, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG0, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG1, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG2, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG4 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG3, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, mULT ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, cHARX ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG0 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG3 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG5 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG6 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG7 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG8 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG4, dIG9 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG5, pAR1 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG5, pAR2 ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG5, pLUS ), bfalse ) ],
% 0.73/1.14 [ =( eq4( dIG5, mULT ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, cHARX ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG0 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG3 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG4 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG6 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG7 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG8 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG5, dIG9 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, pAR1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, pAR2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, pLUS ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, mULT ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, cHARX ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG0 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG3 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG4 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG5 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG7 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG8 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG6, dIG9 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, pAR1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, pAR2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, pLUS ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, mULT ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, cHARX ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG0 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG3 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG4 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG5 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG6 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG8 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG7, dIG9 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, pAR1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, pAR2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, pLUS ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, mULT ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, cHARX ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG0 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG3 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG4 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG5 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG6 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG7 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG8, dIG9 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, pAR1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, pAR2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, pLUS ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, mULT ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, cHARX ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG0 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG1 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG2 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG3 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG4 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG5 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG6 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG7 ), bfalse ) ],
% 0.77/1.65 [ =( eq4( dIG9, dIG8 ), bfalse ) ],
% 0.77/1.65 [ =( eq5( bfalse, btrue ), bfalse ) ],
% 0.77/1.65 [ =( eq5( btrue, bfalse ), bfalse ) ],
% 0.77/1.65 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( add( X, Z ), add( Y, T ) ),
% 0.77/1.65 bfalse ) ],
% 0.77/1.65 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( add( X, Z ), add( Y, T ) ), eq3(
% 0.77/1.65 Z, T ) ) ],
% 0.77/1.65 [ ~( =( eq3( X, Y ), bfalse ) ), =( eq3( mul( X, Z ), mul( Y, T ) ),
% 0.77/1.65 bfalse ) ],
% 0.77/1.65 [ ~( =( eq3( X, Y ), btrue ) ), =( eq3( mul( X, Z ), mul( Y, T ) ), eq3(
% 0.77/1.65 Z, T ) ) ],
% 0.77/1.65 [ =( eq3( num( X ), num( Y ) ), eq2( X, Y ) ) ],
% 0.77/1.65 [ =( eq3( x, add( X, Y ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( x, mul( X, Y ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( x, num( X ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( add( X, Y ), x ), bfalse ) ],
% 0.77/1.65 [ =( eq3( add( X, Y ), mul( Z, T ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( add( X, Y ), num( Z ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( mul( X, Y ), x ), bfalse ) ],
% 0.77/1.65 [ =( eq3( mul( X, Y ), add( Z, T ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( mul( X, Y ), num( Z ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( num( X ), x ), bfalse ) ],
% 0.77/1.65 [ =( eq3( num( X ), add( Y, Z ) ), bfalse ) ],
% 0.77/1.65 [ =( eq3( num( X ), mul( Y, Z ) ), bfalse ) ],
% 0.77/1.65 [ =( eq2( s( X ), s( Y ) ), eq2( X, Y ) ) ],
% 0.77/1.65 [ =( eq2( z, s( X ) ), bfalse ) ],
% 0.77/1.65 [ =( eq2( s( X ), z ), bfalse ) ],
% 0.77/1.65 [ =( eq( X, X ), btrue ) ],
% 0.77/1.65 [ =( eq2( X, X ), btrue ) ],
% 0.77/1.65 [ =( eq3( X, X ), btrue ) ],
% 0.77/1.65 [ =( eq4( X, X ), btrue ) ],
% 0.77/1.65 [ =( eq5( X, X ), btrue ) ],
% 0.77/1.65 [ ~( =( eq4( X, Y ), bfalse ) ), =( eq( cons( X, Z ), cons( Y, T ) ),
% 0.77/1.65 bfalse ) ],
% 0.77/1.65 [ ~( =( eq4( X, Y ), btrue ) ), =( eq( cons( X, Z ), cons( Y, T ) ), eq(
% 24.52/24.95 Z, T ) ) ],
% 24.52/24.95 [ =( eq( nil, cons( X, Y ) ), bfalse ) ],
% 24.52/24.95 [ =( eq( cons( X, Y ), nil ), bfalse ) ],
% 24.52/24.95 [ ~( =( eq5( prop3( X ), bfalse ), btrue ) ) ]
% 24.52/24.95 ] .
% 24.52/24.95
% 24.52/24.95
% 24.52/24.95 percentage equality = 1.000000, percentage horn = 1.000000
% 24.52/24.95 This is a pure equality problem
% 24.52/24.95
% 24.52/24.95
% 24.52/24.95
% 24.52/24.95 Options Used:
% 24.52/24.95
% 24.52/24.95 useres = 1
% 24.52/24.95 useparamod = 1
% 24.52/24.95 useeqrefl = 1
% 24.52/24.95 useeqfact = 1
% 24.52/24.95 usefactor = 1
% 24.52/24.95 usesimpsplitting = 0
% 24.52/24.95 usesimpdemod = 5
% 24.52/24.95 usesimpres = 3
% 24.52/24.95
% 24.52/24.95 resimpinuse = 1000
% 24.52/24.95 resimpclauses = 20000
% 24.52/24.95 substype = eqrewr
% 24.52/24.95 backwardsubs = 1
% 24.52/24.95 selectoldest = 5
% 24.52/24.95
% 24.52/24.95 litorderings [0] = split
% 24.52/24.95 litorderings [1] = extend the termordering, first sorting on arguments
% 24.52/24.95
% 24.52/24.95 termordering = kbo
% 24.52/24.95
% 24.52/24.95 litapriori = 0
% 24.52/24.95 termapriori = 1
% 24.52/24.95 litaposteriori = 0
% 24.52/24.95 termaposteriori = 0
% 24.52/24.95 demodaposteriori = 0
% 24.52/24.95 ordereqreflfact = 0
% 24.52/24.95
% 24.52/24.95 litselect = negord
% 24.52/24.95
% 24.52/24.95 maxweight = 15
% 24.52/24.95 maxdepth = 30000
% 24.52/24.95 maxlength = 115
% 24.52/24.95 maxnrvars = 195
% 24.52/24.95 excuselevel = 1
% 24.52/24.95 increasemaxweight = 1
% 24.52/24.95
% 24.52/24.95 maxselected = 10000000
% 24.52/24.95 maxnrclauses = 10000000
% 24.52/24.95
% 24.52/24.95 showgenerated = 0
% 24.52/24.95 showkept = 0
% 24.52/24.95 showselected = 0
% 24.52/24.95 showdeleted = 0
% 24.52/24.95 showresimp = 1
% 24.52/24.95 showstatus = 2000
% 24.52/24.95
% 24.52/24.95 prologoutput = 1
% 24.52/24.95 nrgoals = 5000000
% 24.52/24.95 totalproof = 1
% 24.52/24.95
% 24.52/24.95 Symbols occurring in the translation:
% 24.52/24.95
% 24.52/24.95 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 24.52/24.95 . [1, 2] (w:1, o:61, a:1, s:1, b:0),
% 24.52/24.95 ! [4, 1] (w:0, o:46, a:1, s:1, b:0),
% 24.52/24.95 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 24.52/24.95 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 24.52/24.95 pair2 [42, 2] (w:1, o:86, a:1, s:1, b:0),
% 24.52/24.95 aux [43, 2] (w:1, o:87, a:1, s:1, b:0),
% 24.52/24.95 s [44, 1] (w:1, o:52, a:1, s:1, b:0),
% 24.52/24.95 left [47, 1] (w:1, o:53, a:1, s:1, b:0),
% 24.52/24.95 aux2 [48, 2] (w:1, o:88, a:1, s:1, b:0),
% 24.52/24.95 z [49, 0] (w:1, o:17, a:1, s:1, b:0),
% 24.52/24.95 right [50, 1] (w:1, o:51, a:1, s:1, b:0),
% 24.52/24.95 mod10 [51, 1] (w:1, o:54, a:1, s:1, b:0),
% 24.52/24.95 aux3 [54, 3] (w:1, o:101, a:1, s:1, b:0),
% 24.52/24.95 cons [55, 2] (w:1, o:89, a:1, s:1, b:0),
% 24.52/24.95 showNumnum [56, 2] (w:1, o:90, a:1, s:1, b:0),
% 24.52/24.95 btrue [57, 0] (w:1, o:24, a:1, s:1, b:0),
% 24.52/24.95 impl [59, 2] (w:1, o:91, a:1, s:1, b:0),
% 24.52/24.95 bfalse [60, 0] (w:1, o:26, a:1, s:1, b:0),
% 24.52/24.95 nil [61, 0] (w:1, o:28, a:1, s:1, b:0),
% 24.52/24.95 append [63, 2] (w:1, o:92, a:1, s:1, b:0),
% 24.52/24.95 x2 [65, 2] (w:1, o:93, a:1, s:1, b:0),
% 24.52/24.95 min10 [67, 1] (w:1, o:55, a:1, s:1, b:0),
% 24.52/24.95 dIG0 [68, 0] (w:1, o:30, a:1, s:1, b:0),
% 24.52/24.95 dIG1 [69, 0] (w:1, o:31, a:1, s:1, b:0),
% 24.52/24.95 dIG2 [70, 0] (w:1, o:32, a:1, s:1, b:0),
% 24.52/24.95 dIG3 [71, 0] (w:1, o:33, a:1, s:1, b:0),
% 24.52/24.95 dIG4 [72, 0] (w:1, o:34, a:1, s:1, b:0),
% 24.52/24.95 dIG5 [73, 0] (w:1, o:35, a:1, s:1, b:0),
% 24.52/24.95 dIG6 [74, 0] (w:1, o:36, a:1, s:1, b:0),
% 24.52/24.95 dIG7 [75, 0] (w:1, o:37, a:1, s:1, b:0),
% 24.52/24.95 dIG8 [76, 0] (w:1, o:38, a:1, s:1, b:0),
% 24.52/24.95 dIG9 [77, 0] (w:1, o:39, a:1, s:1, b:0),
% 24.52/24.95 showNum [79, 1] (w:1, o:56, a:1, s:1, b:0),
% 24.52/24.95 x [80, 0] (w:1, o:40, a:1, s:1, b:0),
% 24.52/24.95 show [81, 1] (w:1, o:57, a:1, s:1, b:0),
% 24.52/24.95 cHARX [82, 0] (w:1, o:29, a:1, s:1, b:0),
% 24.52/24.95 add [85, 2] (w:1, o:94, a:1, s:1, b:0),
% 24.52/24.95 pLUS [86, 0] (w:1, o:43, a:1, s:1, b:0),
% 24.52/24.95 mul [89, 2] (w:1, o:95, a:1, s:1, b:0),
% 24.52/24.95 showF [90, 1] (w:1, o:58, a:1, s:1, b:0),
% 24.52/24.95 mULT [91, 0] (w:1, o:27, a:1, s:1, b:0),
% 24.52/24.95 num [92, 1] (w:1, o:59, a:1, s:1, b:0),
% 24.52/24.95 pAR1 [93, 0] (w:1, o:44, a:1, s:1, b:0),
% 24.52/24.95 pAR2 [94, 0] (w:1, o:45, a:1, s:1, b:0),
% 24.52/24.95 prop3 [96, 1] (w:1, o:60, a:1, s:1, b:0),
% 24.52/24.95 eq [97, 2] (w:1, o:96, a:1, s:1, b:0),
% 24.52/24.95 eq5 [98, 2] (w:1, o:100, a:1, s:1, b:0),
% 24.52/24.95 eq4 [99, 2] (w:1, o:99, a:1, s:1, b:0),
% 24.52/24.95 eq3 [100, 2] (w:1, o:98, a:1, s:1, b:0),
% 24.52/24.95 eq2 [101, 2] (w:1, o:97, a:1, s:1, b:0).
% 24.52/24.95
% 24.52/24.95
% 24.52/24.95 Starting Search:
% 24.52/24.95
% 24.52/24.95 Resimplifying inuse:
% 24.52/24.95 Done
% 24.52/24.95
% 24.52/24.95 Resimplifying inuse:
% 24.52/24.95 Done
% 24.52/24.95
% 24.52/24.95 Failed to find proof!
% 24.52/24.95 maxweight = 15
% 24.52/24.95 maxnrclauses = 10000000
% 24.52/24.95 Generated: 19673
% 24.52/24.95 Kept: 1727
% 24.52/24.95
% 24.52/24.95
% 24.52/24.95 The strategy used was not complete!
% 24.52/24.95
% 24.52/24.95 Increased maxweight to 16
% 24.52/24.95
% 24.52/24.95 Starting Search:
% 24.52/24.95
% 24.52/24.95 Resimplifying inuse:
% 24.52/24.95 Done
% 24.52/24.95
% 24.52/24.95
% 24.52/24.95 Intermediate Status:
% 24.52/24.95 Generated: 20456
% 24.52/24.95 Kept: 2008
% 24.52/24.95 Inuse: 1327
% 24.52/24.95 Deleted: 167
% 101.15/101.65 Deletedinuse: 3
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Failed to find proof!
% 101.15/101.65 maxweight = 16
% 101.15/101.65 maxnrclauses = 10000000
% 101.15/101.65 Generated: 29306
% 101.15/101.65 Kept: 3074
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 The strategy used was not complete!
% 101.15/101.65
% 101.15/101.65 Increased maxweight to 17
% 101.15/101.65
% 101.15/101.65 Starting Search:
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 20495
% 101.15/101.65 Kept: 2002
% 101.15/101.65 Inuse: 1307
% 101.15/101.65 Deleted: 196
% 101.15/101.65 Deletedinuse: 3
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 34838
% 101.15/101.65 Kept: 4006
% 101.15/101.65 Inuse: 2272
% 101.15/101.65 Deleted: 799
% 101.15/101.65 Deletedinuse: 6
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Failed to find proof!
% 101.15/101.65 maxweight = 17
% 101.15/101.65 maxnrclauses = 10000000
% 101.15/101.65 Generated: 55782
% 101.15/101.65 Kept: 5712
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 The strategy used was not complete!
% 101.15/101.65
% 101.15/101.65 Increased maxweight to 18
% 101.15/101.65
% 101.15/101.65 Starting Search:
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 22679
% 101.15/101.65 Kept: 2000
% 101.15/101.65 Inuse: 1334
% 101.15/101.65 Deleted: 247
% 101.15/101.65 Deletedinuse: 3
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 39081
% 101.15/101.65 Kept: 4002
% 101.15/101.65 Inuse: 2136
% 101.15/101.65 Deleted: 659
% 101.15/101.65 Deletedinuse: 6
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 57490
% 101.15/101.65 Kept: 6004
% 101.15/101.65 Inuse: 3262
% 101.15/101.65 Deleted: 1208
% 101.15/101.65 Deletedinuse: 7
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 89010
% 101.15/101.65 Kept: 8004
% 101.15/101.65 Inuse: 5301
% 101.15/101.65 Deleted: 2433
% 101.15/101.65 Deletedinuse: 7
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Failed to find proof!
% 101.15/101.65 maxweight = 18
% 101.15/101.65 maxnrclauses = 10000000
% 101.15/101.65 Generated: 91113
% 101.15/101.65 Kept: 8154
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 The strategy used was not complete!
% 101.15/101.65
% 101.15/101.65 Increased maxweight to 19
% 101.15/101.65
% 101.15/101.65 Starting Search:
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 26149
% 101.15/101.65 Kept: 2006
% 101.15/101.65 Inuse: 1392
% 101.15/101.65 Deleted: 291
% 101.15/101.65 Deletedinuse: 3
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 40837
% 101.15/101.65 Kept: 4007
% 101.15/101.65 Inuse: 2122
% 101.15/101.65 Deleted: 419
% 101.15/101.65 Deletedinuse: 6
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 54155
% 101.15/101.65 Kept: 6009
% 101.15/101.65 Inuse: 2811
% 101.15/101.65 Deleted: 846
% 101.15/101.65 Deletedinuse: 7
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 75835
% 101.15/101.65 Kept: 8009
% 101.15/101.65 Inuse: 3862
% 101.15/101.65 Deleted: 1428
% 101.15/101.65 Deletedinuse: 7
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 116989
% 101.15/101.65 Kept: 10011
% 101.15/101.65 Inuse: 5606
% 101.15/101.65 Deleted: 2602
% 101.15/101.65 Deletedinuse: 14
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 141062
% 101.15/101.65 Kept: 12013
% 101.15/101.65 Inuse: 6807
% 101.15/101.65 Deleted: 3497
% 101.15/101.65 Deletedinuse: 24
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 157376
% 101.15/101.65 Kept: 14013
% 101.15/101.65 Inuse: 7755
% 101.15/101.65 Deleted: 4433
% 101.15/101.65 Deletedinuse: 24
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Failed to find proof!
% 101.15/101.65 maxweight = 19
% 101.15/101.65 maxnrclauses = 10000000
% 101.15/101.65 Generated: 186548
% 101.15/101.65 Kept: 15877
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 The strategy used was not complete!
% 101.15/101.65
% 101.15/101.65 Increased maxweight to 20
% 101.15/101.65
% 101.15/101.65 Starting Search:
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 22896
% 101.15/101.65 Kept: 2032
% 101.15/101.65 Inuse: 1259
% 101.15/101.65 Deleted: 247
% 101.15/101.65 Deletedinuse: 3
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 55173
% 101.15/101.65 Kept: 4035
% 101.15/101.65 Inuse: 2105
% 101.15/101.65 Deleted: 479
% 101.15/101.65 Deletedinuse: 6
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 78830
% 101.15/101.65 Kept: 6041
% 101.15/101.65 Inuse: 2787
% 101.15/101.65 Deleted: 850
% 101.15/101.65 Deletedinuse: 7
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 95382
% 101.15/101.65 Kept: 8045
% 101.15/101.65 Inuse: 3618
% 101.15/101.65 Deleted: 1190
% 101.15/101.65 Deletedinuse: 13
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 113353
% 101.15/101.65 Kept: 10080
% 101.15/101.65 Inuse: 4254
% 101.15/101.65 Deleted: 1684
% 101.15/101.65 Deletedinuse: 13
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65 Resimplifying inuse:
% 101.15/101.65 Done
% 101.15/101.65
% 101.15/101.65
% 101.15/101.65 Intermediate Status:
% 101.15/101.65 Generated: 128555
% 101.15/101.65 Kept: 12084
% 299.44/300.04 Terminated
% 299.44/300.04 Bliksem ended
%------------------------------------------------------------------------------