%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PRO010+2 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:58:07 PM UTC 2025 % Result : Theorem 6.75s 6.96s % Output : Proof 6.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PRO010+2 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n020.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 08:46:53 EDT 2025 % 0.12/0.34 % CPUTime : % 6.75/6.96 SZS status Theorem for theBenchmark.p % 6.75/6.96 SZS output start Proof for theBenchmark.p % 6.75/6.96 Clause #21 (by assumption #[]): Eq % 6.75/6.96 (∀ (X60 X61 X62 : Iota), % 6.75/6.96 And (occurrence_of X60 X62) (leaf_occ X61 X60) → Not (Exists fun X63 => min_precedes X61 X63 X62)) % 6.75/6.96 True % 6.75/6.96 Clause #22 (by assumption #[]): Eq (∀ (X64 X65 X66 : Iota), And (occurrence_of X64 X65) (occurrence_of X64 X66) → Eq X65 X66) True % 6.75/6.96 Clause #31 (by assumption #[]): Eq % 6.75/6.96 (∀ (X95 : Iota), % 6.75/6.96 occurrence_of X95 tptp0 → % 6.75/6.96 Exists fun X96 => % 6.75/6.96 Exists fun X97 => % 6.75/6.96 Exists fun X98 => % 6.75/6.96 And % 6.75/6.96 (And % 6.75/6.96 (And % 6.75/6.96 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 X95)) (occurrence_of X97 tptp4)) % 6.75/6.96 (next_subocc X96 X97 tptp0)) % 6.75/6.96 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 6.75/6.96 (next_subocc X97 X98 tptp0)) % 6.75/6.96 (leaf_occ X98 X95)) % 6.75/6.96 True % 6.75/6.96 Clause #43 (by assumption #[]): Eq (Ne tptp1 tptp2) True % 6.75/6.96 Clause #44 (by assumption #[]): Eq % 6.75/6.96 (Not % 6.75/6.96 (∀ (X99 : Iota), % 6.75/6.96 occurrence_of X99 tptp0 → % 6.75/6.96 Exists fun X100 => % 6.75/6.96 Exists fun X101 => % 6.75/6.96 And % 6.75/6.96 (And (leaf_occ X101 X99) % 6.75/6.96 (occurrence_of X101 tptp1 → % 6.75/6.96 Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes X100 X102 tptp0)))) % 6.75/6.96 (occurrence_of X101 tptp2 → % 6.75/6.96 Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes X100 X103 tptp0))))) % 6.75/6.96 True % 6.75/6.96 Clause #54 (by clausification #[43]): Ne tptp1 tptp2 % 6.75/6.96 Clause #92 (by clausification #[22]): ∀ (a : Iota), Eq (∀ (X65 X66 : Iota), And (occurrence_of a X65) (occurrence_of a X66) → Eq X65 X66) True % 6.75/6.96 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), Eq (∀ (X66 : Iota), And (occurrence_of a a_1) (occurrence_of a X66) → Eq a_1 X66) True % 6.75/6.96 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), Eq (And (occurrence_of a a_1) (occurrence_of a a_2) → Eq a_1 a_2) True % 6.75/6.96 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (occurrence_of a a_1) (occurrence_of a a_2)) False) (Eq (Eq a_1 a_2) True) % 6.75/6.96 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), Or (Eq (Eq a a_1) True) (Or (Eq (occurrence_of a_2 a) False) (Eq (occurrence_of a_2 a_1) False)) % 6.75/6.96 Clause #97 (by clausification #[96]): ∀ (a a_1 a_2 : Iota), Or (Eq (occurrence_of a a_1) False) (Or (Eq (occurrence_of a a_2) False) (Eq a_1 a_2)) % 6.75/6.96 Clause #156 (by clausification #[21]): ∀ (a : Iota), % 6.75/6.96 Eq (∀ (X61 X62 : Iota), And (occurrence_of a X62) (leaf_occ X61 a) → Not (Exists fun X63 => min_precedes X61 X63 X62)) % 6.75/6.96 True % 6.75/6.96 Clause #157 (by clausification #[156]): ∀ (a a_1 : Iota), % 6.75/6.96 Eq (∀ (X62 : Iota), And (occurrence_of a X62) (leaf_occ a_1 a) → Not (Exists fun X63 => min_precedes a_1 X63 X62)) % 6.75/6.96 True % 6.75/6.96 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), % 6.75/6.96 Eq (And (occurrence_of a a_1) (leaf_occ a_2 a) → Not (Exists fun X63 => min_precedes a_2 X63 a_1)) True % 6.75/6.96 Clause #159 (by clausification #[158]): ∀ (a a_1 a_2 : Iota), % 6.75/6.96 Or (Eq (And (occurrence_of a a_1) (leaf_occ a_2 a)) False) % 6.75/6.96 (Eq (Not (Exists fun X63 => min_precedes a_2 X63 a_1)) True) % 6.75/6.96 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), % 6.75/6.96 Or (Eq (Not (Exists fun X63 => min_precedes a X63 a_1)) True) % 6.75/6.96 (Or (Eq (occurrence_of a_2 a_1) False) (Eq (leaf_occ a a_2) False)) % 6.75/6.96 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 : Iota), % 6.75/6.96 Or (Eq (occurrence_of a a_1) False) % 6.75/6.96 (Or (Eq (leaf_occ a_2 a) False) (Eq (Exists fun X63 => min_precedes a_2 X63 a_1) False)) % 6.75/6.96 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.96 Or (Eq (occurrence_of a a_1) False) (Or (Eq (leaf_occ a_2 a) False) (Eq (min_precedes a_2 a_3 a_1) False)) % 6.75/6.96 Clause #274 (by clausification #[31]): ∀ (a : Iota), % 6.75/6.96 Eq % 6.75/6.96 (occurrence_of a tptp0 → % 6.75/6.96 Exists fun X96 => % 6.75/6.96 Exists fun X97 => % 6.75/6.96 Exists fun X98 => % 6.75/6.96 And % 6.75/6.96 (And % 6.75/6.96 (And % 6.75/6.96 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 a)) (occurrence_of X97 tptp4)) % 6.75/6.96 (next_subocc X96 X97 tptp0)) % 6.75/6.97 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 6.75/6.97 (next_subocc X97 X98 tptp0)) % 6.75/6.97 (leaf_occ X98 a)) % 6.75/6.97 True % 6.75/6.97 Clause #275 (by clausification #[274]): ∀ (a : Iota), % 6.75/6.97 Or (Eq (occurrence_of a tptp0) False) % 6.75/6.97 (Eq % 6.75/6.97 (Exists fun X96 => % 6.75/6.97 Exists fun X97 => % 6.75/6.97 Exists fun X98 => % 6.75/6.97 And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 a)) (occurrence_of X97 tptp4)) % 6.75/6.97 (next_subocc X96 X97 tptp0)) % 6.75/6.97 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 6.75/6.97 (next_subocc X97 X98 tptp0)) % 6.75/6.97 (leaf_occ X98 a)) % 6.75/6.97 True) % 6.75/6.97 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), % 6.75/6.97 Or (Eq (occurrence_of a tptp0) False) % 6.75/6.97 (Eq % 6.75/6.97 (Exists fun X97 => % 6.75/6.97 Exists fun X98 => % 6.75/6.97 And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 6.75/6.97 (occurrence_of X97 tptp4)) % 6.75/6.97 (next_subocc (skS.0 13 a a_1) X97 tptp0)) % 6.75/6.97 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 6.75/6.97 (next_subocc X97 X98 tptp0)) % 6.75/6.97 (leaf_occ X98 a)) % 6.75/6.97 True) % 6.75/6.97 Clause #277 (by clausification #[276]): ∀ (a a_1 a_2 : Iota), % 6.75/6.97 Or (Eq (occurrence_of a tptp0) False) % 6.75/6.97 (Eq % 6.75/6.97 (Exists fun X98 => % 6.75/6.97 And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 6.75/6.97 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 6.75/6.97 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 6.75/6.97 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 6.75/6.97 (next_subocc (skS.0 14 a a_1 a_2) X98 tptp0)) % 6.75/6.97 (leaf_occ X98 a)) % 6.75/6.97 True) % 6.75/6.97 Clause #278 (by clausification #[277]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.97 Or (Eq (occurrence_of a tptp0) False) % 6.75/6.97 (Eq % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And % 6.75/6.97 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 6.75/6.97 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 6.75/6.97 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 6.75/6.97 (Or (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp1) (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp2))) % 6.75/6.97 (next_subocc (skS.0 14 a a_1 a_2) (skS.0 15 a a_1 a_2 a_3) tptp0)) % 6.75/6.97 (leaf_occ (skS.0 15 a a_1 a_2 a_3) a)) % 6.75/6.97 True) % 6.75/6.97 Clause #279 (by clausification #[278]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (leaf_occ (skS.0 15 a a_1 a_2 a_3) a) True) % 6.75/6.97 Clause #287 (by clausification #[44]): Eq % 6.75/6.97 (∀ (X99 : Iota), % 6.75/6.97 occurrence_of X99 tptp0 → % 6.75/6.97 Exists fun X100 => % 6.75/6.97 Exists fun X101 => % 6.75/6.97 And % 6.75/6.97 (And (leaf_occ X101 X99) % 6.75/6.97 (occurrence_of X101 tptp1 → % 6.75/6.97 Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes X100 X102 tptp0)))) % 6.75/6.97 (occurrence_of X101 tptp2 → % 6.75/6.97 Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes X100 X103 tptp0)))) % 6.75/6.97 False % 6.75/6.97 Clause #288 (by clausification #[287]): ∀ (a : Iota), % 6.75/6.97 Eq % 6.75/6.97 (Not % 6.75/6.97 (occurrence_of (skS.0 17 a) tptp0 → % 6.75/6.97 Exists fun X100 => % 6.75/6.97 Exists fun X101 => % 6.75/6.97 And % 6.75/6.97 (And (leaf_occ X101 (skS.0 17 a)) % 6.75/6.97 (occurrence_of X101 tptp1 → % 6.75/6.97 Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes X100 X102 tptp0)))) % 6.75/6.97 (occurrence_of X101 tptp2 → % 6.75/6.97 Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes X100 X103 tptp0))))) % 6.75/6.97 True % 6.75/6.97 Clause #289 (by clausification #[288]): ∀ (a : Iota), % 6.75/6.97 Eq % 6.75/6.97 (occurrence_of (skS.0 17 a) tptp0 → % 6.75/6.97 Exists fun X100 => % 6.75/6.97 Exists fun X101 => % 6.75/6.97 And % 6.75/6.97 (And (leaf_occ X101 (skS.0 17 a)) % 6.75/6.97 (occurrence_of X101 tptp1 → % 6.75/6.97 Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes X100 X102 tptp0)))) % 6.82/7.00 (occurrence_of X101 tptp2 → % 6.82/7.00 Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes X100 X103 tptp0)))) % 6.82/7.00 False % 6.82/7.00 Clause #290 (by clausification #[289]): ∀ (a : Iota), Eq (occurrence_of (skS.0 17 a) tptp0) True % 6.82/7.00 Clause #291 (by clausification #[289]): ∀ (a : Iota), % 6.82/7.00 Eq % 6.82/7.00 (Exists fun X100 => % 6.82/7.00 Exists fun X101 => % 6.82/7.00 And % 6.82/7.00 (And (leaf_occ X101 (skS.0 17 a)) % 6.82/7.00 (occurrence_of X101 tptp1 → % 6.82/7.00 Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes X100 X102 tptp0)))) % 6.82/7.00 (occurrence_of X101 tptp2 → % 6.82/7.00 Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes X100 X103 tptp0)))) % 6.82/7.00 False % 6.82/7.00 Clause #292 (by superposition #[290, 279]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (leaf_occ (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 17 a)) True) % 6.82/7.00 Clause #298 (by superposition #[290, 162]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or (Eq True False) (Or (Eq (leaf_occ a (skS.0 17 a_1)) False) (Eq (min_precedes a a_2 tptp0) False)) % 6.82/7.00 Clause #317 (by clausification #[298]): ∀ (a a_1 a_2 : Iota), Or (Eq (leaf_occ a (skS.0 17 a_1)) False) (Eq (min_precedes a a_2 tptp0) False) % 6.82/7.00 Clause #346 (by clausification #[291]): ∀ (a a_1 : Iota), % 6.82/7.00 Eq % 6.82/7.00 (Exists fun X101 => % 6.82/7.00 And % 6.82/7.00 (And (leaf_occ X101 (skS.0 17 a)) % 6.82/7.00 (occurrence_of X101 tptp1 → % 6.82/7.00 Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_1 X102 tptp0)))) % 6.82/7.00 (occurrence_of X101 tptp2 → % 6.82/7.00 Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_1 X103 tptp0)))) % 6.82/7.00 False % 6.82/7.00 Clause #347 (by clausification #[346]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Eq % 6.82/7.00 (And % 6.82/7.00 (And (leaf_occ a (skS.0 17 a_1)) % 6.82/7.00 (occurrence_of a tptp1 → Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_2 X102 tptp0)))) % 6.82/7.00 (occurrence_of a tptp2 → Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_2 X103 tptp0)))) % 6.82/7.00 False % 6.82/7.00 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or % 6.82/7.00 (Eq % 6.82/7.00 (And (leaf_occ a (skS.0 17 a_1)) % 6.82/7.00 (occurrence_of a tptp1 → Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_2 X102 tptp0)))) % 6.82/7.00 False) % 6.82/7.00 (Eq (occurrence_of a tptp2 → Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_2 X103 tptp0))) % 6.82/7.00 False) % 6.82/7.00 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or % 6.82/7.00 (Eq (occurrence_of a tptp2 → Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_1 X103 tptp0))) % 6.82/7.00 False) % 6.82/7.00 (Or (Eq (leaf_occ a (skS.0 17 a_2)) False) % 6.82/7.00 (Eq % 6.82/7.00 (occurrence_of a tptp1 → Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_1 X102 tptp0))) % 6.82/7.00 False)) % 6.82/7.00 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.00 (Or % 6.82/7.00 (Eq % 6.82/7.00 (occurrence_of a tptp1 → Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_2 X102 tptp0))) % 6.82/7.00 False) % 6.82/7.00 (Eq (occurrence_of a tptp2) True)) % 6.82/7.00 Clause #351 (by clausification #[349]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.00 (Or % 6.82/7.00 (Eq % 6.82/7.00 (occurrence_of a tptp1 → Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_2 X102 tptp0))) % 6.82/7.00 False) % 6.82/7.00 (Eq (Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_2 X103 tptp0))) False)) % 6.82/7.00 Clause #353 (by clausification #[350]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.00 (Or (Eq (occurrence_of a tptp2) True) % 6.82/7.00 (Eq (Not (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_2 X102 tptp0))) False)) % 6.82/7.00 Clause #361 (by clausification #[353]): ∀ (a a_1 a_2 : Iota), % 6.82/7.00 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.00 (Or (Eq (occurrence_of a tptp2) True) % 6.82/7.00 (Eq (Exists fun X102 => And (occurrence_of X102 tptp2) (min_precedes a_2 X102 tptp0)) True)) % 6.82/7.00 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 a_3 : Iota), % 6.82/7.02 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.02 (Or (Eq (occurrence_of a tptp2) True) % 6.82/7.02 (Eq (And (occurrence_of (skS.0 18 a_2 a_3) tptp2) (min_precedes a_2 (skS.0 18 a_2 a_3) tptp0)) True)) % 6.82/7.02 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 6.82/7.02 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.02 (Or (Eq (occurrence_of a tptp2) True) (Eq (min_precedes a_2 (skS.0 18 a_2 a_3) tptp0) True)) % 6.82/7.02 Clause #365 (by clausification #[292]): ∀ (a a_1 a_2 a_3 : Iota), Eq (leaf_occ (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 17 a)) True % 6.82/7.02 Clause #366 (by superposition #[365, 317]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (min_precedes (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) a_4 tptp0) False) % 6.82/7.02 Clause #368 (by superposition #[365, 363]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.82/7.02 Or (Eq True False) % 6.82/7.02 (Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) % 6.82/7.02 (Eq (min_precedes a_4 (skS.0 18 a_4 a_5) tptp0) True)) % 6.82/7.02 Clause #373 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (min_precedes (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) a_4 tptp0) False % 6.82/7.02 Clause #490 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.82/7.02 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) % 6.82/7.02 (Eq (min_precedes a_4 (skS.0 18 a_4 a_5) tptp0) True) % 6.82/7.02 Clause #501 (by superposition #[490, 373]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) (Eq True False) % 6.82/7.02 Clause #517 (by clausification #[501]): ∀ (a a_1 a_2 a_3 : Iota), Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True % 6.82/7.02 Clause #518 (by superposition #[517, 97]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.82/7.02 Or (Eq True False) (Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) a_4) False) (Eq tptp2 a_4)) % 6.82/7.02 Clause #541 (by clausification #[518]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) a_4) False) (Eq tptp2 a_4) % 6.82/7.02 Clause #586 (by clausification #[351]): ∀ (a a_1 a_2 : Iota), % 6.82/7.02 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.02 (Or (Eq (Not (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_2 X103 tptp0))) False) % 6.82/7.02 (Eq (occurrence_of a tptp1) True)) % 6.82/7.02 Clause #588 (by clausification #[586]): ∀ (a a_1 a_2 : Iota), % 6.82/7.02 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.02 (Or (Eq (occurrence_of a tptp1) True) % 6.82/7.02 (Eq (Exists fun X103 => And (occurrence_of X103 tptp1) (min_precedes a_2 X103 tptp0)) True)) % 6.82/7.02 Clause #589 (by clausification #[588]): ∀ (a a_1 a_2 a_3 : Iota), % 6.82/7.02 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.02 (Or (Eq (occurrence_of a tptp1) True) % 6.82/7.02 (Eq (And (occurrence_of (skS.0 19 a_2 a_3) tptp1) (min_precedes a_2 (skS.0 19 a_2 a_3) tptp0)) True)) % 6.82/7.02 Clause #590 (by clausification #[589]): ∀ (a a_1 a_2 a_3 : Iota), % 6.82/7.02 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 6.82/7.02 (Or (Eq (occurrence_of a tptp1) True) (Eq (min_precedes a_2 (skS.0 19 a_2 a_3) tptp0) True)) % 6.82/7.02 Clause #592 (by superposition #[590, 365]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.82/7.02 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) True) % 6.82/7.02 (Or (Eq (min_precedes a_4 (skS.0 19 a_4 a_5) tptp0) True) (Eq False True)) % 6.82/7.02 Clause #745 (by clausification #[592]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.82/7.02 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) True) % 6.82/7.02 (Eq (min_precedes a_4 (skS.0 19 a_4 a_5) tptp0) True) % 6.82/7.02 Clause #746 (by superposition #[745, 541]): ∀ (a a_1 : Iota), Or (Eq (min_precedes a (skS.0 19 a a_1) tptp0) True) (Or (Eq True False) (Eq tptp2 tptp1)) % 6.82/7.02 Clause #771 (by clausification #[746]): ∀ (a a_1 : Iota), Or (Eq (min_precedes a (skS.0 19 a a_1) tptp0) True) (Eq tptp2 tptp1) % 6.82/7.02 Clause #772 (by forward contextual literal cutting #[771, 54]): ∀ (a a_1 : Iota), Eq (min_precedes a (skS.0 19 a a_1) tptp0) True % 6.82/7.02 Clause #773 (by superposition #[772, 373]): Eq True False % 6.82/7.02 Clause #796 (by clausification #[773]): False % 6.82/7.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------