Bliksem---1.12.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Bliksem---1.12
% Problem  : SWC259+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : bliksem %s

% Computer : n023.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:35:16 EDT 2022

% Result   : Theorem 2.82s 3.26s
% Output   : Refutation 2.82s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SWC259+1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.13  % Command  : bliksem %s
% 0.13/0.34  % Computer : n023.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % DateTime : Sun Jun 12 00:25:06 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.43/1.16  *** allocated 10000 integers for termspace/termends
% 0.43/1.16  *** allocated 10000 integers for clauses
% 0.43/1.16  *** allocated 10000 integers for justifications
% 0.43/1.16  Bliksem 1.12
% 0.43/1.16  
% 0.43/1.16  
% 0.43/1.16  Automatic Strategy Selection
% 0.43/1.16  
% 0.43/1.16  *** allocated 15000 integers for termspace/termends
% 0.43/1.16  
% 0.43/1.16  Clauses:
% 0.43/1.16  
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! neq( X, Y ), ! X = Y }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), X = Y, neq( X, Y ) }.
% 0.43/1.16  { ssItem( skol1 ) }.
% 0.43/1.16  { ssItem( skol48 ) }.
% 0.43/1.16  { ! skol1 = skol48 }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ! memberP( X, Y ), ssList( skol2( Z, T ) )
% 0.43/1.16     }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ! memberP( X, Y ), alpha1( X, Y, skol2( X, 
% 0.43/1.16    Y ) ) }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ! ssList( Z ), ! alpha1( X, Y, Z ), memberP
% 0.43/1.16    ( X, Y ) }.
% 0.43/1.16  { ! alpha1( X, Y, Z ), ssList( skol3( T, U, W ) ) }.
% 0.43/1.16  { ! alpha1( X, Y, Z ), app( Z, cons( Y, skol3( X, Y, Z ) ) ) = X }.
% 0.43/1.16  { ! ssList( T ), ! app( Z, cons( Y, T ) ) = X, alpha1( X, Y, Z ) }.
% 0.43/1.16  { ! ssList( X ), ! singletonP( X ), ssItem( skol4( Y ) ) }.
% 0.43/1.16  { ! ssList( X ), ! singletonP( X ), cons( skol4( X ), nil ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ! cons( Y, nil ) = X, singletonP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! frontsegP( X, Y ), ssList( skol5( Z, T )
% 0.43/1.16     ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! frontsegP( X, Y ), app( Y, skol5( X, Y )
% 0.43/1.16     ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Y, Z ) = X, frontsegP
% 0.43/1.16    ( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X, Y ), ssList( skol6( Z, T ) )
% 0.43/1.16     }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X, Y ), app( skol6( X, Y ), Y )
% 0.43/1.16     = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Z, Y ) = X, rearsegP
% 0.43/1.16    ( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! segmentP( X, Y ), ssList( skol7( Z, T ) )
% 0.43/1.16     }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! segmentP( X, Y ), alpha2( X, Y, skol7( X
% 0.43/1.16    , Y ) ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! alpha2( X, Y, Z ), 
% 0.43/1.16    segmentP( X, Y ) }.
% 0.43/1.16  { ! alpha2( X, Y, Z ), ssList( skol8( T, U, W ) ) }.
% 0.43/1.16  { ! alpha2( X, Y, Z ), app( app( Z, Y ), skol8( X, Y, Z ) ) = X }.
% 0.43/1.16  { ! ssList( T ), ! app( app( Z, Y ), T ) = X, alpha2( X, Y, Z ) }.
% 0.43/1.16  { ! ssList( X ), ! cyclefreeP( X ), ! ssItem( Y ), alpha3( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol9( Y ) ), cyclefreeP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha3( X, skol9( X ) ), cyclefreeP( X ) }.
% 0.43/1.16  { ! alpha3( X, Y ), ! ssItem( Z ), alpha21( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol10( Z, T ) ), alpha3( X, Y ) }.
% 0.43/1.16  { ! alpha21( X, Y, skol10( X, Y ) ), alpha3( X, Y ) }.
% 0.43/1.16  { ! alpha21( X, Y, Z ), ! ssList( T ), alpha28( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol11( T, U, W ) ), alpha21( X, Y, Z ) }.
% 0.43/1.16  { ! alpha28( X, Y, Z, skol11( X, Y, Z ) ), alpha21( X, Y, Z ) }.
% 0.43/1.16  { ! alpha28( X, Y, Z, T ), ! ssList( U ), alpha35( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol12( U, W, V0, V1 ) ), alpha28( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha35( X, Y, Z, T, skol12( X, Y, Z, T ) ), alpha28( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha35( X, Y, Z, T, U ), ! ssList( W ), alpha41( X, Y, Z, T, U, W ) }
% 0.43/1.16    .
% 0.43/1.16  { ssList( skol13( W, V0, V1, V2, V3 ) ), alpha35( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha41( X, Y, Z, T, U, skol13( X, Y, Z, T, U ) ), alpha35( X, Y, Z, T
% 0.43/1.16    , U ) }.
% 0.43/1.16  { ! alpha41( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.43/1.16     ) ) = X, alpha12( Y, Z ) }.
% 0.43/1.16  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha41( X, Y, Z, T, U, 
% 0.43/1.16    W ) }.
% 0.43/1.16  { ! alpha12( Y, Z ), alpha41( X, Y, Z, T, U, W ) }.
% 0.43/1.16  { ! alpha12( X, Y ), ! leq( X, Y ), ! leq( Y, X ) }.
% 0.43/1.16  { leq( X, Y ), alpha12( X, Y ) }.
% 0.43/1.16  { leq( Y, X ), alpha12( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ! totalorderP( X ), ! ssItem( Y ), alpha4( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol14( Y ) ), totalorderP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha4( X, skol14( X ) ), totalorderP( X ) }.
% 0.43/1.16  { ! alpha4( X, Y ), ! ssItem( Z ), alpha22( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol15( Z, T ) ), alpha4( X, Y ) }.
% 0.43/1.16  { ! alpha22( X, Y, skol15( X, Y ) ), alpha4( X, Y ) }.
% 0.43/1.16  { ! alpha22( X, Y, Z ), ! ssList( T ), alpha29( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol16( T, U, W ) ), alpha22( X, Y, Z ) }.
% 0.43/1.16  { ! alpha29( X, Y, Z, skol16( X, Y, Z ) ), alpha22( X, Y, Z ) }.
% 0.43/1.16  { ! alpha29( X, Y, Z, T ), ! ssList( U ), alpha36( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol17( U, W, V0, V1 ) ), alpha29( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha36( X, Y, Z, T, skol17( X, Y, Z, T ) ), alpha29( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha36( X, Y, Z, T, U ), ! ssList( W ), alpha42( X, Y, Z, T, U, W ) }
% 0.43/1.16    .
% 0.43/1.16  { ssList( skol18( W, V0, V1, V2, V3 ) ), alpha36( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha42( X, Y, Z, T, U, skol18( X, Y, Z, T, U ) ), alpha36( X, Y, Z, T
% 0.43/1.16    , U ) }.
% 0.43/1.16  { ! alpha42( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.43/1.16     ) ) = X, alpha13( Y, Z ) }.
% 0.43/1.16  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha42( X, Y, Z, T, U, 
% 0.43/1.16    W ) }.
% 0.43/1.16  { ! alpha13( Y, Z ), alpha42( X, Y, Z, T, U, W ) }.
% 0.43/1.16  { ! alpha13( X, Y ), leq( X, Y ), leq( Y, X ) }.
% 0.43/1.16  { ! leq( X, Y ), alpha13( X, Y ) }.
% 0.43/1.16  { ! leq( Y, X ), alpha13( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ! strictorderP( X ), ! ssItem( Y ), alpha5( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol19( Y ) ), strictorderP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha5( X, skol19( X ) ), strictorderP( X ) }.
% 0.43/1.16  { ! alpha5( X, Y ), ! ssItem( Z ), alpha23( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol20( Z, T ) ), alpha5( X, Y ) }.
% 0.43/1.16  { ! alpha23( X, Y, skol20( X, Y ) ), alpha5( X, Y ) }.
% 0.43/1.16  { ! alpha23( X, Y, Z ), ! ssList( T ), alpha30( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol21( T, U, W ) ), alpha23( X, Y, Z ) }.
% 0.43/1.16  { ! alpha30( X, Y, Z, skol21( X, Y, Z ) ), alpha23( X, Y, Z ) }.
% 0.43/1.16  { ! alpha30( X, Y, Z, T ), ! ssList( U ), alpha37( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol22( U, W, V0, V1 ) ), alpha30( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha37( X, Y, Z, T, skol22( X, Y, Z, T ) ), alpha30( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha37( X, Y, Z, T, U ), ! ssList( W ), alpha43( X, Y, Z, T, U, W ) }
% 0.43/1.16    .
% 0.43/1.16  { ssList( skol23( W, V0, V1, V2, V3 ) ), alpha37( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha43( X, Y, Z, T, U, skol23( X, Y, Z, T, U ) ), alpha37( X, Y, Z, T
% 0.43/1.16    , U ) }.
% 0.43/1.16  { ! alpha43( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.43/1.16     ) ) = X, alpha14( Y, Z ) }.
% 0.43/1.16  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha43( X, Y, Z, T, U, 
% 0.43/1.16    W ) }.
% 0.43/1.16  { ! alpha14( Y, Z ), alpha43( X, Y, Z, T, U, W ) }.
% 0.43/1.16  { ! alpha14( X, Y ), lt( X, Y ), lt( Y, X ) }.
% 0.43/1.16  { ! lt( X, Y ), alpha14( X, Y ) }.
% 0.43/1.16  { ! lt( Y, X ), alpha14( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ! totalorderedP( X ), ! ssItem( Y ), alpha6( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol24( Y ) ), totalorderedP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha6( X, skol24( X ) ), totalorderedP( X ) }.
% 0.43/1.16  { ! alpha6( X, Y ), ! ssItem( Z ), alpha15( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol25( Z, T ) ), alpha6( X, Y ) }.
% 0.43/1.16  { ! alpha15( X, Y, skol25( X, Y ) ), alpha6( X, Y ) }.
% 0.43/1.16  { ! alpha15( X, Y, Z ), ! ssList( T ), alpha24( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol26( T, U, W ) ), alpha15( X, Y, Z ) }.
% 0.43/1.16  { ! alpha24( X, Y, Z, skol26( X, Y, Z ) ), alpha15( X, Y, Z ) }.
% 0.43/1.16  { ! alpha24( X, Y, Z, T ), ! ssList( U ), alpha31( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol27( U, W, V0, V1 ) ), alpha24( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha31( X, Y, Z, T, skol27( X, Y, Z, T ) ), alpha24( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha31( X, Y, Z, T, U ), ! ssList( W ), alpha38( X, Y, Z, T, U, W ) }
% 0.43/1.16    .
% 0.43/1.16  { ssList( skol28( W, V0, V1, V2, V3 ) ), alpha31( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha38( X, Y, Z, T, U, skol28( X, Y, Z, T, U ) ), alpha31( X, Y, Z, T
% 0.43/1.16    , U ) }.
% 0.43/1.16  { ! alpha38( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.43/1.16     ) ) = X, leq( Y, Z ) }.
% 0.43/1.16  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha38( X, Y, Z, T, U, 
% 0.43/1.16    W ) }.
% 0.43/1.16  { ! leq( Y, Z ), alpha38( X, Y, Z, T, U, W ) }.
% 0.43/1.16  { ! ssList( X ), ! strictorderedP( X ), ! ssItem( Y ), alpha7( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol29( Y ) ), strictorderedP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha7( X, skol29( X ) ), strictorderedP( X ) }.
% 0.43/1.16  { ! alpha7( X, Y ), ! ssItem( Z ), alpha16( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol30( Z, T ) ), alpha7( X, Y ) }.
% 0.43/1.16  { ! alpha16( X, Y, skol30( X, Y ) ), alpha7( X, Y ) }.
% 0.43/1.16  { ! alpha16( X, Y, Z ), ! ssList( T ), alpha25( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol31( T, U, W ) ), alpha16( X, Y, Z ) }.
% 0.43/1.16  { ! alpha25( X, Y, Z, skol31( X, Y, Z ) ), alpha16( X, Y, Z ) }.
% 0.43/1.16  { ! alpha25( X, Y, Z, T ), ! ssList( U ), alpha32( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol32( U, W, V0, V1 ) ), alpha25( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha32( X, Y, Z, T, skol32( X, Y, Z, T ) ), alpha25( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha32( X, Y, Z, T, U ), ! ssList( W ), alpha39( X, Y, Z, T, U, W ) }
% 0.43/1.16    .
% 0.43/1.16  { ssList( skol33( W, V0, V1, V2, V3 ) ), alpha32( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha39( X, Y, Z, T, U, skol33( X, Y, Z, T, U ) ), alpha32( X, Y, Z, T
% 0.43/1.16    , U ) }.
% 0.43/1.16  { ! alpha39( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.43/1.16     ) ) = X, lt( Y, Z ) }.
% 0.43/1.16  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha39( X, Y, Z, T, U, 
% 0.43/1.16    W ) }.
% 0.43/1.16  { ! lt( Y, Z ), alpha39( X, Y, Z, T, U, W ) }.
% 0.43/1.16  { ! ssList( X ), ! duplicatefreeP( X ), ! ssItem( Y ), alpha8( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol34( Y ) ), duplicatefreeP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha8( X, skol34( X ) ), duplicatefreeP( X ) }.
% 0.43/1.16  { ! alpha8( X, Y ), ! ssItem( Z ), alpha17( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol35( Z, T ) ), alpha8( X, Y ) }.
% 0.43/1.16  { ! alpha17( X, Y, skol35( X, Y ) ), alpha8( X, Y ) }.
% 0.43/1.16  { ! alpha17( X, Y, Z ), ! ssList( T ), alpha26( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol36( T, U, W ) ), alpha17( X, Y, Z ) }.
% 0.43/1.16  { ! alpha26( X, Y, Z, skol36( X, Y, Z ) ), alpha17( X, Y, Z ) }.
% 0.43/1.16  { ! alpha26( X, Y, Z, T ), ! ssList( U ), alpha33( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol37( U, W, V0, V1 ) ), alpha26( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha33( X, Y, Z, T, skol37( X, Y, Z, T ) ), alpha26( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha33( X, Y, Z, T, U ), ! ssList( W ), alpha40( X, Y, Z, T, U, W ) }
% 0.43/1.16    .
% 0.43/1.16  { ssList( skol38( W, V0, V1, V2, V3 ) ), alpha33( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha40( X, Y, Z, T, U, skol38( X, Y, Z, T, U ) ), alpha33( X, Y, Z, T
% 0.43/1.16    , U ) }.
% 0.43/1.16  { ! alpha40( X, Y, Z, T, U, W ), ! app( app( T, cons( Y, U ) ), cons( Z, W
% 0.43/1.16     ) ) = X, ! Y = Z }.
% 0.43/1.16  { app( app( T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha40( X, Y, Z, T, U, 
% 0.43/1.16    W ) }.
% 0.43/1.16  { Y = Z, alpha40( X, Y, Z, T, U, W ) }.
% 0.43/1.16  { ! ssList( X ), ! equalelemsP( X ), ! ssItem( Y ), alpha9( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ssItem( skol39( Y ) ), equalelemsP( X ) }.
% 0.43/1.16  { ! ssList( X ), ! alpha9( X, skol39( X ) ), equalelemsP( X ) }.
% 0.43/1.16  { ! alpha9( X, Y ), ! ssItem( Z ), alpha18( X, Y, Z ) }.
% 0.43/1.16  { ssItem( skol40( Z, T ) ), alpha9( X, Y ) }.
% 0.43/1.16  { ! alpha18( X, Y, skol40( X, Y ) ), alpha9( X, Y ) }.
% 0.43/1.16  { ! alpha18( X, Y, Z ), ! ssList( T ), alpha27( X, Y, Z, T ) }.
% 0.43/1.16  { ssList( skol41( T, U, W ) ), alpha18( X, Y, Z ) }.
% 0.43/1.16  { ! alpha27( X, Y, Z, skol41( X, Y, Z ) ), alpha18( X, Y, Z ) }.
% 0.43/1.16  { ! alpha27( X, Y, Z, T ), ! ssList( U ), alpha34( X, Y, Z, T, U ) }.
% 0.43/1.16  { ssList( skol42( U, W, V0, V1 ) ), alpha27( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha34( X, Y, Z, T, skol42( X, Y, Z, T ) ), alpha27( X, Y, Z, T ) }.
% 0.43/1.16  { ! alpha34( X, Y, Z, T, U ), ! app( T, cons( Y, cons( Z, U ) ) ) = X, Y = 
% 0.43/1.16    Z }.
% 0.43/1.16  { app( T, cons( Y, cons( Z, U ) ) ) = X, alpha34( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! Y = Z, alpha34( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! neq( X, Y ), ! X = Y }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), X = Y, neq( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ssList( cons( Y, X ) ) }.
% 0.43/1.16  { ssList( nil ) }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ! cons( Y, X ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z ), ! ssItem( T ), ! cons( Z, X
% 0.43/1.16     ) = cons( T, Y ), Z = T }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z ), ! ssItem( T ), ! cons( Z, X
% 0.43/1.16     ) = cons( T, Y ), Y = X }.
% 0.43/1.16  { ! ssList( X ), nil = X, ssList( skol43( Y ) ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, ssItem( skol49( Y ) ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, cons( skol49( X ), skol43( X ) ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), ! nil = cons( Y, X ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, ssItem( hd( X ) ) }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), hd( cons( Y, X ) ) = Y }.
% 0.43/1.16  { ! ssList( X ), nil = X, ssList( tl( X ) ) }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), tl( cons( Y, X ) ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ssList( app( X, Y ) ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z ), cons( Z, app( Y, X ) ) = app
% 0.43/1.16    ( cons( Z, Y ), X ) }.
% 0.43/1.16  { ! ssList( X ), app( nil, X ) = X }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! leq( X, Y ), ! leq( Y, X ), X = Y }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! leq( X, Y ), ! leq( Y, Z )
% 0.43/1.16    , leq( X, Z ) }.
% 0.43/1.16  { ! ssItem( X ), leq( X, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! geq( X, Y ), leq( Y, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! leq( Y, X ), geq( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y ), ! lt( Y, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! lt( X, Y ), ! lt( Y, Z ), 
% 0.43/1.16    lt( X, Z ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! gt( X, Y ), lt( Y, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! lt( Y, X ), gt( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z ), ! memberP( app( Y, Z ), X )
% 0.43/1.16    , memberP( Y, X ), memberP( Z, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z ), ! memberP( Y, X ), memberP( 
% 0.43/1.16    app( Y, Z ), X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z ), ! memberP( Z, X ), memberP( 
% 0.43/1.16    app( Y, Z ), X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! memberP( cons( Y, Z ), X )
% 0.43/1.16    , X = Y, memberP( Z, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! X = Y, memberP( cons( Y, Z
% 0.43/1.16     ), X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! memberP( Z, X ), memberP( 
% 0.43/1.16    cons( Y, Z ), X ) }.
% 0.43/1.16  { ! ssItem( X ), ! memberP( nil, X ) }.
% 0.43/1.16  { ! singletonP( nil ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! frontsegP( X, Y ), ! 
% 0.43/1.16    frontsegP( Y, Z ), frontsegP( X, Z ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! frontsegP( X, Y ), ! frontsegP( Y, X ), X
% 0.43/1.16     = Y }.
% 0.43/1.16  { ! ssList( X ), frontsegP( X, X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! frontsegP( X, Y ), 
% 0.43/1.16    frontsegP( app( X, Z ), Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! ssList( T ), ! frontsegP( 
% 0.43/1.16    cons( X, Z ), cons( Y, T ) ), X = Y }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! ssList( T ), ! frontsegP( 
% 0.43/1.16    cons( X, Z ), cons( Y, T ) ), frontsegP( Z, T ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z ), ! ssList( T ), ! X = Y, ! 
% 0.43/1.16    frontsegP( Z, T ), frontsegP( cons( X, Z ), cons( Y, T ) ) }.
% 0.43/1.16  { ! ssList( X ), frontsegP( X, nil ) }.
% 0.43/1.16  { ! ssList( X ), ! frontsegP( nil, X ), nil = X }.
% 0.43/1.16  { ! ssList( X ), ! nil = X, frontsegP( nil, X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! rearsegP( X, Y ), ! 
% 0.43/1.16    rearsegP( Y, Z ), rearsegP( X, Z ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X, Y ), ! rearsegP( Y, X ), X =
% 0.43/1.16     Y }.
% 0.43/1.16  { ! ssList( X ), rearsegP( X, X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! rearsegP( X, Y ), rearsegP
% 0.43/1.16    ( app( Z, X ), Y ) }.
% 0.43/1.16  { ! ssList( X ), rearsegP( X, nil ) }.
% 0.43/1.16  { ! ssList( X ), ! rearsegP( nil, X ), nil = X }.
% 0.43/1.16  { ! ssList( X ), ! nil = X, rearsegP( nil, X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! segmentP( X, Y ), ! 
% 0.43/1.16    segmentP( Y, Z ), segmentP( X, Z ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! segmentP( X, Y ), ! segmentP( Y, X ), X =
% 0.43/1.16     Y }.
% 0.43/1.16  { ! ssList( X ), segmentP( X, X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! ssList( T ), ! segmentP( X
% 0.43/1.16    , Y ), segmentP( app( app( Z, X ), T ), Y ) }.
% 0.43/1.16  { ! ssList( X ), segmentP( X, nil ) }.
% 0.43/1.16  { ! ssList( X ), ! segmentP( nil, X ), nil = X }.
% 0.43/1.16  { ! ssList( X ), ! nil = X, segmentP( nil, X ) }.
% 0.43/1.16  { ! ssItem( X ), cyclefreeP( cons( X, nil ) ) }.
% 0.43/1.16  { cyclefreeP( nil ) }.
% 0.43/1.16  { ! ssItem( X ), totalorderP( cons( X, nil ) ) }.
% 0.43/1.16  { totalorderP( nil ) }.
% 0.43/1.16  { ! ssItem( X ), strictorderP( cons( X, nil ) ) }.
% 0.43/1.16  { strictorderP( nil ) }.
% 0.43/1.16  { ! ssItem( X ), totalorderedP( cons( X, nil ) ) }.
% 0.43/1.16  { totalorderedP( nil ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! totalorderedP( cons( X, Y ) ), nil = Y, 
% 0.43/1.16    alpha10( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! nil = Y, totalorderedP( cons( X, Y ) ) }
% 0.43/1.16    .
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! alpha10( X, Y ), totalorderedP( cons( X, 
% 0.43/1.16    Y ) ) }.
% 0.43/1.16  { ! alpha10( X, Y ), ! nil = Y }.
% 0.43/1.16  { ! alpha10( X, Y ), alpha19( X, Y ) }.
% 0.43/1.16  { nil = Y, ! alpha19( X, Y ), alpha10( X, Y ) }.
% 0.43/1.16  { ! alpha19( X, Y ), totalorderedP( Y ) }.
% 0.43/1.16  { ! alpha19( X, Y ), leq( X, hd( Y ) ) }.
% 0.43/1.16  { ! totalorderedP( Y ), ! leq( X, hd( Y ) ), alpha19( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), strictorderedP( cons( X, nil ) ) }.
% 0.43/1.16  { strictorderedP( nil ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! strictorderedP( cons( X, Y ) ), nil = Y, 
% 0.43/1.16    alpha11( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! nil = Y, strictorderedP( cons( X, Y ) ) }
% 0.43/1.16    .
% 0.43/1.16  { ! ssItem( X ), ! ssList( Y ), ! alpha11( X, Y ), strictorderedP( cons( X
% 0.43/1.16    , Y ) ) }.
% 0.43/1.16  { ! alpha11( X, Y ), ! nil = Y }.
% 0.43/1.16  { ! alpha11( X, Y ), alpha20( X, Y ) }.
% 0.43/1.16  { nil = Y, ! alpha20( X, Y ), alpha11( X, Y ) }.
% 0.43/1.16  { ! alpha20( X, Y ), strictorderedP( Y ) }.
% 0.43/1.16  { ! alpha20( X, Y ), lt( X, hd( Y ) ) }.
% 0.43/1.16  { ! strictorderedP( Y ), ! lt( X, hd( Y ) ), alpha20( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), duplicatefreeP( cons( X, nil ) ) }.
% 0.43/1.16  { duplicatefreeP( nil ) }.
% 0.43/1.16  { ! ssItem( X ), equalelemsP( cons( X, nil ) ) }.
% 0.43/1.16  { equalelemsP( nil ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, ssItem( skol44( Y ) ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, hd( X ) = skol44( X ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, ssList( skol45( Y ) ) }.
% 0.43/1.16  { ! ssList( X ), nil = X, tl( X ) = skol45( X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), nil = Y, nil = X, ! hd( Y ) = hd( X ), ! tl
% 0.43/1.16    ( Y ) = tl( X ), Y = X }.
% 0.43/1.16  { ! ssList( X ), nil = X, cons( hd( X ), tl( X ) ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Z, Y ) = app( X, Y )
% 0.43/1.16    , Z = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), ! app( Y, Z ) = app( Y, X )
% 0.43/1.16    , Z = X }.
% 0.43/1.16  { ! ssList( X ), ! ssItem( Y ), cons( Y, X ) = app( cons( Y, nil ), X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! ssList( Z ), app( app( X, Y ), Z ) = app
% 0.43/1.16    ( X, app( Y, Z ) ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! nil = app( X, Y ), nil = Y }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! nil = app( X, Y ), nil = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), ! nil = Y, ! nil = X, nil = app( X, Y ) }.
% 0.43/1.16  { ! ssList( X ), app( X, nil ) = X }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), nil = X, hd( app( X, Y ) ) = hd( X ) }.
% 0.43/1.16  { ! ssList( X ), ! ssList( Y ), nil = X, tl( app( X, Y ) ) = app( tl( X ), 
% 0.43/1.16    Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! geq( X, Y ), ! geq( Y, X ), X = Y }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! geq( X, Y ), ! geq( Y, Z )
% 0.43/1.16    , geq( X, Z ) }.
% 0.43/1.16  { ! ssItem( X ), geq( X, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! lt( X, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! leq( X, Y ), ! lt( Y, Z )
% 0.43/1.16    , lt( X, Z ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! leq( X, Y ), X = Y, lt( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y ), ! X = Y }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y ), leq( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), X = Y, ! leq( X, Y ), lt( X, Y ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! gt( X, Y ), ! gt( Y, X ) }.
% 0.43/1.16  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z ), ! gt( X, Y ), ! gt( Y, Z ), 
% 0.43/1.16    gt( X, Z ) }.
% 0.43/1.16  { ssList( skol46 ) }.
% 0.43/1.16  { ssList( skol50 ) }.
% 0.43/1.16  { ssList( skol51 ) }.
% 0.43/1.16  { ssList( skol52 ) }.
% 0.43/1.16  { skol50 = skol52 }.
% 0.43/1.16  { skol46 = skol51 }.
% 0.43/1.16  { ! totalorderedP( skol46 ) }.
% 0.43/1.16  { ssItem( skol53 ), alpha44( skol51, skol52 ) }.
% 0.43/1.16  { ssList( skol54 ), alpha44( skol51, skol52 ) }.
% 0.43/1.16  { alpha46( skol51, skol52, skol53, skol54, skol55 ), alpha44( skol51, 
% 0.43/1.16    skol52 ) }.
% 0.43/1.16  { ! ssItem( X ), ! memberP( skol55, X ), ! lt( X, skol53 ), alpha44( skol51
% 0.43/1.16    , skol52 ) }.
% 0.43/1.16  { ! alpha46( X, Y, Z, T, U ), alpha45( X, Z, U ) }.
% 0.43/1.16  { ! alpha46( X, Y, Z, T, U ), app( app( T, X ), U ) = Y }.
% 0.43/1.16  { ! alpha46( X, Y, Z, T, U ), alpha47( Z, T ) }.
% 0.43/1.16  { ! alpha45( X, Z, U ), ! app( app( T, X ), U ) = Y, ! alpha47( Z, T ), 
% 0.43/1.16    alpha46( X, Y, Z, T, U ) }.
% 0.43/1.16  { ! alpha47( X, Y ), ! ssItem( Z ), ! memberP( Y, Z ), ! lt( X, Z ) }.
% 0.43/1.16  { ssItem( skol47( Z, T ) ), alpha47( X, Y ) }.
% 0.43/1.16  { memberP( Y, skol47( Z, Y ) ), alpha47( X, Y ) }.
% 0.43/1.16  { lt( X, skol47( X, Y ) ), alpha47( X, Y ) }.
% 0.43/1.16  { ! alpha45( X, Y, Z ), ssList( Z ) }.
% 0.43/1.16  { ! alpha45( X, Y, Z ), cons( Y, nil ) = X }.
% 0.43/1.16  { ! ssList( Z ), ! cons( Y, nil ) = X, alpha45( X, Y, Z ) }.
% 0.43/1.16  { ! alpha44( X, Y ), nil = Y }.
% 0.43/1.16  { ! alpha44( X, Y ), nil = X }.
% 0.43/1.16  { ! nil = Y, ! nil = X, alpha44( X, Y ) }.
% 0.43/1.16  
% 0.43/1.16  *** allocated 15000 integers for clauses
% 0.43/1.16  percentage equality = 0.130682, percentage horn = 0.753333
% 0.43/1.16  This is a problem with some equality
% 0.43/1.16  
% 0.43/1.16  
% 0.43/1.16  
% 0.43/1.16  Options Used:
% 0.43/1.16  
% 0.43/1.16  useres =            1
% 0.43/1.16  useparamod =        1
% 0.43/1.16  useeqrefl =         1
% 0.43/1.16  useeqfact =         1
% 0.43/1.16  usefactor =         1
% 0.43/1.16  usesimpsplitting =  0
% 0.43/1.16  usesimpdemod =      5
% 0.43/1.16  usesimpres =        3
% 0.43/1.16  
% 0.43/1.16  resimpinuse      =  1000
% 0.43/1.16  resimpclauses =     20000
% 0.43/1.16  substype =          eqrewr
% 0.43/1.16  backwardsubs =      1
% 0.43/1.16  selectoldest =      5
% 0.43/1.16  
% 0.43/1.16  litorderings [0] =  split
% 0.43/1.16  litorderings [1] =  extend the termordering, first sorting on arguments
% 0.43/1.16  
% 0.43/1.16  termordering =      kbo
% 0.43/1.16  
% 0.43/1.16  litapriori =        0
% 0.43/1.16  termapriori =       1
% 0.43/1.16  litaposteriori =    0
% 0.43/1.16  termaposteriori =   0
% 0.43/1.16  demodaposteriori =  0
% 0.43/1.16  ordereqreflfact =   0
% 0.43/1.16  
% 0.43/1.16  litselect =         negord
% 0.43/1.16  
% 0.43/1.16  maxweight =         15
% 0.43/1.16  maxdepth =          30000
% 0.43/1.16  maxlength =         115
% 0.43/1.16  maxnrvars =         195
% 0.43/1.16  excuselevel =       1
% 0.43/1.16  increasemaxweight = 1
% 0.43/1.16  
% 0.43/1.16  maxselected =       10000000
% 0.43/1.16  maxnrclauses =      10000000
% 0.43/1.16  
% 0.43/1.16  showgenerated =    0
% 0.43/1.16  showkept =         0
% 0.43/1.16  showselected =     0
% 0.43/1.16  showdeleted =      0
% 0.43/1.16  showresimp =       1
% 0.43/1.16  showstatus =       2000
% 0.96/1.37  
% 0.96/1.37  prologoutput =     0
% 0.96/1.37  nrgoals =          5000000
% 0.96/1.37  totalproof =       1
% 0.96/1.37  
% 0.96/1.37  Symbols occurring in the translation:
% 0.96/1.37  
% 0.96/1.37  {}  [0, 0]      (w:1, o:2, a:1, s:1, b:0), 
% 0.96/1.37  .  [1, 2]      (w:1, o:54, a:1, s:1, b:0), 
% 0.96/1.37  !  [4, 1]      (w:0, o:25, a:1, s:1, b:0), 
% 0.96/1.37  =  [13, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.96/1.37  ==>  [14, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.96/1.37  ssItem  [36, 1]      (w:1, o:30, a:1, s:1, b:0), 
% 0.96/1.37  neq  [38, 2]      (w:1, o:81, a:1, s:1, b:0), 
% 0.96/1.37  ssList  [39, 1]      (w:1, o:31, a:1, s:1, b:0), 
% 0.96/1.37  memberP  [40, 2]      (w:1, o:80, a:1, s:1, b:0), 
% 0.96/1.37  cons  [43, 2]      (w:1, o:82, a:1, s:1, b:0), 
% 0.96/1.37  app  [44, 2]      (w:1, o:83, a:1, s:1, b:0), 
% 0.96/1.37  singletonP  [45, 1]      (w:1, o:32, a:1, s:1, b:0), 
% 0.96/1.37  nil  [46, 0]      (w:1, o:10, a:1, s:1, b:0), 
% 0.96/1.37  frontsegP  [47, 2]      (w:1, o:84, a:1, s:1, b:0), 
% 0.96/1.37  rearsegP  [48, 2]      (w:1, o:85, a:1, s:1, b:0), 
% 0.96/1.37  segmentP  [49, 2]      (w:1, o:86, a:1, s:1, b:0), 
% 0.96/1.37  cyclefreeP  [50, 1]      (w:1, o:33, a:1, s:1, b:0), 
% 0.96/1.37  leq  [53, 2]      (w:1, o:78, a:1, s:1, b:0), 
% 0.96/1.37  totalorderP  [54, 1]      (w:1, o:48, a:1, s:1, b:0), 
% 0.96/1.37  strictorderP  [55, 1]      (w:1, o:34, a:1, s:1, b:0), 
% 0.96/1.37  lt  [56, 2]      (w:1, o:79, a:1, s:1, b:0), 
% 0.96/1.37  totalorderedP  [57, 1]      (w:1, o:49, a:1, s:1, b:0), 
% 0.96/1.37  strictorderedP  [58, 1]      (w:1, o:35, a:1, s:1, b:0), 
% 0.96/1.37  duplicatefreeP  [59, 1]      (w:1, o:50, a:1, s:1, b:0), 
% 0.96/1.37  equalelemsP  [60, 1]      (w:1, o:51, a:1, s:1, b:0), 
% 0.96/1.37  hd  [61, 1]      (w:1, o:52, a:1, s:1, b:0), 
% 0.96/1.37  tl  [62, 1]      (w:1, o:53, a:1, s:1, b:0), 
% 0.96/1.37  geq  [63, 2]      (w:1, o:87, a:1, s:1, b:0), 
% 0.96/1.37  gt  [64, 2]      (w:1, o:88, a:1, s:1, b:0), 
% 0.96/1.37  alpha1  [68, 3]      (w:1, o:117, a:1, s:1, b:1), 
% 0.96/1.37  alpha2  [69, 3]      (w:1, o:122, a:1, s:1, b:1), 
% 0.96/1.37  alpha3  [70, 2]      (w:1, o:90, a:1, s:1, b:1), 
% 0.96/1.37  alpha4  [71, 2]      (w:1, o:91, a:1, s:1, b:1), 
% 0.96/1.37  alpha5  [72, 2]      (w:1, o:94, a:1, s:1, b:1), 
% 0.96/1.37  alpha6  [73, 2]      (w:1, o:95, a:1, s:1, b:1), 
% 0.96/1.37  alpha7  [74, 2]      (w:1, o:96, a:1, s:1, b:1), 
% 0.96/1.37  alpha8  [75, 2]      (w:1, o:97, a:1, s:1, b:1), 
% 0.96/1.37  alpha9  [76, 2]      (w:1, o:98, a:1, s:1, b:1), 
% 0.96/1.37  alpha10  [77, 2]      (w:1, o:99, a:1, s:1, b:1), 
% 0.96/1.37  alpha11  [78, 2]      (w:1, o:100, a:1, s:1, b:1), 
% 0.96/1.37  alpha12  [79, 2]      (w:1, o:101, a:1, s:1, b:1), 
% 0.96/1.37  alpha13  [80, 2]      (w:1, o:102, a:1, s:1, b:1), 
% 0.96/1.37  alpha14  [81, 2]      (w:1, o:103, a:1, s:1, b:1), 
% 0.96/1.37  alpha15  [82, 3]      (w:1, o:118, a:1, s:1, b:1), 
% 0.96/1.37  alpha16  [83, 3]      (w:1, o:119, a:1, s:1, b:1), 
% 0.96/1.37  alpha17  [84, 3]      (w:1, o:120, a:1, s:1, b:1), 
% 0.96/1.37  alpha18  [85, 3]      (w:1, o:121, a:1, s:1, b:1), 
% 0.96/1.37  alpha19  [86, 2]      (w:1, o:104, a:1, s:1, b:1), 
% 0.96/1.37  alpha20  [87, 2]      (w:1, o:89, a:1, s:1, b:1), 
% 0.96/1.37  alpha21  [88, 3]      (w:1, o:123, a:1, s:1, b:1), 
% 0.96/1.37  alpha22  [89, 3]      (w:1, o:124, a:1, s:1, b:1), 
% 0.96/1.37  alpha23  [90, 3]      (w:1, o:125, a:1, s:1, b:1), 
% 0.96/1.37  alpha24  [91, 4]      (w:1, o:136, a:1, s:1, b:1), 
% 0.96/1.37  alpha25  [92, 4]      (w:1, o:137, a:1, s:1, b:1), 
% 0.96/1.37  alpha26  [93, 4]      (w:1, o:138, a:1, s:1, b:1), 
% 0.96/1.37  alpha27  [94, 4]      (w:1, o:139, a:1, s:1, b:1), 
% 0.96/1.37  alpha28  [95, 4]      (w:1, o:140, a:1, s:1, b:1), 
% 0.96/1.37  alpha29  [96, 4]      (w:1, o:141, a:1, s:1, b:1), 
% 0.96/1.37  alpha30  [97, 4]      (w:1, o:142, a:1, s:1, b:1), 
% 0.96/1.37  alpha31  [98, 5]      (w:1, o:150, a:1, s:1, b:1), 
% 0.96/1.37  alpha32  [99, 5]      (w:1, o:151, a:1, s:1, b:1), 
% 0.96/1.37  alpha33  [100, 5]      (w:1, o:152, a:1, s:1, b:1), 
% 0.96/1.37  alpha34  [101, 5]      (w:1, o:153, a:1, s:1, b:1), 
% 0.96/1.37  alpha35  [102, 5]      (w:1, o:154, a:1, s:1, b:1), 
% 0.96/1.37  alpha36  [103, 5]      (w:1, o:155, a:1, s:1, b:1), 
% 0.96/1.37  alpha37  [104, 5]      (w:1, o:156, a:1, s:1, b:1), 
% 0.96/1.37  alpha38  [105, 6]      (w:1, o:164, a:1, s:1, b:1), 
% 0.96/1.37  alpha39  [106, 6]      (w:1, o:165, a:1, s:1, b:1), 
% 0.96/1.37  alpha40  [107, 6]      (w:1, o:166, a:1, s:1, b:1), 
% 0.96/1.37  alpha41  [108, 6]      (w:1, o:167, a:1, s:1, b:1), 
% 0.96/1.37  alpha42  [109, 6]      (w:1, o:168, a:1, s:1, b:1), 
% 0.96/1.37  alpha43  [110, 6]      (w:1, o:169, a:1, s:1, b:1), 
% 0.96/1.37  alpha44  [111, 2]      (w:1, o:92, a:1, s:1, b:1), 
% 0.96/1.37  alpha45  [112, 3]      (w:1, o:126, a:1, s:1, b:1), 
% 0.96/1.37  alpha46  [113, 5]      (w:1, o:157, a:1, s:1, b:1), 
% 0.96/1.37  alpha47  [114, 2]      (w:1, o:93, a:1, s:1, b:1), 
% 0.96/1.37  skol1  [115, 0]      (w:1, o:16, a:1, s:1, b:1), 
% 0.96/1.37  skol2  [116, 2]      (w:1, o:107, a:1, s:1, b:1), 
% 2.82/3.26  skol3  [117, 3]      (w:1, o:129, a:1, s:1, b:1), 
% 2.82/3.26  skol4  [118, 1]      (w:1, o:38, a:1, s:1, b:1), 
% 2.82/3.26  skol5  [119, 2]      (w:1, o:110, a:1, s:1, b:1), 
% 2.82/3.26  skol6  [120, 2]      (w:1, o:111, a:1, s:1, b:1), 
% 2.82/3.26  skol7  [121, 2]      (w:1, o:112, a:1, s:1, b:1), 
% 2.82/3.26  skol8  [122, 3]      (w:1, o:130, a:1, s:1, b:1), 
% 2.82/3.26  skol9  [123, 1]      (w:1, o:39, a:1, s:1, b:1), 
% 2.82/3.26  skol10  [124, 2]      (w:1, o:105, a:1, s:1, b:1), 
% 2.82/3.26  skol11  [125, 3]      (w:1, o:131, a:1, s:1, b:1), 
% 2.82/3.26  skol12  [126, 4]      (w:1, o:143, a:1, s:1, b:1), 
% 2.82/3.26  skol13  [127, 5]      (w:1, o:158, a:1, s:1, b:1), 
% 2.82/3.26  skol14  [128, 1]      (w:1, o:40, a:1, s:1, b:1), 
% 2.82/3.26  skol15  [129, 2]      (w:1, o:106, a:1, s:1, b:1), 
% 2.82/3.26  skol16  [130, 3]      (w:1, o:132, a:1, s:1, b:1), 
% 2.82/3.26  skol17  [131, 4]      (w:1, o:144, a:1, s:1, b:1), 
% 2.82/3.26  skol18  [132, 5]      (w:1, o:159, a:1, s:1, b:1), 
% 2.82/3.26  skol19  [133, 1]      (w:1, o:41, a:1, s:1, b:1), 
% 2.82/3.26  skol20  [134, 2]      (w:1, o:113, a:1, s:1, b:1), 
% 2.82/3.26  skol21  [135, 3]      (w:1, o:127, a:1, s:1, b:1), 
% 2.82/3.26  skol22  [136, 4]      (w:1, o:145, a:1, s:1, b:1), 
% 2.82/3.26  skol23  [137, 5]      (w:1, o:160, a:1, s:1, b:1), 
% 2.82/3.26  skol24  [138, 1]      (w:1, o:42, a:1, s:1, b:1), 
% 2.82/3.26  skol25  [139, 2]      (w:1, o:114, a:1, s:1, b:1), 
% 2.82/3.26  skol26  [140, 3]      (w:1, o:128, a:1, s:1, b:1), 
% 2.82/3.26  skol27  [141, 4]      (w:1, o:146, a:1, s:1, b:1), 
% 2.82/3.26  skol28  [142, 5]      (w:1, o:161, a:1, s:1, b:1), 
% 2.82/3.26  skol29  [143, 1]      (w:1, o:43, a:1, s:1, b:1), 
% 2.82/3.26  skol30  [144, 2]      (w:1, o:115, a:1, s:1, b:1), 
% 2.82/3.26  skol31  [145, 3]      (w:1, o:133, a:1, s:1, b:1), 
% 2.82/3.26  skol32  [146, 4]      (w:1, o:147, a:1, s:1, b:1), 
% 2.82/3.26  skol33  [147, 5]      (w:1, o:162, a:1, s:1, b:1), 
% 2.82/3.26  skol34  [148, 1]      (w:1, o:36, a:1, s:1, b:1), 
% 2.82/3.26  skol35  [149, 2]      (w:1, o:116, a:1, s:1, b:1), 
% 2.82/3.26  skol36  [150, 3]      (w:1, o:134, a:1, s:1, b:1), 
% 2.82/3.26  skol37  [151, 4]      (w:1, o:148, a:1, s:1, b:1), 
% 2.82/3.26  skol38  [152, 5]      (w:1, o:163, a:1, s:1, b:1), 
% 2.82/3.26  skol39  [153, 1]      (w:1, o:37, a:1, s:1, b:1), 
% 2.82/3.26  skol40  [154, 2]      (w:1, o:108, a:1, s:1, b:1), 
% 2.82/3.26  skol41  [155, 3]      (w:1, o:135, a:1, s:1, b:1), 
% 2.82/3.26  skol42  [156, 4]      (w:1, o:149, a:1, s:1, b:1), 
% 2.82/3.26  skol43  [157, 1]      (w:1, o:44, a:1, s:1, b:1), 
% 2.82/3.26  skol44  [158, 1]      (w:1, o:45, a:1, s:1, b:1), 
% 2.82/3.26  skol45  [159, 1]      (w:1, o:46, a:1, s:1, b:1), 
% 2.82/3.26  skol46  [160, 0]      (w:1, o:17, a:1, s:1, b:1), 
% 2.82/3.26  skol47  [161, 2]      (w:1, o:109, a:1, s:1, b:1), 
% 2.82/3.26  skol48  [162, 0]      (w:1, o:18, a:1, s:1, b:1), 
% 2.82/3.26  skol49  [163, 1]      (w:1, o:47, a:1, s:1, b:1), 
% 2.82/3.26  skol50  [164, 0]      (w:1, o:19, a:1, s:1, b:1), 
% 2.82/3.26  skol51  [165, 0]      (w:1, o:20, a:1, s:1, b:1), 
% 2.82/3.26  skol52  [166, 0]      (w:1, o:21, a:1, s:1, b:1), 
% 2.82/3.26  skol53  [167, 0]      (w:1, o:22, a:1, s:1, b:1), 
% 2.82/3.26  skol54  [168, 0]      (w:1, o:23, a:1, s:1, b:1), 
% 2.82/3.26  skol55  [169, 0]      (w:1, o:24, a:1, s:1, b:1).
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Starting Search:
% 2.82/3.26  
% 2.82/3.26  *** allocated 22500 integers for clauses
% 2.82/3.26  *** allocated 33750 integers for clauses
% 2.82/3.26  *** allocated 50625 integers for clauses
% 2.82/3.26  *** allocated 22500 integers for termspace/termends
% 2.82/3.26  *** allocated 75937 integers for clauses
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 33750 integers for termspace/termends
% 2.82/3.26  *** allocated 113905 integers for clauses
% 2.82/3.26  *** allocated 50625 integers for termspace/termends
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    3415
% 2.82/3.26  Kept:         2005
% 2.82/3.26  Inuse:        198
% 2.82/3.26  Deleted:      9
% 2.82/3.26  Deletedinuse: 2
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 170857 integers for clauses
% 2.82/3.26  *** allocated 75937 integers for termspace/termends
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 256285 integers for clauses
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    7142
% 2.82/3.26  Kept:         4008
% 2.82/3.26  Inuse:        400
% 2.82/3.26  Deleted:      11
% 2.82/3.26  Deletedinuse: 2
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 113905 integers for termspace/termends
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 384427 integers for clauses
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    10285
% 2.82/3.26  Kept:         6008
% 2.82/3.26  Inuse:        546
% 2.82/3.26  Deleted:      14
% 2.82/3.26  Deletedinuse: 4
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 170857 integers for termspace/termends
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 576640 integers for clauses
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    14689
% 2.82/3.26  Kept:         8559
% 2.82/3.26  Inuse:        681
% 2.82/3.26  Deleted:      14
% 2.82/3.26  Deletedinuse: 4
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 256285 integers for termspace/termends
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    19065
% 2.82/3.26  Kept:         10580
% 2.82/3.26  Inuse:        765
% 2.82/3.26  Deleted:      14
% 2.82/3.26  Deletedinuse: 4
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 864960 integers for clauses
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    26137
% 2.82/3.26  Kept:         12641
% 2.82/3.26  Inuse:        792
% 2.82/3.26  Deleted:      25
% 2.82/3.26  Deletedinuse: 15
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 384427 integers for termspace/termends
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    32049
% 2.82/3.26  Kept:         14852
% 2.82/3.26  Inuse:        844
% 2.82/3.26  Deleted:      31
% 2.82/3.26  Deletedinuse: 19
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    38796
% 2.82/3.26  Kept:         16872
% 2.82/3.26  Inuse:        884
% 2.82/3.26  Deleted:      52
% 2.82/3.26  Deletedinuse: 20
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    47862
% 2.82/3.26  Kept:         19015
% 2.82/3.26  Inuse:        914
% 2.82/3.26  Deleted:      54
% 2.82/3.26  Deletedinuse: 22
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 1297440 integers for clauses
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying clauses:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 576640 integers for termspace/termends
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    56777
% 2.82/3.26  Kept:         21192
% 2.82/3.26  Inuse:        946
% 2.82/3.26  Deleted:      2334
% 2.82/3.26  Deletedinuse: 30
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    64201
% 2.82/3.26  Kept:         23215
% 2.82/3.26  Inuse:        987
% 2.82/3.26  Deleted:      2341
% 2.82/3.26  Deletedinuse: 36
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    71017
% 2.82/3.26  Kept:         25220
% 2.82/3.26  Inuse:        1021
% 2.82/3.26  Deleted:      2341
% 2.82/3.26  Deletedinuse: 36
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    78390
% 2.82/3.26  Kept:         27649
% 2.82/3.26  Inuse:        1057
% 2.82/3.26  Deleted:      2345
% 2.82/3.26  Deletedinuse: 37
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 1946160 integers for clauses
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    88785
% 2.82/3.26  Kept:         29758
% 2.82/3.26  Inuse:        1082
% 2.82/3.26  Deleted:      2346
% 2.82/3.26  Deletedinuse: 38
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  *** allocated 864960 integers for termspace/termends
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    97760
% 2.82/3.26  Kept:         32076
% 2.82/3.26  Inuse:        1107
% 2.82/3.26  Deleted:      2346
% 2.82/3.26  Deletedinuse: 38
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    105645
% 2.82/3.26  Kept:         34118
% 2.82/3.26  Inuse:        1132
% 2.82/3.26  Deleted:      2352
% 2.82/3.26  Deletedinuse: 41
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    112579
% 2.82/3.26  Kept:         36137
% 2.82/3.26  Inuse:        1161
% 2.82/3.26  Deleted:      2361
% 2.82/3.26  Deletedinuse: 49
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  Done
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Intermediate Status:
% 2.82/3.26  Generated:    117063
% 2.82/3.26  Kept:         38265
% 2.82/3.26  Inuse:        1182
% 2.82/3.26  Deleted:      2362
% 2.82/3.26  Deletedinuse: 49
% 2.82/3.26  
% 2.82/3.26  Resimplifying inuse:
% 2.82/3.26  
% 2.82/3.26  Bliksems!, er is een bewijs:
% 2.82/3.26  % SZS status Theorem
% 2.82/3.26  % SZS output start Refutation
% 2.82/3.26  
% 2.82/3.26  (223) {G0,W6,D3,L2,V1,M2} I { ! ssItem( X ), totalorderedP( cons( X, nil )
% 2.82/3.26     ) }.
% 2.82/3.26  (224) {G0,W2,D2,L1,V0,M1} I { totalorderedP( nil ) }.
% 2.82/3.26  (279) {G0,W3,D2,L1,V0,M1} I { skol52 ==> skol50 }.
% 2.82/3.26  (280) {G0,W3,D2,L1,V0,M1} I { skol51 ==> skol46 }.
% 2.82/3.26  (281) {G0,W2,D2,L1,V0,M1} I { ! totalorderedP( skol46 ) }.
% 2.82/3.26  (282) {G1,W5,D2,L2,V0,M2} I;d(280);d(279) { ssItem( skol53 ), alpha44( 
% 2.82/3.26    skol46, skol50 ) }.
% 2.82/3.26  (284) {G1,W9,D2,L2,V0,M2} I;d(280);d(280);d(279);d(279) { alpha46( skol46, 
% 2.82/3.26    skol50, skol53, skol54, skol55 ), alpha44( skol46, skol50 ) }.
% 2.82/3.26  (286) {G0,W10,D2,L2,V5,M2} I { ! alpha46( X, Y, Z, T, U ), alpha45( X, Z, U
% 2.82/3.26     ) }.
% 2.82/3.26  (295) {G0,W9,D3,L2,V3,M2} I { ! alpha45( X, Y, Z ), cons( Y, nil ) = X }.
% 2.82/3.26  (298) {G0,W6,D2,L2,V2,M2} I { ! alpha44( X, Y ), nil = X }.
% 2.82/3.26  (874) {G1,W3,D2,L1,V1,M1} P(298,281);r(224) { ! alpha44( skol46, X ) }.
% 2.82/3.26  (884) {G2,W2,D2,L1,V0,M1} R(874,282) { ssItem( skol53 ) }.
% 2.82/3.26  (20534) {G2,W6,D2,L1,V0,M1} S(284);r(874) { alpha46( skol46, skol50, skol53
% 2.82/3.26    , skol54, skol55 ) }.
% 2.82/3.26  (23090) {G3,W4,D3,L1,V0,M1} R(223,884) { totalorderedP( cons( skol53, nil )
% 2.82/3.26     ) }.
% 2.82/3.26  (34771) {G3,W4,D2,L1,V0,M1} R(286,20534) { alpha45( skol46, skol53, skol55
% 2.82/3.26     ) }.
% 2.82/3.26  (37295) {G4,W5,D3,L1,V0,M1} R(295,34771) { cons( skol53, nil ) ==> skol46
% 2.82/3.26     }.
% 2.82/3.26  (38268) {G5,W0,D0,L0,V0,M0} S(23090);d(37295);r(281) {  }.
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  % SZS output end Refutation
% 2.82/3.26  found a proof!
% 2.82/3.26  
% 2.82/3.26  
% 2.82/3.26  Unprocessed initial clauses:
% 2.82/3.26  
% 2.82/3.26  (38270) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! neq( X, Y )
% 2.82/3.26    , ! X = Y }.
% 2.82/3.26  (38271) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), X = Y, neq( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38272) {G0,W2,D2,L1,V0,M1}  { ssItem( skol1 ) }.
% 2.82/3.26  (38273) {G0,W2,D2,L1,V0,M1}  { ssItem( skol48 ) }.
% 2.82/3.26  (38274) {G0,W3,D2,L1,V0,M1}  { ! skol1 = skol48 }.
% 2.82/3.26  (38275) {G0,W11,D3,L4,V4,M4}  { ! ssList( X ), ! ssItem( Y ), ! memberP( X
% 2.82/3.26    , Y ), ssList( skol2( Z, T ) ) }.
% 2.82/3.26  (38276) {G0,W13,D3,L4,V2,M4}  { ! ssList( X ), ! ssItem( Y ), ! memberP( X
% 2.82/3.26    , Y ), alpha1( X, Y, skol2( X, Y ) ) }.
% 2.82/3.26  (38277) {G0,W13,D2,L5,V3,M5}  { ! ssList( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! alpha1( X, Y, Z ), memberP( X, Y ) }.
% 2.82/3.26  (38278) {G0,W9,D3,L2,V6,M2}  { ! alpha1( X, Y, Z ), ssList( skol3( T, U, W
% 2.82/3.26     ) ) }.
% 2.82/3.26  (38279) {G0,W14,D5,L2,V3,M2}  { ! alpha1( X, Y, Z ), app( Z, cons( Y, skol3
% 2.82/3.26    ( X, Y, Z ) ) ) = X }.
% 2.82/3.26  (38280) {G0,W13,D4,L3,V4,M3}  { ! ssList( T ), ! app( Z, cons( Y, T ) ) = X
% 2.82/3.26    , alpha1( X, Y, Z ) }.
% 2.82/3.26  (38281) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ! singletonP( X ), ssItem( 
% 2.82/3.26    skol4( Y ) ) }.
% 2.82/3.26  (38282) {G0,W10,D4,L3,V1,M3}  { ! ssList( X ), ! singletonP( X ), cons( 
% 2.82/3.26    skol4( X ), nil ) = X }.
% 2.82/3.26  (38283) {G0,W11,D3,L4,V2,M4}  { ! ssList( X ), ! ssItem( Y ), ! cons( Y, 
% 2.82/3.26    nil ) = X, singletonP( X ) }.
% 2.82/3.26  (38284) {G0,W11,D3,L4,V4,M4}  { ! ssList( X ), ! ssList( Y ), ! frontsegP( 
% 2.82/3.26    X, Y ), ssList( skol5( Z, T ) ) }.
% 2.82/3.26  (38285) {G0,W14,D4,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), ! frontsegP( 
% 2.82/3.26    X, Y ), app( Y, skol5( X, Y ) ) = X }.
% 2.82/3.26  (38286) {G0,W14,D3,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! app( Y, Z ) = X, frontsegP( X, Y ) }.
% 2.82/3.26  (38287) {G0,W11,D3,L4,V4,M4}  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X
% 2.82/3.26    , Y ), ssList( skol6( Z, T ) ) }.
% 2.82/3.26  (38288) {G0,W14,D4,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X
% 2.82/3.26    , Y ), app( skol6( X, Y ), Y ) = X }.
% 2.82/3.26  (38289) {G0,W14,D3,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! app( Z, Y ) = X, rearsegP( X, Y ) }.
% 2.82/3.26  (38290) {G0,W11,D3,L4,V4,M4}  { ! ssList( X ), ! ssList( Y ), ! segmentP( X
% 2.82/3.26    , Y ), ssList( skol7( Z, T ) ) }.
% 2.82/3.26  (38291) {G0,W13,D3,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), ! segmentP( X
% 2.82/3.26    , Y ), alpha2( X, Y, skol7( X, Y ) ) }.
% 2.82/3.26  (38292) {G0,W13,D2,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! alpha2( X, Y, Z ), segmentP( X, Y ) }.
% 2.82/3.26  (38293) {G0,W9,D3,L2,V6,M2}  { ! alpha2( X, Y, Z ), ssList( skol8( T, U, W
% 2.82/3.26     ) ) }.
% 2.82/3.26  (38294) {G0,W14,D4,L2,V3,M2}  { ! alpha2( X, Y, Z ), app( app( Z, Y ), 
% 2.82/3.26    skol8( X, Y, Z ) ) = X }.
% 2.82/3.26  (38295) {G0,W13,D4,L3,V4,M3}  { ! ssList( T ), ! app( app( Z, Y ), T ) = X
% 2.82/3.26    , alpha2( X, Y, Z ) }.
% 2.82/3.26  (38296) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! cyclefreeP( X ), ! ssItem( 
% 2.82/3.26    Y ), alpha3( X, Y ) }.
% 2.82/3.26  (38297) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol9( Y ) ), 
% 2.82/3.26    cyclefreeP( X ) }.
% 2.82/3.26  (38298) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha3( X, skol9( X ) ), 
% 2.82/3.26    cyclefreeP( X ) }.
% 2.82/3.26  (38299) {G0,W9,D2,L3,V3,M3}  { ! alpha3( X, Y ), ! ssItem( Z ), alpha21( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38300) {G0,W7,D3,L2,V4,M2}  { ssItem( skol10( Z, T ) ), alpha3( X, Y ) }.
% 2.82/3.26  (38301) {G0,W9,D3,L2,V2,M2}  { ! alpha21( X, Y, skol10( X, Y ) ), alpha3( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38302) {G0,W11,D2,L3,V4,M3}  { ! alpha21( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha28( X, Y, Z, T ) }.
% 2.82/3.26  (38303) {G0,W9,D3,L2,V6,M2}  { ssList( skol11( T, U, W ) ), alpha21( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38304) {G0,W12,D3,L2,V3,M2}  { ! alpha28( X, Y, Z, skol11( X, Y, Z ) ), 
% 2.82/3.26    alpha21( X, Y, Z ) }.
% 2.82/3.26  (38305) {G0,W13,D2,L3,V5,M3}  { ! alpha28( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha35( X, Y, Z, T, U ) }.
% 2.82/3.26  (38306) {G0,W11,D3,L2,V8,M2}  { ssList( skol12( U, W, V0, V1 ) ), alpha28( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38307) {G0,W15,D3,L2,V4,M2}  { ! alpha35( X, Y, Z, T, skol12( X, Y, Z, T )
% 2.82/3.26     ), alpha28( X, Y, Z, T ) }.
% 2.82/3.26  (38308) {G0,W15,D2,L3,V6,M3}  { ! alpha35( X, Y, Z, T, U ), ! ssList( W ), 
% 2.82/3.26    alpha41( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38309) {G0,W13,D3,L2,V10,M2}  { ssList( skol13( W, V0, V1, V2, V3 ) ), 
% 2.82/3.26    alpha35( X, Y, Z, T, U ) }.
% 2.82/3.26  (38310) {G0,W18,D3,L2,V5,M2}  { ! alpha41( X, Y, Z, T, U, skol13( X, Y, Z, 
% 2.82/3.26    T, U ) ), alpha35( X, Y, Z, T, U ) }.
% 2.82/3.26  (38311) {G0,W21,D5,L3,V6,M3}  { ! alpha41( X, Y, Z, T, U, W ), ! app( app( 
% 2.82/3.26    T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha12( Y, Z ) }.
% 2.82/3.26  (38312) {G0,W18,D5,L2,V6,M2}  { app( app( T, cons( Y, U ) ), cons( Z, W ) )
% 2.82/3.26     = X, alpha41( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38313) {G0,W10,D2,L2,V6,M2}  { ! alpha12( Y, Z ), alpha41( X, Y, Z, T, U, 
% 2.82/3.26    W ) }.
% 2.82/3.26  (38314) {G0,W9,D2,L3,V2,M3}  { ! alpha12( X, Y ), ! leq( X, Y ), ! leq( Y, 
% 2.82/3.26    X ) }.
% 2.82/3.26  (38315) {G0,W6,D2,L2,V2,M2}  { leq( X, Y ), alpha12( X, Y ) }.
% 2.82/3.26  (38316) {G0,W6,D2,L2,V2,M2}  { leq( Y, X ), alpha12( X, Y ) }.
% 2.82/3.26  (38317) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! totalorderP( X ), ! ssItem
% 2.82/3.26    ( Y ), alpha4( X, Y ) }.
% 2.82/3.26  (38318) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol14( Y ) ), 
% 2.82/3.26    totalorderP( X ) }.
% 2.82/3.26  (38319) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha4( X, skol14( X ) ), 
% 2.82/3.26    totalorderP( X ) }.
% 2.82/3.26  (38320) {G0,W9,D2,L3,V3,M3}  { ! alpha4( X, Y ), ! ssItem( Z ), alpha22( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38321) {G0,W7,D3,L2,V4,M2}  { ssItem( skol15( Z, T ) ), alpha4( X, Y ) }.
% 2.82/3.26  (38322) {G0,W9,D3,L2,V2,M2}  { ! alpha22( X, Y, skol15( X, Y ) ), alpha4( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38323) {G0,W11,D2,L3,V4,M3}  { ! alpha22( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha29( X, Y, Z, T ) }.
% 2.82/3.26  (38324) {G0,W9,D3,L2,V6,M2}  { ssList( skol16( T, U, W ) ), alpha22( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38325) {G0,W12,D3,L2,V3,M2}  { ! alpha29( X, Y, Z, skol16( X, Y, Z ) ), 
% 2.82/3.26    alpha22( X, Y, Z ) }.
% 2.82/3.26  (38326) {G0,W13,D2,L3,V5,M3}  { ! alpha29( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha36( X, Y, Z, T, U ) }.
% 2.82/3.26  (38327) {G0,W11,D3,L2,V8,M2}  { ssList( skol17( U, W, V0, V1 ) ), alpha29( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38328) {G0,W15,D3,L2,V4,M2}  { ! alpha36( X, Y, Z, T, skol17( X, Y, Z, T )
% 2.82/3.26     ), alpha29( X, Y, Z, T ) }.
% 2.82/3.26  (38329) {G0,W15,D2,L3,V6,M3}  { ! alpha36( X, Y, Z, T, U ), ! ssList( W ), 
% 2.82/3.26    alpha42( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38330) {G0,W13,D3,L2,V10,M2}  { ssList( skol18( W, V0, V1, V2, V3 ) ), 
% 2.82/3.26    alpha36( X, Y, Z, T, U ) }.
% 2.82/3.26  (38331) {G0,W18,D3,L2,V5,M2}  { ! alpha42( X, Y, Z, T, U, skol18( X, Y, Z, 
% 2.82/3.26    T, U ) ), alpha36( X, Y, Z, T, U ) }.
% 2.82/3.26  (38332) {G0,W21,D5,L3,V6,M3}  { ! alpha42( X, Y, Z, T, U, W ), ! app( app( 
% 2.82/3.26    T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha13( Y, Z ) }.
% 2.82/3.26  (38333) {G0,W18,D5,L2,V6,M2}  { app( app( T, cons( Y, U ) ), cons( Z, W ) )
% 2.82/3.26     = X, alpha42( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38334) {G0,W10,D2,L2,V6,M2}  { ! alpha13( Y, Z ), alpha42( X, Y, Z, T, U, 
% 2.82/3.26    W ) }.
% 2.82/3.26  (38335) {G0,W9,D2,L3,V2,M3}  { ! alpha13( X, Y ), leq( X, Y ), leq( Y, X )
% 2.82/3.26     }.
% 2.82/3.26  (38336) {G0,W6,D2,L2,V2,M2}  { ! leq( X, Y ), alpha13( X, Y ) }.
% 2.82/3.26  (38337) {G0,W6,D2,L2,V2,M2}  { ! leq( Y, X ), alpha13( X, Y ) }.
% 2.82/3.26  (38338) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! strictorderP( X ), ! ssItem
% 2.82/3.26    ( Y ), alpha5( X, Y ) }.
% 2.82/3.26  (38339) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol19( Y ) ), 
% 2.82/3.26    strictorderP( X ) }.
% 2.82/3.26  (38340) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha5( X, skol19( X ) ), 
% 2.82/3.26    strictorderP( X ) }.
% 2.82/3.26  (38341) {G0,W9,D2,L3,V3,M3}  { ! alpha5( X, Y ), ! ssItem( Z ), alpha23( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38342) {G0,W7,D3,L2,V4,M2}  { ssItem( skol20( Z, T ) ), alpha5( X, Y ) }.
% 2.82/3.26  (38343) {G0,W9,D3,L2,V2,M2}  { ! alpha23( X, Y, skol20( X, Y ) ), alpha5( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38344) {G0,W11,D2,L3,V4,M3}  { ! alpha23( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha30( X, Y, Z, T ) }.
% 2.82/3.26  (38345) {G0,W9,D3,L2,V6,M2}  { ssList( skol21( T, U, W ) ), alpha23( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38346) {G0,W12,D3,L2,V3,M2}  { ! alpha30( X, Y, Z, skol21( X, Y, Z ) ), 
% 2.82/3.26    alpha23( X, Y, Z ) }.
% 2.82/3.26  (38347) {G0,W13,D2,L3,V5,M3}  { ! alpha30( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha37( X, Y, Z, T, U ) }.
% 2.82/3.26  (38348) {G0,W11,D3,L2,V8,M2}  { ssList( skol22( U, W, V0, V1 ) ), alpha30( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38349) {G0,W15,D3,L2,V4,M2}  { ! alpha37( X, Y, Z, T, skol22( X, Y, Z, T )
% 2.82/3.26     ), alpha30( X, Y, Z, T ) }.
% 2.82/3.26  (38350) {G0,W15,D2,L3,V6,M3}  { ! alpha37( X, Y, Z, T, U ), ! ssList( W ), 
% 2.82/3.26    alpha43( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38351) {G0,W13,D3,L2,V10,M2}  { ssList( skol23( W, V0, V1, V2, V3 ) ), 
% 2.82/3.26    alpha37( X, Y, Z, T, U ) }.
% 2.82/3.26  (38352) {G0,W18,D3,L2,V5,M2}  { ! alpha43( X, Y, Z, T, U, skol23( X, Y, Z, 
% 2.82/3.26    T, U ) ), alpha37( X, Y, Z, T, U ) }.
% 2.82/3.26  (38353) {G0,W21,D5,L3,V6,M3}  { ! alpha43( X, Y, Z, T, U, W ), ! app( app( 
% 2.82/3.26    T, cons( Y, U ) ), cons( Z, W ) ) = X, alpha14( Y, Z ) }.
% 2.82/3.26  (38354) {G0,W18,D5,L2,V6,M2}  { app( app( T, cons( Y, U ) ), cons( Z, W ) )
% 2.82/3.26     = X, alpha43( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38355) {G0,W10,D2,L2,V6,M2}  { ! alpha14( Y, Z ), alpha43( X, Y, Z, T, U, 
% 2.82/3.26    W ) }.
% 2.82/3.26  (38356) {G0,W9,D2,L3,V2,M3}  { ! alpha14( X, Y ), lt( X, Y ), lt( Y, X )
% 2.82/3.26     }.
% 2.82/3.26  (38357) {G0,W6,D2,L2,V2,M2}  { ! lt( X, Y ), alpha14( X, Y ) }.
% 2.82/3.26  (38358) {G0,W6,D2,L2,V2,M2}  { ! lt( Y, X ), alpha14( X, Y ) }.
% 2.82/3.26  (38359) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! totalorderedP( X ), ! 
% 2.82/3.26    ssItem( Y ), alpha6( X, Y ) }.
% 2.82/3.26  (38360) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol24( Y ) ), 
% 2.82/3.26    totalorderedP( X ) }.
% 2.82/3.26  (38361) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha6( X, skol24( X ) ), 
% 2.82/3.26    totalorderedP( X ) }.
% 2.82/3.26  (38362) {G0,W9,D2,L3,V3,M3}  { ! alpha6( X, Y ), ! ssItem( Z ), alpha15( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38363) {G0,W7,D3,L2,V4,M2}  { ssItem( skol25( Z, T ) ), alpha6( X, Y ) }.
% 2.82/3.26  (38364) {G0,W9,D3,L2,V2,M2}  { ! alpha15( X, Y, skol25( X, Y ) ), alpha6( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38365) {G0,W11,D2,L3,V4,M3}  { ! alpha15( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha24( X, Y, Z, T ) }.
% 2.82/3.26  (38366) {G0,W9,D3,L2,V6,M2}  { ssList( skol26( T, U, W ) ), alpha15( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38367) {G0,W12,D3,L2,V3,M2}  { ! alpha24( X, Y, Z, skol26( X, Y, Z ) ), 
% 2.82/3.26    alpha15( X, Y, Z ) }.
% 2.82/3.26  (38368) {G0,W13,D2,L3,V5,M3}  { ! alpha24( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha31( X, Y, Z, T, U ) }.
% 2.82/3.26  (38369) {G0,W11,D3,L2,V8,M2}  { ssList( skol27( U, W, V0, V1 ) ), alpha24( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38370) {G0,W15,D3,L2,V4,M2}  { ! alpha31( X, Y, Z, T, skol27( X, Y, Z, T )
% 2.82/3.26     ), alpha24( X, Y, Z, T ) }.
% 2.82/3.26  (38371) {G0,W15,D2,L3,V6,M3}  { ! alpha31( X, Y, Z, T, U ), ! ssList( W ), 
% 2.82/3.26    alpha38( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38372) {G0,W13,D3,L2,V10,M2}  { ssList( skol28( W, V0, V1, V2, V3 ) ), 
% 2.82/3.26    alpha31( X, Y, Z, T, U ) }.
% 2.82/3.26  (38373) {G0,W18,D3,L2,V5,M2}  { ! alpha38( X, Y, Z, T, U, skol28( X, Y, Z, 
% 2.82/3.26    T, U ) ), alpha31( X, Y, Z, T, U ) }.
% 2.82/3.26  (38374) {G0,W21,D5,L3,V6,M3}  { ! alpha38( X, Y, Z, T, U, W ), ! app( app( 
% 2.82/3.26    T, cons( Y, U ) ), cons( Z, W ) ) = X, leq( Y, Z ) }.
% 2.82/3.26  (38375) {G0,W18,D5,L2,V6,M2}  { app( app( T, cons( Y, U ) ), cons( Z, W ) )
% 2.82/3.26     = X, alpha38( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38376) {G0,W10,D2,L2,V6,M2}  { ! leq( Y, Z ), alpha38( X, Y, Z, T, U, W )
% 2.82/3.26     }.
% 2.82/3.26  (38377) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! strictorderedP( X ), ! 
% 2.82/3.26    ssItem( Y ), alpha7( X, Y ) }.
% 2.82/3.26  (38378) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol29( Y ) ), 
% 2.82/3.26    strictorderedP( X ) }.
% 2.82/3.26  (38379) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha7( X, skol29( X ) ), 
% 2.82/3.26    strictorderedP( X ) }.
% 2.82/3.26  (38380) {G0,W9,D2,L3,V3,M3}  { ! alpha7( X, Y ), ! ssItem( Z ), alpha16( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38381) {G0,W7,D3,L2,V4,M2}  { ssItem( skol30( Z, T ) ), alpha7( X, Y ) }.
% 2.82/3.26  (38382) {G0,W9,D3,L2,V2,M2}  { ! alpha16( X, Y, skol30( X, Y ) ), alpha7( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38383) {G0,W11,D2,L3,V4,M3}  { ! alpha16( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha25( X, Y, Z, T ) }.
% 2.82/3.26  (38384) {G0,W9,D3,L2,V6,M2}  { ssList( skol31( T, U, W ) ), alpha16( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38385) {G0,W12,D3,L2,V3,M2}  { ! alpha25( X, Y, Z, skol31( X, Y, Z ) ), 
% 2.82/3.26    alpha16( X, Y, Z ) }.
% 2.82/3.26  (38386) {G0,W13,D2,L3,V5,M3}  { ! alpha25( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha32( X, Y, Z, T, U ) }.
% 2.82/3.26  (38387) {G0,W11,D3,L2,V8,M2}  { ssList( skol32( U, W, V0, V1 ) ), alpha25( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38388) {G0,W15,D3,L2,V4,M2}  { ! alpha32( X, Y, Z, T, skol32( X, Y, Z, T )
% 2.82/3.26     ), alpha25( X, Y, Z, T ) }.
% 2.82/3.26  (38389) {G0,W15,D2,L3,V6,M3}  { ! alpha32( X, Y, Z, T, U ), ! ssList( W ), 
% 2.82/3.26    alpha39( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38390) {G0,W13,D3,L2,V10,M2}  { ssList( skol33( W, V0, V1, V2, V3 ) ), 
% 2.82/3.26    alpha32( X, Y, Z, T, U ) }.
% 2.82/3.26  (38391) {G0,W18,D3,L2,V5,M2}  { ! alpha39( X, Y, Z, T, U, skol33( X, Y, Z, 
% 2.82/3.26    T, U ) ), alpha32( X, Y, Z, T, U ) }.
% 2.82/3.26  (38392) {G0,W21,D5,L3,V6,M3}  { ! alpha39( X, Y, Z, T, U, W ), ! app( app( 
% 2.82/3.26    T, cons( Y, U ) ), cons( Z, W ) ) = X, lt( Y, Z ) }.
% 2.82/3.26  (38393) {G0,W18,D5,L2,V6,M2}  { app( app( T, cons( Y, U ) ), cons( Z, W ) )
% 2.82/3.26     = X, alpha39( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38394) {G0,W10,D2,L2,V6,M2}  { ! lt( Y, Z ), alpha39( X, Y, Z, T, U, W )
% 2.82/3.26     }.
% 2.82/3.26  (38395) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! duplicatefreeP( X ), ! 
% 2.82/3.26    ssItem( Y ), alpha8( X, Y ) }.
% 2.82/3.26  (38396) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol34( Y ) ), 
% 2.82/3.26    duplicatefreeP( X ) }.
% 2.82/3.26  (38397) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha8( X, skol34( X ) ), 
% 2.82/3.26    duplicatefreeP( X ) }.
% 2.82/3.26  (38398) {G0,W9,D2,L3,V3,M3}  { ! alpha8( X, Y ), ! ssItem( Z ), alpha17( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38399) {G0,W7,D3,L2,V4,M2}  { ssItem( skol35( Z, T ) ), alpha8( X, Y ) }.
% 2.82/3.26  (38400) {G0,W9,D3,L2,V2,M2}  { ! alpha17( X, Y, skol35( X, Y ) ), alpha8( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38401) {G0,W11,D2,L3,V4,M3}  { ! alpha17( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha26( X, Y, Z, T ) }.
% 2.82/3.26  (38402) {G0,W9,D3,L2,V6,M2}  { ssList( skol36( T, U, W ) ), alpha17( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38403) {G0,W12,D3,L2,V3,M2}  { ! alpha26( X, Y, Z, skol36( X, Y, Z ) ), 
% 2.82/3.26    alpha17( X, Y, Z ) }.
% 2.82/3.26  (38404) {G0,W13,D2,L3,V5,M3}  { ! alpha26( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha33( X, Y, Z, T, U ) }.
% 2.82/3.26  (38405) {G0,W11,D3,L2,V8,M2}  { ssList( skol37( U, W, V0, V1 ) ), alpha26( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38406) {G0,W15,D3,L2,V4,M2}  { ! alpha33( X, Y, Z, T, skol37( X, Y, Z, T )
% 2.82/3.26     ), alpha26( X, Y, Z, T ) }.
% 2.82/3.26  (38407) {G0,W15,D2,L3,V6,M3}  { ! alpha33( X, Y, Z, T, U ), ! ssList( W ), 
% 2.82/3.26    alpha40( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38408) {G0,W13,D3,L2,V10,M2}  { ssList( skol38( W, V0, V1, V2, V3 ) ), 
% 2.82/3.26    alpha33( X, Y, Z, T, U ) }.
% 2.82/3.26  (38409) {G0,W18,D3,L2,V5,M2}  { ! alpha40( X, Y, Z, T, U, skol38( X, Y, Z, 
% 2.82/3.26    T, U ) ), alpha33( X, Y, Z, T, U ) }.
% 2.82/3.26  (38410) {G0,W21,D5,L3,V6,M3}  { ! alpha40( X, Y, Z, T, U, W ), ! app( app( 
% 2.82/3.26    T, cons( Y, U ) ), cons( Z, W ) ) = X, ! Y = Z }.
% 2.82/3.26  (38411) {G0,W18,D5,L2,V6,M2}  { app( app( T, cons( Y, U ) ), cons( Z, W ) )
% 2.82/3.26     = X, alpha40( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38412) {G0,W10,D2,L2,V6,M2}  { Y = Z, alpha40( X, Y, Z, T, U, W ) }.
% 2.82/3.26  (38413) {G0,W9,D2,L4,V2,M4}  { ! ssList( X ), ! equalelemsP( X ), ! ssItem
% 2.82/3.26    ( Y ), alpha9( X, Y ) }.
% 2.82/3.26  (38414) {G0,W7,D3,L3,V2,M3}  { ! ssList( X ), ssItem( skol39( Y ) ), 
% 2.82/3.26    equalelemsP( X ) }.
% 2.82/3.26  (38415) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), ! alpha9( X, skol39( X ) ), 
% 2.82/3.26    equalelemsP( X ) }.
% 2.82/3.26  (38416) {G0,W9,D2,L3,V3,M3}  { ! alpha9( X, Y ), ! ssItem( Z ), alpha18( X
% 2.82/3.26    , Y, Z ) }.
% 2.82/3.26  (38417) {G0,W7,D3,L2,V4,M2}  { ssItem( skol40( Z, T ) ), alpha9( X, Y ) }.
% 2.82/3.26  (38418) {G0,W9,D3,L2,V2,M2}  { ! alpha18( X, Y, skol40( X, Y ) ), alpha9( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38419) {G0,W11,D2,L3,V4,M3}  { ! alpha18( X, Y, Z ), ! ssList( T ), 
% 2.82/3.26    alpha27( X, Y, Z, T ) }.
% 2.82/3.26  (38420) {G0,W9,D3,L2,V6,M2}  { ssList( skol41( T, U, W ) ), alpha18( X, Y, 
% 2.82/3.26    Z ) }.
% 2.82/3.26  (38421) {G0,W12,D3,L2,V3,M2}  { ! alpha27( X, Y, Z, skol41( X, Y, Z ) ), 
% 2.82/3.26    alpha18( X, Y, Z ) }.
% 2.82/3.26  (38422) {G0,W13,D2,L3,V5,M3}  { ! alpha27( X, Y, Z, T ), ! ssList( U ), 
% 2.82/3.26    alpha34( X, Y, Z, T, U ) }.
% 2.82/3.26  (38423) {G0,W11,D3,L2,V8,M2}  { ssList( skol42( U, W, V0, V1 ) ), alpha27( 
% 2.82/3.26    X, Y, Z, T ) }.
% 2.82/3.26  (38424) {G0,W15,D3,L2,V4,M2}  { ! alpha34( X, Y, Z, T, skol42( X, Y, Z, T )
% 2.82/3.26     ), alpha27( X, Y, Z, T ) }.
% 2.82/3.26  (38425) {G0,W18,D5,L3,V5,M3}  { ! alpha34( X, Y, Z, T, U ), ! app( T, cons
% 2.82/3.26    ( Y, cons( Z, U ) ) ) = X, Y = Z }.
% 2.82/3.26  (38426) {G0,W15,D5,L2,V5,M2}  { app( T, cons( Y, cons( Z, U ) ) ) = X, 
% 2.82/3.26    alpha34( X, Y, Z, T, U ) }.
% 2.82/3.26  (38427) {G0,W9,D2,L2,V5,M2}  { ! Y = Z, alpha34( X, Y, Z, T, U ) }.
% 2.82/3.26  (38428) {G0,W10,D2,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), ! neq( X, Y )
% 2.82/3.26    , ! X = Y }.
% 2.82/3.26  (38429) {G0,W10,D2,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), X = Y, neq( X
% 2.82/3.26    , Y ) }.
% 2.82/3.26  (38430) {G0,W8,D3,L3,V2,M3}  { ! ssList( X ), ! ssItem( Y ), ssList( cons( 
% 2.82/3.26    Y, X ) ) }.
% 2.82/3.26  (38431) {G0,W2,D2,L1,V0,M1}  { ssList( nil ) }.
% 2.82/3.26  (38432) {G0,W9,D3,L3,V2,M3}  { ! ssList( X ), ! ssItem( Y ), ! cons( Y, X )
% 2.82/3.26     = X }.
% 2.82/3.26  (38433) {G0,W18,D3,L6,V4,M6}  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z )
% 2.82/3.26    , ! ssItem( T ), ! cons( Z, X ) = cons( T, Y ), Z = T }.
% 2.82/3.26  (38434) {G0,W18,D3,L6,V4,M6}  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z )
% 2.82/3.26    , ! ssItem( T ), ! cons( Z, X ) = cons( T, Y ), Y = X }.
% 2.82/3.26  (38435) {G0,W8,D3,L3,V2,M3}  { ! ssList( X ), nil = X, ssList( skol43( Y )
% 2.82/3.26     ) }.
% 2.82/3.26  (38436) {G0,W8,D3,L3,V2,M3}  { ! ssList( X ), nil = X, ssItem( skol49( Y )
% 2.82/3.26     ) }.
% 2.82/3.26  (38437) {G0,W12,D4,L3,V1,M3}  { ! ssList( X ), nil = X, cons( skol49( X ), 
% 2.82/3.26    skol43( X ) ) = X }.
% 2.82/3.26  (38438) {G0,W9,D3,L3,V2,M3}  { ! ssList( X ), ! ssItem( Y ), ! nil = cons( 
% 2.82/3.26    Y, X ) }.
% 2.82/3.26  (38439) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), nil = X, ssItem( hd( X ) )
% 2.82/3.26     }.
% 2.82/3.26  (38440) {G0,W10,D4,L3,V2,M3}  { ! ssList( X ), ! ssItem( Y ), hd( cons( Y, 
% 2.82/3.26    X ) ) = Y }.
% 2.82/3.26  (38441) {G0,W8,D3,L3,V1,M3}  { ! ssList( X ), nil = X, ssList( tl( X ) )
% 2.82/3.26     }.
% 2.82/3.26  (38442) {G0,W10,D4,L3,V2,M3}  { ! ssList( X ), ! ssItem( Y ), tl( cons( Y, 
% 2.82/3.26    X ) ) = X }.
% 2.82/3.26  (38443) {G0,W8,D3,L3,V2,M3}  { ! ssList( X ), ! ssList( Y ), ssList( app( X
% 2.82/3.26    , Y ) ) }.
% 2.82/3.26  (38444) {G0,W17,D4,L4,V3,M4}  { ! ssList( X ), ! ssList( Y ), ! ssItem( Z )
% 2.82/3.26    , cons( Z, app( Y, X ) ) = app( cons( Z, Y ), X ) }.
% 2.82/3.26  (38445) {G0,W7,D3,L2,V1,M2}  { ! ssList( X ), app( nil, X ) = X }.
% 2.82/3.26  (38446) {G0,W13,D2,L5,V2,M5}  { ! ssItem( X ), ! ssItem( Y ), ! leq( X, Y )
% 2.82/3.26    , ! leq( Y, X ), X = Y }.
% 2.82/3.26  (38447) {G0,W15,D2,L6,V3,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z )
% 2.82/3.26    , ! leq( X, Y ), ! leq( Y, Z ), leq( X, Z ) }.
% 2.82/3.26  (38448) {G0,W5,D2,L2,V1,M2}  { ! ssItem( X ), leq( X, X ) }.
% 2.82/3.26  (38449) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! geq( X, Y )
% 2.82/3.26    , leq( Y, X ) }.
% 2.82/3.26  (38450) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! leq( Y, X )
% 2.82/3.26    , geq( X, Y ) }.
% 2.82/3.26  (38451) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y )
% 2.82/3.26    , ! lt( Y, X ) }.
% 2.82/3.26  (38452) {G0,W15,D2,L6,V3,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z )
% 2.82/3.26    , ! lt( X, Y ), ! lt( Y, Z ), lt( X, Z ) }.
% 2.82/3.26  (38453) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! gt( X, Y )
% 2.82/3.26    , lt( Y, X ) }.
% 2.82/3.26  (38454) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! lt( Y, X )
% 2.82/3.26    , gt( X, Y ) }.
% 2.82/3.26  (38455) {G0,W17,D3,L6,V3,M6}  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! memberP( app( Y, Z ), X ), memberP( Y, X ), memberP( Z, X ) }.
% 2.82/3.26  (38456) {G0,W14,D3,L5,V3,M5}  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! memberP( Y, X ), memberP( app( Y, Z ), X ) }.
% 2.82/3.26  (38457) {G0,W14,D3,L5,V3,M5}  { ! ssItem( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! memberP( Z, X ), memberP( app( Y, Z ), X ) }.
% 2.82/3.26  (38458) {G0,W17,D3,L6,V3,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! memberP( cons( Y, Z ), X ), X = Y, memberP( Z, X ) }.
% 2.82/3.26  (38459) {G0,W14,D3,L5,V3,M5}  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! X = Y, memberP( cons( Y, Z ), X ) }.
% 2.82/3.26  (38460) {G0,W14,D3,L5,V3,M5}  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! memberP( Z, X ), memberP( cons( Y, Z ), X ) }.
% 2.82/3.26  (38461) {G0,W5,D2,L2,V1,M2}  { ! ssItem( X ), ! memberP( nil, X ) }.
% 2.82/3.26  (38462) {G0,W2,D2,L1,V0,M1}  { ! singletonP( nil ) }.
% 2.82/3.26  (38463) {G0,W15,D2,L6,V3,M6}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! frontsegP( X, Y ), ! frontsegP( Y, Z ), frontsegP( X, Z ) }.
% 2.82/3.26  (38464) {G0,W13,D2,L5,V2,M5}  { ! ssList( X ), ! ssList( Y ), ! frontsegP( 
% 2.82/3.26    X, Y ), ! frontsegP( Y, X ), X = Y }.
% 2.82/3.26  (38465) {G0,W5,D2,L2,V1,M2}  { ! ssList( X ), frontsegP( X, X ) }.
% 2.82/3.26  (38466) {G0,W14,D3,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! frontsegP( X, Y ), frontsegP( app( X, Z ), Y ) }.
% 2.82/3.26  (38467) {G0,W18,D3,L6,V4,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! ssList( T ), ! frontsegP( cons( X, Z ), cons( Y, T ) ), X = Y }.
% 2.82/3.26  (38468) {G0,W18,D3,L6,V4,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! ssList( T ), ! frontsegP( cons( X, Z ), cons( Y, T ) ), frontsegP( Z
% 2.82/3.26    , T ) }.
% 2.82/3.26  (38469) {G0,W21,D3,L7,V4,M7}  { ! ssItem( X ), ! ssItem( Y ), ! ssList( Z )
% 2.82/3.26    , ! ssList( T ), ! X = Y, ! frontsegP( Z, T ), frontsegP( cons( X, Z ), 
% 2.82/3.26    cons( Y, T ) ) }.
% 2.82/3.26  (38470) {G0,W5,D2,L2,V1,M2}  { ! ssList( X ), frontsegP( X, nil ) }.
% 2.82/3.26  (38471) {G0,W8,D2,L3,V1,M3}  { ! ssList( X ), ! frontsegP( nil, X ), nil = 
% 2.82/3.26    X }.
% 2.82/3.26  (38472) {G0,W8,D2,L3,V1,M3}  { ! ssList( X ), ! nil = X, frontsegP( nil, X
% 2.82/3.26     ) }.
% 2.82/3.26  (38473) {G0,W15,D2,L6,V3,M6}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! rearsegP( X, Y ), ! rearsegP( Y, Z ), rearsegP( X, Z ) }.
% 2.82/3.26  (38474) {G0,W13,D2,L5,V2,M5}  { ! ssList( X ), ! ssList( Y ), ! rearsegP( X
% 2.82/3.26    , Y ), ! rearsegP( Y, X ), X = Y }.
% 2.82/3.26  (38475) {G0,W5,D2,L2,V1,M2}  { ! ssList( X ), rearsegP( X, X ) }.
% 2.82/3.26  (38476) {G0,W14,D3,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! rearsegP( X, Y ), rearsegP( app( Z, X ), Y ) }.
% 2.82/3.26  (38477) {G0,W5,D2,L2,V1,M2}  { ! ssList( X ), rearsegP( X, nil ) }.
% 2.82/3.26  (38478) {G0,W8,D2,L3,V1,M3}  { ! ssList( X ), ! rearsegP( nil, X ), nil = X
% 2.82/3.26     }.
% 2.82/3.26  (38479) {G0,W8,D2,L3,V1,M3}  { ! ssList( X ), ! nil = X, rearsegP( nil, X )
% 2.82/3.26     }.
% 2.82/3.26  (38480) {G0,W15,D2,L6,V3,M6}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! segmentP( X, Y ), ! segmentP( Y, Z ), segmentP( X, Z ) }.
% 2.82/3.26  (38481) {G0,W13,D2,L5,V2,M5}  { ! ssList( X ), ! ssList( Y ), ! segmentP( X
% 2.82/3.26    , Y ), ! segmentP( Y, X ), X = Y }.
% 2.82/3.26  (38482) {G0,W5,D2,L2,V1,M2}  { ! ssList( X ), segmentP( X, X ) }.
% 2.82/3.26  (38483) {G0,W18,D4,L6,V4,M6}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.26    , ! ssList( T ), ! segmentP( X, Y ), segmentP( app( app( Z, X ), T ), Y )
% 2.82/3.26     }.
% 2.82/3.26  (38484) {G0,W5,D2,L2,V1,M2}  { ! ssList( X ), segmentP( X, nil ) }.
% 2.82/3.26  (38485) {G0,W8,D2,L3,V1,M3}  { ! ssList( X ), ! segmentP( nil, X ), nil = X
% 2.82/3.26     }.
% 2.82/3.26  (38486) {G0,W8,D2,L3,V1,M3}  { ! ssList( X ), ! nil = X, segmentP( nil, X )
% 2.82/3.26     }.
% 2.82/3.26  (38487) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), cyclefreeP( cons( X, nil ) )
% 2.82/3.26     }.
% 2.82/3.26  (38488) {G0,W2,D2,L1,V0,M1}  { cyclefreeP( nil ) }.
% 2.82/3.26  (38489) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), totalorderP( cons( X, nil ) )
% 2.82/3.26     }.
% 2.82/3.26  (38490) {G0,W2,D2,L1,V0,M1}  { totalorderP( nil ) }.
% 2.82/3.26  (38491) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), strictorderP( cons( X, nil )
% 2.82/3.26     ) }.
% 2.82/3.26  (38492) {G0,W2,D2,L1,V0,M1}  { strictorderP( nil ) }.
% 2.82/3.26  (38493) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), totalorderedP( cons( X, nil )
% 2.82/3.26     ) }.
% 2.82/3.26  (38494) {G0,W2,D2,L1,V0,M1}  { totalorderedP( nil ) }.
% 2.82/3.26  (38495) {G0,W14,D3,L5,V2,M5}  { ! ssItem( X ), ! ssList( Y ), ! 
% 2.82/3.26    totalorderedP( cons( X, Y ) ), nil = Y, alpha10( X, Y ) }.
% 2.82/3.26  (38496) {G0,W11,D3,L4,V2,M4}  { ! ssItem( X ), ! ssList( Y ), ! nil = Y, 
% 2.82/3.26    totalorderedP( cons( X, Y ) ) }.
% 2.82/3.26  (38497) {G0,W11,D3,L4,V2,M4}  { ! ssItem( X ), ! ssList( Y ), ! alpha10( X
% 2.82/3.26    , Y ), totalorderedP( cons( X, Y ) ) }.
% 2.82/3.26  (38498) {G0,W6,D2,L2,V2,M2}  { ! alpha10( X, Y ), ! nil = Y }.
% 2.82/3.26  (38499) {G0,W6,D2,L2,V2,M2}  { ! alpha10( X, Y ), alpha19( X, Y ) }.
% 2.82/3.26  (38500) {G0,W9,D2,L3,V2,M3}  { nil = Y, ! alpha19( X, Y ), alpha10( X, Y )
% 2.82/3.26     }.
% 2.82/3.26  (38501) {G0,W5,D2,L2,V2,M2}  { ! alpha19( X, Y ), totalorderedP( Y ) }.
% 2.82/3.26  (38502) {G0,W7,D3,L2,V2,M2}  { ! alpha19( X, Y ), leq( X, hd( Y ) ) }.
% 2.82/3.26  (38503) {G0,W9,D3,L3,V2,M3}  { ! totalorderedP( Y ), ! leq( X, hd( Y ) ), 
% 2.82/3.26    alpha19( X, Y ) }.
% 2.82/3.26  (38504) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), strictorderedP( cons( X, nil
% 2.82/3.26     ) ) }.
% 2.82/3.26  (38505) {G0,W2,D2,L1,V0,M1}  { strictorderedP( nil ) }.
% 2.82/3.26  (38506) {G0,W14,D3,L5,V2,M5}  { ! ssItem( X ), ! ssList( Y ), ! 
% 2.82/3.26    strictorderedP( cons( X, Y ) ), nil = Y, alpha11( X, Y ) }.
% 2.82/3.26  (38507) {G0,W11,D3,L4,V2,M4}  { ! ssItem( X ), ! ssList( Y ), ! nil = Y, 
% 2.82/3.26    strictorderedP( cons( X, Y ) ) }.
% 2.82/3.26  (38508) {G0,W11,D3,L4,V2,M4}  { ! ssItem( X ), ! ssList( Y ), ! alpha11( X
% 2.82/3.26    , Y ), strictorderedP( cons( X, Y ) ) }.
% 2.82/3.26  (38509) {G0,W6,D2,L2,V2,M2}  { ! alpha11( X, Y ), ! nil = Y }.
% 2.82/3.26  (38510) {G0,W6,D2,L2,V2,M2}  { ! alpha11( X, Y ), alpha20( X, Y ) }.
% 2.82/3.26  (38511) {G0,W9,D2,L3,V2,M3}  { nil = Y, ! alpha20( X, Y ), alpha11( X, Y )
% 2.82/3.26     }.
% 2.82/3.26  (38512) {G0,W5,D2,L2,V2,M2}  { ! alpha20( X, Y ), strictorderedP( Y ) }.
% 2.82/3.26  (38513) {G0,W7,D3,L2,V2,M2}  { ! alpha20( X, Y ), lt( X, hd( Y ) ) }.
% 2.82/3.26  (38514) {G0,W9,D3,L3,V2,M3}  { ! strictorderedP( Y ), ! lt( X, hd( Y ) ), 
% 2.82/3.26    alpha20( X, Y ) }.
% 2.82/3.26  (38515) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), duplicatefreeP( cons( X, nil
% 2.82/3.26     ) ) }.
% 2.82/3.26  (38516) {G0,W2,D2,L1,V0,M1}  { duplicatefreeP( nil ) }.
% 2.82/3.26  (38517) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), equalelemsP( cons( X, nil ) )
% 2.82/3.26     }.
% 2.82/3.26  (38518) {G0,W2,D2,L1,V0,M1}  { equalelemsP( nil ) }.
% 2.82/3.26  (38519) {G0,W8,D3,L3,V2,M3}  { ! ssList( X ), nil = X, ssItem( skol44( Y )
% 2.82/3.26     ) }.
% 2.82/3.26  (38520) {G0,W10,D3,L3,V1,M3}  { ! ssList( X ), nil = X, hd( X ) = skol44( X
% 2.82/3.26     ) }.
% 2.82/3.26  (38521) {G0,W8,D3,L3,V2,M3}  { ! ssList( X ), nil = X, ssList( skol45( Y )
% 2.82/3.26     ) }.
% 2.82/3.26  (38522) {G0,W10,D3,L3,V1,M3}  { ! ssList( X ), nil = X, tl( X ) = skol45( X
% 2.82/3.26     ) }.
% 2.82/3.26  (38523) {G0,W23,D3,L7,V2,M7}  { ! ssList( X ), ! ssList( Y ), nil = Y, nil 
% 2.82/3.26    = X, ! hd( Y ) = hd( X ), ! tl( Y ) = tl( X ), Y = X }.
% 2.82/3.26  (38524) {G0,W12,D4,L3,V1,M3}  { ! ssList( X ), nil = X, cons( hd( X ), tl( 
% 2.82/3.26    X ) ) = X }.
% 2.82/3.26  (38525) {G0,W16,D3,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.27    , ! app( Z, Y ) = app( X, Y ), Z = X }.
% 2.82/3.27  (38526) {G0,W16,D3,L5,V3,M5}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.27    , ! app( Y, Z ) = app( Y, X ), Z = X }.
% 2.82/3.27  (38527) {G0,W13,D4,L3,V2,M3}  { ! ssList( X ), ! ssItem( Y ), cons( Y, X ) 
% 2.82/3.27    = app( cons( Y, nil ), X ) }.
% 2.82/3.27  (38528) {G0,W17,D4,L4,V3,M4}  { ! ssList( X ), ! ssList( Y ), ! ssList( Z )
% 2.82/3.27    , app( app( X, Y ), Z ) = app( X, app( Y, Z ) ) }.
% 2.82/3.27  (38529) {G0,W12,D3,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), ! nil = app( 
% 2.82/3.27    X, Y ), nil = Y }.
% 2.82/3.27  (38530) {G0,W12,D3,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), ! nil = app( 
% 2.82/3.27    X, Y ), nil = X }.
% 2.82/3.27  (38531) {G0,W15,D3,L5,V2,M5}  { ! ssList( X ), ! ssList( Y ), ! nil = Y, ! 
% 2.82/3.27    nil = X, nil = app( X, Y ) }.
% 2.82/3.27  (38532) {G0,W7,D3,L2,V1,M2}  { ! ssList( X ), app( X, nil ) = X }.
% 2.82/3.27  (38533) {G0,W14,D4,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), nil = X, hd( 
% 2.82/3.27    app( X, Y ) ) = hd( X ) }.
% 2.82/3.27  (38534) {G0,W16,D4,L4,V2,M4}  { ! ssList( X ), ! ssList( Y ), nil = X, tl( 
% 2.82/3.27    app( X, Y ) ) = app( tl( X ), Y ) }.
% 2.82/3.27  (38535) {G0,W13,D2,L5,V2,M5}  { ! ssItem( X ), ! ssItem( Y ), ! geq( X, Y )
% 2.82/3.27    , ! geq( Y, X ), X = Y }.
% 2.82/3.27  (38536) {G0,W15,D2,L6,V3,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z )
% 2.82/3.27    , ! geq( X, Y ), ! geq( Y, Z ), geq( X, Z ) }.
% 2.82/3.27  (38537) {G0,W5,D2,L2,V1,M2}  { ! ssItem( X ), geq( X, X ) }.
% 2.82/3.27  (38538) {G0,W5,D2,L2,V1,M2}  { ! ssItem( X ), ! lt( X, X ) }.
% 2.82/3.27  (38539) {G0,W15,D2,L6,V3,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z )
% 2.82/3.27    , ! leq( X, Y ), ! lt( Y, Z ), lt( X, Z ) }.
% 2.82/3.27  (38540) {G0,W13,D2,L5,V2,M5}  { ! ssItem( X ), ! ssItem( Y ), ! leq( X, Y )
% 2.82/3.27    , X = Y, lt( X, Y ) }.
% 2.82/3.27  (38541) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y )
% 2.82/3.27    , ! X = Y }.
% 2.82/3.27  (38542) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! lt( X, Y )
% 2.82/3.27    , leq( X, Y ) }.
% 2.82/3.27  (38543) {G0,W13,D2,L5,V2,M5}  { ! ssItem( X ), ! ssItem( Y ), X = Y, ! leq
% 2.82/3.27    ( X, Y ), lt( X, Y ) }.
% 2.82/3.27  (38544) {G0,W10,D2,L4,V2,M4}  { ! ssItem( X ), ! ssItem( Y ), ! gt( X, Y )
% 2.82/3.27    , ! gt( Y, X ) }.
% 2.82/3.27  (38545) {G0,W15,D2,L6,V3,M6}  { ! ssItem( X ), ! ssItem( Y ), ! ssItem( Z )
% 2.82/3.27    , ! gt( X, Y ), ! gt( Y, Z ), gt( X, Z ) }.
% 2.82/3.27  (38546) {G0,W2,D2,L1,V0,M1}  { ssList( skol46 ) }.
% 2.82/3.27  (38547) {G0,W2,D2,L1,V0,M1}  { ssList( skol50 ) }.
% 2.82/3.27  (38548) {G0,W2,D2,L1,V0,M1}  { ssList( skol51 ) }.
% 2.82/3.27  (38549) {G0,W2,D2,L1,V0,M1}  { ssList( skol52 ) }.
% 2.82/3.27  (38550) {G0,W3,D2,L1,V0,M1}  { skol50 = skol52 }.
% 2.82/3.27  (38551) {G0,W3,D2,L1,V0,M1}  { skol46 = skol51 }.
% 2.82/3.27  (38552) {G0,W2,D2,L1,V0,M1}  { ! totalorderedP( skol46 ) }.
% 2.82/3.27  (38553) {G0,W5,D2,L2,V0,M2}  { ssItem( skol53 ), alpha44( skol51, skol52 )
% 2.82/3.27     }.
% 2.82/3.27  (38554) {G0,W5,D2,L2,V0,M2}  { ssList( skol54 ), alpha44( skol51, skol52 )
% 2.82/3.27     }.
% 2.82/3.27  (38555) {G0,W9,D2,L2,V0,M2}  { alpha46( skol51, skol52, skol53, skol54, 
% 2.82/3.27    skol55 ), alpha44( skol51, skol52 ) }.
% 2.82/3.27  (38556) {G0,W11,D2,L4,V1,M4}  { ! ssItem( X ), ! memberP( skol55, X ), ! lt
% 2.82/3.27    ( X, skol53 ), alpha44( skol51, skol52 ) }.
% 2.82/3.27  (38557) {G0,W10,D2,L2,V5,M2}  { ! alpha46( X, Y, Z, T, U ), alpha45( X, Z, 
% 2.82/3.27    U ) }.
% 2.82/3.27  (38558) {G0,W13,D4,L2,V5,M2}  { ! alpha46( X, Y, Z, T, U ), app( app( T, X
% 2.82/3.27     ), U ) = Y }.
% 2.82/3.27  (38559) {G0,W9,D2,L2,V5,M2}  { ! alpha46( X, Y, Z, T, U ), alpha47( Z, T )
% 2.82/3.27     }.
% 2.82/3.27  (38560) {G0,W20,D4,L4,V5,M4}  { ! alpha45( X, Z, U ), ! app( app( T, X ), U
% 2.82/3.27     ) = Y, ! alpha47( Z, T ), alpha46( X, Y, Z, T, U ) }.
% 2.82/3.27  (38561) {G0,W11,D2,L4,V3,M4}  { ! alpha47( X, Y ), ! ssItem( Z ), ! memberP
% 2.82/3.27    ( Y, Z ), ! lt( X, Z ) }.
% 2.82/3.27  (38562) {G0,W7,D3,L2,V4,M2}  { ssItem( skol47( Z, T ) ), alpha47( X, Y )
% 2.82/3.27     }.
% 2.82/3.27  (38563) {G0,W8,D3,L2,V3,M2}  { memberP( Y, skol47( Z, Y ) ), alpha47( X, Y
% 2.82/3.27     ) }.
% 2.82/3.27  (38564) {G0,W8,D3,L2,V2,M2}  { lt( X, skol47( X, Y ) ), alpha47( X, Y ) }.
% 2.82/3.27  (38565) {G0,W6,D2,L2,V3,M2}  { ! alpha45( X, Y, Z ), ssList( Z ) }.
% 2.82/3.27  (38566) {G0,W9,D3,L2,V3,M2}  { ! alpha45( X, Y, Z ), cons( Y, nil ) = X }.
% 2.82/3.27  (38567) {G0,W11,D3,L3,V3,M3}  { ! ssList( Z ), ! cons( Y, nil ) = X, 
% 2.82/3.27    alpha45( X, Y, Z ) }.
% 2.82/3.27  (38568) {G0,W6,D2,L2,V2,M2}  { ! alpha44( X, Y ), nil = Y }.
% 2.82/3.27  (38569) {G0,W6,D2,L2,V2,M2}  { ! alpha44( X, Y ), nil = X }.
% 2.82/3.27  (38570) {G0,W9,D2,L3,V2,M3}  { ! nil = Y, ! nil = X, alpha44( X, Y ) }.
% 2.82/3.27  
% 2.82/3.27  
% 2.82/3.27  Total Proof:
% 2.82/3.27  
% 2.82/3.27  subsumption: (223) {G0,W6,D3,L2,V1,M2} I { ! ssItem( X ), totalorderedP( 
% 2.82/3.28    cons( X, nil ) ) }.
% 2.82/3.28  parent0: (38493) {G0,W6,D3,L2,V1,M2}  { ! ssItem( X ), totalorderedP( cons
% 2.82/3.28    ( X, nil ) ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28     1 ==> 1
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (224) {G0,W2,D2,L1,V0,M1} I { totalorderedP( nil ) }.
% 2.82/3.28  parent0: (38494) {G0,W2,D2,L1,V0,M1}  { totalorderedP( nil ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  eqswap: (39311) {G0,W3,D2,L1,V0,M1}  { skol52 = skol50 }.
% 2.82/3.28  parent0[0]: (38550) {G0,W3,D2,L1,V0,M1}  { skol50 = skol52 }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (279) {G0,W3,D2,L1,V0,M1} I { skol52 ==> skol50 }.
% 2.82/3.28  parent0: (39311) {G0,W3,D2,L1,V0,M1}  { skol52 = skol50 }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  eqswap: (39659) {G0,W3,D2,L1,V0,M1}  { skol51 = skol46 }.
% 2.82/3.28  parent0[0]: (38551) {G0,W3,D2,L1,V0,M1}  { skol46 = skol51 }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (280) {G0,W3,D2,L1,V0,M1} I { skol51 ==> skol46 }.
% 2.82/3.28  parent0: (39659) {G0,W3,D2,L1,V0,M1}  { skol51 = skol46 }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (281) {G0,W2,D2,L1,V0,M1} I { ! totalorderedP( skol46 ) }.
% 2.82/3.28  parent0: (38552) {G0,W2,D2,L1,V0,M1}  { ! totalorderedP( skol46 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (40934) {G1,W5,D2,L2,V0,M2}  { alpha44( skol46, skol52 ), ssItem( 
% 2.82/3.28    skol53 ) }.
% 2.82/3.28  parent0[0]: (280) {G0,W3,D2,L1,V0,M1} I { skol51 ==> skol46 }.
% 2.82/3.28  parent1[1; 1]: (38553) {G0,W5,D2,L2,V0,M2}  { ssItem( skol53 ), alpha44( 
% 2.82/3.28    skol51, skol52 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (40935) {G1,W5,D2,L2,V0,M2}  { alpha44( skol46, skol50 ), ssItem( 
% 2.82/3.28    skol53 ) }.
% 2.82/3.28  parent0[0]: (279) {G0,W3,D2,L1,V0,M1} I { skol52 ==> skol50 }.
% 2.82/3.28  parent1[0; 2]: (40934) {G1,W5,D2,L2,V0,M2}  { alpha44( skol46, skol52 ), 
% 2.82/3.28    ssItem( skol53 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (282) {G1,W5,D2,L2,V0,M2} I;d(280);d(279) { ssItem( skol53 ), 
% 2.82/3.28    alpha44( skol46, skol50 ) }.
% 2.82/3.28  parent0: (40935) {G1,W5,D2,L2,V0,M2}  { alpha44( skol46, skol50 ), ssItem( 
% 2.82/3.28    skol53 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 1
% 2.82/3.28     1 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (42441) {G1,W9,D2,L2,V0,M2}  { alpha44( skol46, skol52 ), alpha46
% 2.82/3.28    ( skol51, skol52, skol53, skol54, skol55 ) }.
% 2.82/3.28  parent0[0]: (280) {G0,W3,D2,L1,V0,M1} I { skol51 ==> skol46 }.
% 2.82/3.28  parent1[1; 1]: (38555) {G0,W9,D2,L2,V0,M2}  { alpha46( skol51, skol52, 
% 2.82/3.28    skol53, skol54, skol55 ), alpha44( skol51, skol52 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (42443) {G1,W9,D2,L2,V0,M2}  { alpha46( skol46, skol52, skol53, 
% 2.82/3.28    skol54, skol55 ), alpha44( skol46, skol52 ) }.
% 2.82/3.28  parent0[0]: (280) {G0,W3,D2,L1,V0,M1} I { skol51 ==> skol46 }.
% 2.82/3.28  parent1[1; 1]: (42441) {G1,W9,D2,L2,V0,M2}  { alpha44( skol46, skol52 ), 
% 2.82/3.28    alpha46( skol51, skol52, skol53, skol54, skol55 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (42445) {G1,W9,D2,L2,V0,M2}  { alpha44( skol46, skol50 ), alpha46
% 2.82/3.28    ( skol46, skol52, skol53, skol54, skol55 ) }.
% 2.82/3.28  parent0[0]: (279) {G0,W3,D2,L1,V0,M1} I { skol52 ==> skol50 }.
% 2.82/3.28  parent1[1; 2]: (42443) {G1,W9,D2,L2,V0,M2}  { alpha46( skol46, skol52, 
% 2.82/3.28    skol53, skol54, skol55 ), alpha44( skol46, skol52 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (42447) {G1,W9,D2,L2,V0,M2}  { alpha46( skol46, skol50, skol53, 
% 2.82/3.28    skol54, skol55 ), alpha44( skol46, skol50 ) }.
% 2.82/3.28  parent0[0]: (279) {G0,W3,D2,L1,V0,M1} I { skol52 ==> skol50 }.
% 2.82/3.28  parent1[1; 2]: (42445) {G1,W9,D2,L2,V0,M2}  { alpha44( skol46, skol50 ), 
% 2.82/3.28    alpha46( skol46, skol52, skol53, skol54, skol55 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (284) {G1,W9,D2,L2,V0,M2} I;d(280);d(280);d(279);d(279) { 
% 2.82/3.28    alpha46( skol46, skol50, skol53, skol54, skol55 ), alpha44( skol46, 
% 2.82/3.28    skol50 ) }.
% 2.82/3.28  parent0: (42447) {G1,W9,D2,L2,V0,M2}  { alpha46( skol46, skol50, skol53, 
% 2.82/3.28    skol54, skol55 ), alpha44( skol46, skol50 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28     1 ==> 1
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (286) {G0,W10,D2,L2,V5,M2} I { ! alpha46( X, Y, Z, T, U ), 
% 2.82/3.28    alpha45( X, Z, U ) }.
% 2.82/3.28  parent0: (38557) {G0,W10,D2,L2,V5,M2}  { ! alpha46( X, Y, Z, T, U ), 
% 2.82/3.28    alpha45( X, Z, U ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28     Y := Y
% 2.82/3.28     Z := Z
% 2.82/3.28     T := T
% 2.82/3.28     U := U
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28     1 ==> 1
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (295) {G0,W9,D3,L2,V3,M2} I { ! alpha45( X, Y, Z ), cons( Y, 
% 2.82/3.28    nil ) = X }.
% 2.82/3.28  parent0: (38566) {G0,W9,D3,L2,V3,M2}  { ! alpha45( X, Y, Z ), cons( Y, nil
% 2.82/3.28     ) = X }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28     Y := Y
% 2.82/3.28     Z := Z
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28     1 ==> 1
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (298) {G0,W6,D2,L2,V2,M2} I { ! alpha44( X, Y ), nil = X }.
% 2.82/3.28  parent0: (38569) {G0,W6,D2,L2,V2,M2}  { ! alpha44( X, Y ), nil = X }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28     Y := Y
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28     1 ==> 1
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  eqswap: (43501) {G0,W6,D2,L2,V2,M2}  { X = nil, ! alpha44( X, Y ) }.
% 2.82/3.28  parent0[1]: (298) {G0,W6,D2,L2,V2,M2} I { ! alpha44( X, Y ), nil = X }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28     Y := Y
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (43502) {G1,W5,D2,L2,V1,M2}  { ! totalorderedP( nil ), ! alpha44( 
% 2.82/3.28    skol46, X ) }.
% 2.82/3.28  parent0[0]: (43501) {G0,W6,D2,L2,V2,M2}  { X = nil, ! alpha44( X, Y ) }.
% 2.82/3.28  parent1[0; 2]: (281) {G0,W2,D2,L1,V0,M1} I { ! totalorderedP( skol46 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := skol46
% 2.82/3.28     Y := X
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43513) {G1,W3,D2,L1,V1,M1}  { ! alpha44( skol46, X ) }.
% 2.82/3.28  parent0[0]: (43502) {G1,W5,D2,L2,V1,M2}  { ! totalorderedP( nil ), ! 
% 2.82/3.28    alpha44( skol46, X ) }.
% 2.82/3.28  parent1[0]: (224) {G0,W2,D2,L1,V0,M1} I { totalorderedP( nil ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (874) {G1,W3,D2,L1,V1,M1} P(298,281);r(224) { ! alpha44( 
% 2.82/3.28    skol46, X ) }.
% 2.82/3.28  parent0: (43513) {G1,W3,D2,L1,V1,M1}  { ! alpha44( skol46, X ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := X
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43514) {G2,W2,D2,L1,V0,M1}  { ssItem( skol53 ) }.
% 2.82/3.28  parent0[0]: (874) {G1,W3,D2,L1,V1,M1} P(298,281);r(224) { ! alpha44( skol46
% 2.82/3.28    , X ) }.
% 2.82/3.28  parent1[1]: (282) {G1,W5,D2,L2,V0,M2} I;d(280);d(279) { ssItem( skol53 ), 
% 2.82/3.28    alpha44( skol46, skol50 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := skol50
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (884) {G2,W2,D2,L1,V0,M1} R(874,282) { ssItem( skol53 ) }.
% 2.82/3.28  parent0: (43514) {G2,W2,D2,L1,V0,M1}  { ssItem( skol53 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43515) {G2,W6,D2,L1,V0,M1}  { alpha46( skol46, skol50, skol53
% 2.82/3.28    , skol54, skol55 ) }.
% 2.82/3.28  parent0[0]: (874) {G1,W3,D2,L1,V1,M1} P(298,281);r(224) { ! alpha44( skol46
% 2.82/3.28    , X ) }.
% 2.82/3.28  parent1[1]: (284) {G1,W9,D2,L2,V0,M2} I;d(280);d(280);d(279);d(279) { 
% 2.82/3.28    alpha46( skol46, skol50, skol53, skol54, skol55 ), alpha44( skol46, 
% 2.82/3.28    skol50 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := skol50
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (20534) {G2,W6,D2,L1,V0,M1} S(284);r(874) { alpha46( skol46, 
% 2.82/3.28    skol50, skol53, skol54, skol55 ) }.
% 2.82/3.28  parent0: (43515) {G2,W6,D2,L1,V0,M1}  { alpha46( skol46, skol50, skol53, 
% 2.82/3.28    skol54, skol55 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43516) {G1,W4,D3,L1,V0,M1}  { totalorderedP( cons( skol53, nil
% 2.82/3.28     ) ) }.
% 2.82/3.28  parent0[0]: (223) {G0,W6,D3,L2,V1,M2} I { ! ssItem( X ), totalorderedP( 
% 2.82/3.28    cons( X, nil ) ) }.
% 2.82/3.28  parent1[0]: (884) {G2,W2,D2,L1,V0,M1} R(874,282) { ssItem( skol53 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := skol53
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (23090) {G3,W4,D3,L1,V0,M1} R(223,884) { totalorderedP( cons( 
% 2.82/3.28    skol53, nil ) ) }.
% 2.82/3.28  parent0: (43516) {G1,W4,D3,L1,V0,M1}  { totalorderedP( cons( skol53, nil )
% 2.82/3.28     ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43517) {G1,W4,D2,L1,V0,M1}  { alpha45( skol46, skol53, skol55
% 2.82/3.28     ) }.
% 2.82/3.28  parent0[0]: (286) {G0,W10,D2,L2,V5,M2} I { ! alpha46( X, Y, Z, T, U ), 
% 2.82/3.28    alpha45( X, Z, U ) }.
% 2.82/3.28  parent1[0]: (20534) {G2,W6,D2,L1,V0,M1} S(284);r(874) { alpha46( skol46, 
% 2.82/3.28    skol50, skol53, skol54, skol55 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := skol46
% 2.82/3.28     Y := skol50
% 2.82/3.28     Z := skol53
% 2.82/3.28     T := skol54
% 2.82/3.28     U := skol55
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (34771) {G3,W4,D2,L1,V0,M1} R(286,20534) { alpha45( skol46, 
% 2.82/3.28    skol53, skol55 ) }.
% 2.82/3.28  parent0: (43517) {G1,W4,D2,L1,V0,M1}  { alpha45( skol46, skol53, skol55 )
% 2.82/3.28     }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  eqswap: (43518) {G0,W9,D3,L2,V3,M2}  { Y = cons( X, nil ), ! alpha45( Y, X
% 2.82/3.28    , Z ) }.
% 2.82/3.28  parent0[1]: (295) {G0,W9,D3,L2,V3,M2} I { ! alpha45( X, Y, Z ), cons( Y, 
% 2.82/3.28    nil ) = X }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := Y
% 2.82/3.28     Y := X
% 2.82/3.28     Z := Z
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43519) {G1,W5,D3,L1,V0,M1}  { skol46 = cons( skol53, nil ) }.
% 2.82/3.28  parent0[1]: (43518) {G0,W9,D3,L2,V3,M2}  { Y = cons( X, nil ), ! alpha45( Y
% 2.82/3.28    , X, Z ) }.
% 2.82/3.28  parent1[0]: (34771) {G3,W4,D2,L1,V0,M1} R(286,20534) { alpha45( skol46, 
% 2.82/3.28    skol53, skol55 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28     X := skol53
% 2.82/3.28     Y := skol46
% 2.82/3.28     Z := skol55
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  eqswap: (43520) {G1,W5,D3,L1,V0,M1}  { cons( skol53, nil ) = skol46 }.
% 2.82/3.28  parent0[0]: (43519) {G1,W5,D3,L1,V0,M1}  { skol46 = cons( skol53, nil ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (37295) {G4,W5,D3,L1,V0,M1} R(295,34771) { cons( skol53, nil )
% 2.82/3.28     ==> skol46 }.
% 2.82/3.28  parent0: (43520) {G1,W5,D3,L1,V0,M1}  { cons( skol53, nil ) = skol46 }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28     0 ==> 0
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  paramod: (43522) {G4,W2,D2,L1,V0,M1}  { totalorderedP( skol46 ) }.
% 2.82/3.28  parent0[0]: (37295) {G4,W5,D3,L1,V0,M1} R(295,34771) { cons( skol53, nil ) 
% 2.82/3.28    ==> skol46 }.
% 2.82/3.28  parent1[0; 1]: (23090) {G3,W4,D3,L1,V0,M1} R(223,884) { totalorderedP( cons
% 2.82/3.28    ( skol53, nil ) ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  resolution: (43523) {G1,W0,D0,L0,V0,M0}  {  }.
% 2.82/3.28  parent0[0]: (281) {G0,W2,D2,L1,V0,M1} I { ! totalorderedP( skol46 ) }.
% 2.82/3.28  parent1[0]: (43522) {G4,W2,D2,L1,V0,M1}  { totalorderedP( skol46 ) }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  substitution1:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  subsumption: (38268) {G5,W0,D0,L0,V0,M0} S(23090);d(37295);r(281) {  }.
% 2.82/3.28  parent0: (43523) {G1,W0,D0,L0,V0,M0}  {  }.
% 2.82/3.28  substitution0:
% 2.82/3.28  end
% 2.82/3.28  permutation0:
% 2.82/3.28  end
% 2.82/3.28  
% 2.82/3.28  Proof check complete!
% 2.82/3.28  
% 2.82/3.28  Memory use:
% 2.82/3.28  
% 2.82/3.28  space for terms:        698764
% 2.82/3.28  space for clauses:      1652362
% 2.82/3.28  
% 2.82/3.28  
% 2.82/3.28  clauses generated:      117067
% 2.82/3.28  clauses kept:           38269
% 2.82/3.28  clauses selected:       1182
% 2.82/3.28  clauses deleted:        2366
% 2.82/3.28  clauses inuse deleted:  53
% 2.82/3.28  
% 2.82/3.28  subsentry:          338679
% 2.82/3.28  literals s-matched: 208494
% 2.82/3.28  literals matched:   179379
% 2.82/3.28  full subsumption:   71021
% 2.82/3.28  
% 2.82/3.28  checksum:           -607075376
% 2.82/3.28  
% 2.82/3.28  
% 2.82/3.28  Bliksem ended
%------------------------------------------------------------------------------