%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUN073+2 : TPTP v9.2.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n003.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:49 PM UTC 2025 % Result : Theorem 5.24s 5.48s % Output : Proof 5.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUN073+2 : TPTP v9.2.0. Released v7.3.0. % 0.13/0.13 % Command : duper %s % 0.14/0.34 % Computer : n003.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 11:43:08 EDT 2025 % 0.20/0.34 % CPUTime : % 5.24/5.48 SZS status Theorem for theBenchmark.p % 5.24/5.48 SZS output start Proof for theBenchmark.p % 5.24/5.48 Clause #0 (by assumption #[]): Eq (Exists fun Y24 => ∀ (X19 : Iota), Or (And (Not (r1 X19)) (Ne X19 Y24)) (And (r1 X19) (Eq X19 Y24))) True % 5.24/5.48 Clause #6 (by assumption #[]): Eq % 5.24/5.48 (∀ (X3 X10 : Iota), % 5.24/5.48 Or (∀ (Y12 : Iota), Or (∀ (Y13 : Iota), Or (Not (r2 X3 Y13)) (Ne Y13 Y12)) (Not (r2 X10 Y12))) (Eq X3 X10)) % 5.24/5.48 True % 5.24/5.48 Clause #10 (by assumption #[]): Eq (∀ (X7 Y10 : Iota), Or (∀ (Y20 : Iota), Or (Not (r1 Y20)) (Ne Y20 Y10)) (Not (r2 X7 Y10))) True % 5.24/5.48 Clause #11 (by assumption #[]): Eq % 5.24/5.48 (Not % 5.24/5.48 (∀ (Y1 : Iota), % 5.24/5.48 Or (∀ (Y2 : Iota), Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 Y2))) (Ne Y2 Y1)) % 5.24/5.48 (∀ (Y3 : Iota), Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 Y3))) (Not (r2 Y3 Y1))))) % 5.24/5.48 True % 5.24/5.48 Clause #12 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (Y10 : Iota), Or (∀ (Y20 : Iota), Or (Not (r1 Y20)) (Ne Y20 Y10)) (Not (r2 a Y10))) True % 5.24/5.48 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (Or (∀ (Y20 : Iota), Or (Not (r1 Y20)) (Ne Y20 a)) (Not (r2 a_1 a))) True % 5.24/5.48 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Or (Eq (∀ (Y20 : Iota), Or (Not (r1 Y20)) (Ne Y20 a)) True) (Eq (Not (r2 a_1 a)) True) % 5.24/5.48 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 : Iota), Or (Eq (Not (r2 a a_1)) True) (Eq (Or (Not (r1 a_2)) (Ne a_2 a_1)) True) % 5.24/5.48 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), Or (Eq (Or (Not (r1 a)) (Ne a a_1)) True) (Eq (r2 a_2 a_1) False) % 5.24/5.48 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), Or (Eq (r2 a a_1) False) (Or (Eq (Not (r1 a_2)) True) (Eq (Ne a_2 a_1) True)) % 5.24/5.48 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), Or (Eq (r2 a a_1) False) (Or (Eq (Ne a_2 a_1) True) (Eq (r1 a_2) False)) % 5.24/5.48 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Or (Eq (r2 a a_1) False) (Or (Eq (r1 a_2) False) (Ne a_2 a_1)) % 5.24/5.48 Clause #20 (by destructive equality resolution #[19]): ∀ (a a_1 : Iota), Or (Eq (r2 a a_1) False) (Eq (r1 a_1) False) % 5.24/5.48 Clause #30 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X19 : Iota), Or (And (Not (r1 X19)) (Ne X19 (skS.0 2 a))) (And (r1 X19) (Eq X19 (skS.0 2 a)))) True % 5.24/5.48 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Eq (Or (And (Not (r1 a)) (Ne a (skS.0 2 a_1))) (And (r1 a) (Eq a (skS.0 2 a_1)))) True % 5.24/5.48 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Or (Eq (And (Not (r1 a)) (Ne a (skS.0 2 a_1))) True) (Eq (And (r1 a) (Eq a (skS.0 2 a_1))) True) % 5.24/5.48 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Or (Eq (And (r1 a) (Eq a (skS.0 2 a_1))) True) (Eq (Ne a (skS.0 2 a_1)) True) % 5.24/5.48 Clause #34 (by clausification #[32]): ∀ (a a_1 : Iota), Or (Eq (And (r1 a) (Eq a (skS.0 2 a_1))) True) (Eq (Not (r1 a)) True) % 5.24/5.48 Clause #36 (by clausification #[33]): ∀ (a a_1 : Iota), Or (Eq (Ne a (skS.0 2 a_1)) True) (Eq (r1 a) True) % 5.24/5.48 Clause #49 (by clausification #[36]): ∀ (a a_1 : Iota), Or (Eq (r1 a) True) (Ne a (skS.0 2 a_1)) % 5.24/5.48 Clause #50 (by destructive equality resolution #[49]): ∀ (a : Iota), Eq (r1 (skS.0 2 a)) True % 5.24/5.48 Clause #55 (by clausification #[34]): ∀ (a a_1 : Iota), Or (Eq (Not (r1 a)) True) (Eq (Eq a (skS.0 2 a_1)) True) % 5.24/5.48 Clause #57 (by clausification #[55]): ∀ (a a_1 : Iota), Or (Eq (Eq a (skS.0 2 a_1)) True) (Eq (r1 a) False) % 5.24/5.48 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), Or (Eq (r1 a) False) (Eq a (skS.0 2 a_1)) % 5.24/5.48 Clause #109 (by clausification #[6]): ∀ (a : Iota), % 5.24/5.48 Eq % 5.24/5.48 (∀ (X10 : Iota), % 5.24/5.48 Or (∀ (Y12 : Iota), Or (∀ (Y13 : Iota), Or (Not (r2 a Y13)) (Ne Y13 Y12)) (Not (r2 X10 Y12))) (Eq a X10)) % 5.24/5.48 True % 5.24/5.48 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), % 5.24/5.48 Eq (Or (∀ (Y12 : Iota), Or (∀ (Y13 : Iota), Or (Not (r2 a Y13)) (Ne Y13 Y12)) (Not (r2 a_1 Y12))) (Eq a a_1)) True % 5.24/5.48 Clause #111 (by clausification #[110]): ∀ (a a_1 : Iota), % 5.24/5.48 Or (Eq (∀ (Y12 : Iota), Or (∀ (Y13 : Iota), Or (Not (r2 a Y13)) (Ne Y13 Y12)) (Not (r2 a_1 Y12))) True) % 5.24/5.48 (Eq (Eq a a_1) True) % 5.24/5.48 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 5.24/5.48 Or (Eq (Eq a a_1) True) (Eq (Or (∀ (Y13 : Iota), Or (Not (r2 a Y13)) (Ne Y13 a_2)) (Not (r2 a_1 a_2))) True) % 5.35/5.51 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 : Iota), Or (Eq (Or (∀ (Y13 : Iota), Or (Not (r2 a Y13)) (Ne Y13 a_1)) (Not (r2 a_2 a_1))) True) (Eq a a_2) % 5.35/5.51 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 5.35/5.51 Or (Eq a a_1) (Or (Eq (∀ (Y13 : Iota), Or (Not (r2 a Y13)) (Ne Y13 a_2)) True) (Eq (Not (r2 a_1 a_2)) True)) % 5.35/5.51 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq a a_1) (Or (Eq (Not (r2 a_1 a_2)) True) (Eq (Or (Not (r2 a a_3)) (Ne a_3 a_2)) True)) % 5.35/5.51 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq a a_1) (Or (Eq (Or (Not (r2 a a_2)) (Ne a_2 a_3)) True) (Eq (r2 a_1 a_3) False)) % 5.35/5.51 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 a_3 : Iota), % 5.35/5.51 Or (Eq a a_1) (Or (Eq (r2 a_1 a_2) False) (Or (Eq (Not (r2 a a_3)) True) (Eq (Ne a_3 a_2) True))) % 5.35/5.51 Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq a a_1) (Or (Eq (r2 a_1 a_2) False) (Or (Eq (Ne a_3 a_2) True) (Eq (r2 a a_3) False))) % 5.35/5.51 Clause #119 (by clausification #[118]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq a a_1) (Or (Eq (r2 a_1 a_2) False) (Or (Eq (r2 a a_3) False) (Ne a_3 a_2))) % 5.35/5.51 Clause #120 (by destructive equality resolution #[119]): ∀ (a a_1 a_2 : Iota), Or (Eq a a_1) (Or (Eq (r2 a_1 a_2) False) (Eq (r2 a a_2) False)) % 5.35/5.51 Clause #183 (by clausification #[11]): Eq % 5.35/5.51 (∀ (Y1 : Iota), % 5.35/5.51 Or (∀ (Y2 : Iota), Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 Y2))) (Ne Y2 Y1)) % 5.35/5.51 (∀ (Y3 : Iota), Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 Y3))) (Not (r2 Y3 Y1)))) % 5.35/5.51 False % 5.35/5.51 Clause #184 (by clausification #[183]): ∀ (a : Iota), % 5.35/5.51 Eq % 5.35/5.51 (Not % 5.35/5.51 (Or (∀ (Y2 : Iota), Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 Y2))) (Ne Y2 (skS.0 16 a))) % 5.35/5.51 (∀ (Y3 : Iota), Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 Y3))) (Not (r2 Y3 (skS.0 16 a)))))) % 5.35/5.51 True % 5.35/5.51 Clause #185 (by clausification #[184]): ∀ (a : Iota), % 5.35/5.51 Eq % 5.35/5.51 (Or (∀ (Y2 : Iota), Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 Y2))) (Ne Y2 (skS.0 16 a))) % 5.35/5.51 (∀ (Y3 : Iota), Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 Y3))) (Not (r2 Y3 (skS.0 16 a))))) % 5.35/5.51 False % 5.35/5.51 Clause #186 (by clausification #[185]): ∀ (a : Iota), Eq (∀ (Y3 : Iota), Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 Y3))) (Not (r2 Y3 (skS.0 16 a)))) False % 5.35/5.51 Clause #187 (by clausification #[185]): ∀ (a : Iota), Eq (∀ (Y2 : Iota), Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 Y2))) (Ne Y2 (skS.0 16 a))) False % 5.35/5.51 Clause #188 (by clausification #[186]): ∀ (a a_1 : Iota), % 5.35/5.51 Eq % 5.35/5.51 (Not (Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 (skS.0 17 a a_1)))) (Not (r2 (skS.0 17 a a_1) (skS.0 16 a))))) % 5.35/5.51 True % 5.35/5.51 Clause #189 (by clausification #[188]): ∀ (a a_1 : Iota), % 5.35/5.51 Eq (Or (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 (skS.0 17 a a_1)))) (Not (r2 (skS.0 17 a a_1) (skS.0 16 a)))) % 5.35/5.51 False % 5.35/5.51 Clause #190 (by clausification #[189]): ∀ (a a_1 : Iota), Eq (Not (r2 (skS.0 17 a a_1) (skS.0 16 a))) False % 5.35/5.51 Clause #191 (by clausification #[189]): ∀ (a a_1 : Iota), Eq (∀ (Y5 : Iota), Or (Not (r1 Y5)) (Not (r2 Y5 (skS.0 17 a a_1)))) False % 5.35/5.51 Clause #192 (by clausification #[190]): ∀ (a a_1 : Iota), Eq (r2 (skS.0 17 a a_1) (skS.0 16 a)) True % 5.35/5.51 Clause #195 (by superposition #[192, 120]): ∀ (a a_1 a_2 : Iota), Or (Eq a (skS.0 17 a_1 a_2)) (Or (Eq True False) (Eq (r2 a (skS.0 16 a_1)) False)) % 5.35/5.51 Clause #197 (by clausification #[191]): ∀ (a a_1 a_2 : Iota), % 5.35/5.51 Eq (Not (Or (Not (r1 (skS.0 18 a a_1 a_2))) (Not (r2 (skS.0 18 a a_1 a_2) (skS.0 17 a a_1))))) True % 5.35/5.51 Clause #198 (by clausification #[197]): ∀ (a a_1 a_2 : Iota), Eq (Or (Not (r1 (skS.0 18 a a_1 a_2))) (Not (r2 (skS.0 18 a a_1 a_2) (skS.0 17 a a_1)))) False % 5.35/5.51 Clause #199 (by clausification #[198]): ∀ (a a_1 a_2 : Iota), Eq (Not (r2 (skS.0 18 a a_1 a_2) (skS.0 17 a a_1))) False % 5.35/5.51 Clause #201 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), Eq (r2 (skS.0 18 a a_1 a_2) (skS.0 17 a a_1)) True % 5.35/5.51 Clause #202 (by superposition #[201, 20]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (r1 (skS.0 17 a a_1)) False) % 5.35/5.51 Clause #205 (by clausification #[202]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 17 a a_1)) False % 5.36/5.53 Clause #233 (by clausification #[195]): ∀ (a a_1 a_2 : Iota), Or (Eq a (skS.0 17 a_1 a_2)) (Eq (r2 a (skS.0 16 a_1)) False) % 5.36/5.53 Clause #247 (by clausification #[187]): ∀ (a a_1 : Iota), % 5.36/5.53 Eq (Not (Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 (skS.0 20 a a_1)))) (Ne (skS.0 20 a a_1) (skS.0 16 a)))) True % 5.36/5.53 Clause #248 (by clausification #[247]): ∀ (a a_1 : Iota), % 5.36/5.53 Eq (Or (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 (skS.0 20 a a_1)))) (Ne (skS.0 20 a a_1) (skS.0 16 a))) False % 5.36/5.53 Clause #249 (by clausification #[248]): ∀ (a a_1 : Iota), Eq (Ne (skS.0 20 a a_1) (skS.0 16 a)) False % 5.36/5.53 Clause #250 (by clausification #[248]): ∀ (a a_1 : Iota), Eq (∀ (Y4 : Iota), Or (Not (r1 Y4)) (Not (r2 Y4 (skS.0 20 a a_1)))) False % 5.36/5.53 Clause #251 (by clausification #[249]): ∀ (a a_1 : Iota), Eq (skS.0 20 a a_1) (skS.0 16 a) % 5.36/5.53 Clause #253 (by clausification #[250]): ∀ (a a_1 a_2 : Iota), % 5.36/5.53 Eq (Not (Or (Not (r1 (skS.0 21 a a_1 a_2))) (Not (r2 (skS.0 21 a a_1 a_2) (skS.0 20 a a_1))))) True % 5.36/5.53 Clause #254 (by clausification #[253]): ∀ (a a_1 a_2 : Iota), Eq (Or (Not (r1 (skS.0 21 a a_1 a_2))) (Not (r2 (skS.0 21 a a_1 a_2) (skS.0 20 a a_1)))) False % 5.36/5.53 Clause #255 (by clausification #[254]): ∀ (a a_1 a_2 : Iota), Eq (Not (r2 (skS.0 21 a a_1 a_2) (skS.0 20 a a_1))) False % 5.36/5.53 Clause #256 (by clausification #[254]): ∀ (a a_1 a_2 : Iota), Eq (Not (r1 (skS.0 21 a a_1 a_2))) False % 5.36/5.53 Clause #257 (by clausification #[255]): ∀ (a a_1 a_2 : Iota), Eq (r2 (skS.0 21 a a_1 a_2) (skS.0 20 a a_1)) True % 5.36/5.53 Clause #258 (by forward demodulation #[257, 251]): ∀ (a a_1 a_2 : Iota), Eq (r2 (skS.0 21 a a_1 a_2) (skS.0 16 a)) True % 5.36/5.53 Clause #262 (by clausification #[256]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 21 a a_1 a_2)) True % 5.36/5.53 Clause #263 (by superposition #[262, 58]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (skS.0 21 a a_1 a_2) (skS.0 2 a_3)) % 5.36/5.53 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 21 a a_1 a_2) (skS.0 2 a_3) % 5.36/5.53 Clause #265 (by superposition #[264, 258]): ∀ (a a_1 : Iota), Eq (r2 (skS.0 2 a) (skS.0 16 a_1)) True % 5.36/5.53 Clause #272 (by superposition #[265, 233]): ∀ (a a_1 a_2 : Iota), Or (Eq (skS.0 2 a) (skS.0 17 a_1 a_2)) (Eq True False) % 5.36/5.53 Clause #279 (by clausification #[272]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 2 a) (skS.0 17 a_1 a_2) % 5.36/5.53 Clause #287 (by superposition #[279, 205]): ∀ (a : Iota), Eq (r1 (skS.0 2 a)) False % 5.36/5.53 Clause #291 (by superposition #[287, 50]): Eq False True % 5.36/5.53 Clause #292 (by clausification #[291]): False % 5.36/5.53 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------