%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUN059+2 : TPTP v9.2.0. Bugfixed v7.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.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:47 PM UTC 2025 % Result : Theorem 8.68s 8.85s % Output : Proof 8.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUN059+2 : TPTP v9.2.0. Bugfixed v7.4.0. % 0.04/0.13 % Command : duper %s % 0.13/0.34 % Computer : n017.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 : Thu Oct 2 11:37:38 EDT 2025 % 0.13/0.34 % CPUTime : % 8.68/8.85 SZS status Theorem for theBenchmark.p % 8.68/8.85 SZS output start Proof for theBenchmark.p % 8.68/8.85 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 % 8.68/8.85 Clause #3 (by assumption #[]): Eq % 8.68/8.85 (∀ (X16 X17 : Iota), % 8.68/8.85 Exists fun Y23 => ∀ (X18 : Iota), Or (And (Not (r4 X16 X17 X18)) (Ne X18 Y23)) (And (r4 X16 X17 X18) (Eq X18 Y23))) % 8.68/8.85 True % 8.68/8.85 Clause #7 (by assumption #[]): Eq (∀ (X4 : Iota), Exists fun Y9 => And (Exists fun Y16 => And (r1 Y16) (r3 X4 Y16 Y9)) (Eq Y9 X4)) True % 8.68/8.85 Clause #8 (by assumption #[]): Eq % 8.68/8.85 (∀ (X5 : Iota), % 8.68/8.85 Exists fun Y8 => And (Exists fun Y17 => And (r1 Y17) (r4 X5 Y17 Y8)) (Exists fun Y18 => And (r1 Y18) (Eq Y8 Y18))) % 8.68/8.85 True % 8.68/8.85 Clause #11 (by assumption #[]): Eq % 8.68/8.85 (Not % 8.68/8.85 (Exists fun Y1 => % 8.68/8.85 Exists fun Y3 => % 8.68/8.85 Exists fun Y2 => % 8.68/8.85 Exists fun Y4 => % 8.68/8.85 And (Exists fun Y5 => And (r4 Y2 Y2 Y5) (Eq Y4 Y5)) % 8.68/8.85 (Exists fun Y6 => And (r4 Y3 Y3 Y6) (Exists fun Y7 => And (r4 Y1 Y1 Y7) (r3 Y7 Y6 Y4))))) % 8.68/8.85 True % 8.68/8.85 Clause #21 (by clausification #[7]): ∀ (a : Iota), Eq (Exists fun Y9 => And (Exists fun Y16 => And (r1 Y16) (r3 a Y16 Y9)) (Eq Y9 a)) True % 8.68/8.85 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Eq (And (Exists fun Y16 => And (r1 Y16) (r3 a Y16 (skS.0 0 a a_1))) (Eq (skS.0 0 a a_1) a)) True % 8.68/8.85 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (Eq (skS.0 0 a a_1) a) True % 8.68/8.85 Clause #24 (by clausification #[22]): ∀ (a a_1 : Iota), Eq (Exists fun Y16 => And (r1 Y16) (r3 a Y16 (skS.0 0 a a_1))) True % 8.68/8.85 Clause #25 (by clausification #[23]): ∀ (a a_1 : Iota), Eq (skS.0 0 a a_1) a % 8.68/8.85 Clause #26 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), Eq (And (r1 (skS.0 1 a a_1 a_2)) (r3 a (skS.0 1 a a_1 a_2) (skS.0 0 a a_1))) True % 8.68/8.85 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Eq (r3 a (skS.0 1 a a_1 a_2) (skS.0 0 a a_1)) True % 8.68/8.85 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 1 a a_1 a_2)) True % 8.68/8.85 Clause #29 (by forward demodulation #[27, 25]): ∀ (a a_1 a_2 : Iota), Eq (r3 a (skS.0 1 a a_1 a_2) a) True % 8.68/8.85 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 % 8.68/8.85 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 % 8.68/8.85 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) % 8.68/8.85 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) % 8.68/8.85 Clause #55 (by clausification #[34]): ∀ (a a_1 : Iota), Or (Eq (Not (r1 a)) True) (Eq (Eq a (skS.0 2 a_1)) True) % 8.68/8.85 Clause #57 (by clausification #[55]): ∀ (a a_1 : Iota), Or (Eq (Eq a (skS.0 2 a_1)) True) (Eq (r1 a) False) % 8.68/8.85 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), Or (Eq (r1 a) False) (Eq a (skS.0 2 a_1)) % 8.68/8.85 Clause #59 (by superposition #[58, 28]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (skS.0 1 a a_1 a_2) (skS.0 2 a_3)) (Eq False True) % 8.68/8.85 Clause #74 (by clausification #[59]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 1 a a_1 a_2) (skS.0 2 a_3) % 8.68/8.85 Clause #75 (by superposition #[74, 29]): ∀ (a a_1 : Iota), Eq (r3 a (skS.0 2 a_1) a) True % 8.68/8.85 Clause #79 (by clausification #[3]): ∀ (a : Iota), % 8.68/8.85 Eq % 8.68/8.85 (∀ (X17 : Iota), % 8.68/8.85 Exists fun Y23 => ∀ (X18 : Iota), Or (And (Not (r4 a X17 X18)) (Ne X18 Y23)) (And (r4 a X17 X18) (Eq X18 Y23))) % 8.68/8.85 True % 8.68/8.85 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), % 8.68/8.85 Eq (Exists fun Y23 => ∀ (X18 : Iota), Or (And (Not (r4 a a_1 X18)) (Ne X18 Y23)) (And (r4 a a_1 X18) (Eq X18 Y23))) % 8.68/8.85 True % 8.68/8.85 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : Iota), % 8.68/8.85 Eq % 8.68/8.85 (∀ (X18 : Iota), % 8.68/8.85 Or (And (Not (r4 a a_1 X18)) (Ne X18 (skS.0 5 a a_1 a_2))) (And (r4 a a_1 X18) (Eq X18 (skS.0 5 a a_1 a_2)))) % 8.68/8.85 True % 8.68/8.85 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 a_3 : Iota), % 8.68/8.85 Eq (Or (And (Not (r4 a a_1 a_2)) (Ne a_2 (skS.0 5 a a_1 a_3))) (And (r4 a a_1 a_2) (Eq a_2 (skS.0 5 a a_1 a_3)))) True % 8.68/8.88 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 8.68/8.88 Or (Eq (And (Not (r4 a a_1 a_2)) (Ne a_2 (skS.0 5 a a_1 a_3))) True) % 8.68/8.88 (Eq (And (r4 a a_1 a_2) (Eq a_2 (skS.0 5 a a_1 a_3))) True) % 8.68/8.88 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 : Iota), % 8.68/8.88 Or (Eq (And (r4 a a_1 a_2) (Eq a_2 (skS.0 5 a a_1 a_3))) True) (Eq (Ne a_2 (skS.0 5 a a_1 a_3)) True) % 8.68/8.88 Clause #85 (by clausification #[83]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (And (r4 a a_1 a_2) (Eq a_2 (skS.0 5 a a_1 a_3))) True) (Eq (Not (r4 a a_1 a_2)) True) % 8.68/8.88 Clause #87 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (Ne a (skS.0 5 a_1 a_2 a_3)) True) (Eq (r4 a_1 a_2 a) True) % 8.68/8.88 Clause #90 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r4 a a_1 a_2) True) (Ne a_2 (skS.0 5 a a_1 a_3)) % 8.68/8.88 Clause #91 (by destructive equality resolution #[90]): ∀ (a a_1 a_2 : Iota), Eq (r4 a a_1 (skS.0 5 a a_1 a_2)) True % 8.68/8.88 Clause #137 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (Not (r4 a a_1 a_2)) True) (Eq (Eq a_2 (skS.0 5 a a_1 a_3)) True) % 8.68/8.88 Clause #139 (by clausification #[137]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (Eq a (skS.0 5 a_1 a_2 a_3)) True) (Eq (r4 a_1 a_2 a) False) % 8.68/8.88 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r4 a a_1 a_2) False) (Eq a_2 (skS.0 5 a a_1 a_3)) % 8.68/8.88 Clause #148 (by clausification #[8]): ∀ (a : Iota), % 8.68/8.88 Eq (Exists fun Y8 => And (Exists fun Y17 => And (r1 Y17) (r4 a Y17 Y8)) (Exists fun Y18 => And (r1 Y18) (Eq Y8 Y18))) % 8.68/8.88 True % 8.68/8.88 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), % 8.68/8.88 Eq % 8.68/8.88 (And (Exists fun Y17 => And (r1 Y17) (r4 a Y17 (skS.0 10 a a_1))) % 8.68/8.88 (Exists fun Y18 => And (r1 Y18) (Eq (skS.0 10 a a_1) Y18))) % 8.68/8.88 True % 8.68/8.88 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), Eq (Exists fun Y18 => And (r1 Y18) (Eq (skS.0 10 a a_1) Y18)) True % 8.68/8.88 Clause #151 (by clausification #[149]): ∀ (a a_1 : Iota), Eq (Exists fun Y17 => And (r1 Y17) (r4 a Y17 (skS.0 10 a a_1))) True % 8.68/8.88 Clause #152 (by clausification #[150]): ∀ (a a_1 a_2 : Iota), Eq (And (r1 (skS.0 11 a a_1 a_2)) (Eq (skS.0 10 a a_1) (skS.0 11 a a_1 a_2))) True % 8.68/8.88 Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 : Iota), Eq (Eq (skS.0 10 a a_1) (skS.0 11 a a_1 a_2)) True % 8.68/8.88 Clause #154 (by clausification #[152]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 11 a a_1 a_2)) True % 8.68/8.88 Clause #155 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 10 a a_1) (skS.0 11 a a_1 a_2) % 8.68/8.88 Clause #156 (by forward demodulation #[154, 155]): ∀ (a a_1 : Iota), Eq (r1 (skS.0 10 a a_1)) True % 8.68/8.88 Clause #157 (by superposition #[156, 58]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (skS.0 10 a a_1) (skS.0 2 a_2)) % 8.68/8.88 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 10 a a_1) (skS.0 2 a_2) % 8.68/8.88 Clause #161 (by superposition #[158, 158]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 10 a a_1) (skS.0 10 a_2 a_3) % 8.68/8.88 Clause #173 (by clausification #[151]): ∀ (a a_1 a_2 : Iota), Eq (And (r1 (skS.0 15 a a_1 a_2)) (r4 a (skS.0 15 a a_1 a_2) (skS.0 10 a a_1))) True % 8.68/8.88 Clause #174 (by clausification #[173]): ∀ (a a_1 a_2 : Iota), Eq (r4 a (skS.0 15 a a_1 a_2) (skS.0 10 a a_1)) True % 8.68/8.88 Clause #175 (by clausification #[173]): ∀ (a a_1 a_2 : Iota), Eq (r1 (skS.0 15 a a_1 a_2)) True % 8.68/8.88 Clause #177 (by superposition #[174, 161]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (r4 a (skS.0 15 a a_1 a_2) (skS.0 10 a_3 a_4)) True % 8.68/8.88 Clause #178 (by superposition #[175, 58]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (skS.0 15 a a_1 a_2) (skS.0 2 a_3)) % 8.68/8.88 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 15 a a_1 a_2) (skS.0 2 a_3) % 8.68/8.88 Clause #182 (by superposition #[179, 179]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (skS.0 15 a a_1 a_2) (skS.0 15 a_3 a_4 a_5) % 8.68/8.88 Clause #183 (by clausification #[11]): Eq % 8.68/8.88 (Exists fun Y1 => % 8.68/8.88 Exists fun Y3 => % 8.68/8.88 Exists fun Y2 => % 8.68/8.88 Exists fun Y4 => % 8.68/8.88 And (Exists fun Y5 => And (r4 Y2 Y2 Y5) (Eq Y4 Y5)) % 8.68/8.88 (Exists fun Y6 => And (r4 Y3 Y3 Y6) (Exists fun Y7 => And (r4 Y1 Y1 Y7) (r3 Y7 Y6 Y4)))) % 8.68/8.88 False % 8.68/8.88 Clause #184 (by clausification #[183]): ∀ (a : Iota), % 8.68/8.90 Eq % 8.68/8.90 (Exists fun Y3 => % 8.68/8.90 Exists fun Y2 => % 8.68/8.90 Exists fun Y4 => % 8.68/8.90 And (Exists fun Y5 => And (r4 Y2 Y2 Y5) (Eq Y4 Y5)) % 8.68/8.90 (Exists fun Y6 => And (r4 Y3 Y3 Y6) (Exists fun Y7 => And (r4 a a Y7) (r3 Y7 Y6 Y4)))) % 8.68/8.90 False % 8.68/8.90 Clause #185 (by clausification #[184]): ∀ (a a_1 : Iota), % 8.68/8.90 Eq % 8.68/8.90 (Exists fun Y2 => % 8.68/8.90 Exists fun Y4 => % 8.68/8.90 And (Exists fun Y5 => And (r4 Y2 Y2 Y5) (Eq Y4 Y5)) % 8.68/8.90 (Exists fun Y6 => And (r4 a a Y6) (Exists fun Y7 => And (r4 a_1 a_1 Y7) (r3 Y7 Y6 Y4)))) % 8.68/8.90 False % 8.68/8.90 Clause #186 (by clausification #[185]): ∀ (a a_1 a_2 : Iota), % 8.68/8.90 Eq % 8.68/8.90 (Exists fun Y4 => % 8.68/8.90 And (Exists fun Y5 => And (r4 a a Y5) (Eq Y4 Y5)) % 8.68/8.90 (Exists fun Y6 => And (r4 a_1 a_1 Y6) (Exists fun Y7 => And (r4 a_2 a_2 Y7) (r3 Y7 Y6 Y4)))) % 8.68/8.90 False % 8.68/8.90 Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 a_3 : Iota), % 8.68/8.90 Eq % 8.68/8.90 (And (Exists fun Y5 => And (r4 a a Y5) (Eq a_1 Y5)) % 8.68/8.90 (Exists fun Y6 => And (r4 a_2 a_2 Y6) (Exists fun Y7 => And (r4 a_3 a_3 Y7) (r3 Y7 Y6 a_1)))) % 8.68/8.90 False % 8.68/8.90 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), % 8.68/8.90 Or (Eq (Exists fun Y5 => And (r4 a a Y5) (Eq a_1 Y5)) False) % 8.68/8.90 (Eq (Exists fun Y6 => And (r4 a_2 a_2 Y6) (Exists fun Y7 => And (r4 a_3 a_3 Y7) (r3 Y7 Y6 a_1))) False) % 8.68/8.90 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.68/8.90 Or (Eq (Exists fun Y6 => And (r4 a a Y6) (Exists fun Y7 => And (r4 a_1 a_1 Y7) (r3 Y7 Y6 a_2))) False) % 8.68/8.90 (Eq (And (r4 a_3 a_3 a_4) (Eq a_2 a_4)) False) % 8.68/8.90 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.68/8.90 Or (Eq (And (r4 a a a_1) (Eq a_2 a_1)) False) % 8.68/8.90 (Eq (And (r4 a_3 a_3 a_4) (Exists fun Y7 => And (r4 a_5 a_5 Y7) (r3 Y7 a_4 a_2))) False) % 8.68/8.90 Clause #191 (by clausification #[190]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.68/8.90 Or (Eq (And (r4 a a a_1) (Exists fun Y7 => And (r4 a_2 a_2 Y7) (r3 Y7 a_1 a_3))) False) % 8.68/8.90 (Or (Eq (r4 a_4 a_4 a_5) False) (Eq (Eq a_3 a_5) False)) % 8.68/8.90 Clause #192 (by clausification #[191]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.68/8.90 Or (Eq (r4 a a a_1) False) % 8.68/8.90 (Or (Eq (Eq a_2 a_1) False) % 8.68/8.90 (Or (Eq (r4 a_3 a_3 a_4) False) (Eq (Exists fun Y7 => And (r4 a_5 a_5 Y7) (r3 Y7 a_4 a_2)) False))) % 8.68/8.90 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.68/8.90 Or (Eq (r4 a a a_1) False) % 8.68/8.90 (Or (Eq (r4 a_2 a_2 a_3) False) (Or (Eq (Exists fun Y7 => And (r4 a_4 a_4 Y7) (r3 Y7 a_3 a_5)) False) (Ne a_5 a_1))) % 8.68/8.90 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.68/8.90 Or (Eq (r4 a a a_1) False) % 8.68/8.90 (Or (Eq (r4 a_2 a_2 a_3) False) (Or (Ne a_4 a_1) (Eq (And (r4 a_5 a_5 a_6) (r3 a_6 a_3 a_4)) False))) % 8.68/8.90 Clause #195 (by clausification #[194]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.68/8.90 Or (Eq (r4 a a a_1) False) % 8.68/8.90 (Or (Eq (r4 a_2 a_2 a_3) False) (Or (Ne a_4 a_1) (Or (Eq (r4 a_5 a_5 a_6) False) (Eq (r3 a_6 a_3 a_4) False)))) % 8.68/8.90 Clause #196 (by destructive equality resolution #[195]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.68/8.90 Or (Eq (r4 a a a_1) False) % 8.68/8.90 (Or (Eq (r4 a_2 a_2 a_3) False) (Or (Eq (r4 a_4 a_4 a_5) False) (Eq (r3 a_5 a_3 a_1) False))) % 8.68/8.90 Clause #199 (by superposition #[177, 140]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (skS.0 10 a a_1) (skS.0 5 a_2 (skS.0 15 a_2 a_3 a_4) a_5)) % 8.68/8.90 Clause #362 (by clausification #[199]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (skS.0 10 a a_1) (skS.0 5 a_2 (skS.0 15 a_2 a_3 a_4) a_5) % 8.68/8.90 Clause #363 (by superposition #[362, 156]): ∀ (a a_1 a_2 a_3 : Iota), Eq (r1 (skS.0 5 a (skS.0 15 a a_1 a_2) a_3)) True % 8.68/8.90 Clause #375 (by superposition #[363, 182]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (r1 (skS.0 5 a (skS.0 15 a_1 a_2 a_3) a_4)) True % 8.68/8.90 Clause #376 (by superposition #[375, 58]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (skS.0 5 a (skS.0 15 a_1 a_2 a_3) a_4) (skS.0 2 a_5)) % 8.68/8.90 Clause #450 (by clausification #[376]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (skS.0 5 a (skS.0 15 a_1 a_2 a_3) a_4) (skS.0 2 a_5) % 8.68/8.90 Clause #451 (by superposition #[450, 91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (r4 a (skS.0 15 a_1 a_2 a_3) (skS.0 2 a_4)) True % 8.68/8.90 Clause #476 (by superposition #[451, 196]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.68/8.91 Or (Eq True False) (Or (Eq (r4 a a a_1) False) (Or (Eq (r4 a_2 a_2 a_3) False) (Eq (r3 a_3 a_1 (skS.0 2 a_4)) False))) % 8.68/8.91 Clause #482 (by clausification #[476]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.68/8.91 Or (Eq (r4 a a a_1) False) (Or (Eq (r4 a_2 a_2 a_3) False) (Eq (r3 a_3 a_1 (skS.0 2 a_4)) False)) % 8.68/8.91 Clause #486 (by superposition #[482, 451]): ∀ (a a_1 a_2 a_3 : Iota), % 8.68/8.91 Or (Eq (r4 a a a_1) False) (Or (Eq (r3 a_1 (skS.0 2 a_2) (skS.0 2 a_3)) False) (Eq False True)) % 8.68/8.91 Clause #489 (by clausification #[486]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (r4 a a a_1) False) (Eq (r3 a_1 (skS.0 2 a_2) (skS.0 2 a_3)) False) % 8.68/8.91 Clause #493 (by superposition #[489, 451]): ∀ (a a_1 a_2 : Iota), Or (Eq (r3 (skS.0 2 a) (skS.0 2 a_1) (skS.0 2 a_2)) False) (Eq False True) % 8.68/8.91 Clause #503 (by clausification #[493]): ∀ (a a_1 a_2 : Iota), Eq (r3 (skS.0 2 a) (skS.0 2 a_1) (skS.0 2 a_2)) False % 8.68/8.91 Clause #504 (by superposition #[503, 75]): Eq False True % 8.68/8.91 Clause #505 (by clausification #[504]): False % 8.68/8.91 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------