%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NUM925+5 : TPTP v8.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n028.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:17 EDT 2022 % Result : Unknown 53.24s 53.39s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : NUM925+5 : TPTP v8.1.0. Released v5.3.0. % 0.10/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n028.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:54:19 EDT 2022 % 0.12/0.33 % CPUTime : % 2.17/2.37 ----- Otter 3.3f, August 2004 ----- % 2.17/2.37 The process was started by sandbox2 on n028.cluster.edu, % 2.17/2.37 Wed Jul 27 09:54:19 2022 % 2.17/2.37 The command was "./otter". The process ID is 5700. % 2.17/2.37 % 2.17/2.37 set(prolog_style_variables). % 2.17/2.37 set(auto). % 2.17/2.37 dependent: set(auto1). % 2.17/2.37 dependent: set(process_input). % 2.17/2.37 dependent: clear(print_kept). % 2.17/2.37 dependent: clear(print_new_demod). % 2.17/2.37 dependent: clear(print_back_demod). % 2.17/2.37 dependent: clear(print_back_sub). % 2.17/2.37 dependent: set(control_memory). % 2.17/2.37 dependent: assign(max_mem, 12000). % 2.17/2.37 dependent: assign(pick_given_ratio, 4). % 2.17/2.37 dependent: assign(stats_level, 1). % 2.17/2.37 dependent: assign(max_seconds, 10800). % 2.17/2.37 clear(print_given). % 2.17/2.37 % 2.17/2.37 formula_list(usable). % 2.17/2.37 all A (A=A). % 2.17/2.37 all X_a (power(X_a)&semiring_0(X_a)->ti(X_a,one_one(X_a))=one_one(X_a)). % 2.17/2.37 all B_1 B_2 X_a (linord219039673up_add(X_a)->plus_plus(X_a,ti(X_a,B_1),B_2)=plus_plus(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (linord219039673up_add(X_a)->plus_plus(X_a,B_1,ti(X_a,B_2))=plus_plus(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (linord219039673up_add(X_a)->ti(X_a,plus_plus(X_a,B_1,B_2))=plus_plus(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (number_semiring(X_a)->plus_plus(X_a,ti(X_a,B_1),B_2)=plus_plus(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (number_semiring(X_a)->plus_plus(X_a,B_1,ti(X_a,B_2))=plus_plus(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (number_semiring(X_a)->ti(X_a,plus_plus(X_a,B_1,B_2))=plus_plus(X_a,B_1,B_2)). % 2.17/2.37 all X_a (power(X_a)&mult_zero(X_a)&no_zero_divisors(X_a)&zero_ne_q_one(X_a)->ti(X_a,zero_zero(X_a))=zero_zero(X_a)). % 2.17/2.37 all X_a (linord219039673up_add(X_a)->ti(X_a,zero_zero(X_a))=zero_zero(X_a)). % 2.17/2.37 all X_a (power(X_a)&semiring_0(X_a)->ti(X_a,zero_zero(X_a))=zero_zero(X_a)). % 2.17/2.37 all X_a (ti(X_a,undefined(X_a))=undefined(X_a)). % 2.17/2.37 all B_1 (bit0(ti(int,B_1))=bit0(B_1)). % 2.17/2.37 all B_1 (ti(int,bit0(B_1))=bit0(B_1)). % 2.17/2.37 all B_1 (bit1(ti(int,B_1))=bit1(B_1)). % 2.17/2.37 all B_1 (ti(int,bit1(B_1))=bit1(B_1)). % 2.17/2.37 ti(int,pls)=pls. % 2.17/2.37 all B_1 X_a (number(X_a)->number_number_of(X_a,ti(int,B_1))=number_number_of(X_a,B_1)). % 2.17/2.37 all B_1 X_a (number(X_a)->ti(X_a,number_number_of(X_a,B_1))=number_number_of(X_a,B_1)). % 2.17/2.37 all B_1 X_a (number_semiring(X_a)->semiring_1_of_nat(X_a,ti(nat,B_1))=semiring_1_of_nat(X_a,B_1)). % 2.17/2.37 all B_1 X_a (number_semiring(X_a)->ti(X_a,semiring_1_of_nat(X_a,B_1))=semiring_1_of_nat(X_a,B_1)). % 2.17/2.37 all B_1 B_2 X_a (linordered_idom(X_a)-> (ord_less(X_a,ti(X_a,B_1),B_2)<->ord_less(X_a,B_1,B_2))). % 2.17/2.37 all B_1 B_2 X_a (linordered_idom(X_a)-> (ord_less(X_a,B_1,ti(X_a,B_2))<->ord_less(X_a,B_1,B_2))). % 2.17/2.37 all B_1 B_2 (ord_less(nat,ti(nat,B_1),B_2)<->ord_less(nat,B_1,B_2)). % 2.17/2.37 all B_1 B_2 (ord_less(nat,B_1,ti(nat,B_2))<->ord_less(nat,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (power(X_a)&mult_zero(X_a)&no_zero_divisors(X_a)&zero_ne_q_one(X_a)->power_power(X_a,ti(X_a,B_1),B_2)=power_power(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (power(X_a)&mult_zero(X_a)&no_zero_divisors(X_a)&zero_ne_q_one(X_a)->power_power(X_a,B_1,ti(nat,B_2))=power_power(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (power(X_a)&mult_zero(X_a)&no_zero_divisors(X_a)&zero_ne_q_one(X_a)->ti(X_a,power_power(X_a,B_1,B_2))=power_power(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (power(X_a)&semiring_0(X_a)->power_power(X_a,ti(X_a,B_1),B_2)=power_power(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (power(X_a)&semiring_0(X_a)->power_power(X_a,B_1,ti(nat,B_2))=power_power(X_a,B_1,B_2)). % 2.17/2.37 all B_1 B_2 X_a (power(X_a)&semiring_0(X_a)->ti(X_a,power_power(X_a,B_1,B_2))=power_power(X_a,B_1,B_2)). % 2.17/2.37 ti(nat,n)=n. % 2.17/2.37 ti(int,t)=t. % 2.17/2.37 ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))). % 2.17/2.37 ord_less(int,one_one(int),t). % 2.17/2.37 all X_a (linordered_idom(X_a)-> (all Xa Ya (plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)<->ti(X_a,Xa)=zero_zero(X_a)&ti(X_a,Ya)=zero_zero(X_a)))). % 2.17/2.37 all X_a (semiring_1(X_a)->power_power(X_a,one_one(X_a),number_number_of(nat,bit0(bit1(pls))))=one_one(X_a)). % 2.17/2.37 all X_a (semiring_1(X_a)->power_power(X_a,zero_zero(X_a),number_number_of(nat,bit0(bit1(pls))))=zero_zero(X_a)). % 2.17/2.37 all X_a (ring_11004092258visors(X_a)-> (all A_2 (power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls))))=zero_zero(X_a)<->ti(X_a,A_2)=zero_zero(X_a)))). % 2.17/2.37 all X_a (number_ring(X_a)-> (all W (plus_plus(X_a,one_one(X_a),number_number_of(X_a,W))=number_number_of(X_a,plus_plus(int,bit1(pls),W))))). % 2.17/2.37 all X_a (number_ring(X_a)-> (all V (plus_plus(X_a,number_number_of(X_a,V),one_one(X_a))=number_number_of(X_a,plus_plus(int,V,bit1(pls)))))). % 2.17/2.37 all X_a (number_ring(X_a)->plus_plus(X_a,one_one(X_a),one_one(X_a))=number_number_of(X_a,bit0(bit1(pls)))). % 2.17/2.37 all X_a (number_semiring(X_a)->plus_plus(X_a,one_one(X_a),one_one(X_a))=number_number_of(X_a,bit0(bit1(pls)))). % 2.17/2.37 all X (power_power(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),number_number_of(nat,bit0(bit1(pls))))=power_power(int,X,number_number_of(nat,bit0(bit0(bit1(pls)))))). % 2.17/2.37 all X_a (power(X_a)&semiring_0(X_a)-> (all W ((number_number_of(nat,W)=zero_zero(nat)->power_power(X_a,zero_zero(X_a),number_number_of(nat,W))=one_one(X_a))& (number_number_of(nat,W)!=zero_zero(nat)->power_power(X_a,zero_zero(X_a),number_number_of(nat,W))=zero_zero(X_a))))). % 2.17/2.37 all X_a (number_ring(X_a)->one_one(X_a)=number_number_of(X_a,bit1(pls))). % 2.17/2.37 all X_a (number_ring(X_a)->number_number_of(X_a,bit1(pls))=one_one(X_a)). % 2.17/2.37 ord_less(nat,zero_zero(nat),n). % 2.17/2.37 all X Y (ord_less(int,X,Y)|X=Y|ord_less(int,Y,X)). % 2.17/2.37 all K_1 L_1 (ord_less(int,number_number_of(int,K_1),number_number_of(int,L_1))<->ord_less(int,K_1,L_1)). % 2.17/2.37 all V W (plus_plus(int,number_number_of(int,V),number_number_of(int,W))=number_number_of(int,plus_plus(int,V,W))). % 2.17/2.37 all X_a (number_ring(X_a)&linordered_idom(X_a)-> (all Xa Ya (ord_less(X_a,number_number_of(X_a,Xa),number_number_of(X_a,Ya))<->ord_less(int,Xa,Ya)))). % 2.17/2.37 zero_zero(int)=number_number_of(int,pls). % 2.17/2.37 all M N (power_power(int,semiring_1_of_nat(int,M),N)=semiring_1_of_nat(int,power_power(nat,M,N))). % 2.17/2.37 all M N (semiring_1_of_nat(int,power_power(nat,M,N))=power_power(int,semiring_1_of_nat(int,M),N)). % 2.17/2.37 all M N Z (plus_plus(int,semiring_1_of_nat(int,M),plus_plus(int,semiring_1_of_nat(int,N),Z))=plus_plus(int,semiring_1_of_nat(int,plus_plus(nat,M,N)),Z)). % 2.17/2.37 all M N (plus_plus(int,semiring_1_of_nat(int,M),semiring_1_of_nat(int,N))=semiring_1_of_nat(int,plus_plus(nat,M,N))). % 2.17/2.37 semiring_1_of_nat(int,one_one(nat))=one_one(int). % 2.17/2.37 number_number_of(nat,pls)=zero_zero(nat). % 2.17/2.37 zero_zero(nat)=number_number_of(nat,pls). % 2.17/2.37 all Na (semiring_1_of_nat(int,Na)=zero_zero(int)<->Na=zero_zero(nat)). % 2.17/2.37 semiring_1_of_nat(int,zero_zero(nat))=zero_zero(int). % 2.17/2.37 plus_plus(nat,one_one(nat),one_one(nat))=number_number_of(nat,bit0(bit1(pls))). % 2.17/2.37 all K1 K2 (ord_less(int,bit1(K1),bit1(K2))<->ord_less(int,K1,K2)). % 2.17/2.37 all K_1 L_1 (ord_less(int,bit1(K_1),bit1(L_1))<->ord_less(int,K_1,L_1)). % 2.17/2.37 -ord_less(int,pls,pls). % 2.17/2.37 all K1 K2 (ord_less(int,bit0(K1),bit0(K2))<->ord_less(int,K1,K2)). % 2.17/2.37 all K_1 L_1 (ord_less(int,bit0(K_1),bit0(L_1))<->ord_less(int,K_1,L_1)). % 2.17/2.37 all K I J (ord_less(int,I,J)->ord_less(int,plus_plus(int,I,K),plus_plus(int,J,K))). % 2.17/2.37 all V_1 V ((ord_less(int,V,pls)->plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1))=number_number_of(nat,V_1))& (-ord_less(int,V,pls)-> (ord_less(int,V_1,pls)->plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1))=number_number_of(nat,V))& (-ord_less(int,V_1,pls)->plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1))=number_number_of(nat,plus_plus(int,V,V_1))))). % 2.17/2.37 one_one(int)=number_number_of(int,bit1(pls)). % 2.17/2.37 number_number_of(nat,bit1(pls))=one_one(nat). % 2.17/2.37 one_one(nat)=number_number_of(nat,bit1(pls)). % 2.17/2.37 all X_a (number_ring(X_a)&ring_char_0(X_a)-> (all Xa Ya (number_number_of(X_a,Xa)=number_number_of(X_a,Ya)<->Xa=Ya))). % 2.17/2.37 all X_a (number(X_a)-> (all Wa Xa (number_number_of(X_a,Wa)=ti(X_a,Xa)<->ti(X_a,Xa)=number_number_of(X_a,Wa)))). % 2.17/2.37 all K_1 L_1 (bit1(K_1)=bit1(L_1)<->K_1=L_1). % 2.17/2.37 all K_1 L_1 (bit0(K_1)=bit0(L_1)<->K_1=L_1). % 2.17/2.37 all X_a (linordered_idom(X_a)-> (all A_2 (ord_less(X_a,plus_plus(X_a,A_2,A_2),zero_zero(X_a))<->ord_less(X_a,A_2,zero_zero(X_a))))). % 2.17/2.37 all Z1 Z2 Z3 (plus_plus(int,plus_plus(int,Z1,Z2),Z3)=plus_plus(int,Z1,plus_plus(int,Z2,Z3))). % 2.17/2.37 all X Y Z (plus_plus(int,X,plus_plus(int,Y,Z))=plus_plus(int,Y,plus_plus(int,X,Z))). % 2.17/2.37 all Z W (plus_plus(int,Z,W)=plus_plus(int,W,Z)). % 2.17/2.37 all Ma Na (semiring_1_of_nat(int,Ma)=semiring_1_of_nat(int,Na)<->Ma=Na). % 2.17/2.37 all X_a (number_ring(X_a)&linordered_idom(X_a)-> (all Xa (ord_less(X_a,number_number_of(X_a,Xa),zero_zero(X_a))<->ord_less(int,Xa,pls)))). % 2.17/2.37 all X_a (number_ring(X_a)&linordered_idom(X_a)-> (all Ya (ord_less(X_a,zero_zero(X_a),number_number_of(X_a,Ya))<->ord_less(int,pls,Ya)))). % 2.17/2.37 all K_1 (ord_less(int,bit1(K_1),pls)<->ord_less(int,K_1,pls)). % 2.17/2.37 all K1 K2 (ord_less(int,bit1(K1),bit0(K2))<->ord_less(int,K1,K2)). % 2.17/2.37 all K_1 L_1 (ord_less(int,bit1(K_1),bit0(L_1))<->ord_less(int,K_1,L_1)). % 2.17/2.37 all K_1 (ord_less(int,bit0(K_1),pls)<->ord_less(int,K_1,pls)). % 2.17/2.37 all K_1 (ord_less(int,pls,bit0(K_1))<->ord_less(int,pls,K_1)). % 2.17/2.37 all Wa (ord_less(int,bit1(Wa),zero_zero(int))<->ord_less(int,Wa,zero_zero(int))). % 2.17/2.37 -ord_less(int,pls,zero_zero(int)). % 2.17/2.37 all Wa (ord_less(int,bit0(Wa),zero_zero(int))<->ord_less(int,Wa,zero_zero(int))). % 2.17/2.37 ord_less(int,zero_zero(int),one_one(int)). % 2.17/2.37 all Wa Z_1 (ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))<->ord_less(int,Wa,Z_1)|Wa=Z_1). % 2.17/2.37 all K (-ord_less(int,semiring_1_of_nat(int,K),zero_zero(int))). % 2.17/2.37 all X_a (number_ring(X_a)&linordered_idom(X_a)-> (all Xa (ord_less(X_a,number_number_of(X_a,Xa),one_one(X_a))<->ord_less(int,Xa,bit1(pls))))). % 2.17/2.37 all X_a (number_ring(X_a)&linordered_idom(X_a)-> (all Ya (ord_less(X_a,one_one(X_a),number_number_of(X_a,Ya))<->ord_less(int,bit1(pls),Ya)))). % 2.17/2.37 all Z_1 (ord_less(int,plus_plus(int,plus_plus(int,one_one(int),Z_1),Z_1),zero_zero(int))<->ord_less(int,Z_1,zero_zero(int))). % 2.17/2.37 all X_a (linord219039673up_add(X_a)-> (all A_2 (plus_plus(X_a,A_2,A_2)=zero_zero(X_a)<->ti(X_a,A_2)=zero_zero(X_a)))). % 2.17/2.37 all K (bit1(K)!=pls). % 2.17/2.37 all L (pls!=bit1(L)). % 2.17/2.37 all K L (bit1(K)!=bit0(L)). % 2.17/2.37 all K L (bit0(K)!=bit1(L)). % 2.17/2.37 all K_1 (bit0(K_1)=pls<->K_1=pls). % 2.17/2.37 all L_1 (pls=bit0(L_1)<->pls=L_1). % 2.17/2.37 bit0(pls)=pls. % 2.17/2.37 pls=zero_zero(int). % 2.17/2.37 zero_zero(int)!=one_one(int). % 2.17/2.37 all K (plus_plus(int,K,pls)=K). % 2.17/2.37 all K (plus_plus(int,pls,K)=K). % 2.17/2.37 all K L (plus_plus(int,bit0(K),bit0(L))=bit0(plus_plus(int,K,L))). % 2.17/2.37 all K (bit0(K)=plus_plus(int,K,K)). % 2.17/2.37 all Z (plus_plus(int,Z,zero_zero(int))=Z). % 2.17/2.37 all Z (plus_plus(int,zero_zero(int),Z)=Z). % 2.17/2.37 all X_a (number_semiring(X_a)->number_number_of(X_a,pls)=zero_zero(X_a)). % 2.17/2.37 all X_a (number_ring(X_a)->number_number_of(X_a,pls)=zero_zero(X_a)). % 2.17/2.37 all X_a (number_ring(X_a)->zero_zero(X_a)=number_number_of(X_a,pls)). % 2.17/2.37 all X_a (number_ring(X_a)-> (all A_1 (plus_plus(X_a,number_number_of(X_a,pls),A_1)=ti(X_a,A_1)))). % 2.17/2.37 all X_a (number_ring(X_a)-> (all A_1 (plus_plus(X_a,A_1,number_number_of(X_a,pls))=ti(X_a,A_1)))). % 2.17/2.37 all X_a (power(X_a)&mult_zero(X_a)&no_zero_divisors(X_a)&zero_ne_q_one(X_a)-> (all A_2 Wa (power_power(X_a,A_2,number_number_of(nat,Wa))=zero_zero(X_a)<->ti(X_a,A_2)=zero_zero(X_a)&number_number_of(nat,Wa)!=zero_zero(nat)))). % 2.17/2.37 all X_a (number_ring(X_a)-> (all V W Z (plus_plus(X_a,number_number_of(X_a,V),plus_plus(X_a,number_number_of(X_a,W),Z))=plus_plus(X_a,number_number_of(X_a,plus_plus(int,V,W)),Z)))). % 2.17/2.37 all X_a (number_ring(X_a)-> (all V W (plus_plus(X_a,number_number_of(X_a,V),number_number_of(X_a,W))=number_number_of(X_a,plus_plus(int,V,W))))). % 2.17/2.37 all X_a (number_ring(X_a)-> (all V W (number_number_of(X_a,plus_plus(int,V,W))=plus_plus(X_a,number_number_of(X_a,V),number_number_of(X_a,W))))). % 2.17/2.37 all K L (plus_plus(int,bit1(K),bit0(L))=bit1(plus_plus(int,K,L))). % 2.17/2.37 all K L (plus_plus(int,bit0(K),bit1(L))=bit1(plus_plus(int,K,L))). % 2.17/2.37 all K (bit1(K)=plus_plus(int,plus_plus(int,one_one(int),K),K)). % 2.17/2.37 all Z (plus_plus(int,plus_plus(int,one_one(int),Z),Z)!=zero_zero(int)). % 2.17/2.37 all X_a (number_semiring(X_a)-> (all N (number_number_of(X_a,semiring_1_of_nat(int,N))=semiring_1_of_nat(X_a,N)))). % 2.17/2.37 all X_a (linordered_idom(X_a)-> (all A_2 (ord_less(X_a,zero_zero(X_a),power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))))<->ti(X_a,A_2)!=zero_zero(X_a)))). % 2.17/2.37 all X_a (linordered_idom(X_a)-> (all A_1 (-ord_less(X_a,power_power(X_a,A_1,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X_a))))). % 2.17/2.37 all X_a (linordered_idom(X_a)-> (all Xa Ya (ord_less(X_a,zero_zero(X_a),plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))))<->ti(X_a,Xa)!=zero_zero(X_a)|ti(X_a,Ya)!=zero_zero(X_a)))). % 2.17/2.37 linord219039673up_add(int). % 2.17/2.37 ring_11004092258visors(int). % 2.17/2.37 no_zero_divisors(int). % 2.17/2.37 linordered_idom(int). % 2.17/2.37 number_semiring(int). % 2.17/2.37 zero_ne_q_one(int). % 2.17/2.37 semiring_1(int). % 2.17/2.37 semiring_0(int). % 2.17/2.37 mult_zero(int). % 2.17/2.37 ring_char_0(int). % 2.17/2.37 number_ring(int). % 2.17/2.37 power(int). % 2.17/2.37 number(int). % 2.17/2.37 no_zero_divisors(nat). % 2.17/2.37 number_semiring(nat). % 2.17/2.37 zero_ne_q_one(nat). % 2.17/2.37 semiring_1(nat). % 2.17/2.37 semiring_0(nat). % 2.17/2.37 mult_zero(nat). % 2.17/2.37 power(nat). % 2.17/2.37 number(nat). % 2.17/2.37 all T A (ti(T,ti(T,A))=ti(T,A)). % 2.17/2.37 -(power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls))))!=zero_zero(int)). % 2.17/2.37 end_of_list. % 2.17/2.37 % 2.17/2.37 -------> usable clausifies to: % 2.17/2.37 % 2.17/2.37 list(usable). % 2.17/2.37 0 [] A=A. % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|ti(X_a,one_one(X_a))=one_one(X_a). % 2.17/2.37 0 [] -linord219039673up_add(X_a)|plus_plus(X_a,ti(X_a,B_1),B_2)=plus_plus(X_a,B_1,B_2). % 2.17/2.37 0 [] -linord219039673up_add(X_a)|plus_plus(X_a,B_1,ti(X_a,B_2))=plus_plus(X_a,B_1,B_2). % 2.17/2.37 0 [] -linord219039673up_add(X_a)|ti(X_a,plus_plus(X_a,B_1,B_2))=plus_plus(X_a,B_1,B_2). % 2.17/2.37 0 [] -number_semiring(X_a)|plus_plus(X_a,ti(X_a,B_1),B_2)=plus_plus(X_a,B_1,B_2). % 2.17/2.37 0 [] -number_semiring(X_a)|plus_plus(X_a,B_1,ti(X_a,B_2))=plus_plus(X_a,B_1,B_2). % 2.17/2.37 0 [] -number_semiring(X_a)|ti(X_a,plus_plus(X_a,B_1,B_2))=plus_plus(X_a,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|ti(X_a,zero_zero(X_a))=zero_zero(X_a). % 2.17/2.37 0 [] -linord219039673up_add(X_a)|ti(X_a,zero_zero(X_a))=zero_zero(X_a). % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|ti(X_a,zero_zero(X_a))=zero_zero(X_a). % 2.17/2.37 0 [] ti(X_a,undefined(X_a))=undefined(X_a). % 2.17/2.37 0 [] bit0(ti(int,B_1))=bit0(B_1). % 2.17/2.37 0 [] ti(int,bit0(B_1))=bit0(B_1). % 2.17/2.37 0 [] bit1(ti(int,B_1))=bit1(B_1). % 2.17/2.37 0 [] ti(int,bit1(B_1))=bit1(B_1). % 2.17/2.37 0 [] ti(int,pls)=pls. % 2.17/2.37 0 [] -number(X_a)|number_number_of(X_a,ti(int,B_1))=number_number_of(X_a,B_1). % 2.17/2.37 0 [] -number(X_a)|ti(X_a,number_number_of(X_a,B_1))=number_number_of(X_a,B_1). % 2.17/2.37 0 [] -number_semiring(X_a)|semiring_1_of_nat(X_a,ti(nat,B_1))=semiring_1_of_nat(X_a,B_1). % 2.17/2.37 0 [] -number_semiring(X_a)|ti(X_a,semiring_1_of_nat(X_a,B_1))=semiring_1_of_nat(X_a,B_1). % 2.17/2.37 0 [] -linordered_idom(X_a)| -ord_less(X_a,ti(X_a,B_1),B_2)|ord_less(X_a,B_1,B_2). % 2.17/2.37 0 [] -linordered_idom(X_a)|ord_less(X_a,ti(X_a,B_1),B_2)| -ord_less(X_a,B_1,B_2). % 2.17/2.37 0 [] -linordered_idom(X_a)| -ord_less(X_a,B_1,ti(X_a,B_2))|ord_less(X_a,B_1,B_2). % 2.17/2.37 0 [] -linordered_idom(X_a)|ord_less(X_a,B_1,ti(X_a,B_2))| -ord_less(X_a,B_1,B_2). % 2.17/2.37 0 [] -ord_less(nat,ti(nat,B_1),B_2)|ord_less(nat,B_1,B_2). % 2.17/2.37 0 [] ord_less(nat,ti(nat,B_1),B_2)| -ord_less(nat,B_1,B_2). % 2.17/2.37 0 [] -ord_less(nat,B_1,ti(nat,B_2))|ord_less(nat,B_1,B_2). % 2.17/2.37 0 [] ord_less(nat,B_1,ti(nat,B_2))| -ord_less(nat,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|power_power(X_a,ti(X_a,B_1),B_2)=power_power(X_a,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|power_power(X_a,B_1,ti(nat,B_2))=power_power(X_a,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|ti(X_a,power_power(X_a,B_1,B_2))=power_power(X_a,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|power_power(X_a,ti(X_a,B_1),B_2)=power_power(X_a,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|power_power(X_a,B_1,ti(nat,B_2))=power_power(X_a,B_1,B_2). % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|ti(X_a,power_power(X_a,B_1,B_2))=power_power(X_a,B_1,B_2). % 2.17/2.37 0 [] ti(nat,n)=n. % 2.17/2.37 0 [] ti(int,t)=t. % 2.17/2.37 0 [] ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))). % 2.17/2.37 0 [] ord_less(int,one_one(int),t). % 2.17/2.37 0 [] -linordered_idom(X_a)|plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))!=zero_zero(X_a)|ti(X_a,Xa)=zero_zero(X_a). % 2.17/2.37 0 [] -linordered_idom(X_a)|plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))!=zero_zero(X_a)|ti(X_a,Ya)=zero_zero(X_a). % 2.17/2.37 0 [] -linordered_idom(X_a)|plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(X_a)|ti(X_a,Xa)!=zero_zero(X_a)|ti(X_a,Ya)!=zero_zero(X_a). % 2.17/2.37 0 [] -semiring_1(X_a)|power_power(X_a,one_one(X_a),number_number_of(nat,bit0(bit1(pls))))=one_one(X_a). % 2.17/2.37 0 [] -semiring_1(X_a)|power_power(X_a,zero_zero(X_a),number_number_of(nat,bit0(bit1(pls))))=zero_zero(X_a). % 2.17/2.37 0 [] -ring_11004092258visors(X_a)|power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls))))!=zero_zero(X_a)|ti(X_a,A_2)=zero_zero(X_a). % 2.17/2.37 0 [] -ring_11004092258visors(X_a)|power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls))))=zero_zero(X_a)|ti(X_a,A_2)!=zero_zero(X_a). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,one_one(X_a),number_number_of(X_a,W))=number_number_of(X_a,plus_plus(int,bit1(pls),W)). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,number_number_of(X_a,V),one_one(X_a))=number_number_of(X_a,plus_plus(int,V,bit1(pls))). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,one_one(X_a),one_one(X_a))=number_number_of(X_a,bit0(bit1(pls))). % 2.17/2.37 0 [] -number_semiring(X_a)|plus_plus(X_a,one_one(X_a),one_one(X_a))=number_number_of(X_a,bit0(bit1(pls))). % 2.17/2.37 0 [] power_power(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),number_number_of(nat,bit0(bit1(pls))))=power_power(int,X,number_number_of(nat,bit0(bit0(bit1(pls))))). % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|number_number_of(nat,W)!=zero_zero(nat)|power_power(X_a,zero_zero(X_a),number_number_of(nat,W))=one_one(X_a). % 2.17/2.37 0 [] -power(X_a)| -semiring_0(X_a)|number_number_of(nat,W)=zero_zero(nat)|power_power(X_a,zero_zero(X_a),number_number_of(nat,W))=zero_zero(X_a). % 2.17/2.37 0 [] -number_ring(X_a)|one_one(X_a)=number_number_of(X_a,bit1(pls)). % 2.17/2.37 0 [] -number_ring(X_a)|number_number_of(X_a,bit1(pls))=one_one(X_a). % 2.17/2.37 0 [] ord_less(nat,zero_zero(nat),n). % 2.17/2.37 0 [] ord_less(int,X,Y)|X=Y|ord_less(int,Y,X). % 2.17/2.37 0 [] -ord_less(int,number_number_of(int,K_1),number_number_of(int,L_1))|ord_less(int,K_1,L_1). % 2.17/2.37 0 [] ord_less(int,number_number_of(int,K_1),number_number_of(int,L_1))| -ord_less(int,K_1,L_1). % 2.17/2.37 0 [] plus_plus(int,number_number_of(int,V),number_number_of(int,W))=number_number_of(int,plus_plus(int,V,W)). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)| -ord_less(X_a,number_number_of(X_a,Xa),number_number_of(X_a,Ya))|ord_less(int,Xa,Ya). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)|ord_less(X_a,number_number_of(X_a,Xa),number_number_of(X_a,Ya))| -ord_less(int,Xa,Ya). % 2.17/2.37 0 [] zero_zero(int)=number_number_of(int,pls). % 2.17/2.37 0 [] power_power(int,semiring_1_of_nat(int,M),N)=semiring_1_of_nat(int,power_power(nat,M,N)). % 2.17/2.37 0 [] semiring_1_of_nat(int,power_power(nat,M,N))=power_power(int,semiring_1_of_nat(int,M),N). % 2.17/2.37 0 [] plus_plus(int,semiring_1_of_nat(int,M),plus_plus(int,semiring_1_of_nat(int,N),Z))=plus_plus(int,semiring_1_of_nat(int,plus_plus(nat,M,N)),Z). % 2.17/2.37 0 [] plus_plus(int,semiring_1_of_nat(int,M),semiring_1_of_nat(int,N))=semiring_1_of_nat(int,plus_plus(nat,M,N)). % 2.17/2.37 0 [] semiring_1_of_nat(int,one_one(nat))=one_one(int). % 2.17/2.37 0 [] number_number_of(nat,pls)=zero_zero(nat). % 2.17/2.37 0 [] zero_zero(nat)=number_number_of(nat,pls). % 2.17/2.37 0 [] semiring_1_of_nat(int,Na)!=zero_zero(int)|Na=zero_zero(nat). % 2.17/2.37 0 [] semiring_1_of_nat(int,Na)=zero_zero(int)|Na!=zero_zero(nat). % 2.17/2.37 0 [] semiring_1_of_nat(int,zero_zero(nat))=zero_zero(int). % 2.17/2.37 0 [] plus_plus(nat,one_one(nat),one_one(nat))=number_number_of(nat,bit0(bit1(pls))). % 2.17/2.37 0 [] -ord_less(int,bit1(K1),bit1(K2))|ord_less(int,K1,K2). % 2.17/2.37 0 [] ord_less(int,bit1(K1),bit1(K2))| -ord_less(int,K1,K2). % 2.17/2.37 0 [] -ord_less(int,bit1(K_1),bit1(L_1))|ord_less(int,K_1,L_1). % 2.17/2.37 0 [] ord_less(int,bit1(K_1),bit1(L_1))| -ord_less(int,K_1,L_1). % 2.17/2.37 0 [] -ord_less(int,pls,pls). % 2.17/2.37 0 [] -ord_less(int,bit0(K1),bit0(K2))|ord_less(int,K1,K2). % 2.17/2.37 0 [] ord_less(int,bit0(K1),bit0(K2))| -ord_less(int,K1,K2). % 2.17/2.37 0 [] -ord_less(int,bit0(K_1),bit0(L_1))|ord_less(int,K_1,L_1). % 2.17/2.37 0 [] ord_less(int,bit0(K_1),bit0(L_1))| -ord_less(int,K_1,L_1). % 2.17/2.37 0 [] -ord_less(int,I,J)|ord_less(int,plus_plus(int,I,K),plus_plus(int,J,K)). % 2.17/2.37 0 [] -ord_less(int,V,pls)|plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1))=number_number_of(nat,V_1). % 2.17/2.37 0 [] ord_less(int,V,pls)| -ord_less(int,V_1,pls)|plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1))=number_number_of(nat,V). % 2.17/2.37 0 [] ord_less(int,V,pls)|ord_less(int,V_1,pls)|plus_plus(nat,number_number_of(nat,V),number_number_of(nat,V_1))=number_number_of(nat,plus_plus(int,V,V_1)). % 2.17/2.37 0 [] one_one(int)=number_number_of(int,bit1(pls)). % 2.17/2.37 0 [] number_number_of(nat,bit1(pls))=one_one(nat). % 2.17/2.37 0 [] one_one(nat)=number_number_of(nat,bit1(pls)). % 2.17/2.37 0 [] -number_ring(X_a)| -ring_char_0(X_a)|number_number_of(X_a,Xa)!=number_number_of(X_a,Ya)|Xa=Ya. % 2.17/2.37 0 [] -number_ring(X_a)| -ring_char_0(X_a)|number_number_of(X_a,Xa)=number_number_of(X_a,Ya)|Xa!=Ya. % 2.17/2.37 0 [] -number(X_a)|number_number_of(X_a,Wa)!=ti(X_a,Xa)|ti(X_a,Xa)=number_number_of(X_a,Wa). % 2.17/2.37 0 [] -number(X_a)|number_number_of(X_a,Wa)=ti(X_a,Xa)|ti(X_a,Xa)!=number_number_of(X_a,Wa). % 2.17/2.37 0 [] bit1(K_1)!=bit1(L_1)|K_1=L_1. % 2.17/2.37 0 [] bit1(K_1)=bit1(L_1)|K_1!=L_1. % 2.17/2.37 0 [] bit0(K_1)!=bit0(L_1)|K_1=L_1. % 2.17/2.37 0 [] bit0(K_1)=bit0(L_1)|K_1!=L_1. % 2.17/2.37 0 [] -linordered_idom(X_a)| -ord_less(X_a,plus_plus(X_a,A_2,A_2),zero_zero(X_a))|ord_less(X_a,A_2,zero_zero(X_a)). % 2.17/2.37 0 [] -linordered_idom(X_a)|ord_less(X_a,plus_plus(X_a,A_2,A_2),zero_zero(X_a))| -ord_less(X_a,A_2,zero_zero(X_a)). % 2.17/2.37 0 [] plus_plus(int,plus_plus(int,Z1,Z2),Z3)=plus_plus(int,Z1,plus_plus(int,Z2,Z3)). % 2.17/2.37 0 [] plus_plus(int,X,plus_plus(int,Y,Z))=plus_plus(int,Y,plus_plus(int,X,Z)). % 2.17/2.37 0 [] plus_plus(int,Z,W)=plus_plus(int,W,Z). % 2.17/2.37 0 [] semiring_1_of_nat(int,Ma)!=semiring_1_of_nat(int,Na)|Ma=Na. % 2.17/2.37 0 [] semiring_1_of_nat(int,Ma)=semiring_1_of_nat(int,Na)|Ma!=Na. % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)| -ord_less(X_a,number_number_of(X_a,Xa),zero_zero(X_a))|ord_less(int,Xa,pls). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)|ord_less(X_a,number_number_of(X_a,Xa),zero_zero(X_a))| -ord_less(int,Xa,pls). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)| -ord_less(X_a,zero_zero(X_a),number_number_of(X_a,Ya))|ord_less(int,pls,Ya). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)|ord_less(X_a,zero_zero(X_a),number_number_of(X_a,Ya))| -ord_less(int,pls,Ya). % 2.17/2.37 0 [] -ord_less(int,bit1(K_1),pls)|ord_less(int,K_1,pls). % 2.17/2.37 0 [] ord_less(int,bit1(K_1),pls)| -ord_less(int,K_1,pls). % 2.17/2.37 0 [] -ord_less(int,bit1(K1),bit0(K2))|ord_less(int,K1,K2). % 2.17/2.37 0 [] ord_less(int,bit1(K1),bit0(K2))| -ord_less(int,K1,K2). % 2.17/2.37 0 [] -ord_less(int,bit1(K_1),bit0(L_1))|ord_less(int,K_1,L_1). % 2.17/2.37 0 [] ord_less(int,bit1(K_1),bit0(L_1))| -ord_less(int,K_1,L_1). % 2.17/2.37 0 [] -ord_less(int,bit0(K_1),pls)|ord_less(int,K_1,pls). % 2.17/2.37 0 [] ord_less(int,bit0(K_1),pls)| -ord_less(int,K_1,pls). % 2.17/2.37 0 [] -ord_less(int,pls,bit0(K_1))|ord_less(int,pls,K_1). % 2.17/2.37 0 [] ord_less(int,pls,bit0(K_1))| -ord_less(int,pls,K_1). % 2.17/2.37 0 [] -ord_less(int,bit1(Wa),zero_zero(int))|ord_less(int,Wa,zero_zero(int)). % 2.17/2.37 0 [] ord_less(int,bit1(Wa),zero_zero(int))| -ord_less(int,Wa,zero_zero(int)). % 2.17/2.37 0 [] -ord_less(int,pls,zero_zero(int)). % 2.17/2.37 0 [] -ord_less(int,bit0(Wa),zero_zero(int))|ord_less(int,Wa,zero_zero(int)). % 2.17/2.37 0 [] ord_less(int,bit0(Wa),zero_zero(int))| -ord_less(int,Wa,zero_zero(int)). % 2.17/2.37 0 [] ord_less(int,zero_zero(int),one_one(int)). % 2.17/2.37 0 [] -ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))|ord_less(int,Wa,Z_1)|Wa=Z_1. % 2.17/2.37 0 [] ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))| -ord_less(int,Wa,Z_1). % 2.17/2.37 0 [] ord_less(int,Wa,plus_plus(int,Z_1,one_one(int)))|Wa!=Z_1. % 2.17/2.37 0 [] -ord_less(int,semiring_1_of_nat(int,K),zero_zero(int)). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)| -ord_less(X_a,number_number_of(X_a,Xa),one_one(X_a))|ord_less(int,Xa,bit1(pls)). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)|ord_less(X_a,number_number_of(X_a,Xa),one_one(X_a))| -ord_less(int,Xa,bit1(pls)). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)| -ord_less(X_a,one_one(X_a),number_number_of(X_a,Ya))|ord_less(int,bit1(pls),Ya). % 2.17/2.37 0 [] -number_ring(X_a)| -linordered_idom(X_a)|ord_less(X_a,one_one(X_a),number_number_of(X_a,Ya))| -ord_less(int,bit1(pls),Ya). % 2.17/2.37 0 [] -ord_less(int,plus_plus(int,plus_plus(int,one_one(int),Z_1),Z_1),zero_zero(int))|ord_less(int,Z_1,zero_zero(int)). % 2.17/2.37 0 [] ord_less(int,plus_plus(int,plus_plus(int,one_one(int),Z_1),Z_1),zero_zero(int))| -ord_less(int,Z_1,zero_zero(int)). % 2.17/2.37 0 [] -linord219039673up_add(X_a)|plus_plus(X_a,A_2,A_2)!=zero_zero(X_a)|ti(X_a,A_2)=zero_zero(X_a). % 2.17/2.37 0 [] -linord219039673up_add(X_a)|plus_plus(X_a,A_2,A_2)=zero_zero(X_a)|ti(X_a,A_2)!=zero_zero(X_a). % 2.17/2.37 0 [] bit1(K)!=pls. % 2.17/2.37 0 [] pls!=bit1(L). % 2.17/2.37 0 [] bit1(K)!=bit0(L). % 2.17/2.37 0 [] bit0(K)!=bit1(L). % 2.17/2.37 0 [] bit0(K_1)!=pls|K_1=pls. % 2.17/2.37 0 [] bit0(K_1)=pls|K_1!=pls. % 2.17/2.37 0 [] pls!=bit0(L_1)|pls=L_1. % 2.17/2.37 0 [] pls=bit0(L_1)|pls!=L_1. % 2.17/2.37 0 [] bit0(pls)=pls. % 2.17/2.37 0 [] pls=zero_zero(int). % 2.17/2.37 0 [] zero_zero(int)!=one_one(int). % 2.17/2.37 0 [] plus_plus(int,K,pls)=K. % 2.17/2.37 0 [] plus_plus(int,pls,K)=K. % 2.17/2.37 0 [] plus_plus(int,bit0(K),bit0(L))=bit0(plus_plus(int,K,L)). % 2.17/2.37 0 [] bit0(K)=plus_plus(int,K,K). % 2.17/2.37 0 [] plus_plus(int,Z,zero_zero(int))=Z. % 2.17/2.37 0 [] plus_plus(int,zero_zero(int),Z)=Z. % 2.17/2.37 0 [] -number_semiring(X_a)|number_number_of(X_a,pls)=zero_zero(X_a). % 2.17/2.37 0 [] -number_ring(X_a)|number_number_of(X_a,pls)=zero_zero(X_a). % 2.17/2.37 0 [] -number_ring(X_a)|zero_zero(X_a)=number_number_of(X_a,pls). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,number_number_of(X_a,pls),A_1)=ti(X_a,A_1). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,A_1,number_number_of(X_a,pls))=ti(X_a,A_1). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|power_power(X_a,A_2,number_number_of(nat,Wa))!=zero_zero(X_a)|ti(X_a,A_2)=zero_zero(X_a). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|power_power(X_a,A_2,number_number_of(nat,Wa))!=zero_zero(X_a)|number_number_of(nat,Wa)!=zero_zero(nat). % 2.17/2.37 0 [] -power(X_a)| -mult_zero(X_a)| -no_zero_divisors(X_a)| -zero_ne_q_one(X_a)|power_power(X_a,A_2,number_number_of(nat,Wa))=zero_zero(X_a)|ti(X_a,A_2)!=zero_zero(X_a)|number_number_of(nat,Wa)=zero_zero(nat). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,number_number_of(X_a,V),plus_plus(X_a,number_number_of(X_a,W),Z))=plus_plus(X_a,number_number_of(X_a,plus_plus(int,V,W)),Z). % 2.17/2.37 0 [] -number_ring(X_a)|plus_plus(X_a,number_number_of(X_a,V),number_number_of(X_a,W))=number_number_of(X_a,plus_plus(int,V,W)). % 2.17/2.37 0 [] -number_ring(X_a)|number_number_of(X_a,plus_plus(int,V,W))=plus_plus(X_a,number_number_of(X_a,V),number_number_of(X_a,W)). % 2.17/2.37 0 [] plus_plus(int,bit1(K),bit0(L))=bit1(plus_plus(int,K,L)). % 2.17/2.37 0 [] plus_plus(int,bit0(K),bit1(L))=bit1(plus_plus(int,K,L)). % 2.17/2.37 0 [] bit1(K)=plus_plus(int,plus_plus(int,one_one(int),K),K). % 2.17/2.37 0 [] plus_plus(int,plus_plus(int,one_one(int),Z),Z)!=zero_zero(int). % 2.17/2.37 0 [] -number_semiring(X_a)|number_number_of(X_a,semiring_1_of_nat(int,N))=semiring_1_of_nat(X_a,N). % 2.17/2.37 0 [] -linordered_idom(X_a)| -ord_less(X_a,zero_zero(X_a),power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))))|ti(X_a,A_2)!=zero_zero(X_a). % 2.17/2.37 0 [] -linordered_idom(X_a)|ord_less(X_a,zero_zero(X_a),power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))))|ti(X_a,A_2)=zero_zero(X_a). % 2.17/2.37 0 [] -linordered_idom(X_a)| -ord_less(X_a,power_power(X_a,A_1,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X_a)). % 2.17/2.37 0 [] -linordered_idom(X_a)| -ord_less(X_a,zero_zero(X_a),plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))))|ti(X_a,Xa)!=zero_zero(X_a)|ti(X_a,Ya)!=zero_zero(X_a). % 2.17/2.37 0 [] -linordered_idom(X_a)|ord_less(X_a,zero_zero(X_a),plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))))|ti(X_a,Xa)=zero_zero(X_a). % 2.17/2.37 0 [] -linordered_idom(X_a)|ord_less(X_a,zero_zero(X_a),plus_plus(X_a,power_power(X_a,Xa,number_number_of(nat,bit0(bit1(pls)))),power_power(X_a,Ya,number_number_of(nat,bit0(bit1(pls))))))|ti(X_a,Ya)=zero_zero(X_a). % 2.17/2.37 0 [] linord219039673up_add(int). % 2.17/2.37 0 [] ring_11004092258visors(int). % 2.17/2.37 0 [] no_zero_divisors(int). % 2.17/2.37 0 [] linordered_idom(int). % 2.17/2.37 0 [] number_semiring(int). % 2.17/2.37 0 [] zero_ne_q_one(int). % 2.17/2.37 0 [] semiring_1(int). % 2.17/2.37 0 [] semiring_0(int). % 2.17/2.37 0 [] mult_zero(int). % 2.17/2.37 0 [] ring_char_0(int). % 2.17/2.37 0 [] number_ring(int). % 2.17/2.37 0 [] power(int). % 2.17/2.37 0 [] number(int). % 2.17/2.37 0 [] no_zero_divisors(nat). % 2.17/2.37 0 [] number_semiring(nat). % 2.17/2.37 0 [] zero_ne_q_one(nat). % 2.17/2.37 0 [] semiring_1(nat). % 2.17/2.37 0 [] semiring_0(nat). % 2.17/2.37 0 [] mult_zero(nat). % 2.17/2.37 0 [] power(nat). % 2.17/2.37 0 [] number(nat). % 2.17/2.37 0 [] ti(T,ti(T,A))=ti(T,A). % 2.17/2.37 0 [] power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls))))=zero_zero(int). % 2.17/2.37 end_of_list. % 2.17/2.37 % 2.17/2.37 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=7. % 2.17/2.37 % 2.17/2.37 This ia a non-Horn set with equality. The strategy will be % 2.17/2.37 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.17/2.37 deletion, with positive clauses in sos and nonpositive % 2.17/2.37 clauses in usable. % 2.17/2.37 % 2.17/2.37 dependent: set(knuth_bendix). % 2.17/2.37 dependent: set(anl_eq). % 2.17/2.37 dependent: set(para_from). % 2.17/2.37 dependent: set(para_into). % 2.17/2.37 dependent: clear(para_from_right). % 2.17/2.37 dependent: clear(para_into_right). % 2.17/2.37 dependent: set(para_from_vars). % 2.17/2.37 dependent: set(eq_units_both_ways). % 2.17/2.37 dependent: set(dynamic_demod_all). % 2.17/2.37 dependent: set(dynamic_demod). % 2.17/2.37 dependent: set(order_eq). % 2.17/2.37 dependent: set(back_demod). % 2.17/2.37 dependent: set(lrpo). % 2.17/2.37 dependent: set(hyper_res). % 2.17/2.37 dependent: set(unit_deletion). % 2.17/2.37 dependent: set(factor). % 2.17/2.37 % 2.17/2.37 ------------> process usable: % 2.17/2.37 ** KEPT (pick-wt=11): 1 [] -power(A)| -semiring_0(A)|ti(A,one_one(A))=one_one(A). % 2.17/2.37 ** KEPT (pick-wt=13): 2 [] -linord219039673up_add(A)|plus_plus(A,ti(A,B),C)=plus_plus(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=13): 3 [] -linord219039673up_add(A)|plus_plus(A,B,ti(A,C))=plus_plus(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=13): 4 [] -linord219039673up_add(A)|ti(A,plus_plus(A,B,C))=plus_plus(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=13): 5 [] -number_semiring(A)|plus_plus(A,ti(A,B),C)=plus_plus(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=13): 6 [] -number_semiring(A)|plus_plus(A,B,ti(A,C))=plus_plus(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=13): 7 [] -number_semiring(A)|ti(A,plus_plus(A,B,C))=plus_plus(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=15): 8 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|ti(A,zero_zero(A))=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=9): 9 [] -linord219039673up_add(A)|ti(A,zero_zero(A))=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=11): 10 [] -power(A)| -semiring_0(A)|ti(A,zero_zero(A))=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=11): 11 [] -number(A)|number_number_of(A,ti(int,B))=number_number_of(A,B). % 2.17/2.37 ** KEPT (pick-wt=11): 12 [] -number(A)|ti(A,number_number_of(A,B))=number_number_of(A,B). % 2.17/2.37 ** KEPT (pick-wt=11): 13 [] -number_semiring(A)|semiring_1_of_nat(A,ti(nat,B))=semiring_1_of_nat(A,B). % 2.17/2.37 ** KEPT (pick-wt=11): 14 [] -number_semiring(A)|ti(A,semiring_1_of_nat(A,B))=semiring_1_of_nat(A,B). % 2.17/2.37 ** KEPT (pick-wt=12): 15 [] -linordered_idom(A)| -ord_less(A,ti(A,B),C)|ord_less(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=12): 16 [] -linordered_idom(A)|ord_less(A,ti(A,B),C)| -ord_less(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=12): 17 [] -linordered_idom(A)| -ord_less(A,B,ti(A,C))|ord_less(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=12): 18 [] -linordered_idom(A)|ord_less(A,B,ti(A,C))| -ord_less(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=10): 19 [] -ord_less(nat,ti(nat,A),B)|ord_less(nat,A,B). % 2.17/2.37 ** KEPT (pick-wt=10): 20 [] ord_less(nat,ti(nat,A),B)| -ord_less(nat,A,B). % 2.17/2.37 ** KEPT (pick-wt=10): 21 [] -ord_less(nat,A,ti(nat,B))|ord_less(nat,A,B). % 2.17/2.37 ** KEPT (pick-wt=10): 22 [] ord_less(nat,A,ti(nat,B))| -ord_less(nat,A,B). % 2.17/2.37 ** KEPT (pick-wt=19): 23 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|power_power(A,ti(A,B),C)=power_power(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=19): 24 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|power_power(A,B,ti(nat,C))=power_power(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=19): 25 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|ti(A,power_power(A,B,C))=power_power(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=15): 26 [] -power(A)| -semiring_0(A)|power_power(A,ti(A,B),C)=power_power(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=15): 27 [] -power(A)| -semiring_0(A)|power_power(A,B,ti(nat,C))=power_power(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=15): 28 [] -power(A)| -semiring_0(A)|ti(A,power_power(A,B,C))=power_power(A,B,C). % 2.17/2.37 ** KEPT (pick-wt=29): 29 [] -linordered_idom(A)|plus_plus(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),power_power(A,C,number_number_of(nat,bit0(bit1(pls)))))!=zero_zero(A)|ti(A,B)=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=29): 30 [] -linordered_idom(A)|plus_plus(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),power_power(A,C,number_number_of(nat,bit0(bit1(pls)))))!=zero_zero(A)|ti(A,C)=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=35): 31 [] -linordered_idom(A)|plus_plus(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),power_power(A,C,number_number_of(nat,bit0(bit1(pls)))))=zero_zero(A)|ti(A,B)!=zero_zero(A)|ti(A,C)!=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=14): 32 [] -semiring_1(A)|power_power(A,one_one(A),number_number_of(nat,bit0(bit1(pls))))=one_one(A). % 2.17/2.37 ** KEPT (pick-wt=14): 33 [] -semiring_1(A)|power_power(A,zero_zero(A),number_number_of(nat,bit0(bit1(pls))))=zero_zero(A). % 2.17/2.37 ** KEPT (pick-wt=19): 34 [] -ring_11004092258visors(A)|power_power(A,B,number_number_of(nat,bit0(bit1(pls))))!=zero_zero(A)|ti(A,B)=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=19): 35 [] -ring_11004092258visors(A)|power_power(A,B,number_number_of(nat,bit0(bit1(pls))))=zero_zero(A)|ti(A,B)!=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=17): 36 [] -number_ring(A)|plus_plus(A,one_one(A),number_number_of(A,B))=number_number_of(A,plus_plus(int,bit1(pls),B)). % 2.17/2.38 ** KEPT (pick-wt=17): 37 [] -number_ring(A)|plus_plus(A,number_number_of(A,B),one_one(A))=number_number_of(A,plus_plus(int,B,bit1(pls))). % 2.17/2.38 ** KEPT (pick-wt=14): 38 [] -number_ring(A)|plus_plus(A,one_one(A),one_one(A))=number_number_of(A,bit0(bit1(pls))). % 2.17/2.38 ** KEPT (pick-wt=14): 39 [] -number_semiring(A)|plus_plus(A,one_one(A),one_one(A))=number_number_of(A,bit0(bit1(pls))). % 2.17/2.38 ** KEPT (pick-wt=20): 40 [] -power(A)| -semiring_0(A)|number_number_of(nat,B)!=zero_zero(nat)|power_power(A,zero_zero(A),number_number_of(nat,B))=one_one(A). % 2.17/2.38 ** KEPT (pick-wt=20): 41 [] -power(A)| -semiring_0(A)|number_number_of(nat,B)=zero_zero(nat)|power_power(A,zero_zero(A),number_number_of(nat,B))=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=9): 42 [] -number_ring(A)|one_one(A)=number_number_of(A,bit1(pls)). % 2.17/2.38 Following clause subsumed by 42 during input processing: 0 [flip.2] -number_ring(A)|one_one(A)=number_number_of(A,bit1(pls)). % 2.17/2.38 ** KEPT (pick-wt=12): 43 [] -ord_less(int,number_number_of(int,A),number_number_of(int,B))|ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=12): 44 [] ord_less(int,number_number_of(int,A),number_number_of(int,B))| -ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=16): 45 [] -number_ring(A)| -linordered_idom(A)| -ord_less(A,number_number_of(A,B),number_number_of(A,C))|ord_less(int,B,C). % 2.17/2.38 ** KEPT (pick-wt=16): 46 [] -number_ring(A)| -linordered_idom(A)|ord_less(A,number_number_of(A,B),number_number_of(A,C))| -ord_less(int,B,C). % 2.17/2.38 ** KEPT (pick-wt=10): 47 [] semiring_1_of_nat(int,A)!=zero_zero(int)|A=zero_zero(nat). % 2.17/2.38 ** KEPT (pick-wt=10): 48 [] semiring_1_of_nat(int,A)=zero_zero(int)|A!=zero_zero(nat). % 2.17/2.38 ** KEPT (pick-wt=10): 49 [] -ord_less(int,bit1(A),bit1(B))|ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=10): 50 [] ord_less(int,bit1(A),bit1(B))| -ord_less(int,A,B). % 2.17/2.38 Following clause subsumed by 49 during input processing: 0 [] -ord_less(int,bit1(A),bit1(B))|ord_less(int,A,B). % 2.17/2.38 Following clause subsumed by 50 during input processing: 0 [] ord_less(int,bit1(A),bit1(B))| -ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=4): 51 [] -ord_less(int,pls,pls). % 2.17/2.38 ** KEPT (pick-wt=10): 52 [] -ord_less(int,bit0(A),bit0(B))|ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=10): 53 [] ord_less(int,bit0(A),bit0(B))| -ord_less(int,A,B). % 2.17/2.38 Following clause subsumed by 52 during input processing: 0 [] -ord_less(int,bit0(A),bit0(B))|ord_less(int,A,B). % 2.17/2.38 Following clause subsumed by 53 during input processing: 0 [] ord_less(int,bit0(A),bit0(B))| -ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=14): 54 [] -ord_less(int,A,B)|ord_less(int,plus_plus(int,A,C),plus_plus(int,B,C)). % 2.17/2.38 ** KEPT (pick-wt=16): 55 [] -ord_less(int,A,pls)|plus_plus(nat,number_number_of(nat,A),number_number_of(nat,B))=number_number_of(nat,B). % 2.17/2.38 ** KEPT (pick-wt=20): 56 [] 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.17/2.38 ** KEPT (pick-wt=14): 57 [] -number_ring(A)| -ring_char_0(A)|number_number_of(A,B)!=number_number_of(A,C)|B=C. % 2.17/2.38 ** KEPT (pick-wt=14): 58 [] -number_ring(A)| -ring_char_0(A)|number_number_of(A,B)=number_number_of(A,C)|B!=C. % 2.17/2.38 ** KEPT (pick-wt=16): 59 [] -number(A)|number_number_of(A,B)!=ti(A,C)|ti(A,C)=number_number_of(A,B). % 2.17/2.38 ** KEPT (pick-wt=16): 60 [] -number(A)|number_number_of(A,B)=ti(A,C)|ti(A,C)!=number_number_of(A,B). % 2.17/2.38 ** KEPT (pick-wt=8): 61 [] bit1(A)!=bit1(B)|A=B. % 2.17/2.38 ** KEPT (pick-wt=8): 62 [] bit1(A)=bit1(B)|A!=B. % 2.17/2.38 ** KEPT (pick-wt=8): 63 [] bit0(A)!=bit0(B)|A=B. % 2.17/2.38 ** KEPT (pick-wt=8): 64 [] bit0(A)=bit0(B)|A!=B. % 2.17/2.38 ** KEPT (pick-wt=15): 65 [] -linordered_idom(A)| -ord_less(A,plus_plus(A,B,B),zero_zero(A))|ord_less(A,B,zero_zero(A)). % 2.17/2.38 ** KEPT (pick-wt=15): 66 [] -linordered_idom(A)|ord_less(A,plus_plus(A,B,B),zero_zero(A))| -ord_less(A,B,zero_zero(A)). % 2.17/2.38 ** KEPT (pick-wt=10): 67 [] semiring_1_of_nat(int,A)!=semiring_1_of_nat(int,B)|A=B. % 2.17/2.38 ** KEPT (pick-wt=10): 68 [] semiring_1_of_nat(int,A)=semiring_1_of_nat(int,B)|A!=B. % 2.17/2.38 ** KEPT (pick-wt=15): 69 [] -number_ring(A)| -linordered_idom(A)| -ord_less(A,number_number_of(A,B),zero_zero(A))|ord_less(int,B,pls). % 2.17/2.38 ** KEPT (pick-wt=15): 70 [] -number_ring(A)| -linordered_idom(A)|ord_less(A,number_number_of(A,B),zero_zero(A))| -ord_less(int,B,pls). % 2.17/2.38 ** KEPT (pick-wt=15): 71 [] -number_ring(A)| -linordered_idom(A)| -ord_less(A,zero_zero(A),number_number_of(A,B))|ord_less(int,pls,B). % 2.17/2.38 ** KEPT (pick-wt=15): 72 [] -number_ring(A)| -linordered_idom(A)|ord_less(A,zero_zero(A),number_number_of(A,B))| -ord_less(int,pls,B). % 2.17/2.38 ** KEPT (pick-wt=9): 73 [] -ord_less(int,bit1(A),pls)|ord_less(int,A,pls). % 2.17/2.38 ** KEPT (pick-wt=9): 74 [] ord_less(int,bit1(A),pls)| -ord_less(int,A,pls). % 2.17/2.38 ** KEPT (pick-wt=10): 75 [] -ord_less(int,bit1(A),bit0(B))|ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=10): 76 [] ord_less(int,bit1(A),bit0(B))| -ord_less(int,A,B). % 2.17/2.38 Following clause subsumed by 75 during input processing: 0 [] -ord_less(int,bit1(A),bit0(B))|ord_less(int,A,B). % 2.17/2.38 Following clause subsumed by 76 during input processing: 0 [] ord_less(int,bit1(A),bit0(B))| -ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=9): 77 [] -ord_less(int,bit0(A),pls)|ord_less(int,A,pls). % 2.17/2.38 ** KEPT (pick-wt=9): 78 [] ord_less(int,bit0(A),pls)| -ord_less(int,A,pls). % 2.17/2.38 ** KEPT (pick-wt=9): 79 [] -ord_less(int,pls,bit0(A))|ord_less(int,pls,A). % 2.17/2.38 ** KEPT (pick-wt=9): 80 [] ord_less(int,pls,bit0(A))| -ord_less(int,pls,A). % 2.17/2.38 ** KEPT (pick-wt=11): 81 [] -ord_less(int,bit1(A),zero_zero(int))|ord_less(int,A,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=11): 82 [] ord_less(int,bit1(A),zero_zero(int))| -ord_less(int,A,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=5): 83 [] -ord_less(int,pls,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=11): 84 [] -ord_less(int,bit0(A),zero_zero(int))|ord_less(int,A,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=11): 85 [] ord_less(int,bit0(A),zero_zero(int))| -ord_less(int,A,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=15): 86 [] -ord_less(int,A,plus_plus(int,B,one_one(int)))|ord_less(int,A,B)|A=B. % 2.17/2.38 ** KEPT (pick-wt=12): 87 [] ord_less(int,A,plus_plus(int,B,one_one(int)))| -ord_less(int,A,B). % 2.17/2.38 ** KEPT (pick-wt=11): 88 [] ord_less(int,A,plus_plus(int,B,one_one(int)))|A!=B. % 2.17/2.38 ** KEPT (pick-wt=7): 89 [] -ord_less(int,semiring_1_of_nat(int,A),zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=16): 90 [] -number_ring(A)| -linordered_idom(A)| -ord_less(A,number_number_of(A,B),one_one(A))|ord_less(int,B,bit1(pls)). % 2.17/2.38 ** KEPT (pick-wt=16): 91 [] -number_ring(A)| -linordered_idom(A)|ord_less(A,number_number_of(A,B),one_one(A))| -ord_less(int,B,bit1(pls)). % 2.17/2.38 ** KEPT (pick-wt=16): 92 [] -number_ring(A)| -linordered_idom(A)| -ord_less(A,one_one(A),number_number_of(A,B))|ord_less(int,bit1(pls),B). % 2.17/2.38 ** KEPT (pick-wt=16): 93 [] -number_ring(A)| -linordered_idom(A)|ord_less(A,one_one(A),number_number_of(A,B))| -ord_less(int,bit1(pls),B). % 2.17/2.38 ** KEPT (pick-wt=17): 94 [] -ord_less(int,plus_plus(int,plus_plus(int,one_one(int),A),A),zero_zero(int))|ord_less(int,A,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=17): 95 [] ord_less(int,plus_plus(int,plus_plus(int,one_one(int),A),A),zero_zero(int))| -ord_less(int,A,zero_zero(int)). % 2.17/2.38 ** KEPT (pick-wt=15): 96 [] -linord219039673up_add(A)|plus_plus(A,B,B)!=zero_zero(A)|ti(A,B)=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=15): 97 [] -linord219039673up_add(A)|plus_plus(A,B,B)=zero_zero(A)|ti(A,B)!=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=4): 98 [] bit1(A)!=pls. % 2.17/2.38 Following clause subsumed by 98 during input processing: 0 [flip.1] bit1(A)!=pls. % 2.17/2.38 ** KEPT (pick-wt=5): 99 [] bit1(A)!=bit0(B). % 2.17/2.38 ** KEPT (pick-wt=5): 100 [] bit0(A)!=bit1(B). % 2.17/2.38 ** KEPT (pick-wt=7): 101 [] bit0(A)!=pls|A=pls. % 2.17/2.38 ** KEPT (pick-wt=7): 102 [] bit0(A)=pls|A!=pls. % 2.17/2.38 ** KEPT (pick-wt=7): 104 [copy,103,flip.1] bit0(A)!=pls|pls=A. % 2.17/2.38 ** KEPT (pick-wt=7): 106 [copy,105,flip.1] bit0(A)=pls|pls!=A. % 2.17/2.38 ** KEPT (pick-wt=5): 107 [] zero_zero(int)!=one_one(int). % 2.17/2.38 ** KEPT (pick-wt=8): 109 [copy,108,flip.2] -number_semiring(A)|zero_zero(A)=number_number_of(A,pls). % 2.17/2.38 ** KEPT (pick-wt=8): 111 [copy,110,flip.2] -number_ring(A)|zero_zero(A)=number_number_of(A,pls). % 2.17/2.38 Following clause subsumed by 111 during input processing: 0 [] -number_ring(A)|zero_zero(A)=number_number_of(A,pls). % 2.17/2.38 ** KEPT (pick-wt=12): 113 [copy,112,flip.2] -number_ring(A)|ti(A,B)=plus_plus(A,number_number_of(A,pls),B). % 2.17/2.38 ** KEPT (pick-wt=12): 115 [copy,114,flip.2] -number_ring(A)|ti(A,B)=plus_plus(A,B,number_number_of(A,pls)). % 2.17/2.38 ** KEPT (pick-wt=23): 116 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|power_power(A,B,number_number_of(nat,C))!=zero_zero(A)|ti(A,B)=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=23): 117 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|power_power(A,B,number_number_of(nat,C))!=zero_zero(A)|number_number_of(nat,C)!=zero_zero(nat). % 2.17/2.38 ** KEPT (pick-wt=29): 118 [] -power(A)| -mult_zero(A)| -no_zero_divisors(A)| -zero_ne_q_one(A)|power_power(A,B,number_number_of(nat,C))=zero_zero(A)|ti(A,B)!=zero_zero(A)|number_number_of(nat,C)=zero_zero(nat). % 2.17/2.38 ** KEPT (pick-wt=23): 120 [copy,119,flip.2] -number_ring(A)|plus_plus(A,number_number_of(A,plus_plus(int,B,C)),D)=plus_plus(A,number_number_of(A,B),plus_plus(A,number_number_of(A,C),D)). % 2.17/2.38 ** KEPT (pick-wt=17): 122 [copy,121,flip.2] -number_ring(A)|number_number_of(A,plus_plus(int,B,C))=plus_plus(A,number_number_of(A,B),number_number_of(A,C)). % 2.17/2.38 Following clause subsumed by 122 during input processing: 0 [] -number_ring(A)|number_number_of(A,plus_plus(int,B,C))=plus_plus(A,number_number_of(A,B),number_number_of(A,C)). % 2.17/2.38 ** KEPT (pick-wt=11): 123 [] plus_plus(int,plus_plus(int,one_one(int),A),A)!=zero_zero(int). % 2.17/2.38 ** KEPT (pick-wt=11): 124 [] -number_semiring(A)|number_number_of(A,semiring_1_of_nat(int,B))=semiring_1_of_nat(A,B). % 2.17/2.38 ** KEPT (pick-wt=20): 125 [] -linordered_idom(A)| -ord_less(A,zero_zero(A),power_power(A,B,number_number_of(nat,bit0(bit1(pls)))))|ti(A,B)!=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=20): 126 [] -linordered_idom(A)|ord_less(A,zero_zero(A),power_power(A,B,number_number_of(nat,bit0(bit1(pls)))))|ti(A,B)=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=14): 127 [] -linordered_idom(A)| -ord_less(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),zero_zero(A)). % 2.17/2.38 ** KEPT (pick-wt=36): 128 [] -linordered_idom(A)| -ord_less(A,zero_zero(A),plus_plus(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),power_power(A,C,number_number_of(nat,bit0(bit1(pls))))))|ti(A,B)!=zero_zero(A)|ti(A,C)!=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=30): 129 [] -linordered_idom(A)|ord_less(A,zero_zero(A),plus_plus(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),power_power(A,C,number_number_of(nat,bit0(bit1(pls))))))|ti(A,B)=zero_zero(A). % 2.17/2.38 ** KEPT (pick-wt=30): 130 [] -linordered_idom(A)|ord_less(A,zero_zero(A),plus_plus(A,power_power(A,B,number_number_of(nat,bit0(bit1(pls)))),power_power(A,C,number_number_of(nat,bit0(bit1(pls))))))|ti(A,C)=zero_zero(A). % 2.17/2.38 Following clause subsumed by 100 during input processing: 0 [copy,99,flip.1] bit0(A)!=bit1(B). % 2.17/2.38 Following clause subsumed by 99 during input processing: 0 [copy,100,flip.1] bit1(A)!=bit0(B). % 2.17/2.38 ** KEPT (pick-wt=11): 132 [copy,123,flip.1] zero_zero(int)!=plus_plus(int,plus_plus(int,one_one(int),A),A). % 2.17/2.38 Following clause subsumed by 123 during input processing: 0 [copy,132,flip.1] plus_plus(int,plus_plus(int,one_one(int),A),A)!=zero_zero(int). % 2.17/2.38 % 2.17/2.38 ------------> process sos: % 2.17/2.38 ** KEPT (pick-wt=3): 134 [] A=A. % 2.17/2.38 ** KEPT (pick-wt=7): 135 [] ti(A,undefined(A))=undefined(A). % 2.17/2.38 ---> New Demodulator: 136 [new_demod,135] ti(A,undefined(A))=undefined(A). % 2.17/2.38 ** KEPT (pick-wt=7): 137 [] bit0(ti(int,A))=bit0(A). % 2.17/2.38 ---> New Demodulator: 138 [new_demod,137] bit0(ti(int,A))=bit0(A). % 2.17/2.38 ** KEPT (pick-wt=7): 139 [] ti(int,bit0(A))=bit0(A). % 2.17/2.38 ---> New Demodulator: 140 [new_demod,139] ti(int,bit0(A))=bit0(A). % 2.17/2.38 ** KEPT (pick-wt=7): 141 [] bit1(ti(int,A))=bit1(A). % 2.17/2.38 ---> New Demodulator: 142 [new_demod,141] bit1(ti(int,A))=bit1(A). % 2.17/2.38 ** KEPT (pick-wt=7): 143 [] ti(int,bit1(A))=bit1(A). % 2.17/2.38 ---> New Demodulator: 144 [new_demod,143] ti(int,bit1(A))=bit1(A). % 2.17/2.38 ** KEPT (pick-wt=5): 145 [] ti(int,pls)=pls. % 2.17/2.38 ---> New Demodulator: 146 [new_demod,145] ti(int,pls)=pls. % 2.17/2.38 ** KEPT (pick-wt=5): 147 [] ti(nat,n)=n. % 2.17/2.38 ---> New Demodulator: 148 [new_demod,147] ti(nat,n)=n. % 2.17/2.38 ** KEPT (pick-wt=5): 149 [] ti(int,t)=t. % 2.17/2.38 ---> New Demodulator: 150 [new_demod,149] ti(int,t)=t. % 2.17/2.38 ** KEPT (pick-wt=11): 151 [] ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))). % 2.17/2.38 ** KEPT (pick-wt=5): 152 [] ord_less(int,one_one(int),t). % 2.17/2.38 ** KEPT (pick-wt=25): 153 [] power_power(int,power_power(int,A,number_number_of(nat,bit0(bit1(pls)))),number_number_of(nat,bit0(bit1(pls))))=power_power(int,A,number_number_of(nat,bit0(bit0(bit1(pls))))). % 2.17/2.38 ** KEPT (pick-wt=5): 154 [] ord_less(nat,zero_zero(nat),n). % 2.17/2.38 ** KEPT (pick-wt=11): 155 [] ord_less(int,A,B)|A=B|ord_less(int,B,A). % 2.17/2.38 ** KEPT (pick-wt=15): 157 [copy,156,flip.1] number_number_of(int,plus_plus(int,A,B))=plus_plus(int,number_number_of(int,A),number_number_of(int,B)). % 2.17/2.38 ---> New Demodulator: 158 [new_demod,157] number_number_of(int,plus_plus(int,A,B))=plus_plus(int,number_number_of(int,A),number_number_of(int,B)). % 2.17/2.38 ** KEPT (pick-wt=6): 159 [] zero_zero(int)=number_number_of(int,pls). % 2.17/2.38 ---> New Demodulator: 160 [new_demod,159] zero_zero(int)=number_number_of(int,pls). % 2.17/2.38 ** KEPT (pick-wt=13): 162 [copy,161,flip.1] semiring_1_of_nat(int,power_power(nat,A,B))=power_power(int,semiring_1_of_nat(int,A),B). % 2.17/2.38 ---> New Demodulator: 163 [new_demod,162] semiring_1_of_nat(int,power_power(nat,A,B))=power_power(int,semiring_1_of_nat(int,A),B). % 2.17/2.38 Following clause subsumed by 134 during input processing: 0 [demod,163] power_power(int,semiring_1_of_nat(int,A),B)=power_power(int,semiring_1_of_nat(int,A),B). % 2.17/2.38 ** KEPT (pick-wt=21): 165 [copy,164,flip.1] plus_plus(int,semiring_1_of_nat(int,plus_plus(nat,A,B)),C)=plus_plus(int,semiring_1_of_nat(int,A),plus_plus(int,semiring_1_of_nat(int,B),C)). % 2.17/2.38 ---> New Demodulator: 166 [new_demod,165] plus_plus(int,semiring_1_of_nat(int,plus_plus(nat,A,B)),C)=plus_plus(int,semiring_1_of_nat(int,A),plus_plus(int,semiring_1_of_nat(int,B),C)). % 2.17/2.38 ** KEPT (pick-wt=15): 168 [copy,167,flip.1] semiring_1_of_nat(int,plus_plus(nat,A,B))=plus_plus(int,semiring_1_of_nat(int,A),semiring_1_of_nat(int,B)). % 2.17/2.38 ---> New Demodulator: 169 [new_demod,168] semiring_1_of_nat(int,plus_plus(nat,A,B))=plus_plus(int,semiring_1_of_nat(int,A),semiring_1_of_nat(int,B)). % 2.17/2.38 ** KEPT (pick-wt=7): 170 [] semiring_1_of_nat(int,one_one(nat))=one_one(int). % 2.17/2.38 ---> New Demodulator: 171 [new_demod,170] semiring_1_of_nat(int,one_one(nat))=one_one(int). % 2.17/2.38 ** KEPT (pick-wt=6): 173 [copy,172,flip.1] zero_zero(nat)=number_number_of(nat,pls). % 2.17/2.38 ---> New Demodulator: 174 [new_demod,173] zero_zero(nat)=number_number_of(nat,pls). % 2.17/2.38 Following clause subsumed by 134 during input processing: 0 [demod,174] number_number_of(nat,pls)=number_number_of(nat,pls). % 2.17/2.38 ** KEPT (pick-wt=9): 176 [copy,175,demod,174,160] semiring_1_of_nat(int,number_number_of(nat,pls))=number_number_of(int,pls). % 2.17/2.38 ---> New Demodulator: 177 [new_demod,176] semiring_1_of_nat(int,number_number_of(nat,pls))=number_number_of(int,pls). % 2.17/2.38 ** KEPT (pick-wt=12): 178 [] plus_plus(nat,one_one(nat),one_one(nat))=number_number_of(nat,bit0(bit1(pls))). % 2.17/2.38 ---> New Demodulator: 179 [new_demod,178] plus_plus(nat,one_one(nat),one_one(nat))=number_number_of(nat,bit0(bit1(pls))). % 2.17/2.38 ** KEPT (pick-wt=23): 181 [copy,180,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.17/2.38 ** KEPT (pick-wt=7): 182 [] one_one(int)=number_number_of(int,bit1(pls)). % 2.17/2.38 ---> New Demodulator: 183 [new_demod,182] one_one(int)=number_number_of(int,bit1(pls)). % 2.17/2.38 ** KEPT (pick-wt=7): 185 [copy,184,flip.1] one_one(nat)=number_number_of(nat,bit1(pls)). % 2.17/2.38 ---> New Demodulator: 186 [new_demod,185] one_one(nat)=number_number_of(nat,bit1(pls)). % 2.17/2.38 Following clause subsumed by 134 during input processing: 0 [demod,186] number_number_of(nat,bit1(pls))=number_number_of(nat,bit1(pls)). % 2.17/2.38 ** KEPT (pick-wt=15): 187 [] plus_plus(int,plus_plus(int,A,B),C)=plus_plus(int,A,plus_plus(int,B,C)). % 2.17/2.38 ---> New Demodulator: 188 [new_demod,187] plus_plus(int,plus_plus(int,A,B),C)=plus_plus(int,A,plus_plus(int,B,C)). % 2.17/2.38 ** KEPT (pick-wt=15): 189 [] plus_plus(int,A,plus_plus(int,B,C))=plus_plus(int,B,plus_plus(int,A,C)). % 2.17/2.38 ** KEPT (pick-wt=9): 190 [] plus_plus(int,A,B)=plus_plus(int,B,A). % 2.17/2.38 ** KEPT (pick-wt=9): 192 [copy,191,demod,160,183] ord_less(int,number_number_of(int,pls),number_number_of(int,bit1(pls))). % 2.17/2.38 ** KEPT (pick-wt=4): 193 [] bit0(pls)=pls. % 2.17/2.38 ---> New Demodulator: 194 [new_demod,193] bit0(pls)=pls. % 2.17/2.38 ** KEPT (pick-wt=5): 196 [copy,195,demod,160,flip.1] number_number_of(int,pls)=pls. % 2.17/2.38 ---> New Demodulator: 197 [new_demod,196] number_number_of(int,pls)=pls. % 2.17/2.38 ** KEPT (pick-wt=6): 198 [] plus_plus(int,A,pls)=A. % 2.17/2.38 ---> New Demodulator: 199 [new_demod,198] plus_plus(int,A,pls)=A. % 2.17/2.38 ** KEPT (pick-wt=6): 200 [] plus_plus(int,pls,A)=A. % 2.17/2.38 ---> New Demodulator: 201 [new_demod,200] plus_plus(int,pls,A)=A. % 2.17/2.38 ** KEPT (pick-wt=12): 203 [copy,202,flip.1] bit0(plus_plus(int,A,B))=plus_plus(int,bit0(A),bit0(B)). % 2.17/2.38 ---> New Demodulator: 204 [new_demod,203] bit0(plus_plus(int,A,B))=plus_plus(int,bit0(A),bit0(B)). % 2.17/2.38 ** KEPT (pick-wt=7): 205 [] bit0(A)=plus_plus(int,A,A). % 2.17/2.38 ---> New Demodulator: 206 [new_demod,205] bit0(A)=plus_plus(int,A,A). % 2.17/2.38 Following clause subsumed by 134 during input processing: 0 [demod,160,197,199] A=A. % 2.17/2.38 Following clause subsumed by 134 during input processing: 0 [demod,160,197,201] A=A. % 2.17/2.38 ** KEPT (pick-wt=14): 208 [copy,207,demod,206,flip.1] bit1(plus_plus(int,A,B))=plus_plus(int,bit1(A),plus_plus(int,B,B)). % 2.17/2.38 ---> New Demodulator: 209 [new_demod,208] bit1(plus_plus(int,A,B))=plus_plus(int,bit1(A),plus_plus(int,B,B)). % 2.17/2.38 ** KEPT (pick-wt=17): 211 [copy,210,demod,206,188,209] plus_plus(int,A,plus_plus(int,A,bit1(B)))=plus_plus(int,bit1(A),plus_plus(int,B,B)). % 2.17/2.38 ** KEPT (pick-wt=13): 213 [copy,212,demod,183,188] bit1(A)=plus_plus(int,number_number_of(int,bit1(pls)),plus_plus(int,A,A)). % 2.17/2.38 ** KEPT (pick-wt=2): 214 [] linord219039673up_add(int). % 2.17/2.38 ** KEPT (pick-wt=2): 215 [] ring_11004092258visors(int). % 2.17/2.38 ** KEPT (pick-wt=2): 216 [] no_zero_divisors(int). % 2.17/2.38 ** KEPT (pick-wt=2): 217 [] linordered_idom(int). % 2.17/2.38 ** KEPT (pick-wt=2): 218 [] number_semiring(int). % 2.17/2.38 ** KEPT (pick-wt=2): 219 [] zero_ne_q_one(int). % 2.17/2.38 ** KEPT (pick-wt=2): 220 [] semiring_1(int). % 2.17/2.38 ** KEPT (pick-wt=2): 221 [] semiring_0(int). % 2.17/2.38 ** KEPT (pick-wt=2): 222 [] mult_zero(int). % 2.17/2.38 ** KEPT (pick-wt=2): 223 [] ring_char_0(int). % 2.17/2.38 ** KEPT (pick-wt=2): 224 [] number_ring(int). % 2.17/2.38 ** KEPT (pick-wt=2): 225 [] power(int). % 2.17/2.38 ** KEPT (pick-wt=2): 226 [] number(int). % 2.17/2.38 ** KEPT (pick-wt=2): 227 [] no_zero_divisors(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 228 [] number_semiring(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 229 [] zero_ne_q_one(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 230 [] semiring_1(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 231 [] semiring_0(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 232 [] mult_zero(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 233 [] power(nat). % 2.17/2.38 ** KEPT (pick-wt=2): 234 [] number(nat). % 2.17/2.38 ** KEPT (pick-wt=9): 235 [] ti(A,ti(A,B))=ti(A,B). % 2.17/2.38 ---> New Demodulator: 236 [new_demod,235] ti(A,ti(A,B))=ti(A,B). % 2.17/2.38 ** KEPT (pick-wt=21): 238 [copy,237,demod,183,206,160,197] power_power(int,plus_plus(int,number_number_of(int,bit1(pls)),semiring_1_of_nat(int,n)),number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls))))=pls. % 2.17/2.38 ---> New Demodulator: 239 [new_demod,238] power_power(int,plus_plus(int,number_number_of(int,bit1(pls)),semiring_1_of_nat(int,n)),number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls))))=pls. % 2.17/2.38 Following clause subsumed by 134 during input processing: 0 [copy,134,flip.1] A=A. % 2.17/2.38 >>>> Starting back demodulation with 136. % 2.17/2.38 >>>> Starting back demodulation with 138. % 2.17/2.38 >>>> Starting back demodulation with 140. % 2.17/2.38 >>>> Starting back demodulation with 142. % 2.17/2.38 >>>> Starting back demodulation with 144. % 2.17/2.38 >>>> Starting back demodulation with 146. % 2.17/2.38 >>>> Starting back demodulation with 148. % 2.17/2.38 >>>> Starting back demodulation with 150. % 2.17/2.38 ** KEPT (pick-wt=41): 240 [copy,153,flip.1,demod,206,206,188,206,206] power_power(int,A,number_number_of(nat,plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),bit1(pls))))))=power_power(int,power_power(int,A,number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))),number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))). % 2.17/2.38 >>>> Starting back demodulation with 158. % 2.17/2.38 >>>> Starting back demodulation with 160. % 2.17/2.38 >> back demodulating 151 with 160. % 2.17/2.38 >> back demodulating 132 with 160. % 2.17/2.38 >> back demodulating 123 with 160. % 2.17/2.38 >> back demodulating 107 with 160. % 2.17/2.38 >> back demodulating 95 with 160. % 2.17/2.38 >> back demodulating 94 with 160. % 2.17/2.38 >> back demodulating 89 with 160. % 2.17/2.38 >> back demodulating 85 with 160. % 2.17/2.38 >> back demodulating 84 with 160. % 2.17/2.38 >> back demodulating 83 with 160. % 2.17/2.38 >> back demodulating 82 with 160. % 2.17/2.38 >> back demodulating 81 with 160. % 2.17/2.38 >> back demodulating 48 with 160. % 2.17/2.38 >> back demodulating 47 with 160. % 2.17/2.38 >>>> Starting back demodulation with 163. % 2.17/2.38 >>>> Starting back demodulation with 166. % 2.17/2.38 >>>> Starting back demodulation with 169. % 2.17/2.38 >> back demodulating 165 with 169. % 2.17/2.38 >>>> Starting back demodulation with 171. % 2.17/2.38 >>>> Starting back demodulation with 174. % 2.17/2.38 >> back demodulating 154 with 174. % 2.17/2.38 >> back demodulating 118 with 174. % 2.17/2.38 >> back demodulating 117 with 174. % 2.17/2.38 >> back demodulating 41 with 174. % 2.17/2.38 >> back demodulating 40 with 174. % 2.17/2.38 >>>> Starting back demodulation with 177. % 2.17/2.38 >>>> Starting back demodulation with 179. % 2.17/2.38 >>>> Starting back demodulation with 183. % 2.17/2.38 >> back demodulating 170 with 183. % 2.17/2.38 >> back demodulating 152 with 183. % 2.17/2.38 >> back demodulating 88 with 183. % 2.17/2.38 >> back demodulating 87 with 183. % 2.17/2.38 >> back demodulating 86 with 183. % 2.17/2.38 >>>> Starting back demodulation with 186. % 2.17/2.38 >> back demodulating 178 with 186. % 2.17/2.38 >>>> Starting back demodulation with 188. % 2.17/2.38 Following clause subsumed by 189 during input processing: 0 [copy,189,flip.1] plus_plus(int,A,plus_plus(int,B,C))=plus_plus(int,B,plus_plus(int,A,C)). % 2.17/2.38 Following clause subsumed by 190 during input processing: 0 [copy,190,flip.1] plus_plus(int,A,B)=plus_plus(int,B,A). % 2.17/2.38 >>>> Starting back demodulation with 194. % 2.17/2.38 >>>> Starting back demodulation with 197. % 2.17/2.38 >> back demodulating 192 with 197. % 2.17/2.38 >> back demodulating 176 with 197. % 2.17/2.38 >> back demodulating 159 with 197. % 2.17/2.38 >>>> Starting back demodulation with 199. % 2.17/2.38 >>>> Starting back demodulation with 201. % 2.17/2.38 >>>> Starting back demodulation with 204. % 2.17/2.38 >>>> Starting back demodulation with 206. % 2.17/2.38 >> back demodulating 203 with 206. % 2.17/2.38 >> back demodulating 193 with 206. % 2.17/2.38 >> back demodulating 153 with 206. % 2.17/2.38 >> back demodulating 139 with 206. % 2.17/2.38 >> back demodulating 137 with 206. % 2.17/2.38 >> back demodulating 133 with 206. % 2.17/2.38 >> back demodulating 131 with 206. % 2.17/2.38 >> back demodulating 130 with 206. % 2.17/2.38 >> back demodulating 129 with 206. % 2.17/2.38 >> back demodulating 128 with 206. % 2.17/2.38 >> back demodulating 127 with 206. % 2.17/2.38 >> back demodulating 126 with 206. % 2.17/2.38 >> back demodulating 125 with 206. % 2.17/2.38 >> back demodulating 106 with 206. % 2.17/2.38 >> back demodulating 104 with 206. % 2.17/2.38 >> back demodulating 102 with 206. % 2.17/2.38 >> back demodulating 101 with 206. % 2.17/2.38 >> back demodulating 100 with 206. % 2.17/2.38 >> back demodulating 99 with 206. % 2.17/2.38 >> back demodulating 80 with 206. % 2.17/2.38 >> back demodulating 79 with 206. % 2.17/2.38 >> back demodulating 78 with 206. % 2.17/2.38 >> back demodulating 77 with 206. % 2.17/2.38 >> back demodulating 76 with 206. % 2.17/2.38 >> back demodulating 75 with 206. % 2.17/2.38 >> back demodulating 64 with 206. % 2.17/2.38 >> back demodulating 63 with 206. % 2.17/2.38 >> back demodulating 53 with 206. % 2.17/2.38 >> back demodulating 52 with 206. % 2.17/2.38 >> back demodulating 39 with 206. % 2.17/2.38 >> back demodulating 38 with 206. % 2.17/2.38 >> back demodulating 35 with 206. % 2.17/2.38 >> back demodulating 34 with 206. % 2.17/2.38 >> back demodulating 33 with 206. % 2.17/2.38 >> back demodulating 32 with 206. % 2.17/2.38 >> back demodulating 31 with 206. % 2.17/2.38 >> back demodulating 30 with 206. % 2.17/2.38 >> back demodulating 29 with 206. % 2.17/2.38 >>>> Starting back demodulation with 209. % 2.17/2.38 ** KEPT (pick-wt=17): 307 [copy,211,flip.1] plus_plus(int,bit1(A),plus_plus(int,B,B))=plus_plus(int,A,plus_plus(int,A,bit1(B))). % 2.17/2.38 ** KEPT (pick-wt=13): 308 [copy,213,flip.1] plus_plus(int,number_number_of(int,bit1(pls)),plus_plus(int,A,A))=bit1(A). % 2.17/2.38 >>>> Starting back demodulation with 236. % 2.17/2.38 >>>> Starting back demodulation with 239. % 2.17/2.38 Following clause subsumed by 271 during input processing: 0 [copy,240,flip.1,demod,264,264] power_power(int,power_power(int,A,plus_plus(nat,number_number_of(nat,bit1(pls)),number_number_of(nat,bit1(pls)))),plus_plus(nat,number_number_of(nat,bit1(pls)),number_number_of(nat,bit1(pls))))=power_power(int,A,number_number_of(nat,plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),bit1(pls)))))). % 53.17/53.39 >>>> Starting back demodulation with 258. % 53.17/53.39 >>>> Starting back demodulation with 264. % 53.17/53.39 >> back demodulating 240 with 264. % 53.17/53.39 >> back demodulating 238 with 264. % 53.17/53.39 >>>> Starting back demodulation with 267. % 53.17/53.39 >>>> Starting back demodulation with 269. % 53.17/53.39 ** KEPT (pick-wt=21): 312 [copy,270,flip.1] plus_plus(int,A,plus_plus(int,A,plus_plus(int,B,B)))=plus_plus(int,A,plus_plus(int,B,plus_plus(int,A,B))). % 53.17/53.39 Following clause subsumed by 309 during input processing: 0 [copy,271,flip.1] power_power(int,A,number_number_of(nat,plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),bit1(pls))))))=power_power(int,power_power(int,A,plus_plus(nat,number_number_of(nat,bit1(pls)),number_number_of(nat,bit1(pls)))),plus_plus(nat,number_number_of(nat,bit1(pls)),number_number_of(nat,bit1(pls)))). % 53.17/53.39 >>>> Starting back demodulation with 273. % 53.17/53.39 >>>> Starting back demodulation with 275. % 53.17/53.39 Following clause subsumed by 289 during input processing: 0 [copy,288,flip.1] bit1(A)!=plus_plus(int,B,B). % 53.17/53.39 Following clause subsumed by 288 during input processing: 0 [copy,289,flip.1] plus_plus(int,A,A)!=bit1(B). % 53.17/53.39 Following clause subsumed by 211 during input processing: 0 [copy,307,flip.1] plus_plus(int,A,plus_plus(int,A,bit1(B)))=plus_plus(int,bit1(A),plus_plus(int,B,B)). % 53.17/53.39 Following clause subsumed by 213 during input processing: 0 [copy,308,flip.1] bit1(A)=plus_plus(int,number_number_of(int,bit1(pls)),plus_plus(int,A,A)). % 53.17/53.39 Following clause subsumed by 271 during input processing: 0 [copy,309,flip.1] power_power(int,power_power(int,A,plus_plus(nat,number_number_of(nat,bit1(pls)),number_number_of(nat,bit1(pls)))),plus_plus(nat,number_number_of(nat,bit1(pls)),number_number_of(nat,bit1(pls))))=power_power(int,A,number_number_of(nat,plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),plus_plus(int,bit1(pls),bit1(pls)))))). % 53.17/53.39 >>>> Starting back demodulation with 311. % 53.17/53.39 Following clause subsumed by 270 during input processing: 0 [copy,312,flip.1] plus_plus(int,A,plus_plus(int,B,plus_plus(int,A,B)))=plus_plus(int,A,plus_plus(int,A,plus_plus(int,B,B))). % 53.17/53.39 % 53.17/53.39 ======= end of input processing ======= % 53.17/53.39 % 53.17/53.39 =========== start of search =========== % 53.17/53.39 % 53.17/53.39 % 53.17/53.39 Resetting weight limit to 7. % 53.17/53.39 % 53.17/53.39 % 53.17/53.39 Resetting weight limit to 7. % 53.17/53.39 % 53.17/53.39 sos_size=524 % 53.17/53.39 % 53.17/53.39 Search stopped because sos empty. % 53.17/53.39 % 53.17/53.39 % 53.17/53.39 Search stopped because sos empty. % 53.17/53.39 % 53.17/53.39 ============ end of search ============ % 53.17/53.39 % 53.17/53.39 -------------- statistics ------------- % 53.17/53.39 clauses given 593 % 53.17/53.39 clauses generated 311253 % 53.17/53.39 clauses kept 785 % 53.17/53.39 clauses forward subsumed 1993 % 53.17/53.39 clauses back subsumed 3 % 53.17/53.39 Kbytes malloced 5859 % 53.17/53.39 % 53.17/53.39 ----------- times (seconds) ----------- % 53.17/53.39 user CPU time 51.03 (0 hr, 0 min, 51 sec) % 53.17/53.39 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 53.17/53.39 wall-clock time 53 (0 hr, 0 min, 53 sec) % 53.17/53.39 % 53.17/53.39 Process 5700 finished Wed Jul 27 09:55:12 2022 % 53.24/53.39 Otter interrupted % 53.24/53.39 PROOF NOT FOUND %------------------------------------------------------------------------------