%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYN924+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 08:08:15 PM UTC 2025 % Result : Theorem 7.55s 7.73s % Output : Proof 7.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYN924+1 : TPTP v9.2.0. Released v3.1.0. % 0.03/0.12 % Command : duper %s % 0.10/0.32 % Computer : n012.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Thu Oct 2 15:30:23 EDT 2025 % 0.10/0.32 % CPUTime : % 7.55/7.73 SZS status Theorem for theBenchmark.p % 7.55/7.73 SZS output start Proof for theBenchmark.p % 7.55/7.73 Clause #0 (by assumption #[]): Eq (Not (Iff (Exists fun X => Or (p X) (q X)) (Or (Exists fun X => p X) (Exists fun X => q X)))) True % 7.55/7.73 Clause #1 (by betaEtaReduce #[0]): Eq (Not (Iff (Exists fun X => Or (p X) (q X)) (Or (Exists p) (Exists q)))) True % 7.55/7.73 Clause #2 (by clausification #[1]): Eq (Iff (Exists fun X => Or (p X) (q X)) (Or (Exists p) (Exists q))) False % 7.55/7.73 Clause #3 (by clausification #[2]): Or (Eq (Exists fun X => Or (p X) (q X)) False) (Eq (Or (Exists p) (Exists q)) False) % 7.55/7.73 Clause #4 (by clausification #[2]): Or (Eq (Exists fun X => Or (p X) (q X)) True) (Eq (Or (Exists p) (Exists q)) True) % 7.55/7.73 Clause #5 (by clausification #[3]): ∀ (a : Iota), Or (Eq (Or (Exists p) (Exists q)) False) (Eq (Or (p a) (q a)) False) % 7.55/7.73 Clause #6 (by clausification #[5]): ∀ (a : Iota), Or (Eq (Or (p a) (q a)) False) (Eq (Exists q) False) % 7.55/7.73 Clause #7 (by clausification #[5]): ∀ (a : Iota), Or (Eq (Or (p a) (q a)) False) (Eq (Exists p) False) % 7.55/7.73 Clause #8 (by clausification #[6]): ∀ (a : Iota), Or (Eq (Exists q) False) (Eq (q a) False) % 7.55/7.73 Clause #10 (by clausification #[8]): ∀ (a a_1 : Iota), Or (Eq (q a) False) (Eq (q a_1) False) % 7.55/7.73 Clause #13 (by clausification #[7]): ∀ (a : Iota), Or (Eq (Exists p) False) (Eq (p a) False) % 7.55/7.73 Clause #15 (by clausification #[13]): ∀ (a a_1 : Iota), Or (Eq (p a) False) (Eq (p a_1) False) % 7.55/7.73 Clause #16 (by clausification #[4]): ∀ (a : Iota), Or (Eq (Or (Exists p) (Exists q)) True) (Eq (Or (p (skS.0 0 a)) (q (skS.0 0 a))) True) % 7.55/7.73 Clause #17 (by clausification #[16]): ∀ (a : Iota), Or (Eq (Or (p (skS.0 0 a)) (q (skS.0 0 a))) True) (Or (Eq (Exists p) True) (Eq (Exists q) True)) % 7.55/7.73 Clause #18 (by clausification #[17]): ∀ (a : Iota), Or (Eq (Exists p) True) (Or (Eq (Exists q) True) (Or (Eq (p (skS.0 0 a)) True) (Eq (q (skS.0 0 a)) True))) % 7.55/7.73 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), % 7.55/7.73 Or (Eq (Exists q) True) (Or (Eq (p (skS.0 0 a)) True) (Or (Eq (q (skS.0 0 a)) True) (Eq (p (skS.0 1 a_1)) True))) % 7.55/7.73 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 : Iota), % 7.55/7.73 Or (Eq (p (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (q (skS.0 0 a)) True) (Or (Eq (p (skS.0 1 a_1)) True) (Eq (q (skS.0 2 a_2)) True))) % 7.55/7.73 Clause #22 (by superposition #[20, 15]): ∀ (a a_1 a_2 a_3 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Or (Eq True False) (Eq (p a_3) False)))) % 7.55/7.73 Clause #28 (by clausification #[22]): ∀ (a a_1 a_2 a_3 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) (Or (Eq (p (skS.0 1 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Eq (p a_3) False))) % 7.55/7.73 Clause #29 (by superposition #[28, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_1)) True) % 7.55/7.73 (Or (Eq (q (skS.0 2 a_2)) True) % 7.55/7.73 (Or (Eq False True) % 7.55/7.73 (Or (Eq (q (skS.0 0 a_3)) True) (Or (Eq (p (skS.0 1 a_4)) True) (Eq (q (skS.0 2 a_5)) True)))))) % 7.55/7.73 Clause #41 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_1)) True) % 7.55/7.73 (Or (Eq (q (skS.0 2 a_2)) True) % 7.55/7.73 (Or (Eq (q (skS.0 0 a_3)) True) (Or (Eq (p (skS.0 1 a_4)) True) (Eq (q (skS.0 2 a_5)) True))))) % 7.55/7.73 Clause #68 (by equality factoring #[41]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_1)) True) % 7.55/7.73 (Or (Eq (q (skS.0 0 a_2)) True) (Or (Eq (p (skS.0 1 a_3)) True) (Or (Ne True True) (Eq (q (skS.0 2 a_4)) True))))) % 7.55/7.73 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_1)) True) % 7.55/7.73 (Or (Eq (q (skS.0 0 a_2)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_3)) True) (Or (Eq (q (skS.0 2 a_4)) True) (Or (Eq True False) (Eq True False)))))) % 7.55/7.73 Clause #71 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_1)) True) % 7.55/7.73 (Or (Eq (q (skS.0 0 a_2)) True) % 7.55/7.73 (Or (Eq (p (skS.0 1 a_3)) True) (Or (Eq (q (skS.0 2 a_4)) True) (Eq True False))))) % 7.55/7.73 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.55/7.73 Or (Eq (q (skS.0 0 a)) True) % 7.59/7.80 (Or (Eq (p (skS.0 1 a_1)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_2)) True) (Or (Eq (p (skS.0 1 a_3)) True) (Eq (q (skS.0 2 a_4)) True)))) % 7.59/7.80 Clause #94 (by equality factoring #[72]): ∀ (a a_1 a_2 a_3 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 0 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Or (Ne True True) (Eq (p (skS.0 1 a_3)) True)))) % 7.59/7.80 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 a_3 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 0 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_1)) True) % 7.59/7.80 (Or (Eq (q (skS.0 2 a_2)) True) (Or (Eq (p (skS.0 1 a_3)) True) (Or (Eq True False) (Eq True False))))) % 7.59/7.80 Clause #97 (by clausification #[95]): ∀ (a a_1 a_2 a_3 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 0 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Or (Eq (p (skS.0 1 a_3)) True) (Eq True False)))) % 7.59/7.80 Clause #98 (by clausification #[97]): ∀ (a a_1 a_2 a_3 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 0 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Eq (p (skS.0 1 a_3)) True))) % 7.59/7.80 Clause #111 (by equality factoring #[98]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) (Or (Eq (p (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (q (skS.0 0 a_2)) True))) % 7.59/7.80 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) % 7.59/7.80 (Or (Eq (p (skS.0 1 a_1)) True) (Or (Eq (q (skS.0 0 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.59/7.80 Clause #114 (by clausification #[112]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) (Or (Eq (p (skS.0 1 a_1)) True) (Or (Eq (q (skS.0 0 a_2)) True) (Eq True False))) % 7.59/7.80 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 : Iota), Or (Eq (q (skS.0 2 a)) True) (Or (Eq (p (skS.0 1 a_1)) True) (Eq (q (skS.0 0 a_2)) True)) % 7.59/7.80 Clause #120 (by superposition #[115, 15]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) (Or (Eq (q (skS.0 0 a_1)) True) (Or (Eq True False) (Eq (p a_2) False))) % 7.59/7.80 Clause #143 (by clausification #[120]): ∀ (a a_1 a_2 : Iota), Or (Eq (q (skS.0 2 a)) True) (Or (Eq (q (skS.0 0 a_1)) True) (Eq (p a_2) False)) % 7.59/7.80 Clause #144 (by superposition #[143, 115]): ∀ (a a_1 a_2 a_3 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Or (Eq False True) (Eq (q (skS.0 0 a_3)) True)))) % 7.59/7.80 Clause #181 (by clausification #[144]): ∀ (a a_1 a_2 a_3 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 0 a_1)) True) (Or (Eq (q (skS.0 2 a_2)) True) (Eq (q (skS.0 0 a_3)) True))) % 7.59/7.80 Clause #199 (by equality factoring #[181]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) (Or (Eq (q (skS.0 2 a_1)) True) (Or (Ne True True) (Eq (q (skS.0 0 a_2)) True))) % 7.59/7.80 Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) % 7.59/7.80 (Or (Eq (q (skS.0 2 a_1)) True) (Or (Eq (q (skS.0 0 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.59/7.80 Clause #202 (by clausification #[200]): ∀ (a a_1 a_2 : Iota), % 7.59/7.80 Or (Eq (q (skS.0 2 a)) True) (Or (Eq (q (skS.0 2 a_1)) True) (Or (Eq (q (skS.0 0 a_2)) True) (Eq True False))) % 7.59/7.80 Clause #203 (by clausification #[202]): ∀ (a a_1 a_2 : Iota), Or (Eq (q (skS.0 2 a)) True) (Or (Eq (q (skS.0 2 a_1)) True) (Eq (q (skS.0 0 a_2)) True)) % 7.59/7.80 Clause #211 (by equality factoring #[203]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Or (Ne True True) (Eq (q (skS.0 2 a_1)) True)) % 7.59/7.80 Clause #212 (by clausification #[211]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Or (Eq (q (skS.0 2 a_1)) True) (Or (Eq True False) (Eq True False))) % 7.59/7.80 Clause #214 (by clausification #[212]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Or (Eq (q (skS.0 2 a_1)) True) (Eq True False)) % 7.59/7.80 Clause #215 (by clausification #[214]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Eq (q (skS.0 2 a_1)) True) % 7.59/7.80 Clause #218 (by superposition #[215, 10]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Or (Eq True False) (Eq (q a_1) False)) % 7.59/7.80 Clause #221 (by clausification #[218]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Eq (q a_1) False) % 7.59/7.80 Clause #223 (by superposition #[221, 215]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Or (Eq (q (skS.0 0 a_1)) True) (Eq False True)) % 7.59/7.81 Clause #228 (by clausification #[223]): ∀ (a a_1 : Iota), Or (Eq (q (skS.0 0 a)) True) (Eq (q (skS.0 0 a_1)) True) % 7.59/7.81 Clause #230 (by equality factoring #[228]): ∀ (a : Iota), Or (Ne True True) (Eq (q (skS.0 0 a)) True) % 7.59/7.81 Clause #231 (by clausification #[230]): ∀ (a : Iota), Or (Eq (q (skS.0 0 a)) True) (Or (Eq True False) (Eq True False)) % 7.59/7.81 Clause #233 (by clausification #[231]): ∀ (a : Iota), Or (Eq (q (skS.0 0 a)) True) (Eq True False) % 7.59/7.81 Clause #234 (by clausification #[233]): ∀ (a : Iota), Eq (q (skS.0 0 a)) True % 7.59/7.81 Clause #235 (by superposition #[234, 10]): ∀ (a : Iota), Or (Eq True False) (Eq (q a) False) % 7.59/7.81 Clause #237 (by clausification #[235]): ∀ (a : Iota), Eq (q a) False % 7.59/7.81 Clause #238 (by superposition #[237, 234]): Eq False True % 7.59/7.81 Clause #239 (by clausification #[238]): False % 7.59/7.81 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------