%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM924+5 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n006.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:37 EDT 2022
% Result : Theorem 0.81s 1.21s
% Output : Refutation 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.11 % Problem : NUM924+5 : TPTP v8.1.0. Released v5.3.0.
% 0.04/0.12 % Command : bliksem %s
% 0.12/0.32 % Computer : n006.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % DateTime : Wed Jul 6 21:27:06 EDT 2022
% 0.12/0.32 % CPUTime :
% 0.79/1.17 *** allocated 10000 integers for termspace/termends
% 0.79/1.17 *** allocated 10000 integers for clauses
% 0.79/1.17 *** allocated 10000 integers for justifications
% 0.79/1.17 Bliksem 1.12
% 0.79/1.17
% 0.79/1.17
% 0.79/1.17 Automatic Strategy Selection
% 0.79/1.17
% 0.79/1.17 *** allocated 15000 integers for termspace/termends
% 0.79/1.17
% 0.79/1.17 Clauses:
% 0.79/1.17
% 0.79/1.17 { ! semiring_1( X ), ti( X, one_one( X ) ) = one_one( X ) }.
% 0.79/1.17 { ! number( X ), ! semiring( X ), plus_plus( X, ti( X, Y ), Z ) = plus_plus
% 0.79/1.17 ( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! semiring( X ), plus_plus( X, Y, ti( X, Z ) ) = plus_plus
% 0.79/1.17 ( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! semiring( X ), ti( X, plus_plus( X, Y, Z ) ) = plus_plus
% 0.79/1.17 ( X, Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), plus_plus( X, ti( X, Y ), Z ) = plus_plus( X, Y,
% 0.79/1.17 Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), plus_plus( X, Y, ti( X, Z ) ) = plus_plus( X, Y,
% 0.79/1.17 Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), ti( X, plus_plus( X, Y, Z ) ) = plus_plus( X, Y,
% 0.79/1.17 Z ) }.
% 0.79/1.17 { ! number( X ), ! semiring( X ), times_times( X, ti( X, Y ), Z ) =
% 0.79/1.17 times_times( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! semiring( X ), times_times( X, Y, ti( X, Z ) ) =
% 0.79/1.17 times_times( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! semiring( X ), ti( X, times_times( X, Y, Z ) ) =
% 0.79/1.17 times_times( X, Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), times_times( X, ti( X, Y ), Z ) = times_times( X
% 0.79/1.17 , Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), times_times( X, Y, ti( X, Z ) ) = times_times( X
% 0.79/1.17 , Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), ti( X, times_times( X, Y, Z ) ) = times_times( X
% 0.79/1.17 , Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), ti( X, zero_zero( X ) ) = zero_zero( X ) }.
% 0.79/1.17 { ! semiring_1( X ), ti( X, zero_zero( X ) ) = zero_zero( X ) }.
% 0.79/1.17 { ti( X, undefined( X ) ) = undefined( X ) }.
% 0.79/1.17 { ! zprime( ti( int, X ) ), zprime( X ) }.
% 0.79/1.17 { ! zprime( X ), zprime( ti( int, X ) ) }.
% 0.79/1.17 { bit0( ti( int, X ) ) = bit0( X ) }.
% 0.79/1.17 { ti( int, bit0( X ) ) = bit0( X ) }.
% 0.79/1.17 { bit1( ti( int, X ) ) = bit1( X ) }.
% 0.79/1.17 { ti( int, bit1( X ) ) = bit1( X ) }.
% 0.79/1.17 { ti( int, pls ) = pls }.
% 0.79/1.17 { ! number( X ), number_number_of( X, ti( int, Y ) ) = number_number_of( X
% 0.79/1.17 , Y ) }.
% 0.79/1.17 { ! number( X ), ti( X, number_number_of( X, Y ) ) = number_number_of( X, Y
% 0.79/1.17 ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less( X, ti( X, Y ), Z ), ord_less
% 0.79/1.17 ( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less( X, Y, Z ), ord_less( X, ti( X
% 0.79/1.17 , Y ), Z ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less( X, Y, ti( X, Z ) ), ord_less
% 0.79/1.17 ( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less( X, Y, Z ), ord_less( X, Y, ti
% 0.79/1.17 ( X, Z ) ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, ti( X, Y ), Z ), ord_less( X, Y, Z
% 0.79/1.17 ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, Y, Z ), ord_less( X, ti( X, Y ), Z
% 0.79/1.17 ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, Y, ti( X, Z ) ), ord_less( X, Y, Z
% 0.79/1.17 ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, Y, Z ), ord_less( X, Y, ti( X, Z )
% 0.79/1.17 ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, ti( X, Y ), Z ),
% 0.79/1.17 ord_less_eq( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, Y, Z ), ord_less_eq( X
% 0.79/1.17 , ti( X, Y ), Z ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, Y, ti( X, Z ) ),
% 0.79/1.17 ord_less_eq( X, Y, Z ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, Y, Z ), ord_less_eq( X
% 0.79/1.17 , Y, ti( X, Z ) ) }.
% 0.79/1.17 { ! linordered_ring( X ), ! ord_less_eq( X, ti( X, Y ), Z ), ord_less_eq( X
% 0.79/1.17 , Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), ! ord_less_eq( X, Y, Z ), ord_less_eq( X, ti( X,
% 0.79/1.17 Y ), Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), ! ord_less_eq( X, Y, ti( X, Z ) ), ord_less_eq( X
% 0.79/1.17 , Y, Z ) }.
% 0.79/1.17 { ! linordered_ring( X ), ! ord_less_eq( X, Y, Z ), ord_less_eq( X, Y, ti(
% 0.79/1.17 X, Z ) ) }.
% 0.79/1.17 { ! semiring_1( X ), power_power( X, ti( X, Y ), Z ) = power_power( X, Y, Z
% 0.79/1.17 ) }.
% 0.79/1.17 { ! semiring_1( X ), power_power( X, Y, ti( nat, Z ) ) = power_power( X, Y
% 0.79/1.17 , Z ) }.
% 0.79/1.17 { ! semiring_1( X ), ti( X, power_power( X, Y, Z ) ) = power_power( X, Y, Z
% 0.79/1.17 ) }.
% 0.79/1.17 { ! twoSqu33214720sum2sq( ti( int, X ) ), twoSqu33214720sum2sq( X ) }.
% 0.79/1.17 { ! twoSqu33214720sum2sq( X ), twoSqu33214720sum2sq( ti( int, X ) ) }.
% 0.79/1.17 { ti( int, m ) = m }.
% 0.79/1.17 { ti( int, s ) = s }.
% 0.79/1.17 { ti( int, t ) = t }.
% 0.79/1.17 { ord_less( int, t, zero_zero( int ) ) }.
% 0.79/1.17 { ord_less( int, t, one_one( int ) ) }.
% 0.79/1.17 { ord_less( int, times_times( int, plus_plus( int, times_times( int,
% 0.79/1.17 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.79/1.17 ), t ), times_times( int, plus_plus( int, times_times( int,
% 0.79/1.17 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.79/1.17 ), zero_zero( int ) ) ) }.
% 0.79/1.17 { plus_plus( int, power_power( int, s, number_number_of( nat, bit0( bit1(
% 0.79/1.17 pls ) ) ) ), one_one( int ) ) = times_times( int, plus_plus( int,
% 0.79/1.17 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.79/1.17 ), one_one( int ) ), t ) }.
% 0.79/1.17 { ! t = zero_zero( int ), plus_plus( int, power_power( int, s,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) =
% 0.79/1.17 zero_zero( int ) }.
% 0.79/1.17 { ! ord_less_eq( int, one_one( int ), t ) }.
% 0.79/1.17 { ord_less( int, zero_zero( int ), plus_plus( int, times_times( int,
% 0.79/1.17 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.79/1.17 ) ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, plus_plus( X, power_power( X, Y,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( X, Z,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ) ), zero_zero( X ) ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, zero_zero( X ), plus_plus( X,
% 0.79/1.17 power_power( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.79/1.17 power_power( X, Z, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ), !
% 0.79/1.17 ti( X, Y ) = zero_zero( X ), ! ti( X, Z ) = zero_zero( X ) }.
% 0.79/1.17 { ! linordered_idom( X ), ti( X, Y ) = zero_zero( X ), ord_less( X,
% 0.79/1.17 zero_zero( X ), plus_plus( X, power_power( X, Y, number_number_of( nat,
% 0.79/1.17 bit0( bit1( pls ) ) ) ), power_power( X, Z, number_number_of( nat, bit0(
% 0.79/1.17 bit1( pls ) ) ) ) ) ) }.
% 0.79/1.17 { ! linordered_idom( X ), ti( X, Z ) = zero_zero( X ), ord_less( X,
% 0.79/1.17 zero_zero( X ), plus_plus( X, power_power( X, Y, number_number_of( nat,
% 0.79/1.17 bit0( bit1( pls ) ) ) ), power_power( X, Z, number_number_of( nat, bit0(
% 0.79/1.17 bit1( pls ) ) ) ) ) ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! plus_plus( X, power_power( X, Y,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( X, Z,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = zero_zero( X ), ti( X
% 0.79/1.17 , Y ) = zero_zero( X ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! plus_plus( X, power_power( X, Y,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( X, Z,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = zero_zero( X ), ti( X
% 0.79/1.17 , Z ) = zero_zero( X ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ti( X, Y ) = zero_zero( X ), ! ti( X, Z ) =
% 0.79/1.17 zero_zero( X ), plus_plus( X, power_power( X, Y, number_number_of( nat,
% 0.79/1.17 bit0( bit1( pls ) ) ) ), power_power( X, Z, number_number_of( nat, bit0(
% 0.79/1.17 bit1( pls ) ) ) ) ) = zero_zero( X ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, power_power( X, Y,
% 0.79/1.17 number_number_of( nat, bit0( bit1( pls ) ) ) ), zero_zero( X ) ) }.
% 0.79/1.17 { ! linordered_idom( X ), ! ord_less( X, zero_zero( X ), power_power( X, Y
% 0.79/1.17 , number_number_of( nat, bit0( bit1( pls ) ) ) ) ), ! ti( X, Y ) =
% 0.79/1.17 zero_zero( X ) }.
% 0.79/1.17 { ! linordered_idom( X ), ti( X, Y ) = zero_zero( X ), ord_less( X,
% 0.79/1.17 zero_zero( X ), power_power( X, Y, number_number_of( nat, bit0( bit1( pls
% 0.79/1.17 ) ) ) ) ) }.
% 0.79/1.17 { ! semiring_1( X ), power_power( X, one_one( X ), number_number_of( nat,
% 0.79/1.17 bit0( bit1( pls ) ) ) ) = one_one( X ) }.
% 0.79/1.17 { ! semiring_1( X ), power_power( X, zero_zero( X ), number_number_of( nat
% 0.79/1.17 , bit0( bit1( pls ) ) ) ) = zero_zero( X ) }.
% 0.79/1.17 { ! ring_11004092258visors( X ), ! power_power( X, Y, number_number_of( nat
% 0.79/1.17 , bit0( bit1( pls ) ) ) ) = zero_zero( X ), ti( X, Y ) = zero_zero( X ) }
% 0.79/1.17 .
% 0.79/1.17 { ! ring_11004092258visors( X ), ! ti( X, Y ) = zero_zero( X ), power_power
% 0.79/1.17 ( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) = zero_zero( X ) }
% 0.79/1.17 .
% 0.79/1.17 { ! number_ring( X ), plus_plus( X, one_one( X ), number_number_of( X, Y )
% 0.79/1.17 ) = number_number_of( X, plus_plus( int, bit1( pls ), Y ) ) }.
% 0.79/1.17 { ! number_ring( X ), plus_plus( X, number_number_of( X, Y ), one_one( X )
% 0.79/1.17 ) = number_number_of( X, plus_plus( int, Y, bit1( pls ) ) ) }.
% 0.79/1.17 { ord_less( int, t, plus_plus( int, times_times( int, number_number_of( int
% 0.79/1.17 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) ) }.
% 0.79/1.17 { plus_plus( int, power_power( int, s, number_number_of( nat, bit0( bit1(
% 0.79/1.17 pls ) ) ) ), one_one( int ) ) = times_times( int, plus_plus( int,
% 0.79/1.17 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.79/1.17 ), one_one( int ) ), skol1 ) }.
% 0.79/1.17 { zprime( plus_plus( int, times_times( int, number_number_of( int, bit0(
% 0.79/1.17 bit0( bit1( pls ) ) ) ), m ), one_one( int ) ) ) }.
% 0.79/1.17 { twoSqu33214720sum2sq( times_times( int, plus_plus( int, times_times( int
% 0.79/1.17 , number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int
% 0.79/1.17 ) ), t ) ) }.
% 0.79/1.17 { ord_less_eq( int, X, X ) }.
% 0.79/1.17 { number_number_of( int, X ) = X }.
% 0.79/1.17 { times_times( int, X, Y ) = times_times( int, Y, X ) }.
% 0.79/1.17 { ord_less_eq( int, X, Y ), ord_less_eq( int, Y, X ) }.
% 0.79/1.17 { times_times( int, number_number_of( int, X ), number_number_of( int, Y )
% 0.79/1.17 ) = number_number_of( int, times_times( int, X, Y ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, number_number_of( int, X ), number_number_of( int, Y
% 0.79/1.17 ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, number_number_of( int, X )
% 0.79/1.17 , number_number_of( int, Y ) ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( X,
% 0.79/1.17 number_number_of( X, Y ), number_number_of( X, Z ) ), ord_less_eq( int, Y
% 0.79/1.17 , Z ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( int, Y, Z ),
% 0.79/1.17 ord_less_eq( X, number_number_of( X, Y ), number_number_of( X, Z ) ) }.
% 0.79/1.17 { times_times( int, times_times( int, X, Y ), Z ) = times_times( int, X,
% 0.79/1.17 times_times( int, Y, Z ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ! ord_less_eq( int, Y, Z ), ord_less_eq( int
% 0.79/1.17 , X, Z ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ! ord_less_eq( int, Y, X ), X = Y }.
% 0.79/1.17 { power_power( int, X, plus_plus( nat, Y, Z ) ) = times_times( int,
% 0.79/1.17 power_power( int, X, Y ), power_power( int, X, Z ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit1( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit1( X ), bit1( Y ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit1( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit1( X ), bit1( Y ) ) }.
% 0.79/1.17 { ord_less_eq( int, pls, pls ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit0( X ), bit0( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit0( Y ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit0( X ), bit0( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit0( Y ) ) }.
% 0.79/1.17 { ! ord_less( int, X, Y ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less( int, X, Y ), ! X = Y }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), X = Y, ord_less( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, plus_plus( int, Z, X ),
% 0.79/1.17 plus_plus( int, Z, Y ) ) }.
% 0.79/1.17 { ! number_number_of( nat, X ) = zero_zero( nat ), ord_less_eq( int, X, pls
% 0.79/1.17 ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, pls ), number_number_of( nat, X ) = zero_zero( nat
% 0.79/1.17 ) }.
% 0.79/1.17 { ! zero_zero( nat ) = number_number_of( nat, X ), ord_less_eq( int, X, pls
% 0.79/1.17 ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, pls ), zero_zero( nat ) = number_number_of( nat, X
% 0.79/1.17 ) }.
% 0.79/1.17 { ! number_semiring( X ), ! ord_less_eq( int, pls, Y ), ! ord_less_eq( int
% 0.79/1.17 , pls, Z ), times_times( X, number_number_of( X, Y ), number_number_of( X
% 0.79/1.17 , Z ) ) = number_number_of( X, times_times( int, Y, Z ) ) }.
% 0.79/1.17 { ! number_ring( X ), times_times( X, number_number_of( X, Y ), times_times
% 0.79/1.17 ( X, number_number_of( X, Z ), T ) ) = times_times( X, number_number_of(
% 0.79/1.17 X, times_times( int, Y, Z ) ), T ) }.
% 0.79/1.17 { ! number_ring( X ), times_times( X, number_number_of( X, Y ),
% 0.79/1.17 number_number_of( X, Z ) ) = number_number_of( X, times_times( int, Y, Z
% 0.79/1.17 ) ) }.
% 0.79/1.17 { ! number_ring( X ), number_number_of( X, times_times( int, Y, Z ) ) =
% 0.79/1.17 times_times( X, number_number_of( X, Y ), number_number_of( X, Z ) ) }.
% 0.79/1.17 { ! linord581940658strict( X ), ! ord_less_eq( X, plus_plus( X, times_times
% 0.79/1.17 ( X, Y, Y ), times_times( X, Z, Z ) ), zero_zero( X ) ), ti( X, Y ) =
% 0.79/1.17 zero_zero( X ) }.
% 0.79/1.17 { ! linord581940658strict( X ), ! ord_less_eq( X, plus_plus( X, times_times
% 0.79/1.17 ( X, Y, Y ), times_times( X, Z, Z ) ), zero_zero( X ) ), ti( X, Z ) =
% 0.79/1.17 zero_zero( X ) }.
% 0.79/1.17 { ! linord581940658strict( X ), ! ti( X, Y ) = zero_zero( X ), ! ti( X, Z )
% 0.79/1.17 = zero_zero( X ), ord_less_eq( X, plus_plus( X, times_times( X, Y, Y ),
% 0.79/1.17 times_times( X, Z, Z ) ), zero_zero( X ) ) }.
% 0.79/1.17 { ! linordered_ring( X ), ord_less_eq( X, zero_zero( X ), plus_plus( X,
% 0.79/1.17 times_times( X, Y, Y ), times_times( X, Z, Z ) ) ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( X,
% 0.79/1.17 number_number_of( X, Y ), zero_zero( X ) ), ord_less_eq( int, Y, pls ) }
% 0.79/1.17 .
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( int, Y, pls )
% 0.79/1.17 , ord_less_eq( X, number_number_of( X, Y ), zero_zero( X ) ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( X, zero_zero(
% 0.79/1.17 X ), number_number_of( X, Y ) ), ord_less_eq( int, pls, Y ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( int, pls, Y )
% 0.79/1.17 , ord_less_eq( X, zero_zero( X ), number_number_of( X, Y ) ) }.
% 0.79/1.17 { ! ord_less( nat, zero_zero( nat ), number_number_of( nat, X ) ), ord_less
% 0.79/1.17 ( int, pls, X ) }.
% 0.79/1.17 { ! ord_less( int, pls, X ), ord_less( nat, zero_zero( nat ),
% 0.79/1.17 number_number_of( nat, X ) ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ! ord_less_eq( X, number_number_of( X, Y
% 0.79/1.17 ), number_number_of( X, Z ) ), ! ord_less( X, number_number_of( X, Z ),
% 0.79/1.17 number_number_of( X, Y ) ) }.
% 0.79/1.17 { ! number( X ), ! linorder( X ), ord_less( X, number_number_of( X, Z ),
% 0.79/1.17 number_number_of( X, Y ) ), ord_less_eq( X, number_number_of( X, Y ),
% 0.79/1.17 number_number_of( X, Z ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, pls, bit1( X ) ), ord_less_eq( int, pls, X ) }.
% 0.79/1.17 { ! ord_less_eq( int, pls, X ), ord_less_eq( int, pls, bit1( X ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit1( Y ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, Y ), ord_less_eq( int, bit0( X ), bit1( Y ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit0( X ), pls ), ord_less_eq( int, X, pls ) }.
% 0.79/1.17 { ! ord_less_eq( int, X, pls ), ord_less_eq( int, bit0( X ), pls ) }.
% 0.79/1.17 { ! ord_less_eq( int, pls, bit0( X ) ), ord_less_eq( int, pls, X ) }.
% 0.79/1.17 { ! ord_less_eq( int, pls, X ), ord_less_eq( int, pls, bit0( X ) ) }.
% 0.79/1.17 { ! ord_less( int, X, Y ), ! ord_less_eq( int, Z, T ), ord_less( int,
% 0.79/1.17 plus_plus( int, X, Z ), plus_plus( int, Y, T ) ) }.
% 0.79/1.17 { number_number_of( nat, pls ) = zero_zero( nat ) }.
% 0.79/1.17 { zero_zero( nat ) = number_number_of( nat, pls ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( X,
% 0.79/1.17 number_number_of( X, Y ), one_one( X ) ), ord_less_eq( int, Y, bit1( pls
% 0.79/1.17 ) ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( int, Y, bit1(
% 0.79/1.17 pls ) ), ord_less_eq( X, number_number_of( X, Y ), one_one( X ) ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( X, one_one( X
% 0.79/1.17 ), number_number_of( X, Y ) ), ord_less_eq( int, bit1( pls ), Y ) }.
% 0.79/1.17 { ! number_ring( X ), ! linordered_idom( X ), ! ord_less_eq( int, bit1( pls
% 0.79/1.17 ), Y ), ord_less_eq( X, one_one( X ), number_number_of( X, Y ) ) }.
% 0.79/1.17 { plus_plus( nat, one_one( nat ), one_one( nat ) ) = number_number_of( nat
% 0.79/1.17 , bit0( bit1( pls ) ) ) }.
% 0.79/1.17 { times_times( int, pls, X ) = pls }.
% 0.79/1.17 { times_times( int, bit0( X ), Y ) = bit0( times_times( int, X, Y ) ) }.
% 0.79/1.17 { ! ord_less( int, number_number_of( int, X ), number_number_of( int, Y ) )
% 0.79/1.17 , ord_less( int, X, Y ) }.
% 0.79/1.17 { ! ord_less( int, X, Y ), ord_less( int, number_number_of( int, X ),
% 0.79/1.17 number_number_of( int, Y ) ) }.
% 0.79/1.17 { times_times( int, X, one_one( int ) ) = X }.
% 0.79/1.17 { times_times( int, one_one( int ), X ) = X }.
% 0.79/1.17 { plus_plus( int, number_number_of( int, X ), number_number_of( int, Y ) )
% 0.79/1.17 = number_number_of( int, plus_plus( int, X, Y ) ) }.
% 0.79/1.17 { times_times( int, plus_plus( int, X, Y ), Z ) = plus_plus( int,
% 0.79/1.17 times_times( int, X, Z ), times_times( int, Y, Z ) ) }.
% 0.79/1.17 { times_times( int, X, plus_plus( int, Y, Z ) ) = plus_plus( int,
% 0.79/1.17 times_times( int, X, Y ), times_times( int, X, Z ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit1( X ), pls ), ord_less( int, X, pls ) }.
% 0.79/1.17 { ! ord_less( int, X, pls ), ord_less_eq( int, bit1( X ), pls ) }.
% 0.79/1.17 { ! ord_less( int, pls, bit1( X ) ), ord_less_eq( int, pls, X ) }.
% 0.79/1.17 { ! ord_less_eq( int, pls, X ), ord_less( int, pls, bit1( X ) ) }.
% 0.79/1.17 { ! ord_less_eq( int, bit1( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.79/1.17 { ! ord_less( int, X, Y ), ord_less_eq( int, bit1( X ), bit0( Y ) ) }.
% 0.79/1.18 { ! ord_less_eq( int, bit1( X ), bit0( Y ) ), ord_less( int, X, Y ) }.
% 0.79/1.18 { ! ord_less( int, X, Y ), ord_less_eq( int, bit1( X ), bit0( Y ) ) }.
% 0.79/1.18 { ! ord_less( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.18 { ! ord_less_eq( int, X, Y ), ord_less( int, bit0( X ), bit1( Y ) ) }.
% 0.79/1.18 { ! ord_less( int, bit0( X ), bit1( Y ) ), ord_less_eq( int, X, Y ) }.
% 0.79/1.18 { ! ord_less_eq( int, X, Y ), ord_less( int, bit0( X ), bit1( Y ) ) }.
% 0.79/1.18 { ! ord_less( nat, number_number_of( nat, X ), number_number_of( nat, Y ) )
% 0.79/1.18 , alpha1( X, Y ) }.
% 0.79/1.18 { ! ord_less( nat, number_number_of( nat, X ), number_number_of( nat, Y ) )
% 0.79/1.18 , ord_less( int, X, Y ) }.
% 0.79/1.18 { ! alpha1( X, Y ), ! ord_less( int, X, Y ), ord_less( nat,
% 0.79/1.18 number_number_of( nat, X ), number_number_of( nat, Y ) ) }.
% 0.79/1.18 { ! alpha1( X, Y ), ! ord_less( int, X, Y ), ord_less( int, pls, Y ) }.
% 0.79/1.18 { ord_less( int, X, Y ), alpha1( X, Y ) }.
% 0.79/1.18 { ! ord_less( int, pls, Y ), alpha1( X, Y ) }.
% 0.79/1.18 { ! ord_less_eq( int, one_one( int ), X ), ord_less( int, zero_zero( int )
% 0.79/1.18 , X ) }.
% 0.79/1.18 { ! ord_less( int, zero_zero( int ), X ), ord_less_eq( int, one_one( int )
% 0.79/1.18 , X ) }.
% 0.79/1.18 { number_number_of( nat, bit1( pls ) ) = one_one( nat ) }.
% 0.79/1.18 { one_one( nat ) = number_number_of( nat, bit1( pls ) ) }.
% 0.79/1.18 { ! ord_less( int, X, Y ), ord_less_eq( int, plus_plus( int, X, one_one(
% 0.79/1.18 int ) ), Y ) }.
% 0.79/1.18 { ! ord_less_eq( int, plus_plus( int, X, one_one( int ) ), Y ), ord_less(
% 0.79/1.18 int, X, Y ) }.
% 0.79/1.18 { ! ord_less( int, X, Y ), ord_less_eq( int, plus_plus( int, X, one_one(
% 0.79/1.18 int ) ), Y ) }.
% 0.79/1.18 { ! ord_less( int, X, plus_plus( int, Y, one_one( int ) ) ), ord_less_eq(
% 0.79/1.18 int, X, Y ) }.
% 0.79/1.18 { ! ord_less_eq( int, X, Y ), ord_less( int, X, plus_plus( int, Y, one_one
% 0.79/1.18 ( int ) ) ) }.
% 0.79/1.18 { ! number_semiring( X ), ! ord_less_eq( int, pls, Y ), ! ord_less_eq( int
% 0.79/1.18 , pls, Z ), plus_plus( X, number_number_of( X, Y ), number_number_of( X,
% 0.79/1.18 Z ) ) = number_number_of( X, plus_plus( int, Y, Z ) ) }.
% 0.79/1.18 { ! ord_less( int, Y, pls ), plus_plus( nat, number_number_of( nat, Y ),
% 0.79/1.18 number_number_of( nat, X ) ) = number_number_of( nat, X ) }.
% 0.79/1.18 { ord_less( int, Y, pls ), ! ord_less( int, X, pls ), plus_plus( nat,
% 0.79/1.18 number_number_of( nat, Y ), number_number_of( nat, X ) ) =
% 0.79/1.18 number_number_of( nat, Y ) }.
% 0.79/1.18 { ord_less( int, Y, pls ), ord_less( int, X, pls ), plus_plus( nat,
% 0.79/1.18 number_number_of( nat, Y ), number_number_of( nat, X ) ) =
% 0.79/1.18 number_number_of( nat, plus_plus( int, Y, X ) ) }.
% 0.79/1.18 { ! ord_less_eq( int, zero_zero( int ), X ), ord_less( int, zero_zero( int
% 0.79/1.18 ), plus_plus( int, one_one( int ), X ) ) }.
% 0.79/1.18 { ! number_ring( X ), ! ring_char_0( X ), ! number_number_of( X, Y ) =
% 0.79/1.18 number_number_of( X, Z ), Y = Z }.
% 0.79/1.18 { ! number_ring( X ), ! ring_char_0( X ), ! Y = Z, number_number_of( X, Y )
% 0.79/1.18 = number_number_of( X, Z ) }.
% 0.79/1.18 { ! number( X ), ! number_number_of( X, Y ) = ti( X, Z ), ti( X, Z ) =
% 0.79/1.18 number_number_of( X, Y ) }.
% 0.79/1.18 { ! number( X ), ! ti( X, Z ) = number_number_of( X, Y ), number_number_of
% 0.79/1.18 ( X, Y ) = ti( X, Z ) }.
% 0.79/1.18 { ! bit1( X ) = bit1( Y ), X = Y }.
% 0.79/1.18 { ! X = Y, bit1( X ) = bit1( Y ) }.
% 0.79/1.18 { ! bit0( X ) = bit0( Y ), X = Y }.
% 0.79/1.18 { ! X = Y, bit0( X ) = bit0( Y ) }.
% 0.79/1.18 { ord_less( int, X, Y ), X = Y, ord_less( int, Y, X ) }.
% 0.79/1.18 { ! linord581940658strict( X ), ! plus_plus( X, times_times( X, Y, Y ),
% 0.79/1.18 times_times( X, Z, Z ) ) = zero_zero( X ), ti( X, Y ) = zero_zero( X ) }
% 0.79/1.18 .
% 0.79/1.18 { ! linord581940658strict( X ), ! plus_plus( X, times_times( X, Y, Y ),
% 0.79/1.18 times_times( X, Z, Z ) ) = zero_zero( X ), ti( X, Z ) = zero_zero( X ) }
% 0.79/1.18 .
% 0.79/1.18 { ! linord581940658strict( X ), ! ti( X, Y ) = zero_zero( X ), ! ti( X, Z )
% 0.79/1.18 = zero_zero( X ), plus_plus( X, times_times( X, Y, Y ), times_times( X,
% 0.79/1.18 Z, Z ) ) = zero_zero( X ) }.
% 0.79/1.18 { ! number( X ), ! semiring( X ), times_times( X, plus_plus( X, Y, Z ),
% 0.79/1.18 number_number_of( X, T ) ) = plus_plus( X, times_times( X, Y,
% 0.79/1.18 number_number_of( X, T ) ), times_times( X, Z, number_number_of( X, T ) )
% 0.79/1.18 ) }.
% 0.79/1.18 { ! number( X ), ! semiring( X ), times_times( X, number_number_of( X, Y )
% 0.79/1.18 , plus_plus( X, Z, T ) ) = plus_plus( X, times_times( X, number_number_of
% 0.79/1.18 ( X, Y ), Z ), times_times( X, number_number_of( X, Y ), T ) ) }.
% 0.79/1.18 { plus_plus( int, plus_plus( int, X, Y ), Z ) = plus_plus( int, X,
% 0.81/1.21 plus_plus( int, Y, Z ) ) }.
% 0.81/1.21 { plus_plus( int, X, plus_plus( int, Y, Z ) ) = plus_plus( int, Y,
% 0.81/1.21 plus_plus( int, X, Z ) ) }.
% 0.81/1.21 { plus_plus( int, X, Y ) = plus_plus( int, Y, X ) }.
% 0.81/1.21 { zero_zero( int ) = number_number_of( int, pls ) }.
% 0.81/1.21 { ring_11004092258visors( int ) }.
% 0.81/1.21 { linord581940658strict( int ) }.
% 0.81/1.21 { linordered_ring( int ) }.
% 0.81/1.21 { linordered_idom( int ) }.
% 0.81/1.21 { number_semiring( int ) }.
% 0.81/1.21 { linorder( int ) }.
% 0.81/1.21 { semiring_1( int ) }.
% 0.81/1.21 { ring_char_0( int ) }.
% 0.81/1.21 { number_ring( int ) }.
% 0.81/1.21 { semiring( int ) }.
% 0.81/1.21 { number( int ) }.
% 0.81/1.21 { number_semiring( nat ) }.
% 0.81/1.21 { linorder( nat ) }.
% 0.81/1.21 { semiring_1( nat ) }.
% 0.81/1.21 { semiring( nat ) }.
% 0.81/1.21 { number( nat ) }.
% 0.81/1.21 { ti( X, ti( X, Y ) ) = ti( X, Y ) }.
% 0.81/1.21 { ! ord_less( int, plus_plus( int, power_power( int, s, number_number_of(
% 0.81/1.21 nat, bit0( bit1( pls ) ) ) ), one_one( int ) ), zero_zero( int ) ) }.
% 0.81/1.21
% 0.81/1.21 *** allocated 15000 integers for clauses
% 0.81/1.21 percentage equality = 0.271300, percentage horn = 0.951220
% 0.81/1.21 This is a problem with some equality
% 0.81/1.21
% 0.81/1.21
% 0.81/1.21
% 0.81/1.21 Options Used:
% 0.81/1.21
% 0.81/1.21 useres = 1
% 0.81/1.21 useparamod = 1
% 0.81/1.21 useeqrefl = 1
% 0.81/1.21 useeqfact = 1
% 0.81/1.21 usefactor = 1
% 0.81/1.21 usesimpsplitting = 0
% 0.81/1.21 usesimpdemod = 5
% 0.81/1.21 usesimpres = 3
% 0.81/1.21
% 0.81/1.21 resimpinuse = 1000
% 0.81/1.21 resimpclauses = 20000
% 0.81/1.21 substype = eqrewr
% 0.81/1.21 backwardsubs = 1
% 0.81/1.21 selectoldest = 5
% 0.81/1.21
% 0.81/1.21 litorderings [0] = split
% 0.81/1.21 litorderings [1] = extend the termordering, first sorting on arguments
% 0.81/1.21
% 0.81/1.21 termordering = kbo
% 0.81/1.21
% 0.81/1.21 litapriori = 0
% 0.81/1.21 termapriori = 1
% 0.81/1.21 litaposteriori = 0
% 0.81/1.21 termaposteriori = 0
% 0.81/1.21 demodaposteriori = 0
% 0.81/1.21 ordereqreflfact = 0
% 0.81/1.21
% 0.81/1.21 litselect = negord
% 0.81/1.21
% 0.81/1.21 maxweight = 15
% 0.81/1.21 maxdepth = 30000
% 0.81/1.21 maxlength = 115
% 0.81/1.21 maxnrvars = 195
% 0.81/1.21 excuselevel = 1
% 0.81/1.21 increasemaxweight = 1
% 0.81/1.21
% 0.81/1.21 maxselected = 10000000
% 0.81/1.21 maxnrclauses = 10000000
% 0.81/1.21
% 0.81/1.21 showgenerated = 0
% 0.81/1.21 showkept = 0
% 0.81/1.21 showselected = 0
% 0.81/1.21 showdeleted = 0
% 0.81/1.21 showresimp = 1
% 0.81/1.21 showstatus = 2000
% 0.81/1.21
% 0.81/1.21 prologoutput = 0
% 0.81/1.21 nrgoals = 5000000
% 0.81/1.21 totalproof = 1
% 0.81/1.21
% 0.81/1.21 Symbols occurring in the translation:
% 0.81/1.21
% 0.81/1.21 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.81/1.21 . [1, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.81/1.21 ! [4, 1] (w:0, o:49, a:1, s:1, b:0),
% 0.81/1.21 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.81/1.21 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.81/1.21 semiring_1 [36, 1] (w:1, o:56, a:1, s:1, b:0),
% 0.81/1.21 one_one [37, 1] (w:1, o:60, a:1, s:1, b:0),
% 0.81/1.21 ti [38, 2] (w:1, o:96, a:1, s:1, b:0),
% 0.81/1.21 number [42, 1] (w:1, o:57, a:1, s:1, b:0),
% 0.81/1.21 semiring [43, 1] (w:1, o:61, a:1, s:1, b:0),
% 0.81/1.21 plus_plus [44, 3] (w:1, o:101, a:1, s:1, b:0),
% 0.81/1.21 linordered_ring [45, 1] (w:1, o:62, a:1, s:1, b:0),
% 0.81/1.21 times_times [46, 3] (w:1, o:102, a:1, s:1, b:0),
% 0.81/1.21 zero_zero [47, 1] (w:1, o:63, a:1, s:1, b:0),
% 0.81/1.21 undefined [48, 1] (w:1, o:65, a:1, s:1, b:0),
% 0.81/1.21 int [49, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.81/1.21 zprime [50, 1] (w:1, o:66, a:1, s:1, b:0),
% 0.81/1.21 bit0 [51, 1] (w:1, o:67, a:1, s:1, b:0),
% 0.81/1.21 bit1 [52, 1] (w:1, o:68, a:1, s:1, b:0),
% 0.81/1.21 pls [53, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.81/1.21 number_number_of [54, 2] (w:1, o:97, a:1, s:1, b:0),
% 0.81/1.21 linorder [55, 1] (w:1, o:69, a:1, s:1, b:0),
% 0.81/1.21 ord_less [56, 3] (w:1, o:99, a:1, s:1, b:0),
% 0.81/1.21 linordered_idom [57, 1] (w:1, o:70, a:1, s:1, b:0),
% 0.81/1.21 ord_less_eq [58, 3] (w:1, o:100, a:1, s:1, b:0),
% 0.81/1.21 power_power [59, 3] (w:1, o:103, a:1, s:1, b:0),
% 0.81/1.21 nat [60, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.81/1.21 twoSqu33214720sum2sq [61, 1] (w:1, o:64, a:1, s:1, b:0),
% 0.81/1.21 m [62, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.81/1.21 s [63, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.81/1.21 t [64, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.81/1.21 ring_11004092258visors [71, 1] (w:1, o:54, a:1, s:1, b:0),
% 0.81/1.21 number_ring [72, 1] (w:1, o:58, a:1, s:1, b:0),
% 0.81/1.21 number_semiring [90, 1] (w:1, o:59, a:1, s:1, b:0),
% 0.81/1.21 linord581940658strict [92, 1] (w:1, o:71, a:1, s:1, b:0),
% 0.81/1.21 ring_char_0 [97, 1] (w:1, o:55, a:1, s:1, b:0),
% 0.81/1.21 alpha1 [102, 2] (w:1, o:98, a:1, s:1, b:1),
% 0.81/1.21 skol1 [103, 0] (w:1, o:25, a:1, s:1, b:1).
% 0.81/1.21
% 0.81/1.21
% 0.81/1.21 Starting Search:
% 0.81/1.21
% 0.81/1.21 *** allocated 22500 integers for clauses
% 0.81/1.21 *** allocated 33750 integers for clauses
% 0.81/1.21 *** allocated 50625 integers for clauses
% 0.81/1.21 *** allocated 22500 integers for termspace/termends
% 0.81/1.21 *** allocated 75937 integers for clauses
% 0.81/1.21 Resimplifying inuse:
% 0.81/1.21 Done
% 0.81/1.21
% 0.81/1.21 *** allocated 33750 integers for termspace/termends
% 0.81/1.21
% 0.81/1.21 Bliksems!, er is een bewijs:
% 0.81/1.21 % SZS status Theorem
% 0.81/1.21 % SZS output start Refutation
% 0.81/1.21
% 0.81/1.21 (51) {G0,W35,D9,L1,V0,M1} I { ord_less( int, times_times( int, plus_plus(
% 0.81/1.21 int, times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) )
% 0.81/1.21 ), m ), one_one( int ) ), t ), times_times( int, plus_plus( int,
% 0.81/1.21 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.81/1.21 ), one_one( int ) ), zero_zero( int ) ) ) }.
% 0.81/1.21 (52) {G0,W29,D9,L1,V0,M1} I { times_times( int, plus_plus( int, times_times
% 0.81/1.21 ( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one
% 0.81/1.21 ( int ) ), t ) ==> plus_plus( int, power_power( int, s, number_number_of
% 0.81/1.21 ( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) }.
% 0.81/1.21 (77) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X }.
% 0.81/1.21 (78) {G0,W9,D3,L1,V2,M1} I { times_times( int, X, Y ) = times_times( int, Y
% 0.81/1.21 , X ) }.
% 0.81/1.21 (126) {G0,W6,D3,L1,V1,M1} I { times_times( int, pls, X ) ==> pls }.
% 0.81/1.21 (127) {G0,W11,D4,L1,V2,M1} I { times_times( int, bit0( X ), Y ) ==> bit0(
% 0.81/1.21 times_times( int, X, Y ) ) }.
% 0.81/1.21 (174) {G1,W4,D3,L1,V0,M1} I;d(77) { zero_zero( int ) ==> pls }.
% 0.81/1.21 (192) {G2,W15,D7,L1,V0,M1} I;d(174) { ! ord_less( int, plus_plus( int,
% 0.81/1.21 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.21 one_one( int ) ), pls ) }.
% 0.81/1.21 (1118) {G1,W6,D3,L1,V1,M1} P(78,126) { times_times( int, X, pls ) ==> pls
% 0.81/1.21 }.
% 0.81/1.21 (1219) {G3,W0,D0,L0,V0,M0} S(51);d(52);d(77);d(127);d(127);d(174);d(1118);r
% 0.81/1.21 (192) { }.
% 0.81/1.21
% 0.81/1.21
% 0.81/1.21 % SZS output end Refutation
% 0.81/1.21 found a proof!
% 0.81/1.21
% 0.81/1.21
% 0.81/1.21 Unprocessed initial clauses:
% 0.81/1.21
% 0.81/1.21 (1221) {G0,W9,D4,L2,V1,M2} { ! semiring_1( X ), ti( X, one_one( X ) ) =
% 0.81/1.21 one_one( X ) }.
% 0.81/1.21 (1222) {G0,W15,D4,L3,V3,M3} { ! number( X ), ! semiring( X ), plus_plus( X
% 0.81/1.21 , ti( X, Y ), Z ) = plus_plus( X, Y, Z ) }.
% 0.81/1.21 (1223) {G0,W15,D4,L3,V3,M3} { ! number( X ), ! semiring( X ), plus_plus( X
% 0.81/1.21 , Y, ti( X, Z ) ) = plus_plus( X, Y, Z ) }.
% 0.81/1.21 (1224) {G0,W15,D4,L3,V3,M3} { ! number( X ), ! semiring( X ), ti( X,
% 0.81/1.21 plus_plus( X, Y, Z ) ) = plus_plus( X, Y, Z ) }.
% 0.81/1.21 (1225) {G0,W13,D4,L2,V3,M2} { ! linordered_ring( X ), plus_plus( X, ti( X
% 0.81/1.21 , Y ), Z ) = plus_plus( X, Y, Z ) }.
% 0.81/1.21 (1226) {G0,W13,D4,L2,V3,M2} { ! linordered_ring( X ), plus_plus( X, Y, ti
% 0.81/1.21 ( X, Z ) ) = plus_plus( X, Y, Z ) }.
% 0.81/1.21 (1227) {G0,W13,D4,L2,V3,M2} { ! linordered_ring( X ), ti( X, plus_plus( X
% 0.81/1.21 , Y, Z ) ) = plus_plus( X, Y, Z ) }.
% 0.81/1.21 (1228) {G0,W15,D4,L3,V3,M3} { ! number( X ), ! semiring( X ), times_times
% 0.81/1.21 ( X, ti( X, Y ), Z ) = times_times( X, Y, Z ) }.
% 0.81/1.21 (1229) {G0,W15,D4,L3,V3,M3} { ! number( X ), ! semiring( X ), times_times
% 0.81/1.21 ( X, Y, ti( X, Z ) ) = times_times( X, Y, Z ) }.
% 0.81/1.21 (1230) {G0,W15,D4,L3,V3,M3} { ! number( X ), ! semiring( X ), ti( X,
% 0.81/1.21 times_times( X, Y, Z ) ) = times_times( X, Y, Z ) }.
% 0.81/1.21 (1231) {G0,W13,D4,L2,V3,M2} { ! linordered_ring( X ), times_times( X, ti(
% 0.81/1.21 X, Y ), Z ) = times_times( X, Y, Z ) }.
% 0.81/1.21 (1232) {G0,W13,D4,L2,V3,M2} { ! linordered_ring( X ), times_times( X, Y,
% 0.81/1.21 ti( X, Z ) ) = times_times( X, Y, Z ) }.
% 0.81/1.21 (1233) {G0,W13,D4,L2,V3,M2} { ! linordered_ring( X ), ti( X, times_times(
% 0.81/1.21 X, Y, Z ) ) = times_times( X, Y, Z ) }.
% 0.81/1.21 (1234) {G0,W9,D4,L2,V1,M2} { ! linordered_ring( X ), ti( X, zero_zero( X )
% 0.81/1.21 ) = zero_zero( X ) }.
% 0.81/1.21 (1235) {G0,W9,D4,L2,V1,M2} { ! semiring_1( X ), ti( X, zero_zero( X ) ) =
% 0.81/1.21 zero_zero( X ) }.
% 0.81/1.21 (1236) {G0,W7,D4,L1,V1,M1} { ti( X, undefined( X ) ) = undefined( X ) }.
% 0.81/1.21 (1237) {G0,W6,D3,L2,V1,M2} { ! zprime( ti( int, X ) ), zprime( X ) }.
% 0.81/1.21 (1238) {G0,W6,D3,L2,V1,M2} { ! zprime( X ), zprime( ti( int, X ) ) }.
% 0.81/1.21 (1239) {G0,W7,D4,L1,V1,M1} { bit0( ti( int, X ) ) = bit0( X ) }.
% 0.81/1.21 (1240) {G0,W7,D4,L1,V1,M1} { ti( int, bit0( X ) ) = bit0( X ) }.
% 0.81/1.21 (1241) {G0,W7,D4,L1,V1,M1} { bit1( ti( int, X ) ) = bit1( X ) }.
% 0.81/1.21 (1242) {G0,W7,D4,L1,V1,M1} { ti( int, bit1( X ) ) = bit1( X ) }.
% 0.81/1.21 (1243) {G0,W5,D3,L1,V0,M1} { ti( int, pls ) = pls }.
% 0.81/1.21 (1244) {G0,W11,D4,L2,V2,M2} { ! number( X ), number_number_of( X, ti( int
% 0.81/1.21 , Y ) ) = number_number_of( X, Y ) }.
% 0.81/1.21 (1245) {G0,W11,D4,L2,V2,M2} { ! number( X ), ti( X, number_number_of( X, Y
% 0.81/1.21 ) ) = number_number_of( X, Y ) }.
% 0.81/1.21 (1246) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.81/1.21 X, ti( X, Y ), Z ), ord_less( X, Y, Z ) }.
% 0.81/1.21 (1247) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.81/1.21 X, Y, Z ), ord_less( X, ti( X, Y ), Z ) }.
% 0.81/1.21 (1248) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.81/1.21 X, Y, ti( X, Z ) ), ord_less( X, Y, Z ) }.
% 0.81/1.21 (1249) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ! ord_less(
% 0.81/1.21 X, Y, Z ), ord_less( X, Y, ti( X, Z ) ) }.
% 0.81/1.21 (1250) {G0,W12,D3,L3,V3,M3} { ! linordered_idom( X ), ! ord_less( X, ti( X
% 0.81/1.21 , Y ), Z ), ord_less( X, Y, Z ) }.
% 0.81/1.21 (1251) {G0,W12,D3,L3,V3,M3} { ! linordered_idom( X ), ! ord_less( X, Y, Z
% 0.81/1.21 ), ord_less( X, ti( X, Y ), Z ) }.
% 0.81/1.21 (1252) {G0,W12,D3,L3,V3,M3} { ! linordered_idom( X ), ! ord_less( X, Y, ti
% 0.81/1.21 ( X, Z ) ), ord_less( X, Y, Z ) }.
% 0.81/1.21 (1253) {G0,W12,D3,L3,V3,M3} { ! linordered_idom( X ), ! ord_less( X, Y, Z
% 0.81/1.21 ), ord_less( X, Y, ti( X, Z ) ) }.
% 0.81/1.21 (1254) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.81/1.21 ord_less_eq( X, ti( X, Y ), Z ), ord_less_eq( X, Y, Z ) }.
% 0.81/1.21 (1255) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.81/1.21 ord_less_eq( X, Y, Z ), ord_less_eq( X, ti( X, Y ), Z ) }.
% 0.81/1.21 (1256) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.81/1.21 ord_less_eq( X, Y, ti( X, Z ) ), ord_less_eq( X, Y, Z ) }.
% 0.81/1.21 (1257) {G0,W14,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.81/1.21 ord_less_eq( X, Y, Z ), ord_less_eq( X, Y, ti( X, Z ) ) }.
% 0.81/1.21 (1258) {G0,W12,D3,L3,V3,M3} { ! linordered_ring( X ), ! ord_less_eq( X, ti
% 0.81/1.21 ( X, Y ), Z ), ord_less_eq( X, Y, Z ) }.
% 0.81/1.21 (1259) {G0,W12,D3,L3,V3,M3} { ! linordered_ring( X ), ! ord_less_eq( X, Y
% 0.81/1.21 , Z ), ord_less_eq( X, ti( X, Y ), Z ) }.
% 0.81/1.21 (1260) {G0,W12,D3,L3,V3,M3} { ! linordered_ring( X ), ! ord_less_eq( X, Y
% 0.81/1.21 , ti( X, Z ) ), ord_less_eq( X, Y, Z ) }.
% 0.81/1.21 (1261) {G0,W12,D3,L3,V3,M3} { ! linordered_ring( X ), ! ord_less_eq( X, Y
% 0.81/1.21 , Z ), ord_less_eq( X, Y, ti( X, Z ) ) }.
% 0.81/1.21 (1262) {G0,W13,D4,L2,V3,M2} { ! semiring_1( X ), power_power( X, ti( X, Y
% 0.81/1.21 ), Z ) = power_power( X, Y, Z ) }.
% 0.81/1.21 (1263) {G0,W13,D4,L2,V3,M2} { ! semiring_1( X ), power_power( X, Y, ti(
% 0.81/1.21 nat, Z ) ) = power_power( X, Y, Z ) }.
% 0.81/1.21 (1264) {G0,W13,D4,L2,V3,M2} { ! semiring_1( X ), ti( X, power_power( X, Y
% 0.81/1.21 , Z ) ) = power_power( X, Y, Z ) }.
% 0.81/1.21 (1265) {G0,W6,D3,L2,V1,M2} { ! twoSqu33214720sum2sq( ti( int, X ) ),
% 0.81/1.21 twoSqu33214720sum2sq( X ) }.
% 0.81/1.21 (1266) {G0,W6,D3,L2,V1,M2} { ! twoSqu33214720sum2sq( X ),
% 0.81/1.21 twoSqu33214720sum2sq( ti( int, X ) ) }.
% 0.81/1.21 (1267) {G0,W5,D3,L1,V0,M1} { ti( int, m ) = m }.
% 0.81/1.21 (1268) {G0,W5,D3,L1,V0,M1} { ti( int, s ) = s }.
% 0.81/1.21 (1269) {G0,W5,D3,L1,V0,M1} { ti( int, t ) = t }.
% 0.81/1.21 (1270) {G0,W5,D3,L1,V0,M1} { ord_less( int, t, zero_zero( int ) ) }.
% 0.81/1.21 (1271) {G0,W5,D3,L1,V0,M1} { ord_less( int, t, one_one( int ) ) }.
% 0.81/1.21 (1272) {G0,W35,D9,L1,V0,M1} { ord_less( int, times_times( int, plus_plus(
% 0.81/1.21 int, times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) )
% 0.81/1.21 ), m ), one_one( int ) ), t ), times_times( int, plus_plus( int,
% 0.81/1.21 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.81/1.21 ), one_one( int ) ), zero_zero( int ) ) ) }.
% 0.81/1.21 (1273) {G0,W29,D9,L1,V0,M1} { plus_plus( int, power_power( int, s,
% 0.81/1.21 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) =
% 0.81/1.21 times_times( int, plus_plus( int, times_times( int, number_number_of( int
% 0.81/1.21 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ), t ) }.
% 0.81/1.21 (1274) {G0,W19,D7,L2,V0,M2} { ! t = zero_zero( int ), plus_plus( int,
% 0.81/1.21 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.21 one_one( int ) ) = zero_zero( int ) }.
% 0.81/1.21 (1275) {G0,W5,D3,L1,V0,M1} { ! ord_less_eq( int, one_one( int ), t ) }.
% 0.81/1.21 (1276) {G0,W17,D8,L1,V0,M1} { ord_less( int, zero_zero( int ), plus_plus(
% 0.81/1.21 int, times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) )
% 0.81/1.21 ), m ), one_one( int ) ) ) }.
% 0.81/1.21 (1277) {G0,W24,D7,L2,V3,M2} { ! linordered_idom( X ), ! ord_less( X,
% 0.81/1.21 plus_plus( X, power_power( X, Y, number_number_of( nat, bit0( bit1( pls )
% 0.81/1.21 ) ) ), power_power( X, Z, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.21 ), zero_zero( X ) ) }.
% 0.81/1.21 (1278) {G0,W36,D7,L4,V3,M4} { ! linordered_idom( X ), ! ord_less( X,
% 0.81/1.21 zero_zero( X ), plus_plus( X, power_power( X, Y, number_number_of( nat,
% 0.81/1.21 bit0( bit1( pls ) ) ) ), power_power( X, Z, number_number_of( nat, bit0(
% 0.81/1.21 bit1( pls ) ) ) ) ) ), ! ti( X, Y ) = zero_zero( X ), ! ti( X, Z ) =
% 0.81/1.21 zero_zero( X ) }.
% 0.81/1.21 (1279) {G0,W30,D7,L3,V3,M3} { ! linordered_idom( X ), ti( X, Y ) =
% 0.81/1.21 zero_zero( X ), ord_less( X, zero_zero( X ), plus_plus( X, power_power( X
% 0.81/1.21 , Y, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( X, Z,
% 0.81/1.21 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ) }.
% 0.81/1.21 (1280) {G0,W30,D7,L3,V3,M3} { ! linordered_idom( X ), ti( X, Z ) =
% 0.81/1.21 zero_zero( X ), ord_less( X, zero_zero( X ), plus_plus( X, power_power( X
% 0.81/1.21 , Y, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( X, Z,
% 0.81/1.21 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) ) }.
% 0.81/1.21 (1281) {G0,W29,D7,L3,V3,M3} { ! linordered_idom( X ), ! plus_plus( X,
% 0.81/1.21 power_power( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.21 power_power( X, Z, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) =
% 0.81/1.21 zero_zero( X ), ti( X, Y ) = zero_zero( X ) }.
% 0.81/1.21 (1282) {G0,W29,D7,L3,V3,M3} { ! linordered_idom( X ), ! plus_plus( X,
% 0.81/1.21 power_power( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.21 power_power( X, Z, number_number_of( nat, bit0( bit1( pls ) ) ) ) ) =
% 0.81/1.21 zero_zero( X ), ti( X, Z ) = zero_zero( X ) }.
% 0.81/1.21 (1283) {G0,W35,D7,L4,V3,M4} { ! linordered_idom( X ), ! ti( X, Y ) =
% 0.81/1.21 zero_zero( X ), ! ti( X, Z ) = zero_zero( X ), plus_plus( X, power_power
% 0.81/1.21 ( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ), power_power( X, Z
% 0.81/1.21 , number_number_of( nat, bit0( bit1( pls ) ) ) ) ) = zero_zero( X ) }.
% 0.81/1.21 (1284) {G0,W14,D6,L2,V2,M2} { ! linordered_idom( X ), ! ord_less( X,
% 0.81/1.21 power_power( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.21 zero_zero( X ) ) }.
% 0.81/1.21 (1285) {G0,W20,D6,L3,V2,M3} { ! linordered_idom( X ), ! ord_less( X,
% 0.81/1.21 zero_zero( X ), power_power( X, Y, number_number_of( nat, bit0( bit1( pls
% 0.81/1.21 ) ) ) ) ), ! ti( X, Y ) = zero_zero( X ) }.
% 0.81/1.21 (1286) {G0,W20,D6,L3,V2,M3} { ! linordered_idom( X ), ti( X, Y ) =
% 0.81/1.21 zero_zero( X ), ord_less( X, zero_zero( X ), power_power( X, Y,
% 0.81/1.21 number_number_of( nat, bit0( bit1( pls ) ) ) ) ) }.
% 0.81/1.21 (1287) {G0,W14,D6,L2,V1,M2} { ! semiring_1( X ), power_power( X, one_one(
% 0.81/1.21 X ), number_number_of( nat, bit0( bit1( pls ) ) ) ) = one_one( X ) }.
% 0.81/1.21 (1288) {G0,W14,D6,L2,V1,M2} { ! semiring_1( X ), power_power( X, zero_zero
% 0.81/1.21 ( X ), number_number_of( nat, bit0( bit1( pls ) ) ) ) = zero_zero( X )
% 0.81/1.21 }.
% 0.81/1.21 (1289) {G0,W19,D6,L3,V2,M3} { ! ring_11004092258visors( X ), ! power_power
% 0.81/1.21 ( X, Y, number_number_of( nat, bit0( bit1( pls ) ) ) ) = zero_zero( X ),
% 0.81/1.21 ti( X, Y ) = zero_zero( X ) }.
% 0.81/1.21 (1290) {G0,W19,D6,L3,V2,M3} { ! ring_11004092258visors( X ), ! ti( X, Y )
% 0.81/1.21 = zero_zero( X ), power_power( X, Y, number_number_of( nat, bit0( bit1(
% 0.81/1.21 pls ) ) ) ) = zero_zero( X ) }.
% 0.81/1.21 (1291) {G0,W17,D5,L2,V2,M2} { ! number_ring( X ), plus_plus( X, one_one( X
% 0.81/1.21 ), number_number_of( X, Y ) ) = number_number_of( X, plus_plus( int,
% 0.81/1.21 bit1( pls ), Y ) ) }.
% 0.81/1.21 (1292) {G0,W17,D5,L2,V2,M2} { ! number_ring( X ), plus_plus( X,
% 0.81/1.21 number_number_of( X, Y ), one_one( X ) ) = number_number_of( X, plus_plus
% 0.81/1.21 ( int, Y, bit1( pls ) ) ) }.
% 0.81/1.21 (1293) {G0,W16,D8,L1,V0,M1} { ord_less( int, t, plus_plus( int,
% 0.81/1.21 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.81/1.21 ), one_one( int ) ) ) }.
% 0.81/1.21 (1294) {G0,W29,D9,L1,V0,M1} { plus_plus( int, power_power( int, s,
% 0.81/1.21 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) =
% 0.81/1.21 times_times( int, plus_plus( int, times_times( int, number_number_of( int
% 0.81/1.21 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ), skol1 ) }.
% 0.81/1.21 (1295) {G0,W14,D8,L1,V0,M1} { zprime( plus_plus( int, times_times( int,
% 0.81/1.21 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.81/1.21 ) ) }.
% 0.81/1.21 (1296) {G0,W17,D9,L1,V0,M1} { twoSqu33214720sum2sq( times_times( int,
% 0.81/1.21 plus_plus( int, times_times( int, number_number_of( int, bit0( bit0( bit1
% 0.81/1.21 ( pls ) ) ) ), m ), one_one( int ) ), t ) ) }.
% 0.81/1.21 (1297) {G0,W4,D2,L1,V1,M1} { ord_less_eq( int, X, X ) }.
% 0.81/1.21 (1298) {G0,W5,D3,L1,V1,M1} { number_number_of( int, X ) = X }.
% 0.81/1.21 (1299) {G0,W9,D3,L1,V2,M1} { times_times( int, X, Y ) = times_times( int,
% 0.81/1.21 Y, X ) }.
% 0.81/1.21 (1300) {G0,W8,D2,L2,V2,M2} { ord_less_eq( int, X, Y ), ord_less_eq( int, Y
% 0.81/1.21 , X ) }.
% 0.81/1.21 (1301) {G0,W15,D4,L1,V2,M1} { times_times( int, number_number_of( int, X )
% 0.81/1.21 , number_number_of( int, Y ) ) = number_number_of( int, times_times( int
% 0.81/1.21 , X, Y ) ) }.
% 0.81/1.21 (1302) {G0,W12,D3,L2,V2,M2} { ! ord_less_eq( int, number_number_of( int, X
% 0.81/1.21 ), number_number_of( int, Y ) ), ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1303) {G0,W12,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , number_number_of( int, X ), number_number_of( int, Y ) ) }.
% 0.81/1.21 (1304) {G0,W16,D3,L4,V3,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.21 ! ord_less_eq( X, number_number_of( X, Y ), number_number_of( X, Z ) ),
% 0.81/1.21 ord_less_eq( int, Y, Z ) }.
% 0.81/1.21 (1305) {G0,W16,D3,L4,V3,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.21 ! ord_less_eq( int, Y, Z ), ord_less_eq( X, number_number_of( X, Y ),
% 0.81/1.21 number_number_of( X, Z ) ) }.
% 0.81/1.21 (1306) {G0,W15,D4,L1,V3,M1} { times_times( int, times_times( int, X, Y ),
% 0.81/1.21 Z ) = times_times( int, X, times_times( int, Y, Z ) ) }.
% 0.81/1.21 (1307) {G0,W12,D2,L3,V3,M3} { ! ord_less_eq( int, X, Y ), ! ord_less_eq(
% 0.81/1.21 int, Y, Z ), ord_less_eq( int, X, Z ) }.
% 0.81/1.21 (1308) {G0,W11,D2,L3,V2,M3} { ! ord_less_eq( int, X, Y ), ! ord_less_eq(
% 0.81/1.21 int, Y, X ), X = Y }.
% 0.81/1.21 (1309) {G0,W18,D4,L1,V3,M1} { power_power( int, X, plus_plus( nat, Y, Z )
% 0.81/1.21 ) = times_times( int, power_power( int, X, Y ), power_power( int, X, Z )
% 0.81/1.21 ) }.
% 0.81/1.21 (1310) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit1( Y ) ),
% 0.81/1.21 ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1311) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , bit1( X ), bit1( Y ) ) }.
% 0.81/1.21 (1312) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit1( Y ) ),
% 0.81/1.21 ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1313) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , bit1( X ), bit1( Y ) ) }.
% 0.81/1.21 (1314) {G0,W4,D2,L1,V0,M1} { ord_less_eq( int, pls, pls ) }.
% 0.81/1.21 (1315) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit0( Y ) ),
% 0.81/1.21 ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1316) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , bit0( X ), bit0( Y ) ) }.
% 0.81/1.21 (1317) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit0( Y ) ),
% 0.81/1.21 ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1318) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , bit0( X ), bit0( Y ) ) }.
% 0.81/1.21 (1319) {G0,W8,D2,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int, X
% 0.81/1.21 , Y ) }.
% 0.81/1.21 (1320) {G0,W7,D2,L2,V2,M2} { ! ord_less( int, X, Y ), ! X = Y }.
% 0.81/1.21 (1321) {G0,W11,D2,L3,V2,M3} { ! ord_less_eq( int, X, Y ), X = Y, ord_less
% 0.81/1.21 ( int, X, Y ) }.
% 0.81/1.21 (1322) {G0,W14,D3,L2,V3,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , plus_plus( int, Z, X ), plus_plus( int, Z, Y ) ) }.
% 0.81/1.21 (1323) {G0,W10,D3,L2,V1,M2} { ! number_number_of( nat, X ) = zero_zero(
% 0.81/1.21 nat ), ord_less_eq( int, X, pls ) }.
% 0.81/1.21 (1324) {G0,W10,D3,L2,V1,M2} { ! ord_less_eq( int, X, pls ),
% 0.81/1.21 number_number_of( nat, X ) = zero_zero( nat ) }.
% 0.81/1.21 (1325) {G0,W10,D3,L2,V1,M2} { ! zero_zero( nat ) = number_number_of( nat,
% 0.81/1.21 X ), ord_less_eq( int, X, pls ) }.
% 0.81/1.21 (1326) {G0,W10,D3,L2,V1,M2} { ! ord_less_eq( int, X, pls ), zero_zero( nat
% 0.81/1.21 ) = number_number_of( nat, X ) }.
% 0.81/1.21 (1327) {G0,W25,D4,L4,V3,M4} { ! number_semiring( X ), ! ord_less_eq( int,
% 0.81/1.21 pls, Y ), ! ord_less_eq( int, pls, Z ), times_times( X, number_number_of
% 0.81/1.21 ( X, Y ), number_number_of( X, Z ) ) = number_number_of( X, times_times(
% 0.81/1.21 int, Y, Z ) ) }.
% 0.81/1.21 (1328) {G0,W23,D5,L2,V4,M2} { ! number_ring( X ), times_times( X,
% 0.81/1.21 number_number_of( X, Y ), times_times( X, number_number_of( X, Z ), T ) )
% 0.81/1.21 = times_times( X, number_number_of( X, times_times( int, Y, Z ) ), T )
% 0.81/1.21 }.
% 0.81/1.21 (1329) {G0,W17,D4,L2,V3,M2} { ! number_ring( X ), times_times( X,
% 0.81/1.21 number_number_of( X, Y ), number_number_of( X, Z ) ) = number_number_of(
% 0.81/1.21 X, times_times( int, Y, Z ) ) }.
% 0.81/1.21 (1330) {G0,W17,D4,L2,V3,M2} { ! number_ring( X ), number_number_of( X,
% 0.81/1.21 times_times( int, Y, Z ) ) = times_times( X, number_number_of( X, Y ),
% 0.81/1.21 number_number_of( X, Z ) ) }.
% 0.81/1.21 (1331) {G0,W22,D4,L3,V3,M3} { ! linord581940658strict( X ), ! ord_less_eq
% 0.81/1.21 ( X, plus_plus( X, times_times( X, Y, Y ), times_times( X, Z, Z ) ),
% 0.81/1.21 zero_zero( X ) ), ti( X, Y ) = zero_zero( X ) }.
% 0.81/1.21 (1332) {G0,W22,D4,L3,V3,M3} { ! linord581940658strict( X ), ! ord_less_eq
% 0.81/1.21 ( X, plus_plus( X, times_times( X, Y, Y ), times_times( X, Z, Z ) ),
% 0.81/1.21 zero_zero( X ) ), ti( X, Z ) = zero_zero( X ) }.
% 0.81/1.21 (1333) {G0,W28,D4,L4,V3,M4} { ! linord581940658strict( X ), ! ti( X, Y ) =
% 0.81/1.21 zero_zero( X ), ! ti( X, Z ) = zero_zero( X ), ord_less_eq( X, plus_plus
% 0.81/1.21 ( X, times_times( X, Y, Y ), times_times( X, Z, Z ) ), zero_zero( X ) )
% 0.81/1.21 }.
% 0.81/1.21 (1334) {G0,W16,D4,L2,V3,M2} { ! linordered_ring( X ), ord_less_eq( X,
% 0.81/1.21 zero_zero( X ), plus_plus( X, times_times( X, Y, Y ), times_times( X, Z,
% 0.81/1.21 Z ) ) ) }.
% 0.81/1.21 (1335) {G0,W15,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.21 ! ord_less_eq( X, number_number_of( X, Y ), zero_zero( X ) ), ord_less_eq
% 0.81/1.21 ( int, Y, pls ) }.
% 0.81/1.21 (1336) {G0,W15,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.21 ! ord_less_eq( int, Y, pls ), ord_less_eq( X, number_number_of( X, Y ),
% 0.81/1.21 zero_zero( X ) ) }.
% 0.81/1.21 (1337) {G0,W15,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.21 ! ord_less_eq( X, zero_zero( X ), number_number_of( X, Y ) ), ord_less_eq
% 0.81/1.21 ( int, pls, Y ) }.
% 0.81/1.21 (1338) {G0,W15,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.21 ! ord_less_eq( int, pls, Y ), ord_less_eq( X, zero_zero( X ),
% 0.81/1.21 number_number_of( X, Y ) ) }.
% 0.81/1.21 (1339) {G0,W11,D3,L2,V1,M2} { ! ord_less( nat, zero_zero( nat ),
% 0.81/1.21 number_number_of( nat, X ) ), ord_less( int, pls, X ) }.
% 0.81/1.21 (1340) {G0,W11,D3,L2,V1,M2} { ! ord_less( int, pls, X ), ord_less( nat,
% 0.81/1.21 zero_zero( nat ), number_number_of( nat, X ) ) }.
% 0.81/1.21 (1341) {G0,W20,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), !
% 0.81/1.21 ord_less_eq( X, number_number_of( X, Y ), number_number_of( X, Z ) ), !
% 0.81/1.21 ord_less( X, number_number_of( X, Z ), number_number_of( X, Y ) ) }.
% 0.81/1.21 (1342) {G0,W20,D3,L4,V3,M4} { ! number( X ), ! linorder( X ), ord_less( X
% 0.81/1.21 , number_number_of( X, Z ), number_number_of( X, Y ) ), ord_less_eq( X,
% 0.81/1.21 number_number_of( X, Y ), number_number_of( X, Z ) ) }.
% 0.81/1.21 (1343) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, bit1( X ) ),
% 0.81/1.21 ord_less_eq( int, pls, X ) }.
% 0.81/1.21 (1344) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, X ), ord_less_eq(
% 0.81/1.21 int, pls, bit1( X ) ) }.
% 0.81/1.21 (1345) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit1( Y ) ),
% 0.81/1.21 ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1346) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , bit0( X ), bit1( Y ) ) }.
% 0.81/1.21 (1347) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit0( X ), bit1( Y ) ),
% 0.81/1.21 ord_less_eq( int, X, Y ) }.
% 0.81/1.21 (1348) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less_eq( int
% 0.81/1.21 , bit0( X ), bit1( Y ) ) }.
% 0.81/1.21 (1349) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, bit0( X ), pls ),
% 0.81/1.21 ord_less_eq( int, X, pls ) }.
% 0.81/1.22 (1350) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, X, pls ), ord_less_eq(
% 0.81/1.22 int, bit0( X ), pls ) }.
% 0.81/1.22 (1351) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, bit0( X ) ),
% 0.81/1.22 ord_less_eq( int, pls, X ) }.
% 0.81/1.22 (1352) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, X ), ord_less_eq(
% 0.81/1.22 int, pls, bit0( X ) ) }.
% 0.81/1.22 (1353) {G0,W18,D3,L3,V4,M3} { ! ord_less( int, X, Y ), ! ord_less_eq( int
% 0.81/1.22 , Z, T ), ord_less( int, plus_plus( int, X, Z ), plus_plus( int, Y, T ) )
% 0.81/1.22 }.
% 0.81/1.22 (1354) {G0,W6,D3,L1,V0,M1} { number_number_of( nat, pls ) = zero_zero( nat
% 0.81/1.22 ) }.
% 0.81/1.22 (1355) {G0,W6,D3,L1,V0,M1} { zero_zero( nat ) = number_number_of( nat, pls
% 0.81/1.22 ) }.
% 0.81/1.22 (1356) {G0,W16,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.22 ! ord_less_eq( X, number_number_of( X, Y ), one_one( X ) ), ord_less_eq(
% 0.81/1.22 int, Y, bit1( pls ) ) }.
% 0.81/1.22 (1357) {G0,W16,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.22 ! ord_less_eq( int, Y, bit1( pls ) ), ord_less_eq( X, number_number_of( X
% 0.81/1.22 , Y ), one_one( X ) ) }.
% 0.81/1.22 (1358) {G0,W16,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.22 ! ord_less_eq( X, one_one( X ), number_number_of( X, Y ) ), ord_less_eq(
% 0.81/1.22 int, bit1( pls ), Y ) }.
% 0.81/1.22 (1359) {G0,W16,D3,L4,V2,M4} { ! number_ring( X ), ! linordered_idom( X ),
% 0.81/1.22 ! ord_less_eq( int, bit1( pls ), Y ), ord_less_eq( X, one_one( X ),
% 0.81/1.22 number_number_of( X, Y ) ) }.
% 0.81/1.22 (1360) {G0,W12,D5,L1,V0,M1} { plus_plus( nat, one_one( nat ), one_one( nat
% 0.81/1.22 ) ) = number_number_of( nat, bit0( bit1( pls ) ) ) }.
% 0.81/1.22 (1361) {G0,W6,D3,L1,V1,M1} { times_times( int, pls, X ) = pls }.
% 0.81/1.22 (1362) {G0,W11,D4,L1,V2,M1} { times_times( int, bit0( X ), Y ) = bit0(
% 0.81/1.22 times_times( int, X, Y ) ) }.
% 0.81/1.22 (1363) {G0,W12,D3,L2,V2,M2} { ! ord_less( int, number_number_of( int, X )
% 0.81/1.22 , number_number_of( int, Y ) ), ord_less( int, X, Y ) }.
% 0.81/1.22 (1364) {G0,W12,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less( int,
% 0.81/1.22 number_number_of( int, X ), number_number_of( int, Y ) ) }.
% 0.81/1.22 (1365) {G0,W7,D4,L1,V1,M1} { times_times( int, X, one_one( int ) ) = X }.
% 0.81/1.22 (1366) {G0,W7,D4,L1,V1,M1} { times_times( int, one_one( int ), X ) = X }.
% 0.81/1.22 (1367) {G0,W15,D4,L1,V2,M1} { plus_plus( int, number_number_of( int, X ),
% 0.81/1.22 number_number_of( int, Y ) ) = number_number_of( int, plus_plus( int, X,
% 0.81/1.22 Y ) ) }.
% 0.81/1.22 (1368) {G0,W18,D4,L1,V3,M1} { times_times( int, plus_plus( int, X, Y ), Z
% 0.81/1.22 ) = plus_plus( int, times_times( int, X, Z ), times_times( int, Y, Z ) )
% 0.81/1.22 }.
% 0.81/1.22 (1369) {G0,W18,D4,L1,V3,M1} { times_times( int, X, plus_plus( int, Y, Z )
% 0.81/1.22 ) = plus_plus( int, times_times( int, X, Y ), times_times( int, X, Z ) )
% 0.81/1.22 }.
% 0.81/1.22 (1370) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, bit1( X ), pls ),
% 0.81/1.22 ord_less( int, X, pls ) }.
% 0.81/1.22 (1371) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, X, pls ), ord_less_eq( int,
% 0.81/1.22 bit1( X ), pls ) }.
% 0.81/1.22 (1372) {G0,W9,D3,L2,V1,M2} { ! ord_less( int, pls, bit1( X ) ),
% 0.81/1.22 ord_less_eq( int, pls, X ) }.
% 0.81/1.22 (1373) {G0,W9,D3,L2,V1,M2} { ! ord_less_eq( int, pls, X ), ord_less( int,
% 0.81/1.22 pls, bit1( X ) ) }.
% 0.81/1.22 (1374) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit0( Y ) ),
% 0.81/1.22 ord_less( int, X, Y ) }.
% 0.81/1.22 (1375) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.81/1.22 bit1( X ), bit0( Y ) ) }.
% 0.81/1.22 (1376) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, bit1( X ), bit0( Y ) ),
% 0.81/1.22 ord_less( int, X, Y ) }.
% 0.81/1.22 (1377) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.81/1.22 bit1( X ), bit0( Y ) ) }.
% 0.81/1.22 (1378) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit0( X ), bit1( Y ) ),
% 0.81/1.22 ord_less_eq( int, X, Y ) }.
% 0.81/1.22 (1379) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less( int,
% 0.81/1.22 bit0( X ), bit1( Y ) ) }.
% 0.81/1.22 (1380) {G0,W10,D3,L2,V2,M2} { ! ord_less( int, bit0( X ), bit1( Y ) ),
% 0.81/1.22 ord_less_eq( int, X, Y ) }.
% 0.81/1.22 (1381) {G0,W10,D3,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less( int,
% 0.81/1.22 bit0( X ), bit1( Y ) ) }.
% 0.81/1.22 (1382) {G0,W11,D3,L2,V2,M2} { ! ord_less( nat, number_number_of( nat, X )
% 0.81/1.22 , number_number_of( nat, Y ) ), alpha1( X, Y ) }.
% 0.81/1.22 (1383) {G0,W12,D3,L2,V2,M2} { ! ord_less( nat, number_number_of( nat, X )
% 0.81/1.22 , number_number_of( nat, Y ) ), ord_less( int, X, Y ) }.
% 0.81/1.22 (1384) {G0,W15,D3,L3,V2,M3} { ! alpha1( X, Y ), ! ord_less( int, X, Y ),
% 0.81/1.22 ord_less( nat, number_number_of( nat, X ), number_number_of( nat, Y ) )
% 0.81/1.22 }.
% 0.81/1.22 (1385) {G0,W11,D2,L3,V2,M3} { ! alpha1( X, Y ), ! ord_less( int, X, Y ),
% 0.81/1.22 ord_less( int, pls, Y ) }.
% 0.81/1.22 (1386) {G0,W7,D2,L2,V2,M2} { ord_less( int, X, Y ), alpha1( X, Y ) }.
% 0.81/1.22 (1387) {G0,W7,D2,L2,V2,M2} { ! ord_less( int, pls, Y ), alpha1( X, Y ) }.
% 0.81/1.22 (1388) {G0,W10,D3,L2,V1,M2} { ! ord_less_eq( int, one_one( int ), X ),
% 0.81/1.22 ord_less( int, zero_zero( int ), X ) }.
% 0.81/1.22 (1389) {G0,W10,D3,L2,V1,M2} { ! ord_less( int, zero_zero( int ), X ),
% 0.81/1.22 ord_less_eq( int, one_one( int ), X ) }.
% 0.81/1.22 (1390) {G0,W7,D4,L1,V0,M1} { number_number_of( nat, bit1( pls ) ) =
% 0.81/1.22 one_one( nat ) }.
% 0.81/1.22 (1391) {G0,W7,D4,L1,V0,M1} { one_one( nat ) = number_number_of( nat, bit1
% 0.81/1.22 ( pls ) ) }.
% 0.81/1.22 (1392) {G0,W12,D4,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.81/1.22 plus_plus( int, X, one_one( int ) ), Y ) }.
% 0.81/1.22 (1393) {G0,W12,D4,L2,V2,M2} { ! ord_less_eq( int, plus_plus( int, X,
% 0.81/1.22 one_one( int ) ), Y ), ord_less( int, X, Y ) }.
% 0.81/1.22 (1394) {G0,W12,D4,L2,V2,M2} { ! ord_less( int, X, Y ), ord_less_eq( int,
% 0.81/1.22 plus_plus( int, X, one_one( int ) ), Y ) }.
% 0.81/1.22 (1395) {G0,W12,D4,L2,V2,M2} { ! ord_less( int, X, plus_plus( int, Y,
% 0.81/1.22 one_one( int ) ) ), ord_less_eq( int, X, Y ) }.
% 0.81/1.22 (1396) {G0,W12,D4,L2,V2,M2} { ! ord_less_eq( int, X, Y ), ord_less( int, X
% 0.81/1.22 , plus_plus( int, Y, one_one( int ) ) ) }.
% 0.81/1.22 (1397) {G0,W25,D4,L4,V3,M4} { ! number_semiring( X ), ! ord_less_eq( int,
% 0.81/1.22 pls, Y ), ! ord_less_eq( int, pls, Z ), plus_plus( X, number_number_of( X
% 0.81/1.22 , Y ), number_number_of( X, Z ) ) = number_number_of( X, plus_plus( int,
% 0.81/1.22 Y, Z ) ) }.
% 0.81/1.22 (1398) {G0,W16,D4,L2,V2,M2} { ! ord_less( int, Y, pls ), plus_plus( nat,
% 0.81/1.22 number_number_of( nat, Y ), number_number_of( nat, X ) ) =
% 0.81/1.22 number_number_of( nat, X ) }.
% 0.81/1.22 (1399) {G0,W20,D4,L3,V2,M3} { ord_less( int, Y, pls ), ! ord_less( int, X
% 0.81/1.22 , pls ), plus_plus( nat, number_number_of( nat, Y ), number_number_of(
% 0.81/1.22 nat, X ) ) = number_number_of( nat, Y ) }.
% 0.81/1.22 (1400) {G0,W23,D4,L3,V2,M3} { ord_less( int, Y, pls ), ord_less( int, X,
% 0.81/1.22 pls ), plus_plus( nat, number_number_of( nat, Y ), number_number_of( nat
% 0.81/1.22 , X ) ) = number_number_of( nat, plus_plus( int, Y, X ) ) }.
% 0.81/1.22 (1401) {G0,W14,D4,L2,V1,M2} { ! ord_less_eq( int, zero_zero( int ), X ),
% 0.81/1.22 ord_less( int, zero_zero( int ), plus_plus( int, one_one( int ), X ) )
% 0.81/1.22 }.
% 0.81/1.22 (1402) {G0,W14,D3,L4,V3,M4} { ! number_ring( X ), ! ring_char_0( X ), !
% 0.81/1.22 number_number_of( X, Y ) = number_number_of( X, Z ), Y = Z }.
% 0.81/1.22 (1403) {G0,W14,D3,L4,V3,M4} { ! number_ring( X ), ! ring_char_0( X ), ! Y
% 0.81/1.22 = Z, number_number_of( X, Y ) = number_number_of( X, Z ) }.
% 0.81/1.22 (1404) {G0,W16,D3,L3,V3,M3} { ! number( X ), ! number_number_of( X, Y ) =
% 0.81/1.22 ti( X, Z ), ti( X, Z ) = number_number_of( X, Y ) }.
% 0.81/1.22 (1405) {G0,W16,D3,L3,V3,M3} { ! number( X ), ! ti( X, Z ) =
% 0.81/1.22 number_number_of( X, Y ), number_number_of( X, Y ) = ti( X, Z ) }.
% 0.81/1.22 (1406) {G0,W8,D3,L2,V2,M2} { ! bit1( X ) = bit1( Y ), X = Y }.
% 0.81/1.22 (1407) {G0,W8,D3,L2,V2,M2} { ! X = Y, bit1( X ) = bit1( Y ) }.
% 0.81/1.22 (1408) {G0,W8,D3,L2,V2,M2} { ! bit0( X ) = bit0( Y ), X = Y }.
% 0.81/1.22 (1409) {G0,W8,D3,L2,V2,M2} { ! X = Y, bit0( X ) = bit0( Y ) }.
% 0.81/1.22 (1410) {G0,W11,D2,L3,V2,M3} { ord_less( int, X, Y ), X = Y, ord_less( int
% 0.81/1.22 , Y, X ) }.
% 0.81/1.22 (1411) {G0,W21,D4,L3,V3,M3} { ! linord581940658strict( X ), ! plus_plus( X
% 0.81/1.22 , times_times( X, Y, Y ), times_times( X, Z, Z ) ) = zero_zero( X ), ti(
% 0.81/1.22 X, Y ) = zero_zero( X ) }.
% 0.81/1.22 (1412) {G0,W21,D4,L3,V3,M3} { ! linord581940658strict( X ), ! plus_plus( X
% 0.81/1.22 , times_times( X, Y, Y ), times_times( X, Z, Z ) ) = zero_zero( X ), ti(
% 0.81/1.22 X, Z ) = zero_zero( X ) }.
% 0.81/1.22 (1413) {G0,W27,D4,L4,V3,M4} { ! linord581940658strict( X ), ! ti( X, Y ) =
% 0.81/1.22 zero_zero( X ), ! ti( X, Z ) = zero_zero( X ), plus_plus( X, times_times
% 0.81/1.22 ( X, Y, Y ), times_times( X, Z, Z ) ) = zero_zero( X ) }.
% 0.81/1.22 (1414) {G0,W28,D5,L3,V4,M3} { ! number( X ), ! semiring( X ), times_times
% 0.81/1.22 ( X, plus_plus( X, Y, Z ), number_number_of( X, T ) ) = plus_plus( X,
% 0.81/1.22 times_times( X, Y, number_number_of( X, T ) ), times_times( X, Z,
% 0.81/1.22 number_number_of( X, T ) ) ) }.
% 0.81/1.22 (1415) {G0,W28,D5,L3,V4,M3} { ! number( X ), ! semiring( X ), times_times
% 0.81/1.22 ( X, number_number_of( X, Y ), plus_plus( X, Z, T ) ) = plus_plus( X,
% 0.81/1.22 times_times( X, number_number_of( X, Y ), Z ), times_times( X,
% 0.81/1.22 number_number_of( X, Y ), T ) ) }.
% 0.81/1.22 (1416) {G0,W15,D4,L1,V3,M1} { plus_plus( int, plus_plus( int, X, Y ), Z )
% 0.81/1.22 = plus_plus( int, X, plus_plus( int, Y, Z ) ) }.
% 0.81/1.22 (1417) {G0,W15,D4,L1,V3,M1} { plus_plus( int, X, plus_plus( int, Y, Z ) )
% 0.81/1.22 = plus_plus( int, Y, plus_plus( int, X, Z ) ) }.
% 0.81/1.22 (1418) {G0,W9,D3,L1,V2,M1} { plus_plus( int, X, Y ) = plus_plus( int, Y, X
% 0.81/1.22 ) }.
% 0.81/1.22 (1419) {G0,W6,D3,L1,V0,M1} { zero_zero( int ) = number_number_of( int, pls
% 0.81/1.22 ) }.
% 0.81/1.22 (1420) {G0,W2,D2,L1,V0,M1} { ring_11004092258visors( int ) }.
% 0.81/1.22 (1421) {G0,W2,D2,L1,V0,M1} { linord581940658strict( int ) }.
% 0.81/1.22 (1422) {G0,W2,D2,L1,V0,M1} { linordered_ring( int ) }.
% 0.81/1.22 (1423) {G0,W2,D2,L1,V0,M1} { linordered_idom( int ) }.
% 0.81/1.22 (1424) {G0,W2,D2,L1,V0,M1} { number_semiring( int ) }.
% 0.81/1.22 (1425) {G0,W2,D2,L1,V0,M1} { linorder( int ) }.
% 0.81/1.22 (1426) {G0,W2,D2,L1,V0,M1} { semiring_1( int ) }.
% 0.81/1.22 (1427) {G0,W2,D2,L1,V0,M1} { ring_char_0( int ) }.
% 0.81/1.22 (1428) {G0,W2,D2,L1,V0,M1} { number_ring( int ) }.
% 0.81/1.22 (1429) {G0,W2,D2,L1,V0,M1} { semiring( int ) }.
% 0.81/1.22 (1430) {G0,W2,D2,L1,V0,M1} { number( int ) }.
% 0.81/1.22 (1431) {G0,W2,D2,L1,V0,M1} { number_semiring( nat ) }.
% 0.81/1.22 (1432) {G0,W2,D2,L1,V0,M1} { linorder( nat ) }.
% 0.81/1.22 (1433) {G0,W2,D2,L1,V0,M1} { semiring_1( nat ) }.
% 0.81/1.22 (1434) {G0,W2,D2,L1,V0,M1} { semiring( nat ) }.
% 0.81/1.22 (1435) {G0,W2,D2,L1,V0,M1} { number( nat ) }.
% 0.81/1.22 (1436) {G0,W9,D4,L1,V2,M1} { ti( X, ti( X, Y ) ) = ti( X, Y ) }.
% 0.81/1.22 (1437) {G0,W16,D7,L1,V0,M1} { ! ord_less( int, plus_plus( int, power_power
% 0.81/1.22 ( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int )
% 0.81/1.22 ), zero_zero( int ) ) }.
% 0.81/1.22
% 0.81/1.22
% 0.81/1.22 Total Proof:
% 0.81/1.22
% 0.81/1.22 subsumption: (51) {G0,W35,D9,L1,V0,M1} I { ord_less( int, times_times( int
% 0.81/1.22 , plus_plus( int, times_times( int, number_number_of( int, bit0( bit0(
% 0.81/1.22 bit1( pls ) ) ) ), m ), one_one( int ) ), t ), times_times( int,
% 0.81/1.22 plus_plus( int, times_times( int, number_number_of( int, bit0( bit0( bit1
% 0.81/1.22 ( pls ) ) ) ), m ), one_one( int ) ), zero_zero( int ) ) ) }.
% 0.81/1.22 parent0: (1272) {G0,W35,D9,L1,V0,M1} { ord_less( int, times_times( int,
% 0.81/1.22 plus_plus( int, times_times( int, number_number_of( int, bit0( bit0( bit1
% 0.81/1.22 ( pls ) ) ) ), m ), one_one( int ) ), t ), times_times( int, plus_plus(
% 0.81/1.22 int, times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) )
% 0.81/1.22 ), m ), one_one( int ) ), zero_zero( int ) ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 eqswap: (1496) {G0,W29,D9,L1,V0,M1} { times_times( int, plus_plus( int,
% 0.81/1.22 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.81/1.22 ), one_one( int ) ), t ) = plus_plus( int, power_power( int, s,
% 0.81/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) }.
% 0.81/1.22 parent0[0]: (1273) {G0,W29,D9,L1,V0,M1} { plus_plus( int, power_power( int
% 0.81/1.22 , s, number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) =
% 0.81/1.22 times_times( int, plus_plus( int, times_times( int, number_number_of( int
% 0.81/1.22 , bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int ) ), t ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (52) {G0,W29,D9,L1,V0,M1} I { times_times( int, plus_plus( int
% 0.81/1.22 , times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) )
% 0.81/1.22 , m ), one_one( int ) ), t ) ==> plus_plus( int, power_power( int, s,
% 0.81/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) }.
% 0.81/1.22 parent0: (1496) {G0,W29,D9,L1,V0,M1} { times_times( int, plus_plus( int,
% 0.81/1.22 times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m
% 0.81/1.22 ), one_one( int ) ), t ) = plus_plus( int, power_power( int, s,
% 0.81/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 *** allocated 113905 integers for clauses
% 0.81/1.22 subsumption: (77) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 0.81/1.22 }.
% 0.81/1.22 parent0: (1298) {G0,W5,D3,L1,V1,M1} { number_number_of( int, X ) = X }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (78) {G0,W9,D3,L1,V2,M1} I { times_times( int, X, Y ) =
% 0.81/1.22 times_times( int, Y, X ) }.
% 0.81/1.22 parent0: (1299) {G0,W9,D3,L1,V2,M1} { times_times( int, X, Y ) =
% 0.81/1.22 times_times( int, Y, X ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 Y := Y
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (126) {G0,W6,D3,L1,V1,M1} I { times_times( int, pls, X ) ==>
% 0.81/1.22 pls }.
% 0.81/1.22 parent0: (1361) {G0,W6,D3,L1,V1,M1} { times_times( int, pls, X ) = pls }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (127) {G0,W11,D4,L1,V2,M1} I { times_times( int, bit0( X ), Y
% 0.81/1.22 ) ==> bit0( times_times( int, X, Y ) ) }.
% 0.81/1.22 parent0: (1362) {G0,W11,D4,L1,V2,M1} { times_times( int, bit0( X ), Y ) =
% 0.81/1.22 bit0( times_times( int, X, Y ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 Y := Y
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 *** allocated 50625 integers for termspace/termends
% 0.81/1.22 paramod: (2270) {G1,W4,D3,L1,V0,M1} { zero_zero( int ) = pls }.
% 0.81/1.22 parent0[0]: (77) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 0.81/1.22 }.
% 0.81/1.22 parent1[0; 3]: (1419) {G0,W6,D3,L1,V0,M1} { zero_zero( int ) =
% 0.81/1.22 number_number_of( int, pls ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := pls
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (174) {G1,W4,D3,L1,V0,M1} I;d(77) { zero_zero( int ) ==> pls
% 0.81/1.22 }.
% 0.81/1.22 parent0: (2270) {G1,W4,D3,L1,V0,M1} { zero_zero( int ) = pls }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2700) {G1,W15,D7,L1,V0,M1} { ! ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), pls ) }.
% 0.81/1.22 parent0[0]: (174) {G1,W4,D3,L1,V0,M1} I;d(77) { zero_zero( int ) ==> pls
% 0.81/1.22 }.
% 0.81/1.22 parent1[0; 15]: (1437) {G0,W16,D7,L1,V0,M1} { ! ord_less( int, plus_plus(
% 0.81/1.22 int, power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.22 , one_one( int ) ), zero_zero( int ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (192) {G2,W15,D7,L1,V0,M1} I;d(174) { ! ord_less( int,
% 0.81/1.22 plus_plus( int, power_power( int, s, number_number_of( nat, bit0( bit1(
% 0.81/1.22 pls ) ) ) ), one_one( int ) ), pls ) }.
% 0.81/1.22 parent0: (2700) {G1,W15,D7,L1,V0,M1} { ! ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), pls ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 eqswap: (2701) {G0,W6,D3,L1,V1,M1} { pls ==> times_times( int, pls, X )
% 0.81/1.22 }.
% 0.81/1.22 parent0[0]: (126) {G0,W6,D3,L1,V1,M1} I { times_times( int, pls, X ) ==>
% 0.81/1.22 pls }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2702) {G1,W6,D3,L1,V1,M1} { pls ==> times_times( int, X, pls )
% 0.81/1.22 }.
% 0.81/1.22 parent0[0]: (78) {G0,W9,D3,L1,V2,M1} I { times_times( int, X, Y ) =
% 0.81/1.22 times_times( int, Y, X ) }.
% 0.81/1.22 parent1[0; 2]: (2701) {G0,W6,D3,L1,V1,M1} { pls ==> times_times( int, pls
% 0.81/1.22 , X ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := pls
% 0.81/1.22 Y := X
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 X := X
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 eqswap: (2705) {G1,W6,D3,L1,V1,M1} { times_times( int, X, pls ) ==> pls
% 0.81/1.22 }.
% 0.81/1.22 parent0[0]: (2702) {G1,W6,D3,L1,V1,M1} { pls ==> times_times( int, X, pls
% 0.81/1.22 ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (1118) {G1,W6,D3,L1,V1,M1} P(78,126) { times_times( int, X,
% 0.81/1.22 pls ) ==> pls }.
% 0.81/1.22 parent0: (2705) {G1,W6,D3,L1,V1,M1} { times_times( int, X, pls ) ==> pls
% 0.81/1.22 }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := X
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 0 ==> 0
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2712) {G1,W31,D9,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), times_times( int, plus_plus( int, times_times( int,
% 0.81/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.81/1.22 ), zero_zero( int ) ) ) }.
% 0.81/1.22 parent0[0]: (52) {G0,W29,D9,L1,V0,M1} I { times_times( int, plus_plus( int
% 0.81/1.22 , times_times( int, number_number_of( int, bit0( bit0( bit1( pls ) ) ) )
% 0.81/1.22 , m ), one_one( int ) ), t ) ==> plus_plus( int, power_power( int, s,
% 0.81/1.22 number_number_of( nat, bit0( bit1( pls ) ) ) ), one_one( int ) ) }.
% 0.81/1.22 parent1[0; 2]: (51) {G0,W35,D9,L1,V0,M1} I { ord_less( int, times_times(
% 0.81/1.22 int, plus_plus( int, times_times( int, number_number_of( int, bit0( bit0
% 0.81/1.22 ( bit1( pls ) ) ) ), m ), one_one( int ) ), t ), times_times( int,
% 0.81/1.22 plus_plus( int, times_times( int, number_number_of( int, bit0( bit0( bit1
% 0.81/1.22 ( pls ) ) ) ), m ), one_one( int ) ), zero_zero( int ) ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2713) {G1,W29,D8,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), times_times( int, plus_plus( int, times_times( int,
% 0.81/1.22 bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) ), zero_zero( int ) ) )
% 0.81/1.22 }.
% 0.81/1.22 parent0[0]: (77) {G0,W5,D3,L1,V1,M1} I { number_number_of( int, X ) ==> X
% 0.81/1.22 }.
% 0.81/1.22 parent1[0; 20]: (2712) {G1,W31,D9,L1,V0,M1} { ord_less( int, plus_plus(
% 0.81/1.22 int, power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.22 , one_one( int ) ), times_times( int, plus_plus( int, times_times( int,
% 0.81/1.22 number_number_of( int, bit0( bit0( bit1( pls ) ) ) ), m ), one_one( int )
% 0.81/1.22 ), zero_zero( int ) ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := bit0( bit0( bit1( pls ) ) )
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2714) {G1,W29,D8,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), times_times( int, plus_plus( int, bit0( times_times(
% 0.81/1.22 int, bit0( bit1( pls ) ), m ) ), one_one( int ) ), zero_zero( int ) ) )
% 0.81/1.22 }.
% 0.81/1.22 parent0[0]: (127) {G0,W11,D4,L1,V2,M1} I { times_times( int, bit0( X ), Y )
% 0.81/1.22 ==> bit0( times_times( int, X, Y ) ) }.
% 0.81/1.22 parent1[0; 18]: (2713) {G1,W29,D8,L1,V0,M1} { ord_less( int, plus_plus(
% 0.81/1.22 int, power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.22 , one_one( int ) ), times_times( int, plus_plus( int, times_times( int,
% 0.81/1.22 bit0( bit0( bit1( pls ) ) ), m ), one_one( int ) ), zero_zero( int ) ) )
% 0.81/1.22 }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := bit0( bit1( pls ) )
% 0.81/1.22 Y := m
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2716) {G1,W29,D8,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), times_times( int, plus_plus( int, bit0( bit0(
% 0.81/1.22 times_times( int, bit1( pls ), m ) ) ), one_one( int ) ), zero_zero( int
% 0.81/1.22 ) ) ) }.
% 0.81/1.22 parent0[0]: (127) {G0,W11,D4,L1,V2,M1} I { times_times( int, bit0( X ), Y )
% 0.81/1.22 ==> bit0( times_times( int, X, Y ) ) }.
% 0.81/1.22 parent1[0; 19]: (2714) {G1,W29,D8,L1,V0,M1} { ord_less( int, plus_plus(
% 0.81/1.22 int, power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.22 , one_one( int ) ), times_times( int, plus_plus( int, bit0( times_times(
% 0.81/1.22 int, bit0( bit1( pls ) ), m ) ), one_one( int ) ), zero_zero( int ) ) )
% 0.81/1.22 }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := bit1( pls )
% 0.81/1.22 Y := m
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2717) {G2,W28,D8,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), times_times( int, plus_plus( int, bit0( bit0(
% 0.81/1.22 times_times( int, bit1( pls ), m ) ) ), one_one( int ) ), pls ) ) }.
% 0.81/1.22 parent0[0]: (174) {G1,W4,D3,L1,V0,M1} I;d(77) { zero_zero( int ) ==> pls
% 0.81/1.22 }.
% 0.81/1.22 parent1[0; 27]: (2716) {G1,W29,D8,L1,V0,M1} { ord_less( int, plus_plus(
% 0.81/1.22 int, power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.22 , one_one( int ) ), times_times( int, plus_plus( int, bit0( bit0(
% 0.81/1.22 times_times( int, bit1( pls ), m ) ) ), one_one( int ) ), zero_zero( int
% 0.81/1.22 ) ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 paramod: (2718) {G2,W15,D7,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), pls ) }.
% 0.81/1.22 parent0[0]: (1118) {G1,W6,D3,L1,V1,M1} P(78,126) { times_times( int, X, pls
% 0.81/1.22 ) ==> pls }.
% 0.81/1.22 parent1[0; 14]: (2717) {G2,W28,D8,L1,V0,M1} { ord_less( int, plus_plus(
% 0.81/1.22 int, power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) )
% 0.81/1.22 , one_one( int ) ), times_times( int, plus_plus( int, bit0( bit0(
% 0.81/1.22 times_times( int, bit1( pls ), m ) ) ), one_one( int ) ), pls ) ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 X := plus_plus( int, bit0( bit0( times_times( int, bit1( pls ), m ) ) )
% 0.81/1.22 , one_one( int ) )
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 resolution: (2719) {G3,W0,D0,L0,V0,M0} { }.
% 0.81/1.22 parent0[0]: (192) {G2,W15,D7,L1,V0,M1} I;d(174) { ! ord_less( int,
% 0.81/1.22 plus_plus( int, power_power( int, s, number_number_of( nat, bit0( bit1(
% 0.81/1.22 pls ) ) ) ), one_one( int ) ), pls ) }.
% 0.81/1.22 parent1[0]: (2718) {G2,W15,D7,L1,V0,M1} { ord_less( int, plus_plus( int,
% 0.81/1.22 power_power( int, s, number_number_of( nat, bit0( bit1( pls ) ) ) ),
% 0.81/1.22 one_one( int ) ), pls ) }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 substitution1:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 subsumption: (1219) {G3,W0,D0,L0,V0,M0} S(51);d(52);d(77);d(127);d(127);d(
% 0.81/1.22 174);d(1118);r(192) { }.
% 0.81/1.22 parent0: (2719) {G3,W0,D0,L0,V0,M0} { }.
% 0.81/1.22 substitution0:
% 0.81/1.22 end
% 0.81/1.22 permutation0:
% 0.81/1.22 end
% 0.81/1.22
% 0.81/1.22 Proof check complete!
% 0.81/1.22
% 0.81/1.22 Memory use:
% 0.81/1.22
% 0.81/1.22 space for terms: 22506
% 0.81/1.22 space for clauses: 68791
% 0.81/1.22
% 0.81/1.22
% 0.81/1.22 clauses generated: 5147
% 0.81/1.22 clauses kept: 1220
% 0.81/1.22 clauses selected: 176
% 0.81/1.22 clauses deleted: 18
% 0.81/1.22 clauses inuse deleted: 8
% 0.81/1.22
% 0.81/1.22 subsentry: 13149
% 0.81/1.22 literals s-matched: 7578
% 0.81/1.22 literals matched: 7445
% 0.81/1.22 full subsumption: 1791
% 0.81/1.22
% 0.81/1.22 checksum: -312485298
% 0.81/1.22
% 0.81/1.22
% 0.81/1.22 Bliksem ended
%------------------------------------------------------------------------------