%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM974_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %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 : Fri Oct 3 07:57:41 PM UTC 2025 % Result : Theorem 5.45s 5.60s % Output : Proof 5.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM974_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n028.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % 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 08:27:23 EDT 2025 % 0.12/0.34 % CPUTime : % 5.45/5.60 SZS status Theorem for theBenchmark.p % 5.45/5.60 SZS output start Proof for theBenchmark.p % 5.45/5.60 Clause #0 (by assumption #[]): Eq (ord_less int (one_one int) t) True % 5.45/5.60 Clause #1 (by assumption #[]): Eq (∀ (Ma N1 : nat), Iff (ord_less nat (zero_zero nat) (minus_minus nat N1 Ma)) (ord_less nat Ma N1)) True % 5.45/5.60 Clause #4 (by assumption #[]): Eq (∀ (N1 : nat), Iff (Ne N1 (zero_zero nat)) (ord_less nat (zero_zero nat) N1)) True % 5.45/5.60 Clause #5 (by assumption #[]): Eq (∀ (N2 : nat), Not (ord_less nat N2 (zero_zero nat))) True % 5.45/5.60 Clause #35 (by assumption #[]): Eq (∀ (Z W : int), Iff (ord_less nat (nat1 W) (nat1 Z)) (And (ord_less int (zero_zero int) Z) (ord_less int W Z))) True % 5.45/5.60 Clause #37 (by assumption #[]): Eq (Eq (one_one nat) (nat1 (one_one int))) True % 5.45/5.60 Clause #39 (by assumption #[]): Eq (ord_less_eq int (one_one int) t) True % 5.45/5.60 Clause #77 (by assumption #[]): Eq (∀ (Z : int), Iff (ord_less_eq int (one_one int) Z) (ord_less int (zero_zero int) Z)) True % 5.45/5.60 Clause #108 (by assumption #[]): Eq (∀ (Tn : nat), Eq Tn (minus_minus nat (nat1 t) (one_one nat)) → ord_less nat (zero_zero nat) Tn → thesis) True % 5.45/5.60 Clause #109 (by assumption #[]): Eq (Not thesis) True % 5.45/5.60 Clause #110 (by clausification #[109]): Eq thesis False % 5.45/5.60 Clause #111 (by clausification #[1]): ∀ (a : nat), Eq (∀ (N1 : nat), Iff (ord_less nat (zero_zero nat) (minus_minus nat N1 a)) (ord_less nat a N1)) True % 5.45/5.60 Clause #112 (by clausification #[111]): ∀ (a a_1 : nat), Eq (Iff (ord_less nat (zero_zero nat) (minus_minus nat a a_1)) (ord_less nat a_1 a)) True % 5.45/5.60 Clause #113 (by clausification #[112]): ∀ (a a_1 : nat), Or (Eq (ord_less nat (zero_zero nat) (minus_minus nat a a_1)) True) (Eq (ord_less nat a_1 a) False) % 5.45/5.60 Clause #118 (by clausification #[108]): ∀ (a : nat), Eq (Eq a (minus_minus nat (nat1 t) (one_one nat)) → ord_less nat (zero_zero nat) a → thesis) True % 5.45/5.60 Clause #119 (by clausification #[118]): ∀ (a : nat), % 5.45/5.60 Or (Eq (Eq a (minus_minus nat (nat1 t) (one_one nat))) False) (Eq (ord_less nat (zero_zero nat) a → thesis) True) % 5.45/5.60 Clause #120 (by clausification #[119]): ∀ (a : nat), Or (Eq (ord_less nat (zero_zero nat) a → thesis) True) (Ne a (minus_minus nat (nat1 t) (one_one nat))) % 5.45/5.60 Clause #121 (by clausification #[120]): ∀ (a : nat), % 5.45/5.60 Or (Ne a (minus_minus nat (nat1 t) (one_one nat))) (Or (Eq (ord_less nat (zero_zero nat) a) False) (Eq thesis True)) % 5.45/5.60 Clause #122 (by destructive equality resolution #[121]): Or (Eq (ord_less nat (zero_zero nat) (minus_minus nat (nat1 t) (one_one nat))) False) (Eq thesis True) % 5.45/5.60 Clause #123 (by forward demodulation #[122, 110]): Or (Eq (ord_less nat (zero_zero nat) (minus_minus nat (nat1 t) (one_one nat))) False) (Eq False True) % 5.45/5.60 Clause #124 (by clausification #[123]): Eq (ord_less nat (zero_zero nat) (minus_minus nat (nat1 t) (one_one nat))) False % 5.45/5.60 Clause #137 (by clausification #[4]): ∀ (a : nat), Eq (Iff (Ne a (zero_zero nat)) (ord_less nat (zero_zero nat) a)) True % 5.45/5.60 Clause #139 (by clausification #[137]): ∀ (a : nat), Or (Eq (Ne a (zero_zero nat)) False) (Eq (ord_less nat (zero_zero nat) a) True) % 5.45/5.60 Clause #144 (by clausification #[139]): ∀ (a : nat), Or (Eq (ord_less nat (zero_zero nat) a) True) (Eq a (zero_zero nat)) % 5.45/5.60 Clause #145 (by superposition #[144, 124]): Or (Eq (minus_minus nat (nat1 t) (one_one nat)) (zero_zero nat)) (Eq True False) % 5.45/5.60 Clause #152 (by clausification #[5]): ∀ (a : nat), Eq (Not (ord_less nat a (zero_zero nat))) True % 5.45/5.60 Clause #153 (by clausification #[152]): ∀ (a : nat), Eq (ord_less nat a (zero_zero nat)) False % 5.45/5.60 Clause #155 (by clausification #[37]): Eq (one_one nat) (nat1 (one_one int)) % 5.45/5.60 Clause #342 (by clausification #[145]): Eq (minus_minus nat (nat1 t) (one_one nat)) (zero_zero nat) % 5.45/5.60 Clause #621 (by clausification #[35]): ∀ (a : int), % 5.45/5.60 Eq (∀ (W : int), Iff (ord_less nat (nat1 W) (nat1 a)) (And (ord_less int (zero_zero int) a) (ord_less int W a))) True % 5.45/5.60 Clause #622 (by clausification #[621]): ∀ (a a_1 : int), % 5.45/5.60 Eq (Iff (ord_less nat (nat1 a) (nat1 a_1)) (And (ord_less int (zero_zero int) a_1) (ord_less int a a_1))) True % 5.45/5.60 Clause #623 (by clausification #[622]): ∀ (a a_1 : int), % 5.45/5.60 Or (Eq (ord_less nat (nat1 a) (nat1 a_1)) True) % 5.45/5.62 (Eq (And (ord_less int (zero_zero int) a_1) (ord_less int a a_1)) False) % 5.45/5.62 Clause #625 (by clausification #[623]): ∀ (a a_1 : int), % 5.45/5.62 Or (Eq (ord_less nat (nat1 a) (nat1 a_1)) True) % 5.45/5.62 (Or (Eq (ord_less int (zero_zero int) a_1) False) (Eq (ord_less int a a_1) False)) % 5.45/5.62 Clause #644 (by clausification #[77]): ∀ (a : int), Eq (Iff (ord_less_eq int (one_one int) a) (ord_less int (zero_zero int) a)) True % 5.45/5.62 Clause #646 (by clausification #[644]): ∀ (a : int), Or (Eq (ord_less_eq int (one_one int) a) False) (Eq (ord_less int (zero_zero int) a) True) % 5.45/5.62 Clause #656 (by superposition #[646, 39]): Or (Eq (ord_less int (zero_zero int) t) True) (Eq False True) % 5.45/5.62 Clause #658 (by clausification #[656]): Eq (ord_less int (zero_zero int) t) True % 5.45/5.62 Clause #660 (by superposition #[658, 625]): ∀ (a : int), Or (Eq (ord_less nat (nat1 a) (nat1 t)) True) (Or (Eq True False) (Eq (ord_less int a t) False)) % 5.45/5.62 Clause #983 (by clausification #[660]): ∀ (a : int), Or (Eq (ord_less nat (nat1 a) (nat1 t)) True) (Eq (ord_less int a t) False) % 5.45/5.62 Clause #984 (by superposition #[983, 0]): Or (Eq (ord_less nat (nat1 (one_one int)) (nat1 t)) True) (Eq False True) % 5.45/5.62 Clause #996 (by clausification #[984]): Eq (ord_less nat (nat1 (one_one int)) (nat1 t)) True % 5.45/5.62 Clause #997 (by forward demodulation #[996, 155]): Eq (ord_less nat (one_one nat) (nat1 t)) True % 5.45/5.62 Clause #998 (by superposition #[997, 113]): Or (Eq (ord_less nat (zero_zero nat) (minus_minus nat (nat1 t) (one_one nat))) True) (Eq True False) % 5.45/5.62 Clause #1028 (by clausification #[998]): Eq (ord_less nat (zero_zero nat) (minus_minus nat (nat1 t) (one_one nat))) True % 5.45/5.62 Clause #1029 (by forward demodulation #[1028, 342]): Eq (ord_less nat (zero_zero nat) (zero_zero nat)) True % 5.45/5.62 Clause #1030 (by superposition #[1029, 153]): Eq True False % 5.45/5.62 Clause #1039 (by clausification #[1030]): False % 5.45/5.62 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------