%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWX071+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n004.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 Apr 1 02:11:58 AM UTC 2025
% Result : Timeout 299.60s 300.08s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.09 % Problem : SWX071+1 : TPTP v9.1.0. Released v9.1.0.
% 0.09/0.10 % Command : bliksem %s
% 0.10/0.30 % Computer : n004.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % DateTime : Mon Mar 31 15:52:40 EDT 2025
% 0.10/0.30 % CPUTime :
% 0.74/1.28 *** allocated 10000 integers for termspace/termends
% 0.74/1.28 *** allocated 10000 integers for clauses
% 0.74/1.28 *** allocated 10000 integers for justifications
% 0.74/1.28 Bliksem 1.12
% 0.74/1.28
% 0.74/1.28
% 0.74/1.28 Automatic Strategy Selection
% 0.74/1.28
% 0.74/1.28 *** allocated 15000 integers for termspace/termends
% 0.74/1.28 *** allocated 22500 integers for termspace/termends
% 0.74/1.28 *** allocated 33750 integers for termspace/termends
% 0.74/1.28 *** allocated 50625 integers for termspace/termends
% 0.74/1.28 *** allocated 75937 integers for termspace/termends
% 0.74/1.28
% 0.74/1.28 Clauses:
% 0.74/1.28
% 0.74/1.28 { ! nil = cons( X, Y ) }.
% 0.74/1.28 { ! nil = 1 }.
% 0.74/1.28 { ! nil = 0 }.
% 0.74/1.28 { ! nil = p( X ) }.
% 0.74/1.28 { ! nil = neg( X ) }.
% 0.74/1.28 { ! nil = and( X, Y ) }.
% 0.74/1.28 { ! nil = or( X, Y ) }.
% 0.74/1.28 { ! cons( Z, X ) = cons( T, Y ), X = Y }.
% 0.74/1.28 { ! cons( X, Z ) = cons( Y, T ), X = Y }.
% 0.74/1.28 { ! 1 = cons( X, Y ) }.
% 0.74/1.28 { ! 0 = cons( X, Y ) }.
% 0.74/1.28 { ! cons( X, Y ) = p( Z ) }.
% 0.74/1.28 { ! cons( X, Y ) = neg( Z ) }.
% 0.74/1.28 { ! cons( X, Y ) = and( Z, T ) }.
% 0.74/1.28 { ! cons( X, Y ) = or( Z, T ) }.
% 0.74/1.28 { ! 1 = 0 }.
% 0.74/1.28 { ! 1 = p( X ) }.
% 0.74/1.28 { ! 1 = neg( X ) }.
% 0.74/1.28 { ! 1 = and( X, Y ) }.
% 0.74/1.28 { ! 1 = or( X, Y ) }.
% 0.74/1.28 { ! 0 = p( X ) }.
% 0.74/1.28 { ! 0 = neg( X ) }.
% 0.74/1.28 { ! 0 = and( X, Y ) }.
% 0.74/1.28 { ! 0 = or( X, Y ) }.
% 0.74/1.28 { ! p( X ) = p( Y ), X = Y }.
% 0.74/1.28 { ! p( X ) = neg( Y ) }.
% 0.74/1.28 { ! p( X ) = and( Y, Z ) }.
% 0.74/1.28 { ! p( X ) = or( Y, Z ) }.
% 0.74/1.28 { ! neg( X ) = neg( Y ), X = Y }.
% 0.74/1.28 { ! neg( X ) = and( Y, Z ) }.
% 0.74/1.28 { ! neg( X ) = or( Y, Z ) }.
% 0.74/1.28 { ! and( Z, X ) = and( T, Y ), X = Y }.
% 0.74/1.28 { ! and( X, Z ) = and( Y, T ), X = Y }.
% 0.74/1.28 { ! and( X, Y ) = or( Z, T ) }.
% 0.74/1.28 { ! or( Z, X ) = or( T, Y ), X = Y }.
% 0.74/1.28 { ! or( X, Z ) = or( Y, T ), X = Y }.
% 0.74/1.28 { gr( nil ) }.
% 0.74/1.28 { ! gr( X ), ! gr( Y ), gr( cons( X, Y ) ) }.
% 0.74/1.28 { ! gr( cons( X, Y ) ), gr( X ) }.
% 0.74/1.28 { ! gr( cons( X, Y ) ), gr( Y ) }.
% 0.74/1.28 { gr( 1 ) }.
% 0.74/1.28 { gr( 0 ) }.
% 0.74/1.28 { ! gr( X ), gr( p( X ) ) }.
% 0.74/1.28 { ! gr( p( X ) ), gr( X ) }.
% 0.74/1.28 { ! gr( X ), gr( neg( X ) ) }.
% 0.74/1.28 { ! gr( neg( X ) ), gr( X ) }.
% 0.74/1.28 { ! gr( X ), ! gr( Y ), gr( and( X, Y ) ) }.
% 0.74/1.28 { ! gr( and( X, Y ) ), gr( X ) }.
% 0.74/1.28 { ! gr( and( X, Y ) ), gr( Y ) }.
% 0.74/1.28 { ! gr( X ), ! gr( Y ), gr( or( X, Y ) ) }.
% 0.74/1.28 { ! gr( or( X, Y ) ), gr( X ) }.
% 0.74/1.28 { ! gr( or( X, Y ) ), gr( Y ) }.
% 0.74/1.28 { ! defined_succeeds( X, Y ), ! defined_fails( X, Y ) }.
% 0.74/1.28 { ! defined_terminates( X, Y ), defined_succeeds( X, Y ), defined_fails( X
% 0.74/1.28 , Y ) }.
% 0.74/1.28 { ! eval_succeeds( X, Y, Z ), ! eval_fails( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( X, Y, Z ), eval_succeeds( X, Y, Z ), eval_fails( X, Y
% 0.74/1.28 , Z ) }.
% 0.74/1.28 { ! false_succeeds( X, Y, Z ), ! false_fails( X, Y, Z ) }.
% 0.74/1.28 { ! false_terminates( X, Y, Z ), false_succeeds( X, Y, Z ), false_fails( X
% 0.74/1.28 , Y, Z ) }.
% 0.74/1.28 { ! true_succeeds( X, Y, Z ), ! true_fails( X, Y, Z ) }.
% 0.74/1.28 { ! true_terminates( X, Y, Z ), true_succeeds( X, Y, Z ), true_fails( X, Y
% 0.74/1.28 , Z ) }.
% 0.74/1.28 { ! satisfiable_succeeds( X ), ! satisfiable_fails( X ) }.
% 0.74/1.28 { ! satisfiable_terminates( X ), satisfiable_succeeds( X ),
% 0.74/1.28 satisfiable_fails( X ) }.
% 0.74/1.28 { ! valid_succeeds( X ), ! valid_fails( X ) }.
% 0.74/1.28 { ! valid_terminates( X ), valid_succeeds( X ), valid_fails( X ) }.
% 0.74/1.28 { ! incon_succeeds( X ), ! incon_fails( X ) }.
% 0.74/1.28 { ! incon_terminates( X ), incon_succeeds( X ), incon_fails( X ) }.
% 0.74/1.28 { ! interpretation_succeeds( X ), ! interpretation_fails( X ) }.
% 0.74/1.28 { ! interpretation_terminates( X ), interpretation_succeeds( X ),
% 0.74/1.28 interpretation_fails( X ) }.
% 0.74/1.28 { ! literal_list_succeeds( X ), ! literal_list_fails( X ) }.
% 0.74/1.28 { ! literal_list_terminates( X ), literal_list_succeeds( X ),
% 0.74/1.28 literal_list_fails( X ) }.
% 0.74/1.28 { ! literal_succeeds( X ), ! literal_fails( X ) }.
% 0.74/1.28 { ! literal_terminates( X ), literal_succeeds( X ), literal_fails( X ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! formula_fails( X ) }.
% 0.74/1.28 { ! formula_terminates( X ), formula_succeeds( X ), formula_fails( X ) }.
% 0.74/1.28 { ! member_succeeds( X, Y ), ! member_fails( X, Y ) }.
% 0.74/1.28 { ! member_terminates( X, Y ), member_succeeds( X, Y ), member_fails( X, Y
% 0.74/1.28 ) }.
% 0.74/1.28 { ! list_succeeds( X ), ! list_fails( X ) }.
% 0.74/1.28 { ! list_terminates( X ), list_succeeds( X ), list_fails( X ) }.
% 0.74/1.28 { ! defined_succeeds( X, Y ), alpha1( X, Y ), alpha25( X, Y ) }.
% 0.74/1.28 { ! alpha1( X, Y ), defined_succeeds( X, Y ) }.
% 0.74/1.28 { ! alpha25( X, Y ), defined_succeeds( X, Y ) }.
% 0.74/1.28 { ! alpha25( X, Y ), alpha57( X, Y ), alpha79( X, Y ) }.
% 0.74/1.28 { ! alpha57( X, Y ), alpha25( X, Y ) }.
% 0.74/1.28 { ! alpha79( X, Y ), alpha25( X, Y ) }.
% 0.74/1.28 { ! alpha79( X, Y ), alpha104( X, Y ), alpha120( X, Y ) }.
% 0.74/1.28 { ! alpha104( X, Y ), alpha79( X, Y ) }.
% 0.74/1.28 { ! alpha120( X, Y ), alpha79( X, Y ) }.
% 0.74/1.28 { ! alpha120( X, Y ), alpha137( X, Y ), alpha150( X, Y ) }.
% 0.74/1.28 { ! alpha137( X, Y ), alpha120( X, Y ) }.
% 0.74/1.28 { ! alpha150( X, Y ), alpha120( X, Y ) }.
% 0.74/1.28 { ! alpha150( X, Y ), member_succeeds( p( skol1( Z, Y ) ), Y ) }.
% 0.74/1.28 { ! alpha150( X, Y ), X = p( skol1( X, Y ) ) }.
% 0.74/1.28 { ! X = p( Z ), ! member_succeeds( p( Z ), Y ), alpha150( X, Y ) }.
% 0.74/1.28 { ! alpha137( X, Y ), member_succeeds( neg( p( skol2( Z, Y ) ) ), Y ) }.
% 0.74/1.28 { ! alpha137( X, Y ), X = p( skol2( X, Y ) ) }.
% 0.74/1.28 { ! X = p( Z ), ! member_succeeds( neg( p( Z ) ), Y ), alpha137( X, Y ) }.
% 0.74/1.28 { ! alpha104( X, Y ), defined_succeeds( skol3( Z, Y ), Y ) }.
% 0.74/1.28 { ! alpha104( X, Y ), X = neg( skol3( X, Y ) ) }.
% 0.74/1.28 { ! X = neg( Z ), ! defined_succeeds( Z, Y ), alpha104( X, Y ) }.
% 0.74/1.28 { ! alpha57( X, Y ), X = and( skol4( X, Y ), skol168( X, Y ) ) }.
% 0.74/1.28 { ! alpha57( X, Y ), alpha80( Y, skol4( X, Y ), skol168( X, Y ) ) }.
% 0.74/1.28 { ! X = and( Z, T ), ! alpha80( Y, Z, T ), alpha57( X, Y ) }.
% 0.74/1.28 { ! alpha80( X, Y, Z ), defined_succeeds( Y, X ) }.
% 0.74/1.28 { ! alpha80( X, Y, Z ), defined_succeeds( Z, X ) }.
% 0.74/1.28 { ! defined_succeeds( Y, X ), ! defined_succeeds( Z, X ), alpha80( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha1( X, Y ), X = or( skol5( X, Y ), skol169( X, Y ) ) }.
% 0.74/1.28 { ! alpha1( X, Y ), alpha26( Y, skol5( X, Y ), skol169( X, Y ) ) }.
% 0.74/1.28 { ! X = or( Z, T ), ! alpha26( Y, Z, T ), alpha1( X, Y ) }.
% 0.74/1.28 { ! alpha26( X, Y, Z ), defined_succeeds( Y, X ) }.
% 0.74/1.28 { ! alpha26( X, Y, Z ), defined_succeeds( Z, X ) }.
% 0.74/1.28 { ! defined_succeeds( Y, X ), ! defined_succeeds( Z, X ), alpha26( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! defined_fails( X, Y ), alpha2( X, Y ) }.
% 0.74/1.28 { ! defined_fails( X, Y ), alpha27( X, Y ) }.
% 0.74/1.28 { ! alpha2( X, Y ), ! alpha27( X, Y ), defined_fails( X, Y ) }.
% 0.74/1.28 { ! alpha27( X, Y ), alpha58( X, Y ) }.
% 0.74/1.28 { ! alpha27( X, Y ), alpha81( X, Y ) }.
% 0.74/1.28 { ! alpha58( X, Y ), ! alpha81( X, Y ), alpha27( X, Y ) }.
% 0.74/1.28 { ! alpha81( X, Y ), alpha105( X, Y ) }.
% 0.74/1.28 { ! alpha81( X, Y ), alpha121( X, Y ) }.
% 0.74/1.28 { ! alpha105( X, Y ), ! alpha121( X, Y ), alpha81( X, Y ) }.
% 0.74/1.28 { ! alpha121( X, Y ), alpha138( X, Y ) }.
% 0.74/1.28 { ! alpha121( X, Y ), alpha151( X, Y ) }.
% 0.74/1.28 { ! alpha138( X, Y ), ! alpha151( X, Y ), alpha121( X, Y ) }.
% 0.74/1.28 { ! alpha151( X, Y ), ! X = p( Z ), member_fails( p( Z ), Y ) }.
% 0.74/1.28 { ! member_fails( p( skol6( Z, Y ) ), Y ), alpha151( X, Y ) }.
% 0.74/1.28 { X = p( skol6( X, Y ) ), alpha151( X, Y ) }.
% 0.74/1.28 { ! alpha138( X, Y ), ! X = p( Z ), member_fails( neg( p( Z ) ), Y ) }.
% 0.74/1.28 { ! member_fails( neg( p( skol7( Z, Y ) ) ), Y ), alpha138( X, Y ) }.
% 0.74/1.28 { X = p( skol7( X, Y ) ), alpha138( X, Y ) }.
% 0.74/1.28 { ! alpha105( X, Y ), ! X = neg( Z ), defined_fails( Z, Y ) }.
% 0.74/1.28 { ! defined_fails( skol8( Z, Y ), Y ), alpha105( X, Y ) }.
% 0.74/1.28 { X = neg( skol8( X, Y ) ), alpha105( X, Y ) }.
% 0.74/1.28 { ! alpha58( X, Y ), ! X = and( Z, T ), alpha82( Y, Z, T ) }.
% 0.74/1.28 { X = and( skol9( X, Y ), skol170( X, Y ) ), alpha58( X, Y ) }.
% 0.74/1.28 { ! alpha82( Y, skol9( X, Y ), skol170( X, Y ) ), alpha58( X, Y ) }.
% 0.74/1.28 { ! alpha82( X, Y, Z ), defined_fails( Y, X ), defined_fails( Z, X ) }.
% 0.74/1.28 { ! defined_fails( Y, X ), alpha82( X, Y, Z ) }.
% 0.74/1.28 { ! defined_fails( Z, X ), alpha82( X, Y, Z ) }.
% 0.74/1.28 { ! alpha2( X, Y ), ! X = or( Z, T ), alpha28( Y, Z, T ) }.
% 0.74/1.28 { X = or( skol10( X, Y ), skol171( X, Y ) ), alpha2( X, Y ) }.
% 0.74/1.28 { ! alpha28( Y, skol10( X, Y ), skol171( X, Y ) ), alpha2( X, Y ) }.
% 0.74/1.28 { ! alpha28( X, Y, Z ), defined_fails( Y, X ), defined_fails( Z, X ) }.
% 0.74/1.28 { ! defined_fails( Y, X ), alpha28( X, Y, Z ) }.
% 0.74/1.28 { ! defined_fails( Z, X ), alpha28( X, Y, Z ) }.
% 0.74/1.28 { ! defined_terminates( X, Y ), alpha3( X, Y ) }.
% 0.74/1.28 { ! defined_terminates( X, Y ), alpha29( X, Y ) }.
% 0.74/1.28 { ! alpha3( X, Y ), ! alpha29( X, Y ), defined_terminates( X, Y ) }.
% 0.74/1.28 { ! alpha29( X, Y ), alpha59( X, Y ) }.
% 0.74/1.28 { ! alpha29( X, Y ), alpha83( X, Y ) }.
% 0.74/1.28 { ! alpha59( X, Y ), ! alpha83( X, Y ), alpha29( X, Y ) }.
% 0.74/1.28 { ! alpha83( X, Y ), alpha106( X, Y ) }.
% 0.74/1.28 { ! alpha83( X, Y ), alpha122( X, Y ) }.
% 0.74/1.28 { ! alpha106( X, Y ), ! alpha122( X, Y ), alpha83( X, Y ) }.
% 0.74/1.28 { ! alpha122( X, Y ), alpha139( X, Y ) }.
% 0.74/1.28 { ! alpha122( X, Y ), alpha152( X, Y ) }.
% 0.74/1.28 { ! alpha139( X, Y ), ! alpha152( X, Y ), alpha122( X, Y ) }.
% 0.74/1.28 { ! alpha152( X, Y ), ! X = p( Z ), member_terminates( p( Z ), Y ) }.
% 0.74/1.28 { ! &&, ! member_terminates( p( skol11( Z, Y ) ), Y ), alpha152( X, Y ) }.
% 0.74/1.28 { ! &&, X = p( skol11( X, Y ) ), alpha152( X, Y ) }.
% 0.74/1.28 { ! alpha139( X, Y ), ! X = p( Z ), member_terminates( neg( p( Z ) ), Y ) }
% 0.74/1.28 .
% 0.74/1.28 { ! &&, ! member_terminates( neg( p( skol12( Z, Y ) ) ), Y ), alpha139( X,
% 0.74/1.28 Y ) }.
% 0.74/1.28 { ! &&, X = p( skol12( X, Y ) ), alpha139( X, Y ) }.
% 0.74/1.28 { ! alpha106( X, Y ), ! X = neg( Z ), defined_terminates( Z, Y ) }.
% 0.74/1.28 { ! &&, ! defined_terminates( skol13( Z, Y ), Y ), alpha106( X, Y ) }.
% 0.74/1.28 { ! &&, X = neg( skol13( X, Y ) ), alpha106( X, Y ) }.
% 0.74/1.28 { ! alpha59( X, Y ), ! X = and( Z, T ), alpha84( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = and( skol14( X, Y ), skol172( X, Y ) ), alpha59( X, Y ) }.
% 0.74/1.28 { ! &&, ! alpha84( Y, skol14( X, Y ), skol172( X, Y ) ), alpha59( X, Y ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha84( X, Y, Z ), defined_terminates( Y, X ) }.
% 0.74/1.28 { ! alpha84( X, Y, Z ), alpha107( X, Y, Z ) }.
% 0.74/1.28 { ! defined_terminates( Y, X ), ! alpha107( X, Y, Z ), alpha84( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha107( X, Y, Z ), defined_fails( Y, X ), defined_terminates( Z, X )
% 0.74/1.28 }.
% 0.74/1.28 { ! defined_fails( Y, X ), alpha107( X, Y, Z ) }.
% 0.74/1.28 { ! defined_terminates( Z, X ), alpha107( X, Y, Z ) }.
% 0.74/1.28 { ! alpha3( X, Y ), ! X = or( Z, T ), alpha30( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = or( skol15( X, Y ), skol173( X, Y ) ), alpha3( X, Y ) }.
% 0.74/1.28 { ! &&, ! alpha30( Y, skol15( X, Y ), skol173( X, Y ) ), alpha3( X, Y ) }.
% 0.74/1.28 { ! alpha30( X, Y, Z ), defined_terminates( Y, X ) }.
% 0.74/1.28 { ! alpha30( X, Y, Z ), alpha60( X, Y, Z ) }.
% 0.74/1.28 { ! defined_terminates( Y, X ), ! alpha60( X, Y, Z ), alpha30( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha60( X, Y, Z ), defined_fails( Y, X ), defined_terminates( Z, X ) }
% 0.74/1.28 .
% 0.74/1.28 { ! defined_fails( Y, X ), alpha60( X, Y, Z ) }.
% 0.74/1.28 { ! defined_terminates( Z, X ), alpha60( X, Y, Z ) }.
% 0.74/1.28 { ! eval_succeeds( X, Y, Z ), alpha4( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.74/1.28 { ! alpha4( X, Y, Z ), eval_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! alpha31( X, Y, Z ), eval_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! alpha31( X, Y, Z ), alpha61( X, Y, Z ), alpha85( X, Y, Z ) }.
% 0.74/1.28 { ! alpha61( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.74/1.28 { ! alpha85( X, Y, Z ), alpha31( X, Y, Z ) }.
% 0.74/1.28 { ! alpha85( X, Y, Z ), alpha108( X, Y, Z ), alpha123( X, Y, Z ) }.
% 0.74/1.28 { ! alpha108( X, Y, Z ), alpha85( X, Y, Z ) }.
% 0.74/1.28 { ! alpha123( X, Y, Z ), alpha85( X, Y, Z ) }.
% 0.74/1.28 { ! alpha123( X, Y, Z ), alpha140( X, Y, Z ), alpha153( X, Y, Z ) }.
% 0.74/1.28 { ! alpha140( X, Y, Z ), alpha123( X, Y, Z ) }.
% 0.74/1.28 { ! alpha153( X, Y, Z ), alpha123( X, Y, Z ) }.
% 0.74/1.28 { ! alpha153( X, Y, Z ), alpha166( X, Y, Z ), alpha175( X, Y, Z ) }.
% 0.74/1.28 { ! alpha166( X, Y, Z ), alpha153( X, Y, Z ) }.
% 0.74/1.28 { ! alpha175( X, Y, Z ), alpha153( X, Y, Z ) }.
% 0.74/1.28 { ! alpha175( X, Y, Z ), alpha183( X, Y, Z ), alpha186( X, Y, Z ) }.
% 0.74/1.28 { ! alpha183( X, Y, Z ), alpha175( X, Y, Z ) }.
% 0.74/1.28 { ! alpha186( X, Y, Z ), alpha175( X, Y, Z ) }.
% 0.74/1.28 { ! alpha186( X, Y, Z ), alpha192( X, Y, Z ), alpha199( X, Y, Z ) }.
% 0.74/1.28 { ! alpha192( X, Y, Z ), alpha186( X, Y, Z ) }.
% 0.74/1.28 { ! alpha199( X, Y, Z ), alpha186( X, Y, Z ) }.
% 0.74/1.28 { ! alpha199( X, Y, Z ), alpha205( X, Y, Z ), alpha208( X, Y, Z ) }.
% 0.74/1.28 { ! alpha205( X, Y, Z ), alpha199( X, Y, Z ) }.
% 0.74/1.28 { ! alpha208( X, Y, Z ), alpha199( X, Y, Z ) }.
% 0.74/1.28 { ! alpha208( X, Y, Z ), alpha214( X, Y, Z ), alpha217( X, Y, Z ) }.
% 0.74/1.28 { ! alpha214( X, Y, Z ), alpha208( X, Y, Z ) }.
% 0.74/1.28 { ! alpha217( X, Y, Z ), alpha208( X, Y, Z ) }.
% 0.74/1.28 { ! alpha217( X, Y, Z ), X = p( skol16( X, T, U ) ) }.
% 0.74/1.28 { ! alpha217( X, Y, Z ), alpha223( Y, Z, skol16( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = p( T ), ! alpha223( Y, Z, T ), alpha217( X, Y, Z ) }.
% 0.74/1.28 { ! alpha223( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! alpha223( X, Y, Z ), member_succeeds( p( Z ), X ) }.
% 0.74/1.28 { ! Y = 1, ! member_succeeds( p( Z ), X ), alpha223( X, Y, Z ) }.
% 0.74/1.28 { ! alpha214( X, Y, Z ), X = p( skol17( X, T, U ) ) }.
% 0.74/1.28 { ! alpha214( X, Y, Z ), alpha218( Y, Z, skol17( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = p( T ), ! alpha218( Y, Z, T ), alpha214( X, Y, Z ) }.
% 0.74/1.28 { ! alpha218( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! alpha218( X, Y, Z ), member_succeeds( neg( p( Z ) ), X ) }.
% 0.74/1.28 { ! Y = 0, ! member_succeeds( neg( p( Z ) ), X ), alpha218( X, Y, Z ) }.
% 0.74/1.28 { ! alpha205( X, Y, Z ), X = neg( skol18( X, T, U ) ) }.
% 0.74/1.28 { ! alpha205( X, Y, Z ), alpha209( Y, Z, skol18( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = neg( T ), ! alpha209( Y, Z, T ), alpha205( X, Y, Z ) }.
% 0.74/1.28 { ! alpha209( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! alpha209( X, Y, Z ), eval_succeeds( Z, X, 0 ) }.
% 0.74/1.28 { ! Y = 1, ! eval_succeeds( Z, X, 0 ), alpha209( X, Y, Z ) }.
% 0.74/1.28 { ! alpha192( X, Y, Z ), X = neg( skol19( X, T, U ) ) }.
% 0.74/1.28 { ! alpha192( X, Y, Z ), alpha200( Y, Z, skol19( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = neg( T ), ! alpha200( Y, Z, T ), alpha192( X, Y, Z ) }.
% 0.74/1.28 { ! alpha200( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! alpha200( X, Y, Z ), eval_succeeds( Z, X, 1 ) }.
% 0.74/1.28 { ! Y = 0, ! eval_succeeds( Z, X, 1 ), alpha200( X, Y, Z ) }.
% 0.74/1.28 { ! alpha183( X, Y, Z ), X = and( skol20( X, Y, Z ), skol174( X, Y, Z ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha183( X, Y, Z ), alpha193( Y, Z, skol20( X, Y, Z ), skol174( X, Y,
% 0.74/1.28 Z ) ) }.
% 0.74/1.28 { ! X = and( T, U ), ! alpha193( Y, Z, T, U ), alpha183( X, Y, Z ) }.
% 0.74/1.28 { ! alpha193( X, Y, Z, T ), Y = 1 }.
% 0.74/1.28 { ! alpha193( X, Y, Z, T ), alpha187( X, Z, T ) }.
% 0.74/1.28 { ! Y = 1, ! alpha187( X, Z, T ), alpha193( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha187( X, Y, Z ), eval_succeeds( Y, X, 1 ) }.
% 0.74/1.28 { ! alpha187( X, Y, Z ), eval_succeeds( Z, X, 1 ) }.
% 0.74/1.28 { ! eval_succeeds( Y, X, 1 ), ! eval_succeeds( Z, X, 1 ), alpha187( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha166( X, Y, Z ), X = and( skol21( X, T, U ), skol175( X, T, U ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha166( X, Y, Z ), alpha176( Y, Z, skol21( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = and( T, U ), ! alpha176( Y, Z, T ), alpha166( X, Y, Z ) }.
% 0.74/1.28 { ! alpha176( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! alpha176( X, Y, Z ), eval_succeeds( Z, X, 0 ) }.
% 0.74/1.28 { ! Y = 0, ! eval_succeeds( Z, X, 0 ), alpha176( X, Y, Z ) }.
% 0.74/1.28 { ! alpha140( X, Y, Z ), X = and( skol176( X, T, U ), skol22( X, T, U ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha140( X, Y, Z ), alpha154( Y, Z, skol22( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = and( U, T ), ! alpha154( Y, Z, T ), alpha140( X, Y, Z ) }.
% 0.74/1.28 { ! alpha154( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! alpha154( X, Y, Z ), eval_succeeds( Z, X, 0 ) }.
% 0.74/1.28 { ! Y = 0, ! eval_succeeds( Z, X, 0 ), alpha154( X, Y, Z ) }.
% 0.74/1.28 { ! alpha108( X, Y, Z ), X = or( skol23( X, T, U ), skol177( X, T, U ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha108( X, Y, Z ), alpha124( Y, Z, skol23( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = or( T, U ), ! alpha124( Y, Z, T ), alpha108( X, Y, Z ) }.
% 0.74/1.28 { ! alpha124( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! alpha124( X, Y, Z ), eval_succeeds( Z, X, 1 ) }.
% 0.74/1.28 { ! Y = 1, ! eval_succeeds( Z, X, 1 ), alpha124( X, Y, Z ) }.
% 0.74/1.28 { ! alpha61( X, Y, Z ), X = or( skol178( X, T, U ), skol24( X, T, U ) ) }.
% 0.74/1.28 { ! alpha61( X, Y, Z ), alpha86( Y, Z, skol24( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = or( U, T ), ! alpha86( Y, Z, T ), alpha61( X, Y, Z ) }.
% 0.74/1.28 { ! alpha86( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! alpha86( X, Y, Z ), eval_succeeds( Z, X, 1 ) }.
% 0.74/1.28 { ! Y = 1, ! eval_succeeds( Z, X, 1 ), alpha86( X, Y, Z ) }.
% 0.74/1.28 { ! alpha4( X, Y, Z ), X = or( skol25( X, Y, Z ), skol179( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha4( X, Y, Z ), alpha62( Y, Z, skol25( X, Y, Z ), skol179( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { ! X = or( T, U ), ! alpha62( Y, Z, T, U ), alpha4( X, Y, Z ) }.
% 0.74/1.28 { ! alpha62( X, Y, Z, T ), Y = 0 }.
% 0.74/1.28 { ! alpha62( X, Y, Z, T ), alpha32( X, Z, T ) }.
% 0.74/1.28 { ! Y = 0, ! alpha32( X, Z, T ), alpha62( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha32( X, Y, Z ), eval_succeeds( Y, X, 0 ) }.
% 0.74/1.28 { ! alpha32( X, Y, Z ), eval_succeeds( Z, X, 0 ) }.
% 0.74/1.28 { ! eval_succeeds( Y, X, 0 ), ! eval_succeeds( Z, X, 0 ), alpha32( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! eval_fails( X, Y, Z ), alpha5( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( X, Y, Z ), alpha33( X, Y, Z ) }.
% 0.74/1.28 { ! alpha5( X, Y, Z ), ! alpha33( X, Y, Z ), eval_fails( X, Y, Z ) }.
% 0.74/1.28 { ! alpha33( X, Y, Z ), alpha63( X, Y, Z ) }.
% 0.74/1.28 { ! alpha33( X, Y, Z ), alpha87( X, Y, Z ) }.
% 0.74/1.28 { ! alpha63( X, Y, Z ), ! alpha87( X, Y, Z ), alpha33( X, Y, Z ) }.
% 0.74/1.28 { ! alpha87( X, Y, Z ), alpha109( X, Y, Z ) }.
% 0.74/1.28 { ! alpha87( X, Y, Z ), alpha125( X, Y, Z ) }.
% 0.74/1.28 { ! alpha109( X, Y, Z ), ! alpha125( X, Y, Z ), alpha87( X, Y, Z ) }.
% 0.74/1.28 { ! alpha125( X, Y, Z ), alpha141( X, Y, Z ) }.
% 0.74/1.28 { ! alpha125( X, Y, Z ), alpha155( X, Y, Z ) }.
% 0.74/1.28 { ! alpha141( X, Y, Z ), ! alpha155( X, Y, Z ), alpha125( X, Y, Z ) }.
% 0.74/1.28 { ! alpha155( X, Y, Z ), alpha167( X, Y, Z ) }.
% 0.74/1.28 { ! alpha155( X, Y, Z ), alpha177( X, Y, Z ) }.
% 0.74/1.28 { ! alpha167( X, Y, Z ), ! alpha177( X, Y, Z ), alpha155( X, Y, Z ) }.
% 0.74/1.28 { ! alpha177( X, Y, Z ), alpha184( X, Y, Z ) }.
% 0.74/1.28 { ! alpha177( X, Y, Z ), alpha188( X, Y, Z ) }.
% 0.74/1.28 { ! alpha184( X, Y, Z ), ! alpha188( X, Y, Z ), alpha177( X, Y, Z ) }.
% 0.74/1.28 { ! alpha188( X, Y, Z ), alpha194( X, Y, Z ) }.
% 0.74/1.28 { ! alpha188( X, Y, Z ), alpha201( X, Y, Z ) }.
% 0.74/1.28 { ! alpha194( X, Y, Z ), ! alpha201( X, Y, Z ), alpha188( X, Y, Z ) }.
% 0.74/1.28 { ! alpha201( X, Y, Z ), alpha206( X, Y, Z ) }.
% 0.74/1.28 { ! alpha201( X, Y, Z ), alpha210( X, Y, Z ) }.
% 0.74/1.28 { ! alpha206( X, Y, Z ), ! alpha210( X, Y, Z ), alpha201( X, Y, Z ) }.
% 0.74/1.28 { ! alpha210( X, Y, Z ), alpha215( X, Y, Z ) }.
% 0.74/1.28 { ! alpha210( X, Y, Z ), alpha219( X, Y, Z ) }.
% 0.74/1.28 { ! alpha215( X, Y, Z ), ! alpha219( X, Y, Z ), alpha210( X, Y, Z ) }.
% 0.74/1.28 { ! alpha219( X, Y, Z ), ! X = p( T ), alpha224( Y, Z, T ) }.
% 0.74/1.28 { X = p( skol26( X, T, U ) ), alpha219( X, Y, Z ) }.
% 0.74/1.28 { ! alpha224( Y, Z, skol26( X, Y, Z ) ), alpha219( X, Y, Z ) }.
% 0.74/1.28 { ! alpha224( X, Y, Z ), ! Y = 1, member_fails( p( Z ), X ) }.
% 0.74/1.28 { Y = 1, alpha224( X, Y, Z ) }.
% 0.74/1.28 { ! member_fails( p( Z ), X ), alpha224( X, Y, Z ) }.
% 0.74/1.28 { ! alpha215( X, Y, Z ), ! X = p( T ), alpha220( Y, Z, T ) }.
% 0.74/1.28 { X = p( skol27( X, T, U ) ), alpha215( X, Y, Z ) }.
% 0.74/1.28 { ! alpha220( Y, Z, skol27( X, Y, Z ) ), alpha215( X, Y, Z ) }.
% 0.74/1.28 { ! alpha220( X, Y, Z ), ! Y = 0, member_fails( neg( p( Z ) ), X ) }.
% 0.74/1.28 { Y = 0, alpha220( X, Y, Z ) }.
% 0.74/1.28 { ! member_fails( neg( p( Z ) ), X ), alpha220( X, Y, Z ) }.
% 0.74/1.28 { ! alpha206( X, Y, Z ), ! X = neg( T ), alpha211( Y, Z, T ) }.
% 0.74/1.28 { X = neg( skol28( X, T, U ) ), alpha206( X, Y, Z ) }.
% 0.74/1.28 { ! alpha211( Y, Z, skol28( X, Y, Z ) ), alpha206( X, Y, Z ) }.
% 0.74/1.28 { ! alpha211( X, Y, Z ), ! Y = 1, eval_fails( Z, X, 0 ) }.
% 0.74/1.28 { Y = 1, alpha211( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 0 ), alpha211( X, Y, Z ) }.
% 0.74/1.28 { ! alpha194( X, Y, Z ), ! X = neg( T ), alpha202( Y, Z, T ) }.
% 0.74/1.28 { X = neg( skol29( X, T, U ) ), alpha194( X, Y, Z ) }.
% 0.74/1.28 { ! alpha202( Y, Z, skol29( X, Y, Z ) ), alpha194( X, Y, Z ) }.
% 0.74/1.28 { ! alpha202( X, Y, Z ), ! Y = 0, eval_fails( Z, X, 1 ) }.
% 0.74/1.28 { Y = 0, alpha202( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 1 ), alpha202( X, Y, Z ) }.
% 0.74/1.28 { ! alpha184( X, Y, Z ), ! X = and( T, U ), alpha195( Y, Z, T, U ) }.
% 0.74/1.28 { X = and( skol30( X, Y, Z ), skol180( X, Y, Z ) ), alpha184( X, Y, Z ) }.
% 0.74/1.28 { ! alpha195( Y, Z, skol30( X, Y, Z ), skol180( X, Y, Z ) ), alpha184( X, Y
% 0.74/1.28 , Z ) }.
% 0.74/1.28 { ! alpha195( X, Y, Z, T ), ! Y = 1, alpha189( X, Z, T ) }.
% 0.74/1.28 { Y = 1, alpha195( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha189( X, Z, T ), alpha195( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha189( X, Y, Z ), eval_fails( Y, X, 1 ), eval_fails( Z, X, 1 ) }.
% 0.74/1.28 { ! eval_fails( Y, X, 1 ), alpha189( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 1 ), alpha189( X, Y, Z ) }.
% 0.74/1.28 { ! alpha167( X, Y, Z ), ! X = and( T, U ), alpha178( Y, Z, T ) }.
% 0.74/1.28 { X = and( skol31( X, T, U ), skol181( X, T, U ) ), alpha167( X, Y, Z ) }.
% 0.74/1.28 { ! alpha178( Y, Z, skol31( X, Y, Z ) ), alpha167( X, Y, Z ) }.
% 0.74/1.28 { ! alpha178( X, Y, Z ), ! Y = 0, eval_fails( Z, X, 0 ) }.
% 0.74/1.28 { Y = 0, alpha178( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 0 ), alpha178( X, Y, Z ) }.
% 0.74/1.28 { ! alpha141( X, Y, Z ), ! X = and( U, T ), alpha156( Y, Z, T ) }.
% 0.74/1.28 { X = and( skol182( X, T, U ), skol32( X, T, U ) ), alpha141( X, Y, Z ) }.
% 0.74/1.28 { ! alpha156( Y, Z, skol32( X, Y, Z ) ), alpha141( X, Y, Z ) }.
% 0.74/1.28 { ! alpha156( X, Y, Z ), ! Y = 0, eval_fails( Z, X, 0 ) }.
% 0.74/1.28 { Y = 0, alpha156( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 0 ), alpha156( X, Y, Z ) }.
% 0.74/1.28 { ! alpha109( X, Y, Z ), ! X = or( T, U ), alpha126( Y, Z, T ) }.
% 0.74/1.28 { X = or( skol33( X, T, U ), skol183( X, T, U ) ), alpha109( X, Y, Z ) }.
% 0.74/1.28 { ! alpha126( Y, Z, skol33( X, Y, Z ) ), alpha109( X, Y, Z ) }.
% 0.74/1.28 { ! alpha126( X, Y, Z ), ! Y = 1, eval_fails( Z, X, 1 ) }.
% 0.74/1.28 { Y = 1, alpha126( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 1 ), alpha126( X, Y, Z ) }.
% 0.74/1.28 { ! alpha63( X, Y, Z ), ! X = or( U, T ), alpha88( Y, Z, T ) }.
% 0.74/1.28 { X = or( skol184( X, T, U ), skol34( X, T, U ) ), alpha63( X, Y, Z ) }.
% 0.74/1.28 { ! alpha88( Y, Z, skol34( X, Y, Z ) ), alpha63( X, Y, Z ) }.
% 0.74/1.28 { ! alpha88( X, Y, Z ), ! Y = 1, eval_fails( Z, X, 1 ) }.
% 0.74/1.28 { Y = 1, alpha88( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 1 ), alpha88( X, Y, Z ) }.
% 0.74/1.28 { ! alpha5( X, Y, Z ), ! X = or( T, U ), alpha64( Y, Z, T, U ) }.
% 0.74/1.28 { X = or( skol35( X, Y, Z ), skol185( X, Y, Z ) ), alpha5( X, Y, Z ) }.
% 0.74/1.28 { ! alpha64( Y, Z, skol35( X, Y, Z ), skol185( X, Y, Z ) ), alpha5( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha64( X, Y, Z, T ), ! Y = 0, alpha34( X, Z, T ) }.
% 0.74/1.28 { Y = 0, alpha64( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha34( X, Z, T ), alpha64( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha34( X, Y, Z ), eval_fails( Y, X, 0 ), eval_fails( Z, X, 0 ) }.
% 0.74/1.28 { ! eval_fails( Y, X, 0 ), alpha34( X, Y, Z ) }.
% 0.74/1.28 { ! eval_fails( Z, X, 0 ), alpha34( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( X, Y, Z ), alpha6( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( X, Y, Z ), alpha35( X, Y, Z ) }.
% 0.74/1.28 { ! alpha6( X, Y, Z ), ! alpha35( X, Y, Z ), eval_terminates( X, Y, Z ) }.
% 0.74/1.28 { ! alpha35( X, Y, Z ), alpha65( X, Y, Z ) }.
% 0.74/1.28 { ! alpha35( X, Y, Z ), alpha89( X, Y, Z ) }.
% 0.74/1.28 { ! alpha65( X, Y, Z ), ! alpha89( X, Y, Z ), alpha35( X, Y, Z ) }.
% 0.74/1.28 { ! alpha89( X, Y, Z ), alpha110( X, Y, Z ) }.
% 0.74/1.28 { ! alpha89( X, Y, Z ), alpha127( X, Y, Z ) }.
% 0.74/1.28 { ! alpha110( X, Y, Z ), ! alpha127( X, Y, Z ), alpha89( X, Y, Z ) }.
% 0.74/1.28 { ! alpha127( X, Y, Z ), alpha142( X, Y, Z ) }.
% 0.74/1.28 { ! alpha127( X, Y, Z ), alpha157( X, Y, Z ) }.
% 0.74/1.28 { ! alpha142( X, Y, Z ), ! alpha157( X, Y, Z ), alpha127( X, Y, Z ) }.
% 0.74/1.28 { ! alpha157( X, Y, Z ), alpha168( X, Y, Z ) }.
% 0.74/1.28 { ! alpha157( X, Y, Z ), alpha179( X, Y, Z ) }.
% 0.74/1.28 { ! alpha168( X, Y, Z ), ! alpha179( X, Y, Z ), alpha157( X, Y, Z ) }.
% 0.74/1.28 { ! alpha179( X, Y, Z ), alpha185( X, Y, Z ) }.
% 0.74/1.28 { ! alpha179( X, Y, Z ), alpha190( X, Y, Z ) }.
% 0.74/1.28 { ! alpha185( X, Y, Z ), ! alpha190( X, Y, Z ), alpha179( X, Y, Z ) }.
% 0.74/1.28 { ! alpha190( X, Y, Z ), alpha196( X, Y, Z ) }.
% 0.74/1.28 { ! alpha190( X, Y, Z ), alpha203( X, Y, Z ) }.
% 0.74/1.28 { ! alpha196( X, Y, Z ), ! alpha203( X, Y, Z ), alpha190( X, Y, Z ) }.
% 0.74/1.28 { ! alpha203( X, Y, Z ), alpha207( X, Y, Z ) }.
% 0.74/1.28 { ! alpha203( X, Y, Z ), alpha212( X, Y, Z ) }.
% 0.74/1.28 { ! alpha207( X, Y, Z ), ! alpha212( X, Y, Z ), alpha203( X, Y, Z ) }.
% 0.74/1.28 { ! alpha212( X, Y, Z ), alpha216( X, Y, Z ) }.
% 0.74/1.28 { ! alpha212( X, Y, Z ), alpha221( X, Y, Z ) }.
% 0.74/1.28 { ! alpha216( X, Y, Z ), ! alpha221( X, Y, Z ), alpha212( X, Y, Z ) }.
% 0.74/1.28 { ! alpha221( X, Y, Z ), ! X = p( T ), alpha225( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = p( skol36( X, T, U ) ), alpha221( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha225( Y, Z, skol36( X, Y, Z ) ), alpha221( X, Y, Z ) }.
% 0.74/1.28 { ! alpha225( X, Y, Z ), ! Y = 1, member_terminates( p( Z ), X ) }.
% 0.74/1.28 { ! &&, Y = 1, alpha225( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! member_terminates( p( Z ), X ), alpha225( X, Y, Z ) }.
% 0.74/1.28 { ! alpha216( X, Y, Z ), ! X = p( T ), alpha222( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = p( skol37( X, T, U ) ), alpha216( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha222( Y, Z, skol37( X, Y, Z ) ), alpha216( X, Y, Z ) }.
% 0.74/1.28 { ! alpha222( X, Y, Z ), ! Y = 0, member_terminates( neg( p( Z ) ), X ) }.
% 0.74/1.28 { ! &&, Y = 0, alpha222( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! member_terminates( neg( p( Z ) ), X ), alpha222( X, Y, Z ) }.
% 0.74/1.28 { ! alpha207( X, Y, Z ), ! X = neg( T ), alpha213( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = neg( skol38( X, T, U ) ), alpha207( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha213( Y, Z, skol38( X, Y, Z ) ), alpha207( X, Y, Z ) }.
% 0.74/1.28 { ! alpha213( X, Y, Z ), ! Y = 1, eval_terminates( Z, X, 0 ) }.
% 0.74/1.28 { ! &&, Y = 1, alpha213( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! eval_terminates( Z, X, 0 ), alpha213( X, Y, Z ) }.
% 0.74/1.28 { ! alpha196( X, Y, Z ), ! X = neg( T ), alpha204( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = neg( skol39( X, T, U ) ), alpha196( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha204( Y, Z, skol39( X, Y, Z ) ), alpha196( X, Y, Z ) }.
% 0.74/1.28 { ! alpha204( X, Y, Z ), ! Y = 0, eval_terminates( Z, X, 1 ) }.
% 0.74/1.28 { ! &&, Y = 0, alpha204( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! eval_terminates( Z, X, 1 ), alpha204( X, Y, Z ) }.
% 0.74/1.28 { ! alpha185( X, Y, Z ), ! X = and( T, U ), alpha197( Y, Z, T, U ) }.
% 0.74/1.28 { ! &&, X = and( skol40( X, Y, Z ), skol186( X, Y, Z ) ), alpha185( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! alpha197( Y, Z, skol40( X, Y, Z ), skol186( X, Y, Z ) ), alpha185
% 0.74/1.28 ( X, Y, Z ) }.
% 0.74/1.28 { ! alpha197( X, Y, Z, T ), ! Y = 1, alpha191( X, Z, T ) }.
% 0.74/1.28 { ! &&, Y = 1, alpha197( X, Y, Z, T ) }.
% 0.74/1.28 { ! &&, ! alpha191( X, Z, T ), alpha197( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha191( X, Y, Z ), eval_terminates( Y, X, 1 ) }.
% 0.74/1.28 { ! alpha191( X, Y, Z ), alpha198( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( Y, X, 1 ), ! alpha198( X, Y, Z ), alpha191( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! alpha198( X, Y, Z ), eval_fails( Y, X, 1 ), eval_terminates( Z, X, 1 )
% 0.74/1.28 }.
% 0.74/1.28 { ! eval_fails( Y, X, 1 ), alpha198( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( Z, X, 1 ), alpha198( X, Y, Z ) }.
% 0.74/1.28 { ! alpha168( X, Y, Z ), ! X = and( T, U ), alpha180( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = and( skol41( X, T, U ), skol187( X, T, U ) ), alpha168( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! alpha180( Y, Z, skol41( X, Y, Z ) ), alpha168( X, Y, Z ) }.
% 0.74/1.28 { ! alpha180( X, Y, Z ), ! Y = 0, eval_terminates( Z, X, 0 ) }.
% 0.74/1.28 { ! &&, Y = 0, alpha180( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! eval_terminates( Z, X, 0 ), alpha180( X, Y, Z ) }.
% 0.74/1.28 { ! alpha142( X, Y, Z ), ! X = and( U, T ), alpha158( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = and( skol188( X, T, U ), skol42( X, T, U ) ), alpha142( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! alpha158( Y, Z, skol42( X, Y, Z ) ), alpha142( X, Y, Z ) }.
% 0.74/1.28 { ! alpha158( X, Y, Z ), ! Y = 0, eval_terminates( Z, X, 0 ) }.
% 0.74/1.28 { ! &&, Y = 0, alpha158( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! eval_terminates( Z, X, 0 ), alpha158( X, Y, Z ) }.
% 0.74/1.28 { ! alpha110( X, Y, Z ), ! X = or( T, U ), alpha128( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = or( skol43( X, T, U ), skol189( X, T, U ) ), alpha110( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! alpha128( Y, Z, skol43( X, Y, Z ) ), alpha110( X, Y, Z ) }.
% 0.74/1.28 { ! alpha128( X, Y, Z ), ! Y = 1, eval_terminates( Z, X, 1 ) }.
% 0.74/1.28 { ! &&, Y = 1, alpha128( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! eval_terminates( Z, X, 1 ), alpha128( X, Y, Z ) }.
% 0.74/1.28 { ! alpha65( X, Y, Z ), ! X = or( U, T ), alpha90( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = or( skol190( X, T, U ), skol44( X, T, U ) ), alpha65( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! &&, ! alpha90( Y, Z, skol44( X, Y, Z ) ), alpha65( X, Y, Z ) }.
% 0.74/1.28 { ! alpha90( X, Y, Z ), ! Y = 1, eval_terminates( Z, X, 1 ) }.
% 0.74/1.28 { ! &&, Y = 1, alpha90( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! eval_terminates( Z, X, 1 ), alpha90( X, Y, Z ) }.
% 0.74/1.28 { ! alpha6( X, Y, Z ), ! X = or( T, U ), alpha66( Y, Z, T, U ) }.
% 0.74/1.28 { ! &&, X = or( skol45( X, Y, Z ), skol191( X, Y, Z ) ), alpha6( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! &&, ! alpha66( Y, Z, skol45( X, Y, Z ), skol191( X, Y, Z ) ), alpha6( X
% 0.74/1.28 , Y, Z ) }.
% 0.74/1.28 { ! alpha66( X, Y, Z, T ), ! Y = 0, alpha36( X, Z, T ) }.
% 0.74/1.28 { ! &&, Y = 0, alpha66( X, Y, Z, T ) }.
% 0.74/1.28 { ! &&, ! alpha36( X, Z, T ), alpha66( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha36( X, Y, Z ), eval_terminates( Y, X, 0 ) }.
% 0.74/1.28 { ! alpha36( X, Y, Z ), alpha67( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( Y, X, 0 ), ! alpha67( X, Y, Z ), alpha36( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha67( X, Y, Z ), eval_fails( Y, X, 0 ), eval_terminates( Z, X, 0 ) }
% 0.74/1.28 .
% 0.74/1.28 { ! eval_fails( Y, X, 0 ), alpha67( X, Y, Z ) }.
% 0.74/1.28 { ! eval_terminates( Z, X, 0 ), alpha67( X, Y, Z ) }.
% 0.74/1.28 { ! false_succeeds( X, Y, Z ), alpha7( X, Y, Z ), alpha37( X, Y, Z ) }.
% 0.74/1.28 { ! alpha7( X, Y, Z ), false_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! alpha37( X, Y, Z ), false_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! alpha37( X, Y, Z ), alpha68( X, Y, Z ), alpha91( X, Y, Z ) }.
% 0.74/1.28 { ! alpha68( X, Y, Z ), alpha37( X, Y, Z ) }.
% 0.74/1.28 { ! alpha91( X, Y, Z ), alpha37( X, Y, Z ) }.
% 0.74/1.28 { ! alpha91( X, Y, Z ), alpha111( X, Y, Z ), alpha129( X, Y, Z ) }.
% 0.74/1.28 { ! alpha111( X, Y, Z ), alpha91( X, Y, Z ) }.
% 0.74/1.28 { ! alpha129( X, Y, Z ), alpha91( X, Y, Z ) }.
% 0.74/1.28 { ! alpha129( X, Y, Z ), alpha143( X, Y, Z ), alpha159( X, Y, Z ) }.
% 0.74/1.28 { ! alpha143( X, Y, Z ), alpha129( X, Y, Z ) }.
% 0.74/1.28 { ! alpha159( X, Y, Z ), alpha129( X, Y, Z ) }.
% 0.74/1.28 { ! alpha159( X, Y, Z ), X = p( skol46( X, T, U ) ) }.
% 0.74/1.28 { ! alpha159( X, Y, Z ), alpha169( Y, Z, skol46( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = p( T ), ! alpha169( Y, Z, T ), alpha159( X, Y, Z ) }.
% 0.74/1.28 { ! alpha169( X, Y, Z ), Y = cons( neg( p( Z ) ), X ) }.
% 0.74/1.28 { ! alpha169( X, Y, Z ), member_fails( p( Z ), X ) }.
% 0.74/1.28 { ! Y = cons( neg( p( Z ) ), X ), ! member_fails( p( Z ), X ), alpha169( X
% 0.74/1.28 , Y, Z ) }.
% 0.74/1.28 { ! alpha143( X, Y, Z ), X = neg( skol47( X, T, U ) ) }.
% 0.74/1.28 { ! alpha143( X, Y, Z ), true_succeeds( skol47( X, Y, Z ), Y, Z ) }.
% 0.74/1.28 { ! X = neg( T ), ! true_succeeds( T, Y, Z ), alpha143( X, Y, Z ) }.
% 0.74/1.28 { ! alpha111( X, Y, Z ), X = and( skol48( X, T, U ), skol192( X, T, U ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha111( X, Y, Z ), false_succeeds( skol48( X, Y, Z ), Y, Z ) }.
% 0.74/1.28 { ! X = and( T, U ), ! false_succeeds( T, Y, Z ), alpha111( X, Y, Z ) }.
% 0.74/1.28 { ! alpha68( X, Y, Z ), X = and( skol193( X, T, U ), skol49( X, T, U ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha68( X, Y, Z ), false_succeeds( skol49( X, Y, Z ), Y, Z ) }.
% 0.74/1.28 { ! X = and( U, T ), ! false_succeeds( T, Y, Z ), alpha68( X, Y, Z ) }.
% 0.74/1.28 { ! alpha7( X, Y, Z ), X = or( skol50( X, Y, Z ), skol194( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha7( X, Y, Z ), alpha38( Y, Z, skol50( X, Y, Z ), skol194( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { ! X = or( T, U ), ! alpha38( Y, Z, T, U ), alpha7( X, Y, Z ) }.
% 0.74/1.28 { ! alpha38( X, Y, Z, T ), false_succeeds( T, skol51( U, Y, W, T ), Y ) }.
% 0.74/1.28 { ! alpha38( X, Y, Z, T ), false_succeeds( Z, X, skol51( X, Y, Z, T ) ) }.
% 0.74/1.28 { ! false_succeeds( Z, X, U ), ! false_succeeds( T, U, Y ), alpha38( X, Y,
% 0.74/1.28 Z, T ) }.
% 0.74/1.28 { ! false_fails( X, Y, Z ), alpha8( X, Y, Z ) }.
% 0.74/1.28 { ! false_fails( X, Y, Z ), alpha39( X, Y, Z ) }.
% 0.74/1.28 { ! alpha8( X, Y, Z ), ! alpha39( X, Y, Z ), false_fails( X, Y, Z ) }.
% 0.74/1.28 { ! alpha39( X, Y, Z ), alpha69( X, Y, Z ) }.
% 0.74/1.28 { ! alpha39( X, Y, Z ), alpha92( X, Y, Z ) }.
% 0.74/1.28 { ! alpha69( X, Y, Z ), ! alpha92( X, Y, Z ), alpha39( X, Y, Z ) }.
% 0.74/1.28 { ! alpha92( X, Y, Z ), alpha112( X, Y, Z ) }.
% 0.74/1.28 { ! alpha92( X, Y, Z ), alpha130( X, Y, Z ) }.
% 0.74/1.28 { ! alpha112( X, Y, Z ), ! alpha130( X, Y, Z ), alpha92( X, Y, Z ) }.
% 0.74/1.28 { ! alpha130( X, Y, Z ), alpha144( X, Y, Z ) }.
% 0.74/1.28 { ! alpha130( X, Y, Z ), alpha160( X, Y, Z ) }.
% 0.74/1.28 { ! alpha144( X, Y, Z ), ! alpha160( X, Y, Z ), alpha130( X, Y, Z ) }.
% 0.74/1.28 { ! alpha160( X, Y, Z ), ! X = p( T ), alpha170( Y, Z, T ) }.
% 0.74/1.28 { X = p( skol52( X, T, U ) ), alpha160( X, Y, Z ) }.
% 0.74/1.28 { ! alpha170( Y, Z, skol52( X, Y, Z ) ), alpha160( X, Y, Z ) }.
% 0.74/1.28 { ! alpha170( X, Y, Z ), ! Y = cons( neg( p( Z ) ), X ), member_succeeds( p
% 0.74/1.28 ( Z ), X ) }.
% 0.74/1.28 { Y = cons( neg( p( Z ) ), X ), alpha170( X, Y, Z ) }.
% 0.74/1.28 { ! member_succeeds( p( Z ), X ), alpha170( X, Y, Z ) }.
% 0.74/1.28 { ! alpha144( X, Y, Z ), ! X = neg( T ), true_fails( T, Y, Z ) }.
% 0.74/1.28 { X = neg( skol53( X, T, U ) ), alpha144( X, Y, Z ) }.
% 0.74/1.28 { ! true_fails( skol53( X, Y, Z ), Y, Z ), alpha144( X, Y, Z ) }.
% 0.74/1.28 { ! alpha112( X, Y, Z ), ! X = and( T, U ), false_fails( T, Y, Z ) }.
% 0.74/1.28 { X = and( skol54( X, T, U ), skol195( X, T, U ) ), alpha112( X, Y, Z ) }.
% 0.74/1.28 { ! false_fails( skol54( X, Y, Z ), Y, Z ), alpha112( X, Y, Z ) }.
% 0.74/1.28 { ! alpha69( X, Y, Z ), ! X = and( U, T ), false_fails( T, Y, Z ) }.
% 0.74/1.28 { X = and( skol196( X, T, U ), skol55( X, T, U ) ), alpha69( X, Y, Z ) }.
% 0.74/1.28 { ! false_fails( skol55( X, Y, Z ), Y, Z ), alpha69( X, Y, Z ) }.
% 0.74/1.28 { ! alpha8( X, Y, Z ), ! X = or( T, U ), alpha40( Y, Z, T, U ) }.
% 0.74/1.28 { X = or( skol56( X, Y, Z ), skol197( X, Y, Z ) ), alpha8( X, Y, Z ) }.
% 0.74/1.28 { ! alpha40( Y, Z, skol56( X, Y, Z ), skol197( X, Y, Z ) ), alpha8( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha40( X, Y, Z, T ), false_fails( Z, X, U ), false_fails( T, U, Y ) }
% 0.74/1.28 .
% 0.74/1.28 { ! false_fails( T, skol57( U, Y, W, T ), Y ), alpha40( X, Y, Z, T ) }.
% 0.74/1.28 { ! false_fails( Z, X, skol57( X, Y, Z, T ) ), alpha40( X, Y, Z, T ) }.
% 0.74/1.28 { ! false_terminates( X, Y, Z ), alpha41( X, Y, Z ) }.
% 0.74/1.28 { ! false_terminates( X, Y, Z ), alpha70( X, Y, Z ) }.
% 0.74/1.28 { ! alpha41( X, Y, Z ), ! alpha70( X, Y, Z ), false_terminates( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha70( X, Y, Z ), alpha93( X, Y, Z ) }.
% 0.74/1.28 { ! alpha70( X, Y, Z ), alpha113( X, Y, Z ) }.
% 0.74/1.28 { ! alpha93( X, Y, Z ), ! alpha113( X, Y, Z ), alpha70( X, Y, Z ) }.
% 0.74/1.28 { ! alpha113( X, Y, Z ), alpha131( X, Y, Z ) }.
% 0.74/1.28 { ! alpha113( X, Y, Z ), alpha145( X, Y, Z ) }.
% 0.74/1.28 { ! alpha131( X, Y, Z ), ! alpha145( X, Y, Z ), alpha113( X, Y, Z ) }.
% 0.74/1.28 { ! alpha145( X, Y, Z ), alpha161( X, Y, Z ) }.
% 0.74/1.28 { ! alpha145( X, Y, Z ), alpha171( X, Y, Z ) }.
% 0.74/1.28 { ! alpha161( X, Y, Z ), ! alpha171( X, Y, Z ), alpha145( X, Y, Z ) }.
% 0.74/1.28 { ! alpha171( X, Y, Z ), ! X = p( T ), alpha181( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = p( skol58( X, T, U ) ), alpha171( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha181( Y, Z, skol58( X, Y, Z ) ), alpha171( X, Y, Z ) }.
% 0.74/1.28 { ! alpha181( X, Y, Z ), ! Y = cons( neg( p( Z ) ), X ), alpha9( X, Z ) }.
% 0.74/1.28 { ! &&, Y = cons( neg( p( Z ) ), X ), alpha181( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha9( X, Z ), alpha181( X, Y, Z ) }.
% 0.74/1.28 { ! alpha161( X, Y, Z ), ! X = neg( T ), true_terminates( T, Y, Z ) }.
% 0.74/1.28 { ! &&, X = neg( skol59( X, T, U ) ), alpha161( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! true_terminates( skol59( X, Y, Z ), Y, Z ), alpha161( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha131( X, Y, Z ), ! X = and( T, U ), false_terminates( T, Y, Z ) }.
% 0.74/1.28 { ! &&, X = and( skol60( X, T, U ), skol198( X, T, U ) ), alpha131( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! false_terminates( skol60( X, Y, Z ), Y, Z ), alpha131( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! alpha93( X, Y, Z ), ! X = and( U, T ), false_terminates( T, Y, Z ) }.
% 0.74/1.28 { ! &&, X = and( skol199( X, T, U ), skol61( X, T, U ) ), alpha93( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! false_terminates( skol61( X, Y, Z ), Y, Z ), alpha93( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha41( X, Y, Z ), ! X = or( T, U ), alpha71( Y, Z, T, U ) }.
% 0.74/1.28 { ! &&, X = or( skol62( X, Y, Z ), skol200( X, Y, Z ) ), alpha41( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! &&, ! alpha71( Y, Z, skol62( X, Y, Z ), skol200( X, Y, Z ) ), alpha41(
% 0.74/1.28 X, Y, Z ) }.
% 0.74/1.28 { ! alpha71( X, Y, Z, T ), false_terminates( Z, X, U ) }.
% 0.74/1.28 { ! alpha71( X, Y, Z, T ), alpha94( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! false_terminates( Z, X, skol63( X, Y, Z, T ) ), ! alpha94( X, Y, Z, T,
% 0.74/1.28 skol63( X, Y, Z, T ) ), alpha71( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha94( X, Y, Z, T, U ), false_fails( Z, X, U ), false_terminates( T,
% 0.74/1.28 U, Y ) }.
% 0.74/1.28 { ! false_fails( Z, X, U ), alpha94( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! false_terminates( T, U, Y ), alpha94( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! alpha9( X, Y ), member_terminates( p( Y ), X ) }.
% 0.74/1.28 { ! alpha9( X, Y ), alpha42( X, Y ) }.
% 0.74/1.28 { ! member_terminates( p( Y ), X ), ! alpha42( X, Y ), alpha9( X, Y ) }.
% 0.74/1.28 { ! alpha42( X, Y ), gr( p( Y ) ) }.
% 0.74/1.28 { ! alpha42( X, Y ), gr( X ) }.
% 0.74/1.28 { ! gr( p( Y ) ), ! gr( X ), alpha42( X, Y ) }.
% 0.74/1.28 { ! true_succeeds( X, Y, Z ), alpha10( X, Y, Z ), alpha43( X, Y, Z ) }.
% 0.74/1.28 { ! alpha10( X, Y, Z ), true_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! alpha43( X, Y, Z ), true_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! alpha43( X, Y, Z ), alpha72( X, Y, Z ), alpha95( X, Y, Z ) }.
% 0.74/1.28 { ! alpha72( X, Y, Z ), alpha43( X, Y, Z ) }.
% 0.74/1.28 { ! alpha95( X, Y, Z ), alpha43( X, Y, Z ) }.
% 0.74/1.28 { ! alpha95( X, Y, Z ), alpha114( X, Y, Z ), alpha132( X, Y, Z ) }.
% 0.74/1.28 { ! alpha114( X, Y, Z ), alpha95( X, Y, Z ) }.
% 0.74/1.28 { ! alpha132( X, Y, Z ), alpha95( X, Y, Z ) }.
% 0.74/1.28 { ! alpha132( X, Y, Z ), alpha146( X, Y, Z ), alpha162( X, Y, Z ) }.
% 0.74/1.28 { ! alpha146( X, Y, Z ), alpha132( X, Y, Z ) }.
% 0.74/1.28 { ! alpha162( X, Y, Z ), alpha132( X, Y, Z ) }.
% 0.74/1.28 { ! alpha162( X, Y, Z ), X = p( skol64( X, T, U ) ) }.
% 0.74/1.28 { ! alpha162( X, Y, Z ), alpha172( Y, Z, skol64( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = p( T ), ! alpha172( Y, Z, T ), alpha162( X, Y, Z ) }.
% 0.74/1.28 { ! alpha172( X, Y, Z ), Y = cons( p( Z ), X ) }.
% 0.74/1.28 { ! alpha172( X, Y, Z ), member_fails( neg( p( Z ) ), X ) }.
% 0.74/1.28 { ! Y = cons( p( Z ), X ), ! member_fails( neg( p( Z ) ), X ), alpha172( X
% 0.74/1.28 , Y, Z ) }.
% 0.74/1.28 { ! alpha146( X, Y, Z ), X = neg( skol65( X, T, U ) ) }.
% 0.74/1.28 { ! alpha146( X, Y, Z ), false_succeeds( skol65( X, Y, Z ), Y, Z ) }.
% 0.74/1.28 { ! X = neg( T ), ! false_succeeds( T, Y, Z ), alpha146( X, Y, Z ) }.
% 0.74/1.28 { ! alpha114( X, Y, Z ), X = and( skol66( X, Y, Z ), skol201( X, Y, Z ) ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha114( X, Y, Z ), alpha133( Y, Z, skol66( X, Y, Z ), skol201( X, Y,
% 0.74/1.28 Z ) ) }.
% 0.74/1.28 { ! X = and( T, U ), ! alpha133( Y, Z, T, U ), alpha114( X, Y, Z ) }.
% 0.74/1.28 { ! alpha133( X, Y, Z, T ), true_succeeds( T, skol67( U, Y, W, T ), Y ) }.
% 0.74/1.28 { ! alpha133( X, Y, Z, T ), true_succeeds( Z, X, skol67( X, Y, Z, T ) ) }.
% 0.74/1.28 { ! true_succeeds( Z, X, U ), ! true_succeeds( T, U, Y ), alpha133( X, Y, Z
% 0.74/1.28 , T ) }.
% 0.74/1.28 { ! alpha72( X, Y, Z ), X = or( skol68( X, T, U ), skol202( X, T, U ) ) }.
% 0.74/1.28 { ! alpha72( X, Y, Z ), true_succeeds( skol68( X, Y, Z ), Y, Z ) }.
% 0.74/1.28 { ! X = or( T, U ), ! true_succeeds( T, Y, Z ), alpha72( X, Y, Z ) }.
% 0.74/1.28 { ! alpha10( X, Y, Z ), X = or( skol203( X, T, U ), skol69( X, T, U ) ) }.
% 0.74/1.28 { ! alpha10( X, Y, Z ), true_succeeds( skol69( X, Y, Z ), Y, Z ) }.
% 0.74/1.28 { ! X = or( U, T ), ! true_succeeds( T, Y, Z ), alpha10( X, Y, Z ) }.
% 0.74/1.28 { ! true_fails( X, Y, Z ), alpha11( X, Y, Z ) }.
% 0.74/1.28 { ! true_fails( X, Y, Z ), alpha44( X, Y, Z ) }.
% 0.74/1.28 { ! alpha11( X, Y, Z ), ! alpha44( X, Y, Z ), true_fails( X, Y, Z ) }.
% 0.74/1.28 { ! alpha44( X, Y, Z ), alpha73( X, Y, Z ) }.
% 0.74/1.28 { ! alpha44( X, Y, Z ), alpha96( X, Y, Z ) }.
% 0.74/1.28 { ! alpha73( X, Y, Z ), ! alpha96( X, Y, Z ), alpha44( X, Y, Z ) }.
% 0.74/1.28 { ! alpha96( X, Y, Z ), alpha115( X, Y, Z ) }.
% 0.74/1.28 { ! alpha96( X, Y, Z ), alpha134( X, Y, Z ) }.
% 0.74/1.28 { ! alpha115( X, Y, Z ), ! alpha134( X, Y, Z ), alpha96( X, Y, Z ) }.
% 0.74/1.28 { ! alpha134( X, Y, Z ), alpha147( X, Y, Z ) }.
% 0.74/1.28 { ! alpha134( X, Y, Z ), alpha163( X, Y, Z ) }.
% 0.74/1.28 { ! alpha147( X, Y, Z ), ! alpha163( X, Y, Z ), alpha134( X, Y, Z ) }.
% 0.74/1.28 { ! alpha163( X, Y, Z ), ! X = p( T ), alpha173( Y, Z, T ) }.
% 0.74/1.28 { X = p( skol70( X, T, U ) ), alpha163( X, Y, Z ) }.
% 0.74/1.28 { ! alpha173( Y, Z, skol70( X, Y, Z ) ), alpha163( X, Y, Z ) }.
% 0.74/1.28 { ! alpha173( X, Y, Z ), ! Y = cons( p( Z ), X ), member_succeeds( neg( p(
% 0.74/1.28 Z ) ), X ) }.
% 0.74/1.28 { Y = cons( p( Z ), X ), alpha173( X, Y, Z ) }.
% 0.74/1.28 { ! member_succeeds( neg( p( Z ) ), X ), alpha173( X, Y, Z ) }.
% 0.74/1.28 { ! alpha147( X, Y, Z ), ! X = neg( T ), false_fails( T, Y, Z ) }.
% 0.74/1.28 { X = neg( skol71( X, T, U ) ), alpha147( X, Y, Z ) }.
% 0.74/1.28 { ! false_fails( skol71( X, Y, Z ), Y, Z ), alpha147( X, Y, Z ) }.
% 0.74/1.28 { ! alpha115( X, Y, Z ), ! X = and( T, U ), alpha135( Y, Z, T, U ) }.
% 0.74/1.28 { X = and( skol72( X, Y, Z ), skol204( X, Y, Z ) ), alpha115( X, Y, Z ) }.
% 0.74/1.28 { ! alpha135( Y, Z, skol72( X, Y, Z ), skol204( X, Y, Z ) ), alpha115( X, Y
% 0.74/1.28 , Z ) }.
% 0.74/1.28 { ! alpha135( X, Y, Z, T ), true_fails( Z, X, U ), true_fails( T, U, Y ) }
% 0.74/1.28 .
% 0.74/1.28 { ! true_fails( T, skol73( U, Y, W, T ), Y ), alpha135( X, Y, Z, T ) }.
% 0.74/1.28 { ! true_fails( Z, X, skol73( X, Y, Z, T ) ), alpha135( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha73( X, Y, Z ), ! X = or( T, U ), true_fails( T, Y, Z ) }.
% 0.74/1.28 { X = or( skol74( X, T, U ), skol205( X, T, U ) ), alpha73( X, Y, Z ) }.
% 0.74/1.28 { ! true_fails( skol74( X, Y, Z ), Y, Z ), alpha73( X, Y, Z ) }.
% 0.74/1.28 { ! alpha11( X, Y, Z ), ! X = or( U, T ), true_fails( T, Y, Z ) }.
% 0.74/1.28 { X = or( skol206( X, T, U ), skol75( X, T, U ) ), alpha11( X, Y, Z ) }.
% 0.74/1.28 { ! true_fails( skol75( X, Y, Z ), Y, Z ), alpha11( X, Y, Z ) }.
% 0.74/1.28 { ! true_terminates( X, Y, Z ), alpha45( X, Y, Z ) }.
% 0.74/1.28 { ! true_terminates( X, Y, Z ), alpha74( X, Y, Z ) }.
% 0.74/1.28 { ! alpha45( X, Y, Z ), ! alpha74( X, Y, Z ), true_terminates( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha74( X, Y, Z ), alpha97( X, Y, Z ) }.
% 0.74/1.28 { ! alpha74( X, Y, Z ), alpha116( X, Y, Z ) }.
% 0.74/1.28 { ! alpha97( X, Y, Z ), ! alpha116( X, Y, Z ), alpha74( X, Y, Z ) }.
% 0.74/1.28 { ! alpha116( X, Y, Z ), alpha136( X, Y, Z ) }.
% 0.74/1.28 { ! alpha116( X, Y, Z ), alpha148( X, Y, Z ) }.
% 0.74/1.28 { ! alpha136( X, Y, Z ), ! alpha148( X, Y, Z ), alpha116( X, Y, Z ) }.
% 0.74/1.28 { ! alpha148( X, Y, Z ), alpha164( X, Y, Z ) }.
% 0.74/1.28 { ! alpha148( X, Y, Z ), alpha174( X, Y, Z ) }.
% 0.74/1.28 { ! alpha164( X, Y, Z ), ! alpha174( X, Y, Z ), alpha148( X, Y, Z ) }.
% 0.74/1.28 { ! alpha174( X, Y, Z ), ! X = p( T ), alpha182( Y, Z, T ) }.
% 0.74/1.28 { ! &&, X = p( skol76( X, T, U ) ), alpha174( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha182( Y, Z, skol76( X, Y, Z ) ), alpha174( X, Y, Z ) }.
% 0.74/1.28 { ! alpha182( X, Y, Z ), ! Y = cons( p( Z ), X ), alpha12( X, Z ) }.
% 0.74/1.28 { ! &&, Y = cons( p( Z ), X ), alpha182( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! alpha12( X, Z ), alpha182( X, Y, Z ) }.
% 0.74/1.28 { ! alpha164( X, Y, Z ), ! X = neg( T ), false_terminates( T, Y, Z ) }.
% 0.74/1.28 { ! &&, X = neg( skol77( X, T, U ) ), alpha164( X, Y, Z ) }.
% 0.74/1.28 { ! &&, ! false_terminates( skol77( X, Y, Z ), Y, Z ), alpha164( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! alpha136( X, Y, Z ), ! X = and( T, U ), alpha149( Y, Z, T, U ) }.
% 0.74/1.28 { ! &&, X = and( skol78( X, Y, Z ), skol207( X, Y, Z ) ), alpha136( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, ! alpha149( Y, Z, skol78( X, Y, Z ), skol207( X, Y, Z ) ), alpha136
% 0.74/1.28 ( X, Y, Z ) }.
% 0.74/1.28 { ! alpha149( X, Y, Z, T ), true_terminates( Z, X, U ) }.
% 0.74/1.28 { ! alpha149( X, Y, Z, T ), alpha165( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! true_terminates( Z, X, skol79( X, Y, Z, T ) ), ! alpha165( X, Y, Z, T,
% 0.74/1.28 skol79( X, Y, Z, T ) ), alpha149( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha165( X, Y, Z, T, U ), true_fails( Z, X, U ), true_terminates( T, U
% 0.74/1.28 , Y ) }.
% 0.74/1.28 { ! true_fails( Z, X, U ), alpha165( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! true_terminates( T, U, Y ), alpha165( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! alpha97( X, Y, Z ), ! X = or( T, U ), true_terminates( T, Y, Z ) }.
% 0.74/1.28 { ! &&, X = or( skol80( X, T, U ), skol208( X, T, U ) ), alpha97( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! &&, ! true_terminates( skol80( X, Y, Z ), Y, Z ), alpha97( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha45( X, Y, Z ), ! X = or( U, T ), true_terminates( T, Y, Z ) }.
% 0.74/1.28 { ! &&, X = or( skol209( X, T, U ), skol81( X, T, U ) ), alpha45( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! &&, ! true_terminates( skol81( X, Y, Z ), Y, Z ), alpha45( X, Y, Z ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha12( X, Y ), member_terminates( neg( p( Y ) ), X ) }.
% 0.74/1.28 { ! alpha12( X, Y ), alpha46( X, Y ) }.
% 0.74/1.28 { ! member_terminates( neg( p( Y ) ), X ), ! alpha46( X, Y ), alpha12( X, Y
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha46( X, Y ), gr( neg( p( Y ) ) ) }.
% 0.74/1.28 { ! alpha46( X, Y ), gr( X ) }.
% 0.74/1.28 { ! gr( neg( p( Y ) ) ), ! gr( X ), alpha46( X, Y ) }.
% 0.74/1.28 { ! satisfiable_succeeds( X ), true_succeeds( X, nil, skol82( X ) ) }.
% 0.74/1.28 { ! true_succeeds( X, nil, Y ), satisfiable_succeeds( X ) }.
% 0.74/1.28 { ! satisfiable_fails( X ), true_fails( X, nil, Y ) }.
% 0.74/1.28 { ! true_fails( X, nil, skol83( X ) ), satisfiable_fails( X ) }.
% 0.74/1.28 { ! satisfiable_terminates( X ), true_terminates( X, nil, Y ) }.
% 0.74/1.28 { ! true_terminates( X, nil, skol84( X ) ), satisfiable_terminates( X ) }.
% 0.74/1.28 { ! valid_succeeds( X ), satisfiable_fails( neg( X ) ) }.
% 0.74/1.28 { ! satisfiable_fails( neg( X ) ), valid_succeeds( X ) }.
% 0.74/1.28 { ! valid_fails( X ), satisfiable_succeeds( neg( X ) ) }.
% 0.74/1.28 { ! satisfiable_succeeds( neg( X ) ), valid_fails( X ) }.
% 0.74/1.28 { ! valid_terminates( X ), satisfiable_terminates( neg( X ) ) }.
% 0.74/1.28 { ! valid_terminates( X ), gr( neg( X ) ) }.
% 0.74/1.28 { ! satisfiable_terminates( neg( X ) ), ! gr( neg( X ) ), valid_terminates
% 0.74/1.28 ( X ) }.
% 0.74/1.28 { ! incon_succeeds( X ), member_succeeds( p( skol85( X ) ), X ) }.
% 0.74/1.28 { ! incon_succeeds( X ), member_succeeds( neg( p( skol85( X ) ) ), X ) }.
% 0.74/1.28 { ! member_succeeds( p( Y ), X ), ! member_succeeds( neg( p( Y ) ), X ),
% 0.74/1.28 incon_succeeds( X ) }.
% 0.74/1.28 { ! incon_fails( X ), member_fails( p( Y ), X ), member_fails( neg( p( Y )
% 0.74/1.28 ), X ) }.
% 0.74/1.28 { ! member_fails( p( skol86( X ) ), X ), incon_fails( X ) }.
% 0.74/1.28 { ! member_fails( neg( p( skol86( X ) ) ), X ), incon_fails( X ) }.
% 0.74/1.28 { ! incon_terminates( X ), member_terminates( p( Y ), X ) }.
% 0.74/1.28 { ! incon_terminates( X ), alpha13( X, Y ) }.
% 0.74/1.28 { ! member_terminates( p( skol87( X ) ), X ), ! alpha13( X, skol87( X ) ),
% 0.74/1.28 incon_terminates( X ) }.
% 0.74/1.28 { ! alpha13( X, Y ), member_fails( p( Y ), X ), member_terminates( neg( p(
% 0.74/1.28 Y ) ), X ) }.
% 0.74/1.28 { ! member_fails( p( Y ), X ), alpha13( X, Y ) }.
% 0.74/1.28 { ! member_terminates( neg( p( Y ) ), X ), alpha13( X, Y ) }.
% 0.74/1.28 { ! interpretation_succeeds( X ), literal_list_succeeds( X ) }.
% 0.74/1.28 { ! interpretation_succeeds( X ), incon_fails( X ) }.
% 0.74/1.28 { ! literal_list_succeeds( X ), ! incon_fails( X ), interpretation_succeeds
% 0.74/1.28 ( X ) }.
% 0.74/1.28 { ! interpretation_fails( X ), literal_list_fails( X ), incon_succeeds( X )
% 0.74/1.28 }.
% 0.74/1.28 { ! literal_list_fails( X ), interpretation_fails( X ) }.
% 0.74/1.28 { ! incon_succeeds( X ), interpretation_fails( X ) }.
% 0.74/1.28 { ! interpretation_terminates( X ), literal_list_terminates( X ) }.
% 0.74/1.28 { ! interpretation_terminates( X ), alpha14( X ) }.
% 0.74/1.28 { ! literal_list_terminates( X ), ! alpha14( X ), interpretation_terminates
% 0.74/1.28 ( X ) }.
% 0.74/1.28 { ! alpha14( X ), literal_list_fails( X ), alpha47( X ) }.
% 0.74/1.28 { ! literal_list_fails( X ), alpha14( X ) }.
% 0.74/1.28 { ! alpha47( X ), alpha14( X ) }.
% 0.74/1.28 { ! alpha47( X ), incon_terminates( X ) }.
% 0.74/1.28 { ! alpha47( X ), gr( X ) }.
% 0.74/1.28 { ! incon_terminates( X ), ! gr( X ), alpha47( X ) }.
% 0.74/1.28 { ! literal_list_succeeds( X ), alpha15( X ), X = nil }.
% 0.74/1.28 { ! alpha15( X ), literal_list_succeeds( X ) }.
% 0.74/1.28 { ! X = nil, literal_list_succeeds( X ) }.
% 0.74/1.28 { ! alpha15( X ), X = cons( skol88( X ), skol210( X ) ) }.
% 0.74/1.28 { ! alpha15( X ), alpha48( skol88( X ), skol210( X ) ) }.
% 0.74/1.28 { ! X = cons( Y, Z ), ! alpha48( Y, Z ), alpha15( X ) }.
% 0.74/1.28 { ! alpha48( X, Y ), literal_succeeds( X ) }.
% 0.74/1.28 { ! alpha48( X, Y ), literal_list_succeeds( Y ) }.
% 0.74/1.28 { ! literal_succeeds( X ), ! literal_list_succeeds( Y ), alpha48( X, Y ) }
% 0.74/1.28 .
% 0.74/1.28 { ! literal_list_fails( X ), alpha16( X ) }.
% 0.74/1.28 { ! literal_list_fails( X ), ! X = nil }.
% 0.74/1.28 { ! alpha16( X ), X = nil, literal_list_fails( X ) }.
% 0.74/1.28 { ! alpha16( X ), ! X = cons( Y, Z ), alpha49( Y, Z ) }.
% 0.74/1.28 { X = cons( skol89( X ), skol211( X ) ), alpha16( X ) }.
% 0.74/1.28 { ! alpha49( skol89( X ), skol211( X ) ), alpha16( X ) }.
% 0.74/1.28 { ! alpha49( X, Y ), literal_fails( X ), literal_list_fails( Y ) }.
% 0.74/1.28 { ! literal_fails( X ), alpha49( X, Y ) }.
% 0.74/1.28 { ! literal_list_fails( Y ), alpha49( X, Y ) }.
% 0.74/1.28 { ! literal_list_terminates( X ), ! X = cons( Y, Z ), alpha17( Y, Z ) }.
% 0.74/1.28 { ! &&, X = cons( skol90( X ), skol212( X ) ), ! &&,
% 0.74/1.28 literal_list_terminates( X ) }.
% 0.74/1.28 { ! &&, ! alpha17( skol90( X ), skol212( X ) ), ! &&,
% 0.74/1.28 literal_list_terminates( X ) }.
% 0.74/1.28 { ! alpha17( X, Y ), literal_terminates( X ) }.
% 0.74/1.28 { ! alpha17( X, Y ), alpha50( X, Y ) }.
% 0.74/1.28 { ! literal_terminates( X ), ! alpha50( X, Y ), alpha17( X, Y ) }.
% 0.74/1.28 { ! alpha50( X, Y ), literal_fails( X ), literal_list_terminates( Y ) }.
% 0.74/1.28 { ! literal_fails( X ), alpha50( X, Y ) }.
% 0.74/1.28 { ! literal_list_terminates( Y ), alpha50( X, Y ) }.
% 0.74/1.28 { ! literal_succeeds( X ), X = neg( p( skol91( X ) ) ), X = p( skol213( X )
% 0.74/1.28 ) }.
% 0.74/1.28 { ! X = neg( p( Y ) ), literal_succeeds( X ) }.
% 0.74/1.28 { ! X = p( Y ), literal_succeeds( X ) }.
% 0.74/1.28 { ! literal_fails( X ), ! X = neg( p( Y ) ) }.
% 0.74/1.28 { ! literal_fails( X ), ! X = p( Y ) }.
% 0.74/1.28 { X = neg( p( skol92( X ) ) ), X = p( skol214( X ) ), literal_fails( X ) }
% 0.74/1.28 .
% 0.74/1.28 { ! &&, ! &&, literal_terminates( X ) }.
% 0.74/1.28 { ! formula_succeeds( X ), alpha18( X ), alpha51( X ) }.
% 0.74/1.28 { ! alpha18( X ), formula_succeeds( X ) }.
% 0.74/1.28 { ! alpha51( X ), formula_succeeds( X ) }.
% 0.74/1.28 { ! alpha51( X ), alpha75( X ), alpha98( X ) }.
% 0.74/1.28 { ! alpha75( X ), alpha51( X ) }.
% 0.74/1.28 { ! alpha98( X ), alpha51( X ) }.
% 0.74/1.28 { ! alpha98( X ), alpha117( X ), X = p( skol93( X ) ) }.
% 0.74/1.28 { ! alpha117( X ), alpha98( X ) }.
% 0.74/1.28 { ! X = p( Y ), alpha98( X ) }.
% 0.74/1.28 { ! alpha117( X ), formula_succeeds( skol94( Y ) ) }.
% 0.74/1.28 { ! alpha117( X ), X = neg( skol94( X ) ) }.
% 0.74/1.28 { ! X = neg( Y ), ! formula_succeeds( Y ), alpha117( X ) }.
% 0.74/1.28 { ! alpha75( X ), X = and( skol95( X ), skol215( X ) ) }.
% 0.74/1.28 { ! alpha75( X ), alpha99( skol95( X ), skol215( X ) ) }.
% 0.74/1.28 { ! X = and( Y, Z ), ! alpha99( Y, Z ), alpha75( X ) }.
% 0.74/1.28 { ! alpha99( X, Y ), formula_succeeds( X ) }.
% 0.74/1.28 { ! alpha99( X, Y ), formula_succeeds( Y ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! formula_succeeds( Y ), alpha99( X, Y ) }.
% 0.74/1.28 { ! alpha18( X ), X = or( skol96( X ), skol216( X ) ) }.
% 0.74/1.28 { ! alpha18( X ), alpha52( skol96( X ), skol216( X ) ) }.
% 0.74/1.28 { ! X = or( Y, Z ), ! alpha52( Y, Z ), alpha18( X ) }.
% 0.74/1.28 { ! alpha52( X, Y ), formula_succeeds( X ) }.
% 0.74/1.28 { ! alpha52( X, Y ), formula_succeeds( Y ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! formula_succeeds( Y ), alpha52( X, Y ) }.
% 0.74/1.28 { ! formula_fails( X ), alpha19( X ) }.
% 0.74/1.28 { ! formula_fails( X ), alpha53( X ) }.
% 0.74/1.28 { ! alpha19( X ), ! alpha53( X ), formula_fails( X ) }.
% 0.74/1.28 { ! alpha53( X ), alpha76( X ) }.
% 0.74/1.28 { ! alpha53( X ), alpha100( X ) }.
% 0.74/1.28 { ! alpha76( X ), ! alpha100( X ), alpha53( X ) }.
% 0.74/1.28 { ! alpha100( X ), alpha118( X ) }.
% 0.74/1.28 { ! alpha100( X ), ! X = p( Y ) }.
% 0.74/1.28 { ! alpha118( X ), X = p( skol97( X ) ), alpha100( X ) }.
% 0.74/1.28 { ! alpha118( X ), ! X = neg( Y ), formula_fails( Y ) }.
% 0.74/1.28 { ! formula_fails( skol98( Y ) ), alpha118( X ) }.
% 0.74/1.28 { X = neg( skol98( X ) ), alpha118( X ) }.
% 0.74/1.28 { ! alpha76( X ), ! X = and( Y, Z ), alpha101( Y, Z ) }.
% 0.74/1.28 { X = and( skol99( X ), skol217( X ) ), alpha76( X ) }.
% 0.74/1.28 { ! alpha101( skol99( X ), skol217( X ) ), alpha76( X ) }.
% 0.74/1.28 { ! alpha101( X, Y ), formula_fails( X ), formula_fails( Y ) }.
% 0.74/1.28 { ! formula_fails( X ), alpha101( X, Y ) }.
% 0.74/1.28 { ! formula_fails( Y ), alpha101( X, Y ) }.
% 0.74/1.28 { ! alpha19( X ), ! X = or( Y, Z ), alpha54( Y, Z ) }.
% 0.74/1.28 { X = or( skol100( X ), skol218( X ) ), alpha19( X ) }.
% 0.74/1.28 { ! alpha54( skol100( X ), skol218( X ) ), alpha19( X ) }.
% 0.74/1.28 { ! alpha54( X, Y ), formula_fails( X ), formula_fails( Y ) }.
% 0.74/1.28 { ! formula_fails( X ), alpha54( X, Y ) }.
% 0.74/1.28 { ! formula_fails( Y ), alpha54( X, Y ) }.
% 0.74/1.28 { ! formula_terminates( X ), alpha20( X ) }.
% 0.74/1.28 { ! formula_terminates( X ), alpha55( X ) }.
% 0.74/1.28 { ! alpha20( X ), ! alpha55( X ), formula_terminates( X ) }.
% 0.74/1.28 { ! alpha55( X ), alpha77( X ) }.
% 0.74/1.28 { ! alpha55( X ), alpha102( X ) }.
% 0.74/1.28 { ! alpha77( X ), ! alpha102( X ), alpha55( X ) }.
% 0.74/1.28 { ! alpha102( X ), ! X = neg( Y ), formula_terminates( Y ) }.
% 0.74/1.28 { ! &&, ! formula_terminates( skol101( Y ) ), ! &&, alpha102( X ) }.
% 0.74/1.28 { ! &&, X = neg( skol101( X ) ), ! &&, alpha102( X ) }.
% 0.74/1.28 { ! alpha77( X ), ! X = and( Y, Z ), alpha103( Y, Z ) }.
% 0.74/1.28 { ! &&, X = and( skol102( X ), skol219( X ) ), alpha77( X ) }.
% 0.74/1.28 { ! &&, ! alpha103( skol102( X ), skol219( X ) ), alpha77( X ) }.
% 0.74/1.28 { ! alpha103( X, Y ), formula_terminates( X ) }.
% 0.74/1.28 { ! alpha103( X, Y ), alpha119( X, Y ) }.
% 0.74/1.28 { ! formula_terminates( X ), ! alpha119( X, Y ), alpha103( X, Y ) }.
% 0.74/1.28 { ! alpha119( X, Y ), formula_fails( X ), formula_terminates( Y ) }.
% 0.74/1.28 { ! formula_fails( X ), alpha119( X, Y ) }.
% 0.74/1.28 { ! formula_terminates( Y ), alpha119( X, Y ) }.
% 0.74/1.28 { ! alpha20( X ), ! X = or( Y, Z ), alpha56( Y, Z ) }.
% 0.74/1.28 { ! &&, X = or( skol103( X ), skol220( X ) ), alpha20( X ) }.
% 0.74/1.28 { ! &&, ! alpha56( skol103( X ), skol220( X ) ), alpha20( X ) }.
% 0.74/1.28 { ! alpha56( X, Y ), formula_terminates( X ) }.
% 0.74/1.28 { ! alpha56( X, Y ), alpha78( X, Y ) }.
% 0.74/1.28 { ! formula_terminates( X ), ! alpha78( X, Y ), alpha56( X, Y ) }.
% 0.74/1.28 { ! alpha78( X, Y ), formula_fails( X ), formula_terminates( Y ) }.
% 0.74/1.28 { ! formula_fails( X ), alpha78( X, Y ) }.
% 0.74/1.28 { ! formula_terminates( Y ), alpha78( X, Y ) }.
% 0.74/1.28 { ! member_succeeds( X, Y ), alpha21( X, Y ), Y = cons( X, skol104( X, Y )
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha21( X, Y ), member_succeeds( X, Y ) }.
% 0.74/1.28 { ! Y = cons( X, Z ), member_succeeds( X, Y ) }.
% 0.74/1.28 { ! alpha21( X, Y ), Y = cons( skol221( Y, Z ), skol105( Z, Y ) ) }.
% 0.74/1.28 { ! alpha21( X, Y ), member_succeeds( X, skol105( X, Y ) ) }.
% 0.74/1.28 { ! Y = cons( T, Z ), ! member_succeeds( X, Z ), alpha21( X, Y ) }.
% 0.74/1.28 { ! member_fails( X, Y ), alpha22( X, Y ) }.
% 0.74/1.28 { ! member_fails( X, Y ), ! Y = cons( X, Z ) }.
% 0.74/1.28 { ! alpha22( X, Y ), Y = cons( X, skol106( X, Y ) ), member_fails( X, Y ) }
% 0.74/1.28 .
% 0.74/1.28 { ! alpha22( X, Y ), ! Y = cons( T, Z ), member_fails( X, Z ) }.
% 0.74/1.28 { Y = cons( skol222( Y, Z ), skol107( Z, Y ) ), alpha22( X, Y ) }.
% 0.74/1.28 { ! member_fails( X, skol107( X, Y ) ), alpha22( X, Y ) }.
% 0.74/1.28 { ! member_terminates( X, Y ), ! Y = cons( T, Z ), member_terminates( X, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! &&, Y = cons( skol223( Y, Z ), skol108( Z, Y ) ), ! &&,
% 0.74/1.28 member_terminates( X, Y ) }.
% 0.74/1.28 { ! &&, ! member_terminates( X, skol108( X, Y ) ), ! &&, member_terminates
% 0.74/1.28 ( X, Y ) }.
% 0.74/1.28 { ! list_succeeds( X ), alpha23( X ), X = nil }.
% 0.74/1.28 { ! alpha23( X ), list_succeeds( X ) }.
% 0.74/1.28 { ! X = nil, list_succeeds( X ) }.
% 0.74/1.28 { ! alpha23( X ), list_succeeds( skol109( Y ) ) }.
% 0.74/1.28 { ! alpha23( X ), X = cons( skol224( X ), skol109( X ) ) }.
% 0.74/1.28 { ! X = cons( Z, Y ), ! list_succeeds( Y ), alpha23( X ) }.
% 0.74/1.28 { ! list_fails( X ), alpha24( X ) }.
% 0.74/1.28 { ! list_fails( X ), ! X = nil }.
% 0.74/1.28 { ! alpha24( X ), X = nil, list_fails( X ) }.
% 0.74/1.28 { ! alpha24( X ), ! X = cons( Z, Y ), list_fails( Y ) }.
% 0.74/1.28 { ! list_fails( skol110( Y ) ), alpha24( X ) }.
% 0.74/1.28 { X = cons( skol225( X ), skol110( X ) ), alpha24( X ) }.
% 0.74/1.28 { ! list_terminates( X ), ! X = cons( Z, Y ), list_terminates( Y ) }.
% 0.74/1.28 { ! &&, ! list_terminates( skol111( Y ) ), ! &&, list_terminates( X ) }.
% 0.74/1.28 { ! &&, X = cons( skol226( X ), skol111( X ) ), ! &&, list_terminates( X )
% 0.74/1.28 }.
% 0.74/1.28 { ! sub( X, Y ), ! member_succeeds( Z, X ), member_succeeds( Z, Y ) }.
% 0.74/1.28 { ! member_succeeds( skol112( Z, Y ), Y ), sub( X, Y ) }.
% 0.74/1.28 { member_succeeds( skol112( X, Y ), X ), sub( X, Y ) }.
% 0.74/1.28 { ! list_succeeds( X ), member_terminates( Y, X ) }.
% 0.74/1.28 { ! member_succeeds( X, cons( Z, Y ) ), X = Z, member_succeeds( X, Y ) }.
% 0.74/1.28 { sub( Y, cons( X, Y ) ) }.
% 0.74/1.28 { ! sub( X, Z ), ! sub( Z, Y ), sub( X, Y ) }.
% 0.74/1.28 { sub( nil, X ) }.
% 0.74/1.28 { ! sub( Y, Z ), ! member_succeeds( X, Z ), sub( cons( X, Y ), Z ) }.
% 0.74/1.28 { ! list_succeeds( X ), incon_terminates( X ) }.
% 0.74/1.28 { ! literal_list_succeeds( X ), list_succeeds( X ) }.
% 0.74/1.28 { ! interpretation_succeeds( X ), literal_list_succeeds( X ) }.
% 0.74/1.28 { ! interpretation_succeeds( X ), ! member_succeeds( p( Y ), X ), !
% 0.74/1.28 member_succeeds( neg( p( Y ) ), X ) }.
% 0.74/1.28 { ! literal_list_succeeds( X ), member_succeeds( p( skol113( X ) ), X ),
% 0.74/1.28 interpretation_succeeds( X ) }.
% 0.74/1.28 { ! literal_list_succeeds( X ), member_succeeds( neg( p( skol113( X ) ) ),
% 0.74/1.28 X ), interpretation_succeeds( X ) }.
% 0.74/1.28 { ! interpretation_succeeds( Y ), member_succeeds( neg( p( X ) ), Y ),
% 0.74/1.28 interpretation_succeeds( cons( p( X ), Y ) ) }.
% 0.74/1.28 { ! interpretation_succeeds( Y ), ! member_fails( neg( p( X ) ), Y ),
% 0.74/1.28 interpretation_succeeds( cons( p( X ), Y ) ) }.
% 0.74/1.28 { ! interpretation_succeeds( Y ), member_succeeds( p( X ), Y ),
% 0.74/1.28 interpretation_succeeds( cons( neg( p( X ) ), Y ) ) }.
% 0.74/1.28 { ! interpretation_succeeds( Y ), ! member_fails( p( X ), Y ),
% 0.74/1.28 interpretation_succeeds( cons( neg( p( X ) ), Y ) ) }.
% 0.74/1.28 { interpretation_succeeds( nil ) }.
% 0.74/1.28 { ! true_succeeds( Z, X, Y ), ! interpretation_succeeds( X ),
% 0.74/1.28 interpretation_succeeds( Y ) }.
% 0.74/1.28 { ! true_succeeds( Z, X, Y ), ! literal_list_succeeds( X ),
% 0.74/1.28 literal_list_succeeds( Y ) }.
% 0.74/1.28 { ! true_succeeds( Z, X, Y ), sub( X, Y ) }.
% 0.74/1.28 { ! false_succeeds( Z, X, Y ), ! interpretation_succeeds( X ),
% 0.74/1.28 interpretation_succeeds( Y ) }.
% 0.74/1.28 { ! false_succeeds( Z, X, Y ), ! literal_list_succeeds( X ),
% 0.74/1.28 literal_list_succeeds( Y ) }.
% 0.74/1.28 { ! false_succeeds( Z, X, Y ), sub( X, Y ) }.
% 0.74/1.28 { ! true_succeeds( Z, Y, X ), ! interpretation_succeeds( Y ),
% 0.74/1.28 interpretation_succeeds( X ) }.
% 0.74/1.28 { ! false_succeeds( Z, Y, X ), ! interpretation_succeeds( Y ),
% 0.74/1.28 interpretation_succeeds( X ) }.
% 0.74/1.28 { ! true_succeeds( Z, Y, X ), ! literal_list_succeeds( Y ),
% 0.74/1.28 literal_list_succeeds( X ) }.
% 0.74/1.28 { ! false_succeeds( Z, Y, X ), ! literal_list_succeeds( Y ),
% 0.74/1.28 literal_list_succeeds( X ) }.
% 0.74/1.28 { ! true_succeeds( Z, X, Y ), sub( X, Y ) }.
% 0.74/1.28 { ! false_succeeds( Z, X, Y ), sub( X, Y ) }.
% 0.74/1.28 { ! true_succeeds( X, Y, Z ), ! gr( X ), ! gr( Y ), gr( Z ) }.
% 0.74/1.28 { ! false_succeeds( X, Y, Z ), ! gr( X ), ! gr( Y ), gr( Z ) }.
% 0.74/1.28 { ! true_succeeds( Y, Z, X ), ! gr( Y ), ! gr( Z ), gr( X ) }.
% 0.74/1.28 { ! false_succeeds( Y, Z, X ), ! gr( Y ), ! gr( Z ), gr( X ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! gr( X ), ! literal_list_succeeds( Y ), ! gr( Y
% 0.74/1.28 ), true_terminates( X, Y, Z ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! gr( X ), ! literal_list_succeeds( Y ), ! gr( Y
% 0.74/1.28 ), false_terminates( X, Y, Z ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! gr( X ), satisfiable_terminates( X ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! gr( X ), valid_terminates( X ) }.
% 0.74/1.28 { ! formula_succeeds( X ), ! list_succeeds( Y ), eval_terminates( X, Y, Z )
% 0.74/1.28 }.
% 0.74/1.28 { ! eval_succeeds( X, Y, Z ), ! sub( Y, T ), eval_succeeds( X, T, Z ) }.
% 0.74/1.28 { ! eval_succeeds( X, T, Z ), ! sub( T, Y ), eval_succeeds( X, Y, Z ) }.
% 0.74/1.28 { ! true_succeeds( X, Z, Y ), eval_succeeds( X, Y, 1 ) }.
% 0.74/1.28 { ! false_succeeds( X, Z, Y ), eval_succeeds( X, Y, 0 ) }.
% 0.74/1.28 { ! defined_succeeds( X, Y ), eval_succeeds( X, Y, 1 ), eval_succeeds( X, Y
% 0.74/1.28 , 0 ) }.
% 0.74/1.28 { ! eval_succeeds( X, Y, Z ), ! interpretation_succeeds( Y ), !
% 0.74/1.28 eval_succeeds( X, Y, T ), Z = T }.
% 0.74/1.28 { ! defined_succeeds( X, Y ), ! sub( Y, Z ), defined_succeeds( X, Z ) }.
% 0.74/1.28 { ! defined_succeeds( X, Z ), ! sub( Z, Y ), defined_succeeds( X, Y ) }.
% 0.74/1.28 { ! valid_fails( X ), false_succeeds( X, nil, skol114( X ) ) }.
% 0.74/1.28 { ! false_succeeds( X, nil, Y ), valid_fails( X ) }.
% 0.74/1.28 { ! valid_fails( X ), interpretation_succeeds( skol115( Y ) ) }.
% 0.74/1.28 { ! valid_fails( X ), eval_succeeds( X, skol115( X ), 0 ) }.
% 0.74/1.28 { alpha226, ! eval_succeeds( X, Y, Z ), ! interpretation_succeeds( Y ), !
% 0.74/1.28 literal_list_succeeds( T ), ! sub( T, Y ), ! Z = 1, alpha228( X, Y, T ) }
% 0.74/1.28 .
% 0.74/1.28 { alpha226, ! eval_succeeds( X, Y, Z ), ! interpretation_succeeds( Y ), !
% 0.74/1.28 literal_list_succeeds( T ), ! sub( T, Y ), ! Z = 0, sub( skol116( U, Y, W
% 0.74/1.28 ), Y ) }.
% 0.74/1.28 { alpha226, ! eval_succeeds( X, Y, Z ), ! interpretation_succeeds( Y ), !
% 0.74/1.28 literal_list_succeeds( T ), ! sub( T, Y ), ! Z = 0, false_succeeds( X, T
% 0.74/1.28 , skol116( X, Y, T ) ) }.
% 0.74/1.28 { ! alpha228( X, Y, Z ), sub( skol117( T, Y, U ), Y ) }.
% 0.74/1.28 { ! alpha228( X, Y, Z ), true_succeeds( X, Z, skol117( X, Y, Z ) ) }.
% 0.74/1.28 { ! sub( T, Y ), ! true_succeeds( X, Z, T ), alpha228( X, Y, Z ) }.
% 0.74/1.28 { ! alpha226, alpha280( skol118, skol227, skol231 ) }.
% 0.74/1.28 { ! alpha226, alpha285( skol118, skol227, skol231 ) }.
% 0.74/1.28 { ! alpha280( X, Y, Z ), ! alpha285( X, Y, Z ), alpha226 }.
% 0.74/1.28 { ! alpha285( X, Y, Z ), alpha274( Y, skol119( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha285( X, Y, Z ), alpha298( X, Y, Z, skol119( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha274( Y, T ), ! alpha298( X, Y, Z, T ), alpha285( X, Y, Z ) }.
% 0.74/1.28 { ! alpha298( X, Y, Z, T ), alpha301( X, Y, Z, T ), Z = 0 }.
% 0.74/1.28 { ! alpha298( X, Y, Z, T ), alpha301( X, Y, Z, T ), alpha294( X, Y, T ) }.
% 0.74/1.28 { ! alpha301( X, Y, Z, T ), alpha298( X, Y, Z, T ) }.
% 0.74/1.28 { ! Z = 0, ! alpha294( X, Y, T ), alpha298( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha301( X, Y, Z, T ), Z = 1 }.
% 0.74/1.28 { ! alpha301( X, Y, Z, T ), alpha290( X, Y, T ) }.
% 0.74/1.28 { ! Z = 1, ! alpha290( X, Y, T ), alpha301( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha294( X, Y, Z ), ! sub( T, Y ), ! false_succeeds( X, Z, T ) }.
% 0.74/1.28 { sub( skol120( T, Y, U ), Y ), alpha294( X, Y, Z ) }.
% 0.74/1.28 { false_succeeds( X, Z, skol120( X, Y, Z ) ), alpha294( X, Y, Z ) }.
% 0.74/1.28 { ! alpha290( X, Y, Z ), ! sub( T, Y ), ! true_succeeds( X, Z, T ) }.
% 0.74/1.28 { sub( skol121( T, Y, U ), Y ), alpha290( X, Y, Z ) }.
% 0.74/1.28 { true_succeeds( X, Z, skol121( X, Y, Z ) ), alpha290( X, Y, Z ) }.
% 0.74/1.28 { ! alpha280( X, Y, Z ), alpha286( X, Y, Z ) }.
% 0.74/1.28 { ! alpha280( X, Y, Z ), interpretation_succeeds( Y ) }.
% 0.74/1.28 { ! alpha286( X, Y, Z ), ! interpretation_succeeds( Y ), alpha280( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha286( X, Y, Z ), alpha291( X, Y, Z ), alpha295( X, Y, Z ) }.
% 0.74/1.28 { ! alpha291( X, Y, Z ), alpha286( X, Y, Z ) }.
% 0.74/1.28 { ! alpha295( X, Y, Z ), alpha286( X, Y, Z ) }.
% 0.74/1.28 { ! alpha295( X, Y, Z ), Z = 1 }.
% 0.74/1.28 { ! alpha295( X, Y, Z ), member_succeeds( p( skol122( T, Y, Z ) ), Y ) }.
% 0.74/1.28 { ! alpha295( X, Y, Z ), X = p( skol122( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = p( T ), ! Z = 1, ! member_succeeds( p( T ), Y ), alpha295( X, Y, Z
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha291( X, Y, Z ), alpha296( X, Y, Z ), alpha299( X, Y, Z ) }.
% 0.74/1.28 { ! alpha296( X, Y, Z ), alpha291( X, Y, Z ) }.
% 0.74/1.28 { ! alpha299( X, Y, Z ), alpha291( X, Y, Z ) }.
% 0.74/1.28 { ! alpha299( X, Y, Z ), Z = 0 }.
% 0.74/1.28 { ! alpha299( X, Y, Z ), member_succeeds( neg( p( skol123( T, Y, Z ) ) ), Y
% 0.74/1.28 ) }.
% 0.74/1.28 { ! alpha299( X, Y, Z ), X = p( skol123( X, Y, Z ) ) }.
% 0.74/1.28 { ! X = p( T ), ! Z = 0, ! member_succeeds( neg( p( T ) ), Y ), alpha299( X
% 0.74/1.28 , Y, Z ) }.
% 0.74/1.28 { ! alpha296( X, Y, Z ), alpha300( X, Y, Z ), alpha302( X, Y, Z ) }.
% 0.74/1.28 { ! alpha300( X, Y, Z ), alpha296( X, Y, Z ) }.
% 0.74/1.28 { ! alpha302( X, Y, Z ), alpha296( X, Y, Z ) }.
% 0.74/1.28 { ! alpha302( X, Y, Z ), eval_succeeds( skol124( T, Y, U ), Y, 0 ) }.
% 0.74/1.28 { ! alpha302( X, Y, Z ), alpha268( Y, skol124( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha302( X, Y, Z ), alpha304( X, Z, skol124( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha304( X, Z, T ), ! eval_succeeds( T, Y, 0 ), ! alpha268( Y, T ),
% 0.74/1.28 alpha302( X, Y, Z ) }.
% 0.74/1.28 { ! alpha304( X, Y, Z ), X = neg( Z ) }.
% 0.74/1.28 { ! alpha304( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! X = neg( Z ), ! Y = 1, alpha304( X, Y, Z ) }.
% 0.74/1.28 { ! alpha300( X, Y, Z ), alpha303( X, Y, Z ), alpha305( X, Y, Z ) }.
% 0.74/1.28 { ! alpha303( X, Y, Z ), alpha300( X, Y, Z ) }.
% 0.74/1.28 { ! alpha305( X, Y, Z ), alpha300( X, Y, Z ) }.
% 0.74/1.28 { ! alpha305( X, Y, Z ), eval_succeeds( skol125( T, Y, U ), Y, 1 ) }.
% 0.74/1.28 { ! alpha305( X, Y, Z ), alpha262( Y, skol125( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha305( X, Y, Z ), alpha307( X, Z, skol125( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha307( X, Z, T ), ! eval_succeeds( T, Y, 1 ), ! alpha262( Y, T ),
% 0.74/1.28 alpha305( X, Y, Z ) }.
% 0.74/1.28 { ! alpha307( X, Y, Z ), X = neg( Z ) }.
% 0.74/1.28 { ! alpha307( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! X = neg( Z ), ! Y = 0, alpha307( X, Y, Z ) }.
% 0.74/1.28 { ! alpha303( X, Y, Z ), alpha306( X, Y, Z ), alpha308( X, Y, Z ) }.
% 0.74/1.28 { ! alpha306( X, Y, Z ), alpha303( X, Y, Z ) }.
% 0.74/1.28 { ! alpha308( X, Y, Z ), alpha303( X, Y, Z ) }.
% 0.74/1.28 { ! alpha308( X, Y, Z ), alpha256( Y, skol228( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha308( X, Y, Z ), alpha313( X, Y, Z, skol126( X, Y, Z ), skol228( X
% 0.74/1.28 , Y, Z ) ) }.
% 0.74/1.28 { ! alpha313( X, Y, Z, T, U ), ! alpha256( Y, U ), alpha308( X, Y, Z ) }.
% 0.74/1.28 { ! alpha313( X, Y, Z, T, U ), alpha317( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! alpha313( X, Y, Z, T, U ), eval_succeeds( U, Y, 1 ) }.
% 0.74/1.28 { ! alpha317( X, Y, Z, T, U ), ! eval_succeeds( U, Y, 1 ), alpha313( X, Y,
% 0.74/1.28 Z, T, U ) }.
% 0.74/1.28 { ! alpha317( X, Y, Z, T, U ), alpha310( X, Z, T, U ) }.
% 0.74/1.28 { ! alpha317( X, Y, Z, T, U ), eval_succeeds( T, Y, 1 ) }.
% 0.74/1.28 { ! alpha317( X, Y, Z, T, U ), alpha250( Y, T ) }.
% 0.74/1.28 { ! alpha310( X, Z, T, U ), ! eval_succeeds( T, Y, 1 ), ! alpha250( Y, T )
% 0.74/1.28 , alpha317( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! alpha310( X, Y, Z, T ), X = and( Z, T ) }.
% 0.74/1.28 { ! alpha310( X, Y, Z, T ), Y = 1 }.
% 0.74/1.28 { ! X = and( Z, T ), ! Y = 1, alpha310( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha306( X, Y, Z ), alpha309( X, Y, Z ), alpha311( X, Y, Z ) }.
% 0.74/1.28 { ! alpha309( X, Y, Z ), alpha306( X, Y, Z ) }.
% 0.74/1.28 { ! alpha311( X, Y, Z ), alpha306( X, Y, Z ) }.
% 0.74/1.28 { ! alpha311( X, Y, Z ), eval_succeeds( skol127( T, Y, U ), Y, 0 ) }.
% 0.74/1.28 { ! alpha311( X, Y, Z ), alpha244( Y, skol127( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha311( X, Y, Z ), alpha314( X, Z, skol127( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha314( X, Z, T ), ! eval_succeeds( T, Y, 0 ), ! alpha244( Y, T ),
% 0.74/1.28 alpha311( X, Y, Z ) }.
% 0.74/1.28 { ! alpha314( X, Y, Z ), X = and( Z, skol128( X, Z ) ) }.
% 0.74/1.28 { ! alpha314( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! X = and( Z, T ), ! Y = 0, alpha314( X, Y, Z ) }.
% 0.74/1.28 { ! alpha309( X, Y, Z ), alpha312( X, Y, Z ), alpha315( X, Y, Z ) }.
% 0.74/1.28 { ! alpha312( X, Y, Z ), alpha309( X, Y, Z ) }.
% 0.74/1.28 { ! alpha315( X, Y, Z ), alpha309( X, Y, Z ) }.
% 0.74/1.28 { ! alpha315( X, Y, Z ), eval_succeeds( skol129( T, Y, U ), Y, 0 ) }.
% 0.74/1.28 { ! alpha315( X, Y, Z ), alpha239( Y, skol129( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha315( X, Y, Z ), alpha318( X, Z, skol129( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha318( X, Z, T ), ! eval_succeeds( T, Y, 0 ), ! alpha239( Y, T ),
% 0.74/1.28 alpha315( X, Y, Z ) }.
% 0.74/1.28 { ! alpha318( X, Y, Z ), X = and( skol130( X, Z ), Z ) }.
% 0.74/1.28 { ! alpha318( X, Y, Z ), Y = 0 }.
% 0.74/1.28 { ! X = and( T, Z ), ! Y = 0, alpha318( X, Y, Z ) }.
% 0.74/1.28 { ! alpha312( X, Y, Z ), alpha316( X, Y, Z ), alpha319( X, Y, Z ) }.
% 0.74/1.28 { ! alpha316( X, Y, Z ), alpha312( X, Y, Z ) }.
% 0.74/1.28 { ! alpha319( X, Y, Z ), alpha312( X, Y, Z ) }.
% 0.74/1.28 { ! alpha319( X, Y, Z ), eval_succeeds( skol131( T, Y, U ), Y, 1 ) }.
% 0.74/1.28 { ! alpha319( X, Y, Z ), alpha235( Y, skol131( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha319( X, Y, Z ), alpha321( X, Z, skol131( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha321( X, Z, T ), ! eval_succeeds( T, Y, 1 ), ! alpha235( Y, T ),
% 0.74/1.28 alpha319( X, Y, Z ) }.
% 0.74/1.28 { ! alpha321( X, Y, Z ), X = or( Z, skol132( X, Z ) ) }.
% 0.74/1.28 { ! alpha321( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! X = or( Z, T ), ! Y = 1, alpha321( X, Y, Z ) }.
% 0.74/1.28 { ! alpha316( X, Y, Z ), alpha320( X, Y, Z ), alpha322( X, Y, Z ) }.
% 0.74/1.28 { ! alpha320( X, Y, Z ), alpha316( X, Y, Z ) }.
% 0.74/1.28 { ! alpha322( X, Y, Z ), alpha316( X, Y, Z ) }.
% 0.74/1.28 { ! alpha322( X, Y, Z ), eval_succeeds( skol133( T, Y, U ), Y, 1 ) }.
% 0.74/1.28 { ! alpha322( X, Y, Z ), alpha232( Y, skol133( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha322( X, Y, Z ), alpha324( X, Z, skol133( X, Y, Z ) ) }.
% 0.74/1.28 { ! alpha324( X, Z, T ), ! eval_succeeds( T, Y, 1 ), ! alpha232( Y, T ),
% 0.74/1.28 alpha322( X, Y, Z ) }.
% 0.74/1.28 { ! alpha324( X, Y, Z ), X = or( skol134( X, Z ), Z ) }.
% 0.74/1.28 { ! alpha324( X, Y, Z ), Y = 1 }.
% 0.74/1.28 { ! X = or( T, Z ), ! Y = 1, alpha324( X, Y, Z ) }.
% 0.74/1.28 { ! alpha320( X, Y, Z ), alpha230( Y, skol229( T, Y, U ) ) }.
% 0.74/1.28 { ! alpha320( X, Y, Z ), alpha325( X, Y, Z, skol135( X, Y, Z ), skol229( X
% 0.74/1.28 , Y, Z ) ) }.
% 0.74/1.28 { ! alpha325( X, Y, Z, T, U ), ! alpha230( Y, U ), alpha320( X, Y, Z ) }.
% 0.74/1.28 { ! alpha325( X, Y, Z, T, U ), alpha326( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! alpha325( X, Y, Z, T, U ), eval_succeeds( U, Y, 0 ) }.
% 0.74/1.28 { ! alpha326( X, Y, Z, T, U ), ! eval_succeeds( U, Y, 0 ), alpha325( X, Y,
% 0.74/1.28 Z, T, U ) }.
% 0.74/1.28 { ! alpha326( X, Y, Z, T, U ), alpha323( X, Z, T, U ) }.
% 0.74/1.28 { ! alpha326( X, Y, Z, T, U ), eval_succeeds( T, Y, 0 ) }.
% 0.74/1.28 { ! alpha326( X, Y, Z, T, U ), alpha229( Y, T ) }.
% 0.74/1.28 { ! alpha323( X, Z, T, U ), ! eval_succeeds( T, Y, 0 ), ! alpha229( Y, T )
% 0.74/1.28 , alpha326( X, Y, Z, T, U ) }.
% 0.74/1.28 { ! alpha323( X, Y, Z, T ), X = or( Z, T ) }.
% 0.74/1.28 { ! alpha323( X, Y, Z, T ), Y = 0 }.
% 0.74/1.28 { ! X = or( Z, T ), ! Y = 0, alpha323( X, Y, Z, T ) }.
% 0.74/1.28 { ! alpha274( X, Y ), literal_list_succeeds( Y ) }.
% 0.74/1.28 { ! alpha274( X, Y ), sub( Y, X ) }.
% 0.74/1.28 { ! literal_list_succeeds( Y ), ! sub( Y, X ), alpha274( X, Y ) }.
% 0.74/1.28 { ! alpha268( X, Y ), ! interpretation_succeeds( X ), alpha275( X, Y ) }.
% 0.74/1.28 { interpretation_succeeds( X ), alpha268( X, Y ) }.
% 0.74/1.28 { ! alpha275( X, Y ), alpha268( X, Y ) }.
% 0.74/1.28 { ! alpha275( X, Y ), alpha281( X, Z ), alpha287( X, Y, Z ) }.
% 0.74/1.28 { ! alpha281( X, skol136( X, Z ) ), alpha275( X, Y ) }.
% 0.74/1.28 { ! alpha287( X, Y, skol136( X, Y ) ), alpha275( X, Y ) }.
% 0.74/1.28 { ! alpha287( X, Y, Z ), alpha292( X, Y, Z ) }.
% 0.74/1.28 { ! alpha287( X, Y, Z ), alpha297( X, Y, Z ) }.
% 0.74/1.28 { ! alpha292( X, Y, Z ), ! alpha297( X, Y, Z ), alpha287( X, Y, Z ) }.
% 0.74/1.28 { ! alpha297( X, Y, Z ), ! 0 = 0, sub( skol137( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha297( X, Y, Z ), ! 0 = 0, false_succeeds( Y, Z, skol137( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { 0 = 0, alpha297( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha297( X, Y, Z ) }.
% 0.74/1.28 { ! alpha292( X, Y, Z ), ! 0 = 1, sub( skol138( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha292( X, Y, Z ), ! 0 = 1, true_succeeds( Y, Z, skol138( X, Y, Z ) )
% 0.74/1.28 }.
% 0.74/1.28 { 0 = 1, alpha292( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha292( X, Y, Z ) }.
% 0.74/1.28 { ! alpha281( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.28 { literal_list_succeeds( Y ), alpha281( X, Y ) }.
% 0.74/1.28 { sub( Y, X ), alpha281( X, Y ) }.
% 0.74/1.28 { ! alpha262( X, Y ), ! interpretation_succeeds( X ), alpha269( X, Y ) }.
% 0.74/1.28 { interpretation_succeeds( X ), alpha262( X, Y ) }.
% 0.74/1.28 { ! alpha269( X, Y ), alpha262( X, Y ) }.
% 0.74/1.28 { ! alpha269( X, Y ), alpha276( X, Z ), alpha282( X, Y, Z ) }.
% 0.74/1.28 { ! alpha276( X, skol139( X, Z ) ), alpha269( X, Y ) }.
% 0.74/1.28 { ! alpha282( X, Y, skol139( X, Y ) ), alpha269( X, Y ) }.
% 0.74/1.28 { ! alpha282( X, Y, Z ), alpha288( X, Y, Z ) }.
% 0.74/1.28 { ! alpha282( X, Y, Z ), alpha293( X, Y, Z ) }.
% 0.74/1.28 { ! alpha288( X, Y, Z ), ! alpha293( X, Y, Z ), alpha282( X, Y, Z ) }.
% 0.74/1.28 { ! alpha293( X, Y, Z ), ! 1 = 0, sub( skol140( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha293( X, Y, Z ), ! 1 = 0, false_succeeds( Y, Z, skol140( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { 1 = 0, alpha293( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha293( X, Y, Z ) }.
% 0.74/1.28 { ! alpha288( X, Y, Z ), ! 1 = 1, sub( skol141( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha288( X, Y, Z ), ! 1 = 1, true_succeeds( Y, Z, skol141( X, Y, Z ) )
% 0.74/1.28 }.
% 0.74/1.28 { 1 = 1, alpha288( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha288( X, Y, Z ) }.
% 0.74/1.28 { ! alpha276( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.28 { literal_list_succeeds( Y ), alpha276( X, Y ) }.
% 0.74/1.28 { sub( Y, X ), alpha276( X, Y ) }.
% 0.74/1.28 { ! alpha256( X, Y ), ! interpretation_succeeds( X ), alpha263( X, Y ) }.
% 0.74/1.28 { interpretation_succeeds( X ), alpha256( X, Y ) }.
% 0.74/1.28 { ! alpha263( X, Y ), alpha256( X, Y ) }.
% 0.74/1.28 { ! alpha263( X, Y ), alpha270( X, Z ), alpha277( X, Y, Z ) }.
% 0.74/1.28 { ! alpha270( X, skol142( X, Z ) ), alpha263( X, Y ) }.
% 0.74/1.28 { ! alpha277( X, Y, skol142( X, Y ) ), alpha263( X, Y ) }.
% 0.74/1.28 { ! alpha277( X, Y, Z ), alpha283( X, Y, Z ) }.
% 0.74/1.28 { ! alpha277( X, Y, Z ), alpha289( X, Y, Z ) }.
% 0.74/1.28 { ! alpha283( X, Y, Z ), ! alpha289( X, Y, Z ), alpha277( X, Y, Z ) }.
% 0.74/1.28 { ! alpha289( X, Y, Z ), ! 1 = 0, sub( skol143( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha289( X, Y, Z ), ! 1 = 0, false_succeeds( Y, Z, skol143( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { 1 = 0, alpha289( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha289( X, Y, Z ) }.
% 0.74/1.28 { ! alpha283( X, Y, Z ), ! 1 = 1, sub( skol144( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha283( X, Y, Z ), ! 1 = 1, true_succeeds( Y, Z, skol144( X, Y, Z ) )
% 0.74/1.28 }.
% 0.74/1.28 { 1 = 1, alpha283( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha283( X, Y, Z ) }.
% 0.74/1.28 { ! alpha270( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.28 { literal_list_succeeds( Y ), alpha270( X, Y ) }.
% 0.74/1.28 { sub( Y, X ), alpha270( X, Y ) }.
% 0.74/1.28 { ! alpha250( X, Y ), ! interpretation_succeeds( X ), alpha257( X, Y ) }.
% 0.74/1.28 { interpretation_succeeds( X ), alpha250( X, Y ) }.
% 0.74/1.28 { ! alpha257( X, Y ), alpha250( X, Y ) }.
% 0.74/1.28 { ! alpha257( X, Y ), alpha264( X, Z ), alpha271( X, Y, Z ) }.
% 0.74/1.28 { ! alpha264( X, skol145( X, Z ) ), alpha257( X, Y ) }.
% 0.74/1.28 { ! alpha271( X, Y, skol145( X, Y ) ), alpha257( X, Y ) }.
% 0.74/1.28 { ! alpha271( X, Y, Z ), alpha278( X, Y, Z ) }.
% 0.74/1.28 { ! alpha271( X, Y, Z ), alpha284( X, Y, Z ) }.
% 0.74/1.28 { ! alpha278( X, Y, Z ), ! alpha284( X, Y, Z ), alpha271( X, Y, Z ) }.
% 0.74/1.28 { ! alpha284( X, Y, Z ), ! 1 = 0, sub( skol146( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha284( X, Y, Z ), ! 1 = 0, false_succeeds( Y, Z, skol146( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { 1 = 0, alpha284( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha284( X, Y, Z ) }.
% 0.74/1.28 { ! alpha278( X, Y, Z ), ! 1 = 1, sub( skol147( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha278( X, Y, Z ), ! 1 = 1, true_succeeds( Y, Z, skol147( X, Y, Z ) )
% 0.74/1.28 }.
% 0.74/1.28 { 1 = 1, alpha278( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha278( X, Y, Z ) }.
% 0.74/1.28 { ! alpha264( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.28 { literal_list_succeeds( Y ), alpha264( X, Y ) }.
% 0.74/1.28 { sub( Y, X ), alpha264( X, Y ) }.
% 0.74/1.28 { ! alpha244( X, Y ), ! interpretation_succeeds( X ), alpha251( X, Y ) }.
% 0.74/1.28 { interpretation_succeeds( X ), alpha244( X, Y ) }.
% 0.74/1.28 { ! alpha251( X, Y ), alpha244( X, Y ) }.
% 0.74/1.28 { ! alpha251( X, Y ), alpha258( X, Z ), alpha265( X, Y, Z ) }.
% 0.74/1.28 { ! alpha258( X, skol148( X, Z ) ), alpha251( X, Y ) }.
% 0.74/1.28 { ! alpha265( X, Y, skol148( X, Y ) ), alpha251( X, Y ) }.
% 0.74/1.28 { ! alpha265( X, Y, Z ), alpha272( X, Y, Z ) }.
% 0.74/1.28 { ! alpha265( X, Y, Z ), alpha279( X, Y, Z ) }.
% 0.74/1.28 { ! alpha272( X, Y, Z ), ! alpha279( X, Y, Z ), alpha265( X, Y, Z ) }.
% 0.74/1.28 { ! alpha279( X, Y, Z ), ! 0 = 0, sub( skol149( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha279( X, Y, Z ), ! 0 = 0, false_succeeds( Y, Z, skol149( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { 0 = 0, alpha279( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha279( X, Y, Z ) }.
% 0.74/1.28 { ! alpha272( X, Y, Z ), ! 0 = 1, sub( skol150( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha272( X, Y, Z ), ! 0 = 1, true_succeeds( Y, Z, skol150( X, Y, Z ) )
% 0.74/1.28 }.
% 0.74/1.28 { 0 = 1, alpha272( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha272( X, Y, Z ) }.
% 0.74/1.28 { ! alpha258( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.28 { literal_list_succeeds( Y ), alpha258( X, Y ) }.
% 0.74/1.28 { sub( Y, X ), alpha258( X, Y ) }.
% 0.74/1.28 { ! alpha239( X, Y ), ! interpretation_succeeds( X ), alpha245( X, Y ) }.
% 0.74/1.28 { interpretation_succeeds( X ), alpha239( X, Y ) }.
% 0.74/1.28 { ! alpha245( X, Y ), alpha239( X, Y ) }.
% 0.74/1.28 { ! alpha245( X, Y ), alpha252( X, Z ), alpha259( X, Y, Z ) }.
% 0.74/1.28 { ! alpha252( X, skol151( X, Z ) ), alpha245( X, Y ) }.
% 0.74/1.28 { ! alpha259( X, Y, skol151( X, Y ) ), alpha245( X, Y ) }.
% 0.74/1.28 { ! alpha259( X, Y, Z ), alpha266( X, Y, Z ) }.
% 0.74/1.28 { ! alpha259( X, Y, Z ), alpha273( X, Y, Z ) }.
% 0.74/1.28 { ! alpha266( X, Y, Z ), ! alpha273( X, Y, Z ), alpha259( X, Y, Z ) }.
% 0.74/1.28 { ! alpha273( X, Y, Z ), ! 0 = 0, sub( skol152( X, T, U ), X ) }.
% 0.74/1.28 { ! alpha273( X, Y, Z ), ! 0 = 0, false_succeeds( Y, Z, skol152( X, Y, Z )
% 0.74/1.28 ) }.
% 0.74/1.28 { 0 = 0, alpha273( X, Y, Z ) }.
% 0.74/1.28 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha273( X, Y, Z ) }.
% 0.74/1.28 { ! alpha266( X, Y, Z ), ! 0 = 1, sub( skol153( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha266( X, Y, Z ), ! 0 = 1, true_succeeds( Y, Z, skol153( X, Y, Z ) )
% 0.74/1.29 }.
% 0.74/1.29 { 0 = 1, alpha266( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha266( X, Y, Z ) }.
% 0.74/1.29 { ! alpha252( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.29 { literal_list_succeeds( Y ), alpha252( X, Y ) }.
% 0.74/1.29 { sub( Y, X ), alpha252( X, Y ) }.
% 0.74/1.29 { ! alpha235( X, Y ), ! interpretation_succeeds( X ), alpha240( X, Y ) }.
% 0.74/1.29 { interpretation_succeeds( X ), alpha235( X, Y ) }.
% 0.74/1.29 { ! alpha240( X, Y ), alpha235( X, Y ) }.
% 0.74/1.29 { ! alpha240( X, Y ), alpha246( X, Z ), alpha253( X, Y, Z ) }.
% 0.74/1.29 { ! alpha246( X, skol154( X, Z ) ), alpha240( X, Y ) }.
% 0.74/1.29 { ! alpha253( X, Y, skol154( X, Y ) ), alpha240( X, Y ) }.
% 0.74/1.29 { ! alpha253( X, Y, Z ), alpha260( X, Y, Z ) }.
% 0.74/1.29 { ! alpha253( X, Y, Z ), alpha267( X, Y, Z ) }.
% 0.74/1.29 { ! alpha260( X, Y, Z ), ! alpha267( X, Y, Z ), alpha253( X, Y, Z ) }.
% 0.74/1.29 { ! alpha267( X, Y, Z ), ! 1 = 0, sub( skol155( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha267( X, Y, Z ), ! 1 = 0, false_succeeds( Y, Z, skol155( X, Y, Z )
% 0.74/1.29 ) }.
% 0.74/1.29 { 1 = 0, alpha267( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha267( X, Y, Z ) }.
% 0.74/1.29 { ! alpha260( X, Y, Z ), ! 1 = 1, sub( skol156( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha260( X, Y, Z ), ! 1 = 1, true_succeeds( Y, Z, skol156( X, Y, Z ) )
% 0.74/1.29 }.
% 0.74/1.29 { 1 = 1, alpha260( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha260( X, Y, Z ) }.
% 0.74/1.29 { ! alpha246( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.29 { literal_list_succeeds( Y ), alpha246( X, Y ) }.
% 0.74/1.29 { sub( Y, X ), alpha246( X, Y ) }.
% 0.74/1.29 { ! alpha232( X, Y ), ! interpretation_succeeds( X ), alpha236( X, Y ) }.
% 0.74/1.29 { interpretation_succeeds( X ), alpha232( X, Y ) }.
% 0.74/1.29 { ! alpha236( X, Y ), alpha232( X, Y ) }.
% 0.74/1.29 { ! alpha236( X, Y ), alpha241( X, Z ), alpha247( X, Y, Z ) }.
% 0.74/1.29 { ! alpha241( X, skol157( X, Z ) ), alpha236( X, Y ) }.
% 0.74/1.29 { ! alpha247( X, Y, skol157( X, Y ) ), alpha236( X, Y ) }.
% 0.74/1.29 { ! alpha247( X, Y, Z ), alpha254( X, Y, Z ) }.
% 0.74/1.29 { ! alpha247( X, Y, Z ), alpha261( X, Y, Z ) }.
% 0.74/1.29 { ! alpha254( X, Y, Z ), ! alpha261( X, Y, Z ), alpha247( X, Y, Z ) }.
% 0.74/1.29 { ! alpha261( X, Y, Z ), ! 1 = 0, sub( skol158( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha261( X, Y, Z ), ! 1 = 0, false_succeeds( Y, Z, skol158( X, Y, Z )
% 0.74/1.29 ) }.
% 0.74/1.29 { 1 = 0, alpha261( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha261( X, Y, Z ) }.
% 0.74/1.29 { ! alpha254( X, Y, Z ), ! 1 = 1, sub( skol159( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha254( X, Y, Z ), ! 1 = 1, true_succeeds( Y, Z, skol159( X, Y, Z ) )
% 0.74/1.29 }.
% 0.74/1.29 { 1 = 1, alpha254( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha254( X, Y, Z ) }.
% 0.74/1.29 { ! alpha241( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.29 { literal_list_succeeds( Y ), alpha241( X, Y ) }.
% 0.74/1.29 { sub( Y, X ), alpha241( X, Y ) }.
% 0.74/1.29 { ! alpha230( X, Y ), ! interpretation_succeeds( X ), alpha233( X, Y ) }.
% 0.74/1.29 { interpretation_succeeds( X ), alpha230( X, Y ) }.
% 0.74/1.29 { ! alpha233( X, Y ), alpha230( X, Y ) }.
% 0.74/1.29 { ! alpha233( X, Y ), alpha237( X, Z ), alpha242( X, Y, Z ) }.
% 0.74/1.29 { ! alpha237( X, skol160( X, Z ) ), alpha233( X, Y ) }.
% 0.74/1.29 { ! alpha242( X, Y, skol160( X, Y ) ), alpha233( X, Y ) }.
% 0.74/1.29 { ! alpha242( X, Y, Z ), alpha248( X, Y, Z ) }.
% 0.74/1.29 { ! alpha242( X, Y, Z ), alpha255( X, Y, Z ) }.
% 0.74/1.29 { ! alpha248( X, Y, Z ), ! alpha255( X, Y, Z ), alpha242( X, Y, Z ) }.
% 0.74/1.29 { ! alpha255( X, Y, Z ), ! 0 = 0, sub( skol161( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha255( X, Y, Z ), ! 0 = 0, false_succeeds( Y, Z, skol161( X, Y, Z )
% 0.74/1.29 ) }.
% 0.74/1.29 { 0 = 0, alpha255( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha255( X, Y, Z ) }.
% 0.74/1.29 { ! alpha248( X, Y, Z ), ! 0 = 1, sub( skol162( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha248( X, Y, Z ), ! 0 = 1, true_succeeds( Y, Z, skol162( X, Y, Z ) )
% 0.74/1.29 }.
% 0.74/1.29 { 0 = 1, alpha248( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha248( X, Y, Z ) }.
% 0.74/1.29 { ! alpha237( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.29 { literal_list_succeeds( Y ), alpha237( X, Y ) }.
% 0.74/1.29 { sub( Y, X ), alpha237( X, Y ) }.
% 0.74/1.29 { ! alpha229( X, Y ), ! interpretation_succeeds( X ), alpha231( X, Y ) }.
% 0.74/1.29 { interpretation_succeeds( X ), alpha229( X, Y ) }.
% 0.74/1.29 { ! alpha231( X, Y ), alpha229( X, Y ) }.
% 0.74/1.29 { ! alpha231( X, Y ), alpha234( X, Z ), alpha238( X, Y, Z ) }.
% 0.74/1.29 { ! alpha234( X, skol163( X, Z ) ), alpha231( X, Y ) }.
% 0.74/1.29 { ! alpha238( X, Y, skol163( X, Y ) ), alpha231( X, Y ) }.
% 0.74/1.29 { ! alpha238( X, Y, Z ), alpha243( X, Y, Z ) }.
% 0.74/1.29 { ! alpha238( X, Y, Z ), alpha249( X, Y, Z ) }.
% 0.74/1.29 { ! alpha243( X, Y, Z ), ! alpha249( X, Y, Z ), alpha238( X, Y, Z ) }.
% 0.74/1.29 { ! alpha249( X, Y, Z ), ! 0 = 0, sub( skol164( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha249( X, Y, Z ), ! 0 = 0, false_succeeds( Y, Z, skol164( X, Y, Z )
% 0.74/1.29 ) }.
% 0.74/1.29 { 0 = 0, alpha249( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! false_succeeds( Y, Z, T ), alpha249( X, Y, Z ) }.
% 0.74/1.29 { ! alpha243( X, Y, Z ), ! 0 = 1, sub( skol165( X, T, U ), X ) }.
% 0.74/1.29 { ! alpha243( X, Y, Z ), ! 0 = 1, true_succeeds( Y, Z, skol165( X, Y, Z ) )
% 0.74/1.29 }.
% 0.74/1.29 { 0 = 1, alpha243( X, Y, Z ) }.
% 0.74/1.29 { ! sub( T, X ), ! true_succeeds( Y, Z, T ), alpha243( X, Y, Z ) }.
% 0.74/1.29 { ! alpha234( X, Y ), ! literal_list_succeeds( Y ), ! sub( Y, X ) }.
% 0.74/1.29 { literal_list_succeeds( Y ), alpha234( X, Y ) }.
% 0.74/1.29 { sub( Y, X ), alpha234( X, Y ) }.
% 0.74/1.29 { eval_succeeds( skol166, skol230, skol232 ) }.
% 0.74/1.29 { interpretation_succeeds( skol230 ) }.
% 0.74/1.29 { literal_list_succeeds( skol233 ) }.
% 0.74/1.29 { sub( skol233, skol230 ) }.
% 0.74/1.29 { alpha227( skol166, skol230, skol232, skol233 ), skol232 = 0 }.
% 0.74/1.29 { alpha227( skol166, skol230, skol232, skol233 ), ! sub( X, skol230 ), !
% 0.74/1.29 false_succeeds( skol166, skol233, X ) }.
% 0.74/1.29 { ! alpha227( X, Y, Z, T ), Z = 1 }.
% 0.74/1.29 { ! alpha227( X, Y, Z, T ), ! sub( U, Y ), ! true_succeeds( X, T, U ) }.
% 0.74/1.29 { ! Z = 1, sub( skol167( U, Y, W ), Y ), alpha227( X, Y, Z, T ) }.
% 0.74/1.29 { ! Z = 1, true_succeeds( X, T, skol167( X, Y, T ) ), alpha227( X, Y, Z, T
% 0.74/1.29 ) }.
% 0.74/1.29
% 0.74/1.29 *** allocated 15000 integers for clauses
% 0.74/1.29 *** allocated 22500 integers for clauses
% 0.74/1.29 *** allocated 33750 integers for clauses
% 0.74/1.29 *** allocated 50625 integers for clauses
% 0.74/1.29 percentage equality = 0.140463, percentage horn = 0.811229
% 0.74/1.29 This is a problem with some equality
% 0.74/1.29
% 0.74/1.29
% 0.74/1.29
% 0.74/1.29 Options Used:
% 0.74/1.29
% 0.74/1.29 useres = 1
% 0.74/1.29 useparamod = 1
% 0.74/1.29 useeqrefl = 1
% 0.74/1.29 useeqfact = 1
% 0.74/1.29 usefactor = 1
% 0.74/1.29 usesimpsplitting = 0
% 0.74/1.29 usesimpdemod = 5
% 0.74/1.29 usesimpres = 3
% 0.74/1.29
% 0.74/1.29 resimpinuse = 1000
% 0.74/1.29 resimpclauses = 20000
% 0.74/1.29 substype = eqrewr
% 0.74/1.29 backwardsubs = 1
% 0.74/1.29 selectoldest = 5
% 0.74/1.29
% 0.74/1.29 litorderings [0] = split
% 0.74/1.29 litorderings [1] = extend the termordering, first sorting on arguments
% 0.74/1.29
% 0.74/1.29 termordering = kbo
% 0.74/1.29
% 0.74/1.29 litapriori = 0
% 0.74/1.29 termapriori = 1
% 0.74/1.29 litaposteriori = 0
% 0.74/1.29 termaposteriori = 0
% 0.74/1.29 demodaposteriori = 0
% 0.74/1.29 ordereqreflfact = 0
% 0.74/1.29
% 0.74/1.29 litselect = negord
% 0.74/1.29
% 0.74/1.29 maxweight = 15
% 0.74/1.29 maxdepth = 30000
% 0.74/1.29 maxlength = 115
% 0.74/1.29 maxnrvars = 195
% 0.74/1.29 excuselevel = 1
% 0.74/1.29 increasemaxweight = 1
% 0.74/1.29
% 0.74/1.29 maxselected = 10000000
% 0.74/1.29 maxnrclauses = 10000000
% 0.74/1.29
% 0.74/1.29 showgenerated = 0
% 0.74/1.29 showkept = 0
% 0.74/1.29 showselected = 0
% 0.74/1.29 showdeleted = 0
% 0.74/1.29 showresimp = 1
% 0.74/1.29 showstatus = 2000
% 0.74/1.29
% 0.74/1.29 prologoutput = 0
% 0.74/1.29 nrgoals = 5000000
% 0.74/1.29 totalproof = 1
% 0.74/1.29
% 0.74/1.29 Symbols occurring in the translation:
% 0.74/1.29
% 0.74/1.29 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.74/1.29 . [1, 2] (w:1, o:237, a:1, s:1, b:0),
% 0.74/1.29 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 0.74/1.29 ! [4, 1] (w:0, o:143, a:1, s:1, b:0),
% 0.74/1.29 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.29 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.29 nil [37, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.74/1.29 cons [38, 2] (w:1, o:261, a:1, s:1, b:0),
% 0.74/1.29 1 [39, 0] (w:1, o:33, a:1, s:1, b:0),
% 0.74/1.29 0 [40, 0] (w:1, o:32, a:1, s:1, b:0),
% 0.74/1.29 p [42, 1] (w:1, o:148, a:1, s:1, b:0),
% 0.74/1.29 neg [44, 1] (w:1, o:149, a:1, s:1, b:0),
% 0.74/1.29 and [47, 2] (w:1, o:262, a:1, s:1, b:0),
% 0.74/1.29 or [50, 2] (w:1, o:263, a:1, s:1, b:0),
% 0.74/1.29 gr [127, 1] (w:1, o:153, a:1, s:1, b:0),
% 0.74/1.29 defined_succeeds [138, 2] (w:1, o:264, a:1, s:1, b:0),
% 0.74/1.29 defined_fails [139, 2] (w:1, o:265, a:1, s:1, b:0),
% 0.74/1.29 defined_terminates [140, 2] (w:1, o:266, a:1, s:1, b:0),
% 0.74/1.29 eval_succeeds [144, 3] (w:1, o:389, a:1, s:1, b:0),
% 0.74/1.29 eval_fails [145, 3] (w:1, o:390, a:1, s:1, b:0),
% 0.74/1.29 eval_terminates [146, 3] (w:1, o:391, a:1, s:1, b:0),
% 0.74/1.29 false_succeeds [150, 3] (w:1, o:392, a:1, s:1, b:0),
% 0.74/1.29 false_fails [151, 3] (w:1, o:393, a:1, s:1, b:0),
% 0.74/1.29 false_terminates [152, 3] (w:1, o:394, a:1, s:1, b:0),
% 0.74/1.29 true_succeeds [156, 3] (w:1, o:529, a:1, s:1, b:0),
% 0.74/1.29 true_fails [157, 3] (w:1, o:530, a:1, s:1, b:0),
% 0.74/1.29 true_terminates [158, 3] (w:1, o:531, a:1, s:1, b:0),
% 0.74/1.29 satisfiable_succeeds [160, 1] (w:1, o:154, a:1, s:1, b:0),
% 0.74/1.29 satisfiable_fails [161, 1] (w:1, o:155, a:1, s:1, b:0),
% 0.74/1.29 satisfiable_terminates [162, 1] (w:1, o:156, a:1, s:1, b:0),
% 0.74/1.29 valid_succeeds [164, 1] (w:1, o:157, a:1, s:1, b:0),
% 0.74/1.29 valid_fails [165, 1] (w:1, o:158, a:1, s:1, b:0),
% 0.74/1.29 valid_terminates [166, 1] (w:1, o:159, a:1, s:1, b:0),
% 0.74/1.29 incon_succeeds [168, 1] (w:1, o:160, a:1, s:1, b:0),
% 0.74/1.29 incon_fails [169, 1] (w:1, o:161, a:1, s:1, b:0),
% 0.74/1.29 incon_terminates [170, 1] (w:1, o:162, a:1, s:1, b:0),
% 0.74/1.29 interpretation_succeeds [172, 1] (w:1, o:163, a:1, s:1, b:0),
% 0.74/1.29 interpretation_fails [173, 1] (w:1, o:164, a:1, s:1, b:0),
% 0.74/1.29 interpretation_terminates [174, 1] (w:1, o:165, a:1, s:1, b:0),
% 0.74/1.29 literal_list_succeeds [176, 1] (w:1, o:169, a:1, s:1, b:0),
% 0.74/1.29 literal_list_fails [177, 1] (w:1, o:170, a:1, s:1, b:0),
% 0.74/1.29 literal_list_terminates [178, 1] (w:1, o:171, a:1, s:1, b:0),
% 0.74/1.29 literal_succeeds [180, 1] (w:1, o:172, a:1, s:1, b:0),
% 0.74/1.29 literal_fails [181, 1] (w:1, o:173, a:1, s:1, b:0),
% 0.74/1.29 literal_terminates [182, 1] (w:1, o:174, a:1, s:1, b:0),
% 0.74/1.29 formula_succeeds [184, 1] (w:1, o:150, a:1, s:1, b:0),
% 0.74/1.29 formula_fails [185, 1] (w:1, o:151, a:1, s:1, b:0),
% 0.74/1.29 formula_terminates [186, 1] (w:1, o:152, a:1, s:1, b:0),
% 0.74/1.29 member_succeeds [189, 2] (w:1, o:267, a:1, s:1, b:0),
% 0.74/1.29 member_fails [190, 2] (w:1, o:268, a:1, s:1, b:0),
% 0.74/1.29 member_terminates [191, 2] (w:1, o:269, a:1, s:1, b:0),
% 0.74/1.29 list_succeeds [193, 1] (w:1, o:166, a:1, s:1, b:0),
% 0.74/1.29 list_fails [194, 1] (w:1, o:167, a:1, s:1, b:0),
% 0.74/1.29 list_terminates [195, 1] (w:1, o:168, a:1, s:1, b:0),
% 0.74/1.29 sub [201, 2] (w:1, o:270, a:1, s:1, b:0),
% 0.74/1.29 alpha1 [210, 2] (w:1, o:271, a:1, s:1, b:1),
% 0.74/1.29 alpha2 [211, 2] (w:1, o:290, a:1, s:1, b:1),
% 0.74/1.29 alpha3 [212, 2] (w:1, o:327, a:1, s:1, b:1),
% 0.74/1.29 alpha4 [213, 3] (w:1, o:627, a:1, s:1, b:1),
% 0.74/1.29 alpha5 [214, 3] (w:1, o:632, a:1, s:1, b:1),
% 0.74/1.29 alpha6 [215, 3] (w:1, o:633, a:1, s:1, b:1),
% 0.74/1.29 alpha7 [216, 3] (w:1, o:641, a:1, s:1, b:1),
% 0.74/1.29 alpha8 [217, 3] (w:1, o:646, a:1, s:1, b:1),
% 0.74/1.29 alpha9 [218, 2] (w:1, o:330, a:1, s:1, b:1),
% 0.74/1.29 alpha10 [219, 3] (w:1, o:647, a:1, s:1, b:1),
% 0.74/1.29 alpha11 [220, 3] (w:1, o:651, a:1, s:1, b:1),
% 0.74/1.29 alpha12 [221, 2] (w:1, o:273, a:1, s:1, b:1),
% 0.74/1.29 alpha13 [222, 2] (w:1, o:277, a:1, s:1, b:1),
% 0.74/1.29 alpha14 [223, 1] (w:1, o:175, a:1, s:1, b:1),
% 0.74/1.29 alpha15 [224, 1] (w:1, o:176, a:1, s:1, b:1),
% 0.74/1.29 alpha16 [225, 1] (w:1, o:177, a:1, s:1, b:1),
% 0.74/1.29 alpha17 [226, 2] (w:1, o:278, a:1, s:1, b:1),
% 0.74/1.29 alpha18 [227, 1] (w:1, o:178, a:1, s:1, b:1),
% 0.74/1.29 alpha19 [228, 1] (w:1, o:179, a:1, s:1, b:1),
% 0.74/1.29 alpha20 [229, 1] (w:1, o:184, a:1, s:1, b:1),
% 0.74/1.29 alpha21 [230, 2] (w:1, o:291, a:1, s:1, b:1),
% 0.74/1.29 alpha22 [231, 2] (w:1, o:292, a:1, s:1, b:1),
% 0.74/1.29 alpha23 [232, 1] (w:1, o:185, a:1, s:1, b:1),
% 0.74/1.29 alpha24 [233, 1] (w:1, o:186, a:1, s:1, b:1),
% 0.74/1.29 alpha25 [234, 2] (w:1, o:298, a:1, s:1, b:1),
% 0.74/1.29 alpha26 [235, 3] (w:1, o:723, a:1, s:1, b:1),
% 0.74/1.29 alpha27 [236, 2] (w:1, o:304, a:1, s:1, b:1),
% 0.74/1.29 alpha28 [237, 3] (w:1, o:724, a:1, s:1, b:1),
% 0.74/1.29 alpha29 [238, 2] (w:1, o:306, a:1, s:1, b:1),
% 0.74/1.29 alpha30 [239, 3] (w:1, o:598, a:1, s:1, b:1),
% 0.74/1.29 alpha31 [240, 3] (w:1, o:608, a:1, s:1, b:1),
% 0.74/1.29 alpha32 [241, 3] (w:1, o:616, a:1, s:1, b:1),
% 0.74/1.29 alpha33 [242, 3] (w:1, o:621, a:1, s:1, b:1),
% 0.74/1.29 alpha34 [243, 3] (w:1, o:622, a:1, s:1, b:1),
% 0.74/1.29 alpha35 [244, 3] (w:1, o:623, a:1, s:1, b:1),
% 0.74/1.29 alpha36 [245, 3] (w:1, o:624, a:1, s:1, b:1),
% 0.74/1.29 alpha37 [246, 3] (w:1, o:625, a:1, s:1, b:1),
% 0.74/1.29 alpha38 [247, 4] (w:1, o:742, a:1, s:1, b:1),
% 0.74/1.29 alpha39 [248, 3] (w:1, o:626, a:1, s:1, b:1),
% 0.74/1.29 alpha40 [249, 4] (w:1, o:746, a:1, s:1, b:1),
% 0.74/1.29 alpha41 [250, 3] (w:1, o:628, a:1, s:1, b:1),
% 0.74/1.29 alpha42 [251, 2] (w:1, o:331, a:1, s:1, b:1),
% 0.74/1.29 alpha43 [252, 3] (w:1, o:629, a:1, s:1, b:1),
% 0.74/1.29 alpha44 [253, 3] (w:1, o:630, a:1, s:1, b:1),
% 0.74/1.29 alpha45 [254, 3] (w:1, o:631, a:1, s:1, b:1),
% 0.74/1.29 alpha46 [255, 2] (w:1, o:332, a:1, s:1, b:1),
% 0.74/1.29 alpha47 [256, 1] (w:1, o:187, a:1, s:1, b:1),
% 0.74/1.29 alpha48 [257, 2] (w:1, o:333, a:1, s:1, b:1),
% 0.74/1.29 alpha49 [258, 2] (w:1, o:334, a:1, s:1, b:1),
% 0.74/1.29 alpha50 [259, 2] (w:1, o:335, a:1, s:1, b:1),
% 0.74/1.29 alpha51 [260, 1] (w:1, o:188, a:1, s:1, b:1),
% 0.74/1.29 alpha52 [261, 2] (w:1, o:336, a:1, s:1, b:1),
% 0.74/1.29 alpha53 [262, 1] (w:1, o:189, a:1, s:1, b:1),
% 0.74/1.29 alpha54 [263, 2] (w:1, o:337, a:1, s:1, b:1),
% 0.74/1.29 alpha55 [264, 1] (w:1, o:190, a:1, s:1, b:1),
% 0.74/1.29 alpha56 [265, 2] (w:1, o:338, a:1, s:1, b:1),
% 0.74/1.29 alpha57 [266, 2] (w:1, o:339, a:1, s:1, b:1),
% 0.74/1.29 alpha58 [267, 2] (w:1, o:340, a:1, s:1, b:1),
% 0.74/1.29 alpha59 [268, 2] (w:1, o:341, a:1, s:1, b:1),
% 0.74/1.29 alpha60 [269, 3] (w:1, o:634, a:1, s:1, b:1),
% 0.74/1.29 alpha61 [270, 3] (w:1, o:635, a:1, s:1, b:1),
% 0.74/1.29 alpha62 [271, 4] (w:1, o:747, a:1, s:1, b:1),
% 0.74/1.29 alpha63 [272, 3] (w:1, o:636, a:1, s:1, b:1),
% 0.74/1.29 alpha64 [273, 4] (w:1, o:748, a:1, s:1, b:1),
% 0.74/1.29 alpha65 [274, 3] (w:1, o:637, a:1, s:1, b:1),
% 0.74/1.29 alpha66 [275, 4] (w:1, o:749, a:1, s:1, b:1),
% 0.74/1.29 alpha67 [276, 3] (w:1, o:638, a:1, s:1, b:1),
% 0.74/1.29 alpha68 [277, 3] (w:1, o:639, a:1, s:1, b:1),
% 0.74/1.29 alpha69 [278, 3] (w:1, o:640, a:1, s:1, b:1),
% 0.74/1.29 alpha70 [279, 3] (w:1, o:642, a:1, s:1, b:1),
% 0.74/1.29 alpha71 [280, 4] (w:1, o:750, a:1, s:1, b:1),
% 0.74/1.29 alpha72 [281, 3] (w:1, o:643, a:1, s:1, b:1),
% 0.74/1.29 alpha73 [282, 3] (w:1, o:644, a:1, s:1, b:1),
% 0.74/1.29 alpha74 [283, 3] (w:1, o:645, a:1, s:1, b:1),
% 0.74/1.29 alpha75 [284, 1] (w:1, o:191, a:1, s:1, b:1),
% 0.74/1.29 alpha76 [285, 1] (w:1, o:192, a:1, s:1, b:1),
% 0.74/1.29 alpha77 [286, 1] (w:1, o:193, a:1, s:1, b:1),
% 0.74/1.29 alpha78 [287, 2] (w:1, o:342, a:1, s:1, b:1),
% 0.74/1.29 alpha79 [288, 2] (w:1, o:343, a:1, s:1, b:1),
% 0.74/1.29 alpha80 [289, 3] (w:1, o:725, a:1, s:1, b:1),
% 0.74/1.29 alpha81 [290, 2] (w:1, o:328, a:1, s:1, b:1),
% 0.74/1.29 alpha82 [291, 3] (w:1, o:726, a:1, s:1, b:1),
% 0.74/1.29 alpha83 [292, 2] (w:1, o:329, a:1, s:1, b:1),
% 0.74/1.29 alpha84 [293, 3] (w:1, o:727, a:1, s:1, b:1),
% 0.74/1.29 alpha85 [294, 3] (w:1, o:728, a:1, s:1, b:1),
% 0.74/1.29 alpha86 [295, 3] (w:1, o:729, a:1, s:1, b:1),
% 0.74/1.29 alpha87 [296, 3] (w:1, o:730, a:1, s:1, b:1),
% 0.74/1.29 alpha88 [297, 3] (w:1, o:731, a:1, s:1, b:1),
% 0.74/1.29 alpha89 [298, 3] (w:1, o:732, a:1, s:1, b:1),
% 0.74/1.29 alpha90 [299, 3] (w:1, o:733, a:1, s:1, b:1),
% 0.74/1.29 alpha91 [300, 3] (w:1, o:734, a:1, s:1, b:1),
% 0.74/1.29 alpha92 [301, 3] (w:1, o:735, a:1, s:1, b:1),
% 0.74/1.29 alpha93 [302, 3] (w:1, o:736, a:1, s:1, b:1),
% 0.74/1.29 alpha94 [303, 5] (w:1, o:763, a:1, s:1, b:1),
% 0.74/1.29 alpha95 [304, 3] (w:1, o:737, a:1, s:1, b:1),
% 0.74/1.29 alpha96 [305, 3] (w:1, o:738, a:1, s:1, b:1),
% 0.74/1.29 alpha97 [306, 3] (w:1, o:739, a:1, s:1, b:1),
% 0.74/1.29 alpha98 [307, 1] (w:1, o:194, a:1, s:1, b:1),
% 0.74/1.29 alpha99 [308, 2] (w:1, o:344, a:1, s:1, b:1),
% 0.74/1.29 alpha100 [309, 1] (w:1, o:180, a:1, s:1, b:1),
% 0.74/1.29 alpha101 [310, 2] (w:1, o:279, a:1, s:1, b:1),
% 0.74/1.29 alpha102 [311, 1] (w:1, o:181, a:1, s:1, b:1),
% 0.74/1.29 alpha103 [312, 2] (w:1, o:280, a:1, s:1, b:1),
% 0.74/1.29 alpha104 [313, 2] (w:1, o:281, a:1, s:1, b:1),
% 0.74/1.29 alpha105 [314, 2] (w:1, o:282, a:1, s:1, b:1),
% 0.74/1.29 alpha106 [315, 2] (w:1, o:283, a:1, s:1, b:1),
% 0.74/1.29 alpha107 [316, 3] (w:1, o:648, a:1, s:1, b:1),
% 0.74/1.29 alpha108 [317, 3] (w:1, o:649, a:1, s:1, b:1),
% 0.74/1.29 alpha109 [318, 3] (w:1, o:650, a:1, s:1, b:1),
% 0.74/1.29 alpha110 [319, 3] (w:1, o:652, a:1, s:1, b:1),
% 0.74/1.29 alpha111 [320, 3] (w:1, o:653, a:1, s:1, b:1),
% 0.74/1.29 alpha112 [321, 3] (w:1, o:654, a:1, s:1, b:1),
% 0.74/1.29 alpha113 [322, 3] (w:1, o:655, a:1, s:1, b:1),
% 0.74/1.29 alpha114 [323, 3] (w:1, o:656, a:1, s:1, b:1),
% 0.74/1.29 alpha115 [324, 3] (w:1, o:657, a:1, s:1, b:1),
% 0.74/1.29 alpha116 [325, 3] (w:1, o:658, a:1, s:1, b:1),
% 0.74/1.29 alpha117 [326, 1] (w:1, o:182, a:1, s:1, b:1),
% 0.74/1.29 alpha118 [327, 1] (w:1, o:183, a:1, s:1, b:1),
% 0.74/1.29 alpha119 [328, 2] (w:1, o:272, a:1, s:1, b:1),
% 0.74/1.29 alpha120 [329, 2] (w:1, o:274, a:1, s:1, b:1),
% 0.74/1.29 alpha121 [330, 2] (w:1, o:275, a:1, s:1, b:1),
% 0.74/1.29 alpha122 [331, 2] (w:1, o:276, a:1, s:1, b:1),
% 0.74/1.29 alpha123 [332, 3] (w:1, o:659, a:1, s:1, b:1),
% 0.74/1.29 alpha124 [333, 3] (w:1, o:660, a:1, s:1, b:1),
% 0.74/1.29 alpha125 [334, 3] (w:1, o:661, a:1, s:1, b:1),
% 0.74/1.29 alpha126 [335, 3] (w:1, o:662, a:1, s:1, b:1),
% 0.74/1.29 alpha127 [336, 3] (w:1, o:663, a:1, s:1, b:1),
% 0.74/1.29 alpha128 [337, 3] (w:1, o:664, a:1, s:1, b:1),
% 0.74/1.29 alpha129 [338, 3] (w:1, o:665, a:1, s:1, b:1),
% 0.74/1.29 alpha130 [339, 3] (w:1, o:666, a:1, s:1, b:1),
% 0.74/1.29 alpha131 [340, 3] (w:1, o:667, a:1, s:1, b:1),
% 0.74/1.29 alpha132 [341, 3] (w:1, o:668, a:1, s:1, b:1),
% 0.74/1.29 alpha133 [342, 4] (w:1, o:751, a:1, s:1, b:1),
% 0.74/1.29 alpha134 [343, 3] (w:1, o:669, a:1, s:1, b:1),
% 0.74/1.29 alpha135 [344, 4] (w:1, o:752, a:1, s:1, b:1),
% 0.74/1.29 alpha136 [345, 3] (w:1, o:670, a:1, s:1, b:1),
% 0.74/1.29 alpha137 [346, 2] (w:1, o:284, a:1, s:1, b:1),
% 0.74/1.29 alpha138 [347, 2] (w:1, o:285, a:1, s:1, b:1),
% 0.74/1.29 alpha139 [348, 2] (w:1, o:286, a:1, s:1, b:1),
% 0.74/1.29 alpha140 [349, 3] (w:1, o:671, a:1, s:1, b:1),
% 0.74/1.29 alpha141 [350, 3] (w:1, o:672, a:1, s:1, b:1),
% 0.74/1.29 alpha142 [351, 3] (w:1, o:673, a:1, s:1, b:1),
% 0.74/1.29 alpha143 [352, 3] (w:1, o:674, a:1, s:1, b:1),
% 0.74/1.29 alpha144 [353, 3] (w:1, o:675, a:1, s:1, b:1),
% 0.74/1.29 alpha145 [354, 3] (w:1, o:676, a:1, s:1, b:1),
% 0.74/1.29 alpha146 [355, 3] (w:1, o:677, a:1, s:1, b:1),
% 0.74/1.29 alpha147 [356, 3] (w:1, o:678, a:1, s:1, b:1),
% 0.74/1.29 alpha148 [357, 3] (w:1, o:679, a:1, s:1, b:1),
% 0.74/1.29 alpha149 [358, 4] (w:1, o:753, a:1, s:1, b:1),
% 0.74/1.29 alpha150 [359, 2] (w:1, o:287, a:1, s:1, b:1),
% 0.74/1.29 alpha151 [360, 2] (w:1, o:288, a:1, s:1, b:1),
% 0.74/1.29 alpha152 [361, 2] (w:1, o:289, a:1, s:1, b:1),
% 0.74/1.29 alpha153 [362, 3] (w:1, o:680, a:1, s:1, b:1),
% 0.74/1.29 alpha154 [363, 3] (w:1, o:681, a:1, s:1, b:1),
% 0.74/1.29 alpha155 [364, 3] (w:1, o:682, a:1, s:1, b:1),
% 0.74/1.29 alpha156 [365, 3] (w:1, o:683, a:1, s:1, b:1),
% 0.74/1.29 alpha157 [366, 3] (w:1, o:684, a:1, s:1, b:1),
% 0.74/1.29 alpha158 [367, 3] (w:1, o:685, a:1, s:1, b:1),
% 0.74/1.29 alpha159 [368, 3] (w:1, o:686, a:1, s:1, b:1),
% 0.74/1.29 alpha160 [369, 3] (w:1, o:687, a:1, s:1, b:1),
% 0.74/1.29 alpha161 [370, 3] (w:1, o:688, a:1, s:1, b:1),
% 0.74/1.29 alpha162 [371, 3] (w:1, o:689, a:1, s:1, b:1),
% 0.74/1.29 alpha163 [372, 3] (w:1, o:690, a:1, s:1, b:1),
% 0.74/1.29 alpha164 [373, 3] (w:1, o:691, a:1, s:1, b:1),
% 0.74/1.29 alpha165 [374, 5] (w:1, o:764, a:1, s:1, b:1),
% 0.74/1.29 alpha166 [375, 3] (w:1, o:692, a:1, s:1, b:1),
% 0.74/1.29 alpha167 [376, 3] (w:1, o:693, a:1, s:1, b:1),
% 0.74/1.29 alpha168 [377, 3] (w:1, o:694, a:1, s:1, b:1),
% 0.74/1.29 alpha169 [378, 3] (w:1, o:695, a:1, s:1, b:1),
% 0.74/1.29 alpha170 [379, 3] (w:1, o:696, a:1, s:1, b:1),
% 0.74/1.29 alpha171 [380, 3] (w:1, o:697, a:1, s:1, b:1),
% 0.74/1.29 alpha172 [381, 3] (w:1, o:698, a:1, s:1, b:1),
% 0.74/1.29 alpha173 [382, 3] (w:1, o:699, a:1, s:1, b:1),
% 0.74/1.29 alpha174 [383, 3] (w:1, o:700, a:1, s:1, b:1),
% 0.74/1.29 alpha175 [384, 3] (w:1, o:701, a:1, s:1, b:1),
% 0.74/1.29 alpha176 [385, 3] (w:1, o:702, a:1, s:1, b:1),
% 0.74/1.29 alpha177 [386, 3] (w:1, o:703, a:1, s:1, b:1),
% 0.74/1.29 alpha178 [387, 3] (w:1, o:704, a:1, s:1, b:1),
% 0.74/1.29 alpha179 [388, 3] (w:1, o:705, a:1, s:1, b:1),
% 0.74/1.29 alpha180 [389, 3] (w:1, o:706, a:1, s:1, b:1),
% 0.74/1.29 alpha181 [390, 3] (w:1, o:707, a:1, s:1, b:1),
% 0.74/1.29 alpha182 [391, 3] (w:1, o:708, a:1, s:1, b:1),
% 0.74/1.29 alpha183 [392, 3] (w:1, o:709, a:1, s:1, b:1),
% 0.74/1.29 alpha184 [393, 3] (w:1, o:710, a:1, s:1, b:1),
% 0.74/1.29 alpha185 [394, 3] (w:1, o:711, a:1, s:1, b:1),
% 0.74/1.29 alpha186 [395, 3] (w:1, o:712, a:1, s:1, b:1),
% 0.74/1.29 alpha187 [396, 3] (w:1, o:713, a:1, s:1, b:1),
% 0.74/1.29 alpha188 [397, 3] (w:1, o:714, a:1, s:1, b:1),
% 0.74/1.29 alpha189 [398, 3] (w:1, o:715, a:1, s:1, b:1),
% 0.74/1.29 alpha190 [399, 3] (w:1, o:716, a:1, s:1, b:1),
% 0.74/1.29 alpha191 [400, 3] (w:1, o:717, a:1, s:1, b:1),
% 0.74/1.29 alpha192 [401, 3] (w:1, o:718, a:1, s:1, b:1),
% 0.74/1.29 alpha193 [402, 4] (w:1, o:754, a:1, s:1, b:1),
% 0.74/1.29 alpha194 [403, 3] (w:1, o:719, a:1, s:1, b:1),
% 0.74/1.29 alpha195 [404, 4] (w:1, o:755, a:1, s:1, b:1),
% 0.74/1.29 alpha196 [405, 3] (w:1, o:720, a:1, s:1, b:1),
% 0.74/1.29 alpha197 [406, 4] (w:1, o:756, a:1, s:1, b:1),
% 0.74/1.29 alpha198 [407, 3] (w:1, o:721, a:1, s:1, b:1),
% 0.74/1.29 alpha199 [408, 3] (w:1, o:722, a:1, s:1, b:1),
% 0.74/1.29 alpha200 [409, 3] (w:1, o:532, a:1, s:1, b:1),
% 0.74/1.29 alpha201 [410, 3] (w:1, o:533, a:1, s:1, b:1),
% 0.74/1.29 alpha202 [411, 3] (w:1, o:534, a:1, s:1, b:1),
% 0.74/1.29 alpha203 [412, 3] (w:1, o:535, a:1, s:1, b:1),
% 0.74/1.29 alpha204 [413, 3] (w:1, o:536, a:1, s:1, b:1),
% 0.74/1.29 alpha205 [414, 3] (w:1, o:537, a:1, s:1, b:1),
% 0.74/1.29 alpha206 [415, 3] (w:1, o:538, a:1, s:1, b:1),
% 0.74/1.29 alpha207 [416, 3] (w:1, o:539, a:1, s:1, b:1),
% 0.74/1.29 alpha208 [417, 3] (w:1, o:540, a:1, s:1, b:1),
% 0.74/1.29 alpha209 [418, 3] (w:1, o:541, a:1, s:1, b:1),
% 0.74/1.29 alpha210 [419, 3] (w:1, o:542, a:1, s:1, b:1),
% 0.74/1.29 alpha211 [420, 3] (w:1, o:543, a:1, s:1, b:1),
% 0.74/1.29 alpha212 [421, 3] (w:1, o:544, a:1, s:1, b:1),
% 0.74/1.29 alpha213 [422, 3] (w:1, o:545, a:1, s:1, b:1),
% 0.74/1.29 alpha214 [423, 3] (w:1, o:546, a:1, s:1, b:1),
% 0.74/1.29 alpha215 [424, 3] (w:1, o:547, a:1, s:1, b:1),
% 0.74/1.29 alpha216 [425, 3] (w:1, o:548, a:1, s:1, b:1),
% 0.74/1.29 alpha217 [426, 3] (w:1, o:549, a:1, s:1, b:1),
% 0.74/1.29 alpha218 [427, 3] (w:1, o:550, a:1, s:1, b:1),
% 0.74/1.29 alpha219 [428, 3] (w:1, o:551, a:1, s:1, b:1),
% 0.74/1.29 alpha220 [429, 3] (w:1, o:552, a:1, s:1, b:1),
% 0.74/1.29 alpha221 [430, 3] (w:1, o:553, a:1, s:1, b:1),
% 0.74/1.29 alpha222 [431, 3] (w:1, o:554, a:1, s:1, b:1),
% 0.74/1.29 alpha223 [432, 3] (w:1, o:555, a:1, s:1, b:1),
% 0.74/1.29 alpha224 [433, 3] (w:1, o:556, a:1, s:1, b:1),
% 0.74/1.29 alpha225 [434, 3] (w:1, o:557, a:1, s:1, b:1),
% 0.74/1.29 alpha226 [435, 0] (w:1, o:135, a:1, s:1, b:1),
% 0.74/1.29 alpha227 [436, 4] (w:1, o:740, a:1, s:1, b:1),
% 0.74/1.29 alpha228 [437, 3] (w:1, o:558, a:1, s:1, b:1),
% 0.74/1.29 alpha229 [438, 2] (w:1, o:307, a:1, s:1, b:1),
% 0.74/1.29 alpha230 [439, 2] (w:1, o:308, a:1, s:1, b:1),
% 0.74/1.29 alpha231 [440, 2] (w:1, o:309, a:1, s:1, b:1),
% 0.74/1.29 alpha232 [441, 2] (w:1, o:310, a:1, s:1, b:1),
% 0.74/1.29 alpha233 [442, 2] (w:1, o:311, a:1, s:1, b:1),
% 0.74/1.29 alpha234 [443, 2] (w:1, o:312, a:1, s:1, b:1),
% 0.74/1.29 alpha235 [444, 2] (w:1, o:313, a:1, s:1, b:1),
% 0.74/1.29 alpha236 [445, 2] (w:1, o:314, a:1, s:1, b:1),
% 0.74/1.29 alpha237 [446, 2] (w:1, o:315, a:1, s:1, b:1),
% 0.74/1.29 alpha238 [447, 3] (w:1, o:559, a:1, s:1, b:1),
% 0.74/1.29 alpha239 [448, 2] (w:1, o:316, a:1, s:1, b:1),
% 0.74/1.29 alpha240 [449, 2] (w:1, o:293, a:1, s:1, b:1),
% 0.74/1.29 alpha241 [450, 2] (w:1, o:294, a:1, s:1, b:1),
% 0.74/1.29 alpha242 [451, 3] (w:1, o:560, a:1, s:1, b:1),
% 0.74/1.29 alpha243 [452, 3] (w:1, o:561, a:1, s:1, b:1),
% 0.74/1.29 alpha244 [453, 2] (w:1, o:295, a:1, s:1, b:1),
% 0.74/1.29 alpha245 [454, 2] (w:1, o:296, a:1, s:1, b:1),
% 0.74/1.29 alpha246 [455, 2] (w:1, o:297, a:1, s:1, b:1),
% 0.74/1.29 alpha247 [456, 3] (w:1, o:562, a:1, s:1, b:1),
% 0.74/1.29 alpha248 [457, 3] (w:1, o:563, a:1, s:1, b:1),
% 0.74/1.29 alpha249 [458, 3] (w:1, o:564, a:1, s:1, b:1),
% 0.74/1.29 alpha250 [459, 2] (w:1, o:317, a:1, s:1, b:1),
% 0.74/1.29 alpha251 [460, 2] (w:1, o:318, a:1, s:1, b:1),
% 0.74/1.29 alpha252 [461, 2] (w:1, o:319, a:1, s:1, b:1),
% 0.74/1.29 alpha253 [462, 3] (w:1, o:565, a:1, s:1, b:1),
% 0.74/1.29 alpha254 [463, 3] (w:1, o:566, a:1, s:1, b:1),
% 0.74/1.29 alpha255 [464, 3] (w:1, o:567, a:1, s:1, b:1),
% 0.74/1.29 alpha256 [465, 2] (w:1, o:320, a:1, s:1, b:1),
% 0.74/1.29 alpha257 [466, 2] (w:1, o:321, a:1, s:1, b:1),
% 0.74/1.29 alpha258 [467, 2] (w:1, o:322, a:1, s:1, b:1),
% 0.74/1.29 alpha259 [468, 3] (w:1, o:568, a:1, s:1, b:1),
% 0.74/1.29 alpha260 [469, 3] (w:1, o:569, a:1, s:1, b:1),
% 0.74/1.29 alpha261 [470, 3] (w:1, o:570, a:1, s:1, b:1),
% 0.74/1.29 alpha262 [471, 2] (w:1, o:299, a:1, s:1, b:1),
% 0.74/1.29 alpha263 [472, 2] (w:1, o:300, a:1, s:1, b:1),
% 0.74/1.29 alpha264 [473, 2] (w:1, o:301, a:1, s:1, b:1),
% 0.74/1.29 alpha265 [474, 3] (w:1, o:571, a:1, s:1, b:1),
% 0.74/1.29 alpha266 [475, 3] (w:1, o:572, a:1, s:1, b:1),
% 0.74/1.29 alpha267 [476, 3] (w:1, o:573, a:1, s:1, b:1),
% 0.74/1.29 alpha268 [477, 2] (w:1, o:302, a:1, s:1, b:1),
% 0.74/1.29 alpha269 [478, 2] (w:1, o:303, a:1, s:1, b:1),
% 0.74/1.29 alpha270 [479, 2] (w:1, o:323, a:1, s:1, b:1),
% 0.74/1.29 alpha271 [480, 3] (w:1, o:574, a:1, s:1, b:1),
% 0.74/1.29 alpha272 [481, 3] (w:1, o:575, a:1, s:1, b:1),
% 0.74/1.29 alpha273 [482, 3] (w:1, o:576, a:1, s:1, b:1),
% 0.74/1.29 alpha274 [483, 2] (w:1, o:324, a:1, s:1, b:1),
% 0.74/1.29 alpha275 [484, 2] (w:1, o:325, a:1, s:1, b:1),
% 0.74/1.29 alpha276 [485, 2] (w:1, o:326, a:1, s:1, b:1),
% 0.74/1.29 alpha277 [486, 3] (w:1, o:577, a:1, s:1, b:1),
% 0.74/1.29 alpha278 [487, 3] (w:1, o:578, a:1, s:1, b:1),
% 0.74/1.29 alpha279 [488, 3] (w:1, o:579, a:1, s:1, b:1),
% 0.74/1.29 alpha280 [489, 3] (w:1, o:580, a:1, s:1, b:1),
% 0.74/1.29 alpha281 [490, 2] (w:1, o:305, a:1, s:1, b:1),
% 0.74/1.29 alpha282 [491, 3] (w:1, o:581, a:1, s:1, b:1),
% 0.74/1.29 alpha283 [492, 3] (w:1, o:582, a:1, s:1, b:1),
% 0.74/1.29 alpha284 [493, 3] (w:1, o:583, a:1, s:1, b:1),
% 0.74/1.29 alpha285 [494, 3] (w:1, o:584, a:1, s:1, b:1),
% 0.74/1.29 alpha286 [495, 3] (w:1, o:585, a:1, s:1, b:1),
% 0.74/1.29 alpha287 [496, 3] (w:1, o:586, a:1, s:1, b:1),
% 0.74/1.29 alpha288 [497, 3] (w:1, o:587, a:1, s:1, b:1),
% 0.74/1.29 alpha289 [498, 3] (w:1, o:588, a:1, s:1, b:1),
% 0.74/1.29 alpha290 [499, 3] (w:1, o:589, a:1, s:1, b:1),
% 0.74/1.29 alpha291 [500, 3] (w:1, o:590, a:1, s:1, b:1),
% 0.74/1.29 alpha292 [501, 3] (w:1, o:591, a:1, s:1, b:1),
% 0.74/1.29 alpha293 [502, 3] (w:1, o:592, a:1, s:1, b:1),
% 0.74/1.29 alpha294 [503, 3] (w:1, o:593, a:1, s:1, b:1),
% 0.74/1.29 alpha295 [504, 3] (w:1, o:594, a:1, s:1, b:1),
% 0.74/1.29 alpha296 [505, 3] (w:1, o:595, a:1, s:1, b:1),
% 0.74/1.29 alpha297 [506, 3] (w:1, o:596, a:1, s:1, b:1),
% 0.74/1.29 alpha298 [507, 4] (w:1, o:741, a:1, s:1, b:1),
% 0.74/1.29 alpha299 [508, 3] (w:1, o:597, a:1, s:1, b:1),
% 0.74/1.29 alpha300 [509, 3] (w:1, o:599, a:1, s:1, b:1),
% 0.74/1.29 alpha301 [510, 4] (w:1, o:743, a:1, s:1, b:1),
% 0.74/1.29 alpha302 [511, 3] (w:1, o:600, a:1, s:1, b:1),
% 0.74/1.29 alpha303 [512, 3] (w:1, o:601, a:1, s:1, b:1),
% 0.74/1.29 alpha304 [513, 3] (w:1, o:602, a:1, s:1, b:1),
% 0.74/1.29 alpha305 [514, 3] (w:1, o:603, a:1, s:1, b:1),
% 0.74/1.29 alpha306 [515, 3] (w:1, o:604, a:1, s:1, b:1),
% 0.74/1.29 alpha307 [516, 3] (w:1, o:605, a:1, s:1, b:1),
% 0.74/1.29 alpha308 [517, 3] (w:1, o:606, a:1, s:1, b:1),
% 0.74/1.29 alpha309 [518, 3] (w:1, o:607, a:1, s:1, b:1),
% 0.74/1.29 alpha310 [519, 4] (w:1, o:744, a:1, s:1, b:1),
% 0.74/1.29 alpha311 [520, 3] (w:1, o:609, a:1, s:1, b:1),
% 0.74/1.29 alpha312 [521, 3] (w:1, o:610, a:1, s:1, b:1),
% 0.74/1.29 alpha313 [522, 5] (w:1, o:765, a:1, s:1, b:1),
% 0.74/1.29 alpha314 [523, 3] (w:1, o:611, a:1, s:1, b:1),
% 0.74/1.29 alpha315 [524, 3] (w:1, o:612, a:1, s:1, b:1),
% 0.74/1.29 alpha316 [525, 3] (w:1, o:613, a:1, s:1, b:1),
% 0.74/1.29 alpha317 [526, 5] (w:1, o:766, a:1, s:1, b:1),
% 0.74/1.29 alpha318 [527, 3] (w:1, o:614, a:1, s:1, b:1),
% 0.74/1.29 alpha319 [528, 3] (w:1, o:615, a:1, s:1, b:1),
% 0.74/1.29 alpha320 [529, 3] (w:1, o:617, a:1, s:1, b:1),
% 0.74/1.29 alpha321 [530, 3] (w:1, o:618, a:1, s:1, b:1),
% 0.74/1.29 alpha322 [531, 3] (w:1, o:619, a:1, s:1, b:1),
% 0.74/1.29 alpha323 [532, 4] (w:1, o:745, a:1, s:1, b:1),
% 0.74/1.29 alpha324 [533, 3] (w:1, o:620, a:1, s:1, b:1),
% 0.74/1.29 alpha325 [534, 5] (w:1, o:767, a:1, s:1, b:1),
% 0.74/1.29 alpha326 [535, 5] (w:1, o:768, a:1, s:1, b:1),
% 0.74/1.29 skol1 [536, 2] (w:1, o:345, a:1, s:1, b:1),
% 0.74/1.29 skol2 [537, 2] (w:1, o:378, a:1, s:1, b:1),
% 0.74/1.29 skol3 [538, 2] (w:1, o:382, a:1, s:1, b:1),
% 0.74/1.29 skol4 [539, 2] (w:1, o:383, a:1, s:1, b:1),
% 0.74/1.29 skol5 [540, 2] (w:1, o:384, a:1, s:1, b:1),
% 0.74/1.29 skol6 [541, 2] (w:1, o:385, a:1, s:1, b:1),
% 0.74/1.29 skol7 [542, 2] (w:1, o:386, a:1, s:1, b:1),
% 0.74/1.29 skol8 [543, 2] (w:1, o:387, a:1, s:1, b:1),
% 0.74/1.29 skol9 [544, 2] (w:1, o:388, a:1, s:1, b:1),
% 0.74/1.29 skol10 [545, 2] (w:1, o:346, a:1, s:1, b:1),
% 0.74/1.29 skol11 [546, 2] (w:1, o:352, a:1, s:1, b:1),
% 0.74/1.29 skol12 [547, 2] (w:1, o:354, a:1, s:1, b:1),
% 0.74/1.29 skol13 [548, 2] (w:1, o:356, a:1, s:1, b:1),
% 0.74/1.29 skol14 [549, 2] (w:1, o:362, a:1, s:1, b:1),
% 0.74/1.29 skol15 [550, 2] (w:1, o:366, a:1, s:1, b:1),
% 0.74/1.29 skol16 [551, 3] (w:1, o:402, a:1, s:1, b:1),
% 0.74/1.29 skol17 [552, 3] (w:1, o:408, a:1, s:1, b:1),
% 0.74/1.29 skol18 [553, 3] (w:1, o:415, a:1, s:1, b:1),
% 0.74/1.29 skol19 [554, 3] (w:1, o:426, a:1, s:1, b:1),
% 0.74/1.29 skol20 [555, 3] (w:1, o:461, a:1, s:1, b:1),
% 0.74/1.29 skol21 [556, 3] (w:1, o:472, a:1, s:1, b:1),
% 0.74/1.29 skol22 [557, 3] (w:1, o:473, a:1, s:1, b:1),
% 0.74/1.29 skol23 [558, 3] (w:1, o:476, a:1, s:1, b:1),
% 0.74/1.29 skol24 [559, 3] (w:1, o:477, a:1, s:1, b:1),
% 0.74/1.29 skol25 [560, 3] (w:1, o:478, a:1, s:1, b:1),
% 0.74/1.29 skol26 [561, 3] (w:1, o:479, a:1, s:1, b:1),
% 0.74/1.29 skol27 [562, 3] (w:1, o:480, a:1, s:1, b:1),
% 0.74/1.29 skol28 [563, 3] (w:1, o:481, a:1, s:1, b:1),
% 0.74/1.29 skol29 [564, 3] (w:1, o:482, a:1, s:1, b:1),
% 0.74/1.29 skol30 [565, 3] (w:1, o:483, a:1, s:1, b:1),
% 0.74/1.29 skol31 [566, 3] (w:1, o:484, a:1, s:1, b:1),
% 0.74/1.29 skol32 [567, 3] (w:1, o:485, a:1, s:1, b:1),
% 0.74/1.29 skol33 [568, 3] (w:1, o:486, a:1, s:1, b:1),
% 0.74/1.29 skol34 [569, 3] (w:1, o:487, a:1, s:1, b:1),
% 0.74/1.29 skol35 [570, 3] (w:1, o:488, a:1, s:1, b:1),
% 0.74/1.29 skol36 [571, 3] (w:1, o:489, a:1, s:1, b:1),
% 0.74/1.29 skol37 [572, 3] (w:1, o:490, a:1, s:1, b:1),
% 0.74/1.29 skol38 [573, 3] (w:1, o:491, a:1, s:1, b:1),
% 0.74/1.29 skol39 [574, 3] (w:1, o:492, a:1, s:1, b:1),
% 0.74/1.29 skol40 [575, 3] (w:1, o:493, a:1, s:1, b:1),
% 0.74/1.29 skol41 [576, 3] (w:1, o:494, a:1, s:1, b:1),
% 0.74/1.29 skol42 [577, 3] (w:1, o:495, a:1, s:1, b:1),
% 0.74/1.29 skol43 [578, 3] (w:1, o:496, a:1, s:1, b:1),
% 0.74/1.29 skol44 [579, 3] (w:1, o:497, a:1, s:1, b:1),
% 0.74/1.29 skol45 [580, 3] (w:1, o:498, a:1, s:1, b:1),
% 0.74/1.29 skol46 [581, 3] (w:1, o:499, a:1, s:1, b:1),
% 0.74/1.29 skol47 [582, 3] (w:1, o:500, a:1, s:1, b:1),
% 0.74/1.29 skol48 [583, 3] (w:1, o:501, a:1, s:1, b:1),
% 0.74/1.29 skol49 [584, 3] (w:1, o:502, a:1, s:1, b:1),
% 0.74/1.29 skol50 [585, 3] (w:1, o:503, a:1, s:1, b:1),
% 0.74/1.29 skol51 [586, 4] (w:1, o:757, a:1, s:1, b:1),
% 0.74/1.29 skol52 [587, 3] (w:1, o:504, a:1, s:1, b:1),
% 0.74/1.29 skol53 [588, 3] (w:1, o:505, a:1, s:1, b:1),
% 0.74/1.29 skol54 [589, 3] (w:1, o:506, a:1, s:1, b:1),
% 0.74/1.29 skol55 [590, 3] (w:1, o:507, a:1, s:1, b:1),
% 0.74/1.29 skol56 [591, 3] (w:1, o:508, a:1, s:1, b:1),
% 0.74/1.29 skol57 [592, 4] (w:1, o:758, a:1, s:1, b:1),
% 0.74/1.29 skol58 [593, 3] (w:1, o:509, a:1, s:1, b:1),
% 0.74/1.29 skol59 [594, 3] (w:1, o:510, a:1, s:1, b:1),
% 0.74/1.29 skol60 [595, 3] (w:1, o:511, a:1, s:1, b:1),
% 0.74/1.29 skol61 [596, 3] (w:1, o:512, a:1, s:1, b:1),
% 0.74/1.29 skol62 [597, 3] (w:1, o:513, a:1, s:1, b:1),
% 0.74/1.29 skol63 [598, 4] (w:1, o:759, a:1, s:1, b:1),
% 0.74/1.29 skol64 [599, 3] (w:1, o:514, a:1, s:1, b:1),
% 0.74/1.29 skol65 [600, 3] (w:1, o:515, a:1, s:1, b:1),
% 0.74/1.29 skol66 [601, 3] (w:1, o:516, a:1, s:1, b:1),
% 0.74/1.29 skol67 [602, 4] (w:1, o:760, a:1, s:1, b:1),
% 0.74/1.29 skol68 [603, 3] (w:1, o:517, a:1, s:1, b:1),
% 0.74/1.29 skol69 [604, 3] (w:1, o:518, a:1, s:1, b:1),
% 0.74/1.29 skol70 [605, 3] (w:1, o:519, a:1, s:1, b:1),
% 0.74/1.29 skol71 [606, 3] (w:1, o:520, a:1, s:1, b:1),
% 0.74/1.29 skol72 [607, 3] (w:1, o:521, a:1, s:1, b:1),
% 0.74/1.29 skol73 [608, 4] (w:1, o:761, a:1, s:1, b:1),
% 0.74/1.29 skol74 [609, 3] (w:1, o:522, a:1, s:1, b:1),
% 0.74/1.29 skol75 [610, 3] (w:1, o:523, a:1, s:1, b:1),
% 0.74/1.29 skol76 [611, 3] (w:1, o:524, a:1, s:1, b:1),
% 0.74/1.29 skol77 [612, 3] (w:1, o:525, a:1, s:1, b:1),
% 0.74/1.29 skol78 [613, 3] (w:1, o:526, a:1, s:1, b:1),
% 0.74/1.29 skol79 [614, 4] (w:1, o:762, a:1, s:1, b:1),
% 0.74/1.29 skol80 [615, 3] (w:1, o:527, a:1, s:1, b:1),
% 0.74/1.29 skol81 [616, 3] (w:1, o:528, a:1, s:1, b:1),
% 0.74/1.29 skol82 [617, 1] (w:1, o:195, a:1, s:1, b:1),
% 0.74/1.29 skol83 [618, 1] (w:1, o:196, a:1, s:1, b:1),
% 0.74/1.29 skol84 [619, 1] (w:1, o:197, a:1, s:1, b:1),
% 0.74/1.29 skol85 [620, 1] (w:1, o:198, a:1, s:1, b:1),
% 0.74/1.29 skol86 [621, 1] (w:1, o:199, a:1, s:1, b:1),
% 0.74/1.29 skol87 [622, 1] (w:1, o:200, a:1, s:1, b:1),
% 0.74/1.29 skol88 [623, 1] (w:1, o:201, a:1, s:1, b:1),
% 0.74/1.29 skol89 [624, 1] (w:1, o:202, a:1, s:1, b:1),
% 0.74/1.29 skol90 [625, 1] (w:1, o:203, a:1, s:1, b:1),
% 0.74/1.29 skol91 [626, 1] (w:1, o:204, a:1, s:1, b:1),
% 0.74/1.29 skol92 [627, 1] (w:1, o:205, a:1, s:1, b:1),
% 0.74/1.29 skol93 [628, 1] (w:1, o:206, a:1, s:1, b:1),
% 0.74/1.29 skol94 [629, 1] (w:1, o:207, a:1, s:1, b:1),
% 0.74/1.29 skol95 [630, 1] (w:1, o:208, a:1, s:1, b:1),
% 0.74/1.29 skol96 [631, 1] (w:1, o:209, a:1, s:1, b:1),
% 0.74/1.29 skol97 [632, 1] (w:1, o:210, a:1, s:1, b:1),
% 0.74/1.29 skol98 [633, 1] (w:1, o:211, a:1, s:1, b:1),
% 0.74/1.29 skol99 [634, 1] (w:1, o:212, a:1, s:1, b:1),
% 0.74/1.29 skol100 [635, 1] (w:1, o:213, a:1, s:1, b:1),
% 1.65/2.10 skol101 [636, 1] (w:1, o:214, a:1, s:1, b:1),
% 1.65/2.10 skol102 [637, 1] (w:1, o:215, a:1, s:1, b:1),
% 1.65/2.10 skol103 [638, 1] (w:1, o:216, a:1, s:1, b:1),
% 1.65/2.10 skol104 [639, 2] (w:1, o:347, a:1, s:1, b:1),
% 1.65/2.10 skol105 [640, 2] (w:1, o:348, a:1, s:1, b:1),
% 1.65/2.10 skol106 [641, 2] (w:1, o:349, a:1, s:1, b:1),
% 1.65/2.10 skol107 [642, 2] (w:1, o:350, a:1, s:1, b:1),
% 1.65/2.10 skol108 [643, 2] (w:1, o:351, a:1, s:1, b:1),
% 1.65/2.10 skol109 [644, 1] (w:1, o:217, a:1, s:1, b:1),
% 1.65/2.10 skol110 [645, 1] (w:1, o:218, a:1, s:1, b:1),
% 1.65/2.10 skol111 [646, 1] (w:1, o:219, a:1, s:1, b:1),
% 1.65/2.10 skol112 [647, 2] (w:1, o:353, a:1, s:1, b:1),
% 1.65/2.10 skol113 [648, 1] (w:1, o:220, a:1, s:1, b:1),
% 1.65/2.10 skol114 [649, 1] (w:1, o:221, a:1, s:1, b:1),
% 1.65/2.10 skol115 [650, 1] (w:1, o:222, a:1, s:1, b:1),
% 1.65/2.10 skol116 [651, 3] (w:1, o:427, a:1, s:1, b:1),
% 1.65/2.10 skol117 [652, 3] (w:1, o:428, a:1, s:1, b:1),
% 1.65/2.10 skol118 [653, 0] (w:1, o:136, a:1, s:1, b:1),
% 1.65/2.10 skol119 [654, 3] (w:1, o:429, a:1, s:1, b:1),
% 1.65/2.10 skol120 [655, 3] (w:1, o:430, a:1, s:1, b:1),
% 1.65/2.10 skol121 [656, 3] (w:1, o:431, a:1, s:1, b:1),
% 1.65/2.10 skol122 [657, 3] (w:1, o:432, a:1, s:1, b:1),
% 1.65/2.10 skol123 [658, 3] (w:1, o:433, a:1, s:1, b:1),
% 1.65/2.10 skol124 [659, 3] (w:1, o:434, a:1, s:1, b:1),
% 1.65/2.10 skol125 [660, 3] (w:1, o:435, a:1, s:1, b:1),
% 1.65/2.10 skol126 [661, 3] (w:1, o:436, a:1, s:1, b:1),
% 1.65/2.10 skol127 [662, 3] (w:1, o:437, a:1, s:1, b:1),
% 1.65/2.10 skol128 [663, 2] (w:1, o:355, a:1, s:1, b:1),
% 1.65/2.10 skol129 [664, 3] (w:1, o:438, a:1, s:1, b:1),
% 1.65/2.10 skol130 [665, 2] (w:1, o:357, a:1, s:1, b:1),
% 1.65/2.10 skol131 [666, 3] (w:1, o:439, a:1, s:1, b:1),
% 1.65/2.10 skol132 [667, 2] (w:1, o:358, a:1, s:1, b:1),
% 1.65/2.10 skol133 [668, 3] (w:1, o:440, a:1, s:1, b:1),
% 1.65/2.10 skol134 [669, 2] (w:1, o:359, a:1, s:1, b:1),
% 1.65/2.10 skol135 [670, 3] (w:1, o:441, a:1, s:1, b:1),
% 1.65/2.10 skol136 [671, 2] (w:1, o:360, a:1, s:1, b:1),
% 1.65/2.10 skol137 [672, 3] (w:1, o:442, a:1, s:1, b:1),
% 1.65/2.10 skol138 [673, 3] (w:1, o:443, a:1, s:1, b:1),
% 1.65/2.10 skol139 [674, 2] (w:1, o:361, a:1, s:1, b:1),
% 1.65/2.10 skol140 [675, 3] (w:1, o:444, a:1, s:1, b:1),
% 1.65/2.10 skol141 [676, 3] (w:1, o:445, a:1, s:1, b:1),
% 1.65/2.10 skol142 [677, 2] (w:1, o:363, a:1, s:1, b:1),
% 1.65/2.10 skol143 [678, 3] (w:1, o:446, a:1, s:1, b:1),
% 1.65/2.10 skol144 [679, 3] (w:1, o:447, a:1, s:1, b:1),
% 1.65/2.10 skol145 [680, 2] (w:1, o:364, a:1, s:1, b:1),
% 1.65/2.10 skol146 [681, 3] (w:1, o:448, a:1, s:1, b:1),
% 1.65/2.10 skol147 [682, 3] (w:1, o:449, a:1, s:1, b:1),
% 1.65/2.10 skol148 [683, 2] (w:1, o:365, a:1, s:1, b:1),
% 1.65/2.10 skol149 [684, 3] (w:1, o:450, a:1, s:1, b:1),
% 1.65/2.10 skol150 [685, 3] (w:1, o:395, a:1, s:1, b:1),
% 1.65/2.10 skol151 [686, 2] (w:1, o:367, a:1, s:1, b:1),
% 1.65/2.10 skol152 [687, 3] (w:1, o:396, a:1, s:1, b:1),
% 1.65/2.10 skol153 [688, 3] (w:1, o:397, a:1, s:1, b:1),
% 1.65/2.10 skol154 [689, 2] (w:1, o:368, a:1, s:1, b:1),
% 1.65/2.10 skol155 [690, 3] (w:1, o:398, a:1, s:1, b:1),
% 1.65/2.10 skol156 [691, 3] (w:1, o:399, a:1, s:1, b:1),
% 1.65/2.10 skol157 [692, 2] (w:1, o:369, a:1, s:1, b:1),
% 1.65/2.10 skol158 [693, 3] (w:1, o:400, a:1, s:1, b:1),
% 1.65/2.10 skol159 [694, 3] (w:1, o:401, a:1, s:1, b:1),
% 1.65/2.10 skol160 [695, 2] (w:1, o:370, a:1, s:1, b:1),
% 1.65/2.10 skol161 [696, 3] (w:1, o:403, a:1, s:1, b:1),
% 1.65/2.10 skol162 [697, 3] (w:1, o:404, a:1, s:1, b:1),
% 1.65/2.10 skol163 [698, 2] (w:1, o:371, a:1, s:1, b:1),
% 1.65/2.10 skol164 [699, 3] (w:1, o:405, a:1, s:1, b:1),
% 1.65/2.10 skol165 [700, 3] (w:1, o:406, a:1, s:1, b:1),
% 1.65/2.10 skol166 [701, 0] (w:1, o:137, a:1, s:1, b:1),
% 1.65/2.10 skol167 [702, 3] (w:1, o:407, a:1, s:1, b:1),
% 1.65/2.10 skol168 [703, 2] (w:1, o:372, a:1, s:1, b:1),
% 1.65/2.10 skol169 [704, 2] (w:1, o:373, a:1, s:1, b:1),
% 1.65/2.10 skol170 [705, 2] (w:1, o:374, a:1, s:1, b:1),
% 1.65/2.10 skol171 [706, 2] (w:1, o:375, a:1, s:1, b:1),
% 1.65/2.10 skol172 [707, 2] (w:1, o:376, a:1, s:1, b:1),
% 1.65/2.10 skol173 [708, 2] (w:1, o:377, a:1, s:1, b:1),
% 1.65/2.10 skol174 [709, 3] (w:1, o:409, a:1, s:1, b:1),
% 1.65/2.10 skol175 [710, 3] (w:1, o:410, a:1, s:1, b:1),
% 1.65/2.10 skol176 [711, 3] (w:1, o:411, a:1, s:1, b:1),
% 1.65/2.10 skol177 [712, 3] (w:1, o:412, a:1, s:1, b:1),
% 1.65/2.10 skol178 [713, 3] (w:1, o:413, a:1, s:1, b:1),
% 14.60/15.11 skol179 [714, 3] (w:1, o:414, a:1, s:1, b:1),
% 14.60/15.11 skol180 [715, 3] (w:1, o:416, a:1, s:1, b:1),
% 14.60/15.11 skol181 [716, 3] (w:1, o:417, a:1, s:1, b:1),
% 14.60/15.11 skol182 [717, 3] (w:1, o:418, a:1, s:1, b:1),
% 14.60/15.11 skol183 [718, 3] (w:1, o:419, a:1, s:1, b:1),
% 14.60/15.11 skol184 [719, 3] (w:1, o:420, a:1, s:1, b:1),
% 14.60/15.11 skol185 [720, 3] (w:1, o:421, a:1, s:1, b:1),
% 14.60/15.11 skol186 [721, 3] (w:1, o:422, a:1, s:1, b:1),
% 14.60/15.11 skol187 [722, 3] (w:1, o:423, a:1, s:1, b:1),
% 14.60/15.11 skol188 [723, 3] (w:1, o:424, a:1, s:1, b:1),
% 14.60/15.11 skol189 [724, 3] (w:1, o:425, a:1, s:1, b:1),
% 14.60/15.11 skol190 [725, 3] (w:1, o:451, a:1, s:1, b:1),
% 14.60/15.11 skol191 [726, 3] (w:1, o:452, a:1, s:1, b:1),
% 14.60/15.11 skol192 [727, 3] (w:1, o:453, a:1, s:1, b:1),
% 14.60/15.11 skol193 [728, 3] (w:1, o:454, a:1, s:1, b:1),
% 14.60/15.11 skol194 [729, 3] (w:1, o:455, a:1, s:1, b:1),
% 14.60/15.11 skol195 [730, 3] (w:1, o:456, a:1, s:1, b:1),
% 14.60/15.11 skol196 [731, 3] (w:1, o:457, a:1, s:1, b:1),
% 14.60/15.11 skol197 [732, 3] (w:1, o:458, a:1, s:1, b:1),
% 14.60/15.11 skol198 [733, 3] (w:1, o:459, a:1, s:1, b:1),
% 14.60/15.11 skol199 [734, 3] (w:1, o:460, a:1, s:1, b:1),
% 14.60/15.11 skol200 [735, 3] (w:1, o:462, a:1, s:1, b:1),
% 14.60/15.11 skol201 [736, 3] (w:1, o:463, a:1, s:1, b:1),
% 14.60/15.11 skol202 [737, 3] (w:1, o:464, a:1, s:1, b:1),
% 14.60/15.11 skol203 [738, 3] (w:1, o:465, a:1, s:1, b:1),
% 14.60/15.11 skol204 [739, 3] (w:1, o:466, a:1, s:1, b:1),
% 14.60/15.11 skol205 [740, 3] (w:1, o:467, a:1, s:1, b:1),
% 14.60/15.11 skol206 [741, 3] (w:1, o:468, a:1, s:1, b:1),
% 14.60/15.11 skol207 [742, 3] (w:1, o:469, a:1, s:1, b:1),
% 14.60/15.11 skol208 [743, 3] (w:1, o:470, a:1, s:1, b:1),
% 14.60/15.11 skol209 [744, 3] (w:1, o:471, a:1, s:1, b:1),
% 14.60/15.11 skol210 [745, 1] (w:1, o:223, a:1, s:1, b:1),
% 14.60/15.11 skol211 [746, 1] (w:1, o:224, a:1, s:1, b:1),
% 14.60/15.11 skol212 [747, 1] (w:1, o:225, a:1, s:1, b:1),
% 14.60/15.11 skol213 [748, 1] (w:1, o:226, a:1, s:1, b:1),
% 14.60/15.11 skol214 [749, 1] (w:1, o:227, a:1, s:1, b:1),
% 14.60/15.11 skol215 [750, 1] (w:1, o:228, a:1, s:1, b:1),
% 14.60/15.11 skol216 [751, 1] (w:1, o:229, a:1, s:1, b:1),
% 14.60/15.11 skol217 [752, 1] (w:1, o:230, a:1, s:1, b:1),
% 14.60/15.11 skol218 [753, 1] (w:1, o:231, a:1, s:1, b:1),
% 14.60/15.11 skol219 [754, 1] (w:1, o:232, a:1, s:1, b:1),
% 14.60/15.11 skol220 [755, 1] (w:1, o:233, a:1, s:1, b:1),
% 14.60/15.11 skol221 [756, 2] (w:1, o:379, a:1, s:1, b:1),
% 14.60/15.11 skol222 [757, 2] (w:1, o:380, a:1, s:1, b:1),
% 14.60/15.11 skol223 [758, 2] (w:1, o:381, a:1, s:1, b:1),
% 14.60/15.11 skol224 [759, 1] (w:1, o:234, a:1, s:1, b:1),
% 14.60/15.11 skol225 [760, 1] (w:1, o:235, a:1, s:1, b:1),
% 14.60/15.11 skol226 [761, 1] (w:1, o:236, a:1, s:1, b:1),
% 14.60/15.11 skol227 [762, 0] (w:1, o:138, a:1, s:1, b:1),
% 14.60/15.11 skol228 [763, 3] (w:1, o:474, a:1, s:1, b:1),
% 14.60/15.11 skol229 [764, 3] (w:1, o:475, a:1, s:1, b:1),
% 14.60/15.11 skol230 [765, 0] (w:1, o:139, a:1, s:1, b:1),
% 14.60/15.11 skol231 [766, 0] (w:1, o:140, a:1, s:1, b:1),
% 14.60/15.11 skol232 [767, 0] (w:1, o:141, a:1, s:1, b:1),
% 14.60/15.11 skol233 [768, 0] (w:1, o:142, a:1, s:1, b:1).
% 14.60/15.11
% 14.60/15.11
% 14.60/15.11 Starting Search:
% 14.60/15.11
% 14.60/15.11 *** allocated 75937 integers for clauses
% 14.60/15.11 *** allocated 113905 integers for clauses
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11 *** allocated 170857 integers for clauses
% 14.60/15.11
% 14.60/15.11 Intermediate Status:
% 14.60/15.11 Generated: 3202
% 14.60/15.11 Kept: 2051
% 14.60/15.11 Inuse: 156
% 14.60/15.11 Deleted: 0
% 14.60/15.11 Deletedinuse: 0
% 14.60/15.11
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11 *** allocated 256285 integers for clauses
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11
% 14.60/15.11 Intermediate Status:
% 14.60/15.11 Generated: 7975
% 14.60/15.11 Kept: 4055
% 14.60/15.11 Inuse: 431
% 14.60/15.11 Deleted: 0
% 14.60/15.11 Deletedinuse: 0
% 14.60/15.11
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11 *** allocated 384427 integers for clauses
% 14.60/15.11 *** allocated 113905 integers for termspace/termends
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11
% 14.60/15.11 Intermediate Status:
% 14.60/15.11 Generated: 12795
% 14.60/15.11 Kept: 6086
% 14.60/15.11 Inuse: 766
% 14.60/15.11 Deleted: 0
% 14.60/15.11 Deletedinuse: 0
% 14.60/15.11
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11 *** allocated 576640 integers for clauses
% 14.60/15.11
% 14.60/15.11 Intermediate Status:
% 14.60/15.11 Generated: 18263
% 14.60/15.11 Kept: 8105
% 14.60/15.11 Inuse: 1000
% 14.60/15.11 Deleted: 6
% 14.60/15.11 Deletedinuse: 3
% 14.60/15.11
% 14.60/15.11 *** allocated 170857 integers for termspace/termends
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11 Resimplifying inuse:
% 14.60/15.11 Done
% 14.60/15.11
% 14.60/15.11
% 14.60/15.11 Intermediate Status:
% 14.60/15.11 Generated: 22834
% 14.60/15.11 Kept: 10190
% 14.60/15.11 Inuse: 1098
% 35.84/36.31 Deleted: 6
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 *** allocated 864960 integers for clauses
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 27266
% 35.84/36.31 Kept: 12208
% 35.84/36.31 Inuse: 1243
% 35.84/36.31 Deleted: 6
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 *** allocated 256285 integers for termspace/termends
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 32084
% 35.84/36.31 Kept: 14221
% 35.84/36.31 Inuse: 1440
% 35.84/36.31 Deleted: 17
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 36561
% 35.84/36.31 Kept: 16338
% 35.84/36.31 Inuse: 1525
% 35.84/36.31 Deleted: 19
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 41406
% 35.84/36.31 Kept: 18590
% 35.84/36.31 Inuse: 1628
% 35.84/36.31 Deleted: 21
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 *** allocated 1297440 integers for clauses
% 35.84/36.31 *** allocated 384427 integers for termspace/termends
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying clauses:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 45997
% 35.84/36.31 Kept: 20820
% 35.84/36.31 Inuse: 1718
% 35.84/36.31 Deleted: 3246
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 51194
% 35.84/36.31 Kept: 22881
% 35.84/36.31 Inuse: 1914
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 56354
% 35.84/36.31 Kept: 25334
% 35.84/36.31 Inuse: 1979
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 60911
% 35.84/36.31 Kept: 27387
% 35.84/36.31 Inuse: 2039
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 *** allocated 576640 integers for termspace/termends
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 65856
% 35.84/36.31 Kept: 29388
% 35.84/36.31 Inuse: 2122
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 *** allocated 1946160 integers for clauses
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 70180
% 35.84/36.31 Kept: 31397
% 35.84/36.31 Inuse: 2159
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 75062
% 35.84/36.31 Kept: 33683
% 35.84/36.31 Inuse: 2219
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 81125
% 35.84/36.31 Kept: 36275
% 35.84/36.31 Inuse: 2334
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 86182
% 35.84/36.31 Kept: 38280
% 35.84/36.31 Inuse: 2437
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 91748
% 35.84/36.31 Kept: 40716
% 35.84/36.31 Inuse: 2504
% 35.84/36.31 Deleted: 3255
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying clauses:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 *** allocated 864960 integers for termspace/termends
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 96484
% 35.84/36.31 Kept: 42721
% 35.84/36.31 Inuse: 2612
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 101880
% 35.84/36.31 Kept: 45178
% 35.84/36.31 Inuse: 2669
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 *** allocated 2919240 integers for clauses
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 106902
% 35.84/36.31 Kept: 47185
% 35.84/36.31 Inuse: 2769
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 111247
% 35.84/36.31 Kept: 49870
% 35.84/36.31 Inuse: 2869
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 117087
% 35.84/36.31 Kept: 51895
% 35.84/36.31 Inuse: 3018
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 120981
% 35.84/36.31 Kept: 53940
% 35.84/36.31 Inuse: 3054
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 126468
% 35.84/36.31 Kept: 55942
% 35.84/36.31 Inuse: 3201
% 35.84/36.31 Deleted: 8441
% 35.84/36.31 Deletedinuse: 3
% 35.84/36.31
% 35.84/36.31 Resimplifying inuse:
% 35.84/36.31 Done
% 35.84/36.31
% 35.84/36.31
% 35.84/36.31 Intermediate Status:
% 35.84/36.31 Generated: 129726
% 35.84/36.31 Kept: 57971
% 73.38/73.86 Inuse: 3254
% 73.38/73.86 Deleted: 8441
% 73.38/73.86 Deletedinuse: 3
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 134550
% 73.38/73.86 Kept: 60025
% 73.38/73.86 Inuse: 3364
% 73.38/73.86 Deleted: 8441
% 73.38/73.86 Deletedinuse: 3
% 73.38/73.86
% 73.38/73.86 *** allocated 1297440 integers for termspace/termends
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying clauses:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 141774
% 73.38/73.86 Kept: 62734
% 73.38/73.86 Inuse: 3444
% 73.38/73.86 Deleted: 12825
% 73.38/73.86 Deletedinuse: 6
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 146886
% 73.38/73.86 Kept: 64815
% 73.38/73.86 Inuse: 3524
% 73.38/73.86 Deleted: 13277
% 73.38/73.86 Deletedinuse: 458
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 151905
% 73.38/73.86 Kept: 66866
% 73.38/73.86 Inuse: 3614
% 73.38/73.86 Deleted: 13280
% 73.38/73.86 Deletedinuse: 461
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 *** allocated 4378860 integers for clauses
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 156146
% 73.38/73.86 Kept: 68974
% 73.38/73.86 Inuse: 3724
% 73.38/73.86 Deleted: 13280
% 73.38/73.86 Deletedinuse: 461
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 160294
% 73.38/73.86 Kept: 71003
% 73.38/73.86 Inuse: 3838
% 73.38/73.86 Deleted: 13286
% 73.38/73.86 Deletedinuse: 461
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 165015
% 73.38/73.86 Kept: 73098
% 73.38/73.86 Inuse: 3888
% 73.38/73.86 Deleted: 13286
% 73.38/73.86 Deletedinuse: 461
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 169438
% 73.38/73.86 Kept: 76057
% 73.38/73.86 Inuse: 3908
% 73.38/73.86 Deleted: 13286
% 73.38/73.86 Deletedinuse: 461
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 175828
% 73.38/73.86 Kept: 78282
% 73.38/73.86 Inuse: 3977
% 73.38/73.86 Deleted: 13301
% 73.38/73.86 Deletedinuse: 465
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 184180
% 73.38/73.86 Kept: 81552
% 73.38/73.86 Inuse: 4004
% 73.38/73.86 Deleted: 13333
% 73.38/73.86 Deletedinuse: 469
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying clauses:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 191356
% 73.38/73.86 Kept: 84120
% 73.38/73.86 Inuse: 4070
% 73.38/73.86 Deleted: 27503
% 73.38/73.86 Deletedinuse: 469
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 198484
% 73.38/73.86 Kept: 86936
% 73.38/73.86 Inuse: 4160
% 73.38/73.86 Deleted: 27503
% 73.38/73.86 Deletedinuse: 469
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 203574
% 73.38/73.86 Kept: 89084
% 73.38/73.86 Inuse: 4210
% 73.38/73.86 Deleted: 27505
% 73.38/73.86 Deletedinuse: 471
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 *** allocated 1946160 integers for termspace/termends
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 209432
% 73.38/73.86 Kept: 91629
% 73.38/73.86 Inuse: 4255
% 73.38/73.86 Deleted: 27505
% 73.38/73.86 Deletedinuse: 471
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 216060
% 73.38/73.86 Kept: 94459
% 73.38/73.86 Inuse: 4305
% 73.38/73.86 Deleted: 27505
% 73.38/73.86 Deletedinuse: 471
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 223851
% 73.38/73.86 Kept: 97264
% 73.38/73.86 Inuse: 4385
% 73.38/73.86 Deleted: 27505
% 73.38/73.86 Deletedinuse: 471
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 228852
% 73.38/73.86 Kept: 99367
% 73.38/73.86 Inuse: 4480
% 73.38/73.86 Deleted: 27529
% 73.38/73.86 Deletedinuse: 495
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 *** allocated 6568290 integers for clauses
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 235509
% 73.38/73.86 Kept: 101885
% 73.38/73.86 Inuse: 4535
% 73.38/73.86 Deleted: 27529
% 73.38/73.86 Deletedinuse: 495
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying clauses:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 240797
% 73.38/73.86 Kept: 103887
% 73.38/73.86 Inuse: 4612
% 73.38/73.86 Deleted: 34213
% 73.38/73.86 Deletedinuse: 511
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 246501
% 73.38/73.86 Kept: 105953
% 73.38/73.86 Inuse: 4650
% 73.38/73.86 Deleted: 34213
% 73.38/73.86 Deletedinuse: 511
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 251708
% 73.38/73.86 Kept: 108005
% 73.38/73.86 Inuse: 4871
% 73.38/73.86 Deleted: 34227
% 73.38/73.86 Deletedinuse: 511
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 73.38/73.86 Done
% 73.38/73.86
% 73.38/73.86
% 73.38/73.86 Intermediate Status:
% 73.38/73.86 Generated: 256419
% 73.38/73.86 Kept: 110069
% 73.38/73.86 Inuse: 5055
% 73.38/73.86 Deleted: 34228
% 73.38/73.86 Deletedinuse: 512
% 73.38/73.86
% 73.38/73.86 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89
% 170.41/170.89 Intermediate Status:
% 170.41/170.89 Generated: 261944
% 170.41/170.89 Kept: 112069
% 170.41/170.89 Inuse: 5124
% 170.41/170.89 Deleted: 34232
% 170.41/170.89 Deletedinuse: 516
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89
% 170.41/170.89 Intermediate Status:
% 170.41/170.89 Generated: 270717
% 170.41/170.89 Kept: 114075
% 170.41/170.89 Inuse: 5162
% 170.41/170.89 Deleted: 34232
% 170.41/170.89 Deletedinuse: 516
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89
% 170.41/170.89 Intermediate Status:
% 170.41/170.89 Generated: 283908
% 170.41/170.89 Kept: 116085
% 170.41/170.89 Inuse: 5648
% 170.41/170.89 Deleted: 34232
% 170.41/170.89 Deletedinuse: 516
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89
% 170.41/170.89 Intermediate Status:
% 170.41/170.89 Generated: 306314
% 170.41/170.89 Kept: 118200
% 170.41/170.89 Inuse: 6031
% 170.41/170.89 Deleted: 34232
% 170.41/170.89 Deletedinuse: 516
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89
% 170.41/170.89 Intermediate Status:
% 170.41/170.89 Generated: 321608
% 170.41/170.89 Kept: 120203
% 170.41/170.89 Inuse: 6128
% 170.41/170.89 Deleted: 34233
% 170.41/170.89 Deletedinuse: 517
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89 Resimplifying inuse:
% 170.41/170.89 Done
% 170.41/170.89
% 170.41/170.89
% 170.41/170.89 Intermediate Status:
% 170.41/170.89 Generated: 337002
% 170.41/170.89 Kept: 122337
% 170.41/170.89 Inuse: 6226
% 170.41/170.89 Deleted: 34233
% 170.41/170.89 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying clauses:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 366789
% 170.41/170.90 Kept: 124382
% 170.41/170.90 Inuse: 6301
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 382410
% 170.41/170.90 Kept: 126410
% 170.41/170.90 Inuse: 6446
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 405005
% 170.41/170.90 Kept: 128506
% 170.41/170.90 Inuse: 6626
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 420099
% 170.41/170.90 Kept: 130512
% 170.41/170.90 Inuse: 6706
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 434224
% 170.41/170.90 Kept: 132512
% 170.41/170.90 Inuse: 6796
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 451808
% 170.41/170.90 Kept: 134729
% 170.41/170.90 Inuse: 6871
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 464864
% 170.41/170.90 Kept: 136941
% 170.41/170.90 Inuse: 6896
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 *** allocated 2919240 integers for termspace/termends
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 479322
% 170.41/170.90 Kept: 139010
% 170.41/170.90 Inuse: 6906
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 497559
% 170.41/170.90 Kept: 141839
% 170.41/170.90 Inuse: 6916
% 170.41/170.90 Deleted: 36768
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying clauses:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 510967
% 170.41/170.90 Kept: 143949
% 170.41/170.90 Inuse: 6996
% 170.41/170.90 Deleted: 36957
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 536903
% 170.41/170.90 Kept: 146019
% 170.41/170.90 Inuse: 7071
% 170.41/170.90 Deleted: 36957
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 556489
% 170.41/170.90 Kept: 148042
% 170.41/170.90 Inuse: 7091
% 170.41/170.90 Deleted: 36957
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 566298
% 170.41/170.90 Kept: 150117
% 170.41/170.90 Inuse: 7130
% 170.41/170.90 Deleted: 36957
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 578395
% 170.41/170.90 Kept: 152174
% 170.41/170.90 Inuse: 7181
% 170.41/170.90 Deleted: 36957
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 592498
% 170.41/170.90 Kept: 154174
% 170.41/170.90 Inuse: 7250
% 170.41/170.90 Deleted: 36957
% 170.41/170.90 Deletedinuse: 517
% 170.41/170.90
% 170.41/170.90 *** allocated 9852435 integers for clauses
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 610720
% 170.41/170.90 Kept: 156182
% 170.41/170.90 Inuse: 7335
% 170.41/170.90 Deleted: 36981
% 170.41/170.90 Deletedinuse: 519
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90 Resimplifying inuse:
% 170.41/170.90 Done
% 170.41/170.90
% 170.41/170.90
% 170.41/170.90 Intermediate Status:
% 170.41/170.90 Generated: 631067
% 170.41/170.90 Kept: 158186
% 170.41/170.90 Inuse:Alarm clock
% 299.60/300.08 Bliksem ended
%------------------------------------------------------------------------------