%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYO663-1 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 21 14:29:13 EDT 2022
% Result : Unsatisfiable 4.74s 5.11s
% Output : Refutation 4.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYO663-1 : TPTP v8.1.0. Released v7.3.0.
% 0.11/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Sat Jul 9 01:52:01 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.79/1.19 *** allocated 10000 integers for termspace/termends
% 0.79/1.19 *** allocated 10000 integers for clauses
% 0.79/1.19 *** allocated 10000 integers for justifications
% 0.79/1.19 Bliksem 1.12
% 0.79/1.19
% 0.79/1.19
% 0.79/1.19 Automatic Strategy Selection
% 0.79/1.19
% 0.79/1.19 Clauses:
% 0.79/1.19 [
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc(
% 0.79/1.19 suc( Z ) ) ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y
% 0.79/1.19 ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) )
% 0.79/1.19 ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( T ) ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f(
% 0.79/1.19 T ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 0.79/1.19 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z
% 0.79/1.19 ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ),
% 0.79/1.19 ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f(
% 0.79/1.19 suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z
% 0.79/1.19 ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 0.79/1.19 'E'( f( Y ), f( suc( Y ) ) ), 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( 'LE'( f( X ), s( '0' ) ) ), 'E'( '0', f( X ) ), 'LE'( f( X ), '0' )
% 0.79/1.19 ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 0.79/1.19 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 0.79/1.19 Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( f( Y ), f(
% 0.79/1.19 suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc(
% 0.79/1.19 T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s(
% 0.79/1.19 '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( f( T ), f(
% 0.79/1.19 suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( suc( Z ) ) ) ) ) ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 0.79/1.19 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 0.79/1.19 Z ), suc( X ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' )
% 0.79/1.19 , f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X )
% 0.79/1.19 , f( suc( X ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' )
% 0.79/1.19 , f( suc( Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ) ],
% 0.79/1.19 [ ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( X ) )
% 0.79/1.19 ), iLEQ( suc( X ), suc( X ) ) ],
% 0.79/1.19 [ ~( 'LE'( f( suc( suc( X ) ) ), s( s( '0' ) ) ) ), 'E'( s( '0' ), f(
% 0.79/1.19 suc( suc( X ) ) ) ), 'LE'( f( X ), s( '0' ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( X ) ) ) ), 'E'( f( X ),
% 0.79/1.19 f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 0.79/1.19 T ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) )
% 0.79/1.19 ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ),
% 0.79/1.19 ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( Z ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f(
% 0.79/1.19 Z ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 0.79/1.19 'E'( f( Y ), f( suc( Y ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) )
% 0.79/1.19 ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ),
% 0.79/1.19 ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f(
% 0.79/1.19 suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z
% 0.79/1.19 ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 0.79/1.19 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ 'LE'( f( X ), s( s( '0' ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( X ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( iLEQ( suc( Z ), suc(
% 0.79/1.19 T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f(
% 0.79/1.19 suc( T ) ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( T ) )
% 0.79/1.19 ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f(
% 0.79/1.19 Y ), f( suc( Y ) ) ), 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( X ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( iLEQ( suc( Z )
% 0.79/1.19 , suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y
% 0.79/1.19 ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( f( Z )
% 0.79/1.19 , f( suc( Z ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X ), f( suc( X )
% 0.79/1.19 ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ) ]
% 0.79/1.19 ,
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 0.79/1.19 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 0.79/1.19 Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ),
% 0.79/1.19 suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( f( T ), f( suc(
% 0.79/1.19 T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 suc( Z ) ) ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ],
% 0.79/1.19 [ ~( 'LE'( f( suc( X ) ), s( '0' ) ) ), 'E'( '0', f( suc( X ) ) ), 'LE'(
% 0.79/1.19 f( X ), '0' ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f(
% 0.79/1.19 suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y )
% 0.79/1.19 ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ),
% 0.79/1.19 ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( Y ), f( suc( Y ) ) )
% 0.79/1.19 , 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( 'E'( '0', f( suc( suc( T ) ) ) ) ), ~( iLEQ( suc( T ), suc(
% 0.79/1.19 Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) )
% 0.79/1.19 , ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~(
% 0.79/1.19 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0'
% 0.79/1.19 , f( suc( Z ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z
% 0.79/1.19 ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f( suc( X ) ) ) ]
% 0.79/1.19 ,
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T
% 0.79/1.19 ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X
% 0.79/1.19 ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 suc( Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( X ), f( suc( X )
% 0.79/1.19 ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 0.79/1.19 f( X ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) )
% 0.79/1.19 ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~(
% 0.79/1.19 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T )
% 0.79/1.19 ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'(
% 0.79/1.19 f( Y ), f( suc( Y ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f(
% 0.79/1.19 suc( T ) ) ) ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) )
% 0.79/1.19 , ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Z )
% 0.79/1.19 ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'(
% 0.79/1.19 f( Y ), f( suc( Y ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( iLEQ( suc( Z ),
% 0.79/1.19 suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y )
% 0.79/1.19 ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( Y ), f( suc( Y ) ) )
% 0.79/1.19 , 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Y ), f( suc(
% 0.79/1.19 Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T )
% 0.79/1.19 , suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( Y
% 0.79/1.19 ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'(
% 0.79/1.19 f( X ), f( suc( X ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( X ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y
% 0.79/1.19 ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) )
% 0.79/1.19 ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( Z ), f( suc( Z ) ) )
% 0.79/1.19 , 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f(
% 0.79/1.19 suc( Z ) ) ) ), ~( 'E'( '0', f( suc( suc( T ) ) ) ) ), ~( iLEQ( suc( T )
% 0.79/1.19 , suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y
% 0.79/1.19 ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( f(
% 0.79/1.19 T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( Y ), f( suc( Y ) ) )
% 0.79/1.19 ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z
% 0.79/1.19 ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) )
% 0.79/1.19 , 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X )
% 0.79/1.19 , f( suc( X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ],
% 0.79/1.19 [ ~( 'LE'( f( z ), '0' ) ) ],
% 0.79/1.19 [ ~( 'LE'( f( suc( suc( X ) ) ), s( '0' ) ) ), 'E'( '0', f( suc( suc( X
% 0.79/1.19 ) ) ) ), 'LE'( f( X ), '0' ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc(
% 0.79/1.19 suc( Z ) ) ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y
% 0.79/1.19 ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( f( Z )
% 0.79/1.19 , f( suc( Z ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X ), f( suc( X )
% 0.79/1.19 ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( Y ), f( suc( Y ) ) ),
% 0.79/1.19 'E'( f( T ), f( suc( T ) ) ) ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 0.79/1.19 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 0.79/1.19 Z ), suc( X ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' )
% 0.79/1.19 , f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 X ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y )
% 0.79/1.19 ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'(
% 0.79/1.19 f( Y ), f( suc( Y ) ) ) ],
% 0.79/1.19 [ ~( 'LE'( f( X ), s( s( '0' ) ) ) ), 'E'( s( '0' ), f( X ) ), 'LE'( f(
% 0.79/1.19 X ), s( '0' ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( suc(
% 0.79/1.19 suc( T ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y
% 0.79/1.19 ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) )
% 0.79/1.19 ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( f(
% 0.79/1.19 T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ) ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 0.79/1.19 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 0.79/1.19 Z ), suc( X ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' )
% 0.79/1.19 , f( X ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ) ]
% 0.79/1.19 ,
% 0.79/1.19 [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), 'E'(
% 0.79/1.19 f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( suc( X ) ) ) )
% 0.79/1.19 , ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( '0', f( X ) ) ), iLEQ( suc(
% 0.79/1.19 X ), suc( X ) ) ],
% 0.79/1.19 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X ) ) ) ) )
% 0.79/1.19 , ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ),
% 0.79/1.19 suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y )
% 0.79/1.19 ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ),
% 0.79/1.19 ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'(
% 0.79/1.19 '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X ), f( suc(
% 0.79/1.19 X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( T ), f( suc( T ) ) )
% 0.79/1.19 ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z
% 0.79/1.19 ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 0.79/1.19 X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y )
% 0.79/1.19 ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'(
% 0.79/1.19 f( Y ), f( suc( Y ) ) ) ],
% 0.79/1.19 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 0.79/1.19 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 0.79/1.19 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Y ), f( suc(
% 0.79/1.19 Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 0.79/1.19 Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T )
% 0.79/1.19 , suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s(
% 3.97/4.39 '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( Y ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) )
% 3.97/4.39 ) ],
% 3.97/4.39 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 3.97/4.39 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 3.97/4.39 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc(
% 3.97/4.39 Z ) ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T
% 3.97/4.39 ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 3.97/4.39 suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f(
% 3.97/4.39 suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( suc( Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ) ],
% 3.97/4.39 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 3.97/4.39 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0'
% 3.97/4.39 ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc(
% 3.97/4.39 Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 3.97/4.39 Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 3.97/4.39 X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) )
% 3.97/4.39 ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 3.97/4.39 Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ]
% 3.97/4.39 ,
% 3.97/4.39 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 3.97/4.39 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 3.97/4.39 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 3.97/4.39 Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ),
% 3.97/4.39 suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( T ), f( suc( T ) )
% 3.97/4.39 ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 3.97/4.39 Z ) ) ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ]
% 3.97/4.39 ,
% 3.97/4.39 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 3.97/4.39 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 3.97/4.39 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 3.97/4.39 Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( f( Y ), f(
% 3.97/4.39 suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc(
% 3.97/4.39 T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( T ), f( suc(
% 3.97/4.39 T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 3.97/4.39 suc( Z ) ) ) ) ), 'E'( f( X ), f( suc( X ) ) ) ],
% 3.97/4.39 [ ~( 'LE'( f( suc( X ) ), s( s( '0' ) ) ) ), 'E'( s( '0' ), f( suc( X )
% 3.97/4.39 ) ), 'LE'( f( X ), s( '0' ) ) ],
% 3.97/4.39 [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'(
% 3.97/4.39 s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ),
% 3.97/4.39 ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc(
% 3.97/4.39 Z ), suc( X ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' )
% 3.97/4.39 , f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f(
% 3.97/4.39 suc( X ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f(
% 3.97/4.39 suc( Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( Y ), f( suc( Y ) )
% 3.97/4.39 ) ],
% 3.97/4.39 [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0',
% 3.97/4.39 f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( iLEQ( suc( Z ), suc(
% 3.97/4.39 T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) )
% 3.97/4.39 , ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~(
% 3.97/4.39 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T )
% 3.97/4.39 ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'(
% 3.97/4.39 f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ) ]
% 3.97/4.39 ] .
% 3.97/4.39
% 3.97/4.39
% 3.97/4.39 percentage equality = 0.000000, percentage horn = 0.318182
% 3.97/4.39 This a non-horn, non-equality problem
% 3.97/4.39
% 3.97/4.39
% 3.97/4.39 Options Used:
% 3.97/4.39
% 3.97/4.39 useres = 1
% 4.74/5.11 useparamod = 0
% 4.74/5.11 useeqrefl = 0
% 4.74/5.11 useeqfact = 0
% 4.74/5.11 usefactor = 1
% 4.74/5.11 usesimpsplitting = 0
% 4.74/5.11 usesimpdemod = 0
% 4.74/5.11 usesimpres = 3
% 4.74/5.11
% 4.74/5.11 resimpinuse = 1000
% 4.74/5.11 resimpclauses = 20000
% 4.74/5.11 substype = standard
% 4.74/5.11 backwardsubs = 1
% 4.74/5.11 selectoldest = 5
% 4.74/5.11
% 4.74/5.11 litorderings [0] = split
% 4.74/5.11 litorderings [1] = liftord
% 4.74/5.11
% 4.74/5.11 termordering = none
% 4.74/5.11
% 4.74/5.11 litapriori = 1
% 4.74/5.11 termapriori = 0
% 4.74/5.11 litaposteriori = 0
% 4.74/5.11 termaposteriori = 0
% 4.74/5.11 demodaposteriori = 0
% 4.74/5.11 ordereqreflfact = 0
% 4.74/5.11
% 4.74/5.11 litselect = none
% 4.74/5.11
% 4.74/5.11 maxweight = 15
% 4.74/5.11 maxdepth = 30000
% 4.74/5.11 maxlength = 115
% 4.74/5.11 maxnrvars = 195
% 4.74/5.11 excuselevel = 1
% 4.74/5.11 increasemaxweight = 1
% 4.74/5.11
% 4.74/5.11 maxselected = 10000000
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11
% 4.74/5.11 showgenerated = 0
% 4.74/5.11 showkept = 0
% 4.74/5.11 showselected = 0
% 4.74/5.11 showdeleted = 0
% 4.74/5.11 showresimp = 1
% 4.74/5.11 showstatus = 2000
% 4.74/5.11
% 4.74/5.11 prologoutput = 1
% 4.74/5.11 nrgoals = 5000000
% 4.74/5.11 totalproof = 1
% 4.74/5.11
% 4.74/5.11 Symbols occurring in the translation:
% 4.74/5.11
% 4.74/5.11 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 4.74/5.11 . [1, 2] (w:1, o:30, a:1, s:1, b:0),
% 4.74/5.11 ! [4, 1] (w:0, o:22, a:1, s:1, b:0),
% 4.74/5.11 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.74/5.11 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 4.74/5.11 '0' [39, 0] (w:1, o:6, a:1, s:1, b:0),
% 4.74/5.11 suc [41, 1] (w:1, o:27, a:1, s:1, b:0),
% 4.74/5.11 f [42, 1] (w:1, o:28, a:1, s:1, b:0),
% 4.74/5.11 'E' [43, 2] (w:1, o:55, a:1, s:1, b:0),
% 4.74/5.11 iLEQ [47, 2] (w:1, o:56, a:1, s:1, b:0),
% 4.74/5.11 s [49, 1] (w:1, o:29, a:1, s:1, b:0),
% 4.74/5.11 'LE' [50, 2] (w:1, o:57, a:1, s:1, b:0),
% 4.74/5.11 z [57, 0] (w:1, o:21, a:1, s:1, b:0).
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 15
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 20267
% 4.74/5.11 Kept: 700
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 16
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 16
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 20003
% 4.74/5.11 Kept: 693
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 17
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 17
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 20005
% 4.74/5.11 Kept: 697
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 18
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 18
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 20006
% 4.74/5.11 Kept: 699
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 19
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 19
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 20019
% 4.74/5.11 Kept: 701
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 20
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 20
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19679
% 4.74/5.11 Kept: 693
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 21
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 21
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19679
% 4.74/5.11 Kept: 693
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 22
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 22
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19471
% 4.74/5.11 Kept: 699
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 23
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 23
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19471
% 4.74/5.11 Kept: 700
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 24
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 24
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19471
% 4.74/5.11 Kept: 700
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 25
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 25
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19471
% 4.74/5.11 Kept: 700
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 26
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 26
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19449
% 4.74/5.11 Kept: 704
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 27
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 27
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19449
% 4.74/5.11 Kept: 704
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 28
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Resimplifying inuse:
% 4.74/5.11 Done
% 4.74/5.11
% 4.74/5.11 Failed to find proof!
% 4.74/5.11 maxweight = 28
% 4.74/5.11 maxnrclauses = 10000000
% 4.74/5.11 Generated: 19449
% 4.74/5.11 Kept: 704
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 The strategy used was not complete!
% 4.74/5.11
% 4.74/5.11 Increased maxweight to 29
% 4.74/5.11
% 4.74/5.11 Starting Search:
% 4.74/5.11
% 4.74/5.11
% 4.74/5.11 Bliksems!, er is een bewijs:
% 4.74/5.11 % SZS status Unsatisfiable
% 4.74/5.11 % SZS output start Refutation
% 4.74/5.11
% 4.74/5.11 clause( 2, [ 'E'( '0', f( X ) ), 'LE'( f( X ), '0' ), ~( 'LE'( f( X ), s(
% 4.74/5.11 '0' ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 3, [ ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'( s( '0' ), f( suc( X ) )
% 4.74/5.11 ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y
% 4.74/5.11 ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ),
% 4.74/5.11 ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ),
% 4.74/5.11 ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) )
% 4.74/5.11 ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 4.74/5.11 X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( f( T ), f( suc( T ) )
% 4.74/5.11 ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.11 Z ) ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( iLEQ( suc( T ), suc( Z )
% 4.74/5.11 ) ), ~( iLEQ( suc( Z ), suc( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 5, [ ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( f( X ), f(
% 4.74/5.11 suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f(
% 4.74/5.11 X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 6, [ 'E'( s( '0' ), f( suc( suc( X ) ) ) ), 'LE'( f( X ), s( '0' )
% 4.74/5.11 ), ~( 'LE'( f( suc( suc( X ) ) ), s( s( '0' ) ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 7, [ ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( X ) ) ) ), 'E'(
% 4.74/5.11 f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 10, [ 'LE'( f( X ), s( s( '0' ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 14, [ 'E'( '0', f( suc( X ) ) ), 'LE'( f( X ), '0' ), ~( 'LE'( f(
% 4.74/5.11 suc( X ) ), s( '0' ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 18, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~(
% 4.74/5.11 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc(
% 4.74/5.11 Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~(
% 4.74/5.11 'E'( '0', f( T ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f( Y ), f( suc(
% 4.74/5.11 Y ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ), ~(
% 4.74/5.11 iLEQ( suc( Y ), suc( Z ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( iLEQ(
% 4.74/5.11 suc( X ), suc( Y ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 24, [ ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'( s( '0' ), f( suc( X ) )
% 4.74/5.11 ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( 'E'(
% 4.74/5.11 s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'(
% 4.74/5.11 s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), 'E'( f( T ), f(
% 4.74/5.11 suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) )
% 4.74/5.11 , 'E'( f( Y ), f( suc( Y ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( iLEQ(
% 4.74/5.11 suc( T ), suc( Z ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 25, [ ~( 'LE'( f( z ), '0' ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 26, [ 'E'( '0', f( suc( suc( X ) ) ) ), 'LE'( f( X ), '0' ), ~(
% 4.74/5.11 'LE'( f( suc( suc( X ) ) ), s( '0' ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 29, [ 'E'( s( '0' ), f( X ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 30, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X )
% 4.74/5.11 ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) ) )
% 4.74/5.11 , ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0'
% 4.74/5.11 , f( suc( suc( T ) ) ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( 'E'( f( Y
% 4.74/5.11 ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T
% 4.74/5.11 ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) )
% 4.74/5.11 ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'(
% 4.74/5.11 f( X ), f( suc( X ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( iLEQ( suc(
% 4.74/5.11 Y ), suc( T ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 32, [ ~( 'E'( s( '0' ), f( X ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 4.74/5.11 ~( 'E'( s( '0' ), f( suc( X ) ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 33, [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( suc( X
% 4.74/5.11 ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( '0', f( X ) ) ),
% 4.74/5.11 iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 41, [ 'E'( s( '0' ), f( suc( X ) ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 108, [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( Y ), f( suc( Y ) )
% 4.74/5.11 ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( 'E'( s( '0' ), f( Y
% 4.74/5.11 ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( X )
% 4.74/5.11 ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 4.74/5.11 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( iLEQ( suc( Y ), suc(
% 4.74/5.11 X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 109, [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) )
% 4.74/5.11 ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 4.74/5.11 suc( X ) ) ) ), ~( iLEQ( suc( X ), suc( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 312, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~(
% 4.74/5.11 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), 'E'( f( X ), f( suc(
% 4.74/5.11 X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ),
% 4.74/5.11 ~( iLEQ( suc( Y ), suc( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 313, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( X ) ) ), 'E'(
% 4.74/5.11 f( X ), f( suc( X ) ) ), ~( iLEQ( suc( X ), suc( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 418, [ ~( 'E'( s( '0' ), f( X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ),
% 4.74/5.11 ~( 'E'( s( '0' ), f( Y ) ) ), 'E'( f( X ), f( suc( X ) ) ), ~( 'E'( s(
% 4.74/5.11 '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( iLEQ(
% 4.74/5.11 suc( Y ), suc( X ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 419, [ ~( 'E'( s( '0' ), f( X ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 4.74/5.11 ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( iLEQ( suc( X ), suc( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 481, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X
% 4.74/5.11 ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) )
% 4.74/5.11 ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( 'E'( f( Y
% 4.74/5.11 ), f( suc( Y ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( iLEQ( suc( Y
% 4.74/5.11 ), suc( X ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 482, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X
% 4.74/5.11 ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ),
% 4.74/5.11 ~( iLEQ( suc( X ), suc( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 666, [ 'E'( '0', f( X ) ), 'E'( s( '0' ), f( suc( X ) ) ), 'LE'( f(
% 4.74/5.11 X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 667, [ 'E'( '0', f( X ) ), 'E'( s( '0' ), f( X ) ), 'LE'( f( X ),
% 4.74/5.11 '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 668, [ 'E'( '0', f( z ) ), 'E'( s( '0' ), f( z ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 669, [ 'E'( '0', f( z ) ), 'E'( s( '0' ), f( suc( z ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 670, [ 'E'( '0', f( suc( X ) ) ), 'E'( s( '0' ), f( suc( suc( X ) )
% 4.74/5.11 ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 671, [ 'E'( '0', f( suc( X ) ) ), 'E'( s( '0' ), f( suc( X ) ) ),
% 4.74/5.11 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 672, [ 'E'( '0', f( suc( z ) ) ), 'E'( s( '0' ), f( suc( z ) ) ) ]
% 4.74/5.11 )
% 4.74/5.11 .
% 4.74/5.11 clause( 673, [ 'E'( '0', f( suc( z ) ) ), 'E'( s( '0' ), f( suc( suc( z ) )
% 4.74/5.11 ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 674, [ 'E'( '0', f( suc( suc( X ) ) ) ), 'E'( s( '0' ), f( suc( suc(
% 4.74/5.11 suc( X ) ) ) ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 675, [ 'E'( '0', f( suc( suc( X ) ) ) ), 'E'( s( '0' ), f( suc( suc(
% 4.74/5.11 X ) ) ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 676, [ 'E'( '0', f( suc( suc( z ) ) ) ), 'E'( s( '0' ), f( suc( suc(
% 4.74/5.11 z ) ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 677, [ 'E'( '0', f( suc( suc( z ) ) ) ), 'E'( s( '0' ), f( suc( suc(
% 4.74/5.11 suc( z ) ) ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 678, [ ~( 'E'( '0', f( suc( X ) ) ) ), 'E'( f( X ), f( suc( X ) ) )
% 4.74/5.11 , ~( 'E'( '0', f( X ) ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 681, [ 'E'( s( '0' ), f( suc( suc( X ) ) ) ), 'LE'( f( X ), s( '0'
% 4.74/5.11 ) ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 682, [ 'E'( s( '0' ), f( suc( suc( suc( suc( X ) ) ) ) ) ), 'E'(
% 4.74/5.11 '0', f( suc( suc( X ) ) ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 683, [ 'E'( s( '0' ), f( suc( suc( suc( X ) ) ) ) ), 'E'( '0', f(
% 4.74/5.11 suc( X ) ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 684, [ 'E'( s( '0' ), f( suc( suc( X ) ) ) ), 'E'( '0', f( X ) ),
% 4.74/5.11 'LE'( f( X ), '0' ) ] )
% 4.74/5.11 .
% 4.74/5.11 clause( 685, [ 'E'( '0', f( z ) ), 'E'( s( '0' ), f( suc( suc( z ) ) ) ) ]
% 4.74/5.11 )
% 4.74/5.11 .
% 4.74/5.11 clause( 686, [ 'E'( '0', f( suc( z ) ) ), 'E'( s( '0' ), f( suc( suc( suc(
% 4.74/5.11 z ) ) ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 687, [ 'E'( '0', f( suc( suc( z ) ) ) ), 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 suc( suc( z ) ) ) ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 688, [ 'E'( f( X ), f( suc( X ) ) ), ~( 'E'( s( '0' ), f( suc( X )
% 4.74/5.12 ) ) ), ~( 'E'( s( '0' ), f( X ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 699, [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( suc(
% 4.74/5.12 X ) ) ) ), ~( 'E'( '0', f( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 700, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X
% 4.74/5.12 ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( iLEQ( suc( X ), suc( X ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 701, [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( X ) )
% 4.74/5.12 ), ~( 'E'( '0', f( suc( X ) ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 702, [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( iLEQ( suc( X ), suc(
% 4.74/5.12 X ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 703, [ ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' )
% 4.74/5.12 , f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 704, [ 'E'( '0', f( suc( suc( z ) ) ) ), ~( 'E'( s( '0' ), f( suc(
% 4.74/5.12 suc( z ) ) ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 706, [ 'E'( '0', f( suc( z ) ) ), ~( 'E'( s( '0' ), f( suc( z ) ) )
% 4.74/5.12 ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 708, [ 'E'( '0', f( z ) ), ~( 'E'( s( '0' ), f( z ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 715, [ 'E'( '0', f( z ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 720, [ 'E'( '0', f( suc( z ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 722, [ ~( 'E'( '0', f( suc( suc( z ) ) ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 724, [ ~( 'E'( s( '0' ), f( suc( suc( z ) ) ) ) ) ] )
% 4.74/5.12 .
% 4.74/5.12 clause( 725, [] )
% 4.74/5.12 .
% 4.74/5.12
% 4.74/5.12
% 4.74/5.12 % SZS output end Refutation
% 4.74/5.12 found a proof!
% 4.74/5.12
% 4.74/5.12 % ABCDEFGHIJKLMNOPQRSTUVWXYZ
% 4.74/5.12
% 4.74/5.12 initialclauses(
% 4.74/5.12 [ clause( 727, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( suc( Z ) ) ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ),
% 4.74/5.12 f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) )
% 4.74/5.12 ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( T ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f(
% 4.74/5.12 suc( X ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 728, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( iLEQ( suc(
% 4.74/5.12 T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc(
% 4.74/5.12 Y ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( Z ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f( suc( X
% 4.74/5.12 ) ) ), 'E'( f( Y ), f( suc( Y ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 729, [ ~( 'LE'( f( X ), s( '0' ) ) ), 'E'( '0', f( X ) ), 'LE'( f(
% 4.74/5.12 X ), '0' ) ] )
% 4.74/5.12 , clause( 730, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 4.74/5.12 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~(
% 4.74/5.12 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) )
% 4.74/5.12 ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X )
% 4.74/5.12 ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) )
% 4.74/5.12 , ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) )
% 4.74/5.12 , ~( 'E'( s( '0' ), f( suc( suc( Z ) ) ) ) ) ] )
% 4.74/5.12 , clause( 731, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 4.74/5.12 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) )
% 4.74/5.12 ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X )
% 4.74/5.12 ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) )
% 4.74/5.12 ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ) ]
% 4.74/5.12 )
% 4.74/5.12 , clause( 732, [ ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( suc( X ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.12 , clause( 733, [ ~( 'LE'( f( suc( suc( X ) ) ), s( s( '0' ) ) ) ), 'E'( s(
% 4.74/5.12 '0' ), f( suc( suc( X ) ) ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 4.74/5.12 , clause( 734, [ ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( X ) ) ) ),
% 4.74/5.12 'E'( f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.12 , clause( 735, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0',
% 4.74/5.12 f( suc( suc( T ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f(
% 4.74/5.12 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( T )
% 4.74/5.12 ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( Z ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f( suc( X
% 4.74/5.12 ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 736, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f(
% 4.74/5.12 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f( suc(
% 4.74/5.12 Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~(
% 4.74/5.12 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~(
% 4.74/5.12 'E'( '0', f( Z ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f(
% 4.74/5.12 suc( X ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 737, [ 'LE'( f( X ), s( s( '0' ) ) ) ] )
% 4.74/5.12 , clause( 738, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X )
% 4.74/5.12 , suc( Y ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( T ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X
% 4.74/5.12 ) ) ), 'E'( f( Y ), f( suc( Y ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 739, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) )
% 4.74/5.12 ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~(
% 4.74/5.12 iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f(
% 4.74/5.12 suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ),
% 4.74/5.12 ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X
% 4.74/5.12 ), f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( T ), f(
% 4.74/5.12 suc( T ) ) ) ] )
% 4.74/5.12 , clause( 740, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 4.74/5.12 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ),
% 4.74/5.12 ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) )
% 4.74/5.12 ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~(
% 4.74/5.12 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( suc( Z ) ) ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ]
% 4.74/5.12 )
% 4.74/5.12 , clause( 741, [ ~( 'LE'( f( suc( X ) ), s( '0' ) ) ), 'E'( '0', f( suc( X
% 4.74/5.12 ) ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.12 , clause( 742, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( '0', f(
% 4.74/5.12 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( T )
% 4.74/5.12 ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X ),
% 4.74/5.12 f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( Y ), f( suc(
% 4.74/5.12 Y ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 743, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( suc( suc( T ) ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X )
% 4.74/5.12 , suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T
% 4.74/5.12 ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) )
% 4.74/5.12 , ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~(
% 4.74/5.12 'E'( '0', f( Z ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( X ), f(
% 4.74/5.12 suc( X ) ) ) ] )
% 4.74/5.12 , clause( 744, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'(
% 4.74/5.12 s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( suc( suc( Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( X ),
% 4.74/5.12 f( suc( X ) ) ) ] )
% 4.74/5.12 , clause( 745, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( X ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f(
% 4.74/5.12 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( Z )
% 4.74/5.12 ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( T ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X
% 4.74/5.12 ) ) ), 'E'( f( Y ), f( suc( Y ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'(
% 4.74/5.12 f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 746, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f(
% 4.74/5.12 suc( suc( Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( X ), f( suc(
% 4.74/5.12 X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 747, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( iLEQ(
% 4.74/5.12 suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X )
% 4.74/5.12 , suc( Y ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X ),
% 4.74/5.12 f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( Y ), f( suc(
% 4.74/5.12 Y ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 748, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~(
% 4.74/5.12 iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( Y ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f(
% 4.74/5.12 suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) ) ] )
% 4.74/5.12 , clause( 749, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) )
% 4.74/5.12 ), ~( 'E'( '0', f( X ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0'
% 4.74/5.12 , f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ), f(
% 4.74/5.12 suc( Y ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X ),
% 4.74/5.12 f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( Z ), f( suc(
% 4.74/5.12 Z ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 750, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( suc( suc( T ) ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X )
% 4.74/5.12 , suc( Y ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) ) ),
% 4.74/5.12 ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) ),
% 4.74/5.12 ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X
% 4.74/5.12 ), f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( Y ), f(
% 4.74/5.12 suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 751, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f(
% 4.74/5.12 suc( Y ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) )
% 4.74/5.12 ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 752, [ ~( 'LE'( f( z ), '0' ) ) ] )
% 4.74/5.12 , clause( 753, [ ~( 'LE'( f( suc( suc( X ) ) ), s( '0' ) ) ), 'E'( '0', f(
% 4.74/5.12 suc( suc( X ) ) ) ), 'LE'( f( X ), '0' ) ] )
% 4.74/5.12 , clause( 754, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( X ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( suc( Z ) ) ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f(
% 4.74/5.12 suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ),
% 4.74/5.12 ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( f( X
% 4.74/5.12 ), f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( Y ), f(
% 4.74/5.12 suc( Y ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 755, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 4.74/5.12 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'(
% 4.74/5.12 s( '0' ), f( X ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' )
% 4.74/5.12 , f( suc( Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X ), f( suc( X
% 4.74/5.12 ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 756, [ ~( 'LE'( f( X ), s( s( '0' ) ) ) ), 'E'( s( '0' ), f( X )
% 4.74/5.12 ), 'LE'( f( X ), s( '0' ) ) ] )
% 4.74/5.12 , clause( 757, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) )
% 4.74/5.12 ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( suc( T ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'(
% 4.74/5.12 '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ),
% 4.74/5.12 f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) )
% 4.74/5.12 ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) )
% 4.74/5.12 , ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f(
% 4.74/5.12 X ), f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ) ] )
% 4.74/5.12 , clause( 758, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 4.74/5.12 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) )
% 4.74/5.12 ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X
% 4.74/5.12 ), f( suc( X ) ) ) ] )
% 4.74/5.12 , clause( 759, [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( X
% 4.74/5.12 ) ) ) ), 'E'( f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.12 , clause( 760, [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( suc(
% 4.74/5.12 X ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( '0', f( X ) ) ),
% 4.74/5.12 iLEQ( suc( X ), suc( X ) ) ] )
% 4.74/5.12 , clause( 761, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 4.74/5.12 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) )
% 4.74/5.12 ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( T ), suc( Z ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X )
% 4.74/5.12 , suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T
% 4.74/5.12 ) ) ) ), ~( 'E'( '0', f( T ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) )
% 4.74/5.12 , ~( 'E'( '0', f( suc( Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f( X )
% 4.74/5.12 , f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ), 'E'( f( T ), f( suc(
% 4.74/5.12 T ) ) ) ] )
% 4.74/5.12 , clause( 762, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ(
% 4.74/5.12 suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( Y ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f(
% 4.74/5.12 suc( Z ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 763, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~(
% 4.74/5.12 iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) )
% 4.74/5.12 , ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'(
% 4.74/5.12 s( '0' ), f( suc( Y ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f(
% 4.74/5.12 suc( Z ) ) ) ] )
% 4.74/5.12 , clause( 764, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( suc( Y ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'(
% 4.74/5.12 s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'(
% 4.74/5.12 f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( suc( Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 4.74/5.12 , clause( 765, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 4.74/5.12 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f(
% 4.74/5.12 Z ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0'
% 4.74/5.12 ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X
% 4.74/5.12 ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( suc( Z ) ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Y
% 4.74/5.12 ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 766, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 4.74/5.12 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~(
% 4.74/5.12 'E'( s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ),
% 4.74/5.12 ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f(
% 4.74/5.12 T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s(
% 4.74/5.12 '0' ), f( suc( suc( Z ) ) ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f( Y
% 4.74/5.12 ), f( suc( Y ) ) ) ] )
% 4.74/5.12 , clause( 767, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 4.74/5.12 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 4.74/5.12 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 5.03/5.46 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~(
% 5.03/5.46 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~(
% 5.03/5.46 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) )
% 5.03/5.46 ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~(
% 5.03/5.46 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~(
% 5.03/5.46 'E'( s( '0' ), f( suc( suc( Z ) ) ) ) ), 'E'( f( X ), f( suc( X ) ) ) ]
% 5.03/5.46 )
% 5.03/5.46 , clause( 768, [ ~( 'LE'( f( suc( X ) ), s( s( '0' ) ) ) ), 'E'( s( '0' ),
% 5.03/5.46 f( suc( X ) ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 5.03/5.46 , clause( 769, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 5.03/5.46 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 5.03/5.46 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 5.03/5.46 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~(
% 5.03/5.46 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'(
% 5.03/5.46 s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'(
% 5.03/5.46 f( X ), f( suc( X ) ) ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s(
% 5.03/5.46 '0' ), f( suc( Y ) ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( Y ), f(
% 5.03/5.46 suc( Y ) ) ) ] )
% 5.03/5.46 , clause( 770, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 5.03/5.46 ~( 'E'( '0', f( suc( suc( Y ) ) ) ) ), ~( 'E'( '0', f( X ) ) ), ~( iLEQ(
% 5.03/5.46 suc( Z ), suc( T ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X )
% 5.03/5.46 , suc( Y ) ) ), ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( Z
% 5.03/5.46 ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'(
% 5.03/5.46 '0', f( T ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X
% 5.03/5.46 ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ) ] )
% 5.03/5.46 ] ).
% 5.03/5.46
% 5.03/5.46
% 5.03/5.46
% 5.03/5.46 subsumption(
% 5.03/5.46 clause( 2, [ 'E'( '0', f( X ) ), 'LE'( f( X ), '0' ), ~( 'LE'( f( X ), s(
% 5.03/5.46 '0' ) ) ) ] )
% 5.03/5.46 , clause( 729, [ ~( 'LE'( f( X ), s( '0' ) ) ), 'E'( '0', f( X ) ), 'LE'( f(
% 5.03/5.46 X ), '0' ) ] )
% 5.03/5.46 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1,
% 5.11/5.46 0 ), ==>( 2, 1 )] ) ).
% 5.11/5.46
% 5.11/5.46
% 5.11/5.46 subsumption(
% 5.11/5.46 clause( 3, [ ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'( s( '0' ), f( suc( X ) )
% 5.11/5.46 ) ), ~( 'E'( s( '0' ), f( suc( suc( T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y
% 5.11/5.46 ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ),
% 5.11/5.46 ~( 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ),
% 5.11/5.46 ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) )
% 5.11/5.46 ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 5.11/5.46 X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( f( T ), f( suc( T ) )
% 5.11/5.46 ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 5.11/5.46 Z ) ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( iLEQ( suc( T ), suc( Z )
% 5.11/5.46 ) ), ~( iLEQ( suc( Z ), suc( X ) ) ) ] )
% 5.11/5.46 , clause( 730, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 5.11/5.46 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc(
% 5.11/5.46 T ) ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ),
% 5.11/5.46 ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~(
% 5.11/5.46 'E'( f( Y ), f( suc( Y ) ) ) ), ~( 'E'( s( '0' ), f( suc( T ) ) ) ), ~(
% 5.11/5.46 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) )
% 5.11/5.46 ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X )
% 5.11/5.46 ) ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) )
% 5.11/5.46 , ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) )
% 5.11/5.46 , ~( 'E'( s( '0' ), f( suc( suc( Z ) ) ) ) ) ] )
% 5.11/5.46 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 5.11/5.46 permutation( 0, [ ==>( 0, 16 ), ==>( 1, 0 ), ==>( 2, 1 ), ==>( 3, 2 ),
% 5.11/5.46 ==>( 4, 3 ), ==>( 5, 4 ), ==>( 6, 18 ), ==>( 7, 5 ), ==>( 8, 6 ), ==>( 9
% 5.11/5.46 , 7 ), ==>( 10, 8 ), ==>( 11, 9 ), ==>( 12, 17 ), ==>( 13, 10 ), ==>( 14
% 5.11/5.46 , 11 ), ==>( 15, 12 ), ==>( 16, 13 ), ==>( 17, 14 ), ==>( 18, 15 )] )
% 5.11/5.46 ).
% 5.11/5.46
% 5.11/5.46
% 5.11/5.46 subsumption(
% 5.11/5.46 clause( 5, [ ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( f( X ), f(
% 5.11/5.46 suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f(
% 7.68/8.10 X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 7.68/8.10 , clause( 732, [ ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0'
% 7.68/8.10 ), f( suc( X ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0'
% 7.68/8.10 ), f( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 7.68/8.10 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 7.68/8.10 2 ), ==>( 2, 1 ), ==>( 3, 3 ), ==>( 4, 4 )] ) ).
% 7.68/8.10
% 7.68/8.10
% 7.68/8.10 subsumption(
% 7.68/8.10 clause( 6, [ 'E'( s( '0' ), f( suc( suc( X ) ) ) ), 'LE'( f( X ), s( '0' )
% 7.68/8.10 ), ~( 'LE'( f( suc( suc( X ) ) ), s( s( '0' ) ) ) ) ] )
% 7.68/8.10 , clause( 733, [ ~( 'LE'( f( suc( suc( X ) ) ), s( s( '0' ) ) ) ), 'E'( s(
% 7.68/8.10 '0' ), f( suc( suc( X ) ) ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 7.68/8.10 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1,
% 7.68/8.10 0 ), ==>( 2, 1 )] ) ).
% 7.68/8.10
% 7.68/8.10
% 7.68/8.10 subsumption(
% 7.68/8.10 clause( 7, [ ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( X ) ) ) ), 'E'(
% 7.68/8.10 f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 7.68/8.10 , clause( 734, [ ~( 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( X ) ) ) ),
% 7.68/8.10 'E'( f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 7.68/8.10 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 7.68/8.10 1 ), ==>( 2, 2 ), ==>( 3, 3 )] ) ).
% 7.68/8.10
% 7.68/8.10
% 7.68/8.10 subsumption(
% 7.68/8.10 clause( 10, [ 'LE'( f( X ), s( s( '0' ) ) ) ] )
% 7.68/8.10 , clause( 737, [ 'LE'( f( X ), s( s( '0' ) ) ) ] )
% 7.68/8.10 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 7.68/8.10
% 7.68/8.10
% 7.68/8.10 subsumption(
% 7.68/8.10 clause( 14, [ 'E'( '0', f( suc( X ) ) ), 'LE'( f( X ), '0' ), ~( 'LE'( f(
% 7.68/8.10 suc( X ) ), s( '0' ) ) ) ] )
% 7.68/8.10 , clause( 741, [ ~( 'LE'( f( suc( X ) ), s( '0' ) ) ), 'E'( '0', f( suc( X
% 7.68/8.10 ) ) ), 'LE'( f( X ), '0' ) ] )
% 7.68/8.10 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1,
% 7.68/8.10 0 ), ==>( 2, 1 )] ) ).
% 7.68/8.10
% 7.68/8.10
% 7.68/8.10 subsumption(
% 7.68/8.10 clause( 18, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~(
% 7.68/8.10 'E'( '0', f( X ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc(
% 7.68/8.10 Z ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~(
% 7.68/8.10 'E'( '0', f( T ) ) ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f( Y ), f( suc(
% 7.68/8.10 Y ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( T ), f( suc( T ) ) ), ~(
% 7.68/8.10 iLEQ( suc( Y ), suc( Z ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( iLEQ(
% 7.68/8.10 suc( X ), suc( Y ) ) ) ] )
% 7.68/8.10 , clause( 745, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( Y ) ) ),
% 7.68/8.10 ~( 'E'( '0', f( X ) ) ), ~( iLEQ( suc( Z ), suc( T ) ) ), ~( 'E'( '0', f(
% 7.68/8.10 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( '0', f( suc( Z )
% 7.68/8.10 ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'(
% 7.68/8.10 '0', f( T ) ) ), ~( iLEQ( suc( Y ), suc( Z ) ) ), 'E'( f( X ), f( suc( X
% 7.68/8.10 ) ) ), 'E'( f( Y ), f( suc( Y ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'(
% 7.68/8.10 f( T ), f( suc( T ) ) ) ] )
% 7.68/8.10 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 7.68/8.10 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 13 ),
% 7.68/8.10 ==>( 4, 3 ), ==>( 5, 14 ), ==>( 6, 4 ), ==>( 7, 5 ), ==>( 8, 6 ), ==>( 9
% 7.68/8.10 , 7 ), ==>( 10, 12 ), ==>( 11, 8 ), ==>( 12, 9 ), ==>( 13, 10 ), ==>( 14
% 7.68/8.10 , 11 )] ) ).
% 7.68/8.10
% 7.68/8.10
% 7.68/8.10 subsumption(
% 7.68/8.10 clause( 24, [ ~( 'E'( s( '0' ), f( Z ) ) ), ~( 'E'( s( '0' ), f( suc( X ) )
% 7.68/8.11 ) ), ~( 'E'( s( '0' ), f( Y ) ) ), ~( 'E'( s( '0' ), f( T ) ) ), ~( 'E'(
% 7.68/8.11 s( '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( 'E'(
% 7.68/8.11 s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( Y ) ) ) ), 'E'( f( T ), f(
% 7.68/8.11 suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) ) ), 'E'( f( X ), f( suc( X ) ) )
% 7.68/8.11 , 'E'( f( Y ), f( suc( Y ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( iLEQ(
% 7.68/8.11 suc( T ), suc( Z ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ) ] )
% 7.68/8.11 , clause( 751, [ ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( s( '0' ), f( Z )
% 7.68/8.11 ) ), ~( 'E'( s( '0' ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( Y ) ) ),
% 7.68/8.11 ~( 'E'( s( '0' ), f( T ) ) ), ~( iLEQ( suc( Z ), suc( X ) ) ), ~( 'E'( s(
% 7.68/8.11 '0' ), f( suc( T ) ) ) ), ~( 'E'( s( '0' ), f( suc( Z ) ) ) ), ~( iLEQ(
% 7.68/8.11 suc( T ), suc( Z ) ) ), ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f(
% 7.68/8.11 suc( Y ) ) ) ), 'E'( f( T ), f( suc( T ) ) ), 'E'( f( Z ), f( suc( Z ) )
% 7.68/8.11 ), 'E'( f( X ), f( suc( X ) ) ), 'E'( f( Y ), f( suc( Y ) ) ) ] )
% 7.68/8.11 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 16.44/16.85 permutation( 0, [ ==>( 0, 14 ), ==>( 1, 0 ), ==>( 2, 1 ), ==>( 3, 2 ),
% 16.44/16.85 ==>( 4, 3 ), ==>( 5, 12 ), ==>( 6, 4 ), ==>( 7, 5 ), ==>( 8, 13 ), ==>( 9
% 16.44/16.85 , 6 ), ==>( 10, 7 ), ==>( 11, 8 ), ==>( 12, 9 ), ==>( 13, 10 ), ==>( 14,
% 16.44/16.85 11 )] ) ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 subsumption(
% 16.44/16.85 clause( 25, [ ~( 'LE'( f( z ), '0' ) ) ] )
% 16.44/16.85 , clause( 752, [ ~( 'LE'( f( z ), '0' ) ) ] )
% 16.44/16.85 , substitution( 0, [] ), permutation( 0, [ ==>( 0, 0 )] ) ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 subsumption(
% 16.44/16.85 clause( 26, [ 'E'( '0', f( suc( suc( X ) ) ) ), 'LE'( f( X ), '0' ), ~(
% 16.44/16.85 'LE'( f( suc( suc( X ) ) ), s( '0' ) ) ) ] )
% 16.44/16.85 , clause( 753, [ ~( 'LE'( f( suc( suc( X ) ) ), s( '0' ) ) ), 'E'( '0', f(
% 16.44/16.85 suc( suc( X ) ) ) ), 'LE'( f( X ), '0' ) ] )
% 16.44/16.85 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 2 ), ==>( 1,
% 16.44/16.85 0 ), ==>( 2, 1 )] ) ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 resolution(
% 16.44/16.85 clause( 52669, [ 'E'( s( '0' ), f( X ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 16.44/16.85 , clause( 756, [ ~( 'LE'( f( X ), s( s( '0' ) ) ) ), 'E'( s( '0' ), f( X )
% 16.44/16.85 ), 'LE'( f( X ), s( '0' ) ) ] )
% 16.44/16.85 , 0, clause( 10, [ 'LE'( f( X ), s( s( '0' ) ) ) ] )
% 16.44/16.85 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, X )] )
% 16.44/16.85 ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 subsumption(
% 16.44/16.85 clause( 29, [ 'E'( s( '0' ), f( X ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 16.44/16.85 , clause( 52669, [ 'E'( s( '0' ), f( X ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 16.44/16.85 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 16.44/16.85 1 )] ) ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 subsumption(
% 16.44/16.85 clause( 30, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc( X )
% 16.44/16.85 ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) ) )
% 16.44/16.85 , ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'( '0'
% 16.44/16.85 , f( suc( suc( T ) ) ) ) ), ~( 'E'( '0', f( suc( Y ) ) ) ), ~( 'E'( f( Y
% 16.44/16.85 ), f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T
% 16.44/16.85 ) ) ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) )
% 16.44/16.85 ) ), ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'(
% 16.44/16.85 f( X ), f( suc( X ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( iLEQ( suc(
% 16.44/16.85 Y ), suc( T ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ) ] )
% 16.44/16.85 , clause( 757, [ ~( 'E'( '0', f( suc( X ) ) ) ), ~( 'E'( '0', f( suc( suc(
% 16.44/16.85 X ) ) ) ) ), ~( 'E'( '0', f( Y ) ) ), ~( 'E'( '0', f( suc( suc( Y ) ) ) )
% 16.44/16.85 ), ~( 'E'( '0', f( X ) ) ), ~( 'E'( f( Z ), f( suc( Z ) ) ) ), ~( 'E'(
% 16.44/16.85 '0', f( suc( suc( T ) ) ) ) ), ~( iLEQ( suc( T ), suc( Z ) ) ), ~( 'E'(
% 16.44/16.85 '0', f( suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( 'E'( f( Y ),
% 16.44/16.85 f( suc( Y ) ) ) ), ~( 'E'( '0', f( suc( T ) ) ) ), ~( 'E'( '0', f( T ) )
% 16.44/16.85 ), ~( 'E'( '0', f( suc( suc( Z ) ) ) ) ), ~( 'E'( '0', f( suc( Z ) ) ) )
% 16.44/16.85 , ~( 'E'( f( T ), f( suc( T ) ) ) ), ~( 'E'( '0', f( Z ) ) ), ~( 'E'( f(
% 16.44/16.85 X ), f( suc( X ) ) ) ), ~( iLEQ( suc( Y ), suc( T ) ) ) ] )
% 16.44/16.85 , substitution( 0, [ :=( X, X ), :=( Y, Y ), :=( Z, Z ), :=( T, T )] ),
% 16.44/16.85 permutation( 0, [ ==>( 0, 0 ), ==>( 1, 1 ), ==>( 2, 2 ), ==>( 3, 3 ),
% 16.44/16.85 ==>( 4, 4 ), ==>( 5, 5 ), ==>( 6, 6 ), ==>( 7, 18 ), ==>( 8, 7 ), ==>( 9
% 16.44/16.85 , 16 ), ==>( 10, 8 ), ==>( 11, 9 ), ==>( 12, 10 ), ==>( 13, 11 ), ==>( 14
% 16.44/16.85 , 12 ), ==>( 15, 13 ), ==>( 16, 14 ), ==>( 17, 15 ), ==>( 18, 17 )] )
% 16.44/16.85 ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 subsumption(
% 16.44/16.85 clause( 32, [ ~( 'E'( s( '0' ), f( X ) ) ), 'E'( f( X ), f( suc( X ) ) ),
% 16.44/16.85 ~( 'E'( s( '0' ), f( suc( X ) ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 16.44/16.85 , clause( 759, [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( s( '0' ), f( suc( X
% 16.44/16.85 ) ) ) ), 'E'( f( X ), f( suc( X ) ) ), iLEQ( suc( X ), suc( X ) ) ] )
% 16.44/16.85 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 16.44/16.85 2 ), ==>( 2, 1 ), ==>( 3, 3 )] ) ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 subsumption(
% 16.44/16.85 clause( 33, [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( suc( X
% 16.44/16.85 ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( '0', f( X ) ) ),
% 16.44/16.85 iLEQ( suc( X ), suc( X ) ) ] )
% 16.44/16.85 , clause( 760, [ ~( 'E'( '0', f( suc( suc( X ) ) ) ) ), ~( 'E'( '0', f( suc(
% 16.44/16.85 X ) ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( '0', f( X ) ) ),
% 16.44/16.85 iLEQ( suc( X ), suc( X ) ) ] )
% 16.44/16.85 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 16.44/16.85 1 ), ==>( 2, 2 ), ==>( 3, 3 ), ==>( 4, 4 )] ) ).
% 16.44/16.85
% 16.44/16.85
% 16.44/16.85 resolution(
% 16.44/16.85 clause( 98354, [ 'E'( s( '0' ), f( suc( X ) ) ), 'LE'( f( X ), s( '0' ) ) ]
% 16.44/16.86 )
% 16.44/16.86 , clause( 768, [ ~( 'LE'( f( suc( X ) ), s( s( '0' ) ) ) ), 'E'( s( '0' ),
% 16.44/16.86 f( suc( X ) ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 16.44/16.86 , 0, clause( 10, [ 'LE'( f( X ), s( s( '0' ) ) ) ] )
% 16.44/16.86 , 0, substitution( 0, [ :=( X, X )] ), substitution( 1, [ :=( X, suc( X ) )] )
% 16.44/16.86 ).
% 16.44/16.86
% 16.44/16.86
% 16.44/16.86 subsumption(
% 16.44/16.86 clause( 41, [ 'E'( s( '0' ), f( suc( X ) ) ), 'LE'( f( X ), s( '0' ) ) ] )
% 16.44/16.86 , clause( 98354, [ 'E'( s( '0' ), f( suc( X ) ) ), 'LE'( f( X ), s( '0' ) )
% 16.44/16.86 ] )
% 16.44/16.86 , substitution( 0, [ :=( X, X )] ), permutation( 0, [ ==>( 0, 0 ), ==>( 1,
% 16.44/16.86 1 )] ) ).
% 16.44/16.86
% 16.44/16.86
% 16.44/16.86
% 16.44/16.86 ==> clause( 108, [ ~( 'E'( s( '0' ), f( X ) ) ), ~( 'E'( f( Y ), f( suc( Y
% 16.44/16.86 ) ) ) ), ~( 'E'( s( '0' ), f( suc( suc( Y ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 16.44/16.86 Y ) ) ), ~( 'E'( f( X ), f( suc( X ) ) ) ), ~( 'E'( s( '0' ), f( suc( X )
% 16.44/16.86 ) ) ), ~( 'E'( s( '0' ), f( suc( suc( X ) ) ) ) ), ~( 'E'( s( '0' ), f(
% 16.44/16.86 suc( Y ) ) ) ), ~( iLEQ( suc( X ), suc( Y ) ) ), ~( iLEQ( suc( Y ), suc(
% 16.44/16.86 X ) ) ) ] )
% 16.44/16.86
% 16.44/16.86
% 16.44/16.86
% 16.44/16.86 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 16.44/16.86
% 16.44/16.86 Bliksem ended
%------------------------------------------------------------------------------