%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : NUM924+1 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %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 : 300s
% DateTime : Wed Jul 27 13:10:13 EDT 2022
% Result : Theorem 2.03s 2.27s
% Output : Refutation 2.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 12
% Syntax : Number of clauses : 22 ( 22 unt; 0 nHn; 14 RR)
% Number of literals : 22 ( 15 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-2 aty)
% Number of variables : 15 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(94,axiom,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
file('NUM924+1.p',unknown),
[] ).
cnf(108,axiom,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
file('NUM924+1.p',unknown),
[] ).
cnf(109,axiom,
plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
file('NUM924+1.p',unknown),
[] ).
cnf(138,axiom,
number_number_of_int(A) = A,
file('NUM924+1.p',unknown),
[] ).
cnf(139,axiom,
times_times_int(A,B) = times_times_int(B,A),
file('NUM924+1.p',unknown),
[] ).
cnf(142,axiom,
times_times_int(times_times_int(A,B),C) = times_times_int(A,times_times_int(B,C)),
file('NUM924+1.p',unknown),
[] ).
cnf(152,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('NUM924+1.p',unknown),
[] ).
cnf(154,plain,
number_number_of_nat(bit0(bit1(pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[152])]),
[iquote('copy,152,flip.1')] ).
cnf(156,axiom,
times_times_int(pls,A) = pls,
file('NUM924+1.p',unknown),
[] ).
cnf(163,axiom,
times_times_int(one_one_int,A) = A,
file('NUM924+1.p',unknown),
[] ).
cnf(165,axiom,
times_times_int(plus_plus_int(A,B),C) = plus_plus_int(times_times_int(A,C),times_times_int(B,C)),
file('NUM924+1.p',unknown),
[] ).
cnf(166,axiom,
times_times_int(A,plus_plus_int(B,C)) = plus_plus_int(times_times_int(A,B),times_times_int(A,C)),
file('NUM924+1.p',unknown),
[] ).
cnf(181,axiom,
zero_zero_int = number_number_of_int(pls),
file('NUM924+1.p',unknown),
[] ).
cnf(183,plain,
zero_zero_int = pls,
inference(demod,[status(thm),theory(equality)],[inference(copy,[status(thm)],[181]),138]),
[iquote('copy,181,demod,138')] ).
cnf(184,plain,
~ ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),pls),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[94]),154,183]),
[iquote('back_demod,94,demod,154,183')] ).
cnf(187,plain,
plus_plus_int(times_times_int(bit0(bit0(bit1(pls))),times_times_int(m,t)),t) = plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[109]),154,138,165,142,163])]),
[iquote('back_demod,109,demod,154,138,165,142,163,flip.1')] ).
cnf(188,plain,
ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),plus_plus_int(times_times_int(bit0(bit0(bit1(pls))),times_times_int(m,pls)),pls)),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[108]),138,165,142,163,187,138,183,165,142,163]),
[iquote('back_demod,108,demod,138,165,142,163,187,138,183,165,142,163')] ).
cnf(605,plain,
times_times_int(A,pls) = pls,
inference(para_into,[status(thm),theory(equality)],[156,139]),
[iquote('para_into,155.1.1,139.1.1')] ).
cnf(609,plain,
ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),plus_plus_int(pls,pls)),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[188]),605,605]),
[iquote('back_demod,188,demod,605,605')] ).
cnf(1566,plain,
plus_plus_int(pls,pls) = pls,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[166,156]),156,156])]),
[iquote('para_into,166.1.1,155.1.1,demod,156,156,flip.1')] ).
cnf(1576,plain,
ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),pls),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[609]),1566]),
[iquote('back_demod,609,demod,1566')] ).
cnf(1577,plain,
$false,
inference(binary,[status(thm)],[1576,184]),
[iquote('binary,1576.1,184.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NUM924+1 : TPTP v8.1.0. Released v5.3.0.
% 0.03/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jul 27 09:04:18 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.03/2.23 ----- Otter 3.3f, August 2004 -----
% 2.03/2.23 The process was started by sandbox2 on n017.cluster.edu,
% 2.03/2.23 Wed Jul 27 09:04:18 2022
% 2.03/2.23 The command was "./otter". The process ID is 26913.
% 2.03/2.23
% 2.03/2.23 set(prolog_style_variables).
% 2.03/2.23 set(auto).
% 2.03/2.23 dependent: set(auto1).
% 2.03/2.23 dependent: set(process_input).
% 2.03/2.23 dependent: clear(print_kept).
% 2.03/2.23 dependent: clear(print_new_demod).
% 2.03/2.23 dependent: clear(print_back_demod).
% 2.03/2.23 dependent: clear(print_back_sub).
% 2.03/2.23 dependent: set(control_memory).
% 2.03/2.23 dependent: assign(max_mem, 12000).
% 2.03/2.23 dependent: assign(pick_given_ratio, 4).
% 2.03/2.23 dependent: assign(stats_level, 1).
% 2.03/2.23 dependent: assign(max_seconds, 10800).
% 2.03/2.23 clear(print_given).
% 2.03/2.23
% 2.03/2.23 formula_list(usable).
% 2.03/2.23 all A (A=A).
% 2.03/2.23 ord_less_int(t,zero_zero_int).
% 2.03/2.23 ord_less_int(t,one_one_int).
% 2.03/2.23 ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)).
% 2.03/2.23 plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t).
% 2.03/2.23 t=zero_zero_int->plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=zero_zero_int.
% 2.03/2.23 -ord_less_e_q_int(one_one_int,t).
% 2.03/2.23 ord_less_int(zero_zero_int,plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 all X Y (-ord_less_int(plus_plus_int(power_power_int(X,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y,number_number_of_nat(bit0(bit1(pls))))),zero_zero_int)).
% 2.03/2.23 all X_1 Y_1 (ord_less_int(zero_zero_int,plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls))))))<->X_1!=zero_zero_int|Y_1!=zero_zero_int).
% 2.03/2.23 all X_1 Y_1 (plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls)))))=zero_zero_int<->X_1=zero_zero_int&Y_1=zero_zero_int).
% 2.03/2.23 all A_2 (-ord_less_int(power_power_int(A_2,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int)).
% 2.03/2.23 all A_1 (ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))))<->A_1!=zero_zero_int).
% 2.03/2.23 power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls))))=one_one_nat.
% 2.03/2.23 power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls))))=one_one_int.
% 2.03/2.23 power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls))))=zero_zero_nat.
% 2.03/2.23 power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int.
% 2.03/2.23 all A_1 (power_power_int(A_1,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int<->A_1=zero_zero_int).
% 2.03/2.23 all W_6 (plus_plus_int(one_one_int,number_number_of_int(W_6))=number_number_of_int(plus_plus_int(bit1(pls),W_6))).
% 2.03/2.23 all V_13 (plus_plus_int(number_number_of_int(V_13),one_one_int)=number_number_of_int(plus_plus_int(V_13,bit1(pls)))).
% 2.03/2.23 ord_less_int(t,plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 -(all T (plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)!=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),T))).
% 2.03/2.23 zprime(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 twoSqu526106917sum2sq(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t)).
% 2.03/2.23 all W ord_less_e_q_int(W,W).
% 2.03/2.23 all K_1 (number_number_of_int(K_1)=K_1).
% 2.03/2.23 all Z W (times_times_int(Z,W)=times_times_int(W,Z)).
% 2.03/2.23 all Z W (ord_less_e_q_int(Z,W)|ord_less_e_q_int(W,Z)).
% 2.03/2.23 all V_2 W (times_times_int(number_number_of_int(V_2),number_number_of_int(W))=number_number_of_int(times_times_int(V_2,W))).
% 2.03/2.23 all K L (ord_less_e_q_int(number_number_of_int(K),number_number_of_int(L))<->ord_less_e_q_int(K,L)).
% 2.03/2.23 all X_1 Y_1 (ord_less_e_q_int(number_number_of_int(X_1),number_number_of_int(Y_1))<->ord_less_e_q_int(X_1,Y_1)).
% 2.03/2.23 all Z1 Z2 Z3 (times_times_int(times_times_int(Z1,Z2),Z3)=times_times_int(Z1,times_times_int(Z2,Z3))).
% 2.03/2.23 all K_1 I J (ord_less_e_q_int(I,J)-> (ord_less_e_q_int(J,K_1)->ord_less_e_q_int(I,K_1))).
% 2.03/2.23 all Z W (ord_less_e_q_int(Z,W)-> (ord_less_e_q_int(W,Z)->Z=W)).
% 2.03/2.23 all X Y Z (power_power_int(X,plus_plus_nat(Y,Z))=times_times_int(power_power_int(X,Y),power_power_int(X,Z))).
% 2.03/2.23 all K1 K2 (ord_less_e_q_int(bit1(K1),bit1(K2))<->ord_less_e_q_int(K1,K2)).
% 2.03/2.23 all K L (ord_less_e_q_int(bit1(K),bit1(L))<->ord_less_e_q_int(K,L)).
% 2.03/2.23 ord_less_e_q_int(pls,pls).
% 2.03/2.23 all K1 K2 (ord_less_e_q_int(bit0(K1),bit0(K2))<->ord_less_e_q_int(K1,K2)).
% 2.03/2.23 all K L (ord_less_e_q_int(bit0(K),bit0(L))<->ord_less_e_q_int(K,L)).
% 2.03/2.23 all Z_1 W_1 (ord_less_int(Z_1,W_1)<->ord_less_e_q_int(Z_1,W_1)&Z_1!=W_1).
% 2.03/2.23 all K_1 I J (ord_less_e_q_int(I,J)->ord_less_e_q_int(plus_plus_int(K_1,I),plus_plus_int(K_1,J))).
% 2.03/2.23 all V_7 (number_number_of_nat(V_7)=zero_zero_nat<->ord_less_e_q_int(V_7,pls)).
% 2.03/2.23 all V_7 (zero_zero_nat=number_number_of_nat(V_7)<->ord_less_e_q_int(V_7,pls)).
% 2.03/2.23 all V_12 V_11 (ord_less_e_q_int(pls,V_11)-> (ord_less_e_q_int(pls,V_12)->times_times_nat(number_number_of_nat(V_11),number_number_of_nat(V_12))=number_number_of_nat(times_times_int(V_11,V_12)))).
% 2.03/2.23 all V_12 V_11 (ord_less_e_q_int(pls,V_11)-> (ord_less_e_q_int(pls,V_12)->times_times_int(number_number_of_int(V_11),number_number_of_int(V_12))=number_number_of_int(times_times_int(V_11,V_12)))).
% 2.03/2.23 all V_10 W_5 Z_3 (times_times_int(number_number_of_int(V_10),times_times_int(number_number_of_int(W_5),Z_3))=times_times_int(number_number_of_int(times_times_int(V_10,W_5)),Z_3)).
% 2.03/2.23 all V_9 W_4 (times_times_int(number_number_of_int(V_9),number_number_of_int(W_4))=number_number_of_int(times_times_int(V_9,W_4))).
% 2.03/2.23 all V_8 W_3 (number_number_of_int(times_times_int(V_8,W_3))=times_times_int(number_number_of_int(V_8),number_number_of_int(W_3))).
% 2.03/2.23 all X_1 Y_1 (ord_less_e_q_int(plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1)),zero_zero_int)<->X_1=zero_zero_int&Y_1=zero_zero_int).
% 2.03/2.23 all X_2 Y_2 ord_less_e_q_int(zero_zero_int,plus_plus_int(times_times_int(X_2,X_2),times_times_int(Y_2,Y_2))).
% 2.03/2.23 all X_1 (ord_less_e_q_int(number_number_of_int(X_1),zero_zero_int)<->ord_less_e_q_int(X_1,pls)).
% 2.03/2.23 all Y_1 (ord_less_e_q_int(zero_zero_int,number_number_of_int(Y_1))<->ord_less_e_q_int(pls,Y_1)).
% 2.03/2.23 all V_7 (ord_less_nat(zero_zero_nat,number_number_of_nat(V_7))<->ord_less_int(pls,V_7)).
% 2.03/2.23 all V_7 W_1 (ord_less_e_q_int(number_number_of_int(V_7),number_number_of_int(W_1))<-> -ord_less_int(number_number_of_int(W_1),number_number_of_int(V_7))).
% 2.03/2.23 all V_7 W_1 (ord_less_e_q_nat(number_number_of_nat(V_7),number_number_of_nat(W_1))<-> -ord_less_nat(number_number_of_nat(W_1),number_number_of_nat(V_7))).
% 2.03/2.23 all K (ord_less_e_q_int(pls,bit1(K))<->ord_less_e_q_int(pls,K)).
% 2.03/2.23 all K1 K2 (ord_less_e_q_int(bit0(K1),bit1(K2))<->ord_less_e_q_int(K1,K2)).
% 2.03/2.23 all K L (ord_less_e_q_int(bit0(K),bit1(L))<->ord_less_e_q_int(K,L)).
% 2.03/2.23 all K (ord_less_e_q_int(bit0(K),pls)<->ord_less_e_q_int(K,pls)).
% 2.03/2.23 all K (ord_less_e_q_int(pls,bit0(K))<->ord_less_e_q_int(pls,K)).
% 2.03/2.23 all Z_2 Z W_2 W (ord_less_int(W_2,W)-> (ord_less_e_q_int(Z_2,Z)->ord_less_int(plus_plus_int(W_2,Z_2),plus_plus_int(W,Z)))).
% 2.03/2.23 number_number_of_nat(pls)=zero_zero_nat.
% 2.03/2.23 zero_zero_nat=number_number_of_nat(pls).
% 2.03/2.23 all X_1 (ord_less_e_q_int(number_number_of_int(X_1),one_one_int)<->ord_less_e_q_int(X_1,bit1(pls))).
% 2.03/2.23 all Y_1 (ord_less_e_q_int(one_one_int,number_number_of_int(Y_1))<->ord_less_e_q_int(bit1(pls),Y_1)).
% 2.03/2.23 plus_plus_nat(one_one_nat,one_one_nat)=number_number_of_nat(bit0(bit1(pls))).
% 2.03/2.23 all W (times_times_int(pls,W)=pls).
% 2.03/2.23 all K_1 L_1 (times_times_int(bit0(K_1),L_1)=bit0(times_times_int(K_1,L_1))).
% 2.03/2.23 all K L (ord_less_int(number_number_of_int(K),number_number_of_int(L))<->ord_less_int(K,L)).
% 2.03/2.23 all Z (times_times_int(Z,one_one_int)=Z).
% 2.03/2.23 all Z (times_times_int(one_one_int,Z)=Z).
% 2.03/2.23 all V_2 W (plus_plus_int(number_number_of_int(V_2),number_number_of_int(W))=number_number_of_int(plus_plus_int(V_2,W))).
% 2.03/2.23 all Z1 Z2 W (times_times_int(plus_plus_int(Z1,Z2),W)=plus_plus_int(times_times_int(Z1,W),times_times_int(Z2,W))).
% 2.03/2.23 all W Z1 Z2 (times_times_int(W,plus_plus_int(Z1,Z2))=plus_plus_int(times_times_int(W,Z1),times_times_int(W,Z2))).
% 2.03/2.23 all K (ord_less_e_q_int(bit1(K),pls)<->ord_less_int(K,pls)).
% 2.03/2.23 all K (ord_less_int(pls,bit1(K))<->ord_less_e_q_int(pls,K)).
% 2.03/2.23 all K1 K2 (ord_less_e_q_int(bit1(K1),bit0(K2))<->ord_less_int(K1,K2)).
% 2.03/2.23 all K L (ord_less_e_q_int(bit1(K),bit0(L))<->ord_less_int(K,L)).
% 2.03/2.23 all K1 K2 (ord_less_int(bit0(K1),bit1(K2))<->ord_less_e_q_int(K1,K2)).
% 2.03/2.23 all K L (ord_less_int(bit0(K),bit1(L))<->ord_less_e_q_int(K,L)).
% 2.03/2.23 all V_7 V_6 (ord_less_nat(number_number_of_nat(V_7),number_number_of_nat(V_6))<-> (ord_less_int(V_7,V_6)->ord_less_int(pls,V_6))&ord_less_int(V_7,V_6)).
% 2.03/2.23 all Z_1 (ord_less_e_q_int(one_one_int,Z_1)<->ord_less_int(zero_zero_int,Z_1)).
% 2.03/2.23 number_number_of_nat(bit1(pls))=one_one_nat.
% 2.03/2.23 one_one_nat=number_number_of_nat(bit1(pls)).
% 2.03/2.23 all W Z (ord_less_int(W,Z)->ord_less_e_q_int(plus_plus_int(W,one_one_int),Z)).
% 2.03/2.23 all W_1 Z_1 (ord_less_e_q_int(plus_plus_int(W_1,one_one_int),Z_1)<->ord_less_int(W_1,Z_1)).
% 2.03/2.23 all W_1 Z_1 (ord_less_int(W_1,plus_plus_int(Z_1,one_one_int))<->ord_less_e_q_int(W_1,Z_1)).
% 2.03/2.23 all V_5 V_4 (ord_less_e_q_int(pls,V_4)-> (ord_less_e_q_int(pls,V_5)->plus_plus_int(number_number_of_int(V_4),number_number_of_int(V_5))=number_number_of_int(plus_plus_int(V_4,V_5)))).
% 2.03/2.23 all V_5 V_4 (ord_less_e_q_int(pls,V_4)-> (ord_less_e_q_int(pls,V_5)->plus_plus_nat(number_number_of_nat(V_4),number_number_of_nat(V_5))=number_number_of_nat(plus_plus_int(V_4,V_5)))).
% 2.03/2.23 all V_3 V_2 ((ord_less_int(V_2,pls)->plus_plus_nat(number_number_of_nat(V_2),number_number_of_nat(V_3))=number_number_of_nat(V_3))& (-ord_less_int(V_2,pls)-> (ord_less_int(V_3,pls)->plus_plus_nat(number_number_of_nat(V_2),number_number_of_nat(V_3))=number_number_of_nat(V_2))& (-ord_less_int(V_3,pls)->plus_plus_nat(number_number_of_nat(V_2),number_number_of_nat(V_3))=number_number_of_nat(plus_plus_int(V_2,V_3))))).
% 2.03/2.23 all Z (ord_less_e_q_int(zero_zero_int,Z)->ord_less_int(zero_zero_int,plus_plus_int(one_one_int,Z))).
% 2.03/2.23 all X_1 Y_1 (number_number_of_int(X_1)=number_number_of_int(Y_1)<->X_1=Y_1).
% 2.03/2.23 all W_1 X_1 (number_number_of_nat(W_1)=X_1<->X_1=number_number_of_nat(W_1)).
% 2.03/2.23 all W_1 X_1 (number_number_of_int(W_1)=X_1<->X_1=number_number_of_int(W_1)).
% 2.03/2.23 all K L (bit1(K)=bit1(L)<->K=L).
% 2.03/2.23 all K L (bit0(K)=bit0(L)<->K=L).
% 2.03/2.23 all X Y (ord_less_int(X,Y)|X=Y|ord_less_int(Y,X)).
% 2.03/2.23 all X_1 Y_1 (plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1))=zero_zero_int<->X_1=zero_zero_int&Y_1=zero_zero_int).
% 2.03/2.23 all A B_1 V_1 (times_times_int(plus_plus_int(A,B_1),number_number_of_int(V_1))=plus_plus_int(times_times_int(A,number_number_of_int(V_1)),times_times_int(B_1,number_number_of_int(V_1)))).
% 2.03/2.23 all A B_1 V_1 (times_times_nat(plus_plus_nat(A,B_1),number_number_of_nat(V_1))=plus_plus_nat(times_times_nat(A,number_number_of_nat(V_1)),times_times_nat(B_1,number_number_of_nat(V_1)))).
% 2.03/2.23 all V B C (times_times_int(number_number_of_int(V),plus_plus_int(B,C))=plus_plus_int(times_times_int(number_number_of_int(V),B),times_times_int(number_number_of_int(V),C))).
% 2.03/2.23 all V B C (times_times_nat(number_number_of_nat(V),plus_plus_nat(B,C))=plus_plus_nat(times_times_nat(number_number_of_nat(V),B),times_times_nat(number_number_of_nat(V),C))).
% 2.03/2.23 all Z1 Z2 Z3 (plus_plus_int(plus_plus_int(Z1,Z2),Z3)=plus_plus_int(Z1,plus_plus_int(Z2,Z3))).
% 2.03/2.23 all X Y Z (plus_plus_int(X,plus_plus_int(Y,Z))=plus_plus_int(Y,plus_plus_int(X,Z))).
% 2.03/2.23 all Z W (plus_plus_int(Z,W)=plus_plus_int(W,Z)).
% 2.03/2.23 zero_zero_int=number_number_of_int(pls).
% 2.03/2.23 -ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int).
% 2.03/2.23 end_of_list.
% 2.03/2.23
% 2.03/2.23 -------> usable clausifies to:
% 2.03/2.23
% 2.03/2.23 list(usable).
% 2.03/2.23 0 [] A=A.
% 2.03/2.23 0 [] ord_less_int(t,zero_zero_int).
% 2.03/2.23 0 [] ord_less_int(t,one_one_int).
% 2.03/2.23 0 [] ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)).
% 2.03/2.23 0 [] plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t).
% 2.03/2.23 0 [] t!=zero_zero_int|plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=zero_zero_int.
% 2.03/2.23 0 [] -ord_less_e_q_int(one_one_int,t).
% 2.03/2.23 0 [] ord_less_int(zero_zero_int,plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 0 [] -ord_less_int(plus_plus_int(power_power_int(X,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y,number_number_of_nat(bit0(bit1(pls))))),zero_zero_int).
% 2.03/2.23 0 [] -ord_less_int(zero_zero_int,plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls))))))|X_1!=zero_zero_int|Y_1!=zero_zero_int.
% 2.03/2.23 0 [] ord_less_int(zero_zero_int,plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls))))))|X_1=zero_zero_int.
% 2.03/2.23 0 [] ord_less_int(zero_zero_int,plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls))))))|Y_1=zero_zero_int.
% 2.03/2.23 0 [] plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_int|X_1=zero_zero_int.
% 2.03/2.23 0 [] plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_int|Y_1=zero_zero_int.
% 2.03/2.23 0 [] plus_plus_int(power_power_int(X_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Y_1,number_number_of_nat(bit0(bit1(pls)))))=zero_zero_int|X_1!=zero_zero_int|Y_1!=zero_zero_int.
% 2.03/2.23 0 [] -ord_less_int(power_power_int(A_2,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int).
% 2.03/2.23 0 [] -ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))))|A_1!=zero_zero_int.
% 2.03/2.23 0 [] ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))))|A_1=zero_zero_int.
% 2.03/2.23 0 [] power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls))))=one_one_nat.
% 2.03/2.23 0 [] power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls))))=one_one_int.
% 2.03/2.23 0 [] power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls))))=zero_zero_nat.
% 2.03/2.23 0 [] power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int.
% 2.03/2.23 0 [] power_power_int(A_1,number_number_of_nat(bit0(bit1(pls))))!=zero_zero_int|A_1=zero_zero_int.
% 2.03/2.23 0 [] power_power_int(A_1,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int|A_1!=zero_zero_int.
% 2.03/2.23 0 [] plus_plus_int(one_one_int,number_number_of_int(W_6))=number_number_of_int(plus_plus_int(bit1(pls),W_6)).
% 2.03/2.23 0 [] plus_plus_int(number_number_of_int(V_13),one_one_int)=number_number_of_int(plus_plus_int(V_13,bit1(pls))).
% 2.03/2.23 0 [] ord_less_int(t,plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 0 [] plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),$c1).
% 2.03/2.23 0 [] zprime(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 0 [] twoSqu526106917sum2sq(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t)).
% 2.03/2.23 0 [] ord_less_e_q_int(W,W).
% 2.03/2.23 0 [] number_number_of_int(K_1)=K_1.
% 2.03/2.23 0 [] times_times_int(Z,W)=times_times_int(W,Z).
% 2.03/2.23 0 [] ord_less_e_q_int(Z,W)|ord_less_e_q_int(W,Z).
% 2.03/2.23 0 [] times_times_int(number_number_of_int(V_2),number_number_of_int(W))=number_number_of_int(times_times_int(V_2,W)).
% 2.03/2.23 0 [] -ord_less_e_q_int(number_number_of_int(K),number_number_of_int(L))|ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] ord_less_e_q_int(number_number_of_int(K),number_number_of_int(L))| -ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] -ord_less_e_q_int(number_number_of_int(X_1),number_number_of_int(Y_1))|ord_less_e_q_int(X_1,Y_1).
% 2.03/2.23 0 [] ord_less_e_q_int(number_number_of_int(X_1),number_number_of_int(Y_1))| -ord_less_e_q_int(X_1,Y_1).
% 2.03/2.23 0 [] times_times_int(times_times_int(Z1,Z2),Z3)=times_times_int(Z1,times_times_int(Z2,Z3)).
% 2.03/2.23 0 [] -ord_less_e_q_int(I,J)| -ord_less_e_q_int(J,K_1)|ord_less_e_q_int(I,K_1).
% 2.03/2.23 0 [] -ord_less_e_q_int(Z,W)| -ord_less_e_q_int(W,Z)|Z=W.
% 2.03/2.23 0 [] power_power_int(X,plus_plus_nat(Y,Z))=times_times_int(power_power_int(X,Y),power_power_int(X,Z)).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit1(K1),bit1(K2))|ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] ord_less_e_q_int(bit1(K1),bit1(K2))| -ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit1(K),bit1(L))|ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] ord_less_e_q_int(bit1(K),bit1(L))| -ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] ord_less_e_q_int(pls,pls).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit0(K1),bit0(K2))|ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] ord_less_e_q_int(bit0(K1),bit0(K2))| -ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit0(K),bit0(L))|ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] ord_less_e_q_int(bit0(K),bit0(L))| -ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] -ord_less_int(Z_1,W_1)|ord_less_e_q_int(Z_1,W_1).
% 2.03/2.23 0 [] -ord_less_int(Z_1,W_1)|Z_1!=W_1.
% 2.03/2.23 0 [] ord_less_int(Z_1,W_1)| -ord_less_e_q_int(Z_1,W_1)|Z_1=W_1.
% 2.03/2.23 0 [] -ord_less_e_q_int(I,J)|ord_less_e_q_int(plus_plus_int(K_1,I),plus_plus_int(K_1,J)).
% 2.03/2.23 0 [] number_number_of_nat(V_7)!=zero_zero_nat|ord_less_e_q_int(V_7,pls).
% 2.03/2.23 0 [] number_number_of_nat(V_7)=zero_zero_nat| -ord_less_e_q_int(V_7,pls).
% 2.03/2.23 0 [] zero_zero_nat!=number_number_of_nat(V_7)|ord_less_e_q_int(V_7,pls).
% 2.03/2.23 0 [] zero_zero_nat=number_number_of_nat(V_7)| -ord_less_e_q_int(V_7,pls).
% 2.03/2.23 0 [] -ord_less_e_q_int(pls,V_11)| -ord_less_e_q_int(pls,V_12)|times_times_nat(number_number_of_nat(V_11),number_number_of_nat(V_12))=number_number_of_nat(times_times_int(V_11,V_12)).
% 2.03/2.23 0 [] -ord_less_e_q_int(pls,V_11)| -ord_less_e_q_int(pls,V_12)|times_times_int(number_number_of_int(V_11),number_number_of_int(V_12))=number_number_of_int(times_times_int(V_11,V_12)).
% 2.03/2.23 0 [] times_times_int(number_number_of_int(V_10),times_times_int(number_number_of_int(W_5),Z_3))=times_times_int(number_number_of_int(times_times_int(V_10,W_5)),Z_3).
% 2.03/2.23 0 [] times_times_int(number_number_of_int(V_9),number_number_of_int(W_4))=number_number_of_int(times_times_int(V_9,W_4)).
% 2.03/2.23 0 [] number_number_of_int(times_times_int(V_8,W_3))=times_times_int(number_number_of_int(V_8),number_number_of_int(W_3)).
% 2.03/2.23 0 [] -ord_less_e_q_int(plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1)),zero_zero_int)|X_1=zero_zero_int.
% 2.03/2.23 0 [] -ord_less_e_q_int(plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1)),zero_zero_int)|Y_1=zero_zero_int.
% 2.03/2.23 0 [] ord_less_e_q_int(plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1)),zero_zero_int)|X_1!=zero_zero_int|Y_1!=zero_zero_int.
% 2.03/2.23 0 [] ord_less_e_q_int(zero_zero_int,plus_plus_int(times_times_int(X_2,X_2),times_times_int(Y_2,Y_2))).
% 2.03/2.23 0 [] -ord_less_e_q_int(number_number_of_int(X_1),zero_zero_int)|ord_less_e_q_int(X_1,pls).
% 2.03/2.23 0 [] ord_less_e_q_int(number_number_of_int(X_1),zero_zero_int)| -ord_less_e_q_int(X_1,pls).
% 2.03/2.23 0 [] -ord_less_e_q_int(zero_zero_int,number_number_of_int(Y_1))|ord_less_e_q_int(pls,Y_1).
% 2.03/2.23 0 [] ord_less_e_q_int(zero_zero_int,number_number_of_int(Y_1))| -ord_less_e_q_int(pls,Y_1).
% 2.03/2.23 0 [] -ord_less_nat(zero_zero_nat,number_number_of_nat(V_7))|ord_less_int(pls,V_7).
% 2.03/2.23 0 [] ord_less_nat(zero_zero_nat,number_number_of_nat(V_7))| -ord_less_int(pls,V_7).
% 2.03/2.23 0 [] -ord_less_e_q_int(number_number_of_int(V_7),number_number_of_int(W_1))| -ord_less_int(number_number_of_int(W_1),number_number_of_int(V_7)).
% 2.03/2.23 0 [] ord_less_e_q_int(number_number_of_int(V_7),number_number_of_int(W_1))|ord_less_int(number_number_of_int(W_1),number_number_of_int(V_7)).
% 2.03/2.23 0 [] -ord_less_e_q_nat(number_number_of_nat(V_7),number_number_of_nat(W_1))| -ord_less_nat(number_number_of_nat(W_1),number_number_of_nat(V_7)).
% 2.03/2.23 0 [] ord_less_e_q_nat(number_number_of_nat(V_7),number_number_of_nat(W_1))|ord_less_nat(number_number_of_nat(W_1),number_number_of_nat(V_7)).
% 2.03/2.23 0 [] -ord_less_e_q_int(pls,bit1(K))|ord_less_e_q_int(pls,K).
% 2.03/2.23 0 [] ord_less_e_q_int(pls,bit1(K))| -ord_less_e_q_int(pls,K).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit0(K1),bit1(K2))|ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] ord_less_e_q_int(bit0(K1),bit1(K2))| -ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit0(K),bit1(L))|ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] ord_less_e_q_int(bit0(K),bit1(L))| -ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit0(K),pls)|ord_less_e_q_int(K,pls).
% 2.03/2.23 0 [] ord_less_e_q_int(bit0(K),pls)| -ord_less_e_q_int(K,pls).
% 2.03/2.23 0 [] -ord_less_e_q_int(pls,bit0(K))|ord_less_e_q_int(pls,K).
% 2.03/2.23 0 [] ord_less_e_q_int(pls,bit0(K))| -ord_less_e_q_int(pls,K).
% 2.03/2.23 0 [] -ord_less_int(W_2,W)| -ord_less_e_q_int(Z_2,Z)|ord_less_int(plus_plus_int(W_2,Z_2),plus_plus_int(W,Z)).
% 2.03/2.23 0 [] number_number_of_nat(pls)=zero_zero_nat.
% 2.03/2.23 0 [] zero_zero_nat=number_number_of_nat(pls).
% 2.03/2.23 0 [] -ord_less_e_q_int(number_number_of_int(X_1),one_one_int)|ord_less_e_q_int(X_1,bit1(pls)).
% 2.03/2.23 0 [] ord_less_e_q_int(number_number_of_int(X_1),one_one_int)| -ord_less_e_q_int(X_1,bit1(pls)).
% 2.03/2.23 0 [] -ord_less_e_q_int(one_one_int,number_number_of_int(Y_1))|ord_less_e_q_int(bit1(pls),Y_1).
% 2.03/2.23 0 [] ord_less_e_q_int(one_one_int,number_number_of_int(Y_1))| -ord_less_e_q_int(bit1(pls),Y_1).
% 2.03/2.23 0 [] plus_plus_nat(one_one_nat,one_one_nat)=number_number_of_nat(bit0(bit1(pls))).
% 2.03/2.23 0 [] times_times_int(pls,W)=pls.
% 2.03/2.23 0 [] times_times_int(bit0(K_1),L_1)=bit0(times_times_int(K_1,L_1)).
% 2.03/2.23 0 [] -ord_less_int(number_number_of_int(K),number_number_of_int(L))|ord_less_int(K,L).
% 2.03/2.23 0 [] ord_less_int(number_number_of_int(K),number_number_of_int(L))| -ord_less_int(K,L).
% 2.03/2.23 0 [] times_times_int(Z,one_one_int)=Z.
% 2.03/2.23 0 [] times_times_int(one_one_int,Z)=Z.
% 2.03/2.23 0 [] plus_plus_int(number_number_of_int(V_2),number_number_of_int(W))=number_number_of_int(plus_plus_int(V_2,W)).
% 2.03/2.23 0 [] times_times_int(plus_plus_int(Z1,Z2),W)=plus_plus_int(times_times_int(Z1,W),times_times_int(Z2,W)).
% 2.03/2.23 0 [] times_times_int(W,plus_plus_int(Z1,Z2))=plus_plus_int(times_times_int(W,Z1),times_times_int(W,Z2)).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit1(K),pls)|ord_less_int(K,pls).
% 2.03/2.23 0 [] ord_less_e_q_int(bit1(K),pls)| -ord_less_int(K,pls).
% 2.03/2.23 0 [] -ord_less_int(pls,bit1(K))|ord_less_e_q_int(pls,K).
% 2.03/2.23 0 [] ord_less_int(pls,bit1(K))| -ord_less_e_q_int(pls,K).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit1(K1),bit0(K2))|ord_less_int(K1,K2).
% 2.03/2.23 0 [] ord_less_e_q_int(bit1(K1),bit0(K2))| -ord_less_int(K1,K2).
% 2.03/2.23 0 [] -ord_less_e_q_int(bit1(K),bit0(L))|ord_less_int(K,L).
% 2.03/2.23 0 [] ord_less_e_q_int(bit1(K),bit0(L))| -ord_less_int(K,L).
% 2.03/2.23 0 [] -ord_less_int(bit0(K1),bit1(K2))|ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] ord_less_int(bit0(K1),bit1(K2))| -ord_less_e_q_int(K1,K2).
% 2.03/2.23 0 [] -ord_less_int(bit0(K),bit1(L))|ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] ord_less_int(bit0(K),bit1(L))| -ord_less_e_q_int(K,L).
% 2.03/2.23 0 [] -ord_less_nat(number_number_of_nat(V_7),number_number_of_nat(V_6))| -ord_less_int(V_7,V_6)|ord_less_int(pls,V_6).
% 2.03/2.23 0 [] -ord_less_nat(number_number_of_nat(V_7),number_number_of_nat(V_6))|ord_less_int(V_7,V_6).
% 2.03/2.23 0 [] ord_less_nat(number_number_of_nat(V_7),number_number_of_nat(V_6))| -ord_less_int(pls,V_6)| -ord_less_int(V_7,V_6).
% 2.03/2.23 0 [] -ord_less_e_q_int(one_one_int,Z_1)|ord_less_int(zero_zero_int,Z_1).
% 2.03/2.23 0 [] ord_less_e_q_int(one_one_int,Z_1)| -ord_less_int(zero_zero_int,Z_1).
% 2.03/2.23 0 [] number_number_of_nat(bit1(pls))=one_one_nat.
% 2.03/2.23 0 [] one_one_nat=number_number_of_nat(bit1(pls)).
% 2.03/2.23 0 [] -ord_less_int(W,Z)|ord_less_e_q_int(plus_plus_int(W,one_one_int),Z).
% 2.03/2.23 0 [] -ord_less_e_q_int(plus_plus_int(W_1,one_one_int),Z_1)|ord_less_int(W_1,Z_1).
% 2.03/2.23 0 [] ord_less_e_q_int(plus_plus_int(W_1,one_one_int),Z_1)| -ord_less_int(W_1,Z_1).
% 2.03/2.23 0 [] -ord_less_int(W_1,plus_plus_int(Z_1,one_one_int))|ord_less_e_q_int(W_1,Z_1).
% 2.03/2.23 0 [] ord_less_int(W_1,plus_plus_int(Z_1,one_one_int))| -ord_less_e_q_int(W_1,Z_1).
% 2.03/2.23 0 [] -ord_less_e_q_int(pls,V_4)| -ord_less_e_q_int(pls,V_5)|plus_plus_int(number_number_of_int(V_4),number_number_of_int(V_5))=number_number_of_int(plus_plus_int(V_4,V_5)).
% 2.03/2.23 0 [] -ord_less_e_q_int(pls,V_4)| -ord_less_e_q_int(pls,V_5)|plus_plus_nat(number_number_of_nat(V_4),number_number_of_nat(V_5))=number_number_of_nat(plus_plus_int(V_4,V_5)).
% 2.03/2.23 0 [] -ord_less_int(V_2,pls)|plus_plus_nat(number_number_of_nat(V_2),number_number_of_nat(V_3))=number_number_of_nat(V_3).
% 2.03/2.23 0 [] ord_less_int(V_2,pls)| -ord_less_int(V_3,pls)|plus_plus_nat(number_number_of_nat(V_2),number_number_of_nat(V_3))=number_number_of_nat(V_2).
% 2.03/2.23 0 [] ord_less_int(V_2,pls)|ord_less_int(V_3,pls)|plus_plus_nat(number_number_of_nat(V_2),number_number_of_nat(V_3))=number_number_of_nat(plus_plus_int(V_2,V_3)).
% 2.03/2.23 0 [] -ord_less_e_q_int(zero_zero_int,Z)|ord_less_int(zero_zero_int,plus_plus_int(one_one_int,Z)).
% 2.03/2.23 0 [] number_number_of_int(X_1)!=number_number_of_int(Y_1)|X_1=Y_1.
% 2.03/2.23 0 [] number_number_of_int(X_1)=number_number_of_int(Y_1)|X_1!=Y_1.
% 2.03/2.23 0 [] number_number_of_nat(W_1)!=X_1|X_1=number_number_of_nat(W_1).
% 2.03/2.23 0 [] number_number_of_nat(W_1)=X_1|X_1!=number_number_of_nat(W_1).
% 2.03/2.23 0 [] number_number_of_int(W_1)!=X_1|X_1=number_number_of_int(W_1).
% 2.03/2.23 0 [] number_number_of_int(W_1)=X_1|X_1!=number_number_of_int(W_1).
% 2.03/2.23 0 [] bit1(K)!=bit1(L)|K=L.
% 2.03/2.23 0 [] bit1(K)=bit1(L)|K!=L.
% 2.03/2.23 0 [] bit0(K)!=bit0(L)|K=L.
% 2.03/2.23 0 [] bit0(K)=bit0(L)|K!=L.
% 2.03/2.23 0 [] ord_less_int(X,Y)|X=Y|ord_less_int(Y,X).
% 2.03/2.23 0 [] plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1))!=zero_zero_int|X_1=zero_zero_int.
% 2.03/2.23 0 [] plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1))!=zero_zero_int|Y_1=zero_zero_int.
% 2.03/2.23 0 [] plus_plus_int(times_times_int(X_1,X_1),times_times_int(Y_1,Y_1))=zero_zero_int|X_1!=zero_zero_int|Y_1!=zero_zero_int.
% 2.03/2.23 0 [] times_times_int(plus_plus_int(A,B_1),number_number_of_int(V_1))=plus_plus_int(times_times_int(A,number_number_of_int(V_1)),times_times_int(B_1,number_number_of_int(V_1))).
% 2.03/2.23 0 [] times_times_nat(plus_plus_nat(A,B_1),number_number_of_nat(V_1))=plus_plus_nat(times_times_nat(A,number_number_of_nat(V_1)),times_times_nat(B_1,number_number_of_nat(V_1))).
% 2.03/2.23 0 [] times_times_int(number_number_of_int(V),plus_plus_int(B,C))=plus_plus_int(times_times_int(number_number_of_int(V),B),times_times_int(number_number_of_int(V),C)).
% 2.03/2.23 0 [] times_times_nat(number_number_of_nat(V),plus_plus_nat(B,C))=plus_plus_nat(times_times_nat(number_number_of_nat(V),B),times_times_nat(number_number_of_nat(V),C)).
% 2.03/2.23 0 [] plus_plus_int(plus_plus_int(Z1,Z2),Z3)=plus_plus_int(Z1,plus_plus_int(Z2,Z3)).
% 2.03/2.23 0 [] plus_plus_int(X,plus_plus_int(Y,Z))=plus_plus_int(Y,plus_plus_int(X,Z)).
% 2.03/2.23 0 [] plus_plus_int(Z,W)=plus_plus_int(W,Z).
% 2.03/2.23 0 [] zero_zero_int=number_number_of_int(pls).
% 2.03/2.23 0 [] -ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int).
% 2.03/2.23 end_of_list.
% 2.03/2.23
% 2.03/2.23 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3.
% 2.03/2.23
% 2.03/2.23 This ia a non-Horn set with equality. The strategy will be
% 2.03/2.23 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 2.03/2.23 deletion, with positive clauses in sos and nonpositive
% 2.03/2.23 clauses in usable.
% 2.03/2.23
% 2.03/2.23 dependent: set(knuth_bendix).
% 2.03/2.23 dependent: set(anl_eq).
% 2.03/2.23 dependent: set(para_from).
% 2.03/2.23 dependent: set(para_into).
% 2.03/2.23 dependent: clear(para_from_right).
% 2.03/2.23 dependent: clear(para_into_right).
% 2.03/2.23 dependent: set(para_from_vars).
% 2.03/2.23 dependent: set(eq_units_both_ways).
% 2.03/2.23 dependent: set(dynamic_demod_all).
% 2.03/2.23 dependent: set(dynamic_demod).
% 2.03/2.23 dependent: set(order_eq).
% 2.03/2.23 dependent: set(back_demod).
% 2.03/2.23 dependent: set(lrpo).
% 2.03/2.23 dependent: set(hyper_res).
% 2.03/2.23 dependent: set(unit_deletion).
% 2.03/2.23 dependent: set(factor).
% 2.03/2.23
% 2.03/2.23 ------------> process usable:
% 2.03/2.23 ** KEPT (pick-wt=13): 2 [copy,1,flip.1] zero_zero_int!=t|plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=3): 3 [] -ord_less_e_q_int(one_one_int,t).
% 2.03/2.23 ** KEPT (pick-wt=15): 4 [] -ord_less_int(plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls))))),zero_zero_int).
% 2.03/2.23 ** KEPT (pick-wt=21): 5 [] -ord_less_int(zero_zero_int,plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls))))))|A!=zero_zero_int|B!=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=18): 6 [] plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_int|A=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=18): 7 [] plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_int|B=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=21): 8 [] plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls)))))=zero_zero_int|A!=zero_zero_int|B!=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=8): 9 [] -ord_less_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int).
% 2.03/2.23 ** KEPT (pick-wt=11): 10 [] -ord_less_int(zero_zero_int,power_power_int(A,number_number_of_nat(bit0(bit1(pls)))))|A!=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=11): 11 [] power_power_int(A,number_number_of_nat(bit0(bit1(pls))))!=zero_zero_int|A=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=11): 12 [] power_power_int(A,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int|A!=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=8): 13 [] -ord_less_e_q_int(number_number_of_int(A),number_number_of_int(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 14 [] ord_less_e_q_int(number_number_of_int(A),number_number_of_int(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 13 during input processing: 0 [] -ord_less_e_q_int(number_number_of_int(A),number_number_of_int(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 14 during input processing: 0 [] ord_less_e_q_int(number_number_of_int(A),number_number_of_int(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=9): 15 [] -ord_less_e_q_int(A,B)| -ord_less_e_q_int(B,C)|ord_less_e_q_int(A,C).
% 2.03/2.23 ** KEPT (pick-wt=9): 16 [] -ord_less_e_q_int(A,B)| -ord_less_e_q_int(B,A)|A=B.
% 2.03/2.23 ** KEPT (pick-wt=8): 17 [] -ord_less_e_q_int(bit1(A),bit1(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 18 [] ord_less_e_q_int(bit1(A),bit1(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 17 during input processing: 0 [] -ord_less_e_q_int(bit1(A),bit1(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 18 during input processing: 0 [] ord_less_e_q_int(bit1(A),bit1(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 19 [] -ord_less_e_q_int(bit0(A),bit0(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 20 [] ord_less_e_q_int(bit0(A),bit0(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 19 during input processing: 0 [] -ord_less_e_q_int(bit0(A),bit0(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 20 during input processing: 0 [] ord_less_e_q_int(bit0(A),bit0(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=6): 21 [] -ord_less_int(A,B)|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=6): 22 [] -ord_less_int(A,B)|A!=B.
% 2.03/2.23 ** KEPT (pick-wt=9): 23 [] ord_less_int(A,B)| -ord_less_e_q_int(A,B)|A=B.
% 2.03/2.23 ** KEPT (pick-wt=10): 24 [] -ord_less_e_q_int(A,B)|ord_less_e_q_int(plus_plus_int(C,A),plus_plus_int(C,B)).
% 2.03/2.23 ** KEPT (pick-wt=7): 25 [] number_number_of_nat(A)!=zero_zero_nat|ord_less_e_q_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 26 [] number_number_of_nat(A)=zero_zero_nat| -ord_less_e_q_int(A,pls).
% 2.03/2.23 Following clause subsumed by 25 during input processing: 0 [flip.1] number_number_of_nat(A)!=zero_zero_nat|ord_less_e_q_int(A,pls).
% 2.03/2.23 Following clause subsumed by 26 during input processing: 0 [flip.1] number_number_of_nat(A)=zero_zero_nat| -ord_less_e_q_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=16): 28 [copy,27,flip.3] -ord_less_e_q_int(pls,A)| -ord_less_e_q_int(pls,B)|number_number_of_nat(times_times_int(A,B))=times_times_nat(number_number_of_nat(A),number_number_of_nat(B)).
% 2.03/2.23 ** KEPT (pick-wt=16): 30 [copy,29,flip.3] -ord_less_e_q_int(pls,A)| -ord_less_e_q_int(pls,B)|number_number_of_int(times_times_int(A,B))=times_times_int(number_number_of_int(A),number_number_of_int(B)).
% 2.03/2.23 ** KEPT (pick-wt=12): 31 [] -ord_less_e_q_int(plus_plus_int(times_times_int(A,A),times_times_int(B,B)),zero_zero_int)|A=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=12): 32 [] -ord_less_e_q_int(plus_plus_int(times_times_int(A,A),times_times_int(B,B)),zero_zero_int)|B=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=15): 33 [] ord_less_e_q_int(plus_plus_int(times_times_int(A,A),times_times_int(B,B)),zero_zero_int)|A!=zero_zero_int|B!=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=7): 34 [] -ord_less_e_q_int(number_number_of_int(A),zero_zero_int)|ord_less_e_q_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 35 [] ord_less_e_q_int(number_number_of_int(A),zero_zero_int)| -ord_less_e_q_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 36 [] -ord_less_e_q_int(zero_zero_int,number_number_of_int(A))|ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=7): 37 [] ord_less_e_q_int(zero_zero_int,number_number_of_int(A))| -ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=7): 38 [] -ord_less_nat(zero_zero_nat,number_number_of_nat(A))|ord_less_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=7): 39 [] ord_less_nat(zero_zero_nat,number_number_of_nat(A))| -ord_less_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=10): 40 [] -ord_less_e_q_int(number_number_of_int(A),number_number_of_int(B))| -ord_less_int(number_number_of_int(B),number_number_of_int(A)).
% 2.03/2.23 ** KEPT (pick-wt=10): 41 [] -ord_less_e_q_nat(number_number_of_nat(A),number_number_of_nat(B))| -ord_less_nat(number_number_of_nat(B),number_number_of_nat(A)).
% 2.03/2.23 ** KEPT (pick-wt=7): 42 [] -ord_less_e_q_int(pls,bit1(A))|ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=7): 43 [] ord_less_e_q_int(pls,bit1(A))| -ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=8): 44 [] -ord_less_e_q_int(bit0(A),bit1(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 45 [] ord_less_e_q_int(bit0(A),bit1(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 44 during input processing: 0 [] -ord_less_e_q_int(bit0(A),bit1(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 45 during input processing: 0 [] ord_less_e_q_int(bit0(A),bit1(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=7): 46 [] -ord_less_e_q_int(bit0(A),pls)|ord_less_e_q_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 47 [] ord_less_e_q_int(bit0(A),pls)| -ord_less_e_q_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 48 [] -ord_less_e_q_int(pls,bit0(A))|ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=7): 49 [] ord_less_e_q_int(pls,bit0(A))| -ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=13): 50 [] -ord_less_int(A,B)| -ord_less_e_q_int(C,D)|ord_less_int(plus_plus_int(A,C),plus_plus_int(B,D)).
% 2.03/2.23 ** KEPT (pick-wt=8): 51 [] -ord_less_e_q_int(number_number_of_int(A),one_one_int)|ord_less_e_q_int(A,bit1(pls)).
% 2.03/2.23 ** KEPT (pick-wt=8): 52 [] ord_less_e_q_int(number_number_of_int(A),one_one_int)| -ord_less_e_q_int(A,bit1(pls)).
% 2.03/2.23 ** KEPT (pick-wt=8): 53 [] -ord_less_e_q_int(one_one_int,number_number_of_int(A))|ord_less_e_q_int(bit1(pls),A).
% 2.03/2.23 ** KEPT (pick-wt=8): 54 [] ord_less_e_q_int(one_one_int,number_number_of_int(A))| -ord_less_e_q_int(bit1(pls),A).
% 2.03/2.23 ** KEPT (pick-wt=8): 55 [] -ord_less_int(number_number_of_int(A),number_number_of_int(B))|ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 56 [] ord_less_int(number_number_of_int(A),number_number_of_int(B))| -ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=7): 57 [] -ord_less_e_q_int(bit1(A),pls)|ord_less_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 58 [] ord_less_e_q_int(bit1(A),pls)| -ord_less_int(A,pls).
% 2.03/2.23 ** KEPT (pick-wt=7): 59 [] -ord_less_int(pls,bit1(A))|ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=7): 60 [] ord_less_int(pls,bit1(A))| -ord_less_e_q_int(pls,A).
% 2.03/2.23 ** KEPT (pick-wt=8): 61 [] -ord_less_e_q_int(bit1(A),bit0(B))|ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 62 [] ord_less_e_q_int(bit1(A),bit0(B))| -ord_less_int(A,B).
% 2.03/2.23 Following clause subsumed by 61 during input processing: 0 [] -ord_less_e_q_int(bit1(A),bit0(B))|ord_less_int(A,B).
% 2.03/2.23 Following clause subsumed by 62 during input processing: 0 [] ord_less_e_q_int(bit1(A),bit0(B))| -ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 63 [] -ord_less_int(bit0(A),bit1(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 64 [] ord_less_int(bit0(A),bit1(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 63 during input processing: 0 [] -ord_less_int(bit0(A),bit1(B))|ord_less_e_q_int(A,B).
% 2.03/2.23 Following clause subsumed by 64 during input processing: 0 [] ord_less_int(bit0(A),bit1(B))| -ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=11): 65 [] -ord_less_nat(number_number_of_nat(A),number_number_of_nat(B))| -ord_less_int(A,B)|ord_less_int(pls,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 66 [] -ord_less_nat(number_number_of_nat(A),number_number_of_nat(B))|ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=11): 67 [] ord_less_nat(number_number_of_nat(A),number_number_of_nat(B))| -ord_less_int(pls,B)| -ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=6): 68 [] -ord_less_e_q_int(one_one_int,A)|ord_less_int(zero_zero_int,A).
% 2.03/2.23 ** KEPT (pick-wt=6): 69 [] ord_less_e_q_int(one_one_int,A)| -ord_less_int(zero_zero_int,A).
% 2.03/2.23 ** KEPT (pick-wt=8): 70 [] -ord_less_int(A,B)|ord_less_e_q_int(plus_plus_int(A,one_one_int),B).
% 2.03/2.23 ** KEPT (pick-wt=8): 71 [] -ord_less_e_q_int(plus_plus_int(A,one_one_int),B)|ord_less_int(A,B).
% 2.03/2.23 Following clause subsumed by 70 during input processing: 0 [] ord_less_e_q_int(plus_plus_int(A,one_one_int),B)| -ord_less_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 72 [] -ord_less_int(A,plus_plus_int(B,one_one_int))|ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=8): 73 [] ord_less_int(A,plus_plus_int(B,one_one_int))| -ord_less_e_q_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=16): 75 [copy,74,flip.3] -ord_less_e_q_int(pls,A)| -ord_less_e_q_int(pls,B)|number_number_of_int(plus_plus_int(A,B))=plus_plus_int(number_number_of_int(A),number_number_of_int(B)).
% 2.03/2.23 ** KEPT (pick-wt=16): 77 [copy,76,flip.3] -ord_less_e_q_int(pls,A)| -ord_less_e_q_int(pls,B)|number_number_of_nat(plus_plus_int(A,B))=plus_plus_nat(number_number_of_nat(A),number_number_of_nat(B)).
% 2.03/2.23 ** KEPT (pick-wt=11): 78 [] -ord_less_int(A,pls)|plus_plus_nat(number_number_of_nat(A),number_number_of_nat(B))=number_number_of_nat(B).
% 2.03/2.23 ** KEPT (pick-wt=14): 79 [] ord_less_int(A,pls)| -ord_less_int(B,pls)|plus_plus_nat(number_number_of_nat(A),number_number_of_nat(B))=number_number_of_nat(A).
% 2.03/2.23 ** KEPT (pick-wt=8): 80 [] -ord_less_e_q_int(zero_zero_int,A)|ord_less_int(zero_zero_int,plus_plus_int(one_one_int,A)).
% 2.03/2.23 ** KEPT (pick-wt=8): 81 [] number_number_of_int(A)!=number_number_of_int(B)|A=B.
% 2.03/2.23 ** KEPT (pick-wt=8): 82 [] number_number_of_int(A)=number_number_of_int(B)|A!=B.
% 2.03/2.23 ** KEPT (pick-wt=8): 83 [] number_number_of_nat(A)!=B|B=number_number_of_nat(A).
% 2.03/2.23 ** KEPT (pick-wt=8): 84 [] number_number_of_nat(A)=B|B!=number_number_of_nat(A).
% 2.03/2.23 ** KEPT (pick-wt=8): 85 [] number_number_of_int(A)!=B|B=number_number_of_int(A).
% 2.03/2.23 ** KEPT (pick-wt=8): 86 [] number_number_of_int(A)=B|B!=number_number_of_int(A).
% 2.03/2.23 ** KEPT (pick-wt=8): 87 [] bit1(A)!=bit1(B)|A=B.
% 2.03/2.23 ** KEPT (pick-wt=8): 88 [] bit1(A)=bit1(B)|A!=B.
% 2.03/2.23 ** KEPT (pick-wt=8): 89 [] bit0(A)!=bit0(B)|A=B.
% 2.03/2.23 ** KEPT (pick-wt=8): 90 [] bit0(A)=bit0(B)|A!=B.
% 2.03/2.23 ** KEPT (pick-wt=12): 91 [] plus_plus_int(times_times_int(A,A),times_times_int(B,B))!=zero_zero_int|A=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=12): 92 [] plus_plus_int(times_times_int(A,A),times_times_int(B,B))!=zero_zero_int|B=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=15): 93 [] plus_plus_int(times_times_int(A,A),times_times_int(B,B))=zero_zero_int|A!=zero_zero_int|B!=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=10): 94 [] -ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int).
% 2.03/2.23
% 2.03/2.23 ------------> process sos:
% 2.03/2.23 ** KEPT (pick-wt=3): 105 [] A=A.
% 2.03/2.23 ** KEPT (pick-wt=3): 106 [] ord_less_int(t,zero_zero_int).
% 2.03/2.23 ** KEPT (pick-wt=3): 107 [] ord_less_int(t,one_one_int).
% 2.03/2.23 ** KEPT (pick-wt=23): 108 [] ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)).
% 2.03/2.23 ** KEPT (pick-wt=20): 109 [] plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t).
% 2.03/2.23 ---> New Demodulator: 110 [new_demod,109] plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t).
% 2.03/2.23 ** KEPT (pick-wt=11): 111 [] ord_less_int(zero_zero_int,plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 ** KEPT (pick-wt=18): 112 [] ord_less_int(zero_zero_int,plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls))))))|A=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=18): 113 [] ord_less_int(zero_zero_int,plus_plus_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),power_power_int(B,number_number_of_nat(bit0(bit1(pls))))))|B=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=11): 114 [] ord_less_int(zero_zero_int,power_power_int(A,number_number_of_nat(bit0(bit1(pls)))))|A=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=8): 115 [] power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls))))=one_one_nat.
% 2.03/2.23 ---> New Demodulator: 116 [new_demod,115] power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls))))=one_one_nat.
% 2.03/2.23 ** KEPT (pick-wt=8): 117 [] power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls))))=one_one_int.
% 2.03/2.23 ---> New Demodulator: 118 [new_demod,117] power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls))))=one_one_int.
% 2.03/2.23 ** KEPT (pick-wt=8): 119 [] power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls))))=zero_zero_nat.
% 2.03/2.23 ---> New Demodulator: 120 [new_demod,119] power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls))))=zero_zero_nat.
% 2.03/2.23 ** KEPT (pick-wt=8): 121 [] power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int.
% 2.03/2.23 ---> New Demodulator: 122 [new_demod,121] power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls))))=zero_zero_int.
% 2.03/2.23 ** KEPT (pick-wt=10): 124 [copy,123,flip.1] number_number_of_int(plus_plus_int(bit1(pls),A))=plus_plus_int(one_one_int,number_number_of_int(A)).
% 2.03/2.23 ---> New Demodulator: 125 [new_demod,124] number_number_of_int(plus_plus_int(bit1(pls),A))=plus_plus_int(one_one_int,number_number_of_int(A)).
% 2.03/2.23 ** KEPT (pick-wt=10): 127 [copy,126,flip.1] number_number_of_int(plus_plus_int(A,bit1(pls)))=plus_plus_int(number_number_of_int(A),one_one_int).
% 2.03/2.23 ---> New Demodulator: 128 [new_demod,127] number_number_of_int(plus_plus_int(A,bit1(pls)))=plus_plus_int(number_number_of_int(A),one_one_int).
% 2.03/2.23 ** KEPT (pick-wt=11): 129 [] ord_less_int(t,plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 ** KEPT (pick-wt=23): 131 [copy,130,demod,110] times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),$c1).
% 2.03/2.23 ---> New Demodulator: 132 [new_demod,131] times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t)=times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),$c1).
% 2.03/2.23 ** KEPT (pick-wt=10): 133 [] zprime(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int)).
% 2.03/2.23 ** KEPT (pick-wt=12): 135 [copy,134,demod,132] twoSqu526106917sum2sq(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),$c1)).
% 2.03/2.23 ** KEPT (pick-wt=3): 136 [] ord_less_e_q_int(A,A).
% 2.03/2.23 ** KEPT (pick-wt=4): 137 [] number_number_of_int(A)=A.
% 2.03/2.23 ---> New Demodulator: 138 [new_demod,137] number_number_of_int(A)=A.
% 2.03/2.23 ** KEPT (pick-wt=7): 139 [] times_times_int(A,B)=times_times_int(B,A).
% 2.03/2.23 ** KEPT (pick-wt=6): 140 [] ord_less_e_q_int(A,B)|ord_less_e_q_int(B,A).
% 2.03/2.23 Following clause subsumed by 105 during input processing: 0 [demod,138,138,138] times_times_int(A,B)=times_times_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=11): 141 [] times_times_int(times_times_int(A,B),C)=times_times_int(A,times_times_int(B,C)).
% 2.03/2.23 ---> New Demodulator: 142 [new_demod,141] times_times_int(times_times_int(A,B),C)=times_times_int(A,times_times_int(B,C)).
% 2.03/2.23 ** KEPT (pick-wt=13): 144 [copy,143,flip.1] times_times_int(power_power_int(A,B),power_power_int(A,C))=power_power_int(A,plus_plus_nat(B,C)).
% 2.03/2.23 ---> New Demodulator: 145 [new_demod,144] times_times_int(power_power_int(A,B),power_power_int(A,C))=power_power_int(A,plus_plus_nat(B,C)).
% 2.03/2.23 Following clause subsumed by 136 during input processing: 0 [] ord_less_e_q_int(pls,pls).
% 2.03/2.23 Following clause subsumed by 105 during input processing: 0 [demod,138,138,138,142] times_times_int(A,times_times_int(B,C))=times_times_int(A,times_times_int(B,C)).
% 2.03/2.23 Following clause subsumed by 105 during input processing: 0 [demod,138,138,138] times_times_int(A,B)=times_times_int(A,B).
% 2.03/2.23 Following clause subsumed by 105 during input processing: 0 [demod,138,138,138] times_times_int(A,B)=times_times_int(A,B).
% 2.03/2.23 ** KEPT (pick-wt=9): 146 [] ord_less_e_q_int(zero_zero_int,plus_plus_int(times_times_int(A,A),times_times_int(B,B))).
% 2.03/2.23 ** KEPT (pick-wt=6): 148 [copy,147,demod,138,138,138,138] ord_less_e_q_int(A,B)|ord_less_int(B,A).
% 2.03/2.23 ** KEPT (pick-wt=10): 149 [] ord_less_e_q_nat(number_number_of_nat(A),number_number_of_nat(B))|ord_less_nat(number_number_of_nat(B),number_number_of_nat(A)).
% 2.03/2.23 ** KEPT (pick-wt=4): 150 [] number_number_of_nat(pls)=zero_zero_nat.
% 2.03/2.23 ---> New Demodulator: 151 [new_demod,150] number_number_of_nat(pls)=zero_zero_nat.
% 2.03/2.23 Following clause subsumed by 105 during input processing: 0 [demod,151] zero_zero_nat=zero_zero_nat.
% 2.03/2.23 ** KEPT (pick-wt=8): 153 [copy,152,flip.1] number_number_of_nat(bit0(bit1(pls)))=plus_plus_nat(one_one_nat,one_one_nat).
% 2.03/2.24 ---> New Demodulator: 154 [new_demod,153] number_number_of_nat(bit0(bit1(pls)))=plus_plus_nat(one_one_nat,one_one_nat).
% 2.03/2.24 ** KEPT (pick-wt=5): 155 [] times_times_int(pls,A)=pls.
% 2.03/2.24 ---> New Demodulator: 156 [new_demod,155] times_times_int(pls,A)=pls.
% 2.03/2.24 ** KEPT (pick-wt=9): 158 [copy,157,flip.1] bit0(times_times_int(A,B))=times_times_int(bit0(A),B).
% 2.03/2.24 ---> New Demodulator: 159 [new_demod,158] bit0(times_times_int(A,B))=times_times_int(bit0(A),B).
% 2.03/2.24 ** KEPT (pick-wt=5): 160 [] times_times_int(A,one_one_int)=A.
% 2.03/2.24 ---> New Demodulator: 161 [new_demod,160] times_times_int(A,one_one_int)=A.
% 2.03/2.24 ** KEPT (pick-wt=5): 162 [] times_times_int(one_one_int,A)=A.
% 2.03/2.24 ---> New Demodulator: 163 [new_demod,162] times_times_int(one_one_int,A)=A.
% 2.03/2.24 Following clause subsumed by 105 during input processing: 0 [demod,138,138,138] plus_plus_int(A,B)=plus_plus_int(A,B).
% 2.03/2.24 ** KEPT (pick-wt=13): 164 [] times_times_int(plus_plus_int(A,B),C)=plus_plus_int(times_times_int(A,C),times_times_int(B,C)).
% 2.03/2.24 ---> New Demodulator: 165 [new_demod,164] times_times_int(plus_plus_int(A,B),C)=plus_plus_int(times_times_int(A,C),times_times_int(B,C)).
% 2.03/2.24 ** KEPT (pick-wt=13): 166 [] times_times_int(A,plus_plus_int(B,C))=plus_plus_int(times_times_int(A,B),times_times_int(A,C)).
% 2.03/2.24 ---> New Demodulator: 167 [new_demod,166] times_times_int(A,plus_plus_int(B,C))=plus_plus_int(times_times_int(A,B),times_times_int(A,C)).
% 2.03/2.24 ** KEPT (pick-wt=5): 168 [] number_number_of_nat(bit1(pls))=one_one_nat.
% 2.03/2.24 ---> New Demodulator: 169 [new_demod,168] number_number_of_nat(bit1(pls))=one_one_nat.
% 2.03/2.24 Following clause subsumed by 105 during input processing: 0 [demod,169] one_one_nat=one_one_nat.
% 2.03/2.24 ** KEPT (pick-wt=16): 171 [copy,170,flip.3] ord_less_int(A,pls)|ord_less_int(B,pls)|number_number_of_nat(plus_plus_int(A,B))=plus_plus_nat(number_number_of_nat(A),number_number_of_nat(B)).
% 2.03/2.24 ** KEPT (pick-wt=9): 172 [] ord_less_int(A,B)|A=B|ord_less_int(B,A).
% 2.03/2.24 Following clause subsumed by 105 during input processing: 0 [demod,138,165,138,138] plus_plus_int(times_times_int(A,C),times_times_int(B,C))=plus_plus_int(times_times_int(A,C),times_times_int(B,C)).
% 2.03/2.24 ** KEPT (pick-wt=16): 173 [] times_times_nat(plus_plus_nat(A,B),number_number_of_nat(C))=plus_plus_nat(times_times_nat(A,number_number_of_nat(C)),times_times_nat(B,number_number_of_nat(C))).
% 2.03/2.24 ---> New Demodulator: 174 [new_demod,173] times_times_nat(plus_plus_nat(A,B),number_number_of_nat(C))=plus_plus_nat(times_times_nat(A,number_number_of_nat(C)),times_times_nat(B,number_number_of_nat(C))).
% 2.03/2.24 Following clause subsumed by 105 during input processing: 0 [demod,138,167,138,138] plus_plus_int(times_times_int(A,B),times_times_int(A,C))=plus_plus_int(times_times_int(A,B),times_times_int(A,C)).
% 2.03/2.24 ** KEPT (pick-wt=16): 175 [] times_times_nat(number_number_of_nat(A),plus_plus_nat(B,C))=plus_plus_nat(times_times_nat(number_number_of_nat(A),B),times_times_nat(number_number_of_nat(A),C)).
% 2.03/2.24 ---> New Demodulator: 176 [new_demod,175] times_times_nat(number_number_of_nat(A),plus_plus_nat(B,C))=plus_plus_nat(times_times_nat(number_number_of_nat(A),B),times_times_nat(number_number_of_nat(A),C)).
% 2.03/2.24 ** KEPT (pick-wt=11): 177 [] plus_plus_int(plus_plus_int(A,B),C)=plus_plus_int(A,plus_plus_int(B,C)).
% 2.03/2.24 ---> New Demodulator: 178 [new_demod,177] plus_plus_int(plus_plus_int(A,B),C)=plus_plus_int(A,plus_plus_int(B,C)).
% 2.03/2.24 ** KEPT (pick-wt=11): 179 [] plus_plus_int(A,plus_plus_int(B,C))=plus_plus_int(B,plus_plus_int(A,C)).
% 2.03/2.24 ** KEPT (pick-wt=7): 180 [] plus_plus_int(A,B)=plus_plus_int(B,A).
% 2.03/2.24 ** KEPT (pick-wt=3): 182 [copy,181,demod,138] zero_zero_int=pls.
% 2.03/2.24 ---> New Demodulator: 183 [new_demod,182] zero_zero_int=pls.
% 2.03/2.24 Following clause subsumed by 105 during input processing: 0 [copy,105,flip.1] A=A.
% 2.03/2.24 105 back subsumes 97.
% 2.03/2.24 >>>> Starting back demodulation with 110.
% 2.03/2.24 >> back demodulating 94 with 110.
% 2.03/2.24 >> back demodulating 2 with 110.
% 2.03/2.24 >>>> Starting back demodulation with 116.
% 2.03/2.24 >>>> Starting back demodulation with 118.
% 2.03/2.24 >>>> Starting back demodulation with 120.
% 2.03/2.24 >>>> Starting back demodulation with 122.
% 2.03/2.24 >>>> Starting back demodulation with 125.
% 2.03/2.27 >>>> Starting back demodulation with 128.
% 2.03/2.27 >>>> Starting back demodulation with 132.
% 2.03/2.27 >> back demodulating 109 with 132.
% 2.03/2.27 >> back demodulating 108 with 132.
% 2.03/2.27 >>>> Starting back demodulation with 138.
% 2.03/2.27 >> back demodulating 135 with 138.
% 2.03/2.27 >> back demodulating 133 with 138.
% 2.03/2.27 >> back demodulating 131 with 138.
% 2.03/2.27 >> back demodulating 129 with 138.
% 2.03/2.27 >> back demodulating 127 with 138.
% 2.03/2.27 >> back demodulating 124 with 138.
% 2.03/2.27 >> back demodulating 111 with 138.
% 2.03/2.27 >> back demodulating 102 with 138.
% 2.03/2.27 >> back demodulating 99 with 138.
% 2.03/2.27 >> back demodulating 86 with 138.
% 2.03/2.27 >> back demodulating 85 with 138.
% 2.03/2.27 >> back demodulating 82 with 138.
% 2.03/2.27 >> back demodulating 81 with 138.
% 2.03/2.27 >> back demodulating 75 with 138.
% 2.03/2.27 >> back demodulating 56 with 138.
% 2.03/2.27 >> back demodulating 55 with 138.
% 2.03/2.27 >> back demodulating 54 with 138.
% 2.03/2.27 >> back demodulating 53 with 138.
% 2.03/2.27 >> back demodulating 52 with 138.
% 2.03/2.27 >> back demodulating 51 with 138.
% 2.03/2.27 >> back demodulating 40 with 138.
% 2.03/2.27 >> back demodulating 37 with 138.
% 2.03/2.27 >> back demodulating 36 with 138.
% 2.03/2.27 >> back demodulating 35 with 138.
% 2.03/2.27 >> back demodulating 34 with 138.
% 2.03/2.27 >> back demodulating 30 with 138.
% 2.03/2.27 >> back demodulating 14 with 138.
% 2.03/2.27 >> back demodulating 13 with 138.
% 2.03/2.27 Following clause subsumed by 139 during input processing: 0 [copy,139,flip.1] times_times_int(A,B)=times_times_int(B,A).
% 2.03/2.27 >>>> Starting back demodulation with 142.
% 2.03/2.27 >>>> Starting back demodulation with 145.
% 2.03/2.27 >>>> Starting back demodulation with 151.
% 2.03/2.27 >> back demodulating 101 with 151.
% 2.03/2.27 >>>> Starting back demodulation with 154.
% 2.03/2.27 >> back demodulating 121 with 154.
% 2.03/2.27 >> back demodulating 119 with 154.
% 2.03/2.27 >> back demodulating 117 with 154.
% 2.03/2.27 >> back demodulating 115 with 154.
% 2.03/2.27 >> back demodulating 114 with 154.
% 2.03/2.27 >> back demodulating 113 with 154.
% 2.03/2.27 >> back demodulating 112 with 154.
% 2.03/2.27 >> back demodulating 96 with 154.
% 2.03/2.27 >> back demodulating 95 with 154.
% 2.03/2.27 >> back demodulating 12 with 154.
% 2.03/2.27 >> back demodulating 11 with 154.
% 2.03/2.27 >> back demodulating 10 with 154.
% 2.03/2.27 >> back demodulating 9 with 154.
% 2.03/2.27 >> back demodulating 8 with 154.
% 2.03/2.27 >> back demodulating 7 with 154.
% 2.03/2.27 >> back demodulating 6 with 154.
% 2.03/2.27 >> back demodulating 5 with 154.
% 2.03/2.27 >> back demodulating 4 with 154.
% 2.03/2.27 >>>> Starting back demodulation with 156.
% 2.03/2.27 >>>> Starting back demodulation with 159.
% 2.03/2.27 >>>> Starting back demodulation with 161.
% 2.03/2.27 >>>> Starting back demodulation with 163.
% 2.03/2.27 >>>> Starting back demodulation with 165.
% 2.03/2.27 >>>> Starting back demodulation with 167.
% 2.03/2.27 >>>> Starting back demodulation with 169.
% 2.03/2.27 >>>> Starting back demodulation with 174.
% 2.03/2.27 >>>> Starting back demodulation with 176.
% 2.03/2.27 >>>> Starting back demodulation with 178.
% 2.03/2.27 Following clause subsumed by 179 during input processing: 0 [copy,179,flip.1] plus_plus_int(A,plus_plus_int(B,C))=plus_plus_int(B,plus_plus_int(A,C)).
% 2.03/2.27 Following clause subsumed by 180 during input processing: 0 [copy,180,flip.1] plus_plus_int(A,B)=plus_plus_int(B,A).
% 2.03/2.27 >>>> Starting back demodulation with 183.
% 2.03/2.27 >> back demodulating 146 with 183.
% 2.03/2.27 >> back demodulating 106 with 183.
% 2.03/2.27 >> back demodulating 104 with 183.
% 2.03/2.27 >> back demodulating 100 with 183.
% 2.03/2.27 >> back demodulating 93 with 183.
% 2.03/2.27 >> back demodulating 92 with 183.
% 2.03/2.27 >> back demodulating 91 with 183.
% 2.03/2.27 >> back demodulating 80 with 183.
% 2.03/2.27 >> back demodulating 69 with 183.
% 2.03/2.27 >> back demodulating 68 with 183.
% 2.03/2.27 >> back demodulating 33 with 183.
% 2.03/2.27 >> back demodulating 32 with 183.
% 2.03/2.27 >> back demodulating 31 with 183.
% 2.03/2.27 >>>> Starting back demodulation with 187.
% 2.03/2.27 >>>> Starting back demodulation with 192.
% 2.03/2.27 >> back demodulating 189 with 192.
% 2.03/2.27 >>>> Starting back demodulation with 195.
% 2.03/2.27 >>>> Starting back demodulation with 197.
% 2.03/2.27 199 back subsumes 84.
% 2.03/2.27 199 back subsumes 83.
% 2.03/2.27 >>>> Starting back demodulation with 206.
% 2.03/2.27 >>>> Starting back demodulation with 208.
% 2.03/2.27 >>>> Starting back demodulation with 210.
% 2.03/2.27 >>>> Starting back demodulation with 212.
% 2.03/2.27
% 2.03/2.27 ======= end of input processing =======
% 2.03/2.27
% 2.03/2.27 =========== start of search ===========
% 2.03/2.27
% 2.03/2.27 -------- PROOF --------
% 2.03/2.27
% 2.03/2.27 ----> UNIT CONFLICT at 0.04 sec ----> 1577 [binary,1576.1,184.1] $F.
% 2.03/2.27
% 2.03/2.27 Length of proof is 9. Level of proof is 5.
% 2.03/2.27
% 2.03/2.27 ---------------- PROOF ----------------
% 2.03/2.27 % SZS status Theorem
% 2.03/2.27 % SZS output start Refutation
% See solution above
% 2.03/2.27 ------------ end of proof -------------
% 2.03/2.27
% 2.03/2.27
% 2.03/2.27 Search stopped by max_proofs option.
% 2.03/2.27
% 2.03/2.27
% 2.03/2.27 Search stopped by max_proofs option.
% 2.03/2.27
% 2.03/2.27 ============ end of search ============
% 2.03/2.27
% 2.03/2.27 -------------- statistics -------------
% 2.03/2.27 clauses given 56
% 2.03/2.27 clauses generated 2079
% 2.03/2.27 clauses kept 1446
% 2.03/2.27 clauses forward subsumed 939
% 2.03/2.27 clauses back subsumed 11
% 2.03/2.27 Kbytes malloced 3906
% 2.03/2.27
% 2.03/2.27 ----------- times (seconds) -----------
% 2.03/2.27 user CPU time 0.04 (0 hr, 0 min, 0 sec)
% 2.03/2.27 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 2.03/2.27 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 2.03/2.27
% 2.03/2.27 That finishes the proof of the theorem.
% 2.03/2.27
% 2.03/2.27 Process 26913 finished Wed Jul 27 09:04:20 2022
% 2.03/2.27 Otter interrupted
% 2.03/2.27 PROOF FOUND
%------------------------------------------------------------------------------