%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM924+6 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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 : Fri Oct 3 07:57:34 PM UTC 2025 % Result : Theorem 140.84s 141.00s % Output : Proof 141.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : NUM924+6 : TPTP v9.2.0. Released v5.3.0. % 0.07/0.12 % Command : duper %s % 0.12/0.33 % Computer : n023.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 07:03:53 EDT 2025 % 0.12/0.34 % CPUTime : % 140.84/141.00 SZS status Theorem for theBenchmark.p % 140.84/141.00 SZS output start Proof for theBenchmark.p % 140.84/141.00 Clause #39 (by assumption #[]): Eq (∀ (B_1_1 : Iota), Eq (ti int (bit0 B_1_1)) (bit0 B_1_1)) True % 140.84/141.00 Clause #40 (by assumption #[]): Eq (∀ (B_1_1 : Iota), Eq (bit1 (ti int B_1_1)) (bit1 B_1_1)) True % 140.84/141.00 Clause #41 (by assumption #[]): Eq (∀ (B_1_1 : Iota), Eq (ti int (bit1 B_1_1)) (bit1 B_1_1)) True % 140.84/141.00 Clause #42 (by assumption #[]): Eq (Eq (ti int min) min) True % 140.84/141.00 Clause #67 (by assumption #[]): Eq % 140.84/141.00 (ord_less int % 140.84/141.00 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.84/141.00 t) % 140.84/141.00 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.84/141.00 (zero_zero int))) % 140.84/141.00 True % 140.84/141.00 Clause #68 (by assumption #[]): Eq % 140.84/141.00 (Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 140.84/141.00 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.84/141.00 t)) % 140.84/141.00 True % 140.84/141.00 Clause #87 (by assumption #[]): Eq (∀ (K : Iota), Eq (number_number_of int K) (ti int K)) True % 140.84/141.00 Clause #88 (by assumption #[]): Eq (∀ (Z W : Iota), Eq (times_times int Z W) (times_times int W Z)) True % 140.84/141.00 Clause #124 (by assumption #[]): Eq (∀ (W : Iota), Eq (times_times int pls W) pls) True % 140.84/141.00 Clause #125 (by assumption #[]): Eq (∀ (K L : Iota), Eq (times_times int (bit0 K) L) (bit0 (times_times int K L))) True % 140.84/141.00 Clause #127 (by assumption #[]): Eq (∀ (Z : Iota), Eq (times_times int Z (one_one int)) (ti int Z)) True % 140.84/141.00 Clause #156 (by assumption #[]): Eq (∀ (Z W : Iota), Eq (plus_plus int Z W) (plus_plus int W Z)) True % 140.84/141.00 Clause #169 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 140.84/141.00 Clause #180 (by assumption #[]): Eq (Eq pls (zero_zero int)) True % 140.84/141.00 Clause #186 (by assumption #[]): Eq (∀ (K : Iota), Eq (plus_plus int pls K) (ti int K)) True % 140.84/141.00 Clause #216 (by assumption #[]): Eq (∀ (K L : Iota), Eq (plus_plus int (bit1 K) (bit0 L)) (bit1 (plus_plus int K L))) True % 140.84/141.00 Clause #381 (by assumption #[]): Eq % 140.84/141.00 (Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 140.84/141.00 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 140.84/141.00 True % 140.84/141.00 Clause #639 (by assumption #[]): Eq % 140.84/141.00 (Not % 140.84/141.00 (ord_less int (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 140.84/141.00 (zero_zero int))) % 140.84/141.00 True % 140.84/141.00 Clause #758 (by clausification #[180]): Eq pls (zero_zero int) % 140.84/141.00 Clause #799 (by clausification #[42]): Eq (ti int min) min % 140.84/141.00 Clause #852 (by clausification #[169]): Eq (one_one int) (number_number_of int (bit1 pls)) % 140.84/141.00 Clause #1007 (by clausification #[39]): ∀ (a : Iota), Eq (Eq (ti int (bit0 a)) (bit0 a)) True % 140.84/141.00 Clause #1008 (by clausification #[1007]): ∀ (a : Iota), Eq (ti int (bit0 a)) (bit0 a) % 140.84/141.00 Clause #1013 (by clausification #[40]): ∀ (a : Iota), Eq (Eq (bit1 (ti int a)) (bit1 a)) True % 140.84/141.00 Clause #1014 (by clausification #[1013]): ∀ (a : Iota), Eq (bit1 (ti int a)) (bit1 a) % 140.84/141.00 Clause #1024 (by clausification #[124]): ∀ (a : Iota), Eq (Eq (times_times int pls a) pls) True % 140.84/141.00 Clause #1025 (by clausification #[1024]): ∀ (a : Iota), Eq (times_times int pls a) pls % 140.84/141.00 Clause #1026 (by clausification #[41]): ∀ (a : Iota), Eq (Eq (ti int (bit1 a)) (bit1 a)) True % 140.84/141.00 Clause #1027 (by clausification #[1026]): ∀ (a : Iota), Eq (ti int (bit1 a)) (bit1 a) % 140.84/141.00 Clause #1223 (by clausification #[87]): ∀ (a : Iota), Eq (Eq (number_number_of int a) (ti int a)) True % 140.84/141.00 Clause #1224 (by clausification #[1223]): ∀ (a : Iota), Eq (number_number_of int a) (ti int a) % 140.84/141.00 Clause #1235 (by backward demodulation #[1224, 1014]): ∀ (a : Iota), Eq (bit1 (number_number_of int a)) (bit1 a) % 140.84/141.00 Clause #1244 (by superposition #[1224, 799]): Eq (number_number_of int min) min % 140.84/141.00 Clause #1246 (by superposition #[1224, 1008]): ∀ (a : Iota), Eq (number_number_of int (bit0 a)) (bit0 a) % 140.84/141.00 Clause #1247 (by superposition #[1224, 1027]): ∀ (a : Iota), Eq (number_number_of int (bit1 a)) (bit1 a) % 140.84/141.00 Clause #1277 (by superposition #[1247, 852]): Eq (one_one int) (bit1 pls) % 140.86/141.03 Clause #1336 (by forward demodulation #[67, 758]): Eq % 140.86/141.03 (ord_less int % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.86/141.03 t) % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.86/141.03 pls)) % 140.86/141.03 True % 140.86/141.03 Clause #1337 (by forward demodulation #[1336, 1277]): Eq % 140.86/141.03 (ord_less int % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.86/141.03 t) % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) % 140.86/141.03 pls)) % 140.86/141.03 True % 140.86/141.03 Clause #1338 (by forward demodulation #[1337, 1246]): Eq % 140.86/141.03 (ord_less int % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 140.86/141.03 t) % 140.86/141.03 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) pls)) % 140.86/141.03 True % 140.86/141.03 Clause #1339 (by forward demodulation #[1338, 1277]): Eq % 140.86/141.03 (ord_less int % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) t) % 140.86/141.03 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) pls)) % 140.86/141.03 True % 140.86/141.03 Clause #1340 (by forward demodulation #[1339, 1246]): Eq % 140.86/141.03 (ord_less int (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) t) % 140.86/141.03 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) pls)) % 140.86/141.03 True % 140.86/141.03 Clause #1341 (by clausification #[68]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 140.86/141.03 Clause #1342 (by forward demodulation #[1341, 1277]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 140.86/141.03 Clause #1343 (by forward demodulation #[1342, 1277]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.03 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) t) % 140.86/141.03 Clause #1344 (by forward demodulation #[1343, 1246]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.03 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) t) % 140.86/141.03 Clause #1345 (by backward demodulation #[1344, 1340]): Eq % 140.86/141.03 (ord_less int (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.03 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) pls)) % 140.86/141.03 True % 140.86/141.03 Clause #1573 (by clausification #[186]): ∀ (a : Iota), Eq (Eq (plus_plus int pls a) (ti int a)) True % 140.86/141.03 Clause #1574 (by clausification #[1573]): ∀ (a : Iota), Eq (plus_plus int pls a) (ti int a) % 140.86/141.03 Clause #1575 (by forward demodulation #[1574, 1224]): ∀ (a : Iota), Eq (plus_plus int pls a) (number_number_of int a) % 140.86/141.03 Clause #1700 (by clausification #[88]): ∀ (a : Iota), Eq (∀ (W : Iota), Eq (times_times int a W) (times_times int W a)) True % 140.86/141.03 Clause #1701 (by clausification #[1700]): ∀ (a a_1 : Iota), Eq (Eq (times_times int a a_1) (times_times int a_1 a)) True % 140.86/141.03 Clause #1702 (by clausification #[1701]): ∀ (a a_1 : Iota), Eq (times_times int a a_1) (times_times int a_1 a) % 140.86/141.03 Clause #1703 (by superposition #[1702, 1344]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.03 (times_times int t (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls))) % 140.86/141.03 Clause #1704 (by superposition #[1702, 1344]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.03 (times_times int (plus_plus int (times_times int m (bit0 (bit0 (bit1 pls)))) (bit1 pls)) t) % 140.86/141.03 Clause #1709 (by superposition #[1702, 1025]): ∀ (a : Iota), Eq (times_times int a pls) pls % 140.86/141.06 Clause #2578 (by clausification #[125]): ∀ (a : Iota), Eq (∀ (L : Iota), Eq (times_times int (bit0 a) L) (bit0 (times_times int a L))) True % 140.86/141.06 Clause #2579 (by clausification #[2578]): ∀ (a a_1 : Iota), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 140.86/141.06 Clause #2580 (by clausification #[2579]): ∀ (a a_1 : Iota), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 140.86/141.06 Clause #2596 (by superposition #[2580, 1702]): ∀ (a a_1 : Iota), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a_1 a)) % 140.86/141.06 Clause #2621 (by clausification #[127]): ∀ (a : Iota), Eq (Eq (times_times int a (one_one int)) (ti int a)) True % 140.86/141.06 Clause #2622 (by clausification #[2621]): ∀ (a : Iota), Eq (times_times int a (one_one int)) (ti int a) % 140.86/141.06 Clause #2623 (by forward demodulation #[2622, 1277]): ∀ (a : Iota), Eq (times_times int a (bit1 pls)) (ti int a) % 140.86/141.06 Clause #2624 (by forward demodulation #[2623, 1224]): ∀ (a : Iota), Eq (times_times int a (bit1 pls)) (number_number_of int a) % 140.86/141.06 Clause #3147 (by superposition #[2596, 2580]): ∀ (a a_1 : Iota), Eq (times_times int (bit0 a) a_1) (times_times int (bit0 a_1) a) % 140.86/141.06 Clause #3166 (by superposition #[3147, 2624]): ∀ (a : Iota), Eq (times_times int (bit0 (bit1 pls)) a) (number_number_of int (bit0 a)) % 140.86/141.06 Clause #3176 (by superposition #[3147, 1702]): ∀ (a a_1 : Iota), Eq (times_times int a (bit0 a_1)) (times_times int (bit0 a) a_1) % 140.86/141.06 Clause #3456 (by clausification #[156]): ∀ (a : Iota), Eq (∀ (W : Iota), Eq (plus_plus int a W) (plus_plus int W a)) True % 140.86/141.06 Clause #3457 (by clausification #[3456]): ∀ (a a_1 : Iota), Eq (Eq (plus_plus int a a_1) (plus_plus int a_1 a)) True % 140.86/141.06 Clause #3458 (by clausification #[3457]): ∀ (a a_1 : Iota), Eq (plus_plus int a a_1) (plus_plus int a_1 a) % 140.86/141.06 Clause #4408 (by clausification #[216]): ∀ (a : Iota), Eq (∀ (L : Iota), Eq (plus_plus int (bit1 a) (bit0 L)) (bit1 (plus_plus int a L))) True % 140.86/141.06 Clause #4409 (by clausification #[4408]): ∀ (a a_1 : Iota), Eq (Eq (plus_plus int (bit1 a) (bit0 a_1)) (bit1 (plus_plus int a a_1))) True % 140.86/141.06 Clause #4410 (by clausification #[4409]): ∀ (a a_1 : Iota), Eq (plus_plus int (bit1 a) (bit0 a_1)) (bit1 (plus_plus int a a_1)) % 140.86/141.06 Clause #5362 (by superposition #[3176, 1702]): ∀ (a a_1 : Iota), Eq (times_times int a (bit0 a_1)) (times_times int a_1 (bit0 a)) % 140.86/141.06 Clause #5500 (by forward demodulation #[3166, 1246]): ∀ (a : Iota), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 140.86/141.06 Clause #5516 (by superposition #[5500, 5362]): ∀ (a : Iota), Eq (times_times int a (bit0 (bit0 (bit1 pls)))) (bit0 (bit0 a)) % 140.86/141.06 Clause #9100 (by clausification #[381]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 140.86/141.06 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 140.86/141.06 Clause #9101 (by forward demodulation #[9100, 1244]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 140.86/141.06 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 140.86/141.06 Clause #9102 (by forward demodulation #[9101, 1277]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 140.86/141.06 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 140.86/141.06 Clause #13766 (by clausification #[639]): Eq % 140.86/141.06 (ord_less int (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 140.86/141.06 (zero_zero int)) % 140.86/141.06 False % 140.86/141.06 Clause #13767 (by forward demodulation #[13766, 758]): Eq (ord_less int (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) pls) False % 140.86/141.06 Clause #13768 (by forward demodulation #[13767, 3458]): Eq (ord_less int (plus_plus int (one_one int) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) pls) False % 140.86/141.06 Clause #13769 (by forward demodulation #[13768, 1277]): Eq (ord_less int (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) pls) False % 140.86/141.06 Clause #17126 (by forward demodulation #[1345, 1709]): Eq (ord_less int (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) pls) True % 141.03/141.25 Clause #17127 (by forward demodulation #[17126, 9102]): Eq (ord_less int (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) pls) True % 141.03/141.25 Clause #27122 (by forward demodulation #[1703, 9102]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls))) % 141.03/141.25 Clause #27123 (by forward demodulation #[27122, 3458]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (plus_plus int (bit1 pls) (times_times int (bit0 (bit0 (bit1 pls))) m))) % 141.03/141.25 Clause #27124 (by forward demodulation #[27123, 3176]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (plus_plus int (bit1 pls) (times_times int (bit0 (bit1 pls)) (bit0 m)))) % 141.03/141.25 Clause #27125 (by forward demodulation #[27124, 5362]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (plus_plus int (bit1 pls) (times_times int m (bit0 (bit0 (bit1 pls)))))) % 141.03/141.25 Clause #27126 (by forward demodulation #[27125, 5516]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (plus_plus int (bit1 pls) (bit0 (bit0 m)))) % 141.03/141.25 Clause #27127 (by forward demodulation #[27126, 4410]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (bit1 (plus_plus int pls (bit0 m)))) % 141.03/141.25 Clause #27128 (by forward demodulation #[27127, 1575]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (bit1 (number_number_of int (bit0 m)))) % 141.03/141.25 Clause #27129 (by forward demodulation #[27128, 1235]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 141.03/141.25 (times_times int t (bit1 (bit0 m))) % 141.03/141.25 Clause #27132 (by backward demodulation #[27129, 17127]): Eq (ord_less int (times_times int t (bit1 (bit0 m))) pls) True % 141.03/141.25 Clause #27166 (by forward demodulation #[1704, 3458]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int (plus_plus int (times_times int m (bit0 (bit0 (bit1 pls)))) (bit1 pls)) t) % 141.03/141.25 Clause #27167 (by forward demodulation #[27166, 3458]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int (plus_plus int (bit1 pls) (times_times int m (bit0 (bit0 (bit1 pls))))) t) % 141.03/141.25 Clause #27168 (by forward demodulation #[27167, 5516]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int (plus_plus int (bit1 pls) (bit0 (bit0 m))) t) % 141.03/141.25 Clause #27169 (by forward demodulation #[27168, 1702]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int t (plus_plus int (bit1 pls) (bit0 (bit0 m)))) % 141.03/141.25 Clause #27170 (by forward demodulation #[27169, 4410]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int t (bit1 (plus_plus int pls (bit0 m)))) % 141.03/141.25 Clause #27171 (by forward demodulation #[27170, 1575]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int t (bit1 (number_number_of int (bit0 m)))) % 141.03/141.25 Clause #27172 (by forward demodulation #[27171, 1235]): Eq (plus_plus int (bit1 pls) (power_power int s (number_number_of nat (bit0 (bit1 pls))))) % 141.03/141.25 (times_times int t (bit1 (bit0 m))) % 141.03/141.25 Clause #27173 (by backward demodulation #[27172, 13769]): Eq (ord_less int (times_times int t (bit1 (bit0 m))) pls) False % 141.03/141.25 Clause #29308 (by superposition #[27173, 27132]): Eq False True % 141.03/141.25 Clause #29325 (by clausification #[29308]): False % 141.03/141.25 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------