%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PRO011+2 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n022.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:08 PM UTC 2025 % Result : Theorem 5.59s 5.80s % Output : Proof 5.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PRO011+2 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.14/0.34 % Computer : n022.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 08:46:38 EDT 2025 % 0.14/0.35 % CPUTime : % 5.59/5.80 SZS status Theorem for theBenchmark.p % 5.59/5.80 SZS output start Proof for theBenchmark.p % 5.59/5.80 Clause #21 (by assumption #[]): Eq % 5.59/5.80 (∀ (X60 X61 X62 : Iota), % 5.59/5.80 And (occurrence_of X60 X62) (leaf_occ X61 X60) → Not (Exists fun X63 => min_precedes X61 X63 X62)) % 5.59/5.80 True % 5.59/5.80 Clause #22 (by assumption #[]): Eq (∀ (X64 X65 X66 : Iota), And (occurrence_of X64 X65) (occurrence_of X64 X66) → Eq X65 X66) True % 5.59/5.80 Clause #31 (by assumption #[]): Eq % 5.59/5.80 (∀ (X95 : Iota), % 5.59/5.80 occurrence_of X95 tptp0 → % 5.59/5.80 Exists fun X96 => % 5.59/5.80 Exists fun X97 => % 5.59/5.80 Exists fun X98 => % 5.59/5.80 And % 5.59/5.80 (And % 5.59/5.80 (And % 5.59/5.80 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 X95)) (occurrence_of X97 tptp4)) % 5.59/5.80 (next_subocc X96 X97 tptp0)) % 5.59/5.80 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 5.59/5.80 (next_subocc X97 X98 tptp0)) % 5.59/5.80 (leaf_occ X98 X95)) % 5.59/5.80 True % 5.59/5.80 Clause #43 (by assumption #[]): Eq (Ne tptp1 tptp2) True % 5.59/5.80 Clause #44 (by assumption #[]): Eq % 5.59/5.80 (Not % 5.59/5.80 (∀ (X99 : Iota), % 5.59/5.80 occurrence_of X99 tptp0 → % 5.59/5.80 Exists fun X100 => % 5.59/5.80 Exists fun X101 => % 5.59/5.80 And % 5.59/5.80 (And (leaf_occ X101 X99) % 5.59/5.80 (occurrence_of X101 tptp1 → % 5.59/5.80 Not % 5.59/5.80 (Exists fun X102 => % 5.59/5.80 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 X99)) % 5.59/5.80 (min_precedes X100 X102 tptp0)))) % 5.59/5.80 (occurrence_of X101 tptp2 → % 5.59/5.80 Not % 5.59/5.80 (Exists fun X103 => % 5.59/5.80 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 X99)) % 5.59/5.80 (min_precedes X100 X103 tptp0))))) % 5.59/5.80 True % 5.59/5.80 Clause #54 (by clausification #[43]): Ne tptp1 tptp2 % 5.59/5.80 Clause #92 (by clausification #[22]): ∀ (a : Iota), Eq (∀ (X65 X66 : Iota), And (occurrence_of a X65) (occurrence_of a X66) → Eq X65 X66) True % 5.59/5.80 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 % 5.59/5.80 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 % 5.59/5.80 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) % 5.59/5.80 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)) % 5.59/5.80 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)) % 5.59/5.80 Clause #156 (by clausification #[21]): ∀ (a : Iota), % 5.59/5.80 Eq (∀ (X61 X62 : Iota), And (occurrence_of a X62) (leaf_occ X61 a) → Not (Exists fun X63 => min_precedes X61 X63 X62)) % 5.59/5.80 True % 5.59/5.80 Clause #157 (by clausification #[156]): ∀ (a a_1 : Iota), % 5.59/5.80 Eq (∀ (X62 : Iota), And (occurrence_of a X62) (leaf_occ a_1 a) → Not (Exists fun X63 => min_precedes a_1 X63 X62)) % 5.59/5.80 True % 5.59/5.80 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), % 5.59/5.80 Eq (And (occurrence_of a a_1) (leaf_occ a_2 a) → Not (Exists fun X63 => min_precedes a_2 X63 a_1)) True % 5.59/5.80 Clause #159 (by clausification #[158]): ∀ (a a_1 a_2 : Iota), % 5.59/5.80 Or (Eq (And (occurrence_of a a_1) (leaf_occ a_2 a)) False) % 5.59/5.80 (Eq (Not (Exists fun X63 => min_precedes a_2 X63 a_1)) True) % 5.59/5.80 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), % 5.59/5.80 Or (Eq (Not (Exists fun X63 => min_precedes a X63 a_1)) True) % 5.59/5.80 (Or (Eq (occurrence_of a_2 a_1) False) (Eq (leaf_occ a a_2) False)) % 5.59/5.80 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 : Iota), % 5.59/5.80 Or (Eq (occurrence_of a a_1) False) % 5.59/5.80 (Or (Eq (leaf_occ a_2 a) False) (Eq (Exists fun X63 => min_precedes a_2 X63 a_1) False)) % 5.59/5.80 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 5.59/5.80 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)) % 5.59/5.80 Clause #274 (by clausification #[31]): ∀ (a : Iota), % 5.59/5.80 Eq % 5.59/5.80 (occurrence_of a tptp0 → % 5.59/5.80 Exists fun X96 => % 5.59/5.80 Exists fun X97 => % 5.59/5.82 Exists fun X98 => % 5.59/5.82 And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 a)) (occurrence_of X97 tptp4)) % 5.59/5.82 (next_subocc X96 X97 tptp0)) % 5.59/5.82 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 5.59/5.82 (next_subocc X97 X98 tptp0)) % 5.59/5.82 (leaf_occ X98 a)) % 5.59/5.82 True % 5.59/5.82 Clause #275 (by clausification #[274]): ∀ (a : Iota), % 5.59/5.82 Or (Eq (occurrence_of a tptp0) False) % 5.59/5.82 (Eq % 5.59/5.82 (Exists fun X96 => % 5.59/5.82 Exists fun X97 => % 5.59/5.82 Exists fun X98 => % 5.59/5.82 And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 a)) (occurrence_of X97 tptp4)) % 5.59/5.82 (next_subocc X96 X97 tptp0)) % 5.59/5.82 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 5.59/5.82 (next_subocc X97 X98 tptp0)) % 5.59/5.82 (leaf_occ X98 a)) % 5.59/5.82 True) % 5.59/5.82 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), % 5.59/5.82 Or (Eq (occurrence_of a tptp0) False) % 5.59/5.82 (Eq % 5.59/5.82 (Exists fun X97 => % 5.59/5.82 Exists fun X98 => % 5.59/5.82 And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 5.59/5.82 (occurrence_of X97 tptp4)) % 5.59/5.82 (next_subocc (skS.0 13 a a_1) X97 tptp0)) % 5.59/5.82 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 5.59/5.82 (next_subocc X97 X98 tptp0)) % 5.59/5.82 (leaf_occ X98 a)) % 5.59/5.82 True) % 5.59/5.82 Clause #277 (by clausification #[276]): ∀ (a a_1 a_2 : Iota), % 5.59/5.82 Or (Eq (occurrence_of a tptp0) False) % 5.59/5.82 (Eq % 5.59/5.82 (Exists fun X98 => % 5.59/5.82 And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 5.59/5.82 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 5.59/5.82 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 5.59/5.82 (Or (occurrence_of X98 tptp1) (occurrence_of X98 tptp2))) % 5.59/5.82 (next_subocc (skS.0 14 a a_1 a_2) X98 tptp0)) % 5.59/5.82 (leaf_occ X98 a)) % 5.59/5.82 True) % 5.59/5.82 Clause #278 (by clausification #[277]): ∀ (a a_1 a_2 a_3 : Iota), % 5.59/5.82 Or (Eq (occurrence_of a tptp0) False) % 5.59/5.82 (Eq % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And % 5.59/5.82 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 5.59/5.82 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 5.59/5.82 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 5.59/5.82 (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))) % 5.59/5.82 (next_subocc (skS.0 14 a a_1 a_2) (skS.0 15 a a_1 a_2 a_3) tptp0)) % 5.59/5.82 (leaf_occ (skS.0 15 a a_1 a_2 a_3) a)) % 5.59/5.82 True) % 5.59/5.82 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) % 5.59/5.82 Clause #287 (by clausification #[44]): Eq % 5.59/5.82 (∀ (X99 : Iota), % 5.59/5.82 occurrence_of X99 tptp0 → % 5.59/5.82 Exists fun X100 => % 5.59/5.82 Exists fun X101 => % 5.59/5.82 And % 5.59/5.82 (And (leaf_occ X101 X99) % 5.59/5.82 (occurrence_of X101 tptp1 → % 5.59/5.82 Not % 5.59/5.82 (Exists fun X102 => % 5.59/5.82 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 X99)) % 5.59/5.82 (min_precedes X100 X102 tptp0)))) % 5.59/5.82 (occurrence_of X101 tptp2 → % 5.59/5.82 Not % 5.59/5.82 (Exists fun X103 => % 5.59/5.82 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 X99)) % 5.59/5.82 (min_precedes X100 X103 tptp0)))) % 5.59/5.82 False % 5.59/5.82 Clause #288 (by clausification #[287]): ∀ (a : Iota), % 5.59/5.82 Eq % 5.59/5.82 (Not % 5.59/5.82 (occurrence_of (skS.0 17 a) tptp0 → % 5.59/5.82 Exists fun X100 => % 5.59/5.82 Exists fun X101 => % 5.59/5.82 And % 5.59/5.82 (And (leaf_occ X101 (skS.0 17 a)) % 5.59/5.82 (occurrence_of X101 tptp1 → % 5.59/5.82 Not % 5.59/5.82 (Exists fun X102 => % 5.59/5.82 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a))) % 5.59/5.83 (min_precedes X100 X102 tptp0)))) % 5.59/5.83 (occurrence_of X101 tptp2 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X103 => % 5.59/5.83 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a))) % 5.59/5.83 (min_precedes X100 X103 tptp0))))) % 5.59/5.83 True % 5.59/5.83 Clause #289 (by clausification #[288]): ∀ (a : Iota), % 5.59/5.83 Eq % 5.59/5.83 (occurrence_of (skS.0 17 a) tptp0 → % 5.59/5.83 Exists fun X100 => % 5.59/5.83 Exists fun X101 => % 5.59/5.83 And % 5.59/5.83 (And (leaf_occ X101 (skS.0 17 a)) % 5.59/5.83 (occurrence_of X101 tptp1 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X102 => % 5.59/5.83 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a))) % 5.59/5.83 (min_precedes X100 X102 tptp0)))) % 5.59/5.83 (occurrence_of X101 tptp2 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X103 => % 5.59/5.83 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a))) % 5.59/5.83 (min_precedes X100 X103 tptp0)))) % 5.59/5.83 False % 5.59/5.83 Clause #290 (by clausification #[289]): ∀ (a : Iota), Eq (occurrence_of (skS.0 17 a) tptp0) True % 5.59/5.83 Clause #291 (by clausification #[289]): ∀ (a : Iota), % 5.59/5.83 Eq % 5.59/5.83 (Exists fun X100 => % 5.59/5.83 Exists fun X101 => % 5.59/5.83 And % 5.59/5.83 (And (leaf_occ X101 (skS.0 17 a)) % 5.59/5.83 (occurrence_of X101 tptp1 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X102 => % 5.59/5.83 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a))) % 5.59/5.83 (min_precedes X100 X102 tptp0)))) % 5.59/5.83 (occurrence_of X101 tptp2 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X103 => % 5.59/5.83 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a))) % 5.59/5.83 (min_precedes X100 X103 tptp0)))) % 5.59/5.83 False % 5.59/5.83 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) % 5.59/5.83 Clause #298 (by superposition #[290, 162]): ∀ (a a_1 a_2 : Iota), % 5.59/5.83 Or (Eq True False) (Or (Eq (leaf_occ a (skS.0 17 a_1)) False) (Eq (min_precedes a a_2 tptp0) False)) % 5.59/5.83 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) % 5.59/5.83 Clause #346 (by clausification #[291]): ∀ (a a_1 : Iota), % 5.59/5.83 Eq % 5.59/5.83 (Exists fun X101 => % 5.59/5.83 And % 5.59/5.83 (And (leaf_occ X101 (skS.0 17 a)) % 5.59/5.83 (occurrence_of X101 tptp1 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X102 => % 5.59/5.83 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a))) % 5.59/5.83 (min_precedes a_1 X102 tptp0)))) % 5.59/5.83 (occurrence_of X101 tptp2 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X103 => % 5.59/5.83 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a))) % 5.59/5.83 (min_precedes a_1 X103 tptp0)))) % 5.59/5.83 False % 5.59/5.83 Clause #347 (by clausification #[346]): ∀ (a a_1 a_2 : Iota), % 5.59/5.83 Eq % 5.59/5.83 (And % 5.59/5.83 (And (leaf_occ a (skS.0 17 a_1)) % 5.59/5.83 (occurrence_of a tptp1 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X102 => % 5.59/5.83 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.59/5.83 (min_precedes a_2 X102 tptp0)))) % 5.59/5.83 (occurrence_of a tptp2 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X103 => % 5.59/5.83 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a_1))) % 5.59/5.83 (min_precedes a_2 X103 tptp0)))) % 5.59/5.83 False % 5.59/5.83 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 : Iota), % 5.59/5.83 Or % 5.59/5.83 (Eq % 5.59/5.83 (And (leaf_occ a (skS.0 17 a_1)) % 5.59/5.83 (occurrence_of a tptp1 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X102 => % 5.59/5.83 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.59/5.83 (min_precedes a_2 X102 tptp0)))) % 5.59/5.83 False) % 5.59/5.83 (Eq % 5.59/5.83 (occurrence_of a tptp2 → % 5.59/5.83 Not % 5.59/5.83 (Exists fun X103 => % 5.59/5.83 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a_1))) % 5.59/5.83 (min_precedes a_2 X103 tptp0))) % 5.59/5.83 False) % 5.59/5.83 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 : Iota), % 5.69/5.85 Or % 5.69/5.85 (Eq % 5.69/5.85 (occurrence_of a tptp2 → % 5.69/5.85 Not % 5.69/5.85 (Exists fun X103 => % 5.69/5.85 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X103 tptp0))) % 5.69/5.85 False) % 5.69/5.85 (Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Eq % 5.69/5.85 (occurrence_of a tptp1 → % 5.69/5.85 Not % 5.69/5.85 (Exists fun X102 => % 5.69/5.85 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X102 tptp0))) % 5.69/5.85 False)) % 5.69/5.85 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 : Iota), % 5.69/5.85 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Or % 5.69/5.85 (Eq % 5.69/5.85 (occurrence_of a tptp1 → % 5.69/5.85 Not % 5.69/5.85 (Exists fun X102 => % 5.69/5.85 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X102 tptp0))) % 5.69/5.85 False) % 5.69/5.85 (Eq (occurrence_of a tptp2) True)) % 5.69/5.85 Clause #351 (by clausification #[349]): ∀ (a a_1 a_2 : Iota), % 5.69/5.85 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Or % 5.69/5.85 (Eq % 5.69/5.85 (occurrence_of a tptp1 → % 5.69/5.85 Not % 5.69/5.85 (Exists fun X102 => % 5.69/5.85 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X102 tptp0))) % 5.69/5.85 False) % 5.69/5.85 (Eq % 5.69/5.85 (Not % 5.69/5.85 (Exists fun X103 => % 5.69/5.85 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X103 tptp0))) % 5.69/5.85 False)) % 5.69/5.85 Clause #353 (by clausification #[350]): ∀ (a a_1 a_2 : Iota), % 5.69/5.85 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Or (Eq (occurrence_of a tptp2) True) % 5.69/5.85 (Eq % 5.69/5.85 (Not % 5.69/5.85 (Exists fun X102 => % 5.69/5.85 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X102 tptp0))) % 5.69/5.85 False)) % 5.69/5.85 Clause #361 (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 % 5.69/5.85 Clause #362 (by superposition #[361, 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) % 5.69/5.85 Clause #376 (by clausification #[362]): ∀ (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 % 5.69/5.85 Clause #394 (by clausification #[353]): ∀ (a a_1 a_2 : Iota), % 5.69/5.85 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Or (Eq (occurrence_of a tptp2) True) % 5.69/5.85 (Eq % 5.69/5.85 (Exists fun X102 => % 5.69/5.85 And (And (occurrence_of X102 tptp2) (subactivity_occurrence X102 (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 X102 tptp0)) % 5.69/5.85 True)) % 5.69/5.85 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 : Iota), % 5.69/5.85 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Or (Eq (occurrence_of a tptp2) True) % 5.69/5.85 (Eq % 5.69/5.85 (And % 5.69/5.85 (And (occurrence_of (skS.0 18 a_1 a_2 a_3) tptp2) % 5.69/5.85 (subactivity_occurrence (skS.0 18 a_1 a_2 a_3) (skS.0 17 a_1))) % 5.69/5.85 (min_precedes a_2 (skS.0 18 a_1 a_2 a_3) tptp0)) % 5.69/5.85 True)) % 5.69/5.85 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 : Iota), % 5.69/5.85 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.85 (Or (Eq (occurrence_of a tptp2) True) (Eq (min_precedes a_2 (skS.0 18 a_1 a_2 a_3) tptp0) True)) % 5.69/5.85 Clause #398 (by superposition #[396, 361]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.69/5.85 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) % 5.69/5.85 (Or (Eq (min_precedes a_4 (skS.0 18 a a_4 a_5) tptp0) True) (Eq False True)) % 5.69/5.85 Clause #399 (by clausification #[398]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.69/5.85 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) % 5.69/5.85 (Eq (min_precedes a_4 (skS.0 18 a a_4 a_5) tptp0) True) % 5.69/5.85 Clause #410 (by superposition #[399, 376]): ∀ (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) % 5.69/5.85 Clause #451 (by clausification #[410]): ∀ (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 % 5.69/5.85 Clause #452 (by superposition #[451, 97]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.69/5.87 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)) % 5.69/5.87 Clause #470 (by clausification #[452]): ∀ (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) % 5.69/5.87 Clause #581 (by clausification #[351]): ∀ (a a_1 a_2 : Iota), % 5.69/5.87 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.87 (Or % 5.69/5.87 (Eq % 5.69/5.87 (Not % 5.69/5.87 (Exists fun X103 => % 5.69/5.87 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a_1))) % 5.69/5.87 (min_precedes a_2 X103 tptp0))) % 5.69/5.87 False) % 5.69/5.87 (Eq (occurrence_of a tptp1) True)) % 5.69/5.87 Clause #583 (by clausification #[581]): ∀ (a a_1 a_2 : Iota), % 5.69/5.87 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.87 (Or (Eq (occurrence_of a tptp1) True) % 5.69/5.87 (Eq % 5.69/5.87 (Exists fun X103 => % 5.69/5.87 And (And (occurrence_of X103 tptp1) (subactivity_occurrence X103 (skS.0 17 a_1))) % 5.69/5.87 (min_precedes a_2 X103 tptp0)) % 5.69/5.87 True)) % 5.69/5.87 Clause #584 (by clausification #[583]): ∀ (a a_1 a_2 a_3 : Iota), % 5.69/5.87 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.87 (Or (Eq (occurrence_of a tptp1) True) % 5.69/5.87 (Eq % 5.69/5.87 (And % 5.69/5.87 (And (occurrence_of (skS.0 19 a_1 a_2 a_3) tptp1) % 5.69/5.87 (subactivity_occurrence (skS.0 19 a_1 a_2 a_3) (skS.0 17 a_1))) % 5.69/5.87 (min_precedes a_2 (skS.0 19 a_1 a_2 a_3) tptp0)) % 5.69/5.87 True)) % 5.69/5.87 Clause #585 (by clausification #[584]): ∀ (a a_1 a_2 a_3 : Iota), % 5.69/5.87 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 5.69/5.87 (Or (Eq (occurrence_of a tptp1) True) (Eq (min_precedes a_2 (skS.0 19 a_1 a_2 a_3) tptp0) True)) % 5.69/5.87 Clause #587 (by superposition #[585, 361]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.69/5.87 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) True) % 5.69/5.87 (Or (Eq (min_precedes a_4 (skS.0 19 a a_4 a_5) tptp0) True) (Eq False True)) % 5.69/5.87 Clause #588 (by clausification #[587]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.69/5.87 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) True) % 5.69/5.87 (Eq (min_precedes a_4 (skS.0 19 a a_4 a_5) tptp0) True) % 5.69/5.87 Clause #589 (by superposition #[588, 470]): ∀ (a a_1 a_2 : Iota), Or (Eq (min_precedes a (skS.0 19 a_1 a a_2) tptp0) True) (Or (Eq True False) (Eq tptp2 tptp1)) % 5.69/5.87 Clause #614 (by clausification #[589]): ∀ (a a_1 a_2 : Iota), Or (Eq (min_precedes a (skS.0 19 a_1 a a_2) tptp0) True) (Eq tptp2 tptp1) % 5.69/5.87 Clause #615 (by forward contextual literal cutting #[614, 54]): ∀ (a a_1 a_2 : Iota), Eq (min_precedes a (skS.0 19 a_1 a a_2) tptp0) True % 5.69/5.87 Clause #616 (by superposition #[615, 376]): Eq True False % 5.69/5.87 Clause #630 (by clausification #[616]): False % 5.69/5.87 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------