%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM852+1 : TPTP v9.2.0. Released v4.1.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:27 PM UTC 2025 % Result : Theorem 5.23s 5.39s % Output : Proof 5.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM852+1 : TPTP v9.2.0. Released v4.1.0. % 0.12/0.14 % Command : duper %s % 0.15/0.35 % Computer : n023.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Fri Oct 3 07:08:38 EDT 2025 % 0.15/0.35 % CPUTime : % 5.23/5.39 SZS status Theorem for theBenchmark.p % 5.23/5.39 SZS output start Proof for theBenchmark.p % 5.23/5.39 Clause #0 (by assumption #[]): Eq (Not (greater (vmul vd481 vd469) (vmul vd480 vd469))) True % 5.23/5.39 Clause #1 (by assumption #[]): Eq (greater vd481 vd480) True % 5.23/5.39 Clause #4 (by assumption #[]): Eq % 5.23/5.39 (∀ (Vd470 Vd471 : Iota), % 5.23/5.39 greater Vd470 Vd471 → greater (vplus (vmul Vd471 vd469) (vmul (vskolem9 Vd470 Vd471) vd469)) (vmul Vd471 vd469)) % 5.23/5.39 True % 5.23/5.39 Clause #7 (by assumption #[]): Eq (∀ (Vd470 Vd471 : Iota), greater Vd470 Vd471 → Eq Vd470 (vplus Vd471 (vskolem9 Vd470 Vd471))) True % 5.23/5.39 Clause #9 (by assumption #[]): Eq (∀ (Vd432 Vd433 Vd434 : Iota), Eq (vmul Vd432 (vplus Vd433 Vd434)) (vplus (vmul Vd432 Vd433) (vmul Vd432 Vd434))) % 5.23/5.39 True % 5.23/5.39 Clause #10 (by assumption #[]): Eq (∀ (Vd418 Vd419 : Iota), Eq (vmul Vd418 Vd419) (vmul Vd419 Vd418)) True % 5.23/5.39 Clause #64 (by clausification #[0]): Eq (greater (vmul vd481 vd469) (vmul vd480 vd469)) False % 5.23/5.39 Clause #92 (by clausification #[4]): ∀ (a : Iota), % 5.23/5.39 Eq % 5.23/5.39 (∀ (Vd471 : Iota), % 5.23/5.39 greater a Vd471 → greater (vplus (vmul Vd471 vd469) (vmul (vskolem9 a Vd471) vd469)) (vmul Vd471 vd469)) % 5.23/5.39 True % 5.23/5.39 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), % 5.23/5.39 Eq (greater a a_1 → greater (vplus (vmul a_1 vd469) (vmul (vskolem9 a a_1) vd469)) (vmul a_1 vd469)) True % 5.23/5.39 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), % 5.23/5.39 Or (Eq (greater a a_1) False) % 5.23/5.39 (Eq (greater (vplus (vmul a_1 vd469) (vmul (vskolem9 a a_1) vd469)) (vmul a_1 vd469)) True) % 5.23/5.39 Clause #95 (by superposition #[94, 1]): Or (Eq (greater (vplus (vmul vd480 vd469) (vmul (vskolem9 vd481 vd480) vd469)) (vmul vd480 vd469)) True) (Eq False True) % 5.23/5.39 Clause #167 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Vd471 : Iota), greater a Vd471 → Eq a (vplus Vd471 (vskolem9 a Vd471))) True % 5.23/5.39 Clause #168 (by clausification #[167]): ∀ (a a_1 : Iota), Eq (greater a a_1 → Eq a (vplus a_1 (vskolem9 a a_1))) True % 5.23/5.39 Clause #169 (by clausification #[168]): ∀ (a a_1 : Iota), Or (Eq (greater a a_1) False) (Eq (Eq a (vplus a_1 (vskolem9 a a_1))) True) % 5.23/5.39 Clause #170 (by clausification #[169]): ∀ (a a_1 : Iota), Or (Eq (greater a a_1) False) (Eq a (vplus a_1 (vskolem9 a a_1))) % 5.23/5.39 Clause #171 (by superposition #[170, 1]): Or (Eq vd481 (vplus vd480 (vskolem9 vd481 vd480))) (Eq False True) % 5.23/5.39 Clause #179 (by clausification #[171]): Eq vd481 (vplus vd480 (vskolem9 vd481 vd480)) % 5.23/5.39 Clause #203 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (Vd433 Vd434 : Iota), Eq (vmul a (vplus Vd433 Vd434)) (vplus (vmul a Vd433) (vmul a Vd434))) True % 5.23/5.39 Clause #204 (by clausification #[203]): ∀ (a a_1 : Iota), Eq (∀ (Vd434 : Iota), Eq (vmul a (vplus a_1 Vd434)) (vplus (vmul a a_1) (vmul a Vd434))) True % 5.23/5.39 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 : Iota), Eq (Eq (vmul a (vplus a_1 a_2)) (vplus (vmul a a_1) (vmul a a_2))) True % 5.23/5.39 Clause #206 (by clausification #[205]): ∀ (a a_1 a_2 : Iota), Eq (vmul a (vplus a_1 a_2)) (vplus (vmul a a_1) (vmul a a_2)) % 5.23/5.39 Clause #223 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (Vd419 : Iota), Eq (vmul a Vd419) (vmul Vd419 a)) True % 5.23/5.39 Clause #224 (by clausification #[223]): ∀ (a a_1 : Iota), Eq (Eq (vmul a a_1) (vmul a_1 a)) True % 5.23/5.39 Clause #225 (by clausification #[224]): ∀ (a a_1 : Iota), Eq (vmul a a_1) (vmul a_1 a) % 5.23/5.39 Clause #227 (by superposition #[225, 64]): Eq (greater (vmul vd469 vd481) (vmul vd480 vd469)) False % 5.23/5.39 Clause #897 (by forward demodulation #[227, 225]): Eq (greater (vmul vd469 vd481) (vmul vd469 vd480)) False % 5.23/5.39 Clause #2098 (by clausification #[95]): Eq (greater (vplus (vmul vd480 vd469) (vmul (vskolem9 vd481 vd480) vd469)) (vmul vd480 vd469)) True % 5.23/5.39 Clause #2099 (by forward demodulation #[2098, 225]): Eq (greater (vplus (vmul vd480 vd469) (vmul (vskolem9 vd481 vd480) vd469)) (vmul vd469 vd480)) True % 5.23/5.39 Clause #2100 (by forward demodulation #[2099, 225]): Eq (greater (vplus (vmul vd480 vd469) (vmul vd469 (vskolem9 vd481 vd480))) (vmul vd469 vd480)) True % 5.23/5.39 Clause #2101 (by forward demodulation #[2100, 225]): Eq (greater (vplus (vmul vd469 vd480) (vmul vd469 (vskolem9 vd481 vd480))) (vmul vd469 vd480)) True % 5.23/5.39 Clause #2102 (by forward demodulation #[2101, 206]): Eq (greater (vmul vd469 (vplus vd480 (vskolem9 vd481 vd480))) (vmul vd469 vd480)) True % 5.23/5.40 Clause #2103 (by forward demodulation #[2102, 179]): Eq (greater (vmul vd469 vd481) (vmul vd469 vd480)) True % 5.23/5.40 Clause #2104 (by superposition #[2103, 897]): Eq True False % 5.23/5.40 Clause #2133 (by clausification #[2104]): False % 5.23/5.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------