%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM852+2 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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 3.95s 4.12s % Output : Proof 3.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM852+2 : TPTP v9.2.0. Released v4.1.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 07:25:23 EDT 2025 % 0.13/0.34 % CPUTime : % 3.95/4.12 SZS status Theorem for theBenchmark.p % 3.95/4.12 SZS output start Proof for theBenchmark.p % 3.95/4.12 Clause #0 (by assumption #[]): Eq (Not (greater (vmul vd481 vd469) (vmul vd480 vd469))) True % 3.95/4.12 Clause #1 (by assumption #[]): Eq (greater vd481 vd480) True % 3.95/4.12 Clause #4 (by assumption #[]): Eq % 3.95/4.12 (∀ (Vd470 Vd471 : Iota), % 3.95/4.12 greater Vd470 Vd471 → greater (vplus (vmul Vd471 vd469) (vmul (vskolem9 Vd470 Vd471) vd469)) (vmul Vd471 vd469)) % 3.95/4.12 True % 3.95/4.12 Clause #7 (by assumption #[]): Eq (∀ (Vd470 Vd471 : Iota), greater Vd470 Vd471 → Eq Vd470 (vplus Vd471 (vskolem9 Vd470 Vd471))) True % 3.95/4.12 Clause #9 (by assumption #[]): Eq (∀ (Vd432 Vd433 Vd434 : Iota), Eq (vmul Vd432 (vplus Vd433 Vd434)) (vplus (vmul Vd432 Vd433) (vmul Vd432 Vd434))) % 3.95/4.12 True % 3.95/4.12 Clause #10 (by assumption #[]): Eq (∀ (Vd418 Vd419 : Iota), Eq (vmul Vd418 Vd419) (vmul Vd419 Vd418)) True % 3.95/4.12 Clause #28 (by clausification #[0]): Eq (greater (vmul vd481 vd469) (vmul vd480 vd469)) False % 3.95/4.12 Clause #29 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (Vd419 : Iota), Eq (vmul a Vd419) (vmul Vd419 a)) True % 3.95/4.12 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Eq (Eq (vmul a a_1) (vmul a_1 a)) True % 3.95/4.12 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Eq (vmul a a_1) (vmul a_1 a) % 3.95/4.12 Clause #33 (by superposition #[31, 28]): Eq (greater (vmul vd469 vd481) (vmul vd480 vd469)) False % 3.95/4.12 Clause #34 (by forward demodulation #[33, 31]): Eq (greater (vmul vd469 vd481) (vmul vd469 vd480)) False % 3.95/4.12 Clause #41 (by clausification #[4]): ∀ (a : Iota), % 3.95/4.12 Eq % 3.95/4.12 (∀ (Vd471 : Iota), % 3.95/4.12 greater a Vd471 → greater (vplus (vmul Vd471 vd469) (vmul (vskolem9 a Vd471) vd469)) (vmul Vd471 vd469)) % 3.95/4.12 True % 3.95/4.12 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 3.95/4.12 Eq (greater a a_1 → greater (vplus (vmul a_1 vd469) (vmul (vskolem9 a a_1) vd469)) (vmul a_1 vd469)) True % 3.95/4.12 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), % 3.95/4.12 Or (Eq (greater a a_1) False) % 3.95/4.12 (Eq (greater (vplus (vmul a_1 vd469) (vmul (vskolem9 a a_1) vd469)) (vmul a_1 vd469)) True) % 3.95/4.12 Clause #44 (by forward demodulation #[43, 31]): ∀ (a a_1 : Iota), % 3.95/4.12 Or (Eq (greater a a_1) False) % 3.95/4.12 (Eq (greater (vplus (vmul a_1 vd469) (vmul vd469 (vskolem9 a a_1))) (vmul a_1 vd469)) True) % 3.95/4.12 Clause #45 (by superposition #[44, 1]): Or (Eq (greater (vplus (vmul vd480 vd469) (vmul vd469 (vskolem9 vd481 vd480))) (vmul vd480 vd469)) True) (Eq False True) % 3.95/4.12 Clause #52 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Vd471 : Iota), greater a Vd471 → Eq a (vplus Vd471 (vskolem9 a Vd471))) True % 3.95/4.12 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Eq (greater a a_1 → Eq a (vplus a_1 (vskolem9 a a_1))) True % 3.95/4.12 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), Or (Eq (greater a a_1) False) (Eq (Eq a (vplus a_1 (vskolem9 a a_1))) True) % 3.95/4.12 Clause #55 (by clausification #[54]): ∀ (a a_1 : Iota), Or (Eq (greater a a_1) False) (Eq a (vplus a_1 (vskolem9 a a_1))) % 3.95/4.12 Clause #56 (by superposition #[55, 1]): Or (Eq vd481 (vplus vd480 (vskolem9 vd481 vd480))) (Eq False True) % 3.95/4.12 Clause #57 (by clausification #[56]): Eq vd481 (vplus vd480 (vskolem9 vd481 vd480)) % 3.95/4.12 Clause #223 (by clausification #[9]): ∀ (a : Iota), Eq (∀ (Vd433 Vd434 : Iota), Eq (vmul a (vplus Vd433 Vd434)) (vplus (vmul a Vd433) (vmul a Vd434))) True % 3.95/4.12 Clause #224 (by clausification #[223]): ∀ (a a_1 : Iota), Eq (∀ (Vd434 : Iota), Eq (vmul a (vplus a_1 Vd434)) (vplus (vmul a a_1) (vmul a Vd434))) True % 3.95/4.12 Clause #225 (by clausification #[224]): ∀ (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 % 3.95/4.12 Clause #226 (by clausification #[225]): ∀ (a a_1 a_2 : Iota), Eq (vmul a (vplus a_1 a_2)) (vplus (vmul a a_1) (vmul a a_2)) % 3.95/4.12 Clause #419 (by clausification #[45]): Eq (greater (vplus (vmul vd480 vd469) (vmul vd469 (vskolem9 vd481 vd480))) (vmul vd480 vd469)) True % 3.95/4.12 Clause #420 (by forward demodulation #[419, 31]): Eq (greater (vplus (vmul vd480 vd469) (vmul vd469 (vskolem9 vd481 vd480))) (vmul vd469 vd480)) True % 3.95/4.12 Clause #421 (by forward demodulation #[420, 31]): Eq (greater (vplus (vmul vd469 vd480) (vmul vd469 (vskolem9 vd481 vd480))) (vmul vd469 vd480)) True % 3.95/4.12 Clause #422 (by forward demodulation #[421, 226]): Eq (greater (vmul vd469 (vplus vd480 (vskolem9 vd481 vd480))) (vmul vd469 vd480)) True % 3.95/4.12 Clause #423 (by forward demodulation #[422, 57]): Eq (greater (vmul vd469 vd481) (vmul vd469 vd480)) True % 3.95/4.12 Clause #424 (by superposition #[423, 34]): Eq True False % 3.95/4.12 Clause #440 (by clausification #[424]): False % 3.95/4.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------