%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUN087+1 : TPTP v9.2.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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:51 PM UTC 2025 % Result : Theorem 181.22s 181.40s % Output : Proof 181.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : NUN087+1 : TPTP v9.2.0. Released v7.3.0. % 0.14/0.14 % Command : duper %s % 0.14/0.35 % Computer : n025.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 11:30:53 EDT 2025 % 0.20/0.35 % CPUTime : % 181.22/181.40 SZS status Theorem for theBenchmark.p % 181.22/181.40 SZS output start Proof for theBenchmark.p % 181.22/181.40 Clause #0 (by assumption #[]): Eq (Exists fun Y24 => ∀ (X19 : Iota), Or (And (id X19 Y24) (r1 X19)) (And (Not (r1 X19)) (Not (id X19 Y24)))) True % 181.22/181.40 Clause #4 (by assumption #[]): Eq (∀ (X20 : Iota), id X20 X20) True % 181.22/181.40 Clause #5 (by assumption #[]): Eq (∀ (X21 X22 : Iota), Or (Not (id X21 X22)) (id X22 X21)) True % 181.22/181.40 Clause #7 (by assumption #[]): Eq (∀ (X26 X27 : Iota), Or (Or (Not (id X26 X27)) (And (Not (r1 X26)) (Not (r1 X27)))) (And (r1 X26) (r1 X27))) True % 181.22/181.40 Clause #10 (by assumption #[]): Eq % 181.22/181.40 (∀ (X38 X39 X40 X41 X42 X43 : Iota), % 181.22/181.40 Or % 181.22/181.40 (Or (Or (Or (Not (id X38 X41)) (Not (id X39 X42))) (Not (id X40 X43))) % 181.22/181.40 (And (Not (r4 X38 X39 X40)) (Not (r4 X41 X42 X43)))) % 181.22/181.40 (And (r4 X38 X39 X40) (r4 X41 X42 X43))) % 181.22/181.40 True % 181.22/181.40 Clause #15 (by assumption #[]): Eq % 181.22/181.40 (∀ (X5 : Iota), % 181.22/181.40 Exists fun Y8 => And (Exists fun Y17 => And (r1 Y17) (r4 X5 Y17 Y8)) (Exists fun Y18 => And (id Y8 Y18) (r1 Y18))) % 181.22/181.40 True % 181.22/181.40 Clause #18 (by assumption #[]): Eq (Not (Exists fun Y1 => And (Exists fun Y2 => And (r1 Y2) (r4 Y2 Y2 Y1)) (Exists fun Y3 => And (id Y1 Y3) (r1 Y3)))) % 181.22/181.40 True % 181.22/181.40 Clause #19 (by clausification #[4]): ∀ (a : Iota), Eq (id a a) True % 181.22/181.40 Clause #20 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (X22 : Iota), Or (Not (id a X22)) (id X22 a)) True % 181.22/181.40 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), Eq (Or (Not (id a a_1)) (id a_1 a)) True % 181.22/181.40 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Or (Eq (Not (id a a_1)) True) (Eq (id a_1 a) True) % 181.22/181.40 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Or (Eq (id a a_1) True) (Eq (id a_1 a) False) % 181.22/181.40 Clause #34 (by clausification #[0]): ∀ (a : Iota), % 181.22/181.40 Eq (∀ (X19 : Iota), Or (And (id X19 (skS.0 0 a)) (r1 X19)) (And (Not (r1 X19)) (Not (id X19 (skS.0 0 a))))) True % 181.22/181.40 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Eq (Or (And (id a (skS.0 0 a_1)) (r1 a)) (And (Not (r1 a)) (Not (id a (skS.0 0 a_1))))) True % 181.22/181.40 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), Or (Eq (And (id a (skS.0 0 a_1)) (r1 a)) True) (Eq (And (Not (r1 a)) (Not (id a (skS.0 0 a_1)))) True) % 181.22/181.40 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), Or (Eq (And (Not (r1 a)) (Not (id a (skS.0 0 a_1)))) True) (Eq (r1 a) True) % 181.22/181.40 Clause #38 (by clausification #[36]): ∀ (a a_1 : Iota), Or (Eq (And (Not (r1 a)) (Not (id a (skS.0 0 a_1)))) True) (Eq (id a (skS.0 0 a_1)) True) % 181.22/181.40 Clause #39 (by clausification #[37]): ∀ (a a_1 : Iota), Or (Eq (r1 a) True) (Eq (Not (id a (skS.0 0 a_1))) True) % 181.22/181.40 Clause #41 (by clausification #[39]): ∀ (a a_1 : Iota), Or (Eq (r1 a) True) (Eq (id a (skS.0 0 a_1)) False) % 181.22/181.40 Clause #42 (by superposition #[41, 19]): ∀ (a : Iota), Or (Eq (r1 (skS.0 0 a)) True) (Eq False True) % 181.22/181.40 Clause #44 (by clausification #[42]): ∀ (a : Iota), Eq (r1 (skS.0 0 a)) True % 181.22/181.40 Clause #120 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (X27 : Iota), Or (Or (Not (id a X27)) (And (Not (r1 a)) (Not (r1 X27)))) (And (r1 a) (r1 X27))) True % 181.22/181.40 Clause #121 (by clausification #[120]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (id a a_1)) (And (Not (r1 a)) (Not (r1 a_1)))) (And (r1 a) (r1 a_1))) True % 181.22/181.40 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (id a a_1)) (And (Not (r1 a)) (Not (r1 a_1)))) True) (Eq (And (r1 a) (r1 a_1)) True) % 181.22/181.40 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 181.22/181.40 Or (Eq (And (r1 a) (r1 a_1)) True) (Or (Eq (Not (id a a_1)) True) (Eq (And (Not (r1 a)) (Not (r1 a_1))) True)) % 181.22/181.40 Clause #125 (by clausification #[123]): ∀ (a a_1 : Iota), Or (Eq (Not (id a a_1)) True) (Or (Eq (And (Not (r1 a)) (Not (r1 a_1))) True) (Eq (r1 a) True)) % 181.22/181.40 Clause #153 (by clausification #[125]): ∀ (a a_1 : Iota), Or (Eq (And (Not (r1 a)) (Not (r1 a_1))) True) (Or (Eq (r1 a) True) (Eq (id a a_1) False)) % 181.22/181.40 Clause #154 (by clausification #[153]): ∀ (a a_1 : Iota), Or (Eq (r1 a) True) (Or (Eq (id a a_1) False) (Eq (Not (r1 a_1)) True)) % 181.22/181.40 Clause #156 (by clausification #[154]): ∀ (a a_1 : Iota), Or (Eq (r1 a) True) (Or (Eq (id a a_1) False) (Eq (r1 a_1) False)) % 181.22/181.40 Clause #193 (by clausification #[10]): ∀ (a : Iota), % 181.22/181.40 Eq % 181.22/181.43 (∀ (X39 X40 X41 X42 X43 : Iota), % 181.22/181.43 Or % 181.22/181.43 (Or (Or (Or (Not (id a X41)) (Not (id X39 X42))) (Not (id X40 X43))) % 181.22/181.43 (And (Not (r4 a X39 X40)) (Not (r4 X41 X42 X43)))) % 181.22/181.43 (And (r4 a X39 X40) (r4 X41 X42 X43))) % 181.22/181.43 True % 181.22/181.43 Clause #194 (by clausification #[193]): ∀ (a a_1 : Iota), % 181.22/181.43 Eq % 181.22/181.43 (∀ (X40 X41 X42 X43 : Iota), % 181.22/181.43 Or % 181.22/181.43 (Or (Or (Or (Not (id a X41)) (Not (id a_1 X42))) (Not (id X40 X43))) % 181.22/181.43 (And (Not (r4 a a_1 X40)) (Not (r4 X41 X42 X43)))) % 181.22/181.43 (And (r4 a a_1 X40) (r4 X41 X42 X43))) % 181.22/181.43 True % 181.22/181.43 Clause #195 (by clausification #[194]): ∀ (a a_1 a_2 : Iota), % 181.22/181.43 Eq % 181.22/181.43 (∀ (X41 X42 X43 : Iota), % 181.22/181.43 Or % 181.22/181.43 (Or (Or (Or (Not (id a X41)) (Not (id a_1 X42))) (Not (id a_2 X43))) % 181.22/181.43 (And (Not (r4 a a_1 a_2)) (Not (r4 X41 X42 X43)))) % 181.22/181.43 (And (r4 a a_1 a_2) (r4 X41 X42 X43))) % 181.22/181.43 True % 181.22/181.43 Clause #196 (by clausification #[195]): ∀ (a a_1 a_2 a_3 : Iota), % 181.22/181.43 Eq % 181.22/181.43 (∀ (X42 X43 : Iota), % 181.22/181.43 Or % 181.22/181.43 (Or (Or (Or (Not (id a a_1)) (Not (id a_2 X42))) (Not (id a_3 X43))) % 181.22/181.43 (And (Not (r4 a a_2 a_3)) (Not (r4 a_1 X42 X43)))) % 181.22/181.43 (And (r4 a a_2 a_3) (r4 a_1 X42 X43))) % 181.22/181.43 True % 181.22/181.43 Clause #197 (by clausification #[196]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 181.22/181.43 Eq % 181.22/181.43 (∀ (X43 : Iota), % 181.22/181.43 Or % 181.22/181.43 (Or (Or (Or (Not (id a a_1)) (Not (id a_2 a_3))) (Not (id a_4 X43))) % 181.22/181.43 (And (Not (r4 a a_2 a_4)) (Not (r4 a_1 a_3 X43)))) % 181.22/181.43 (And (r4 a a_2 a_4) (r4 a_1 a_3 X43))) % 181.22/181.43 True % 181.22/181.43 Clause #198 (by clausification #[197]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.22/181.43 Eq % 181.22/181.43 (Or % 181.22/181.43 (Or (Or (Or (Not (id a a_1)) (Not (id a_2 a_3))) (Not (id a_4 a_5))) % 181.22/181.43 (And (Not (r4 a a_2 a_4)) (Not (r4 a_1 a_3 a_5)))) % 181.22/181.43 (And (r4 a a_2 a_4) (r4 a_1 a_3 a_5))) % 181.22/181.43 True % 181.22/181.43 Clause #199 (by clausification #[198]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.22/181.43 Or % 181.22/181.43 (Eq % 181.22/181.43 (Or (Or (Or (Not (id a a_1)) (Not (id a_2 a_3))) (Not (id a_4 a_5))) % 181.22/181.43 (And (Not (r4 a a_2 a_4)) (Not (r4 a_1 a_3 a_5)))) % 181.22/181.43 True) % 181.22/181.43 (Eq (And (r4 a a_2 a_4) (r4 a_1 a_3 a_5)) True) % 181.22/181.43 Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.22/181.43 Or (Eq (And (r4 a a_1 a_2) (r4 a_3 a_4 a_5)) True) % 181.22/181.43 (Or (Eq (Or (Or (Not (id a a_3)) (Not (id a_1 a_4))) (Not (id a_2 a_5))) True) % 181.22/181.43 (Eq (And (Not (r4 a a_1 a_2)) (Not (r4 a_3 a_4 a_5))) True)) % 181.22/181.43 Clause #202 (by clausification #[200]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.22/181.43 Or (Eq (Or (Or (Not (id a a_1)) (Not (id a_2 a_3))) (Not (id a_4 a_5))) True) % 181.22/181.43 (Or (Eq (And (Not (r4 a a_2 a_4)) (Not (r4 a_1 a_3 a_5))) True) (Eq (r4 a a_2 a_4) True)) % 181.22/181.43 Clause #309 (by clausification #[15]): ∀ (a : Iota), % 181.22/181.43 Eq (Exists fun Y8 => And (Exists fun Y17 => And (r1 Y17) (r4 a Y17 Y8)) (Exists fun Y18 => And (id Y8 Y18) (r1 Y18))) % 181.22/181.43 True % 181.22/181.43 Clause #310 (by clausification #[309]): ∀ (a a_1 : Iota), % 181.22/181.43 Eq % 181.22/181.43 (And (Exists fun Y17 => And (r1 Y17) (r4 a Y17 (skS.0 10 a a_1))) % 181.22/181.43 (Exists fun Y18 => And (id (skS.0 10 a a_1) Y18) (r1 Y18))) % 181.22/181.43 True % 181.22/181.43 Clause #311 (by clausification #[310]): ∀ (a a_1 : Iota), Eq (Exists fun Y18 => And (id (skS.0 10 a a_1) Y18) (r1 Y18)) True % 181.22/181.43 Clause #312 (by clausification #[310]): ∀ (a a_1 : Iota), Eq (Exists fun Y17 => And (r1 Y17) (r4 a Y17 (skS.0 10 a a_1))) True % 181.22/181.43 Clause #313 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), Eq (And (id (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) (r1 (skS.0 11 a a_1 a_2))) True % 181.22/181.43 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 11 a a_1 a_2)) True % 181.22/181.43 Clause #315 (by clausification #[313]): ∀ (a a_1 a_2 : Iota), Eq (id (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) True % 181.22/181.43 Clause #318 (by clausification #[312]): ∀ (a a_1 a_2 : Iota), Eq (And (r1 (skS.0 12 a a_1 a_2)) (r4 a (skS.0 12 a a_1 a_2) (skS.0 10 a a_1))) True % 181.22/181.43 Clause #319 (by clausification #[318]): ∀ (a a_1 a_2 : Iota), Eq (r4 a (skS.0 12 a a_1 a_2) (skS.0 10 a a_1)) True % 181.22/181.43 Clause #320 (by clausification #[318]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 12 a a_1 a_2)) True % 181.22/181.43 Clause #327 (by superposition #[315, 156]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 10 a a_1)) True) (Or (Eq True False) (Eq (r1 (skS.0 11 a a_1 a_2)) False)) % 181.22/181.43 Clause #372 (by clausification #[18]): Eq (Exists fun Y1 => And (Exists fun Y2 => And (r1 Y2) (r4 Y2 Y2 Y1)) (Exists fun Y3 => And (id Y1 Y3) (r1 Y3))) False % 181.26/181.45 Clause #373 (by clausification #[372]): ∀ (a : Iota), Eq (And (Exists fun Y2 => And (r1 Y2) (r4 Y2 Y2 a)) (Exists fun Y3 => And (id a Y3) (r1 Y3))) False % 181.26/181.45 Clause #374 (by clausification #[373]): ∀ (a : Iota), % 181.26/181.45 Or (Eq (Exists fun Y2 => And (r1 Y2) (r4 Y2 Y2 a)) False) (Eq (Exists fun Y3 => And (id a Y3) (r1 Y3)) False) % 181.26/181.45 Clause #375 (by clausification #[374]): ∀ (a a_1 : Iota), Or (Eq (Exists fun Y3 => And (id a Y3) (r1 Y3)) False) (Eq (And (r1 a_1) (r4 a_1 a_1 a)) False) % 181.26/181.45 Clause #376 (by clausification #[375]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (r1 a) (r4 a a a_1)) False) (Eq (And (id a_1 a_2) (r1 a_2)) False) % 181.26/181.45 Clause #377 (by clausification #[376]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (id a a_1) (r1 a_1)) False) (Or (Eq (r1 a_2) False) (Eq (r4 a_2 a_2 a) False)) % 181.26/181.45 Clause #378 (by clausification #[377]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 a) False) (Or (Eq (r4 a a a_1) False) (Or (Eq (id a_1 a_2) False) (Eq (r1 a_2) False))) % 181.26/181.45 Clause #379 (by superposition #[378, 44]): ∀ (a a_1 a_2 : Iota), % 181.26/181.45 Or (Eq (r4 (skS.0 0 a) (skS.0 0 a) a_1) False) (Or (Eq (id a_1 a_2) False) (Or (Eq (r1 a_2) False) (Eq False True))) % 181.26/181.45 Clause #395 (by clausification #[38]): ∀ (a a_1 : Iota), Or (Eq (id a (skS.0 0 a_1)) True) (Eq (Not (r1 a)) True) % 181.26/181.45 Clause #397 (by clausification #[395]): ∀ (a a_1 : Iota), Or (Eq (id a (skS.0 0 a_1)) True) (Eq (r1 a) False) % 181.26/181.45 Clause #403 (by superposition #[397, 320]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (id (skS.0 12 a a_1 a_2) (skS.0 0 a_3)) True) (Eq False True) % 181.26/181.45 Clause #480 (by clausification #[403]): ∀ (a a_1 a_2 a_3 : Iota), Eq (id (skS.0 12 a a_1 a_2) (skS.0 0 a_3)) True % 181.26/181.45 Clause #482 (by superposition #[480, 23]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (id (skS.0 0 a) (skS.0 12 a_1 a_2 a_3)) True) (Eq True False) % 181.26/181.45 Clause #491 (by clausification #[482]): ∀ (a a_1 a_2 a_3 : Iota), Eq (id (skS.0 0 a) (skS.0 12 a_1 a_2 a_3)) True % 181.26/181.45 Clause #677 (by clausification #[202]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (And (Not (r4 a a_1 a_2)) (Not (r4 a_3 a_4 a_5))) True) % 181.26/181.45 (Or (Eq (r4 a a_1 a_2) True) (Or (Eq (Or (Not (id a a_3)) (Not (id a_1 a_4))) True) (Eq (Not (id a_2 a_5)) True))) % 181.26/181.45 Clause #678 (by clausification #[677]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (Or (Not (id a a_3)) (Not (id a_1 a_4))) True) % 181.26/181.45 (Or (Eq (Not (id a_2 a_5)) True) (Eq (Not (r4 a_3 a_4 a_5)) True))) % 181.26/181.45 Clause #680 (by clausification #[678]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (Not (id a_2 a_3)) True) % 181.26/181.45 (Or (Eq (Not (r4 a_4 a_5 a_3)) True) (Or (Eq (Not (id a a_4)) True) (Eq (Not (id a_1 a_5)) True)))) % 181.26/181.45 Clause #681 (by clausification #[680]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (Not (r4 a_3 a_4 a_5)) True) % 181.26/181.45 (Or (Eq (Not (id a a_3)) True) (Or (Eq (Not (id a_1 a_4)) True) (Eq (id a_2 a_5) False)))) % 181.26/181.45 Clause #682 (by clausification #[681]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (Not (id a a_3)) True) % 181.26/181.45 (Or (Eq (Not (id a_1 a_4)) True) (Or (Eq (id a_2 a_5) False) (Eq (r4 a_3 a_4 a_5) False)))) % 181.26/181.45 Clause #683 (by clausification #[682]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (Not (id a_1 a_3)) True) % 181.26/181.45 (Or (Eq (id a_2 a_4) False) (Or (Eq (r4 a_5 a_3 a_4) False) (Eq (id a a_5) False)))) % 181.26/181.45 Clause #684 (by clausification #[683]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (id a_2 a_3) False) (Or (Eq (r4 a_4 a_5 a_3) False) (Or (Eq (id a a_4) False) (Eq (id a_1 a_5) False)))) % 181.26/181.45 Clause #703 (by superposition #[684, 19]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) % 181.26/181.45 (Or (Eq (r4 a_3 a_4 a_2) False) (Or (Eq (id a a_3) False) (Or (Eq (id a_1 a_4) False) (Eq False True)))) % 181.26/181.45 Clause #704 (by clausification #[703]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 181.26/181.45 Or (Eq (r4 a a_1 a_2) True) (Or (Eq (r4 a_3 a_4 a_2) False) (Or (Eq (id a a_3) False) (Eq (id a_1 a_4) False))) % 181.53/181.76 Clause #705 (by superposition #[704, 319]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 181.53/181.76 Or (Eq (r4 a a_1 (skS.0 10 a_2 a_3)) True) % 181.53/181.76 (Or (Eq (id a a_2) False) (Or (Eq (id a_1 (skS.0 12 a_2 a_3 a_4)) False) (Eq False True))) % 181.53/181.76 Clause #729 (by clausification #[327]): ∀ (a a_1 a_2 : Iota), Or (Eq (r1 (skS.0 10 a a_1)) True) (Eq (r1 (skS.0 11 a a_1 a_2)) False) % 181.53/181.76 Clause #730 (by superposition #[729, 314]): ∀ (a a_1 : Iota), Or (Eq (r1 (skS.0 10 a a_1)) True) (Eq False True) % 181.53/181.76 Clause #731 (by clausification #[730]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 10 a a_1)) True % 181.53/181.76 Clause #736 (by superposition #[731, 397]): ∀ (a a_1 a_2 : Iota), Or (Eq (id (skS.0 10 a a_1) (skS.0 0 a_2)) True) (Eq True False) % 181.53/181.76 Clause #761 (by clausification #[736]): ∀ (a a_1 a_2 : Iota), Eq (id (skS.0 10 a a_1) (skS.0 0 a_2)) True % 181.53/181.76 Clause #1342 (by clausification #[379]): ∀ (a a_1 a_2 : Iota), Or (Eq (r4 (skS.0 0 a) (skS.0 0 a) a_1) False) (Or (Eq (id a_1 a_2) False) (Eq (r1 a_2) False)) % 181.53/181.76 Clause #29678 (by clausification #[705]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 181.53/181.76 Or (Eq (r4 a a_1 (skS.0 10 a_2 a_3)) True) (Or (Eq (id a a_2) False) (Eq (id a_1 (skS.0 12 a_2 a_3 a_4)) False)) % 181.53/181.76 Clause #29838 (by superposition #[29678, 19]): ∀ (a a_1 a_2 a_3 : Iota), % 181.53/181.76 Or (Eq (r4 a a_1 (skS.0 10 a a_2)) True) (Or (Eq (id a_1 (skS.0 12 a a_2 a_3)) False) (Eq False True)) % 181.53/181.76 Clause #29839 (by clausification #[29838]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r4 a a_1 (skS.0 10 a a_2)) True) (Eq (id a_1 (skS.0 12 a a_2 a_3)) False) % 181.53/181.76 Clause #29840 (by superposition #[29839, 491]): ∀ (a a_1 a_2 : Iota), Or (Eq (r4 a (skS.0 0 a_1) (skS.0 10 a a_2)) True) (Eq False True) % 181.53/181.76 Clause #29876 (by clausification #[29840]): ∀ (a a_1 a_2 : Iota), Eq (r4 a (skS.0 0 a_1) (skS.0 10 a a_2)) True % 181.53/181.76 Clause #29878 (by superposition #[29876, 1342]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Or (Eq (id (skS.0 10 (skS.0 0 a) a_1) a_2) False) (Eq (r1 a_2) False)) % 181.53/181.76 Clause #29894 (by clausification #[29878]): ∀ (a a_1 a_2 : Iota), Or (Eq (id (skS.0 10 (skS.0 0 a) a_1) a_2) False) (Eq (r1 a_2) False) % 181.53/181.76 Clause #29895 (by superposition #[29894, 761]): ∀ (a : Iota), Or (Eq (r1 (skS.0 0 a)) False) (Eq False True) % 181.53/181.76 Clause #29940 (by clausification #[29895]): ∀ (a : Iota), Eq (r1 (skS.0 0 a)) False % 181.53/181.76 Clause #29941 (by superposition #[29940, 44]): Eq False True % 181.53/181.76 Clause #30103 (by clausification #[29941]): False % 181.53/181.76 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------