%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM951_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:39 PM UTC 2025 % Result : Theorem 80.33s 80.56s % Output : Proof 80.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM951_5 : TPTP v9.2.0. Released v6.0.0. % 0.12/0.14 % Command : duper %s % 0.13/0.35 % Computer : n031.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 07:46:53 EDT 2025 % 0.13/0.35 % CPUTime : % 80.33/80.56 SZS status Theorem for theBenchmark.p % 80.33/80.56 SZS output start Proof for theBenchmark.p % 80.33/80.56 Clause #6 (by assumption #[]): Eq (∀ (L : int), Eq (minus_minus int pls (bit1 L)) (bit1 (minus_minus int min L))) True % 80.33/80.56 Clause #7 (by assumption #[]): Eq (∀ (A : Type), number_ring A → Eq (number_number_of A (bit1 pls)) (one_one A)) True % 80.33/80.56 Clause #13 (by assumption #[]): Eq (∀ (L1 K1 : int), Iff (Eq (bit1 K1) (bit1 L1)) (Eq K1 L1)) True % 80.33/80.56 Clause #19 (by assumption #[]): Eq (∀ (K1 : int), Iff (Eq (bit0 K1) pls) (Eq K1 pls)) True % 80.33/80.56 Clause #21 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 80.33/80.56 Clause #26 (by assumption #[]): Eq (Eq (bit1 min) min) True % 80.33/80.56 Clause #31 (by assumption #[]): Eq % 80.33/80.56 (∀ (A : Type), % 80.33/80.56 number_ring A → % 80.33/80.56 ∀ (Z : A) (W V : int), % 80.33/80.56 Eq (plus_plus A (number_number_of A V) (plus_plus A (number_number_of A W) Z)) % 80.33/80.56 (plus_plus A (number_number_of A (plus_plus int V W)) Z)) % 80.33/80.56 True % 80.33/80.56 Clause #34 (by assumption #[]): Eq (∀ (L K : int), Eq (plus_plus int (bit1 K) (bit0 L)) (bit1 (plus_plus int K L))) True % 80.33/80.56 Clause #38 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of int K) K) True % 80.33/80.56 Clause #39 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int K pls) K) True % 80.33/80.56 Clause #40 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int pls K) K) True % 80.33/80.56 Clause #41 (by assumption #[]): Eq (∀ (K : int), Eq (bit0 K) (plus_plus int K K)) True % 80.33/80.56 Clause #42 (by assumption #[]): Eq (∀ (K : int), Eq (minus_minus int K pls) K) True % 80.33/80.56 Clause #48 (by assumption #[]): Eq (∀ (K : int), Eq (bit1 K) (plus_plus int (plus_plus int (one_one int) K) K)) True % 80.33/80.56 Clause #53 (by assumption #[]): Eq % 80.33/80.56 (∀ (A : Type), % 80.33/80.56 number_ring A → % 80.33/80.56 ∀ (C : A) (W V : int), % 80.33/80.56 Eq (plus_plus A (number_number_of A V) (minus_minus A (number_number_of A W) C)) % 80.33/80.56 (minus_minus A (number_number_of A (plus_plus int V W)) C)) % 80.33/80.56 True % 80.33/80.56 Clause #59 (by assumption #[]): Eq % 80.33/80.56 (∀ (A : Type), cancel_semigroup_add A → ∀ (C1 A2 B2 : A), Iff (Eq (plus_plus A B2 A2) (plus_plus A C1 A2)) (Eq B2 C1)) % 80.33/80.56 True % 80.33/80.56 Clause #65 (by assumption #[]): Eq (∀ (L K : int), Eq (times_times int (bit0 K) L) (bit0 (times_times int K L))) True % 80.33/80.56 Clause #72 (by assumption #[]): Eq (∀ (L K : int), Eq (times_times int (bit1 K) L) (plus_plus int (bit0 (times_times int K L)) L)) True % 80.33/80.56 Clause #75 (by assumption #[]): Eq (∀ (A : Type), comm_monoid_mult A → ∀ (A1 : A), Eq (times_times A A1 (one_one A)) A1) True % 80.33/80.56 Clause #77 (by assumption #[]): Eq (∀ (A : Type), comm_monoid_mult A → ∀ (A1 : A), Eq (times_times A (one_one A) A1) A1) True % 80.33/80.56 Clause #85 (by assumption #[]): Eq % 80.33/80.56 (∀ (W Z2 Z1 : int), % 80.33/80.56 Eq (times_times int (plus_plus int Z1 Z2) W) (plus_plus int (times_times int Z1 W) (times_times int Z2 W))) % 80.33/80.56 True % 80.33/80.56 Clause #86 (by assumption #[]): Eq % 80.33/80.56 (∀ (Z2 Z1 W : int), % 80.33/80.56 Eq (times_times int W (minus_minus int Z1 Z2)) (minus_minus int (times_times int W Z1) (times_times int W Z2))) % 80.33/80.56 True % 80.33/80.56 Clause #91 (by assumption #[]): Eq % 80.33/80.56 (∀ (N1 Ma : int), % 80.33/80.56 Iff (Eq (times_times int Ma N1) (one_one int)) % 80.33/80.56 (Or (And (Eq Ma (one_one int)) (Eq N1 (one_one int))) % 80.33/80.56 (And (Eq Ma (number_number_of int min)) (Eq N1 (number_number_of int min))))) % 80.33/80.56 True % 80.33/80.56 Clause #97 (by assumption #[]): Eq (cancel_semigroup_add int) True % 80.33/80.56 Clause #99 (by assumption #[]): Eq (comm_monoid_mult int) True % 80.33/80.56 Clause #105 (by assumption #[]): Eq (number_ring int) True % 80.33/80.56 Clause #123 (by assumption #[]): Eq % 80.33/80.56 (Not % 80.33/80.56 (Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 80.33/80.56 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)))) % 80.33/80.56 True % 80.33/80.56 Clause #148 (by clausification #[26]): Eq (bit1 min) min % 80.33/80.56 Clause #151 (by clausification #[21]): Eq (bit0 pls) pls % 80.33/80.56 Clause #160 (by clausification #[6]): ∀ (a : int), Eq (Eq (minus_minus int pls (bit1 a)) (bit1 (minus_minus int min a))) True % 80.33/80.56 Clause #161 (by clausification #[160]): ∀ (a : int), Eq (minus_minus int pls (bit1 a)) (bit1 (minus_minus int min a)) % 80.33/80.56 Clause #172 (by clausification #[7]): ∀ (a : Type), Eq (number_ring a → Eq (number_number_of a (bit1 pls)) (one_one a)) True % 80.33/80.59 Clause #173 (by clausification #[172]): ∀ (a : Type), Or (Eq (number_ring a) False) (Eq (Eq (number_number_of a (bit1 pls)) (one_one a)) True) % 80.33/80.59 Clause #174 (by clausification #[173]): ∀ (a : Type), Or (Eq (number_ring a) False) (Eq (number_number_of a (bit1 pls)) (one_one a)) % 80.33/80.59 Clause #175 (by superposition #[174, 105]): Or (Eq (number_number_of int (bit1 pls)) (one_one int)) (Eq False True) % 80.33/80.59 Clause #178 (by clausification #[175]): Eq (number_number_of int (bit1 pls)) (one_one int) % 80.33/80.59 Clause #179 (by clausification #[38]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 80.33/80.59 Clause #180 (by clausification #[179]): ∀ (a : int), Eq (number_number_of int a) a % 80.33/80.59 Clause #181 (by superposition #[180, 178]): Eq (bit1 pls) (one_one int) % 80.33/80.59 Clause #190 (by clausification #[39]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 80.33/80.59 Clause #191 (by clausification #[190]): ∀ (a : int), Eq (plus_plus int a pls) a % 80.33/80.59 Clause #222 (by clausification #[42]): ∀ (a : int), Eq (Eq (minus_minus int a pls) a) True % 80.33/80.59 Clause #223 (by clausification #[222]): ∀ (a : int), Eq (minus_minus int a pls) a % 80.33/80.59 Clause #226 (by superposition #[223, 161]): Eq (minus_minus int pls (bit1 pls)) (bit1 min) % 80.33/80.59 Clause #230 (by forward demodulation #[226, 148]): Eq (minus_minus int pls (bit1 pls)) min % 80.33/80.59 Clause #269 (by clausification #[13]): ∀ (a : int), Eq (∀ (K1 : int), Iff (Eq (bit1 K1) (bit1 a)) (Eq K1 a)) True % 80.33/80.59 Clause #270 (by clausification #[269]): ∀ (a a_1 : int), Eq (Iff (Eq (bit1 a) (bit1 a_1)) (Eq a a_1)) True % 80.33/80.59 Clause #272 (by clausification #[270]): ∀ (a a_1 : int), Or (Eq (Eq (bit1 a) (bit1 a_1)) False) (Eq (Eq a a_1) True) % 80.33/80.59 Clause #330 (by clausification #[19]): ∀ (a : int), Eq (Iff (Eq (bit0 a) pls) (Eq a pls)) True % 80.33/80.59 Clause #332 (by clausification #[330]): ∀ (a : int), Or (Eq (Eq (bit0 a) pls) False) (Eq (Eq a pls) True) % 80.33/80.59 Clause #366 (by clausification #[40]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 80.33/80.59 Clause #367 (by clausification #[366]): ∀ (a : int), Eq (plus_plus int pls a) a % 80.33/80.59 Clause #427 (by clausification #[31]): ∀ (a : Type), % 80.33/80.59 Eq % 80.33/80.59 (number_ring a → % 80.33/80.59 ∀ (Z : a) (W V : int), % 80.33/80.59 Eq (plus_plus a (number_number_of a V) (plus_plus a (number_number_of a W) Z)) % 80.33/80.59 (plus_plus a (number_number_of a (plus_plus int V W)) Z)) % 80.33/80.59 True % 80.33/80.59 Clause #428 (by clausification #[427]): ∀ (a : Type), % 80.33/80.59 Or (Eq (number_ring a) False) % 80.33/80.59 (Eq % 80.33/80.59 (∀ (Z : a) (W V : int), % 80.33/80.59 Eq (plus_plus a (number_number_of a V) (plus_plus a (number_number_of a W) Z)) % 80.33/80.59 (plus_plus a (number_number_of a (plus_plus int V W)) Z)) % 80.33/80.59 True) % 80.33/80.59 Clause #429 (by clausification #[428]): ∀ (a : Type) (a_1 : a), % 80.33/80.59 Or (Eq (number_ring a) False) % 80.33/80.59 (Eq % 80.33/80.59 (∀ (W V : int), % 80.33/80.59 Eq (plus_plus a (number_number_of a V) (plus_plus a (number_number_of a W) a_1)) % 80.33/80.59 (plus_plus a (number_number_of a (plus_plus int V W)) a_1)) % 80.33/80.59 True) % 80.33/80.59 Clause #430 (by clausification #[429]): ∀ (a : Type) (a_1 : int) (a_2 : a), % 80.33/80.59 Or (Eq (number_ring a) False) % 80.33/80.59 (Eq % 80.33/80.59 (∀ (V : int), % 80.33/80.59 Eq (plus_plus a (number_number_of a V) (plus_plus a (number_number_of a a_1) a_2)) % 80.33/80.59 (plus_plus a (number_number_of a (plus_plus int V a_1)) a_2)) % 80.33/80.59 True) % 80.33/80.59 Clause #431 (by clausification #[430]): ∀ (a : Type) (a_1 a_2 : int) (a_3 : a), % 80.33/80.59 Or (Eq (number_ring a) False) % 80.33/80.59 (Eq % 80.33/80.59 (Eq (plus_plus a (number_number_of a a_1) (plus_plus a (number_number_of a a_2) a_3)) % 80.33/80.59 (plus_plus a (number_number_of a (plus_plus int a_1 a_2)) a_3)) % 80.33/80.59 True) % 80.33/80.59 Clause #432 (by clausification #[431]): ∀ (a : Type) (a_1 a_2 : int) (a_3 : a), % 80.33/80.59 Or (Eq (number_ring a) False) % 80.33/80.59 (Eq (plus_plus a (number_number_of a a_1) (plus_plus a (number_number_of a a_2) a_3)) % 80.33/80.59 (plus_plus a (number_number_of a (plus_plus int a_1 a_2)) a_3)) % 80.33/80.59 Clause #433 (by superposition #[432, 105]): ∀ (a a_1 a_2 : int), % 80.33/80.59 Or % 80.33/80.59 (Eq (plus_plus int (number_number_of int a) (plus_plus int (number_number_of int a_1) a_2)) % 80.33/80.59 (plus_plus int (number_number_of int (plus_plus int a a_1)) a_2)) % 80.33/80.59 (Eq False True) % 80.33/80.59 Clause #455 (by clausification #[34]): ∀ (a : int), Eq (∀ (K : int), Eq (plus_plus int (bit1 K) (bit0 a)) (bit1 (plus_plus int K a))) True % 80.42/80.61 Clause #456 (by clausification #[455]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit1 a) (bit0 a_1)) (bit1 (plus_plus int a a_1))) True % 80.42/80.61 Clause #457 (by clausification #[456]): ∀ (a a_1 : int), Eq (plus_plus int (bit1 a) (bit0 a_1)) (bit1 (plus_plus int a a_1)) % 80.42/80.61 Clause #462 (by superposition #[457, 148]): ∀ (a : int), Eq (plus_plus int min (bit0 a)) (bit1 (plus_plus int min a)) % 80.42/80.61 Clause #508 (by clausification #[41]): ∀ (a : int), Eq (Eq (bit0 a) (plus_plus int a a)) True % 80.42/80.61 Clause #509 (by clausification #[508]): ∀ (a : int), Eq (bit0 a) (plus_plus int a a) % 80.42/80.61 Clause #603 (by clausification #[48]): ∀ (a : int), Eq (Eq (bit1 a) (plus_plus int (plus_plus int (one_one int) a) a)) True % 80.42/80.61 Clause #604 (by clausification #[603]): ∀ (a : int), Eq (bit1 a) (plus_plus int (plus_plus int (one_one int) a) a) % 80.42/80.61 Clause #605 (by forward demodulation #[604, 181]): ∀ (a : int), Eq (bit1 a) (plus_plus int (plus_plus int (bit1 pls) a) a) % 80.42/80.61 Clause #649 (by clausification #[53]): ∀ (a : Type), % 80.42/80.61 Eq % 80.42/80.61 (number_ring a → % 80.42/80.61 ∀ (C : a) (W V : int), % 80.42/80.61 Eq (plus_plus a (number_number_of a V) (minus_minus a (number_number_of a W) C)) % 80.42/80.61 (minus_minus a (number_number_of a (plus_plus int V W)) C)) % 80.42/80.61 True % 80.42/80.61 Clause #650 (by clausification #[649]): ∀ (a : Type), % 80.42/80.61 Or (Eq (number_ring a) False) % 80.42/80.61 (Eq % 80.42/80.61 (∀ (C : a) (W V : int), % 80.42/80.61 Eq (plus_plus a (number_number_of a V) (minus_minus a (number_number_of a W) C)) % 80.42/80.61 (minus_minus a (number_number_of a (plus_plus int V W)) C)) % 80.42/80.61 True) % 80.42/80.61 Clause #651 (by clausification #[650]): ∀ (a : Type) (a_1 : a), % 80.42/80.61 Or (Eq (number_ring a) False) % 80.42/80.61 (Eq % 80.42/80.61 (∀ (W V : int), % 80.42/80.61 Eq (plus_plus a (number_number_of a V) (minus_minus a (number_number_of a W) a_1)) % 80.42/80.61 (minus_minus a (number_number_of a (plus_plus int V W)) a_1)) % 80.42/80.61 True) % 80.42/80.61 Clause #652 (by clausification #[651]): ∀ (a : Type) (a_1 : int) (a_2 : a), % 80.42/80.61 Or (Eq (number_ring a) False) % 80.42/80.61 (Eq % 80.42/80.61 (∀ (V : int), % 80.42/80.61 Eq (plus_plus a (number_number_of a V) (minus_minus a (number_number_of a a_1) a_2)) % 80.42/80.61 (minus_minus a (number_number_of a (plus_plus int V a_1)) a_2)) % 80.42/80.61 True) % 80.42/80.61 Clause #653 (by clausification #[652]): ∀ (a : Type) (a_1 a_2 : int) (a_3 : a), % 80.42/80.61 Or (Eq (number_ring a) False) % 80.42/80.61 (Eq % 80.42/80.61 (Eq (plus_plus a (number_number_of a a_1) (minus_minus a (number_number_of a a_2) a_3)) % 80.42/80.61 (minus_minus a (number_number_of a (plus_plus int a_1 a_2)) a_3)) % 80.42/80.61 True) % 80.42/80.61 Clause #654 (by clausification #[653]): ∀ (a : Type) (a_1 a_2 : int) (a_3 : a), % 80.42/80.61 Or (Eq (number_ring a) False) % 80.42/80.61 (Eq (plus_plus a (number_number_of a a_1) (minus_minus a (number_number_of a a_2) a_3)) % 80.42/80.61 (minus_minus a (number_number_of a (plus_plus int a_1 a_2)) a_3)) % 80.42/80.61 Clause #655 (by superposition #[654, 105]): ∀ (a a_1 a_2 : int), % 80.42/80.61 Or % 80.42/80.61 (Eq (plus_plus int (number_number_of int a) (minus_minus int (number_number_of int a_1) a_2)) % 80.42/80.61 (minus_minus int (number_number_of int (plus_plus int a a_1)) a_2)) % 80.42/80.61 (Eq False True) % 80.42/80.61 Clause #736 (by clausification #[59]): ∀ (a : Type), % 80.42/80.61 Eq (cancel_semigroup_add a → ∀ (C1 A2 B2 : a), Iff (Eq (plus_plus a B2 A2) (plus_plus a C1 A2)) (Eq B2 C1)) True % 80.42/80.61 Clause #737 (by clausification #[736]): ∀ (a : Type), % 80.42/80.61 Or (Eq (cancel_semigroup_add a) False) % 80.42/80.61 (Eq (∀ (C1 A2 B2 : a), Iff (Eq (plus_plus a B2 A2) (plus_plus a C1 A2)) (Eq B2 C1)) True) % 80.42/80.61 Clause #738 (by clausification #[737]): ∀ (a : Type) (a_1 : a), % 80.42/80.61 Or (Eq (cancel_semigroup_add a) False) % 80.42/80.61 (Eq (∀ (A2 B2 : a), Iff (Eq (plus_plus a B2 A2) (plus_plus a a_1 A2)) (Eq B2 a_1)) True) % 80.42/80.61 Clause #739 (by clausification #[738]): ∀ (a : Type) (a_1 a_2 : a), % 80.42/80.61 Or (Eq (cancel_semigroup_add a) False) % 80.42/80.61 (Eq (∀ (B2 : a), Iff (Eq (plus_plus a B2 a_1) (plus_plus a a_2 a_1)) (Eq B2 a_2)) True) % 80.42/80.61 Clause #740 (by clausification #[739]): ∀ (a : Type) (a_1 a_2 a_3 : a), % 80.42/80.61 Or (Eq (cancel_semigroup_add a) False) (Eq (Iff (Eq (plus_plus a a_1 a_2) (plus_plus a a_3 a_2)) (Eq a_1 a_3)) True) % 80.42/80.61 Clause #742 (by clausification #[740]): ∀ (a : Type) (a_1 a_2 a_3 : a), % 80.42/80.64 Or (Eq (cancel_semigroup_add a) False) % 80.42/80.64 (Or (Eq (Eq (plus_plus a a_1 a_2) (plus_plus a a_3 a_2)) False) (Eq (Eq a_1 a_3) True)) % 80.42/80.64 Clause #877 (by clausification #[65]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit0 K) a) (bit0 (times_times int K a))) True % 80.42/80.64 Clause #878 (by clausification #[877]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 80.42/80.64 Clause #879 (by clausification #[878]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 80.42/80.64 Clause #1070 (by clausification #[72]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit1 K) a) (plus_plus int (bit0 (times_times int K a)) a)) True % 80.42/80.64 Clause #1071 (by clausification #[1070]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1)) True % 80.42/80.64 Clause #1072 (by clausification #[1071]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 80.42/80.64 Clause #1073 (by forward demodulation #[1072, 879]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (times_times int (bit0 a) a_1) a_1) % 80.42/80.64 Clause #1075 (by superposition #[1073, 191]): ∀ (a : int), Eq (times_times int (bit1 a) pls) (times_times int (bit0 a) pls) % 80.42/80.64 Clause #1135 (by clausification #[75]): ∀ (a : Type), Eq (comm_monoid_mult a → ∀ (A1 : a), Eq (times_times a A1 (one_one a)) A1) True % 80.42/80.64 Clause #1136 (by clausification #[1135]): ∀ (a : Type), Or (Eq (comm_monoid_mult a) False) (Eq (∀ (A1 : a), Eq (times_times a A1 (one_one a)) A1) True) % 80.42/80.64 Clause #1137 (by clausification #[1136]): ∀ (a : Type) (a_1 : a), Or (Eq (comm_monoid_mult a) False) (Eq (Eq (times_times a a_1 (one_one a)) a_1) True) % 80.42/80.64 Clause #1138 (by clausification #[1137]): ∀ (a : Type) (a_1 : a), Or (Eq (comm_monoid_mult a) False) (Eq (times_times a a_1 (one_one a)) a_1) % 80.42/80.64 Clause #1140 (by superposition #[1138, 99]): ∀ (a : int), Or (Eq (times_times int a (one_one int)) a) (Eq False True) % 80.42/80.64 Clause #1141 (by clausification #[1140]): ∀ (a : int), Eq (times_times int a (one_one int)) a % 80.42/80.64 Clause #1142 (by forward demodulation #[1141, 181]): ∀ (a : int), Eq (times_times int a (bit1 pls)) a % 80.42/80.64 Clause #1180 (by clausification #[77]): ∀ (a : Type), Eq (comm_monoid_mult a → ∀ (A1 : a), Eq (times_times a (one_one a) A1) A1) True % 80.42/80.64 Clause #1181 (by clausification #[1180]): ∀ (a : Type), Or (Eq (comm_monoid_mult a) False) (Eq (∀ (A1 : a), Eq (times_times a (one_one a) A1) A1) True) % 80.42/80.64 Clause #1182 (by clausification #[1181]): ∀ (a : Type) (a_1 : a), Or (Eq (comm_monoid_mult a) False) (Eq (Eq (times_times a (one_one a) a_1) a_1) True) % 80.42/80.64 Clause #1183 (by clausification #[1182]): ∀ (a : Type) (a_1 : a), Or (Eq (comm_monoid_mult a) False) (Eq (times_times a (one_one a) a_1) a_1) % 80.42/80.64 Clause #1185 (by superposition #[1183, 99]): ∀ (a : int), Or (Eq (times_times int (one_one int) a) a) (Eq False True) % 80.42/80.64 Clause #1194 (by clausification #[1185]): ∀ (a : int), Eq (times_times int (one_one int) a) a % 80.42/80.64 Clause #1195 (by forward demodulation #[1194, 181]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 80.42/80.64 Clause #1196 (by superposition #[1195, 879]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 80.42/80.64 Clause #1197 (by superposition #[1196, 1075]): Eq (times_times int (bit1 (bit1 pls)) pls) (bit0 pls) % 80.42/80.64 Clause #1199 (by superposition #[1196, 879]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 80.42/80.64 Clause #1204 (by forward demodulation #[1197, 151]): Eq (times_times int (bit1 (bit1 pls)) pls) pls % 80.42/80.64 Clause #1341 (by clausification #[85]): ∀ (a : int), % 80.42/80.64 Eq % 80.42/80.64 (∀ (Z2 Z1 : int), % 80.42/80.64 Eq (times_times int (plus_plus int Z1 Z2) a) (plus_plus int (times_times int Z1 a) (times_times int Z2 a))) % 80.42/80.64 True % 80.42/80.64 Clause #1342 (by clausification #[1341]): ∀ (a a_1 : int), % 80.42/80.64 Eq % 80.42/80.64 (∀ (Z1 : int), % 80.42/80.64 Eq (times_times int (plus_plus int Z1 a) a_1) (plus_plus int (times_times int Z1 a_1) (times_times int a a_1))) % 80.42/80.64 True % 80.42/80.64 Clause #1343 (by clausification #[1342]): ∀ (a a_1 a_2 : int), % 80.42/80.64 Eq (Eq (times_times int (plus_plus int a a_1) a_2) (plus_plus int (times_times int a a_2) (times_times int a_1 a_2))) % 80.42/80.66 True % 80.42/80.66 Clause #1344 (by clausification #[1343]): ∀ (a a_1 a_2 : int), % 80.42/80.66 Eq (times_times int (plus_plus int a a_1) a_2) (plus_plus int (times_times int a a_2) (times_times int a_1 a_2)) % 80.42/80.66 Clause #1348 (by superposition #[1344, 1204]): ∀ (a : int), Eq (times_times int (plus_plus int a (bit1 (bit1 pls))) pls) (plus_plus int (times_times int a pls) pls) % 80.42/80.66 Clause #1385 (by clausification #[86]): ∀ (a : int), % 80.42/80.66 Eq % 80.42/80.66 (∀ (Z1 W : int), % 80.42/80.66 Eq (times_times int W (minus_minus int Z1 a)) (minus_minus int (times_times int W Z1) (times_times int W a))) % 80.42/80.66 True % 80.42/80.66 Clause #1386 (by clausification #[1385]): ∀ (a a_1 : int), % 80.42/80.66 Eq % 80.42/80.66 (∀ (W : int), % 80.42/80.66 Eq (times_times int W (minus_minus int a a_1)) (minus_minus int (times_times int W a) (times_times int W a_1))) % 80.42/80.66 True % 80.42/80.66 Clause #1387 (by clausification #[1386]): ∀ (a a_1 a_2 : int), % 80.42/80.66 Eq % 80.42/80.66 (Eq (times_times int a (minus_minus int a_1 a_2)) (minus_minus int (times_times int a a_1) (times_times int a a_2))) % 80.42/80.66 True % 80.42/80.66 Clause #1388 (by clausification #[1387]): ∀ (a a_1 a_2 : int), % 80.42/80.66 Eq (times_times int a (minus_minus int a_1 a_2)) (minus_minus int (times_times int a a_1) (times_times int a a_2)) % 80.42/80.66 Clause #1393 (by superposition #[1388, 1142]): ∀ (a a_1 : int), Eq (times_times int a (minus_minus int a_1 (bit1 pls))) (minus_minus int (times_times int a a_1) a) % 80.42/80.66 Clause #1411 (by superposition #[1199, 1075]): Eq (times_times int (bit1 (bit0 (bit1 pls))) pls) (bit0 (bit0 pls)) % 80.42/80.66 Clause #1470 (by forward demodulation #[1411, 151]): Eq (times_times int (bit1 (bit0 (bit1 pls))) pls) (bit0 pls) % 80.42/80.66 Clause #1471 (by forward demodulation #[1470, 151]): Eq (times_times int (bit1 (bit0 (bit1 pls))) pls) pls % 80.42/80.66 Clause #1536 (by clausification #[91]): ∀ (a : int), % 80.42/80.66 Eq % 80.42/80.66 (∀ (Ma : int), % 80.42/80.66 Iff (Eq (times_times int Ma a) (one_one int)) % 80.42/80.66 (Or (And (Eq Ma (one_one int)) (Eq a (one_one int))) % 80.42/80.66 (And (Eq Ma (number_number_of int min)) (Eq a (number_number_of int min))))) % 80.42/80.66 True % 80.42/80.66 Clause #1537 (by clausification #[1536]): ∀ (a a_1 : int), % 80.42/80.66 Eq % 80.42/80.66 (Iff (Eq (times_times int a a_1) (one_one int)) % 80.42/80.66 (Or (And (Eq a (one_one int)) (Eq a_1 (one_one int))) % 80.42/80.66 (And (Eq a (number_number_of int min)) (Eq a_1 (number_number_of int min))))) % 80.42/80.66 True % 80.42/80.66 Clause #1538 (by clausification #[1537]): ∀ (a a_1 : int), % 80.42/80.66 Or (Eq (Eq (times_times int a a_1) (one_one int)) True) % 80.42/80.66 (Eq % 80.42/80.66 (Or (And (Eq a (one_one int)) (Eq a_1 (one_one int))) % 80.42/80.66 (And (Eq a (number_number_of int min)) (Eq a_1 (number_number_of int min)))) % 80.42/80.66 False) % 80.42/80.66 Clause #1540 (by clausification #[1538]): ∀ (a a_1 : int), % 80.42/80.66 Or % 80.42/80.66 (Eq % 80.42/80.66 (Or (And (Eq a (one_one int)) (Eq a_1 (one_one int))) % 80.42/80.66 (And (Eq a (number_number_of int min)) (Eq a_1 (number_number_of int min)))) % 80.42/80.66 False) % 80.42/80.66 (Eq (times_times int a a_1) (one_one int)) % 80.42/80.66 Clause #1541 (by clausification #[1540]): ∀ (a a_1 : int), % 80.42/80.66 Or (Eq (times_times int a a_1) (one_one int)) % 80.42/80.66 (Eq (And (Eq a (number_number_of int min)) (Eq a_1 (number_number_of int min))) False) % 80.42/80.66 Clause #1543 (by clausification #[1541]): ∀ (a a_1 : int), % 80.42/80.66 Or (Eq (times_times int a a_1) (one_one int)) % 80.42/80.66 (Or (Eq (Eq a (number_number_of int min)) False) (Eq (Eq a_1 (number_number_of int min)) False)) % 80.42/80.66 Clause #1544 (by clausification #[1543]): ∀ (a a_1 : int), % 80.42/80.66 Or (Eq (times_times int a a_1) (one_one int)) % 80.42/80.66 (Or (Eq (Eq a_1 (number_number_of int min)) False) (Ne a (number_number_of int min))) % 80.42/80.66 Clause #1545 (by clausification #[1544]): ∀ (a a_1 : int), % 80.42/80.66 Or (Eq (times_times int a a_1) (one_one int)) % 80.42/80.66 (Or (Ne a (number_number_of int min)) (Ne a_1 (number_number_of int min))) % 80.42/80.66 Clause #1546 (by destructive equality resolution #[1545]): ∀ (a : int), Or (Eq (times_times int (number_number_of int min) a) (one_one int)) (Ne a (number_number_of int min)) % 80.42/80.66 Clause #1547 (by destructive equality resolution #[1546]): Eq (times_times int (number_number_of int min) (number_number_of int min)) (one_one int) % 80.42/80.66 Clause #1548 (by forward demodulation #[1547, 180]): Eq (times_times int (number_number_of int min) min) (one_one int) % 80.42/80.66 Clause #1549 (by forward demodulation #[1548, 180]): Eq (times_times int min min) (one_one int) % 80.51/80.69 Clause #1550 (by forward demodulation #[1549, 181]): Eq (times_times int min min) (bit1 pls) % 80.51/80.69 Clause #1687 (by clausification #[123]): Eq % 80.51/80.69 (Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 80.51/80.69 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 80.51/80.69 False % 80.51/80.69 Clause #1688 (by clausification #[1687]): Ne (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 80.51/80.69 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 80.51/80.69 Clause #1689 (by forward demodulation #[1688, 180]): Ne (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 80.51/80.69 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 80.51/80.69 Clause #1690 (by forward demodulation #[1689, 181]): Ne (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 80.51/80.69 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 80.51/80.69 Clause #1978 (by clausification #[332]): ∀ (a : int), Or (Eq (Eq a pls) True) (Ne (bit0 a) pls) % 80.51/80.69 Clause #1979 (by clausification #[1978]): ∀ (a : int), Or (Ne (bit0 a) pls) (Eq a pls) % 80.51/80.69 Clause #1983 (by superposition #[1979, 879]): ∀ (a a_1 : int), Or (Ne (times_times int (bit0 a) a_1) pls) (Eq (times_times int a a_1) pls) % 80.51/80.69 Clause #1984 (by superposition #[1983, 1075]): ∀ (a : int), Or (Ne (times_times int (bit1 a) pls) pls) (Eq (times_times int a pls) pls) % 80.51/80.69 Clause #2021 (by superposition #[1984, 1471]): Or (Ne pls pls) (Eq (times_times int (bit0 (bit1 pls)) pls) pls) % 80.51/80.69 Clause #2028 (by eliminate resolved literals #[2021]): Eq (times_times int (bit0 (bit1 pls)) pls) pls % 80.51/80.69 Clause #2230 (by clausification #[272]): ∀ (a a_1 : int), Or (Eq (Eq a a_1) True) (Ne (bit1 a) (bit1 a_1)) % 80.51/80.69 Clause #2231 (by clausification #[2230]): ∀ (a a_1 : int), Or (Ne (bit1 a) (bit1 a_1)) (Eq a a_1) % 80.51/80.69 Clause #2240 (by superposition #[2231, 462]): ∀ (a a_1 : int), Or (Ne (bit1 a) (plus_plus int min (bit0 a_1))) (Eq a (plus_plus int min a_1)) % 80.51/80.69 Clause #2865 (by clausification #[433]): ∀ (a a_1 a_2 : int), % 80.51/80.69 Eq (plus_plus int (number_number_of int a) (plus_plus int (number_number_of int a_1) a_2)) % 80.51/80.69 (plus_plus int (number_number_of int (plus_plus int a a_1)) a_2) % 80.51/80.69 Clause #2866 (by forward demodulation #[2865, 180]): ∀ (a a_1 a_2 : int), % 80.51/80.69 Eq (plus_plus int (number_number_of int a) (plus_plus int a_1 a_2)) % 80.51/80.69 (plus_plus int (number_number_of int (plus_plus int a a_1)) a_2) % 80.51/80.69 Clause #2867 (by forward demodulation #[2866, 180]): ∀ (a a_1 a_2 : int), % 80.51/80.69 Eq (plus_plus int a (plus_plus int a_1 a_2)) (plus_plus int (number_number_of int (plus_plus int a a_1)) a_2) % 80.51/80.69 Clause #2868 (by forward demodulation #[2867, 180]): ∀ (a a_1 a_2 : int), Eq (plus_plus int a (plus_plus int a_1 a_2)) (plus_plus int (plus_plus int a a_1) a_2) % 80.51/80.69 Clause #2871 (by superposition #[2868, 605]): ∀ (a : int), Eq (bit1 a) (plus_plus int (bit1 pls) (plus_plus int a a)) % 80.51/80.69 Clause #2900 (by forward demodulation #[2871, 509]): ∀ (a : int), Eq (bit1 a) (plus_plus int (bit1 pls) (bit0 a)) % 80.51/80.69 Clause #4214 (by clausification #[655]): ∀ (a a_1 a_2 : int), % 80.51/80.69 Eq (plus_plus int (number_number_of int a) (minus_minus int (number_number_of int a_1) a_2)) % 80.51/80.69 (minus_minus int (number_number_of int (plus_plus int a a_1)) a_2) % 80.51/80.69 Clause #4215 (by forward demodulation #[4214, 180]): ∀ (a a_1 a_2 : int), % 80.51/80.69 Eq (plus_plus int (number_number_of int a) (minus_minus int a_1 a_2)) % 80.51/80.69 (minus_minus int (number_number_of int (plus_plus int a a_1)) a_2) % 80.51/80.69 Clause #4216 (by forward demodulation #[4215, 180]): ∀ (a a_1 a_2 : int), % 80.51/80.69 Eq (plus_plus int a (minus_minus int a_1 a_2)) (minus_minus int (number_number_of int (plus_plus int a a_1)) a_2) % 80.51/80.69 Clause #4217 (by forward demodulation #[4216, 180]): ∀ (a a_1 a_2 : int), Eq (plus_plus int a (minus_minus int a_1 a_2)) (minus_minus int (plus_plus int a a_1) a_2) % 80.51/80.69 Clause #4263 (by superposition #[4217, 191]): ∀ (a a_1 : int), Eq (plus_plus int a (minus_minus int pls a_1)) (minus_minus int a a_1) % 80.55/80.82 Clause #4333 (by superposition #[4263, 230]): ∀ (a : int), Eq (plus_plus int a min) (minus_minus int a (bit1 pls)) % 80.55/80.82 Clause #5185 (by clausification #[742]): ∀ (a : Type) (a_1 a_2 a_3 : a), % 80.55/80.82 Or (Eq (cancel_semigroup_add a) False) (Or (Eq (Eq a_1 a_2) True) (Ne (plus_plus a a_1 a_3) (plus_plus a a_2 a_3))) % 80.55/80.82 Clause #5186 (by clausification #[5185]): ∀ (a : Type) (a_1 a_2 a_3 : a), % 80.55/80.82 Or (Eq (cancel_semigroup_add a) False) (Or (Ne (plus_plus a a_1 a_2) (plus_plus a a_3 a_2)) (Eq a_1 a_3)) % 80.55/80.82 Clause #5188 (by superposition #[5186, 97]): ∀ (a a_1 a_2 : int), Or (Ne (plus_plus int a a_1) (plus_plus int a_2 a_1)) (Or (Eq a a_2) (Eq False True)) % 80.55/80.82 Clause #5463 (by clausification #[5188]): ∀ (a a_1 a_2 : int), Or (Ne (plus_plus int a a_1) (plus_plus int a_2 a_1)) (Eq a a_2) % 80.55/80.82 Clause #5548 (by superposition #[5463, 367]): ∀ (a a_1 : int), Or (Ne (plus_plus int a a_1) a_1) (Eq a pls) % 80.55/80.82 Clause #5604 (by superposition #[5548, 605]): ∀ (a : int), Or (Ne (bit1 a) a) (Eq (plus_plus int (bit1 pls) a) pls) % 80.55/80.82 Clause #5769 (by superposition #[5604, 148]): Or (Ne min min) (Eq (plus_plus int (bit1 pls) min) pls) % 80.55/80.82 Clause #5774 (by eliminate resolved literals #[5769]): Eq (plus_plus int (bit1 pls) min) pls % 80.55/80.82 Clause #5777 (by superposition #[5774, 2868]): ∀ (a : int), Eq (plus_plus int (bit1 pls) (plus_plus int min a)) (plus_plus int pls a) % 80.55/80.82 Clause #6670 (by forward demodulation #[5777, 367]): ∀ (a : int), Eq (plus_plus int (bit1 pls) (plus_plus int min a)) a % 80.55/80.82 Clause #6671 (by superposition #[6670, 605]): ∀ (a : int), Eq (bit1 (plus_plus int min a)) (plus_plus int a (plus_plus int min a)) % 80.55/80.82 Clause #7747 (by forward demodulation #[6671, 462]): ∀ (a : int), Eq (plus_plus int min (bit0 a)) (plus_plus int a (plus_plus int min a)) % 80.55/80.82 Clause #7749 (by superposition #[7747, 6670]): Eq (plus_plus int min (bit0 (bit1 pls))) (bit1 pls) % 80.55/80.82 Clause #7794 (by superposition #[7749, 2240]): ∀ (a : int), Or (Ne (bit1 a) (bit1 pls)) (Eq a (plus_plus int min (bit1 pls))) % 80.55/80.82 Clause #7856 (by equality resolution #[7794]): Eq pls (plus_plus int min (bit1 pls)) % 80.55/80.82 Clause #7866 (by superposition #[7856, 2868]): ∀ (a : int), Eq (plus_plus int min (plus_plus int (bit1 pls) a)) (plus_plus int pls a) % 80.55/80.82 Clause #11473 (by forward demodulation #[7866, 367]): ∀ (a : int), Eq (plus_plus int min (plus_plus int (bit1 pls) a)) a % 80.55/80.82 Clause #11490 (by superposition #[11473, 2900]): ∀ (a : int), Eq (plus_plus int min (bit1 a)) (bit0 a) % 80.55/80.82 Clause #13961 (by forward demodulation #[1348, 191]): ∀ (a : int), Eq (times_times int (plus_plus int a (bit1 (bit1 pls))) pls) (times_times int a pls) % 80.55/80.82 Clause #13981 (by superposition #[13961, 11490]): Eq (times_times int (bit0 (bit1 pls)) pls) (times_times int min pls) % 80.55/80.82 Clause #13993 (by superposition #[13981, 2028]): Eq (times_times int min pls) pls % 80.55/80.82 Clause #15451 (by forward demodulation #[1393, 4333]): ∀ (a a_1 : int), Eq (times_times int a (plus_plus int a_1 min)) (minus_minus int (times_times int a a_1) a) % 80.55/80.82 Clause #15517 (by superposition #[15451, 13993]): Eq (times_times int min (plus_plus int pls min)) (minus_minus int pls min) % 80.55/80.82 Clause #16047 (by forward demodulation #[15517, 367]): Eq (times_times int min min) (minus_minus int pls min) % 80.55/80.82 Clause #16048 (by forward demodulation #[16047, 1550]): Eq (bit1 pls) (minus_minus int pls min) % 80.55/80.82 Clause #16075 (by superposition #[16048, 4263]): ∀ (a : int), Eq (plus_plus int a (bit1 pls)) (minus_minus int a min) % 80.55/80.82 Clause #16647 (by backward contextual literal cutting #[16075, 1690]): False % 80.55/80.82 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------