%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.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 : Tue May 5 06:59:08 PM UTC 2026 % Result : Theorem 121.86s 122.09s % Output : Proof 121.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.13 % Command : duper %s % 0.16/0.34 % Computer : n028.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 09:55:00 EDT 2026 % 0.16/0.34 % CPUTime : % 121.86/122.09 SZS status Theorem for theBenchmark.p % 121.86/122.09 SZS output start Proof for theBenchmark.p % 121.86/122.09 Clause #7 (by assumption #[]): Eq (∀ (X X2 X3 : Iota), Ne (n X) (x X2 X3)) True % 121.86/122.09 Clause #38 (by assumption #[]): Eq (∀ (Y : Iota), Eq (d (n Y)) (n z)) True % 121.86/122.09 Clause #39 (by assumption #[]): Eq (∀ (F G : Iota), Eq (d (x F G)) (x (d F) (d G))) True % 121.86/122.09 Clause #41 (by assumption #[]): Eq (Eq (d x2) (n (s z))) True % 121.86/122.09 Clause #49 (by assumption #[]): Eq (∀ (E : Iota), Eq (opt (x (n z) E)) E) True % 121.86/122.09 Clause #53 (by assumption #[]): Eq (Not (Exists fun E => Ne (opt (d E)) (opt (d (opt E))))) True % 121.86/122.09 Clause #69 (by clausification #[41]): Eq (d x2) (n (s z)) % 121.86/122.09 Clause #83 (by clausification #[38]): ∀ (a : Iota), Eq (Eq (d (n a)) (n z)) True % 121.86/122.09 Clause #84 (by clausification #[83]): ∀ (a : Iota), Eq (d (n a)) (n z) % 121.86/122.09 Clause #107 (by clausification #[49]): ∀ (a : Iota), Eq (Eq (opt (x (n z) a)) a) True % 121.86/122.09 Clause #108 (by clausification #[107]): ∀ (a : Iota), Eq (opt (x (n z) a)) a % 121.86/122.09 Clause #111 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (X2 X3 : Iota), Ne (n a) (x X2 X3)) True % 121.86/122.09 Clause #112 (by clausification #[111]): ∀ (a a_1 : Iota), Eq (∀ (X3 : Iota), Ne (n a) (x a_1 X3)) True % 121.86/122.09 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 : Iota), Eq (Ne (n a) (x a_1 a_2)) True % 121.86/122.09 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), Ne (n a) (x a_1 a_2) % 121.86/122.09 Clause #555 (by clausification #[39]): ∀ (a : Iota), Eq (∀ (G : Iota), Eq (d (x a G)) (x (d a) (d G))) True % 121.86/122.09 Clause #556 (by clausification #[555]): ∀ (a a_1 : Iota), Eq (Eq (d (x a a_1)) (x (d a) (d a_1))) True % 121.86/122.09 Clause #557 (by clausification #[556]): ∀ (a a_1 : Iota), Eq (d (x a a_1)) (x (d a) (d a_1)) % 121.86/122.09 Clause #561 (by superposition #[557, 114]): ∀ (a a_1 a_2 : Iota), Ne (n a) (d (x a_1 a_2)) % 121.86/122.09 Clause #570 (by superposition #[557, 84]): ∀ (a a_1 : Iota), Eq (d (x (n a) a_1)) (x (n z) (d a_1)) % 121.86/122.09 Clause #853 (by clausification #[53]): Eq (Exists fun E => Ne (opt (d E)) (opt (d (opt E)))) False % 121.86/122.09 Clause #854 (by clausification #[853]): ∀ (a : Iota), Eq (Ne (opt (d a)) (opt (d (opt a)))) False % 121.86/122.09 Clause #855 (by clausification #[854]): ∀ (a : Iota), Eq (opt (d a)) (opt (d (opt a))) % 121.86/122.09 Clause #864 (by superposition #[855, 108]): ∀ (a : Iota), Eq (opt (d (x (n z) a))) (opt (d a)) % 121.86/122.09 Clause #42587 (by forward demodulation #[864, 570]): ∀ (a : Iota), Eq (opt (x (n z) (d a))) (opt (d a)) % 121.86/122.09 Clause #42588 (by superposition #[42587, 108]): ∀ (a : Iota), Eq (opt (d a)) (d a) % 121.86/122.09 Clause #42662 (by backward demodulation #[42588, 855]): ∀ (a : Iota), Eq (d a) (opt (d (opt a))) % 121.86/122.09 Clause #42711 (by superposition #[42662, 42588]): ∀ (a : Iota), Eq (d a) (d (opt a)) % 121.86/122.09 Clause #42825 (by superposition #[42711, 108]): ∀ (a : Iota), Eq (d (x (n z) a)) (d a) % 121.86/122.09 Clause #42867 (by superposition #[42825, 561]): ∀ (a a_1 : Iota), Ne (n a) (d a_1) % 121.86/122.09 Clause #43114 (by backward contextual literal cutting #[42867, 69]): False % 121.86/122.09 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------