%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM926+5 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.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 : Mon Jul 18 06:27:47 EDT 2022
% Result : Theorem 0.76s 1.22s
% Output : Refutation 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM926+5 : TPTP v8.1.0. Released v5.3.0.
% 0.06/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Thu Jul 7 15:47:15 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.76/1.12 *** allocated 10000 integers for termspace/termends
% 0.76/1.12 *** allocated 10000 integers for clauses
% 0.76/1.12 *** allocated 10000 integers for justifications
% 0.76/1.12 Bliksem 1.12
% 0.76/1.12
% 0.76/1.12
% 0.76/1.12 Automatic Strategy Selection
% 0.76/1.12
% 0.76/1.12
% 0.76/1.12 Clauses:
% 0.76/1.12
% 0.76/1.12 { ! semiring_1( X ), ti( X, one_one( X ) ) = one_one( X ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, ti( X, Y ), Z ) = plus_plus( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, Y, ti( X, Z ) ) = plus_plus( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), ti( X, plus_plus( X, Y, Z ) ) = plus_plus( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! monoid_mult( X ), times_times( X, ti( X, Y ), Z ) = times_times( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! monoid_mult( X ), times_times( X, Y, ti( X, Z ) ) = times_times( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! monoid_mult( X ), ti( X, times_times( X, Y, Z ) ) = times_times( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ti( X, undefined( X ) ) = undefined( X ) }.
% 0.76/1.12 { ! zprime( ti( int, X ) ), zprime( X ) }.
% 0.76/1.12 { ! zprime( X ), zprime( ti( int, X ) ) }.
% 0.76/1.12 { bit0( ti( int, X ) ) = bit0( X ) }.
% 0.76/1.12 { ti( int, bit0( X ) ) = bit0( X ) }.
% 0.76/1.12 { bit1( ti( int, X ) ) = bit1( X ) }.
% 0.76/1.12 { ti( int, bit1( X ) ) = bit1( X ) }.
% 0.76/1.12 { ti( int, pls ) = pls }.
% 0.76/1.12 { ! number( X ), number_number_of( X, ti( int, Y ) ) = number_number_of( X
% 0.76/1.12 , Y ) }.
% 0.76/1.12 { ! number( X ), ti( X, number_number_of( X, Y ) ) = number_number_of( X, Y
% 0.76/1.12 ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less( X, ti( X, Y ), Z ), ord_less
% 0.76/1.12 ( X, Y, Z ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less( X, Y, Z ), ord_less( X, ti( X
% 0.76/1.12 , Y ), Z ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less( X, Y, ti( X, Z ) ), ord_less
% 0.76/1.12 ( X, Y, Z ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less( X, Y, Z ), ord_less( X, Y, ti
% 0.76/1.12 ( X, Z ) ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, ti( X, Y ), Z ),
% 0.76/1.12 ord_less_eq( X, Y, Z ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, Y, Z ), ord_less_eq( X
% 0.76/1.12 , ti( X, Y ), Z ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, Y, ti( X, Z ) ),
% 0.76/1.12 ord_less_eq( X, Y, Z ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, Y, Z ), ord_less_eq( X
% 0.76/1.12 , Y, ti( X, Z ) ) }.
% 0.76/1.12 { ! monoid_mult( X ), power_power( X, ti( X, Y ), Z ) = power_power( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! monoid_mult( X ), power_power( X, Y, ti( nat, Z ) ) = power_power( X, Y
% 0.76/1.12 , Z ) }.
% 0.76/1.12 { ! monoid_mult( X ), ti( X, power_power( X, Y, Z ) ) = power_power( X, Y,
% 0.76/1.12 Z ) }.
% 0.76/1.12 { ! twoSqu33214720sum2sq( ti( int, X ) ), twoSqu33214720sum2sq( X ) }.
% 0.76/1.12 { ! twoSqu33214720sum2sq( X ), twoSqu33214720sum2sq( ti( int, X ) ) }.
% 0.76/1.12 { ti( int, m ) = m }.
% 0.76/1.12 { ti( int, s ) = s }.
% 0.76/1.12 { ti( int, t ) = t }.
% 0.76/1.12 { ord_less_eq( int, one_one( int ), t ) }.
% 0.76/1.12 { ! t = one_one( int ), plus_plus( int, power_power( int, skol1,
% 0.76/1.12 number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int, skol4,
% 0.76/1.12 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = plus_plus( int,
% 0.76/1.12 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.76/1.12 ), one_one( int ) ) }.
% 0.76/1.12 { ! ord_less( int, one_one( int ), t ), plus_plus( int, power_power( int,
% 0.76/1.12 skol2, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int,
% 0.76/1.12 skol5, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = plus_plus( int
% 0.76/1.12 , times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) )
% 0.76/1.12 , m ), one_one( int ) ) }.
% 0.76/1.12 { ord_less( int, t, plus_plus( int, times_times( int, number_number_of( int
% 0.76/1.12 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) ) }.
% 0.76/1.12 { zprime( plus_plus( int, times_times( int, number_number_of( int, bit0(
% 0.76/1.12 bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) ) }.
% 0.76/1.12 { plus_plus( int, power_power( int, s, number_number_of( nat, bit0( bit1(
% 0.76/1.12 pls ) ) ) ), one_one( int ) ) = times_times( int, plus_plus( int,
% 0.76/1.12 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.76/1.12 ), one_one( int ) ), t ) }.
% 0.76/1.12 { twoSqu33214720sum2sq( times_times( int, plus_plus( int, times_times( int
% 0.76/1.12 , number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int
% 0.76/1.12 ) ), t ) ) }.
% 0.76/1.12 { power_power( int, plus_plus( int, X, Y ), number_number_of( nat, bit0(
% 0.76/1.12 bit1( pls ) ) ) ) = plus_plus( int, plus_plus( int, power_power( int, X,
% 0.76/1.12 number_number_of( nat, bit0( bit1( pls ) ) ) ), times_times( int,
% 0.76/1.12 times_times( int, number_number_of( int, bit0( bit1( pls ) ) ), X ), Y )
% 0.76/1.12 ), power_power( int, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) )
% 0.76/1.12 }.
% 0.76/1.12 { power_power( int, plus_plus( int, X, Y ), number_number_of( nat, bit1(
% 0.76/1.12 bit1( pls ) ) ) ) = plus_plus( int, plus_plus( int, plus_plus( int,
% 0.76/1.12 power_power( int, X, number_number_of( nat, bit1( bit1( pls ) ) ) ),
% 0.76/1.12 times_times( int, times_times( int, number_number_of( int, bit1( bit1(
% 0.76/1.12 pls ) ) ), power_power( int, X, number_number_of( nat, bit0( bit1( pls )
% 0.76/1.12 ) ) ) ), Y ) ), times_times( int, times_times( int, number_number_of(
% 0.76/1.12 int, bit1( bit1( pls ) ) ), X ), power_power( int, Y, number_number_of(
% 0.76/1.12 nat, bit0( bit1( pls ) ) ) ) ) ), power_power( int, Y, number_number_of(
% 0.76/1.12 nat, bit1( bit1( pls ) ) ) ) ) }.
% 0.76/1.12 { ! number_semiring( X ), power_power( X, plus_plus( X, Y, Z ),
% 0.76/1.12 number_number_of( nat, bit0( bit1( pls ) ) ) ) = plus_plus( X, plus_plus
% 0.76/1.12 ( X, power_power( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.76/1.12 power_power( X, Z, number_number_of( nat, bit0( bit1( pls ) ) ) ) ),
% 0.76/1.12 times_times( X, times_times( X, number_number_of( X, bit0( bit1( pls ) )
% 0.76/1.12 ), Y ), Z ) ) }.
% 0.76/1.12 { ! monoid_mult( X ), ! number( X ), power_power( X, number_number_of( X, Y
% 0.76/1.12 ), number_number_of( nat, bit0( bit1( pls ) ) ) ) = times_times( X,
% 0.76/1.12 number_number_of( X, Y ), number_number_of( X, Y ) ) }.
% 0.76/1.12 { times_times( int, X, power_power( int, X, number_number_of( nat, bit0(
% 0.76/1.12 bit1( pls ) ) ) ) ) = power_power( int, X, number_number_of( nat, bit1(
% 0.76/1.12 bit1( pls ) ) ) ) }.
% 0.76/1.12 { ! semiring_1( X ), power_power( X, one_one( X ), number_number_of( nat,
% 0.76/1.12 bit0( bit1( pls ) ) ) ) = one_one( X ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, Y, Y ) = power_power( X, Y,
% 0.76/1.12 number_number_of( nat, bit0( bit1( pls ) ) ) ) }.
% 0.76/1.12 { ! monoid_mult( X ), power_power( X, Y, number_number_of( nat, bit0( bit1
% 0.76/1.12 ( pls ) ) ) ) = times_times( X, Y, Y ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), power_power( X, Y, times_times( nat,
% 0.76/1.12 number_number_of( nat, bit0( bit1( pls ) ) ), Z ) ) = times_times( X,
% 0.76/1.12 power_power( X, Y, Z ), power_power( X, Y, Z ) ) }.
% 0.76/1.12 { ! number_ring( X ), plus_plus( X, one_one( X ), number_number_of( X, Y )
% 0.76/1.12 ) = number_number_of( X, plus_plus( int, bit1( pls ), Y ) ) }.
% 0.76/1.12 { ! number_ring( X ), plus_plus( X, number_number_of( X, Y ), one_one( X )
% 0.76/1.12 ) = number_number_of( X, plus_plus( int, Y, bit1( pls ) ) ) }.
% 0.76/1.12 { ! number_ring( X ), plus_plus( X, one_one( X ), one_one( X ) ) =
% 0.76/1.12 number_number_of( X, bit0( bit1( pls ) ) ) }.
% 0.76/1.12 { plus_plus( int, power_power( int, s, number_number_of( nat, bit0( bit1(
% 0.76/1.12 pls ) ) ) ), one_one( int ) ) = times_times( int, plus_plus( int,
% 0.76/1.12 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.76/1.12 ), one_one( int ) ), skol3 ) }.
% 0.76/1.12 { ord_less_eq( int, X, X ) }.
% 0.76/1.12 { ord_less_eq( int, X, Y ), ord_less_eq( int, Y, X ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ! X = Y }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), X = Y, ord_less( int, X, Y ) }.
% 0.76/1.12 { ord_less( int, X, Y ), X = Y, ord_less( int, Y, X ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ! ord_less_eq( int, Y, Z ), ord_less_eq( int
% 0.76/1.12 , X, Z ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ! ord_less_eq( int, Y, X ), X = Y }.
% 0.76/1.12 { ! comm_semiring_1( X ), power_power( X, power_power( X, Y, Z ), T ) =
% 0.76/1.12 power_power( X, Y, times_times( nat, Z, T ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), power_power( X, Y, one_one( nat ) ) = ti( X, Y )
% 0.76/1.12 }.
% 0.76/1.12 { power_power( int, power_power( int, X, Y ), Z ) = power_power( int, X,
% 0.76/1.12 times_times( nat, Y, Z ) ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, number_number_of( X, Y
% 0.76/1.12 ), number_number_of( X, Z ) ), ! ord_less( X, number_number_of( X, Z ),
% 0.76/1.12 number_number_of( X, Y ) ) }.
% 0.76/1.12 { ! number( X ), ! linorder( X ), ord_less( X, number_number_of( X, Z ),
% 0.76/1.12 number_number_of( X, Y ) ), ord_less_eq( X, number_number_of( X, Y ),
% 0.76/1.12 number_number_of( X, Z ) ) }.
% 0.76/1.12 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less( X,
% 0.76/1.12 number_number_of( X, Y ), number_number_of( X, Z ) ), ord_less( int, Y, Z
% 0.76/1.12 ) }.
% 0.76/1.12 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less( int, Y, Z ),
% 0.76/1.12 ord_less( X, number_number_of( X, Y ), number_number_of( X, Z ) ) }.
% 0.76/1.12 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( X,
% 0.76/1.12 number_number_of( X, Y ), number_number_of( X, Z ) ), ord_less_eq( int, Y
% 0.76/1.12 , Z ) }.
% 0.76/1.12 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( int, Y, Z ),
% 0.76/1.12 ord_less_eq( X, number_number_of( X, Y ), number_number_of( X, Z ) ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ! ord_less_eq( int, Z, T ), ord_less( int,
% 0.76/1.12 plus_plus( int, X, Z ), plus_plus( int, Y, T ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, power_power( X, Y, Z ),
% 0.76/1.12 power_power( X, Y, T ) ) = power_power( X, Y, plus_plus( nat, Z, T ) ) }
% 0.76/1.12 .
% 0.76/1.12 { power_power( int, X, plus_plus( nat, Y, Z ) ) = times_times( int,
% 0.76/1.12 power_power( int, X, Y ), power_power( int, X, Z ) ) }.
% 0.76/1.12 { times_times( nat, number_number_of( nat, bit0( bit1( pls ) ) ), X ) =
% 0.76/1.12 plus_plus( nat, X, X ) }.
% 0.76/1.12 { times_times( nat, X, number_number_of( nat, bit0( bit1( pls ) ) ) ) =
% 0.76/1.12 plus_plus( nat, X, X ) }.
% 0.76/1.12 { plus_plus( nat, one_one( nat ), one_one( nat ) ) = number_number_of( nat
% 0.76/1.12 , bit0( bit1( pls ) ) ) }.
% 0.76/1.12 { ! ord_less( int, bit1( X ), bit1( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, bit1( X ), bit1( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, bit1( X ), bit1( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, bit1( X ), bit1( Y ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit1( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit1( X ), bit1( Y ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit1( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit1( X ), bit1( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, pls, pls ) }.
% 0.76/1.12 { ! ord_less( int, bit0( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, bit0( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, bit0( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, bit0( X ), bit0( Y ) ) }.
% 0.76/1.12 { ord_less_eq( int, pls, pls ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit0( X ), bit0( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit0( X ), bit0( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, number_number_of( int, X ), number_number_of( int, Y ) )
% 0.76/1.12 , ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, number_number_of( int, X ),
% 0.76/1.12 number_number_of( int, Y ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, number_number_of( int, X ), number_number_of( int, Y
% 0.76/1.12 ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, number_number_of( int, X )
% 0.76/1.12 , number_number_of( int, Y ) ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, plus_plus( int, X, Z ), plus_plus
% 0.76/1.12 ( int, Y, Z ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, plus_plus( int, Z, X ),
% 0.76/1.12 plus_plus( int, Z, Y ) ) }.
% 0.76/1.12 { ! ord_less( int, Y, pls ), plus_plus( nat, number_number_of( nat, Y ),
% 0.76/1.12 number_number_of( nat, X ) ) = number_number_of( nat, X ) }.
% 0.76/1.12 { ord_less( int, Y, pls ), ! ord_less( int, X, pls ), plus_plus( nat,
% 0.76/1.12 number_number_of( nat, Y ), number_number_of( nat, X ) ) =
% 0.76/1.12 number_number_of( nat, Y ) }.
% 0.76/1.12 { ord_less( int, Y, pls ), ord_less( int, X, pls ), plus_plus( nat,
% 0.76/1.12 number_number_of( nat, Y ), number_number_of( nat, X ) ) =
% 0.76/1.12 number_number_of( nat, plus_plus( int, Y, X ) ) }.
% 0.76/1.12 { number_number_of( nat, bit1( pls ) ) = one_one( nat ) }.
% 0.76/1.12 { one_one( nat ) = number_number_of( nat, bit1( pls ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit1( X ), pls ), ord_less( int, X, pls ) }.
% 0.76/1.12 { ! ord_less( int, X, pls ), ord_less_eq( int, bit1( X ), pls ) }.
% 0.76/1.12 { ! ord_less( int, pls, bit1( X ) ), ord_less_eq( int, pls, X ) }.
% 0.76/1.12 { ! ord_less_eq( int, pls, X ), ord_less( int, pls, bit1( X ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit1( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less_eq( int, bit1( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less_eq( int, bit1( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less_eq( int, bit1( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less( int, bit0( X ), bit1( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less( int, bit0( X ), bit1( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less_eq( int, plus_plus( int, X, one_one(
% 0.76/1.12 int ) ), Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, plus_plus( int, X, one_one( int ) ), Y ), ord_less(
% 0.76/1.12 int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less_eq( int, plus_plus( int, X, one_one(
% 0.76/1.12 int ) ), Y ) }.
% 0.76/1.12 { ! ord_less( int, X, plus_plus( int, Y, one_one( int ) ) ), ord_less_eq(
% 0.76/1.12 int, X, Y ) }.
% 0.76/1.12 { ! ord_less_eq( int, X, Y ), ord_less( int, X, plus_plus( int, Y, one_one
% 0.76/1.12 ( int ) ) ) }.
% 0.76/1.12 { zprime( number_number_of( int, bit0( bit1( pls ) ) ) ) }.
% 0.76/1.12 { ! twoSqu33214720sum2sq( X ), ! twoSqu33214720sum2sq( Y ),
% 0.76/1.12 twoSqu33214720sum2sq( times_times( int, X, Y ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, times_times( X, Y, Z ),
% 0.76/1.12 times_times( X, T, U ) ) = times_times( X, times_times( X, Y, T ),
% 0.76/1.12 times_times( X, Z, U ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, times_times( X, Y, Z ),
% 0.76/1.12 times_times( X, T, U ) ) = times_times( X, T, times_times( X, times_times
% 0.76/1.12 ( X, Y, Z ), U ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, times_times( X, Y, Z ),
% 0.76/1.12 times_times( X, T, U ) ) = times_times( X, Y, times_times( X, Z,
% 0.76/1.12 times_times( X, T, U ) ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, times_times( X, Y, Z ), T ) =
% 0.76/1.12 times_times( X, times_times( X, Y, T ), Z ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, times_times( X, Y, Z ), T ) =
% 0.76/1.12 times_times( X, Y, times_times( X, Z, T ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, Y, times_times( X, Z, T ) ) =
% 0.76/1.12 times_times( X, times_times( X, Y, Z ), T ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, Y, times_times( X, Z, T ) ) =
% 0.76/1.12 times_times( X, Z, times_times( X, Y, T ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), times_times( X, Y, Z ) = times_times( X, Z, Y ) }
% 0.76/1.12 .
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, plus_plus( X, Y, Z ), plus_plus( X
% 0.76/1.12 , T, U ) ) = plus_plus( X, plus_plus( X, Y, T ), plus_plus( X, Z, U ) ) }
% 0.76/1.12 .
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, plus_plus( X, Y, Z ), T ) =
% 0.76/1.12 plus_plus( X, plus_plus( X, Y, T ), Z ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, plus_plus( X, Y, Z ), T ) =
% 0.76/1.12 plus_plus( X, Y, plus_plus( X, Z, T ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, Y, plus_plus( X, Z, T ) ) =
% 0.76/1.12 plus_plus( X, plus_plus( X, Y, Z ), T ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, Y, plus_plus( X, Z, T ) ) =
% 0.76/1.12 plus_plus( X, Z, plus_plus( X, Y, T ) ) }.
% 0.76/1.12 { ! comm_semiring_1( X ), plus_plus( X, Y, Z ) = plus_plus( X, Z, Y ) }.
% 0.76/1.12 { ! number_ring( X ), ! ring_char_0( X ), ! number_number_of( X, Y ) =
% 0.76/1.12 number_number_of( X, Z ), Y = Z }.
% 0.76/1.12 { ! number_ring( X ), ! ring_char_0( X ), ! Y = Z, number_number_of( X, Y )
% 0.76/1.12 = number_number_of( X, Z ) }.
% 0.76/1.12 { ! number( X ), ! number_number_of( X, Y ) = ti( X, Z ), ti( X, Z ) =
% 0.76/1.12 number_number_of( X, Y ) }.
% 0.76/1.12 { ! number( X ), ! ti( X, Z ) = number_number_of( X, Y ), number_number_of
% 0.76/1.12 ( X, Y ) = ti( X, Z ) }.
% 0.76/1.12 { ! bit1( X ) = bit1( Y ), X = Y }.
% 0.76/1.12 { ! X = Y, bit1( X ) = bit1( Y ) }.
% 0.76/1.12 { ! bit0( X ) = bit0( Y ), X = Y }.
% 0.76/1.12 { ! X = Y, bit0( X ) = bit0( Y ) }.
% 0.76/1.12 { times_times( int, times_times( int, X, Y ), Z ) = times_times( int, X,
% 0.76/1.12 times_times( int, Y, Z ) ) }.
% 0.76/1.12 { times_times( int, X, Y ) = times_times( int, Y, X ) }.
% 0.76/1.12 { number_number_of( int, X ) = X }.
% 0.76/1.12 { plus_plus( int, plus_plus( int, X, Y ), Z ) = plus_plus( int, X,
% 0.76/1.12 plus_plus( int, Y, Z ) ) }.
% 0.76/1.12 { plus_plus( int, X, plus_plus( int, Y, Z ) ) = plus_plus( int, Y,
% 0.76/1.12 plus_plus( int, X, Z ) ) }.
% 0.76/1.12 { plus_plus( int, X, Y ) = plus_plus( int, Y, X ) }.
% 0.76/1.12 { ! ord_less( int, bit1( X ), pls ), ord_less( int, X, pls ) }.
% 0.76/1.12 { ! ord_less( int, X, pls ), ord_less( int, bit1( X ), pls ) }.
% 0.76/1.12 { ! ord_less( int, bit1( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, bit1( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, bit1( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.12 { ! ord_less( int, X, Y ), ord_less( int, bit1( X ), bit0( Y ) ) }.
% 0.76/1.12 { ! ord_less( int, bit0( X ), pls ), ord_less( int, X, pls ) }.
% 0.76/1.12 { ! ord_less( int, X, pls ), ord_less( int, bit0( X ), pls ) }.
% 0.76/1.22 { ! ord_less( int, pls, bit0( X ) ), ord_less( int, pls, X ) }.
% 0.76/1.22 { ! ord_less( int, pls, X ), ord_less( int, pls, bit0( X ) ) }.
% 0.76/1.22 { ! ord_less_eq( int, pls, bit1( X ) ), ord_less_eq( int, pls, X ) }.
% 0.76/1.22 { ! ord_less_eq( int, pls, X ), ord_less_eq( int, pls, bit1( X ) ) }.
% 0.76/1.22 { ! ord_less_eq( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.22 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit1( Y ) ) }.
% 0.76/1.22 { ! ord_less_eq( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.22 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit1( Y ) ) }.
% 0.76/1.22 { linordered_idom( int ) }.
% 0.76/1.22 { comm_semiring_1( int ) }.
% 0.76/1.22 { number_semiring( int ) }.
% 0.76/1.22 { linorder( int ) }.
% 0.76/1.22 { monoid_mult( int ) }.
% 0.76/1.22 { semiring_1( int ) }.
% 0.76/1.22 { ring_char_0( int ) }.
% 0.76/1.22 { number_ring( int ) }.
% 0.76/1.22 { number( int ) }.
% 0.76/1.22 { comm_semiring_1( nat ) }.
% 0.76/1.22 { number_semiring( nat ) }.
% 0.76/1.22 { linorder( nat ) }.
% 0.76/1.22 { monoid_mult( nat ) }.
% 0.76/1.22 { semiring_1( nat ) }.
% 0.76/1.22 { number( nat ) }.
% 0.76/1.22 { ti( X, ti( X, Y ) ) = ti( X, Y ) }.
% 0.76/1.22 { ! plus_plus( int, power_power( int, X, number_number_of( nat, bit0( bit1
% 0.76/1.22 ( pls ) ) ) ), power_power( int, Y, number_number_of( nat, bit0( bit1(
% 0.76/1.22 pls ) ) ) ) ) = plus_plus( int, times_times( int, number_number_of( int,
% 0.76/1.22 bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22
% 0.76/1.22 percentage equality = 0.285276, percentage horn = 0.964072
% 0.76/1.22 This is a problem with some equality
% 0.76/1.22
% 0.76/1.22
% 0.76/1.22
% 0.76/1.22 Options Used:
% 0.76/1.22
% 0.76/1.22 useres = 1
% 0.76/1.22 useparamod = 1
% 0.76/1.22 useeqrefl = 1
% 0.76/1.22 useeqfact = 1
% 0.76/1.22 usefactor = 1
% 0.76/1.22 usesimpsplitting = 0
% 0.76/1.22 usesimpdemod = 5
% 0.76/1.22 usesimpres = 3
% 0.76/1.22
% 0.76/1.22 resimpinuse = 1000
% 0.76/1.22 resimpclauses = 20000
% 0.76/1.22 substype = eqrewr
% 0.76/1.22 backwardsubs = 1
% 0.76/1.22 selectoldest = 5
% 0.76/1.22
% 0.76/1.22 litorderings [0] = split
% 0.76/1.22 litorderings [1] = extend the termordering, first sorting on arguments
% 0.76/1.22
% 0.76/1.22 termordering = kbo
% 0.76/1.22
% 0.76/1.22 litapriori = 0
% 0.76/1.22 termapriori = 1
% 0.76/1.22 litaposteriori = 0
% 0.76/1.22 termaposteriori = 0
% 0.76/1.22 demodaposteriori = 0
% 0.76/1.22 ordereqreflfact = 0
% 0.76/1.22
% 0.76/1.22 litselect = negord
% 0.76/1.22
% 0.76/1.22 maxweight = 15
% 0.76/1.22 maxdepth = 30000
% 0.76/1.22 maxlength = 115
% 0.76/1.22 maxnrvars = 195
% 0.76/1.22 excuselevel = 1
% 0.76/1.22 increasemaxweight = 1
% 0.76/1.22
% 0.76/1.22 maxselected = 10000000
% 0.76/1.22 maxnrclauses = 10000000
% 0.76/1.22
% 0.76/1.22 showgenerated = 0
% 0.76/1.22 showkept = 0
% 0.76/1.22 showselected = 0
% 0.76/1.22 showdeleted = 0
% 0.76/1.22 showresimp = 1
% 0.76/1.22 showstatus = 2000
% 0.76/1.22
% 0.76/1.22 prologoutput = 0
% 0.76/1.22 nrgoals = 5000000
% 0.76/1.22 totalproof = 1
% 0.76/1.22
% 0.76/1.22 Symbols occurring in the translation:
% 0.76/1.22
% 0.76/1.22 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.76/1.22 . [1, 2] (w:1, o:80, a:1, s:1, b:0),
% 0.76/1.22 ! [4, 1] (w:0, o:60, a:1, s:1, b:0),
% 0.76/1.22 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.76/1.22 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.76/1.22 semiring_1 [36, 1] (w:1, o:66, a:1, s:1, b:0),
% 0.76/1.22 one_one [37, 1] (w:1, o:70, a:1, s:1, b:0),
% 0.76/1.22 ti [38, 2] (w:1, o:104, a:1, s:1, b:0),
% 0.76/1.22 comm_semiring_1 [41, 1] (w:1, o:73, a:1, s:1, b:0),
% 0.76/1.22 plus_plus [42, 3] (w:1, o:108, a:1, s:1, b:0),
% 0.76/1.22 monoid_mult [43, 1] (w:1, o:76, a:1, s:1, b:0),
% 0.76/1.22 times_times [44, 3] (w:1, o:109, a:1, s:1, b:0),
% 0.76/1.22 undefined [45, 1] (w:1, o:78, a:1, s:1, b:0),
% 0.76/1.22 int [46, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.76/1.22 zprime [47, 1] (w:1, o:79, a:1, s:1, b:0),
% 0.76/1.22 bit0 [48, 1] (w:1, o:71, a:1, s:1, b:0),
% 0.76/1.22 bit1 [49, 1] (w:1, o:72, a:1, s:1, b:0),
% 0.76/1.22 pls [50, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.76/1.22 number [51, 1] (w:1, o:67, a:1, s:1, b:0),
% 0.76/1.22 number_number_of [52, 2] (w:1, o:105, a:1, s:1, b:0),
% 0.76/1.22 linorder [53, 1] (w:1, o:74, a:1, s:1, b:0),
% 0.76/1.22 ord_less [54, 3] (w:1, o:106, a:1, s:1, b:0),
% 0.76/1.22 ord_less_eq [55, 3] (w:1, o:107, a:1, s:1, b:0),
% 0.76/1.22 power_power [56, 3] (w:1, o:110, a:1, s:1, b:0),
% 0.76/1.22 nat [57, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.76/1.22 twoSqu33214720sum2sq [58, 1] (w:1, o:77, a:1, s:1, b:0),
% 0.76/1.22 m [59, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.76/1.22 s [60, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.76/1.22 t [61, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.76/1.22 number_semiring [66, 1] (w:1, o:69, a:1, s:1, b:0),
% 0.76/1.22 number_ring [72, 1] (w:1, o:68, a:1, s:1, b:0),
% 0.76/1.22 linordered_idom [84, 1] (w:1, o:75, a:1, s:1, b:0),
% 0.76/1.22 ring_char_0 [100, 1] (w:1, o:65, a:1, s:1, b:0),
% 0.76/1.22 skol1 [106, 0] (w:1, o:22, a:1, s:1, b:1),
% 0.76/1.22 skol2 [107, 0] (w:1, o:23, a:1, s:1, b:1),
% 0.76/1.22 skol3 [108, 0] (w:1, o:24, a:1, s:1, b:1),
% 0.76/1.22 skol4 [109, 0] (w:1, o:25, a:1, s:1, b:1),
% 0.76/1.22 skol5 [110, 0] (w:1, o:26, a:1, s:1, b:1).
% 0.76/1.22
% 0.76/1.22
% 0.76/1.22 Starting Search:
% 0.76/1.22
% 0.76/1.22 *** allocated 15000 integers for clauses
% 0.76/1.22 *** allocated 22500 integers for clauses
% 0.76/1.22 *** allocated 33750 integers for clauses
% 0.76/1.22 *** allocated 15000 integers for termspace/termends
% 0.76/1.22 *** allocated 50625 integers for clauses
% 0.76/1.22 *** allocated 22500 integers for termspace/termends
% 0.76/1.22 *** allocated 75937 integers for clauses
% 0.76/1.22 Resimplifying inuse:
% 0.76/1.22 Done
% 0.76/1.22
% 0.76/1.22 *** allocated 33750 integers for termspace/termends
% 0.76/1.22 *** allocated 113905 integers for clauses
% 0.76/1.22 *** allocated 50625 integers for termspace/termends
% 0.76/1.22 *** allocated 170857 integers for clauses
% 0.76/1.22
% 0.76/1.22 Bliksems!, er is een bewijs:
% 0.76/1.22 % SZS status Theorem
% 0.76/1.22 % SZS output start Refutation
% 0.76/1.22
% 0.76/1.22 (33) {G0,W5,D3,L1,V0,M1} I { ord_less_eq( int, one_one( int ), t ) }.
% 0.76/1.22 (34) {G0,W36,D8,L2,V0,M2} I { ! one_one( int ) ==> t, plus_plus( int,
% 0.76/1.22 power_power( int, skol1, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.76/1.22 power_power( int, skol4, number_number_of( nat, bit0( bit1( pls ) ) ) ) )
% 0.76/1.22 ==> plus_plus( int, times_times( int, number_number_of( int, bit0( bit0
% 0.76/1.22 ( bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 (35) {G0,W37,D8,L2,V0,M2} I { ! ord_less( int, one_one( int ), t ),
% 0.76/1.22 plus_plus( int, power_power( int, skol2, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ), power_power( int, skol5, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ) ) ==> plus_plus( int, times_times( int,
% 0.76/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.76/1.22 ) }.
% 0.76/1.22 (53) {G0,W4,D2,L1,V1,M1} I { ord_less_eq( int, X, X ) }.
% 0.76/1.22 (56) {G0,W7,D2,L2,V2,M2} I { ! ord_less( int, X, Y ), ! X = Y }.
% 0.76/1.22 (57) {G0,W11,D2,L3,V2,M3} I { ! ord_less_eq( int, X, Y ), X = Y, ord_less(
% 0.76/1.22 int, X, Y ) }.
% 0.76/1.22 (130) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X }.
% 0.76/1.22 (162) {G1,W30,D7,L1,V2,M1} I;d(130) { ! plus_plus( int, power_power( int, X
% 0.76/1.22 , number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int, Y,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==> plus_plus( int,
% 0.76/1.22 times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 (737) {G2,W4,D3,L1,V0,M1} S(34);d(130);r(162) { ! one_one( int ) ==> t }.
% 0.76/1.22 (771) {G2,W5,D3,L1,V0,M1} S(35);d(130);r(162) { ! ord_less( int, one_one(
% 0.76/1.22 int ), t ) }.
% 0.76/1.22 (1733) {G3,W4,D3,L1,V0,M1} R(57,771);r(33) { one_one( int ) ==> t }.
% 0.76/1.22 (2032) {G4,W7,D2,L2,V1,M2} P(57,737);d(1733);d(1733);r(56) { ! X = t, !
% 0.76/1.22 ord_less_eq( int, X, t ) }.
% 0.76/1.22 (2219) {G5,W0,D0,L0,V0,M0} Q(2032);r(53) { }.
% 0.76/1.22
% 0.76/1.22
% 0.76/1.22 % SZS output end Refutation
% 0.76/1.22 found a proof!
% 0.76/1.22
% 0.76/1.22
% 0.76/1.22 Unprocessed initial clauses:
% 0.76/1.22
% 0.76/1.22 (2221) {G0,W9,D4,L2,V1,M2} { ! semiring_1( X ), ti( X, one_one( X ) ) =
% 0.76/1.22 one_one( X ) }.
% 0.76/1.22 (2222) {G0,W13,D4,L2,V3,M2} { ! comm_semiring_1( X ), plus_plus( X, ti( X
% 0.76/1.22 , Y ), Z ) = plus_plus( X, Y, Z ) }.
% 0.76/1.22 (2223) {G0,W13,D4,L2,V3,M2} { ! comm_semiring_1( X ), plus_plus( X, Y, ti
% 0.76/1.22 ( X, Z ) ) = plus_plus( X, Y, Z ) }.
% 0.76/1.22 (2224) {G0,W13,D4,L2,V3,M2} { ! comm_semiring_1( X ), ti( X, plus_plus( X
% 0.76/1.22 , Y, Z ) ) = plus_plus( X, Y, Z ) }.
% 0.76/1.22 (2225) {G0,W13,D4,L2,V3,M2} { ! monoid_mult( X ), times_times( X, ti( X, Y
% 0.76/1.22 ), Z ) = times_times( X, Y, Z ) }.
% 0.76/1.22 (2226) {G0,W13,D4,L2,V3,M2} { ! monoid_mult( X ), times_times( X, Y, ti( X
% 0.76/1.22 , Z ) ) = times_times( X, Y, Z ) }.
% 0.76/1.22 (2227) {G0,W13,D4,L2,V3,M2} { ! monoid_mult( X ), ti( X, times_times( X, Y
% 0.76/1.22 , Z ) ) = times_times( X, Y, Z ) }.
% 0.76/1.22 (2228) {G0,W7,D4,L1,V1,M1} { ti( X, undefined( X ) ) = undefined( X ) }.
% 0.76/1.22 (2229) {G0,W6,D3,L2,V1,M2} { ! zprime( ti( int, X ) ), zprime( X ) }.
% 0.76/1.22 (2230) {G0,W6,D3,L2,V1,M2} { ! zprime( X ), zprime( ti( int, X ) ) }.
% 0.76/1.22 (2231) {G0,W7,D4,L1,V1,M1} { bit0( ti( int, X ) ) = bit0( X ) }.
% 0.76/1.22 (2232) {G0,W7,D4,L1,V1,M1} { ti( int, bit0( X ) ) = bit0( X ) }.
% 0.76/1.22 (2233) {G0,W7,D4,L1,V1,M1} { bit1( ti( int, X ) ) = bit1( X ) }.
% 0.76/1.22 (2234) {G0,W7,D4,L1,V1,M1} { ti( int, bit1( X ) ) = bit1( X ) }.
% 0.76/1.22 (2235) {G0,W5,D3,L1,V0,M1} { ti( int, pls ) = pls }.
% 0.76/1.22 (2236) {G0,W11,D4,L2,V2,M2} { ! number( X ), number_number_of( X, ti( int
% 0.76/1.22 , Y ) ) = number_number_of( X, Y ) }.
% 0.76/1.22 (2237) {G0,W11,D4,L2,V2,M2} { ! number( X ), ti( X, number_number_of( X, Y
% 0.76/1.22 ) ) = number_number_of( X, Y ) }.
% 0.76/1.22 (2238) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.76/1.22 X, ti( X, Y ), Z ), ord_less( X, Y, Z ) }.
% 0.76/1.22 (2239) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.76/1.22 X, Y, Z ), ord_less( X, ti( X, Y ), Z ) }.
% 0.76/1.22 (2240) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.76/1.22 X, Y, ti( X, Z ) ), ord_less( X, Y, Z ) }.
% 0.76/1.22 (2241) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.76/1.22 X, Y, Z ), ord_less( X, Y, ti( X, Z ) ) }.
% 0.76/1.22 (2242) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.76/1.22 ord_less_eq( X, ti( X, Y ), Z ), ord_less_eq( X, Y, Z ) }.
% 0.76/1.22 (2243) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.76/1.22 ord_less_eq( X, Y, Z ), ord_less_eq( X, ti( X, Y ), Z ) }.
% 0.76/1.22 (2244) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.76/1.22 ord_less_eq( X, Y, ti( X, Z ) ), ord_less_eq( X, Y, Z ) }.
% 0.76/1.22 (2245) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.76/1.22 ord_less_eq( X, Y, Z ), ord_less_eq( X, Y, ti( X, Z ) ) }.
% 0.76/1.22 (2246) {G0,W13,D4,L2,V3,M2} { ! monoid_mult( X ), power_power( X, ti( X, Y
% 0.76/1.22 ), Z ) = power_power( X, Y, Z ) }.
% 0.76/1.22 (2247) {G0,W13,D4,L2,V3,M2} { ! monoid_mult( X ), power_power( X, Y, ti(
% 0.76/1.22 nat, Z ) ) = power_power( X, Y, Z ) }.
% 0.76/1.22 (2248) {G0,W13,D4,L2,V3,M2} { ! monoid_mult( X ), ti( X, power_power( X, Y
% 0.76/1.22 , Z ) ) = power_power( X, Y, Z ) }.
% 0.76/1.22 (2249) {G0,W6,D3,L2,V1,M2} { ! twoSqu33214720sum2sq( ti( int, X ) ),
% 0.76/1.22 twoSqu33214720sum2sq( X ) }.
% 0.76/1.22 (2250) {G0,W6,D3,L2,V1,M2} { ! twoSqu33214720sum2sq( X ),
% 0.76/1.22 twoSqu33214720sum2sq( ti( int, X ) ) }.
% 0.76/1.22 (2251) {G0,W5,D3,L1,V0,M1} { ti( int, m ) = m }.
% 0.76/1.22 (2252) {G0,W5,D3,L1,V0,M1} { ti( int, s ) = s }.
% 0.76/1.22 (2253) {G0,W5,D3,L1,V0,M1} { ti( int, t ) = t }.
% 0.76/1.22 (2254) {G0,W5,D3,L1,V0,M1} { ord_less_eq( int, one_one( int ), t ) }.
% 0.76/1.22 (2255) {G0,W36,D8,L2,V0,M2} { ! t = one_one( int ), plus_plus( int,
% 0.76/1.22 power_power( int, skol1, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.76/1.22 power_power( int, skol4, number_number_of( nat, bit0( bit1( pls ) ) ) ) )
% 0.76/1.22 = plus_plus( int, times_times( int, number_number_of( int, bit0( bit0(
% 0.76/1.22 bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 (2256) {G0,W37,D8,L2,V0,M2} { ! ord_less( int, one_one( int ), t ),
% 0.76/1.22 plus_plus( int, power_power( int, skol2, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ), power_power( int, skol5, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ) ) = plus_plus( int, times_times( int, number_number_of
% 0.76/1.22 ( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 (2257) {G0,W16,D8,L1,V0,M1} { ord_less( int, t, plus_plus( int,
% 0.76/1.22 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.76/1.22 ), one_one( int ) ) ) }.
% 0.76/1.22 (2258) {G0,W14,D8,L1,V0,M1} { zprime( plus_plus( int, times_times( int,
% 0.76/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.76/1.22 ) ) }.
% 0.76/1.22 (2259) {G0,W29,D9,L1,V0,M1} { plus_plus( int, power_power( int, s,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) =
% 0.76/1.22 times_times( int, plus_plus( int, times_times( int, number_number_of( int
% 0.76/1.22 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ), t ) }.
% 0.76/1.22 (2260) {G0,W17,D9,L1,V0,M1} { twoSqu33214720sum2sq( times_times( int,
% 0.76/1.22 plus_plus( int, times_times( int, number_number_of( int, bit0( bit0( bit1
% 0.76/1.22 ( pls ) ) ) ), m ), one_one( int ) ), t ) ) }.
% 0.76/1.22 (2261) {G0,W43,D9,L1,V2,M1} { power_power( int, plus_plus( int, X, Y ),
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ) = plus_plus( int,
% 0.76/1.22 plus_plus( int, power_power( int, X, number_number_of( nat, bit0( bit1(
% 0.76/1.22 pls ) ) ) ), times_times( int, times_times( int, number_number_of( int,
% 0.76/1.22 bit0( bit1( pls ) ) ), X ), Y ) ), power_power( int, Y, number_number_of
% 0.76/1.22 ( nat, bit0( bit1( pls ) ) ) ) ) }.
% 0.76/1.22 (2262) {G0,W70,D11,L1,V2,M1} { power_power( int, plus_plus( int, X, Y ),
% 0.76/1.22 number_number_of( nat, bit1( bit1( pls ) ) ) ) = plus_plus( int,
% 0.76/1.22 plus_plus( int, plus_plus( int, power_power( int, X, number_number_of(
% 0.76/1.22 nat, bit1( bit1( pls ) ) ) ), times_times( int, times_times( int,
% 0.76/1.22 number_number_of( int, bit1( bit1( pls ) ) ), power_power( int, X,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ) ), Y ) ), times_times( int
% 0.76/1.22 , times_times( int, number_number_of( int, bit1( bit1( pls ) ) ), X ),
% 0.76/1.22 power_power( int, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ),
% 0.76/1.22 power_power( int, Y, number_number_of( nat, bit1( bit1( pls ) ) ) ) ) }.
% 0.76/1.22 (2263) {G0,W45,D8,L2,V3,M2} { ! number_semiring( X ), power_power( X,
% 0.76/1.22 plus_plus( X, Y, Z ), number_number_of( nat, bit0( bit1( pls ) ) ) ) =
% 0.76/1.22 plus_plus( X, plus_plus( X, power_power( X, Y, number_number_of( nat,
% 0.76/1.22 bit0( bit1( pls ) ) ) ), power_power( X, Z, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ) ), times_times( X, times_times( X, number_number_of( X
% 0.76/1.22 , bit0( bit1( pls ) ) ), Y ), Z ) ) }.
% 0.76/1.22 (2264) {G0,W23,D6,L3,V2,M3} { ! monoid_mult( X ), ! number( X ),
% 0.76/1.22 power_power( X, number_number_of( X, Y ), number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ) = times_times( X, number_number_of( X, Y ),
% 0.76/1.22 number_number_of( X, Y ) ) }.
% 0.76/1.22 (2265) {G0,W20,D7,L1,V1,M1} { times_times( int, X, power_power( int, X,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = power_power( int, X,
% 0.76/1.22 number_number_of( nat, bit1( bit1( pls ) ) ) ) }.
% 0.76/1.22 (2266) {G0,W14,D6,L2,V1,M2} { ! semiring_1( X ), power_power( X, one_one(
% 0.76/1.22 X ), number_number_of( nat, bit0( bit1( pls ) ) ) ) = one_one( X ) }.
% 0.76/1.22 (2267) {G0,W15,D6,L2,V2,M2} { ! comm_semiring_1( X ), times_times( X, Y, Y
% 0.76/1.22 ) = power_power( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.76/1.22 }.
% 0.76/1.22 (2268) {G0,W15,D6,L2,V2,M2} { ! monoid_mult( X ), power_power( X, Y,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ) = times_times( X, Y, Y )
% 0.76/1.22 }.
% 0.76/1.22 (2269) {G0,W24,D7,L2,V3,M2} { ! comm_semiring_1( X ), power_power( X, Y,
% 0.76/1.22 times_times( nat, number_number_of( nat, bit0( bit1( pls ) ) ), Z ) ) =
% 0.76/1.22 times_times( X, power_power( X, Y, Z ), power_power( X, Y, Z ) ) }.
% 0.76/1.22 (2270) {G0,W17,D5,L2,V2,M2} { ! number_ring( X ), plus_plus( X, one_one( X
% 0.76/1.22 ), number_number_of( X, Y ) ) = number_number_of( X, plus_plus( int,
% 0.76/1.22 bit1( pls ), Y ) ) }.
% 0.76/1.22 (2271) {G0,W17,D5,L2,V2,M2} { ! number_ring( X ), plus_plus( X,
% 0.76/1.22 number_number_of( X, Y ), one_one( X ) ) = number_number_of( X, plus_plus
% 0.76/1.22 ( int, Y, bit1( pls ) ) ) }.
% 0.76/1.22 (2272) {G0,W14,D5,L2,V1,M2} { ! number_ring( X ), plus_plus( X, one_one( X
% 0.76/1.22 ), one_one( X ) ) = number_number_of( X, bit0( bit1( pls ) ) ) }.
% 0.76/1.22 (2273) {G0,W29,D9,L1,V0,M1} { plus_plus( int, power_power( int, s,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) =
% 0.76/1.22 times_times( int, plus_plus( int, times_times( int, number_number_of( int
% 0.76/1.22 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ), skol3 ) }.
% 0.76/1.22 (2274) {G0,W4,D2,L1,V1,M1} { ord_less_eq( int, X, X ) }.
% 0.76/1.22 (2275) {G0,W8,D2,L2,V2,M2} { ord_less_eq( int, X, Y ), ord_less_eq( int, Y
% 0.76/1.22 , X ) }.
% 0.76/1.22 (2276) {G0,W8,D2,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int, X
% 0.76/1.22 , Y ) }.
% 0.76/1.22 (2277) {G0,W7,D2,L2,V2,M2} { ! ord_less( int, X, Y ), ! X = Y }.
% 0.76/1.22 (2278) {G0,W11,D2,L3,V2,M3} { ! ord_less_eq( int, X, Y ), X = Y, ord_less
% 0.76/1.22 ( int, X, Y ) }.
% 0.76/1.22 (2279) {G0,W11,D2,L3,V2,M3} { ord_less( int, X, Y ), X = Y, ord_less( int
% 0.76/1.22 , Y, X ) }.
% 0.76/1.22 (2280) {G0,W12,D2,L3,V3,M3} { ! ord_less_eq( int, X, Y ), ! ord_less_eq(
% 0.76/1.22 int, Y, Z ), ord_less_eq( int, X, Z ) }.
% 0.76/1.22 (2281) {G0,W11,D2,L3,V2,M3} { ! ord_less_eq( int, X, Y ), ! ord_less_eq(
% 0.76/1.22 int, Y, X ), X = Y }.
% 0.76/1.22 (2282) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), power_power( X,
% 0.76/1.22 power_power( X, Y, Z ), T ) = power_power( X, Y, times_times( nat, Z, T )
% 0.76/1.22 ) }.
% 0.76/1.22 (2283) {G0,W11,D4,L2,V2,M2} { ! comm_semiring_1( X ), power_power( X, Y,
% 0.76/1.22 one_one( nat ) ) = ti( X, Y ) }.
% 0.76/1.22 (2284) {G0,W15,D4,L1,V3,M1} { power_power( int, power_power( int, X, Y ),
% 0.76/1.22 Z ) = power_power( int, X, times_times( nat, Y, Z ) ) }.
% 0.76/1.22 (2285) {G0,W20,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.76/1.22 ord_less_eq( X, number_number_of( X, Y ), number_number_of( X, Z ) ), !
% 0.76/1.22 ord_less( X, number_number_of( X, Z ), number_number_of( X, Y ) ) }.
% 0.76/1.22 (2286) {G0,W20,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ord_less( X
% 0.76/1.22 , number_number_of( X, Z ), number_number_of( X, Y ) ), ord_less_eq( X,
% 0.76/1.22 number_number_of( X, Y ), number_number_of( X, Z ) ) }.
% 0.76/1.22 (2287) {G0,W16,D3,L4,V3,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.76/1.22 ! ord_less( X, number_number_of( X, Y ), number_number_of( X, Z ) ),
% 0.76/1.22 ord_less( int, Y, Z ) }.
% 0.76/1.22 (2288) {G0,W16,D3,L4,V3,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.76/1.22 ! ord_less( int, Y, Z ), ord_less( X, number_number_of( X, Y ),
% 0.76/1.22 number_number_of( X, Z ) ) }.
% 0.76/1.22 (2289) {G0,W16,D3,L4,V3,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.76/1.22 ! ord_less_eq( X, number_number_of( X, Y ), number_number_of( X, Z ) ),
% 0.76/1.22 ord_less_eq( int, Y, Z ) }.
% 0.76/1.22 (2290) {G0,W16,D3,L4,V3,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.76/1.22 ! ord_less_eq( int, Y, Z ), ord_less_eq( X, number_number_of( X, Y ),
% 0.76/1.22 number_number_of( X, Z ) ) }.
% 0.76/1.22 (2291) {G0,W18,D3,L3,V4,M3} { ! ord_less( int, X, Y ), ! ord_less_eq( int
% 0.76/1.22 , Z, T ), ord_less( int, plus_plus( int, X, Z ), plus_plus( int, Y, T ) )
% 0.76/1.22 }.
% 0.76/1.22 (2292) {G0,W20,D4,L2,V4,M2} { ! comm_semiring_1( X ), times_times( X,
% 0.76/1.22 power_power( X, Y, Z ), power_power( X, Y, T ) ) = power_power( X, Y,
% 0.76/1.22 plus_plus( nat, Z, T ) ) }.
% 0.76/1.22 (2293) {G0,W18,D4,L1,V3,M1} { power_power( int, X, plus_plus( nat, Y, Z )
% 0.76/1.22 ) = times_times( int, power_power( int, X, Y ), power_power( int, X, Z )
% 0.76/1.22 ) }.
% 0.76/1.22 (2294) {G0,W13,D6,L1,V1,M1} { times_times( nat, number_number_of( nat,
% 0.76/1.22 bit0( bit1( pls ) ) ), X ) = plus_plus( nat, X, X ) }.
% 0.76/1.22 (2295) {G0,W13,D6,L1,V1,M1} { times_times( nat, X, number_number_of( nat,
% 0.76/1.22 bit0( bit1( pls ) ) ) ) = plus_plus( nat, X, X ) }.
% 0.76/1.22 (2296) {G0,W12,D5,L1,V0,M1} { plus_plus( nat, one_one( nat ), one_one( nat
% 0.76/1.22 ) ) = number_number_of( nat, bit0( bit1( pls ) ) ) }.
% 0.76/1.22 (2297) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit1( X ), bit1( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2298) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int, bit1
% 0.76/1.22 ( X ), bit1( Y ) ) }.
% 0.76/1.22 (2299) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit1( X ), bit1( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2300) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int, bit1
% 0.76/1.22 ( X ), bit1( Y ) ) }.
% 0.76/1.22 (2301) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit1( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2302) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , bit1( X ), bit1( Y ) ) }.
% 0.76/1.22 (2303) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit1( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2304) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , bit1( X ), bit1( Y ) ) }.
% 0.76/1.22 (2305) {G0,W4,D2,L1,V0,M1} { ! ord_less( int, pls, pls ) }.
% 0.76/1.22 (2306) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit0( X ), bit0( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2307) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int, bit0
% 0.76/1.22 ( X ), bit0( Y ) ) }.
% 0.76/1.22 (2308) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit0( X ), bit0( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2309) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int, bit0
% 0.76/1.22 ( X ), bit0( Y ) ) }.
% 0.76/1.22 (2310) {G0,W4,D2,L1,V0,M1} { ord_less_eq( int, pls, pls ) }.
% 0.76/1.22 (2311) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit0( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2312) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , bit0( X ), bit0( Y ) ) }.
% 0.76/1.22 (2313) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit0( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2314) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , bit0( X ), bit0( Y ) ) }.
% 0.76/1.22 (2315) {G0,W12,D3,L2,V2,M2} { ! ord_less( int, number_number_of( int, X )
% 0.76/1.22 , number_number_of( int, Y ) ), ord_less( int, X, Y ) }.
% 0.76/1.22 (2316) {G0,W12,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int,
% 0.76/1.22 number_number_of( int, X ), number_number_of( int, Y ) ) }.
% 0.76/1.22 (2317) {G0,W12,D3,L2,V2,M2} { ! ord_less_eq( int, number_number_of( int, X
% 0.76/1.22 ), number_number_of( int, Y ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2318) {G0,W12,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , number_number_of( int, X ), number_number_of( int, Y ) ) }.
% 0.76/1.22 (2319) {G0,W14,D3,L2,V3,M2} { ! ord_less( int, X, Y ), ord_less( int,
% 0.76/1.22 plus_plus( int, X, Z ), plus_plus( int, Y, Z ) ) }.
% 0.76/1.22 (2320) {G0,W14,D3,L2,V3,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , plus_plus( int, Z, X ), plus_plus( int, Z, Y ) ) }.
% 0.76/1.22 (2321) {G0,W16,D4,L2,V2,M2} { ! ord_less( int, Y, pls ), plus_plus( nat,
% 0.76/1.22 number_number_of( nat, Y ), number_number_of( nat, X ) ) =
% 0.76/1.22 number_number_of( nat, X ) }.
% 0.76/1.22 (2322) {G0,W20,D4,L3,V2,M3} { ord_less( int, Y, pls ), ! ord_less( int, X
% 0.76/1.22 , pls ), plus_plus( nat, number_number_of( nat, Y ), number_number_of(
% 0.76/1.22 nat, X ) ) = number_number_of( nat, Y ) }.
% 0.76/1.22 (2323) {G0,W23,D4,L3,V2,M3} { ord_less( int, Y, pls ), ord_less( int, X,
% 0.76/1.22 pls ), plus_plus( nat, number_number_of( nat, Y ), number_number_of( nat
% 0.76/1.22 , X ) ) = number_number_of( nat, plus_plus( int, Y, X ) ) }.
% 0.76/1.22 (2324) {G0,W7,D4,L1,V0,M1} { number_number_of( nat, bit1( pls ) ) =
% 0.76/1.22 one_one( nat ) }.
% 0.76/1.22 (2325) {G0,W7,D4,L1,V0,M1} { one_one( nat ) = number_number_of( nat, bit1
% 0.76/1.22 ( pls ) ) }.
% 0.76/1.22 (2326) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, bit1( X ), pls ),
% 0.76/1.22 ord_less( int, X, pls ) }.
% 0.76/1.22 (2327) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, X, pls ), ord_less_eq( int,
% 0.76/1.22 bit1( X ), pls ) }.
% 0.76/1.22 (2328) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, pls, bit1( X ) ),
% 0.76/1.22 ord_less_eq( int, pls, X ) }.
% 0.76/1.22 (2329) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, X ), ord_less( int,
% 0.76/1.22 pls, bit1( X ) ) }.
% 0.76/1.22 (2330) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit0( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2331) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.76/1.22 bit1( X ), bit0( Y ) ) }.
% 0.76/1.22 (2332) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit0( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2333) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.76/1.22 bit1( X ), bit0( Y ) ) }.
% 0.76/1.22 (2334) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit0( X ), bit1( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2335) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less( int,
% 0.76/1.22 bit0( X ), bit1( Y ) ) }.
% 0.76/1.22 (2336) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit0( X ), bit1( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2337) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less( int,
% 0.76/1.22 bit0( X ), bit1( Y ) ) }.
% 0.76/1.22 (2338) {G0,W12,D4,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.76/1.22 plus_plus( int, X, one_one( int ) ), Y ) }.
% 0.76/1.22 (2339) {G0,W12,D4,L2,V2,M2} { ! ord_less_eq( int, plus_plus( int, X,
% 0.76/1.22 one_one( int ) ), Y ), ord_less( int, X, Y ) }.
% 0.76/1.22 (2340) {G0,W12,D4,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.76/1.22 plus_plus( int, X, one_one( int ) ), Y ) }.
% 0.76/1.22 (2341) {G0,W12,D4,L2,V2,M2} { ! ord_less( int, X, plus_plus( int, Y,
% 0.76/1.22 one_one( int ) ) ), ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2342) {G0,W12,D4,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less( int, X
% 0.76/1.22 , plus_plus( int, Y, one_one( int ) ) ) }.
% 0.76/1.22 (2343) {G0,W6,D5,L1,V0,M1} { zprime( number_number_of( int, bit0( bit1(
% 0.76/1.22 pls ) ) ) ) }.
% 0.76/1.22 (2344) {G0,W9,D3,L3,V2,M3} { ! twoSqu33214720sum2sq( X ), !
% 0.76/1.22 twoSqu33214720sum2sq( Y ), twoSqu33214720sum2sq( times_times( int, X, Y )
% 0.76/1.22 ) }.
% 0.76/1.22 (2345) {G0,W23,D4,L2,V5,M2} { ! comm_semiring_1( X ), times_times( X,
% 0.76/1.22 times_times( X, Y, Z ), times_times( X, T, U ) ) = times_times( X,
% 0.76/1.22 times_times( X, Y, T ), times_times( X, Z, U ) ) }.
% 0.76/1.22 (2346) {G0,W23,D5,L2,V5,M2} { ! comm_semiring_1( X ), times_times( X,
% 0.76/1.22 times_times( X, Y, Z ), times_times( X, T, U ) ) = times_times( X, T,
% 0.76/1.22 times_times( X, times_times( X, Y, Z ), U ) ) }.
% 0.76/1.22 (2347) {G0,W23,D5,L2,V5,M2} { ! comm_semiring_1( X ), times_times( X,
% 0.76/1.22 times_times( X, Y, Z ), times_times( X, T, U ) ) = times_times( X, Y,
% 0.76/1.22 times_times( X, Z, times_times( X, T, U ) ) ) }.
% 0.76/1.22 (2348) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), times_times( X,
% 0.76/1.22 times_times( X, Y, Z ), T ) = times_times( X, times_times( X, Y, T ), Z )
% 0.76/1.22 }.
% 0.76/1.22 (2349) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), times_times( X,
% 0.76/1.22 times_times( X, Y, Z ), T ) = times_times( X, Y, times_times( X, Z, T ) )
% 0.76/1.22 }.
% 0.76/1.22 (2350) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), times_times( X, Y,
% 0.76/1.22 times_times( X, Z, T ) ) = times_times( X, times_times( X, Y, Z ), T )
% 0.76/1.22 }.
% 0.76/1.22 (2351) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), times_times( X, Y,
% 0.76/1.22 times_times( X, Z, T ) ) = times_times( X, Z, times_times( X, Y, T ) )
% 0.76/1.22 }.
% 0.76/1.22 (2352) {G0,W11,D3,L2,V3,M2} { ! comm_semiring_1( X ), times_times( X, Y, Z
% 0.76/1.22 ) = times_times( X, Z, Y ) }.
% 0.76/1.22 (2353) {G0,W23,D4,L2,V5,M2} { ! comm_semiring_1( X ), plus_plus( X,
% 0.76/1.22 plus_plus( X, Y, Z ), plus_plus( X, T, U ) ) = plus_plus( X, plus_plus( X
% 0.76/1.22 , Y, T ), plus_plus( X, Z, U ) ) }.
% 0.76/1.22 (2354) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), plus_plus( X,
% 0.76/1.22 plus_plus( X, Y, Z ), T ) = plus_plus( X, plus_plus( X, Y, T ), Z ) }.
% 0.76/1.22 (2355) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), plus_plus( X,
% 0.76/1.22 plus_plus( X, Y, Z ), T ) = plus_plus( X, Y, plus_plus( X, Z, T ) ) }.
% 0.76/1.22 (2356) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), plus_plus( X, Y,
% 0.76/1.22 plus_plus( X, Z, T ) ) = plus_plus( X, plus_plus( X, Y, Z ), T ) }.
% 0.76/1.22 (2357) {G0,W17,D4,L2,V4,M2} { ! comm_semiring_1( X ), plus_plus( X, Y,
% 0.76/1.22 plus_plus( X, Z, T ) ) = plus_plus( X, Z, plus_plus( X, Y, T ) ) }.
% 0.76/1.22 (2358) {G0,W11,D3,L2,V3,M2} { ! comm_semiring_1( X ), plus_plus( X, Y, Z )
% 0.76/1.22 = plus_plus( X, Z, Y ) }.
% 0.76/1.22 (2359) {G0,W14,D3,L4,V3,M4} { ! number_ring( X ), ! ring_char_0( X ), !
% 0.76/1.22 number_number_of( X, Y ) = number_number_of( X, Z ), Y = Z }.
% 0.76/1.22 (2360) {G0,W14,D3,L4,V3,M4} { ! number_ring( X ), ! ring_char_0( X ), ! Y
% 0.76/1.22 = Z, number_number_of( X, Y ) = number_number_of( X, Z ) }.
% 0.76/1.22 (2361) {G0,W16,D3,L3,V3,M3} { ! number( X ), ! number_number_of( X, Y ) =
% 0.76/1.22 ti( X, Z ), ti( X, Z ) = number_number_of( X, Y ) }.
% 0.76/1.22 (2362) {G0,W16,D3,L3,V3,M3} { ! number( X ), ! ti( X, Z ) =
% 0.76/1.22 number_number_of( X, Y ), number_number_of( X, Y ) = ti( X, Z ) }.
% 0.76/1.22 (2363) {G0,W8,D3,L2,V2,M2} { ! bit1( X ) = bit1( Y ), X = Y }.
% 0.76/1.22 (2364) {G0,W8,D3,L2,V2,M2} { ! X = Y, bit1( X ) = bit1( Y ) }.
% 0.76/1.22 (2365) {G0,W8,D3,L2,V2,M2} { ! bit0( X ) = bit0( Y ), X = Y }.
% 0.76/1.22 (2366) {G0,W8,D3,L2,V2,M2} { ! X = Y, bit0( X ) = bit0( Y ) }.
% 0.76/1.22 (2367) {G0,W15,D4,L1,V3,M1} { times_times( int, times_times( int, X, Y ),
% 0.76/1.22 Z ) = times_times( int, X, times_times( int, Y, Z ) ) }.
% 0.76/1.22 (2368) {G0,W9,D3,L1,V2,M1} { times_times( int, X, Y ) = times_times( int,
% 0.76/1.22 Y, X ) }.
% 0.76/1.22 (2369) {G0,W5,D3,L1,V1,M1} { number_number_of( int, X ) = X }.
% 0.76/1.22 (2370) {G0,W15,D4,L1,V3,M1} { plus_plus( int, plus_plus( int, X, Y ), Z )
% 0.76/1.22 = plus_plus( int, X, plus_plus( int, Y, Z ) ) }.
% 0.76/1.22 (2371) {G0,W15,D4,L1,V3,M1} { plus_plus( int, X, plus_plus( int, Y, Z ) )
% 0.76/1.22 = plus_plus( int, Y, plus_plus( int, X, Z ) ) }.
% 0.76/1.22 (2372) {G0,W9,D3,L1,V2,M1} { plus_plus( int, X, Y ) = plus_plus( int, Y, X
% 0.76/1.22 ) }.
% 0.76/1.22 (2373) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, bit1( X ), pls ), ord_less(
% 0.76/1.22 int, X, pls ) }.
% 0.76/1.22 (2374) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, X, pls ), ord_less( int,
% 0.76/1.22 bit1( X ), pls ) }.
% 0.76/1.22 (2375) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit1( X ), bit0( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2376) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int, bit1
% 0.76/1.22 ( X ), bit0( Y ) ) }.
% 0.76/1.22 (2377) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit1( X ), bit0( Y ) ),
% 0.76/1.22 ord_less( int, X, Y ) }.
% 0.76/1.22 (2378) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int, bit1
% 0.76/1.22 ( X ), bit0( Y ) ) }.
% 0.76/1.22 (2379) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, bit0( X ), pls ), ord_less(
% 0.76/1.22 int, X, pls ) }.
% 0.76/1.22 (2380) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, X, pls ), ord_less( int,
% 0.76/1.22 bit0( X ), pls ) }.
% 0.76/1.22 (2381) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, pls, bit0( X ) ), ord_less(
% 0.76/1.22 int, pls, X ) }.
% 0.76/1.22 (2382) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, pls, X ), ord_less( int, pls
% 0.76/1.22 , bit0( X ) ) }.
% 0.76/1.22 (2383) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, bit1( X ) ),
% 0.76/1.22 ord_less_eq( int, pls, X ) }.
% 0.76/1.22 (2384) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, X ), ord_less_eq(
% 0.76/1.22 int, pls, bit1( X ) ) }.
% 0.76/1.22 (2385) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit1( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2386) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , bit0( X ), bit1( Y ) ) }.
% 0.76/1.22 (2387) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit1( Y ) ),
% 0.76/1.22 ord_less_eq( int, X, Y ) }.
% 0.76/1.22 (2388) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.76/1.22 , bit0( X ), bit1( Y ) ) }.
% 0.76/1.22 (2389) {G0,W2,D2,L1,V0,M1} { linordered_idom( int ) }.
% 0.76/1.22 (2390) {G0,W2,D2,L1,V0,M1} { comm_semiring_1( int ) }.
% 0.76/1.22 (2391) {G0,W2,D2,L1,V0,M1} { number_semiring( int ) }.
% 0.76/1.22 (2392) {G0,W2,D2,L1,V0,M1} { linorder( int ) }.
% 0.76/1.22 (2393) {G0,W2,D2,L1,V0,M1} { monoid_mult( int ) }.
% 0.76/1.22 (2394) {G0,W2,D2,L1,V0,M1} { semiring_1( int ) }.
% 0.76/1.22 (2395) {G0,W2,D2,L1,V0,M1} { ring_char_0( int ) }.
% 0.76/1.22 (2396) {G0,W2,D2,L1,V0,M1} { number_ring( int ) }.
% 0.76/1.22 (2397) {G0,W2,D2,L1,V0,M1} { number( int ) }.
% 0.76/1.22 (2398) {G0,W2,D2,L1,V0,M1} { comm_semiring_1( nat ) }.
% 0.76/1.22 (2399) {G0,W2,D2,L1,V0,M1} { number_semiring( nat ) }.
% 0.76/1.22 (2400) {G0,W2,D2,L1,V0,M1} { linorder( nat ) }.
% 0.76/1.22 (2401) {G0,W2,D2,L1,V0,M1} { monoid_mult( nat ) }.
% 0.76/1.22 (2402) {G0,W2,D2,L1,V0,M1} { semiring_1( nat ) }.
% 0.76/1.22 (2403) {G0,W2,D2,L1,V0,M1} { number( nat ) }.
% 0.76/1.22 (2404) {G0,W9,D4,L1,V2,M1} { ti( X, ti( X, Y ) ) = ti( X, Y ) }.
% 0.76/1.22 (2405) {G0,W32,D8,L1,V2,M1} { ! plus_plus( int, power_power( int, X,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int, Y,
% 0.76/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = plus_plus( int,
% 0.76/1.22 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.76/1.22 ), one_one( int ) ) }.
% 0.76/1.22
% 0.76/1.22
% 0.76/1.22 Total Proof:
% 0.76/1.22
% 0.76/1.22 subsumption: (33) {G0,W5,D3,L1,V0,M1} I { ord_less_eq( int, one_one( int )
% 0.76/1.22 , t ) }.
% 0.76/1.22 parent0: (2254) {G0,W5,D3,L1,V0,M1} { ord_less_eq( int, one_one( int ), t
% 0.76/1.22 ) }.
% 0.76/1.22 substitution0:
% 0.76/1.22 end
% 0.76/1.22 permutation0:
% 0.76/1.22 0 ==> 0
% 0.76/1.22 end
% 0.76/1.22
% 0.76/1.22 eqswap: (2448) {G0,W36,D8,L2,V0,M2} { ! one_one( int ) = t, plus_plus( int
% 0.76/1.22 , power_power( int, skol1, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.76/1.22 , power_power( int, skol4, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.76/1.22 ) = plus_plus( int, times_times( int, number_number_of( int, bit0( bit0
% 0.76/1.22 ( bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 parent0[0]: (2255) {G0,W36,D8,L2,V0,M2} { ! t = one_one( int ), plus_plus
% 0.76/1.22 ( int, power_power( int, skol1, number_number_of( nat, bit0( bit1( pls )
% 0.76/1.22 ) ) ), power_power( int, skol4, number_number_of( nat, bit0( bit1( pls )
% 0.76/1.22 ) ) ) ) = plus_plus( int, times_times( int, number_number_of( int, bit0
% 0.76/1.22 ( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 substitution0:
% 0.76/1.22 end
% 0.76/1.22
% 0.76/1.22 subsumption: (34) {G0,W36,D8,L2,V0,M2} I { ! one_one( int ) ==> t,
% 0.76/1.22 plus_plus( int, power_power( int, skol1, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ), power_power( int, skol4, number_number_of( nat, bit0(
% 0.76/1.22 bit1( pls ) ) ) ) ) ==> plus_plus( int, times_times( int,
% 0.76/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.76/1.22 ) }.
% 0.76/1.22 parent0: (2448) {G0,W36,D8,L2,V0,M2} { ! one_one( int ) = t, plus_plus(
% 0.76/1.22 int, power_power( int, skol1, number_number_of( nat, bit0( bit1( pls ) )
% 0.76/1.22 ) ), power_power( int, skol4, number_number_of( nat, bit0( bit1( pls ) )
% 0.76/1.22 ) ) ) = plus_plus( int, times_times( int, number_number_of( int, bit0(
% 0.76/1.22 bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.22 substitution0:
% 0.76/1.22 end
% 0.76/1.22 permutation0:
% 0.76/1.22 0 ==> 0
% 0.76/1.22 1 ==> 1
% 0.76/1.22 end
% 0.76/1.22
% 0.76/1.22 subsumption: (35) {G0,W37,D8,L2,V0,M2} I { ! ord_less( int, one_one( int )
% 0.76/1.22 , t ), plus_plus( int, power_power( int, skol2, number_number_of( nat,
% 0.76/1.22 bit0( bit1( pls ) ) ) ), power_power( int, skol5, number_number_of( nat,
% 0.76/1.22 bit0( bit1( pls ) ) ) ) ) ==> plus_plus( int, times_times( int,
% 0.76/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.76/1.22 ) }.
% 0.76/1.22 parent0: (2256) {G0,W37,D8,L2,V0,M2} { ! ord_less( int, one_one( int ), t
% 0.76/1.22 ), plus_plus( int, power_power( int, skol2, number_number_of( nat, bit0
% 0.76/1.22 ( bit1( pls ) ) ) ), power_power( int, skol5, number_number_of( nat, bit0
% 0.76/1.22 ( bit1( pls ) ) ) ) ) = plus_plus( int, times_times( int,
% 0.76/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.76/1.22 ) }.
% 0.76/1.22 substitution0:
% 0.76/1.22 end
% 0.76/1.22 permutation0:
% 0.76/1.22 0 ==> 0
% 0.76/1.22 1 ==> 1
% 0.76/1.22 end
% 0.76/1.22
% 0.76/1.22 subsumption: (53) {G0,W4,D2,L1,V1,M1} I { ord_less_eq( int, X, X ) }.
% 0.76/1.22 parent0: (2274) {G0,W4,D2,L1,V1,M1} { ord_less_eq( int, X, X ) }.
% 0.76/1.22 substitution0:
% 0.76/1.22 X := X
% 0.76/1.22 end
% 0.76/1.22 permutation0:
% 0.76/1.22 0 ==> 0
% 0.76/1.22 end
% 0.76/1.22
% 0.76/1.22 subsumption: (56) {G0,W7,D2,L2,V2,M2} I { ! ord_less( int, X, Y ), ! X = Y
% 0.76/1.22 }.
% 0.76/1.22 parent0: (2277) {G0,W7,D2,L2,V2,M2} { ! ord_less( int, X, Y ), ! X = Y }.
% 0.76/1.22 substitution0:
% 0.76/1.22 X := X
% 0.76/1.23 Y := Y
% 0.76/1.23 end
% 0.76/1.23 permutation0:
% 0.76/1.23 0 ==> 0
% 0.76/1.23 1 ==> 1
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 subsumption: (57) {G0,W11,D2,L3,V2,M3} I { ! ord_less_eq( int, X, Y ), X =
% 0.76/1.23 Y, ord_less( int, X, Y ) }.
% 0.76/1.23 parent0: (2278) {G0,W11,D2,L3,V2,M3} { ! ord_less_eq( int, X, Y ), X = Y,
% 0.76/1.23 ord_less( int, X, Y ) }.
% 0.76/1.23 substitution0:
% 0.76/1.23 X := X
% 0.76/1.23 Y := Y
% 0.76/1.23 end
% 0.76/1.23 permutation0:
% 0.76/1.23 0 ==> 0
% 0.76/1.23 1 ==> 1
% 0.76/1.23 2 ==> 2
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 subsumption: (130) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 0.76/1.23 }.
% 0.76/1.23 parent0: (2369) {G0,W5,D3,L1,V1,M1} { number_number_of( int, X ) = X }.
% 0.76/1.23 substitution0:
% 0.76/1.23 X := X
% 0.76/1.23 end
% 0.76/1.23 permutation0:
% 0.76/1.23 0 ==> 0
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 *** allocated 75937 integers for termspace/termends
% 0.76/1.23 paramod: (3010) {G1,W30,D7,L1,V2,M1} { ! plus_plus( int, power_power( int
% 0.76/1.23 , X, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int, Y
% 0.76/1.23 , number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = plus_plus( int,
% 0.76/1.23 times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) ) }.
% 0.76/1.23 parent0[0]: (130) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 0.76/1.23 }.
% 0.76/1.23 parent1[0; 24]: (2405) {G0,W32,D8,L1,V2,M1} { ! plus_plus( int,
% 0.76/1.23 power_power( int, X, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.76/1.23 power_power( int, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) =
% 0.76/1.23 plus_plus( int, times_times( int, number_number_of( int, bit0( bit0( bit1
% 0.76/1.23 ( pls ) ) ) ), m ), one_one( int ) ) }.
% 0.76/1.23 substitution0:
% 0.76/1.23 X := bit0( bit0( bit1( pls ) ) )
% 0.76/1.23 end
% 0.76/1.23 substitution1:
% 0.76/1.23 X := X
% 0.76/1.23 Y := Y
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 subsumption: (162) {G1,W30,D7,L1,V2,M1} I;d(130) { ! plus_plus( int,
% 0.76/1.23 power_power( int, X, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.76/1.23 power_power( int, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==>
% 0.76/1.23 plus_plus( int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ),
% 0.76/1.23 one_one( int ) ) }.
% 0.76/1.23 parent0: (3010) {G1,W30,D7,L1,V2,M1} { ! plus_plus( int, power_power( int
% 0.76/1.23 , X, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int, Y
% 0.76/1.23 , number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = plus_plus( int,
% 0.76/1.23 times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) ) }.
% 0.76/1.23 substitution0:
% 0.76/1.23 X := X
% 0.76/1.23 Y := Y
% 0.76/1.23 end
% 0.76/1.23 permutation0:
% 0.76/1.23 0 ==> 0
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 paramod: (3017) {G1,W34,D7,L2,V0,M2} { plus_plus( int, power_power( int,
% 0.76/1.23 skol1, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int,
% 0.76/1.23 skol4, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==> plus_plus(
% 0.76/1.23 int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) )
% 0.76/1.23 , ! one_one( int ) ==> t }.
% 0.76/1.23 parent0[0]: (130) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 0.76/1.23 }.
% 0.76/1.23 parent1[1; 23]: (34) {G0,W36,D8,L2,V0,M2} I { ! one_one( int ) ==> t,
% 0.76/1.23 plus_plus( int, power_power( int, skol1, number_number_of( nat, bit0(
% 0.76/1.23 bit1( pls ) ) ) ), power_power( int, skol4, number_number_of( nat, bit0(
% 0.76/1.23 bit1( pls ) ) ) ) ) ==> plus_plus( int, times_times( int,
% 0.76/1.23 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.76/1.23 ) }.
% 0.76/1.23 substitution0:
% 0.76/1.23 X := bit0( bit0( bit1( pls ) ) )
% 0.76/1.23 end
% 0.76/1.23 substitution1:
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 resolution: (3018) {G2,W4,D3,L1,V0,M1} { ! one_one( int ) ==> t }.
% 0.76/1.23 parent0[0]: (162) {G1,W30,D7,L1,V2,M1} I;d(130) { ! plus_plus( int,
% 0.76/1.23 power_power( int, X, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.76/1.23 power_power( int, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==>
% 0.76/1.23 plus_plus( int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ),
% 0.76/1.23 one_one( int ) ) }.
% 0.76/1.23 parent1[0]: (3017) {G1,W34,D7,L2,V0,M2} { plus_plus( int, power_power( int
% 0.76/1.23 , skol1, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int
% 0.76/1.23 , skol4, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==> plus_plus(
% 0.76/1.23 int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) )
% 0.76/1.23 , ! one_one( int ) ==> t }.
% 0.76/1.23 substitution0:
% 0.76/1.23 X := skol1
% 0.76/1.23 Y := skol4
% 0.76/1.23 end
% 0.76/1.23 substitution1:
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 subsumption: (737) {G2,W4,D3,L1,V0,M1} S(34);d(130);r(162) { ! one_one( int
% 0.76/1.23 ) ==> t }.
% 0.76/1.23 parent0: (3018) {G2,W4,D3,L1,V0,M1} { ! one_one( int ) ==> t }.
% 0.76/1.23 substitution0:
% 0.76/1.23 end
% 0.76/1.23 permutation0:
% 0.76/1.23 0 ==> 0
% 0.76/1.23 end
% 0.76/1.23
% 0.76/1.23 paramod: (3023) {G1,W35,D7,L2,V0,M2} { plus_plus( int, power_power( int,
% 0.76/1.23 skol2, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int,
% 0.76/1.23 skol5, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==> plus_plus(
% 75.94/76.39 int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) )
% 75.94/76.39 , ! ord_less( int, one_one( int ), t ) }.
% 75.94/76.39 parent0[0]: (130) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 75.94/76.39 }.
% 75.94/76.39 parent1[1; 23]: (35) {G0,W37,D8,L2,V0,M2} I { ! ord_less( int, one_one( int
% 75.94/76.39 ), t ), plus_plus( int, power_power( int, skol2, number_number_of( nat,
% 75.94/76.39 bit0( bit1( pls ) ) ) ), power_power( int, skol5, number_number_of( nat,
% 75.94/76.39 bit0( bit1( pls ) ) ) ) ) ==> plus_plus( int, times_times( int,
% 75.94/76.39 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 75.94/76.39 ) }.
% 75.94/76.39 substitution0:
% 75.94/76.39 X := bit0( bit0( bit1( pls ) ) )
% 75.94/76.39 end
% 75.94/76.39 substitution1:
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 resolution: (3024) {G2,W5,D3,L1,V0,M1} { ! ord_less( int, one_one( int ),
% 75.94/76.39 t ) }.
% 75.94/76.39 parent0[0]: (162) {G1,W30,D7,L1,V2,M1} I;d(130) { ! plus_plus( int,
% 75.94/76.39 power_power( int, X, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 75.94/76.39 power_power( int, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==>
% 75.94/76.39 plus_plus( int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ),
% 75.94/76.39 one_one( int ) ) }.
% 75.94/76.39 parent1[0]: (3023) {G1,W35,D7,L2,V0,M2} { plus_plus( int, power_power( int
% 75.94/76.39 , skol2, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( int
% 75.94/76.39 , skol5, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ==> plus_plus(
% 75.94/76.39 int, times_times( int, bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) )
% 75.94/76.39 , ! ord_less( int, one_one( int ), t ) }.
% 75.94/76.39 substitution0:
% 75.94/76.39 X := skol2
% 75.94/76.39 Y := skol5
% 75.94/76.39 end
% 75.94/76.39 substitution1:
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 subsumption: (771) {G2,W5,D3,L1,V0,M1} S(35);d(130);r(162) { ! ord_less(
% 75.94/76.39 int, one_one( int ), t ) }.
% 75.94/76.39 parent0: (3024) {G2,W5,D3,L1,V0,M1} { ! ord_less( int, one_one( int ), t )
% 75.94/76.39 }.
% 75.94/76.39 substitution0:
% 75.94/76.39 end
% 75.94/76.39 permutation0:
% 75.94/76.39 0 ==> 0
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 eqswap: (3025) {G0,W11,D2,L3,V2,M3} { Y = X, ! ord_less_eq( int, X, Y ),
% 75.94/76.39 ord_less( int, X, Y ) }.
% 75.94/76.39 parent0[1]: (57) {G0,W11,D2,L3,V2,M3} I { ! ord_less_eq( int, X, Y ), X = Y
% 75.94/76.39 , ord_less( int, X, Y ) }.
% 75.94/76.39 substitution0:
% 75.94/76.39 X := X
% 75.94/76.39 Y := Y
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 resolution: (3026) {G1,W9,D3,L2,V0,M2} { t = one_one( int ), ! ord_less_eq
% 75.94/76.39 ( int, one_one( int ), t ) }.
% 75.94/76.39 parent0[0]: (771) {G2,W5,D3,L1,V0,M1} S(35);d(130);r(162) { ! ord_less( int
% 75.94/76.39 , one_one( int ), t ) }.
% 75.94/76.39 parent1[2]: (3025) {G0,W11,D2,L3,V2,M3} { Y = X, ! ord_less_eq( int, X, Y
% 75.94/76.39 ), ord_less( int, X, Y ) }.
% 75.94/76.39 substitution0:
% 75.94/76.39 end
% 75.94/76.39 substitution1:
% 75.94/76.39 X := one_one( int )
% 75.94/76.39 Y := t
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 resolution: (3027) {G1,W4,D3,L1,V0,M1} { t = one_one( int ) }.
% 75.94/76.39 parent0[1]: (3026) {G1,W9,D3,L2,V0,M2} { t = one_one( int ), ! ord_less_eq
% 75.94/76.39 ( int, one_one( int ), t ) }.
% 75.94/76.39 parent1[0]: (33) {G0,W5,D3,L1,V0,M1} I { ord_less_eq( int, one_one( int ),
% 75.94/76.39 t ) }.
% 75.94/76.39 substitution0:
% 75.94/76.39 end
% 75.94/76.39 substitution1:
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 eqswap: (3028) {G1,W4,D3,L1,V0,M1} { one_one( int ) = t }.
% 75.94/76.39 parent0[0]: (3027) {G1,W4,D3,L1,V0,M1} { t = one_one( int ) }.
% 75.94/76.39 substitution0:
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 subsumption: (1733) {G3,W4,D3,L1,V0,M1} R(57,771);r(33) { one_one( int )
% 75.94/76.39 ==> t }.
% 75.94/76.39 parent0: (3028) {G1,W4,D3,L1,V0,M1} { one_one( int ) = t }.
% 75.94/76.39 substitution0:
% 75.94/76.39 end
% 75.94/76.39 permutation0:
% 75.94/76.39 0 ==> 0
% 75.94/76.39 end
% 75.94/76.39
% 75.94/76.39 *** allocated 15000 integers for justifications
% 75.94/76.39 *** allocated 113905 integers for termspace/termends
% 75.94/76.39 *** allocated 22500 integers for justifications
% 75.94/76.39 *** allocated 33750 integers for justifications
% 75.94/76.39 *** allocated 256285 integers for clauses
% 75.94/76.39 *** allocated 170857 integers for termspace/termends
% 75.94/76.39 *** allocated 50625 integers for justifications
% 75.94/76.39 *** allocated 75937 integers for justifications
% 75.94/76.39 *** allocated 256285 integers for termspace/termends
% 75.94/76.39 *** allocated 113905 integers for justifications
% 75.94/76.39 *** allocated 384427 integers for clauses
% 75.94/76.39 *** allocated 384427 integers for termspace/termends
% 75.94/76.39 *** allocated 170857 integers for justifications
% 75.94/76.39 *** allocated 576640 integers for termspace/termends
% 75.94/76.39 *** allocated 256285 integers for justifications
% 75.94/76.39 *** allocated 576640 integers for clauses
% 75.94/76.39 *** allocated 864960 integers for termspace/termends
% 75.94/76.39 *** allocated 384427 integers for justifications
% 75.94/76.39 *** allocated 864960 integers for clauses
% 75.94/76.39 *** allocated 1297440 integers for termspace/termends
% 75.94/76.39 *** allocated 576640 integers for justifications
% 75.94/76.39 *** allocated 864960 integersCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------