%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NUM924+2 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n004.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 : 600s
% DateTime : Mon Jul 18 14:23:08 EDT 2022
% Result : Theorem 0.19s 0.49s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : NUM924+2 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n004.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Thu Jul 7 21:20:37 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.19/0.43 ----- Otter 3.2, August 2001 -----
% 0.19/0.43 The process was started by sandbox on n004.cluster.edu,
% 0.19/0.43 Thu Jul 7 21:20:37 2022
% 0.19/0.43 The command was "./sos". The process ID is 29002.
% 0.19/0.43
% 0.19/0.43 set(prolog_style_variables).
% 0.19/0.43 set(auto).
% 0.19/0.43 dependent: set(auto1).
% 0.19/0.43 dependent: set(process_input).
% 0.19/0.43 dependent: clear(print_kept).
% 0.19/0.43 dependent: clear(print_new_demod).
% 0.19/0.43 dependent: clear(print_back_demod).
% 0.19/0.43 dependent: clear(print_back_sub).
% 0.19/0.43 dependent: set(control_memory).
% 0.19/0.43 dependent: assign(max_mem, 12000).
% 0.19/0.43 dependent: assign(pick_given_ratio, 4).
% 0.19/0.43 dependent: assign(stats_level, 1).
% 0.19/0.43 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.43 dependent: assign(sos_limit, 5000).
% 0.19/0.43 dependent: assign(max_weight, 60).
% 0.19/0.43 clear(print_given).
% 0.19/0.43
% 0.19/0.43 formula_list(usable).
% 0.19/0.43
% 0.19/0.43 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=1, max_lits=9.
% 0.19/0.43
% 0.19/0.43 This ia a non-Horn set with equality. The strategy will be
% 0.19/0.43 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.19/0.43 unit deletion, with positive clauses in sos and nonpositive
% 0.19/0.43 clauses in usable.
% 0.19/0.43
% 0.19/0.43 dependent: set(knuth_bendix).
% 0.19/0.43 dependent: set(para_from).
% 0.19/0.43 dependent: set(para_into).
% 0.19/0.43 dependent: clear(para_from_right).
% 0.19/0.43 dependent: clear(para_into_right).
% 0.19/0.43 dependent: set(para_from_vars).
% 0.19/0.43 dependent: set(eq_units_both_ways).
% 0.19/0.43 dependent: set(dynamic_demod_all).
% 0.19/0.43 dependent: set(dynamic_demod).
% 0.19/0.43 dependent: set(order_eq).
% 0.19/0.43 dependent: set(back_demod).
% 0.19/0.43 dependent: set(lrpo).
% 0.19/0.43 dependent: set(hyper_res).
% 0.19/0.43 dependent: set(unit_deletion).
% 0.19/0.43 dependent: set(factor).
% 0.19/0.43
% 0.19/0.43 There is a clause for symmetry of equality, so it is
% 0.19/0.43 assumed that equality is fully axiomatized; therefore,
% 0.19/0.43 paramodulation is disabled.
% 0.19/0.43
% 0.19/0.43 dependent: clear(para_from).
% 0.19/0.43 dependent: clear(para_into).
% 0.19/0.43
% 0.19/0.43 ------------> process usable:
% 0.19/0.43 Following clause subsumed by 34 during input processing: 0 [] {-} -ord_less_eq_int(number_number_of_int(A),number_number_of_int(B))|ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 35 during input processing: 0 [] {-} ord_less_eq_int(number_number_of_int(A),number_number_of_int(B))| -ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 40 during input processing: 0 [] {-} -ord_less_eq_int(bit1(A),bit1(B))|ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 41 during input processing: 0 [] {-} ord_less_eq_int(bit1(A),bit1(B))| -ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 42 during input processing: 0 [] {-} -ord_less_eq_int(bit0(A),bit0(B))|ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 43 during input processing: 0 [] {-} ord_less_eq_int(bit0(A),bit0(B))| -ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 48 during input processing: 0 [flip.1] {-} number_number_of_nat(A)!=zero_zero_nat|ord_less_eq_int(A,pls).
% 0.19/0.43 Following clause subsumed by 49 during input processing: 0 [flip.1] {-} number_number_of_nat(A)=zero_zero_nat| -ord_less_eq_int(A,pls).
% 0.19/0.43 Following clause subsumed by 77 during input processing: 0 [] {-} -ord_less_eq_int(bit0(A),bit1(B))|ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 78 during input processing: 0 [] {-} ord_less_eq_int(bit0(A),bit1(B))| -ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 100 during input processing: 0 [] {-} -ord_less_eq_int(bit1(A),bit0(B))|ord_less_int(A,B).
% 0.19/0.43 Following clause subsumed by 101 during input processing: 0 [] {-} ord_less_eq_int(bit1(A),bit0(B))| -ord_less_int(A,B).
% 0.19/0.43 Following clause subsumed by 102 during input processing: 0 [] {-} -ord_less_int(bit0(A),bit1(B))|ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 103 during input processing: 0 [] {-} ord_less_int(bit0(A),bit1(B))| -ord_less_eq_int(A,B).
% 0.19/0.43 Following clause subsumed by 109 during input processing: 0 [] {-} ord_less_eq_int(plus_plus_int(A,one_one_int),B)| -ord_less_int(A,B).
% 0.19/0.43 Following clause subsumed by 174 during input processing: 0 [flip.1] {-} bit1(A)!=pls.
% 0.19/0.43 Following clause subsumed by 183 during input processing: 0 [] {-} -ord_less_int(bit1(A),bit1(B))|ord_less_int(A,B).
% 0.19/0.43 Following clause subsumed by 184 during input processing: 0 [] {-} ord_less_int(bit1(A),bit1(B))| -ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 186 during input processing: 0 [] {-} -ord_less_int(bit0(A),bit0(B))|ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 187 during input processing: 0 [] {-} ord_less_int(bit0(A),bit0(B))| -ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 92 during input processing: 0 [] {-} -ord_less_int(number_number_of_int(A),number_number_of_int(B))|ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 93 during input processing: 0 [] {-} ord_less_int(number_number_of_int(A),number_number_of_int(B))| -ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 204 during input processing: 0 [] {-} -ord_less_int(bit1(A),bit0(B))|ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 205 during input processing: 0 [] {-} ord_less_int(bit1(A),bit0(B))| -ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 243 during input processing: 0 [] {-} -ord_less_nat(zero_zero_nat,power_power_nat(A,number_number_of_nat(B)))|number_number_of_nat(B)=zero_zero_nat|ord_less_nat(zero_zero_nat,A).
% 0.19/0.44 Following clause subsumed by 244 during input processing: 0 [] {-} ord_less_nat(zero_zero_nat,power_power_nat(A,number_number_of_nat(B)))|number_number_of_nat(B)!=zero_zero_nat.
% 0.19/0.44 Following clause subsumed by 245 during input processing: 0 [] {-} ord_less_nat(zero_zero_nat,power_power_nat(A,number_number_of_nat(B)))| -ord_less_nat(zero_zero_nat,A).
% 0.19/0.44 Following clause subsumed by 192 during input processing: 0 [] {-} -is_int(A)|plus_plus_int(zero_zero_int,A)=A.
% 0.19/0.44 Following clause subsumed by 191 during input processing: 0 [] {-} -is_int(A)|plus_plus_int(A,zero_zero_int)=A.
% 0.19/0.44 Following clause subsumed by 278 during input processing: 0 [] {-} plus_plus_real(times_times_real(A,B),times_times_real(C,D))!=plus_plus_real(times_times_real(A,D),times_times_real(C,B))|A=C|B=D.
% 0.19/0.44 Following clause subsumed by 279 during input processing: 0 [] {-} plus_plus_real(times_times_real(A,B),times_times_real(C,D))=plus_plus_real(times_times_real(A,D),times_times_real(C,B))|A!=C.
% 0.19/0.44 Following clause subsumed by 280 during input processing: 0 [] {-} plus_plus_real(times_times_real(A,B),times_times_real(C,D))=plus_plus_real(times_times_real(A,D),times_times_real(C,B))|B!=D.
% 0.19/0.44 Following clause subsumed by 281 during input processing: 0 [] {-} plus_plus_nat(times_times_nat(A,B),times_times_nat(C,D))!=plus_plus_nat(times_times_nat(A,D),times_times_nat(C,B))|A=C|B=D.
% 0.19/0.44 Following clause subsumed by 282 during input processing: 0 [] {-} plus_plus_nat(times_times_nat(A,B),times_times_nat(C,D))=plus_plus_nat(times_times_nat(A,D),times_times_nat(C,B))|A!=C.
% 0.19/0.44 Following clause subsumed by 283 during input processing: 0 [] {-} plus_plus_nat(times_times_nat(A,B),times_times_nat(C,D))=plus_plus_nat(times_times_nat(A,D),times_times_nat(C,B))|B!=D.
% 0.19/0.44 Following clause subsumed by 284 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -is_int(C)| -is_int(D)|plus_plus_int(times_times_int(A,B),times_times_int(C,D))!=plus_plus_int(times_times_int(A,D),times_times_int(C,B))|A=C|B=D.
% 0.19/0.44 Following clause subsumed by 285 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -is_int(C)| -is_int(D)|plus_plus_int(times_times_int(A,B),times_times_int(C,D))=plus_plus_int(times_times_int(A,D),times_times_int(C,B))|A!=C.
% 0.19/0.44 Following clause subsumed by 286 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -is_int(C)| -is_int(D)|plus_plus_int(times_times_int(A,B),times_times_int(C,D))=plus_plus_int(times_times_int(A,D),times_times_int(C,B))|B!=D.
% 0.19/0.44 Following clause subsumed by 95 during input processing: 0 [] {-} -is_int(A)|times_times_int(one_one_int,A)=A.
% 0.19/0.44 Following clause subsumed by 94 during input processing: 0 [] {-} -is_int(A)|times_times_int(A,one_one_int)=A.
% 0.19/0.44 Following clause subsumed by 328 during input processing: 0 [] {-} pls!=min.
% 0.19/0.44 Following clause subsumed by 330 during input processing: 0 [] {-} bit0(A)!=min.
% 0.19/0.44 Following clause subsumed by 358 during input processing: 0 [] {-} zcong(A,B,C)| -zcong(B,A,C).
% 0.19/0.44 Following clause subsumed by 46 during input processing: 0 [] {-} -is_int(A)| -is_int(B)| -ord_less_eq_int(A,B)|A=B|ord_less_int(A,B).
% 0.19/0.44 Following clause subsumed by 407 during input processing: 0 [] {-} -zcong(A,zero_zero_int,B)|dvd_dvd_int(B,A).
% 0.19/0.44 Following clause subsumed by 408 during input processing: 0 [] {-} zcong(A,zero_zero_int,B)| -dvd_dvd_int(B,A).
% 0.19/0.44 Following clause subsumed by 374 during input processing: 0 [] {-} -is_int(A)| -ord_less_eq_int(zero_zero_int,A)| -ord_less_int(A,B)| -zcong(A,zero_zero_int,B)|A=zero_zero_int.
% 0.19/0.44 Following clause subsumed by 411 during input processing: 0 [] {-} -zprime(A)| -ord_less_int(zero_zero_int,B)|zcong(B,zero_zero_int,A)|zcong(C,zero_zero_int,A)| -zcong(times_times_int(B,C),zero_zero_int,A).
% 0.19/0.44 Following clause subsumed by 411 during input processing: 0 [] {-} -zprime(A)| -ord_less_int(zero_zero_int,B)| -zcong(times_times_int(B,C),zero_zero_int,A)|zcong(B,zero_zero_int,A)|zcong(C,zero_zero_int,A).
% 0.19/0.44 Following clause subsumed by 246 during input processing: 0 [] {-} -zprime(A)| -dvd_dvd_int(A,power_power_int(B,C))| -ord_less_nat(zero_zero_nat,C)|dvd_dvd_int(A,B).
% 0.19/0.44 Following clause subsumed by 18 during input processing: 0 [] {-} plus_plus_real(power_power_real(A,number_number_of_nat(bit0(bit1(pls)))),power_power_real(B,number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_real|A=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 19 during input processing: 0 [] {-} plus_plus_real(power_power_real(A,number_number_of_nat(bit0(bit1(pls)))),power_power_real(B,number_number_of_nat(bit0(bit1(pls)))))!=zero_zero_real|B=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 20 during input processing: 0 [] {-} plus_plus_real(power_power_real(A,number_number_of_nat(bit0(bit1(pls)))),power_power_real(B,number_number_of_nat(bit0(bit1(pls)))))=zero_zero_real|A!=zero_zero_real|B!=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 360 during input processing: 0 [] {-} ord_less_real(A,B)| -ord_less_eq_real(A,B)|A=B.
% 0.19/0.44 Following clause subsumed by 360 during input processing: 0 [] {-} -ord_less_eq_real(A,B)|ord_less_real(A,B)|A=B.
% 0.19/0.44 Following clause subsumed by 424 during input processing: 0 [] {-} ord_less_eq_real(A,B)| -ord_less_real(A,B).
% 0.19/0.44 Following clause subsumed by 137 during input processing: 0 [] {-} plus_plus_real(times_times_real(A,A),times_times_real(B,B))!=zero_zero_real|A=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 138 during input processing: 0 [] {-} plus_plus_real(times_times_real(A,A),times_times_real(B,B))!=zero_zero_real|B=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 139 during input processing: 0 [] {-} plus_plus_real(times_times_real(A,A),times_times_real(B,B))=zero_zero_real|A!=zero_zero_real|B!=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 420 during input processing: 0 [] {-} power_power_nat(A,B)=one_one_nat|B!=zero_zero_nat.
% 0.19/0.44 Following clause subsumed by 420 during input processing: 0 [] {-} A!=zero_zero_nat|power_power_nat(B,A)=one_one_nat.
% 0.19/0.44 Following clause subsumed by 261 during input processing: 0 [] {-} -is_int(A)|power_power_int(A,one_one_nat)=A.
% 0.19/0.44 Following clause subsumed by 302 during input processing: 0 [] {-} -ord_less_eq_int(zero_zero_int,A)|ord_less_eq_int(zero_zero_int,power_power_int(A,B)).
% 0.19/0.44 Following clause subsumed by 245 during input processing: 0 [] {-} -ord_less_nat(zero_zero_nat,A)|ord_less_nat(zero_zero_nat,power_power_nat(A,B)).
% 0.19/0.44 Following clause subsumed by 458 during input processing: 0 [] {-} power_power_real(A,B)!=zero_zero_real|A=zero_zero_real.
% 0.19/0.44 Following clause subsumed by 436 during input processing: 0 [] {-} power_power_nat(A,B)!=zero_zero_nat|A=zero_zero_nat.
% 0.19/0.44 Following clause subsumed by 435 during input processing: 0 [] {-} power_power_nat(A,B)!=zero_zero_nat|B!=zero_zero_nat.
% 0.19/0.44 Following clause subsumed by 437 during input processing: 0 [] {-} power_power_nat(A,B)=zero_zero_nat|A!=zero_zero_nat|B=zero_zero_nat.
% 0.19/0.44 Following clause subsumed by 459 during input processing: 0 [] {-} -is_int(A)|power_power_int(A,B)!=zero_zero_int|A=zero_zero_int.
% 0.19/0.44 Following clause subsumed by 243 during input processing: 0 [] {-} -ord_less_nat(zero_zero_nat,power_power_nat(A,B))|ord_less_nat(zero_zero_nat,A)|B=zero_zero_nat.
% 0.19/0.44 Following clause subsumed by 245 during input processing: 0 [] {-} ord_less_nat(zero_zero_nat,power_power_nat(A,B))| -ord_less_nat(zero_zero_nat,A).
% 0.19/0.49 Following clause subsumed by 244 during input processing: 0 [] {-} ord_less_nat(zero_zero_nat,power_power_nat(A,B))|B!=zero_zero_nat.
% 0.19/0.49 Following clause subsumed by 451 during input processing: 0 [] {-} A!=zero_zero_nat|power_power_real(zero_zero_real,A)=one_one_real.
% 0.19/0.49 Following clause subsumed by 420 during input processing: 0 [] {-} A!=zero_zero_nat|power_power_nat(zero_zero_nat,A)=one_one_nat.
% 0.19/0.49 Following clause subsumed by 452 during input processing: 0 [] {-} A!=zero_zero_nat|power_power_int(zero_zero_int,A)=one_one_int.
% 0.19/0.49 Following clause subsumed by 505 during input processing: 0 [] {-} -ord_less_real(one_one_real,A)| -ord_less_real(power_power_real(A,B),power_power_real(A,C))|ord_less_nat(B,C).
% 0.19/0.49 Following clause subsumed by 502 during input processing: 0 [] {-} -ord_less_real(one_one_real,A)|ord_less_real(power_power_real(A,B),power_power_real(A,C))| -ord_less_nat(B,C).
% 0.19/0.49 Following clause subsumed by 506 during input processing: 0 [] {-} -ord_less_nat(one_one_nat,A)| -ord_less_nat(power_power_nat(A,B),power_power_nat(A,C))|ord_less_nat(B,C).
% 0.19/0.49 Following clause subsumed by 503 during input processing: 0 [] {-} -ord_less_nat(one_one_nat,A)|ord_less_nat(power_power_nat(A,B),power_power_nat(A,C))| -ord_less_nat(B,C).
% 0.19/0.49 Following clause subsumed by 507 during input processing: 0 [] {-} -ord_less_int(one_one_int,A)| -ord_less_int(power_power_int(A,B),power_power_int(A,C))|ord_less_nat(B,C).
% 0.19/0.49 Following clause subsumed by 504 during input processing: 0 [] {-} -ord_less_int(one_one_int,A)|ord_less_int(power_power_int(A,B),power_power_int(A,C))| -ord_less_nat(B,C).
% 0.19/0.49 Following clause subsumed by 460 during input processing: 0 [] {-} -dvd_dvd_nat(A,B)|dvd_dvd_nat(power_power_nat(A,C),power_power_nat(B,C)).
% 0.19/0.49 Following clause subsumed by 520 during input processing: 0 [] {-} dvd_dvd_nat(times_times_nat(A,B),times_times_nat(C,B))| -dvd_dvd_nat(A,C).
% 0.19/0.49 Following clause subsumed by 176 during input processing: 0 [copy,175,flip.1] {-} bit0(A)!=bit1(B).
% 0.19/0.49 Following clause subsumed by 175 during input processing: 0 [copy,176,flip.1] {-} bit1(A)!=bit0(B).
% 0.19/0.49 290 back subsumes 29.
% 0.19/0.49 296 back subsumes 31.
% 0.19/0.49 355 back subsumes 169.
% 0.19/0.49 357 back subsumes 351.
% 0.19/0.49 409 back subsumes 377.
% 0.19/0.49 420 back subsumes 304.
% 0.19/0.49 435 back subsumes 294.
% 0.19/0.49 436 back subsumes 293.
% 0.19/0.49 437 back subsumes 295.
% 0.19/0.49 451 back subsumes 303.
% 0.19/0.49 452 back subsumes 305.
% 0.19/0.49 458 back subsumes 290.
% 0.19/0.49 459 back subsumes 296.
% 0.19/0.49 479 back subsumes 291.
% 0.19/0.49 480 back subsumes 292.
% 0.19/0.49 481 back subsumes 297.
% 0.19/0.49 482 back subsumes 298.
% 0.19/0.49 493 back subsumes 150.
% 0.19/0.49 494 back subsumes 151.
% 0.19/0.49 495 back subsumes 152.
% 0.19/0.49 627 back subsumes 576.
% 0.19/0.49 629 back subsumes 541.
% 0.19/0.49
% 0.19/0.49 ------------> process sos:
% 0.19/0.49 Following clause subsumed by 749 during input processing: 0 [] {-} ord_less_eq_int(pls,pls).
% 0.19/0.49 Following clause subsumed by 769 during input processing: 0 [demod,754] {-} times_times_int(number_number_of_int(A),number_number_of_int(B))=times_times_int(number_number_of_int(A),number_number_of_int(B)).
% 0.19/0.49 Following clause subsumed by 817 during input processing: 0 [demod,850,791,837,837,793,869] {-} plus_plus_int(A,A)=plus_plus_int(A,A).
% 0.19/0.49 Following clause subsumed by 871 during input processing: 0 [demod,850,853,834,834,874] {-} plus_plus_real(A,A)=plus_plus_real(A,A).
% 0.19/0.49 Following clause subsumed by 817 during input processing: 0 [demod,850,791,837,837,795,880] {-} plus_plus_int(A,A)=plus_plus_int(A,A).
% 0.19/0.49 Following clause subsumed by 780 during input processing: 0 [demod,778] {-} zero_zero_nat=zero_zero_nat.
% 0.19/0.49 Following clause subsumed by 890 during input processing: 0 [demod,820,845,845] {-} pls=pls.
% 0.19/0.49 Following clause subsumed by 892 during input processing: 0 [demod,888] {-} zero_zero_real=zero_zero_real.
% 0.19/0.49 Following clause subsumed by 890 during input processing: 0 [demod,845,820,845] {-} pls=pls.
% 0.19/0.49 Following clause subsumed by 908 during input processing: 0 [demod,791] {-} plus_plus_int(number_number_of_int(A),number_number_of_int(B))=plus_plus_int(number_number_of_int(A),number_number_of_int(B)).
% 0.19/0.49 Following clause subsumed by 955 during input processing: 0 [demod,920,906,853,888,888,947] {-} one_one_real=one_one_real.
% 0.19/0.49 Following clause subsumed by 957 during input processing: 0 [demod,920,791,791,820,845,820,845,953] {-} one_one_int=one_one_int.
% 0.19/0.49 Following clause subsumed by 871 during input processing: 0 [demod,920,850,815,815,906,906,888,906,888,906,853,888,888,947,895,895,960] {-} plus_plus_real(one_one_real,one_one_real)=plus_plus_real(one_one_real,one_one_real).
% 0.19/0.49 Following clause subsumed by 817 during input processing: 0 [demod,920,850,815,815,791,791,820,845,791,820,845,791,791,820,845,820,845,953,966] {-} plus_plus_int(one_one_int,one_one_int)=plus_plus_int(one_one_int,one_one_int).
% 0.19/0.49 Following clause subsumed by 1015 during input processing: 0 [] {-} power_power_int(power_power_int(A,B),C)=power_power_int(A,times_times_nat(B,C)).
% 0.19/0.49 Following clause subsumed by 1041 during input processing: 0 [demod,756] {-} times_times_int(A,times_times_int(B,C))=times_times_int(A,times_times_int(B,C)).
% 0.19/0.49 Following clause subsumed by 750 during input processing: 0 [] {-} times_times_int(A,B)=times_times_int(B,A).
% 0.19/0.49 Following clause subsumed by 817 during input processing: 0 [] {-} plus_plus_int(A,B)=plus_plus_int(B,A).
% 0.19/0.49 Following clause subsumed by 816 during input processing: 0 [] {-} plus_plus_int(A,plus_plus_int(B,C))=plus_plus_int(B,plus_plus_int(A,C)).
% 0.19/0.49 Following clause subsumed by 1062 during input processing: 0 [demod,815] {-} plus_plus_int(A,plus_plus_int(B,C))=plus_plus_int(A,plus_plus_int(B,C)).
% 0.19/0.49 Following clause subsumed by 890 during input processing: 0 [demod,845,785,845] {-} pls=pls.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,898] {-} A=A.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,795] {-} 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)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,793] {-} 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)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1124] {-} plus_plus_real(times_times_real(A,B),times_times_real(C,B))=plus_plus_real(times_times_real(A,B),times_times_real(C,B)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1126] {-} plus_plus_nat(times_times_nat(A,B),times_times_nat(C,B))=plus_plus_nat(times_times_nat(A,B),times_times_nat(C,B)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,793] {-} plus_plus_int(times_times_int(A,B),times_times_int(C,B))=plus_plus_int(times_times_int(A,B),times_times_int(C,B)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,759] {-} power_power_int(A,plus_plus_nat(B,C))=power_power_int(A,plus_plus_nat(B,C)).
% 0.19/0.49 Following clause subsumed by 749 during input processing: 0 [demod,845,845] {-} ord_less_eq_int(pls,pls).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1124,1128,1128] {-} plus_plus_real(A,A)=plus_plus_real(A,A).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1126,1130,1130] {-} plus_plus_nat(A,A)=plus_plus_nat(A,A).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,793,869] {-} plus_plus_int(A,A)=plus_plus_int(A,A).
% 0.19/0.49 Following clause subsumed by 1051 during input processing: 0 [demod,1124,1128,flip.1] {-} plus_plus_real(times_times_real(B,A),A)=plus_plus_real(A,times_times_real(B,A)).
% 0.19/0.49 Following clause subsumed by 1052 during input processing: 0 [demod,1126,1130,flip.1] {-} plus_plus_nat(times_times_nat(B,A),A)=plus_plus_nat(A,times_times_nat(B,A)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1124,1128] {-} plus_plus_real(times_times_real(A,B),B)=plus_plus_real(times_times_real(A,B),B).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1126,1130] {-} plus_plus_nat(times_times_nat(A,B),B)=plus_plus_nat(times_times_nat(A,B),B).
% 0.19/0.49 Following clause subsumed by 817 during input processing: 0 [demod,793,1160] {-} plus_plus_int(times_times_int(A,B),B)=plus_plus_int(B,times_times_int(A,B)).
% 0.19/0.49 Following clause subsumed by 749 during input processing: 0 [] {-} ord_less_eq_int(min,min).
% 0.19/0.49 Following c
% 0.19/0.49 -------- PROOF --------
% 0.19/0.49 % SZS status Theorem
% 0.19/0.49 % SZS output start Refutation
% 0.19/0.49 lause subsumed by 1194 during input processing: 0 [demod,845] {-} ord_less_int(min,pls).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1218] {-} minus_minus_int(times_times_int(number_number_of_int(A),B),times_times_int(number_number_of_int(A),C))=minus_minus_int(times_times_int(number_number_of_int(A),B),times_times_int(number_number_of_int(A),C)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1220] {-} minus_minus_int(times_times_int(A,number_number_of_int(C)),times_times_int(B,number_number_of_int(C)))=minus_minus_int(times_times_int(A,number_number_of_int(C)),times_times_int(B,number_number_of_int(C))).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,850,920,1223,1234,1193] {-} minus_minus_int(min,plus_plus_int(A,A))=minus_minus_int(min,plus_plus_int(A,A)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1037] {-} times_times_real(A,times_times_real(B,C))=times_times_real(A,times_times_real(B,C)).
% 0.19/0.49 Following clause subsumed by 1049 during input processing: 0 [] {-} times_times_real(A,B)=times_times_real(B,A).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1128] {-} A=A.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1124] {-} plus_plus_real(times_times_real(A,C),times_times_real(B,C))=plus_plus_real(times_times_real(A,C),times_times_real(B,C)).
% 0.19/0.49 Following clause subsumed by 1281 during input processing: 0 [flip.2] {-} A=zero_zero_nat|times_times_nat(B,power_power_nat(B,minus_minus_nat(A,one_one_nat)))=power_power_nat(B,A).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1137] {-} power_power_real(times_times_real(A,B),C)=power_power_real(times_times_real(A,B),C).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1140] {-} power_power_nat(times_times_nat(A,B),C)=power_power_nat(times_times_nat(A,B),C).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1143] {-} power_power_int(times_times_int(A,B),C)=power_power_int(times_times_int(A,B),C).
% 0.19/0.49 Following clause subsumed by 1049 during input processing: 0 [] {-} times_times_real(power_power_real(A,B),A)=times_times_real(A,power_power_real(A,B)).
% 0.19/0.49 Following clause subsumed by 1050 during input processing: 0 [] {-} times_times_nat(power_power_nat(A,B),A)=times_times_nat(A,power_power_nat(A,B)).
% 0.19/0.49 Following clause subsumed by 750 during input processing: 0 [] {-} times_times_int(power_power_int(A,B),A)=times_times_int(A,power_power_int(A,B)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1080] {-} A=A.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1082] {-} A=A.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1149] {-} one_one_real=one_one_real.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1151] {-} one_one_nat=one_one_nat.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1153] {-} one_one_int=one_one_int.
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1145] {-} power_power_real(A,plus_plus_nat(B,C))=power_power_real(A,plus_plus_nat(B,C)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,1147] {-} power_power_nat(A,plus_plus_nat(B,C))=power_power_nat(A,plus_plus_nat(B,C)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [demod,759] {-} power_power_int(A,plus_plus_nat(B,C))=power_power_int(A,plus_plus_nat(B,C)).
% 0.19/0.49 Following clause subsumed by 1114 during input processing: 0 [] {-} A=A.
% 0.19/0.49
% 0.19/0.49 ----> UNIT CONFLICT at 0.10 sec ----> 1329 [binary,1328.1,1324.1] {-} $F.
% 0.19/0.49
% 0.19/0.49 Length of proof is 12. Level of proof is 5.
% 0.19/0.49
% 0.19/0.49 ---------------- PROOF ----------------
% 0.19/0.49 % SZS status Theorem
% 0.19/0.49 % SZS output start Refutation
% 0.19/0.49
% 0.19/0.49 529 [] {-} -ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int).
% 0.19/0.49 710 [] {-} 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)).
% 0.19/0.49 711 [] {-} 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).
% 0.19/0.49 756,755 [] {-} times_times_int(times_times_int(A,B),C)=times_times_int(A,times_times_int(B,C)).
% 0.19/0.49 785,784 [] {-} times_times_int(pls,A)=pls.
% 0.19/0.49 789 [] {-} plus_plus_int(number_number_of_int(A),number_number_of_int(B))=number_number_of_int(plus_plus_int(A,B)).
% 0.19/0.49 791,790 [copy,789,flip.1] {-} number_number_of_int(plus_plus_int(A,B))=plus_plus_int(number_number_of_int(A),number_number_of_int(B)).
% 0.19/0.49 793,792 [] {-} times_times_int(plus_plus_int(A,B),C)=plus_plus_int(times_times_int(A,C),times_times_int(B,C)).
% 0.19/0.49 815,814 [] {-} plus_plus_int(plus_plus_int(A,B),C)=plus_plus_int(A,plus_plus_int(B,C)).
% 0.19/0.49 818 [] {-} zero_zero_int=number_number_of_int(pls).
% 0.19/0.49 820,819 [copy,818,flip.1] {-} number_number_of_int(pls)=zero_zero_int.
% 0.19/0.49 843 [] {-} pls=zero_zero_int.
% 0.19/0.49 845,844 [copy,843,flip.1] {-} zero_zero_int=pls.
% 0.19/0.49 850,849 [] {-} bit0(A)=plus_plus_int(A,A).
% 0.19/0.49 918 [] {-} bit1(A)=plus_plus_int(plus_plus_int(one_one_int,A),A).
% 0.19/0.49 920,919 [copy,918,demod,815] {-} bit1(A)=plus_plus_int(one_one_int,plus_plus_int(A,A)).
% 0.19/0.49 951 [] {-} number_number_of_int(bit1(pls))=one_one_int.
% 0.19/0.49 953,952 [copy,951,demod,920,791,791,820,845,820,845] {-} plus_plus_int(number_number_of_int(one_one_int),plus_plus_int(pls,pls))=one_one_int.
% 0.19/0.49 961 [] {-} plus_plus_nat(one_one_nat,one_one_nat)=number_number_of_nat(bit0(bit1(pls))).
% 0.19/0.49 963,962 [copy,961,demod,920,850,815,815,flip.1] {-} number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))=plus_plus_nat(one_one_nat,one_one_nat).
% 0.19/0.49 964 [] {-} plus_plus_int(one_one_int,one_one_int)=number_number_of_int(bit0(bit1(pls))).
% 0.19/0.49 966,965 [copy,964,demod,920,850,815,815,791,791,820,845,791,820,845,791,791,820,845,820,845,953,flip.1] {-} plus_plus_int(number_number_of_int(one_one_int),plus_plus_int(pls,plus_plus_int(pls,one_one_int)))=plus_plus_int(one_one_int,one_one_int).
% 0.19/0.49 1110 [] {-} times_times_int(A,zero_zero_int)=zero_zero_int.
% 0.19/0.49 1112,1111 [copy,1110,demod,845,845] {-} times_times_int(A,pls)=pls.
% 0.19/0.49 1158 [] {-} plus_plus_int(A,times_times_int(B,A))=times_times_int(plus_plus_int(B,one_one_int),A).
% 0.19/0.49 1160,1159 [copy,1158,demod,793,flip.1] {-} plus_plus_int(times_times_int(A,B),times_times_int(one_one_int,B))=plus_plus_int(B,times_times_int(A,B)).
% 0.19/0.49 1324 [back_demod,529,demod,920,850,815,815,963,845] {-} -ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),pls).
% 0.19/0.49 1327,1326 [back_demod,711,demod,920,850,815,815,963,920,850,815,815,850,815,815,815,815,815,791,791,820,845,791,820,845,791,791,820,845,791,820,845,791,791,820,845,791,820,845,791,791,820,845,820,845,953,966,793,793,785,793,785,793,793,785,793,785,793,1160,815,815,815,815,815,815,815,793,756,793,785,793,785,793,756,793,785,793,785,793,793,756,flip.1] {-} plus_plus_int(times_times_int(number_number_of_int(one_one_int),times_times_int(m,t)),plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(times_times_int(number_number_of_int(one_one_int),times_times_int(m,t)),plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(times_times_int(m,t),plus_plus_int(times_times_int(one_one_int,times_times_int(m,t)),times_times_int(one_one_int,t)))))))))=plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int).
% 0.19/0.49 1328 [back_demod,710,demod,920,850,815,815,850,815,815,815,815,815,791,791,820,845,791,820,845,791,791,820,845,791,820,845,791,791,820,845,791,820,845,791,791,820,845,820,845,953,966,793,793,785,793,785,793,793,785,793,785,793,1160,815,815,815,815,815,815,815,793,756,793,785,793,785,793,756,793,785,793,785,793,793,756,1327,920,850,815,815,850,815,815,815,815,815,791,791,820,845,791,820,845,791,791,820,845,791,820,845,791,791,820,845,791,820,845,791,791,820,845,820,845,953,966,793,793,785,793,785,793,793,785,793,785,793,1160,815,815,815,815,815,815,815,845,1112] {-} ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),pls).
% 0.19/0.49 1329 [binary,1328.1,1324.1] {-} $F.
% 0.19/0.49
% 0.19/0.49 % SZS output end Refutation
% 0.19/0.49 ------------ end of proof -------------
% 0.19/0.49
% 0.19/0.49
% 0.19/0.49 Search stopped by max_proofs option.
% 0.19/0.49
% 0.19/0.49
% 0.19/0.49 Search stopped by max_proofs option.
% 0.19/0.49
% 0.19/0.49 ============ end of search ============
% 0.19/0.49
% 0.19/0.49 That finishes the proof of the theorem.
% 0.19/0.49
% 0.19/0.49 Process 29002 finished Thu Jul 7 21:20:37 2022
%------------------------------------------------------------------------------