Bliksem---1.12.TMO-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Bliksem---1.12
% Problem  : SWC089+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : bliksem %s

% Computer : n027.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 Jul 19 19:33:41 EDT 2022

% Result   : Timeout 300.03s 300.45s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : SWC089+1 : TPTP v8.1.0. Released v2.4.0.
% 0.04/0.12  % Command  : bliksem %s
% 0.12/0.33  % Computer : n027.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % DateTime : Sun Jun 12 04:39:30 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.69/1.14  *** allocated 10000 integers for termspace/termends
% 0.69/1.14  *** allocated 10000 integers for clauses
% 0.69/1.14  *** allocated 10000 integers for justifications
% 0.69/1.14  Bliksem 1.12
% 0.69/1.14  
% 0.69/1.14  
% 0.69/1.14  Automatic Strategy Selection
% 0.69/1.14  
% 0.69/1.14  *** allocated 15000 integers for termspace/termends
% 0.69/1.14  
% 0.69/1.14  Clauses:
% 0.69/1.14  
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! neq( X, Y ), ! X = Y }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), X = Y, neq( X, Y ) }.
% 0.69/1.14  { ssItem( skol1 ) }.
% 0.69/1.14  { ssItem( skol47 ) }.
% 0.69/1.14  { ! skol1 = skol47 }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ! memberP( X, Y ), ssList( skol2( Z, T ) )
% 0.69/1.14     }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ! memberP( X, Y ), alpha1( X, Y, skol2( X, 
% 0.69/1.14    Y ) ) }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ! ssList( Z ), ! alpha1( X, Y, Z ), memberP
% 0.69/1.14    ( X, Y ) }.
% 0.69/1.14  { ! alpha1( X, Y, Z ), ssList( skol3( T, U, W ) ) }.
% 0.69/1.14  { ! alpha1( X, Y, Z ), app( Z, cons( Y, skol3( X, Y, Z ) ) ) = X }.
% 0.69/1.14  { ! ssList( T ), ! app( Z, cons( Y, T ) ) = X, alpha1( X, Y, Z ) }.
% 0.69/1.14  { ! ssList( X ), ! singletonP( X ), ssItem( skol4( Y ) ) }.
% 0.69/1.14  { ! ssList( X ), ! singletonP( X ), cons( skol4( X ), nil ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ! cons( Y, nil ) = X, singletonP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! frontsegP( X, Y ), ssList( skol5( Z, T )
% 0.69/1.14     ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! frontsegP( X, Y ), app( Y, skol5( X, Y )
% 0.69/1.14     ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Y, Z ) = X, frontsegP
% 0.69/1.14    ( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X, Y ), ssList( skol6( Z, T ) )
% 0.69/1.14     }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X, Y ), app( skol6( X, Y ), Y )
% 0.69/1.14     = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Z, Y ) = X, rearsegP
% 0.69/1.14    ( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! segmentP( X, Y ), ssList( skol7( Z, T ) )
% 0.69/1.14     }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! segmentP( X, Y ), alpha2( X, Y, skol7( X
% 0.69/1.14    , Y ) ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! alpha2( X, Y, Z ), 
% 0.69/1.14    segmentP( X, Y ) }.
% 0.69/1.14  { ! alpha2( X, Y, Z ), ssList( skol8( T, U, W ) ) }.
% 0.69/1.14  { ! alpha2( X, Y, Z ), app( app( Z, Y ), skol8( X, Y, Z ) ) = X }.
% 0.69/1.14  { ! ssList( T ), ! app( app( Z, Y ), T ) = X, alpha2( X, Y, Z ) }.
% 0.69/1.14  { ! ssList( X ), ! cyclefreeP( X ), ! ssItem( Y ), alpha3( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol9( Y ) ), cyclefreeP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha3( X, skol9( X ) ), cyclefreeP( X ) }.
% 0.69/1.14  { ! alpha3( X, Y ), ! ssItem( Z ), alpha21( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol10( Z, T ) ), alpha3( X, Y ) }.
% 0.69/1.14  { ! alpha21( X, Y, skol10( X, Y ) ), alpha3( X, Y ) }.
% 0.69/1.14  { ! alpha21( X, Y, Z ), ! ssList( T ), alpha28( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol11( T, U, W ) ), alpha21( X, Y, Z ) }.
% 0.69/1.14  { ! alpha28( X, Y, Z, skol11( X, Y, Z ) ), alpha21( X, Y, Z ) }.
% 0.69/1.14  { ! alpha28( X, Y, Z, T ), ! ssList( U ), alpha35( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol12( U, W, V0, V1 ) ), alpha28( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha35( X, Y, Z, T, skol12( X, Y, Z, T ) ), alpha28( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha35( X, Y, Z, T, U ), ! ssList( W ), alpha41( X, Y, Z, T, U, W ) }
% 0.69/1.14    .
% 0.69/1.14  { ssList( skol13( W, V0, V1, V2, V3 ) ), alpha35( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! alpha41( X, Y, Z, T, U, skol13( X, Y, Z, T, U ) ), alpha35( X, Y, Z, T
% 0.69/1.14    , U ) }.
% 0.69/1.14  { ! alpha41( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.69/1.14     ) ) = X, alpha12( Y, Z ) }.
% 0.69/1.14  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha41( X, Y, Z, T, U, 
% 0.69/1.14    W ) }.
% 0.69/1.14  { ! alpha12( Y, Z ), alpha41( X, Y, Z, T, U, W ) }.
% 0.69/1.14  { ! alpha12( X, Y ), ! leq( X, Y ), ! leq( Y, X ) }.
% 0.69/1.14  { leq( X, Y ), alpha12( X, Y ) }.
% 0.69/1.14  { leq( Y, X ), alpha12( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ! totalorderP( X ), ! ssItem( Y ), alpha4( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol14( Y ) ), totalorderP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha4( X, skol14( X ) ), totalorderP( X ) }.
% 0.69/1.14  { ! alpha4( X, Y ), ! ssItem( Z ), alpha22( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol15( Z, T ) ), alpha4( X, Y ) }.
% 0.69/1.14  { ! alpha22( X, Y, skol15( X, Y ) ), alpha4( X, Y ) }.
% 0.69/1.14  { ! alpha22( X, Y, Z ), ! ssList( T ), alpha29( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol16( T, U, W ) ), alpha22( X, Y, Z ) }.
% 0.69/1.14  { ! alpha29( X, Y, Z, skol16( X, Y, Z ) ), alpha22( X, Y, Z ) }.
% 0.69/1.14  { ! alpha29( X, Y, Z, T ), ! ssList( U ), alpha36( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol17( U, W, V0, V1 ) ), alpha29( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha36( X, Y, Z, T, skol17( X, Y, Z, T ) ), alpha29( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha36( X, Y, Z, T, U ), ! ssList( W ), alpha42( X, Y, Z, T, U, W ) }
% 0.69/1.14    .
% 0.69/1.14  { ssList( skol18( W, V0, V1, V2, V3 ) ), alpha36( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! alpha42( X, Y, Z, T, U, skol18( X, Y, Z, T, U ) ), alpha36( X, Y, Z, T
% 0.69/1.14    , U ) }.
% 0.69/1.14  { ! alpha42( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.69/1.14     ) ) = X, alpha13( Y, Z ) }.
% 0.69/1.14  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha42( X, Y, Z, T, U, 
% 0.69/1.14    W ) }.
% 0.69/1.14  { ! alpha13( Y, Z ), alpha42( X, Y, Z, T, U, W ) }.
% 0.69/1.14  { ! alpha13( X, Y ), leq( X, Y ), leq( Y, X ) }.
% 0.69/1.14  { ! leq( X, Y ), alpha13( X, Y ) }.
% 0.69/1.14  { ! leq( Y, X ), alpha13( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ! strictorderP( X ), ! ssItem( Y ), alpha5( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol19( Y ) ), strictorderP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha5( X, skol19( X ) ), strictorderP( X ) }.
% 0.69/1.14  { ! alpha5( X, Y ), ! ssItem( Z ), alpha23( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol20( Z, T ) ), alpha5( X, Y ) }.
% 0.69/1.14  { ! alpha23( X, Y, skol20( X, Y ) ), alpha5( X, Y ) }.
% 0.69/1.14  { ! alpha23( X, Y, Z ), ! ssList( T ), alpha30( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol21( T, U, W ) ), alpha23( X, Y, Z ) }.
% 0.69/1.14  { ! alpha30( X, Y, Z, skol21( X, Y, Z ) ), alpha23( X, Y, Z ) }.
% 0.69/1.14  { ! alpha30( X, Y, Z, T ), ! ssList( U ), alpha37( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol22( U, W, V0, V1 ) ), alpha30( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha37( X, Y, Z, T, skol22( X, Y, Z, T ) ), alpha30( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha37( X, Y, Z, T, U ), ! ssList( W ), alpha43( X, Y, Z, T, U, W ) }
% 0.69/1.14    .
% 0.69/1.14  { ssList( skol23( W, V0, V1, V2, V3 ) ), alpha37( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! alpha43( X, Y, Z, T, U, skol23( X, Y, Z, T, U ) ), alpha37( X, Y, Z, T
% 0.69/1.14    , U ) }.
% 0.69/1.14  { ! alpha43( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.69/1.14     ) ) = X, alpha14( Y, Z ) }.
% 0.69/1.14  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha43( X, Y, Z, T, U, 
% 0.69/1.14    W ) }.
% 0.69/1.14  { ! alpha14( Y, Z ), alpha43( X, Y, Z, T, U, W ) }.
% 0.69/1.14  { ! alpha14( X, Y ), lt( X, Y ), lt( Y, X ) }.
% 0.69/1.14  { ! lt( X, Y ), alpha14( X, Y ) }.
% 0.69/1.14  { ! lt( Y, X ), alpha14( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ! totalorderedP( X ), ! ssItem( Y ), alpha6( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol24( Y ) ), totalorderedP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha6( X, skol24( X ) ), totalorderedP( X ) }.
% 0.69/1.14  { ! alpha6( X, Y ), ! ssItem( Z ), alpha15( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol25( Z, T ) ), alpha6( X, Y ) }.
% 0.69/1.14  { ! alpha15( X, Y, skol25( X, Y ) ), alpha6( X, Y ) }.
% 0.69/1.14  { ! alpha15( X, Y, Z ), ! ssList( T ), alpha24( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol26( T, U, W ) ), alpha15( X, Y, Z ) }.
% 0.69/1.14  { ! alpha24( X, Y, Z, skol26( X, Y, Z ) ), alpha15( X, Y, Z ) }.
% 0.69/1.14  { ! alpha24( X, Y, Z, T ), ! ssList( U ), alpha31( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol27( U, W, V0, V1 ) ), alpha24( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha31( X, Y, Z, T, skol27( X, Y, Z, T ) ), alpha24( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha31( X, Y, Z, T, U ), ! ssList( W ), alpha38( X, Y, Z, T, U, W ) }
% 0.69/1.14    .
% 0.69/1.14  { ssList( skol28( W, V0, V1, V2, V3 ) ), alpha31( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! alpha38( X, Y, Z, T, U, skol28( X, Y, Z, T, U ) ), alpha31( X, Y, Z, T
% 0.69/1.14    , U ) }.
% 0.69/1.14  { ! alpha38( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.69/1.14     ) ) = X, leq( Y, Z ) }.
% 0.69/1.14  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha38( X, Y, Z, T, U, 
% 0.69/1.14    W ) }.
% 0.69/1.14  { ! leq( Y, Z ), alpha38( X, Y, Z, T, U, W ) }.
% 0.69/1.14  { ! ssList( X ), ! strictorderedP( X ), ! ssItem( Y ), alpha7( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol29( Y ) ), strictorderedP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha7( X, skol29( X ) ), strictorderedP( X ) }.
% 0.69/1.14  { ! alpha7( X, Y ), ! ssItem( Z ), alpha16( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol30( Z, T ) ), alpha7( X, Y ) }.
% 0.69/1.14  { ! alpha16( X, Y, skol30( X, Y ) ), alpha7( X, Y ) }.
% 0.69/1.14  { ! alpha16( X, Y, Z ), ! ssList( T ), alpha25( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol31( T, U, W ) ), alpha16( X, Y, Z ) }.
% 0.69/1.14  { ! alpha25( X, Y, Z, skol31( X, Y, Z ) ), alpha16( X, Y, Z ) }.
% 0.69/1.14  { ! alpha25( X, Y, Z, T ), ! ssList( U ), alpha32( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol32( U, W, V0, V1 ) ), alpha25( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha32( X, Y, Z, T, skol32( X, Y, Z, T ) ), alpha25( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha32( X, Y, Z, T, U ), ! ssList( W ), alpha39( X, Y, Z, T, U, W ) }
% 0.69/1.14    .
% 0.69/1.14  { ssList( skol33( W, V0, V1, V2, V3 ) ), alpha32( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! alpha39( X, Y, Z, T, U, skol33( X, Y, Z, T, U ) ), alpha32( X, Y, Z, T
% 0.69/1.14    , U ) }.
% 0.69/1.14  { ! alpha39( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.69/1.14     ) ) = X, lt( Y, Z ) }.
% 0.69/1.14  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha39( X, Y, Z, T, U, 
% 0.69/1.14    W ) }.
% 0.69/1.14  { ! lt( Y, Z ), alpha39( X, Y, Z, T, U, W ) }.
% 0.69/1.14  { ! ssList( X ), ! duplicatefreeP( X ), ! ssItem( Y ), alpha8( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol34( Y ) ), duplicatefreeP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha8( X, skol34( X ) ), duplicatefreeP( X ) }.
% 0.69/1.14  { ! alpha8( X, Y ), ! ssItem( Z ), alpha17( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol35( Z, T ) ), alpha8( X, Y ) }.
% 0.69/1.14  { ! alpha17( X, Y, skol35( X, Y ) ), alpha8( X, Y ) }.
% 0.69/1.14  { ! alpha17( X, Y, Z ), ! ssList( T ), alpha26( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol36( T, U, W ) ), alpha17( X, Y, Z ) }.
% 0.69/1.14  { ! alpha26( X, Y, Z, skol36( X, Y, Z ) ), alpha17( X, Y, Z ) }.
% 0.69/1.14  { ! alpha26( X, Y, Z, T ), ! ssList( U ), alpha33( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol37( U, W, V0, V1 ) ), alpha26( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha33( X, Y, Z, T, skol37( X, Y, Z, T ) ), alpha26( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha33( X, Y, Z, T, U ), ! ssList( W ), alpha40( X, Y, Z, T, U, W ) }
% 0.69/1.14    .
% 0.69/1.14  { ssList( skol38( W, V0, V1, V2, V3 ) ), alpha33( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! alpha40( X, Y, Z, T, U, skol38( X, Y, Z, T, U ) ), alpha33( X, Y, Z, T
% 0.69/1.14    , U ) }.
% 0.69/1.14  { ! alpha40( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.69/1.14     ) ) = X, ! Y = Z }.
% 0.69/1.14  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha40( X, Y, Z, T, U, 
% 0.69/1.14    W ) }.
% 0.69/1.14  { Y = Z, alpha40( X, Y, Z, T, U, W ) }.
% 0.69/1.14  { ! ssList( X ), ! equalelemsP( X ), ! ssItem( Y ), alpha9( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ssItem( skol39( Y ) ), equalelemsP( X ) }.
% 0.69/1.14  { ! ssList( X ), ! alpha9( X, skol39( X ) ), equalelemsP( X ) }.
% 0.69/1.14  { ! alpha9( X, Y ), ! ssItem( Z ), alpha18( X, Y, Z ) }.
% 0.69/1.14  { ssItem( skol40( Z, T ) ), alpha9( X, Y ) }.
% 0.69/1.14  { ! alpha18( X, Y, skol40( X, Y ) ), alpha9( X, Y ) }.
% 0.69/1.14  { ! alpha18( X, Y, Z ), ! ssList( T ), alpha27( X, Y, Z, T ) }.
% 0.69/1.14  { ssList( skol41( T, U, W ) ), alpha18( X, Y, Z ) }.
% 0.69/1.14  { ! alpha27( X, Y, Z, skol41( X, Y, Z ) ), alpha18( X, Y, Z ) }.
% 0.69/1.14  { ! alpha27( X, Y, Z, T ), ! ssList( U ), alpha34( X, Y, Z, T, U ) }.
% 0.69/1.14  { ssList( skol42( U, W, V0, V1 ) ), alpha27( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha34( X, Y, Z, T, skol42( X, Y, Z, T ) ), alpha27( X, Y, Z, T ) }.
% 0.69/1.14  { ! alpha34( X, Y, Z, T, U ), ! app( T, cons( Y, cons( Z, U ) ) ) = X, Y = 
% 0.69/1.14    Z }.
% 0.69/1.14  { app( T, cons( Y, cons( Z, U ) ) ) = X, alpha34( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! Y = Z, alpha34( X, Y, Z, T, U ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! neq( X, Y ), ! X = Y }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), X = Y, neq( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ssList( cons( Y, X ) ) }.
% 0.69/1.14  { ssList( nil ) }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ! cons( Y, X ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z ), ! ssItem( T ), ! cons( Z, X
% 0.69/1.14     ) = cons( T, Y ), Z = T }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z ), ! ssItem( T ), ! cons( Z, X
% 0.69/1.14     ) = cons( T, Y ), Y = X }.
% 0.69/1.14  { ! ssList( X ), nil = X, ssList( skol43( Y ) ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, ssItem( skol48( Y ) ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, cons( skol48( X ), skol43( X ) ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), ! nil = cons( Y, X ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, ssItem( hd( X ) ) }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), hd( cons( Y, X ) ) = Y }.
% 0.69/1.14  { ! ssList( X ), nil = X, ssList( tl( X ) ) }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), tl( cons( Y, X ) ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ssList( app( X, Y ) ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z ), cons( Z, app( Y, X ) ) = app
% 0.69/1.14    ( cons( Z, Y ), X ) }.
% 0.69/1.14  { ! ssList( X ), app( nil, X ) = X }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! leq( X, Y ), ! leq( Y, X ), X = Y }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! leq( X, Y ), ! leq( Y, Z )
% 0.69/1.14    , leq( X, Z ) }.
% 0.69/1.14  { ! ssItem( X ), leq( X, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! geq( X, Y ), leq( Y, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! leq( Y, X ), geq( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y ), ! lt( Y, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! lt( X, Y ), ! lt( Y, Z ), 
% 0.69/1.14    lt( X, Z ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! gt( X, Y ), lt( Y, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! lt( Y, X ), gt( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z ), ! memberP( app( Y, Z ), X )
% 0.69/1.14    , memberP( Y, X ), memberP( Z, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z ), ! memberP( Y, X ), memberP( 
% 0.69/1.14    app( Y, Z ), X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z ), ! memberP( Z, X ), memberP( 
% 0.69/1.14    app( Y, Z ), X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! memberP( cons( Y, Z ), X )
% 0.69/1.14    , X = Y, memberP( Z, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! X = Y, memberP( cons( Y, Z
% 0.69/1.14     ), X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! memberP( Z, X ), memberP( 
% 0.69/1.14    cons( Y, Z ), X ) }.
% 0.69/1.14  { ! ssItem( X ), ! memberP( nil, X ) }.
% 0.69/1.14  { ! singletonP( nil ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! frontsegP( X, Y ), ! 
% 0.69/1.14    frontsegP( Y, Z ), frontsegP( X, Z ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! frontsegP( X, Y ), ! frontsegP( Y, X ), X
% 0.69/1.14     = Y }.
% 0.69/1.14  { ! ssList( X ), frontsegP( X, X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! frontsegP( X, Y ), 
% 0.69/1.14    frontsegP( app( X, Z ), Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! ssList( T ), ! frontsegP( 
% 0.69/1.14    cons( X, Z ), cons( Y, T ) ), X = Y }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! ssList( T ), ! frontsegP( 
% 0.69/1.14    cons( X, Z ), cons( Y, T ) ), frontsegP( Z, T ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! ssList( T ), ! X = Y, ! 
% 0.69/1.14    frontsegP( Z, T ), frontsegP( cons( X, Z ), cons( Y, T ) ) }.
% 0.69/1.14  { ! ssList( X ), frontsegP( X, nil ) }.
% 0.69/1.14  { ! ssList( X ), ! frontsegP( nil, X ), nil = X }.
% 0.69/1.14  { ! ssList( X ), ! nil = X, frontsegP( nil, X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! rearsegP( X, Y ), ! 
% 0.69/1.14    rearsegP( Y, Z ), rearsegP( X, Z ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X, Y ), ! rearsegP( Y, X ), X =
% 0.69/1.14     Y }.
% 0.69/1.14  { ! ssList( X ), rearsegP( X, X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! rearsegP( X, Y ), rearsegP
% 0.69/1.14    ( app( Z, X ), Y ) }.
% 0.69/1.14  { ! ssList( X ), rearsegP( X, nil ) }.
% 0.69/1.14  { ! ssList( X ), ! rearsegP( nil, X ), nil = X }.
% 0.69/1.14  { ! ssList( X ), ! nil = X, rearsegP( nil, X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! segmentP( X, Y ), ! 
% 0.69/1.14    segmentP( Y, Z ), segmentP( X, Z ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! segmentP( X, Y ), ! segmentP( Y, X ), X =
% 0.69/1.14     Y }.
% 0.69/1.14  { ! ssList( X ), segmentP( X, X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! ssList( T ), ! segmentP( X
% 0.69/1.14    , Y ), segmentP( app( app( Z, X ), T ), Y ) }.
% 0.69/1.14  { ! ssList( X ), segmentP( X, nil ) }.
% 0.69/1.14  { ! ssList( X ), ! segmentP( nil, X ), nil = X }.
% 0.69/1.14  { ! ssList( X ), ! nil = X, segmentP( nil, X ) }.
% 0.69/1.14  { ! ssItem( X ), cyclefreeP( cons( X, nil ) ) }.
% 0.69/1.14  { cyclefreeP( nil ) }.
% 0.69/1.14  { ! ssItem( X ), totalorderP( cons( X, nil ) ) }.
% 0.69/1.14  { totalorderP( nil ) }.
% 0.69/1.14  { ! ssItem( X ), strictorderP( cons( X, nil ) ) }.
% 0.69/1.14  { strictorderP( nil ) }.
% 0.69/1.14  { ! ssItem( X ), totalorderedP( cons( X, nil ) ) }.
% 0.69/1.14  { totalorderedP( nil ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! totalorderedP( cons( X, Y ) ), nil = Y, 
% 0.69/1.14    alpha10( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! nil = Y, totalorderedP( cons( X, Y ) ) }
% 0.69/1.14    .
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! alpha10( X, Y ), totalorderedP( cons( X, 
% 0.69/1.14    Y ) ) }.
% 0.69/1.14  { ! alpha10( X, Y ), ! nil = Y }.
% 0.69/1.14  { ! alpha10( X, Y ), alpha19( X, Y ) }.
% 0.69/1.14  { nil = Y, ! alpha19( X, Y ), alpha10( X, Y ) }.
% 0.69/1.14  { ! alpha19( X, Y ), totalorderedP( Y ) }.
% 0.69/1.14  { ! alpha19( X, Y ), leq( X, hd( Y ) ) }.
% 0.69/1.14  { ! totalorderedP( Y ), ! leq( X, hd( Y ) ), alpha19( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), strictorderedP( cons( X, nil ) ) }.
% 0.69/1.14  { strictorderedP( nil ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! strictorderedP( cons( X, Y ) ), nil = Y, 
% 0.69/1.14    alpha11( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! nil = Y, strictorderedP( cons( X, Y ) ) }
% 0.69/1.14    .
% 0.69/1.14  { ! ssItem( X ), ! ssList( Y ), ! alpha11( X, Y ), strictorderedP( cons( X
% 0.69/1.14    , Y ) ) }.
% 0.69/1.14  { ! alpha11( X, Y ), ! nil = Y }.
% 0.69/1.14  { ! alpha11( X, Y ), alpha20( X, Y ) }.
% 0.69/1.14  { nil = Y, ! alpha20( X, Y ), alpha11( X, Y ) }.
% 0.69/1.14  { ! alpha20( X, Y ), strictorderedP( Y ) }.
% 0.69/1.14  { ! alpha20( X, Y ), lt( X, hd( Y ) ) }.
% 0.69/1.14  { ! strictorderedP( Y ), ! lt( X, hd( Y ) ), alpha20( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), duplicatefreeP( cons( X, nil ) ) }.
% 0.69/1.14  { duplicatefreeP( nil ) }.
% 0.69/1.14  { ! ssItem( X ), equalelemsP( cons( X, nil ) ) }.
% 0.69/1.14  { equalelemsP( nil ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, ssItem( skol44( Y ) ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, hd( X ) = skol44( X ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, ssList( skol45( Y ) ) }.
% 0.69/1.14  { ! ssList( X ), nil = X, tl( X ) = skol45( X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), nil = Y, nil = X, ! hd( Y ) = hd( X ), ! tl
% 0.69/1.14    ( Y ) = tl( X ), Y = X }.
% 0.69/1.14  { ! ssList( X ), nil = X, cons( hd( X ), tl( X ) ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Z, Y ) = app( X, Y )
% 0.69/1.14    , Z = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Y, Z ) = app( Y, X )
% 0.69/1.14    , Z = X }.
% 0.69/1.14  { ! ssList( X ), ! ssItem( Y ), cons( Y, X ) = app( cons( Y, nil ), X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), app( app( X, Y ), Z ) = app
% 0.69/1.14    ( X, app( Y, Z ) ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! nil = app( X, Y ), nil = Y }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! nil = app( X, Y ), nil = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), ! nil = Y, ! nil = X, nil = app( X, Y ) }.
% 0.69/1.14  { ! ssList( X ), app( X, nil ) = X }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), nil = X, hd( app( X, Y ) ) = hd( X ) }.
% 0.69/1.14  { ! ssList( X ), ! ssList( Y ), nil = X, tl( app( X, Y ) ) = app( tl( X ), 
% 0.69/1.14    Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! geq( X, Y ), ! geq( Y, X ), X = Y }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! geq( X, Y ), ! geq( Y, Z )
% 0.69/1.14    , geq( X, Z ) }.
% 0.69/1.14  { ! ssItem( X ), geq( X, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! lt( X, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! leq( X, Y ), ! lt( Y, Z )
% 0.69/1.14    , lt( X, Z ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! leq( X, Y ), X = Y, lt( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y ), ! X = Y }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y ), leq( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), X = Y, ! leq( X, Y ), lt( X, Y ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! gt( X, Y ), ! gt( Y, X ) }.
% 0.69/1.14  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! gt( X, Y ), ! gt( Y, Z ), 
% 0.69/1.14    gt( X, Z ) }.
% 0.69/1.14  { ssList( skol46 ) }.
% 0.69/1.14  { ssList( skol49 ) }.
% 0.69/1.14  { ssList( skol50 ) }.
% 0.69/1.14  { ssList( skol51 ) }.
% 0.69/1.14  { skol49 = skol51 }.
% 0.69/1.14  { skol46 = skol50 }.
% 0.69/1.14  { neq( skol49, nil ) }.
% 0.69/1.14  { ! ssList( X ), ! neq( X, nil ), ! segmentP( skol49, X ), ! segmentP( 
% 0.69/1.14    skol46, X ) }.
% 0.69/1.14  { nil = skol50, ! nil = skol51 }.
% 0.69/1.14  { ! neq( skol51, nil ), neq( skol50, nil ) }.
% 0.69/1.14  { ! neq( skol51, nil ), ! ssList( X ), skol51 = X, ! ssList( Y ), ! ssList
% 0.69/1.14    ( Z ), ! tl( skol50 ) = Y, ! app( Y, Z ) = X, ! ssItem( T ), ! cons( T, 
% 0.69/1.14    nil ) = Z, ! hd( skol50 ) = T, ! neq( nil, skol50 ), ! neq( nil, skol50 )
% 0.69/1.14     }.
% 0.69/1.14  
% 0.69/1.14  *** allocated 15000 integers for clauses
% 0.69/1.14  percentage equality = 0.133178, percentage horn = 0.762238
% 0.69/1.14  This is a problem with some equality
% 0.69/1.14  
% 0.69/1.14  
% 0.69/1.14  
% 0.69/1.14  Options Used:
% 0.69/1.14  
% 0.69/1.14  useres =            1
% 0.69/1.14  useparamod =        1
% 0.69/1.14  useeqrefl =         1
% 0.69/1.14  useeqfact =         1
% 0.69/1.14  usefactor =         1
% 0.69/1.14  usesimpsplitting =  0
% 0.69/1.14  usesimpdemod =      5
% 0.69/1.14  usesimpres =        3
% 0.69/1.14  
% 0.69/1.14  resimpinuse      =  1000
% 0.69/1.14  resimpclauses =     20000
% 0.69/1.14  substype =          eqrewr
% 0.69/1.14  backwardsubs =      1
% 0.69/1.14  selectoldest =      5
% 0.69/1.14  
% 0.69/1.14  litorderings [0] =  split
% 0.69/1.14  litorderings [1] =  extend the termordering, first sorting on arguments
% 0.69/1.14  
% 0.69/1.14  termordering =      kbo
% 0.69/1.14  
% 0.69/1.14  litapriori =        0
% 0.69/1.14  termapriori =       1
% 0.69/1.14  litaposteriori =    0
% 0.69/1.14  termaposteriori =   0
% 0.69/1.14  demodaposteriori =  0
% 0.69/1.14  ordereqreflfact =   0
% 0.69/1.14  
% 0.69/1.14  litselect =         negord
% 0.69/1.14  
% 0.69/1.14  maxweight =         15
% 0.69/1.14  maxdepth =          30000
% 0.69/1.14  maxlength =         115
% 0.69/1.14  maxnrvars =         195
% 0.69/1.14  excuselevel =       1
% 0.69/1.14  increasemaxweight = 1
% 0.69/1.14  
% 0.69/1.14  maxselected =       10000000
% 0.69/1.14  maxnrclauses =      10000000
% 0.69/1.14  
% 0.69/1.14  showgenerated =    0
% 0.69/1.14  showkept =         0
% 0.69/1.14  showselected =     0
% 0.69/1.14  showdeleted =      0
% 0.69/1.14  showresimp =       1
% 0.69/1.14  showstatus =       2000
% 0.69/1.14  
% 0.69/1.14  prologoutput =     0
% 0.69/1.14  nrgoals =          5000000
% 0.69/1.14  totalproof =       1
% 0.69/1.14  
% 0.69/1.14  Symbols occurring in the translation:
% 0.69/1.14  
% 0.69/1.14  {}  [0, 0]      (w:1, o:2, a:1, s:1, b:0), 
% 0.69/1.14  .  [1, 2]      (w:1, o:51, a:1, s:1, b:0), 
% 0.69/1.14  !  [4, 1]      (w:0, o:22, a:1, s:1, b:0), 
% 0.69/1.14  =  [13, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.69/1.14  ==>  [14, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.69/1.14  ssItem  [36, 1]      (w:1, o:27, a:1, s:1, b:0), 
% 0.69/1.14  neq  [38, 2]      (w:1, o:78, a:1, s:1, b:0), 
% 0.69/1.14  ssList  [39, 1]      (w:1, o:28, a:1, s:1, b:0), 
% 0.69/1.14  memberP  [40, 2]      (w:1, o:77, a:1, s:1, b:0), 
% 0.69/1.14  cons  [43, 2]      (w:1, o:79, a:1, s:1, b:0), 
% 0.69/1.14  app  [44, 2]      (w:1, o:80, a:1, s:1, b:0), 
% 1.31/1.77  singletonP  [45, 1]      (w:1, o:29, a:1, s:1, b:0), 
% 1.31/1.77  nil  [46, 0]      (w:1, o:10, a:1, s:1, b:0), 
% 1.31/1.77  frontsegP  [47, 2]      (w:1, o:81, a:1, s:1, b:0), 
% 1.31/1.77  rearsegP  [48, 2]      (w:1, o:82, a:1, s:1, b:0), 
% 1.31/1.77  segmentP  [49, 2]      (w:1, o:83, a:1, s:1, b:0), 
% 1.31/1.77  cyclefreeP  [50, 1]      (w:1, o:30, a:1, s:1, b:0), 
% 1.31/1.77  leq  [53, 2]      (w:1, o:75, a:1, s:1, b:0), 
% 1.31/1.77  totalorderP  [54, 1]      (w:1, o:45, a:1, s:1, b:0), 
% 1.31/1.77  strictorderP  [55, 1]      (w:1, o:31, a:1, s:1, b:0), 
% 1.31/1.77  lt  [56, 2]      (w:1, o:76, a:1, s:1, b:0), 
% 1.31/1.77  totalorderedP  [57, 1]      (w:1, o:46, a:1, s:1, b:0), 
% 1.31/1.77  strictorderedP  [58, 1]      (w:1, o:32, a:1, s:1, b:0), 
% 1.31/1.77  duplicatefreeP  [59, 1]      (w:1, o:47, a:1, s:1, b:0), 
% 1.31/1.77  equalelemsP  [60, 1]      (w:1, o:48, a:1, s:1, b:0), 
% 1.31/1.77  hd  [61, 1]      (w:1, o:49, a:1, s:1, b:0), 
% 1.31/1.77  tl  [62, 1]      (w:1, o:50, a:1, s:1, b:0), 
% 1.31/1.77  geq  [63, 2]      (w:1, o:84, a:1, s:1, b:0), 
% 1.31/1.77  gt  [64, 2]      (w:1, o:85, a:1, s:1, b:0), 
% 1.31/1.77  alpha1  [68, 3]      (w:1, o:111, a:1, s:1, b:1), 
% 1.31/1.77  alpha2  [69, 3]      (w:1, o:116, a:1, s:1, b:1), 
% 1.31/1.77  alpha3  [70, 2]      (w:1, o:87, a:1, s:1, b:1), 
% 1.31/1.77  alpha4  [71, 2]      (w:1, o:88, a:1, s:1, b:1), 
% 1.31/1.77  alpha5  [72, 2]      (w:1, o:89, a:1, s:1, b:1), 
% 1.31/1.77  alpha6  [73, 2]      (w:1, o:90, a:1, s:1, b:1), 
% 1.31/1.77  alpha7  [74, 2]      (w:1, o:91, a:1, s:1, b:1), 
% 1.31/1.77  alpha8  [75, 2]      (w:1, o:92, a:1, s:1, b:1), 
% 1.31/1.77  alpha9  [76, 2]      (w:1, o:93, a:1, s:1, b:1), 
% 1.31/1.77  alpha10  [77, 2]      (w:1, o:94, a:1, s:1, b:1), 
% 1.31/1.77  alpha11  [78, 2]      (w:1, o:95, a:1, s:1, b:1), 
% 1.31/1.77  alpha12  [79, 2]      (w:1, o:96, a:1, s:1, b:1), 
% 1.31/1.77  alpha13  [80, 2]      (w:1, o:97, a:1, s:1, b:1), 
% 1.31/1.77  alpha14  [81, 2]      (w:1, o:98, a:1, s:1, b:1), 
% 1.31/1.77  alpha15  [82, 3]      (w:1, o:112, a:1, s:1, b:1), 
% 1.31/1.77  alpha16  [83, 3]      (w:1, o:113, a:1, s:1, b:1), 
% 1.31/1.77  alpha17  [84, 3]      (w:1, o:114, a:1, s:1, b:1), 
% 1.31/1.77  alpha18  [85, 3]      (w:1, o:115, a:1, s:1, b:1), 
% 1.31/1.77  alpha19  [86, 2]      (w:1, o:99, a:1, s:1, b:1), 
% 1.31/1.77  alpha20  [87, 2]      (w:1, o:86, a:1, s:1, b:1), 
% 1.31/1.77  alpha21  [88, 3]      (w:1, o:117, a:1, s:1, b:1), 
% 1.31/1.77  alpha22  [89, 3]      (w:1, o:118, a:1, s:1, b:1), 
% 1.31/1.77  alpha23  [90, 3]      (w:1, o:119, a:1, s:1, b:1), 
% 1.31/1.77  alpha24  [91, 4]      (w:1, o:129, a:1, s:1, b:1), 
% 1.31/1.77  alpha25  [92, 4]      (w:1, o:130, a:1, s:1, b:1), 
% 1.31/1.77  alpha26  [93, 4]      (w:1, o:131, a:1, s:1, b:1), 
% 1.31/1.77  alpha27  [94, 4]      (w:1, o:132, a:1, s:1, b:1), 
% 1.31/1.77  alpha28  [95, 4]      (w:1, o:133, a:1, s:1, b:1), 
% 1.31/1.77  alpha29  [96, 4]      (w:1, o:134, a:1, s:1, b:1), 
% 1.31/1.77  alpha30  [97, 4]      (w:1, o:135, a:1, s:1, b:1), 
% 1.31/1.77  alpha31  [98, 5]      (w:1, o:143, a:1, s:1, b:1), 
% 1.31/1.77  alpha32  [99, 5]      (w:1, o:144, a:1, s:1, b:1), 
% 1.31/1.77  alpha33  [100, 5]      (w:1, o:145, a:1, s:1, b:1), 
% 1.31/1.77  alpha34  [101, 5]      (w:1, o:146, a:1, s:1, b:1), 
% 1.31/1.77  alpha35  [102, 5]      (w:1, o:147, a:1, s:1, b:1), 
% 1.31/1.77  alpha36  [103, 5]      (w:1, o:148, a:1, s:1, b:1), 
% 1.31/1.77  alpha37  [104, 5]      (w:1, o:149, a:1, s:1, b:1), 
% 1.31/1.77  alpha38  [105, 6]      (w:1, o:156, a:1, s:1, b:1), 
% 1.31/1.77  alpha39  [106, 6]      (w:1, o:157, a:1, s:1, b:1), 
% 1.31/1.77  alpha40  [107, 6]      (w:1, o:158, a:1, s:1, b:1), 
% 1.31/1.77  alpha41  [108, 6]      (w:1, o:159, a:1, s:1, b:1), 
% 1.31/1.77  alpha42  [109, 6]      (w:1, o:160, a:1, s:1, b:1), 
% 1.31/1.77  alpha43  [110, 6]      (w:1, o:161, a:1, s:1, b:1), 
% 1.31/1.77  skol1  [111, 0]      (w:1, o:16, a:1, s:1, b:1), 
% 1.31/1.77  skol2  [112, 2]      (w:1, o:102, a:1, s:1, b:1), 
% 1.31/1.77  skol3  [113, 3]      (w:1, o:122, a:1, s:1, b:1), 
% 1.31/1.77  skol4  [114, 1]      (w:1, o:35, a:1, s:1, b:1), 
% 1.31/1.77  skol5  [115, 2]      (w:1, o:104, a:1, s:1, b:1), 
% 1.31/1.77  skol6  [116, 2]      (w:1, o:105, a:1, s:1, b:1), 
% 1.31/1.77  skol7  [117, 2]      (w:1, o:106, a:1, s:1, b:1), 
% 1.31/1.77  skol8  [118, 3]      (w:1, o:123, a:1, s:1, b:1), 
% 1.31/1.77  skol9  [119, 1]      (w:1, o:36, a:1, s:1, b:1), 
% 1.31/1.77  skol10  [120, 2]      (w:1, o:100, a:1, s:1, b:1), 
% 1.31/1.77  skol11  [121, 3]      (w:1, o:124, a:1, s:1, b:1), 
% 1.31/1.77  skol12  [122, 4]      (w:1, o:136, a:1, s:1, b:1), 
% 1.31/1.77  skol13  [123, 5]      (w:1, o:150, a:1, s:1, b:1), 
% 1.31/1.77  skol14  [124, 1]      (w:1, o:37, a:1, s:1, b:1), 
% 1.31/1.77  skol15  [125, 2]      (w:1, o:101, a:1, s:1, b:1), 
% 1.31/1.77  skol16  [126, 3]      (w:1, o:125, a:1, s:1, b:1), 
% 1.31/1.77  skol17  [127, 4]      (w:1, o:137, a:1, s:1, b:1), 
% 1.31/1.77  skol18  [128, 5]      (w:1, o:151, a:1, s:1, b:1), 
% 1.31/1.77  skol19  [129, 1]      (w:1, o:38, a:1, s:1, b:1), 
% 10.09/10.48  skol20  [130, 2]      (w:1, o:107, a:1, s:1, b:1), 
% 10.09/10.48  skol21  [131, 3]      (w:1, o:120, a:1, s:1, b:1), 
% 10.09/10.48  skol22  [132, 4]      (w:1, o:138, a:1, s:1, b:1), 
% 10.09/10.48  skol23  [133, 5]      (w:1, o:152, a:1, s:1, b:1), 
% 10.09/10.48  skol24  [134, 1]      (w:1, o:39, a:1, s:1, b:1), 
% 10.09/10.48  skol25  [135, 2]      (w:1, o:108, a:1, s:1, b:1), 
% 10.09/10.48  skol26  [136, 3]      (w:1, o:121, a:1, s:1, b:1), 
% 10.09/10.48  skol27  [137, 4]      (w:1, o:139, a:1, s:1, b:1), 
% 10.09/10.48  skol28  [138, 5]      (w:1, o:153, a:1, s:1, b:1), 
% 10.09/10.48  skol29  [139, 1]      (w:1, o:40, a:1, s:1, b:1), 
% 10.09/10.48  skol30  [140, 2]      (w:1, o:109, a:1, s:1, b:1), 
% 10.09/10.48  skol31  [141, 3]      (w:1, o:126, a:1, s:1, b:1), 
% 10.09/10.48  skol32  [142, 4]      (w:1, o:140, a:1, s:1, b:1), 
% 10.09/10.48  skol33  [143, 5]      (w:1, o:154, a:1, s:1, b:1), 
% 10.09/10.48  skol34  [144, 1]      (w:1, o:33, a:1, s:1, b:1), 
% 10.09/10.48  skol35  [145, 2]      (w:1, o:110, a:1, s:1, b:1), 
% 10.09/10.48  skol36  [146, 3]      (w:1, o:127, a:1, s:1, b:1), 
% 10.09/10.48  skol37  [147, 4]      (w:1, o:141, a:1, s:1, b:1), 
% 10.09/10.48  skol38  [148, 5]      (w:1, o:155, a:1, s:1, b:1), 
% 10.09/10.48  skol39  [149, 1]      (w:1, o:34, a:1, s:1, b:1), 
% 10.09/10.48  skol40  [150, 2]      (w:1, o:103, a:1, s:1, b:1), 
% 10.09/10.48  skol41  [151, 3]      (w:1, o:128, a:1, s:1, b:1), 
% 10.09/10.48  skol42  [152, 4]      (w:1, o:142, a:1, s:1, b:1), 
% 10.09/10.48  skol43  [153, 1]      (w:1, o:41, a:1, s:1, b:1), 
% 10.09/10.48  skol44  [154, 1]      (w:1, o:42, a:1, s:1, b:1), 
% 10.09/10.48  skol45  [155, 1]      (w:1, o:43, a:1, s:1, b:1), 
% 10.09/10.48  skol46  [156, 0]      (w:1, o:17, a:1, s:1, b:1), 
% 10.09/10.48  skol47  [157, 0]      (w:1, o:18, a:1, s:1, b:1), 
% 10.09/10.48  skol48  [158, 1]      (w:1, o:44, a:1, s:1, b:1), 
% 10.09/10.48  skol49  [159, 0]      (w:1, o:19, a:1, s:1, b:1), 
% 10.09/10.48  skol50  [160, 0]      (w:1, o:20, a:1, s:1, b:1), 
% 10.09/10.48  skol51  [161, 0]      (w:1, o:21, a:1, s:1, b:1).
% 10.09/10.48  
% 10.09/10.48  
% 10.09/10.48  Starting Search:
% 10.09/10.48  
% 10.09/10.48  *** allocated 22500 integers for clauses
% 10.09/10.48  *** allocated 33750 integers for clauses
% 10.09/10.48  *** allocated 50625 integers for clauses
% 10.09/10.48  *** allocated 22500 integers for termspace/termends
% 10.09/10.48  *** allocated 75937 integers for clauses
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  *** allocated 33750 integers for termspace/termends
% 10.09/10.48  *** allocated 113905 integers for clauses
% 10.09/10.48  *** allocated 50625 integers for termspace/termends
% 10.09/10.48  
% 10.09/10.48  Intermediate Status:
% 10.09/10.48  Generated:    3759
% 10.09/10.48  Kept:         2003
% 10.09/10.48  Inuse:        209
% 10.09/10.48  Deleted:      7
% 10.09/10.48  Deletedinuse: 2
% 10.09/10.48  
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  *** allocated 170857 integers for clauses
% 10.09/10.48  *** allocated 75937 integers for termspace/termends
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  *** allocated 256285 integers for clauses
% 10.09/10.48  
% 10.09/10.48  Intermediate Status:
% 10.09/10.48  Generated:    6781
% 10.09/10.48  Kept:         4011
% 10.09/10.48  Inuse:        378
% 10.09/10.48  Deleted:      10
% 10.09/10.48  Deletedinuse: 5
% 10.09/10.48  
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  *** allocated 113905 integers for termspace/termends
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  *** allocated 384427 integers for clauses
% 10.09/10.48  
% 10.09/10.48  Intermediate Status:
% 10.09/10.48  Generated:    10316
% 10.09/10.48  Kept:         6040
% 10.09/10.48  Inuse:        491
% 10.09/10.48  Deleted:      20
% 10.09/10.48  Deletedinuse: 15
% 10.09/10.48  
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  *** allocated 170857 integers for termspace/termends
% 10.09/10.48  *** allocated 576640 integers for clauses
% 10.09/10.48  
% 10.09/10.48  Intermediate Status:
% 10.09/10.48  Generated:    13446
% 10.09/10.48  Kept:         8097
% 10.09/10.48  Inuse:        595
% 10.09/10.48  Deleted:      27
% 10.09/10.48  Deletedinuse: 20
% 10.09/10.48  
% 10.09/10.48  Resimplifying inuse:
% 10.09/10.48  Done
% 10.09/10.48  
% 10.09/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  
% 10.11/10.48  Intermediate Status:
% 10.11/10.48  Generated:    17261
% 10.11/10.48  Kept:         10588
% 10.11/10.48  Inuse:        672
% 10.11/10.48  Deleted:      36
% 10.11/10.48  Deletedinuse: 27
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  *** allocated 256285 integers for termspace/termends
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  *** allocated 864960 integers for clauses
% 10.11/10.48  
% 10.11/10.48  Intermediate Status:
% 10.11/10.48  Generated:    21707
% 10.11/10.48  Kept:         12648
% 10.11/10.48  Inuse:        742
% 10.11/10.48  Deleted:      36
% 10.11/10.48  Deletedinuse: 27
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  
% 10.11/10.48  Intermediate Status:
% 10.11/10.48  Generated:    30331
% 10.11/10.48  Kept:         14754
% 10.11/10.48  Inuse:        781
% 10.11/10.48  Deleted:      51
% 10.11/10.48  Deletedinuse: 41
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  *** allocated 384427 integers for termspace/termends
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  
% 10.11/10.48  Intermediate Status:
% 10.11/10.48  Generated:    37248
% 10.11/10.48  Kept:         16778
% 10.11/10.48  Inuse:        844
% 10.11/10.48  Deleted:      75
% 10.11/10.48  Deletedinuse: 63
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 10.11/10.48  Done
% 10.11/10.48  
% 10.11/10.48  *** allocated 1297440 integers for clauses
% 10.11/10.48  
% 10.11/10.48  Intermediate Status:
% 10.11/10.48  Generated:    45729
% 10.11/10.48  Kept:         18923
% 10.11/10.48  Inuse:        896
% 10.11/10.48  Deleted:      97
% 10.11/10.48  Deletedinuse: 67
% 10.11/10.48  
% 10.11/10.48  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying clauses:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    57356
% 29.28/29.70  Kept:         21255
% 29.28/29.70  Inuse:        931
% 29.28/29.70  Deleted:      1869
% 29.28/29.70  Deletedinuse: 68
% 29.28/29.70  
% 29.28/29.70  *** allocated 576640 integers for termspace/termends
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    65583
% 29.28/29.70  Kept:         23263
% 29.28/29.70  Inuse:        962
% 29.28/29.70  Deleted:      1873
% 29.28/29.70  Deletedinuse: 68
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    72896
% 29.28/29.70  Kept:         25378
% 29.28/29.70  Inuse:        1012
% 29.28/29.70  Deleted:      1873
% 29.28/29.70  Deletedinuse: 68
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    82950
% 29.28/29.70  Kept:         27823
% 29.28/29.70  Inuse:        1047
% 29.28/29.70  Deleted:      1875
% 29.28/29.70  Deletedinuse: 70
% 29.28/29.70  
% 29.28/29.70  *** allocated 1946160 integers for clauses
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    91932
% 29.28/29.70  Kept:         29843
% 29.28/29.70  Inuse:        1072
% 29.28/29.70  Deleted:      1875
% 29.28/29.70  Deletedinuse: 70
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  *** allocated 864960 integers for termspace/termends
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    102385
% 29.28/29.70  Kept:         31922
% 29.28/29.70  Inuse:        1102
% 29.28/29.70  Deleted:      1883
% 29.28/29.70  Deletedinuse: 73
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    111340
% 29.28/29.70  Kept:         34009
% 29.28/29.70  Inuse:        1213
% 29.28/29.70  Deleted:      1899
% 29.28/29.70  Deletedinuse: 73
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    124751
% 29.28/29.70  Kept:         36134
% 29.28/29.70  Inuse:        1251
% 29.28/29.70  Deleted:      1911
% 29.28/29.70  Deletedinuse: 73
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    134466
% 29.28/29.70  Kept:         38217
% 29.28/29.70  Inuse:        1275
% 29.28/29.70  Deleted:      1911
% 29.28/29.70  Deletedinuse: 73
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    142059
% 29.28/29.70  Kept:         40270
% 29.28/29.70  Inuse:        1304
% 29.28/29.70  Deleted:      1911
% 29.28/29.70  Deletedinuse: 73
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying clauses:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    153454
% 29.28/29.70  Kept:         42279
% 29.28/29.70  Inuse:        1374
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  *** allocated 2919240 integers for clauses
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    170065
% 29.28/29.70  Kept:         44293
% 29.28/29.70  Inuse:        1426
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    177754
% 29.28/29.70  Kept:         46471
% 29.28/29.70  Inuse:        1470
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    184771
% 29.28/29.70  Kept:         48501
% 29.28/29.70  Inuse:        1484
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    193430
% 29.28/29.70  Kept:         50526
% 29.28/29.70  Inuse:        1502
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  *** allocated 1297440 integers for termspace/termends
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    205036
% 29.28/29.70  Kept:         53306
% 29.28/29.70  Inuse:        1539
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    213662
% 29.28/29.70  Kept:         56153
% 29.28/29.70  Inuse:        1559
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    221048
% 29.28/29.70  Kept:         58174
% 29.28/29.70  Inuse:        1577
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    231456
% 29.28/29.70  Kept:         60300
% 29.28/29.70  Inuse:        1602
% 29.28/29.70  Deleted:      3566
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying clauses:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    239836
% 29.28/29.70  Kept:         62356
% 29.28/29.70  Inuse:        1624
% 29.28/29.70  Deleted:      4715
% 29.28/29.70  Deletedinuse: 76
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  *** allocated 4378860 integers for clauses
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    248933
% 29.28/29.70  Kept:         64417
% 29.28/29.70  Inuse:        1654
% 29.28/29.70  Deleted:      4722
% 29.28/29.70  Deletedinuse: 78
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  Resimplifying inuse:
% 29.28/29.70  Done
% 29.28/29.70  
% 29.28/29.70  
% 29.28/29.70  Intermediate Status:
% 29.28/29.70  Generated:    259863
% 29.28/29.70  Kept:         66437
% 29.28/29.70  Inuse:        1683
% 29.28/29.70  Deleted:      4722
% 55.26/55.65  Deletedinuse: 78
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    269394
% 55.26/55.65  Kept:         68437
% 55.26/55.65  Inuse:        1701
% 55.26/55.65  Deleted:      4722
% 55.26/55.65  Deletedinuse: 78
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    278611
% 55.26/55.65  Kept:         70491
% 55.26/55.65  Inuse:        1717
% 55.26/55.65  Deleted:      4722
% 55.26/55.65  Deletedinuse: 78
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    288615
% 55.26/55.65  Kept:         72494
% 55.26/55.65  Inuse:        1734
% 55.26/55.65  Deleted:      4723
% 55.26/55.65  Deletedinuse: 78
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    293153
% 55.26/55.65  Kept:         74500
% 55.26/55.65  Inuse:        1767
% 55.26/55.65  Deleted:      4724
% 55.26/55.65  Deletedinuse: 78
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    302936
% 55.26/55.65  Kept:         76505
% 55.26/55.65  Inuse:        1863
% 55.26/55.65  Deleted:      4740
% 55.26/55.65  Deletedinuse: 92
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    322537
% 55.26/55.65  Kept:         78510
% 55.26/55.65  Inuse:        1922
% 55.26/55.65  Deleted:      4741
% 55.26/55.65  Deletedinuse: 92
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    334519
% 55.26/55.65  Kept:         80576
% 55.26/55.65  Inuse:        1975
% 55.26/55.65  Deleted:      4748
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying clauses:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    346836
% 55.26/55.65  Kept:         82599
% 55.26/55.65  Inuse:        2009
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  *** allocated 1946160 integers for termspace/termends
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    356372
% 55.26/55.65  Kept:         84605
% 55.26/55.65  Inuse:        2038
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    365424
% 55.26/55.65  Kept:         86611
% 55.26/55.65  Inuse:        2079
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    376325
% 55.26/55.65  Kept:         88629
% 55.26/55.65  Inuse:        2123
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    381739
% 55.26/55.65  Kept:         90726
% 55.26/55.65  Inuse:        2140
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    387797
% 55.26/55.65  Kept:         92764
% 55.26/55.65  Inuse:        2178
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    393090
% 55.26/55.65  Kept:         94787
% 55.26/55.65  Inuse:        2206
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    402110
% 55.26/55.65  Kept:         96797
% 55.26/55.65  Inuse:        2252
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  *** allocated 6568290 integers for clauses
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    408582
% 55.26/55.65  Kept:         98797
% 55.26/55.65  Inuse:        2299
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    429460
% 55.26/55.65  Kept:         100826
% 55.26/55.65  Inuse:        2366
% 55.26/55.65  Deleted:      6267
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying clauses:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    436687
% 55.26/55.65  Kept:         102894
% 55.26/55.65  Inuse:        2392
% 55.26/55.65  Deleted:      7108
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    446522
% 55.26/55.65  Kept:         104914
% 55.26/55.65  Inuse:        2432
% 55.26/55.65  Deleted:      7108
% 55.26/55.65  Deletedinuse: 98
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    453717
% 55.26/55.65  Kept:         107040
% 55.26/55.65  Inuse:        2473
% 55.26/55.65  Deleted:      7109
% 55.26/55.65  Deletedinuse: 99
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    470197
% 55.26/55.65  Kept:         109148
% 55.26/55.65  Inuse:        2497
% 55.26/55.65  Deleted:      7126
% 55.26/55.65  Deletedinuse: 100
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    488791
% 55.26/55.65  Kept:         111213
% 55.26/55.65  Inuse:        2524
% 55.26/55.65  Deleted:      7127
% 55.26/55.65  Deletedinuse: 101
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  Resimplifying inuse:
% 55.26/55.65  Done
% 55.26/55.65  
% 55.26/55.65  
% 55.26/55.65  Intermediate Status:
% 55.26/55.65  Generated:    506003
% 55.26/55.65  Kept:         113225
% 55.26/55.65  Inuse:        2556
% 55.26/55.65  Deleted:      7127
% 55.26/55.65  Deletedinuse: 101
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    513742
% 94.87/95.34  Kept:         115457
% 94.87/95.34  Inuse:        2566
% 94.87/95.34  Deleted:      7127
% 94.87/95.34  Deletedinuse: 101
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    534488
% 94.87/95.34  Kept:         117566
% 94.87/95.34  Inuse:        2716
% 94.87/95.34  Deleted:      7128
% 94.87/95.34  Deletedinuse: 102
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    579401
% 94.87/95.34  Kept:         119569
% 94.87/95.34  Inuse:        2907
% 94.87/95.34  Deleted:      7129
% 94.87/95.34  Deletedinuse: 103
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    598600
% 94.87/95.34  Kept:         121601
% 94.87/95.34  Inuse:        2987
% 94.87/95.34  Deleted:      7129
% 94.87/95.34  Deletedinuse: 103
% 94.87/95.34  
% 94.87/95.34  Resimplifying clauses:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    614152
% 94.87/95.34  Kept:         123628
% 94.87/95.34  Inuse:        3062
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    627371
% 94.87/95.34  Kept:         125637
% 94.87/95.34  Inuse:        3103
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    639053
% 94.87/95.34  Kept:         127675
% 94.87/95.34  Inuse:        3139
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    646040
% 94.87/95.34  Kept:         129820
% 94.87/95.34  Inuse:        3171
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  *** allocated 2919240 integers for termspace/termends
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    654493
% 94.87/95.34  Kept:         131841
% 94.87/95.34  Inuse:        3195
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    659576
% 94.87/95.34  Kept:         133889
% 94.87/95.34  Inuse:        3204
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    669232
% 94.87/95.34  Kept:         136115
% 94.87/95.34  Inuse:        3213
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    679128
% 94.87/95.34  Kept:         138378
% 94.87/95.34  Inuse:        3222
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    684703
% 94.87/95.34  Kept:         140405
% 94.87/95.34  Inuse:        3233
% 94.87/95.34  Deleted:      8381
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying clauses:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    691563
% 94.87/95.34  Kept:         142426
% 94.87/95.34  Inuse:        3249
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    695862
% 94.87/95.34  Kept:         144453
% 94.87/95.34  Inuse:        3259
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    700157
% 94.87/95.34  Kept:         146515
% 94.87/95.34  Inuse:        3270
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    705606
% 94.87/95.34  Kept:         148527
% 94.87/95.34  Inuse:        3294
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    714656
% 94.87/95.34  Kept:         151060
% 94.87/95.34  Inuse:        3311
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    722208
% 94.87/95.34  Kept:         153119
% 94.87/95.34  Inuse:        3322
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  *** allocated 9852435 integers for clauses
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    727416
% 94.87/95.34  Kept:         155153
% 94.87/95.34  Inuse:        3334
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    732940
% 94.87/95.34  Kept:         157218
% 94.87/95.34  Inuse:        3346
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    737598
% 94.87/95.34  Kept:         159462
% 94.87/95.34  Inuse:        3357
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  Resimplifying inuse:
% 94.87/95.34  Done
% 94.87/95.34  
% 94.87/95.34  
% 94.87/95.34  Intermediate Status:
% 94.87/95.34  Generated:    749817
% 94.87/95.34  Kept:         162601
% 94.87/95.34  Inuse:        3406
% 94.87/95.34  Deleted:      8956
% 94.87/95.34  Deletedinuse: 104
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying clauses:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    759264
% 128.96/129.37  Kept:         164719
% 128.96/129.37  Inuse:        3434
% 128.96/129.37  Deleted:      9072
% 128.96/129.37  Deletedinuse: 104
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    769908
% 128.96/129.37  Kept:         166745
% 128.96/129.37  Inuse:        3489
% 128.96/129.37  Deleted:      9072
% 128.96/129.37  Deletedinuse: 104
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    785047
% 128.96/129.37  Kept:         168850
% 128.96/129.37  Inuse:        3563
% 128.96/129.37  Deleted:      9072
% 128.96/129.37  Deletedinuse: 104
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    794322
% 128.96/129.37  Kept:         170879
% 128.96/129.37  Inuse:        3616
% 128.96/129.37  Deleted:      9075
% 128.96/129.37  Deletedinuse: 107
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    797155
% 128.96/129.37  Kept:         173051
% 128.96/129.37  Inuse:        3633
% 128.96/129.37  Deleted:      9078
% 128.96/129.37  Deletedinuse: 110
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    803053
% 128.96/129.37  Kept:         175149
% 128.96/129.37  Inuse:        3675
% 128.96/129.37  Deleted:      9082
% 128.96/129.37  Deletedinuse: 114
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    809725
% 128.96/129.37  Kept:         177263
% 128.96/129.37  Inuse:        3717
% 128.96/129.37  Deleted:      9089
% 128.96/129.37  Deletedinuse: 121
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    822373
% 128.96/129.37  Kept:         179331
% 128.96/129.37  Inuse:        3781
% 128.96/129.37  Deleted:      9090
% 128.96/129.37  Deletedinuse: 122
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    839925
% 128.96/129.37  Kept:         181361
% 128.96/129.37  Inuse:        3849
% 128.96/129.37  Deleted:      9090
% 128.96/129.37  Deletedinuse: 122
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying clauses:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    850907
% 128.96/129.37  Kept:         183509
% 128.96/129.37  Inuse:        3896
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    854065
% 128.96/129.37  Kept:         185567
% 128.96/129.37  Inuse:        3946
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    862203
% 128.96/129.37  Kept:         187580
% 128.96/129.37  Inuse:        3976
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    878144
% 128.96/129.37  Kept:         189640
% 128.96/129.37  Inuse:        4106
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    891580
% 128.96/129.37  Kept:         191713
% 128.96/129.37  Inuse:        4152
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    895816
% 128.96/129.37  Kept:         193869
% 128.96/129.37  Inuse:        4167
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    916008
% 128.96/129.37  Kept:         195912
% 128.96/129.37  Inuse:        4293
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    921985
% 128.96/129.37  Kept:         197928
% 128.96/129.37  Inuse:        4311
% 128.96/129.37  Deleted:      9743
% 128.96/129.37  Deletedinuse: 177
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    925952
% 128.96/129.37  Kept:         199933
% 128.96/129.37  Inuse:        4326
% 128.96/129.37  Deleted:      9745
% 128.96/129.37  Deletedinuse: 179
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    932423
% 128.96/129.37  Kept:         202194
% 128.96/129.37  Inuse:        4363
% 128.96/129.37  Deleted:      9748
% 128.96/129.37  Deletedinuse: 182
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying clauses:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    942357
% 128.96/129.37  Kept:         204208
% 128.96/129.37  Inuse:        4407
% 128.96/129.37  Deleted:      18142
% 128.96/129.37  Deletedinuse: 187
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  *** allocated 4378860 integers for termspace/termends
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    948676
% 128.96/129.37  Kept:         206398
% 128.96/129.37  Inuse:        4446
% 128.96/129.37  Deleted:      18142
% 128.96/129.37  Deletedinuse: 187
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    961686
% 128.96/129.37  Kept:         208417
% 128.96/129.37  Inuse:        4556
% 128.96/129.37  Deleted:      18142
% 128.96/129.37  Deletedinuse: 187
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  Resimplifying inuse:
% 128.96/129.37  Done
% 128.96/129.37  
% 128.96/129.37  
% 128.96/129.37  Intermediate Status:
% 128.96/129.37  Generated:    983280
% 128.96/129.37  Kept:         210454
% 128.96/129.37  Inuse:        4695
% 128.96/129.37  Deleted:      18142
% 182.65/183.13  Deletedinuse: 187
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  
% 182.65/183.13  Intermediate Status:
% 182.65/183.13  Generated:    992746
% 182.65/183.13  Kept:         212528
% 182.65/183.13  Inuse:        4719
% 182.65/183.13  Deleted:      18142
% 182.65/183.13  Deletedinuse: 187
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  
% 182.65/183.13  Intermediate Status:
% 182.65/183.13  Generated:    1006499
% 182.65/183.13  Kept:         214576
% 182.65/183.13  Inuse:        4752
% 182.65/183.13  Deleted:      18142
% 182.65/183.13  Deletedinuse: 187
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  
% 182.65/183.13  Intermediate Status:
% 182.65/183.13  Generated:    1013729
% 182.65/183.13  Kept:         216641
% 182.65/183.13  Inuse:        4770
% 182.65/183.13  Deleted:      18142
% 182.65/183.13  Deletedinuse: 187
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  
% 182.65/183.13  Intermediate Status:
% 182.65/183.13  Generated:    1022838
% 182.65/183.13  Kept:         218646
% 182.65/183.13  Inuse:        4789
% 182.65/183.13  Deleted:      18142
% 182.65/183.13  Deletedinuse: 187
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  
% 182.65/183.13  Intermediate Status:
% 182.65/183.13  Generated:    1033682
% 182.65/183.13  Kept:         220685
% 182.65/183.13  Inuse:        4819
% 182.65/183.13  Deleted:      18142
% 182.65/183.13  Deletedinuse: 187
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  Resimplifying inuse:
% 182.65/183.13  Done
% 182.65/183.13  
% 182.65/183.13  
% 182.65/183.13  Intermediate Status:
% 182.65/183.13  Generated:    1042267
% 182.65/183.13  Kept:         222831
% 182.65/183.14  Inuse:        4850
% 182.65/183.14  Deleted:      18142
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying clauses:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1051544
% 182.65/183.14  Kept:         224854
% 182.65/183.14  Inuse:        4879
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1062479
% 182.65/183.14  Kept:         226871
% 182.65/183.14  Inuse:        4901
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1071570
% 182.65/183.14  Kept:         228883
% 182.65/183.14  Inuse:        4946
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1080162
% 182.65/183.14  Kept:         230938
% 182.65/183.14  Inuse:        4991
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1090053
% 182.65/183.14  Kept:         233126
% 182.65/183.14  Inuse:        5028
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1100934
% 182.65/183.14  Kept:         235414
% 182.65/183.14  Inuse:        5081
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1105164
% 182.65/183.14  Kept:         237429
% 182.65/183.14  Inuse:        5101
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  *** allocated 14778652 integers for clauses
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1116734
% 182.65/183.14  Kept:         239750
% 182.65/183.14  Inuse:        5193
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1126359
% 182.65/183.14  Kept:         241762
% 182.65/183.14  Inuse:        5236
% 182.65/183.14  Deleted:      19069
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying clauses:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1133291
% 182.65/183.14  Kept:         243842
% 182.65/183.14  Inuse:        5265
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1151847
% 182.65/183.14  Kept:         245842
% 182.65/183.14  Inuse:        5342
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1172379
% 182.65/183.14  Kept:         247859
% 182.65/183.14  Inuse:        5432
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1187645
% 182.65/183.14  Kept:         249989
% 182.65/183.14  Inuse:        5496
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1197667
% 182.65/183.14  Kept:         252100
% 182.65/183.14  Inuse:        5534
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1204531
% 182.65/183.14  Kept:         254234
% 182.65/183.14  Inuse:        5546
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 182.65/183.14  Generated:    1212167
% 182.65/183.14  Kept:         256280
% 182.65/183.14  Inuse:        5564
% 182.65/183.14  Deleted:      19380
% 182.65/183.14  Deletedinuse: 187
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  Resimplifying inuse:
% 182.65/183.14  Done
% 182.65/183.14  
% 182.65/183.14  
% 182.65/183.14  Intermediate Status:
% 261.73/262.18  Generated:    1217560
% 261.73/262.18  Kept:         258516
% 261.73/262.18  Inuse:        5574
% 261.73/262.18  Deleted:      19380
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1224097
% 261.73/262.18  Kept:         260739
% 261.73/262.18  Inuse:        5580
% 261.73/262.18  Deleted:      19380
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1231546
% 261.73/262.18  Kept:         263030
% 261.73/262.18  Inuse:        5587
% 261.73/262.18  Deleted:      19380
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying clauses:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1238829
% 261.73/262.18  Kept:         265230
% 261.73/262.18  Inuse:        5605
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1245922
% 261.73/262.18  Kept:         267238
% 261.73/262.18  Inuse:        5620
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1256574
% 261.73/262.18  Kept:         269392
% 261.73/262.18  Inuse:        5656
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1263656
% 261.73/262.18  Kept:         271462
% 261.73/262.18  Inuse:        5680
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1272732
% 261.73/262.18  Kept:         273480
% 261.73/262.18  Inuse:        5721
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1282181
% 261.73/262.18  Kept:         275682
% 261.73/262.18  Inuse:        5787
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1294301
% 261.73/262.18  Kept:         277692
% 261.73/262.18  Inuse:        5821
% 261.73/262.18  Deleted:      20384
% 261.73/262.18  Deletedinuse: 187
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1305955
% 261.73/262.18  Kept:         279693
% 261.73/262.18  Inuse:        5847
% 261.73/262.18  Deleted:      20385
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1316114
% 261.73/262.18  Kept:         281857
% 261.73/262.18  Inuse:        5869
% 261.73/262.18  Deleted:      20385
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1325182
% 261.73/262.18  Kept:         283983
% 261.73/262.18  Inuse:        5883
% 261.73/262.18  Deleted:      20385
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying clauses:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1331657
% 261.73/262.18  Kept:         286012
% 261.73/262.18  Inuse:        5892
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1338858
% 261.73/262.18  Kept:         288083
% 261.73/262.18  Inuse:        5902
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1346221
% 261.73/262.18  Kept:         290461
% 261.73/262.18  Inuse:        5908
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1351114
% 261.73/262.18  Kept:         292461
% 261.73/262.18  Inuse:        5913
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1356122
% 261.73/262.18  Kept:         294588
% 261.73/262.18  Inuse:        5931
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1366905
% 261.73/262.18  Kept:         296634
% 261.73/262.18  Inuse:        5988
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1376592
% 261.73/262.18  Kept:         298782
% 261.73/262.18  Inuse:        6040
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1383262
% 261.73/262.18  Kept:         301131
% 261.73/262.18  Inuse:        6049
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1388616
% 261.73/262.18  Kept:         303206
% 261.73/262.18  Inuse:        6054
% 261.73/262.18  Deleted:      20934
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying clauses:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1395271
% 261.73/262.18  Kept:         305583
% 261.73/262.18  Inuse:        6062
% 261.73/262.18  Deleted:      21337
% 261.73/262.18  Deletedinuse: 188
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  Resimplifying inuse:
% 261.73/262.18  Done
% 261.73/262.18  
% 261.73/262.18  
% 261.73/262.18  Intermediate Status:
% 261.73/262.18  Generated:    1402004
% 261.73/262.18  Kept:         307746
% 261.73/262.18  InCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------