%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PRO009+4 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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 106.87s 107.05s % Output : Proof 107.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PRO009+4 : TPTP v9.2.0. Released v4.0.0. % 0.04/0.13 % Command : duper %s % 0.13/0.34 % Computer : n024.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 08:42:38 EDT 2025 % 0.13/0.34 % CPUTime : % 106.87/107.05 SZS status Theorem for theBenchmark.p % 106.87/107.05 SZS output start Proof for theBenchmark.p % 106.87/107.05 Clause #18 (by assumption #[]): Eq % 106.87/107.05 (∀ (X55 X56 : Iota), % 106.87/107.05 Iff (leaf_occ X55 X56) % 106.87/107.05 (Exists fun X57 => And (And (occurrence_of X56 X57) (subactivity_occurrence X55 X56)) (leaf X55 X57))) % 106.87/107.05 True % 106.87/107.05 Clause #19 (by assumption #[]): Eq % 106.87/107.05 (∀ (X58 X59 : Iota), % 106.87/107.05 Iff (root_occ X58 X59) % 106.87/107.05 (Exists fun X60 => And (And (occurrence_of X59 X60) (subactivity_occurrence X58 X59)) (root X58 X60))) % 106.87/107.05 True % 106.87/107.05 Clause #23 (by assumption #[]): Eq (∀ (X68 X69 X70 : Iota), min_precedes X68 X69 X70 → Exists fun X71 => And (root X71 X70) (min_precedes X71 X69 X70)) % 106.87/107.05 True % 106.87/107.05 Clause #26 (by assumption #[]): Eq % 106.87/107.05 (∀ (X78 X79 X80 : Iota), % 106.87/107.05 Iff (next_subocc X78 X79 X80) % 106.87/107.05 (And (min_precedes X78 X79 X80) % 106.87/107.05 (Not (Exists fun X81 => And (min_precedes X78 X81 X80) (min_precedes X81 X79 X80))))) % 106.87/107.05 True % 106.87/107.05 Clause #27 (by assumption #[]): Eq % 106.87/107.05 (∀ (X82 X83 X84 X85 : Iota), % 106.87/107.05 And (And (min_precedes X82 X83 X84) (occurrence_of X85 X84)) (subactivity_occurrence X83 X85) → % 106.87/107.05 subactivity_occurrence X82 X85) % 106.87/107.05 True % 106.87/107.05 Clause #29 (by assumption #[]): Eq (∀ (X90 X91 X92 X93 : Iota), And (And (occurrence_of X92 X93) (root_occ X90 X92)) (root_occ X91 X92) → Eq X90 X91) % 106.87/107.05 True % 106.87/107.05 Clause #32 (by assumption #[]): Eq % 106.87/107.05 (∀ (X101 : Iota), % 106.87/107.05 occurrence_of X101 tptp0 → % 106.87/107.05 Exists fun X102 => % 106.87/107.05 Exists fun X103 => % 106.87/107.05 Exists fun X104 => % 106.87/107.05 And % 106.87/107.05 (And % 106.87/107.05 (And % 106.87/107.05 (And (And (And (occurrence_of X102 tptp3) (root_occ X102 X101)) (occurrence_of X103 tptp4)) % 106.87/107.05 (next_subocc X102 X103 tptp0)) % 106.87/107.05 (Or (occurrence_of X104 tptp2) (occurrence_of X104 tptp1))) % 106.87/107.05 (next_subocc X103 X104 tptp0)) % 106.87/107.05 (leaf_occ X104 X101)) % 106.87/107.05 True % 106.87/107.05 Clause #45 (by assumption #[]): Eq % 106.87/107.05 (Not % 106.87/107.05 (∀ (X105 : Iota), % 106.87/107.05 occurrence_of X105 tptp0 → % 106.87/107.05 Exists fun X106 => % 106.87/107.05 Exists fun X107 => % 106.87/107.05 And % 106.87/107.05 (And % 106.87/107.05 (And (And (occurrence_of X106 tptp3) (root_occ X106 X105)) % 106.87/107.05 (Or (occurrence_of X107 tptp2) (occurrence_of X107 tptp1))) % 106.87/107.05 (min_precedes X106 X107 tptp0)) % 106.87/107.05 (leaf_occ X107 X105))) % 106.87/107.05 True % 106.87/107.05 Clause #102 (by clausification #[27]): ∀ (a : Iota), % 106.87/107.05 Eq % 106.87/107.05 (∀ (X83 X84 X85 : Iota), % 106.87/107.05 And (And (min_precedes a X83 X84) (occurrence_of X85 X84)) (subactivity_occurrence X83 X85) → % 106.87/107.05 subactivity_occurrence a X85) % 106.87/107.05 True % 106.87/107.05 Clause #103 (by clausification #[102]): ∀ (a a_1 : Iota), % 106.87/107.05 Eq % 106.87/107.05 (∀ (X84 X85 : Iota), % 106.87/107.05 And (And (min_precedes a a_1 X84) (occurrence_of X85 X84)) (subactivity_occurrence a_1 X85) → % 106.87/107.05 subactivity_occurrence a X85) % 106.87/107.05 True % 106.87/107.05 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 106.87/107.05 Eq % 106.87/107.05 (∀ (X85 : Iota), % 106.87/107.05 And (And (min_precedes a a_1 a_2) (occurrence_of X85 a_2)) (subactivity_occurrence a_1 X85) → % 106.87/107.05 subactivity_occurrence a X85) % 106.87/107.05 True % 106.87/107.05 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.05 Eq % 106.87/107.05 (And (And (min_precedes a a_1 a_2) (occurrence_of a_3 a_2)) (subactivity_occurrence a_1 a_3) → % 106.87/107.05 subactivity_occurrence a a_3) % 106.87/107.05 True % 106.87/107.05 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.05 Or (Eq (And (And (min_precedes a a_1 a_2) (occurrence_of a_3 a_2)) (subactivity_occurrence a_1 a_3)) False) % 106.87/107.05 (Eq (subactivity_occurrence a a_3) True) % 106.87/107.05 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.05 Or (Eq (subactivity_occurrence a a_1) True) % 106.87/107.05 (Or (Eq (And (min_precedes a a_2 a_3) (occurrence_of a_1 a_3)) False) (Eq (subactivity_occurrence a_2 a_1) False)) % 106.87/107.05 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.05 Or (Eq (subactivity_occurrence a a_1) True) % 106.87/107.05 (Or (Eq (subactivity_occurrence a_2 a_1) False) % 106.87/107.05 (Or (Eq (min_precedes a a_2 a_3) False) (Eq (occurrence_of a_1 a_3) False))) % 106.87/107.05 Clause #153 (by clausification #[29]): ∀ (a : Iota), % 106.87/107.05 Eq (∀ (X91 X92 X93 : Iota), And (And (occurrence_of X92 X93) (root_occ a X92)) (root_occ X91 X92) → Eq a X91) True % 106.87/107.05 Clause #154 (by clausification #[153]): ∀ (a a_1 : Iota), % 106.87/107.07 Eq (∀ (X92 X93 : Iota), And (And (occurrence_of X92 X93) (root_occ a X92)) (root_occ a_1 X92) → Eq a a_1) True % 106.87/107.07 Clause #155 (by clausification #[154]): ∀ (a a_1 a_2 : Iota), % 106.87/107.07 Eq (∀ (X93 : Iota), And (And (occurrence_of a X93) (root_occ a_1 a)) (root_occ a_2 a) → Eq a_1 a_2) True % 106.87/107.07 Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (And (occurrence_of a a_1) (root_occ a_2 a)) (root_occ a_3 a) → Eq a_2 a_3) True % 106.87/107.07 Clause #157 (by clausification #[156]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.07 Or (Eq (And (And (occurrence_of a a_1) (root_occ a_2 a)) (root_occ a_3 a)) False) (Eq (Eq a_2 a_3) True) % 106.87/107.07 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.07 Or (Eq (Eq a a_1) True) (Or (Eq (And (occurrence_of a_2 a_3) (root_occ a a_2)) False) (Eq (root_occ a_1 a_2) False)) % 106.87/107.07 Clause #159 (by clausification #[158]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.07 Or (Eq (And (occurrence_of a a_1) (root_occ a_2 a)) False) (Or (Eq (root_occ a_3 a) False) (Eq a_2 a_3)) % 106.87/107.07 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.07 Or (Eq (root_occ a a_1) False) (Or (Eq a_2 a) (Or (Eq (occurrence_of a_1 a_3) False) (Eq (root_occ a_2 a_1) False))) % 106.87/107.07 Clause #225 (by clausification #[23]): ∀ (a : Iota), % 106.87/107.07 Eq (∀ (X69 X70 : Iota), min_precedes a X69 X70 → Exists fun X71 => And (root X71 X70) (min_precedes X71 X69 X70)) True % 106.87/107.07 Clause #226 (by clausification #[225]): ∀ (a a_1 : Iota), % 106.87/107.07 Eq (∀ (X70 : Iota), min_precedes a a_1 X70 → Exists fun X71 => And (root X71 X70) (min_precedes X71 a_1 X70)) True % 106.87/107.07 Clause #227 (by clausification #[226]): ∀ (a a_1 a_2 : Iota), Eq (min_precedes a a_1 a_2 → Exists fun X71 => And (root X71 a_2) (min_precedes X71 a_1 a_2)) True % 106.87/107.07 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 106.87/107.07 Or (Eq (min_precedes a a_1 a_2) False) (Eq (Exists fun X71 => And (root X71 a_2) (min_precedes X71 a_1 a_2)) True) % 106.87/107.07 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 a_3 : Iota), % 106.87/107.07 Or (Eq (min_precedes a a_1 a_2) False) % 106.87/107.07 (Eq (And (root (skS.0 5 a_2 a_1 a_3) a_2) (min_precedes (skS.0 5 a_2 a_1 a_3) a_1 a_2)) True) % 106.87/107.07 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (min_precedes a a_1 a_2) False) (Eq (min_precedes (skS.0 5 a_2 a_1 a_3) a_1 a_2) True) % 106.87/107.07 Clause #231 (by clausification #[229]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (min_precedes a a_1 a_2) False) (Eq (root (skS.0 5 a_2 a_1 a_3) a_2) True) % 106.87/107.07 Clause #242 (by clausification #[19]): ∀ (a : Iota), % 106.87/107.07 Eq % 106.87/107.07 (∀ (X59 : Iota), % 106.87/107.07 Iff (root_occ a X59) % 106.87/107.07 (Exists fun X60 => And (And (occurrence_of X59 X60) (subactivity_occurrence a X59)) (root a X60))) % 106.87/107.07 True % 106.87/107.07 Clause #243 (by clausification #[242]): ∀ (a a_1 : Iota), % 106.87/107.07 Eq % 106.87/107.07 (Iff (root_occ a a_1) % 106.87/107.07 (Exists fun X60 => And (And (occurrence_of a_1 X60) (subactivity_occurrence a a_1)) (root a X60))) % 106.87/107.07 True % 106.87/107.07 Clause #244 (by clausification #[243]): ∀ (a a_1 : Iota), % 106.87/107.07 Or (Eq (root_occ a a_1) True) % 106.87/107.07 (Eq (Exists fun X60 => And (And (occurrence_of a_1 X60) (subactivity_occurrence a a_1)) (root a X60)) False) % 106.87/107.07 Clause #246 (by clausification #[244]): ∀ (a a_1 a_2 : Iota), % 106.87/107.07 Or (Eq (root_occ a a_1) True) % 106.87/107.07 (Eq (And (And (occurrence_of a_1 a_2) (subactivity_occurrence a a_1)) (root a a_2)) False) % 106.87/107.07 Clause #247 (by clausification #[246]): ∀ (a a_1 a_2 : Iota), % 106.87/107.07 Or (Eq (root_occ a a_1) True) % 106.87/107.07 (Or (Eq (And (occurrence_of a_1 a_2) (subactivity_occurrence a a_1)) False) (Eq (root a a_2) False)) % 106.87/107.07 Clause #248 (by clausification #[247]): ∀ (a a_1 a_2 : Iota), % 106.87/107.07 Or (Eq (root_occ a a_1) True) % 106.87/107.07 (Or (Eq (root a a_2) False) (Or (Eq (occurrence_of a_1 a_2) False) (Eq (subactivity_occurrence a a_1) False))) % 106.87/107.07 Clause #266 (by clausification #[18]): ∀ (a : Iota), % 106.87/107.07 Eq % 106.87/107.07 (∀ (X56 : Iota), % 106.87/107.07 Iff (leaf_occ a X56) % 106.87/107.07 (Exists fun X57 => And (And (occurrence_of X56 X57) (subactivity_occurrence a X56)) (leaf a X57))) % 106.87/107.07 True % 106.87/107.07 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), % 106.87/107.07 Eq % 106.87/107.07 (Iff (leaf_occ a a_1) % 106.87/107.07 (Exists fun X57 => And (And (occurrence_of a_1 X57) (subactivity_occurrence a a_1)) (leaf a X57))) % 106.91/107.09 True % 106.91/107.09 Clause #269 (by clausification #[267]): ∀ (a a_1 : Iota), % 106.91/107.09 Or (Eq (leaf_occ a a_1) False) % 106.91/107.09 (Eq (Exists fun X57 => And (And (occurrence_of a_1 X57) (subactivity_occurrence a a_1)) (leaf a X57)) True) % 106.91/107.09 Clause #273 (by clausification #[26]): ∀ (a : Iota), % 106.91/107.09 Eq % 106.91/107.09 (∀ (X79 X80 : Iota), % 106.91/107.09 Iff (next_subocc a X79 X80) % 106.91/107.09 (And (min_precedes a X79 X80) % 106.91/107.09 (Not (Exists fun X81 => And (min_precedes a X81 X80) (min_precedes X81 X79 X80))))) % 106.91/107.09 True % 106.91/107.09 Clause #274 (by clausification #[273]): ∀ (a a_1 : Iota), % 106.91/107.09 Eq % 106.91/107.09 (∀ (X80 : Iota), % 106.91/107.09 Iff (next_subocc a a_1 X80) % 106.91/107.09 (And (min_precedes a a_1 X80) % 106.91/107.09 (Not (Exists fun X81 => And (min_precedes a X81 X80) (min_precedes X81 a_1 X80))))) % 106.91/107.09 True % 106.91/107.09 Clause #275 (by clausification #[274]): ∀ (a a_1 a_2 : Iota), % 106.91/107.09 Eq % 106.91/107.09 (Iff (next_subocc a a_1 a_2) % 106.91/107.09 (And (min_precedes a a_1 a_2) (Not (Exists fun X81 => And (min_precedes a X81 a_2) (min_precedes X81 a_1 a_2))))) % 106.91/107.09 True % 106.91/107.09 Clause #277 (by clausification #[275]): ∀ (a a_1 a_2 : Iota), % 106.91/107.09 Or (Eq (next_subocc a a_1 a_2) False) % 106.91/107.09 (Eq (And (min_precedes a a_1 a_2) (Not (Exists fun X81 => And (min_precedes a X81 a_2) (min_precedes X81 a_1 a_2)))) % 106.91/107.09 True) % 106.91/107.09 Clause #283 (by clausification #[269]): ∀ (a a_1 a_2 : Iota), % 106.91/107.09 Or (Eq (leaf_occ a a_1) False) % 106.91/107.09 (Eq % 106.91/107.09 (And (And (occurrence_of a_1 (skS.0 11 a_1 a a_2)) (subactivity_occurrence a a_1)) (leaf a (skS.0 11 a_1 a a_2))) % 106.91/107.09 True) % 106.91/107.09 Clause #285 (by clausification #[283]): ∀ (a a_1 a_2 : Iota), % 106.91/107.09 Or (Eq (leaf_occ a a_1) False) (Eq (And (occurrence_of a_1 (skS.0 11 a_1 a a_2)) (subactivity_occurrence a a_1)) True) % 106.91/107.09 Clause #286 (by clausification #[285]): ∀ (a a_1 : Iota), Or (Eq (leaf_occ a a_1) False) (Eq (subactivity_occurrence a a_1) True) % 106.91/107.09 Clause #289 (by clausification #[277]): ∀ (a a_1 a_2 : Iota), Or (Eq (next_subocc a a_1 a_2) False) (Eq (min_precedes a a_1 a_2) True) % 106.91/107.09 Clause #293 (by clausification #[32]): ∀ (a : Iota), % 106.91/107.09 Eq % 106.91/107.09 (occurrence_of a tptp0 → % 106.91/107.09 Exists fun X102 => % 106.91/107.09 Exists fun X103 => % 106.91/107.09 Exists fun X104 => % 106.91/107.09 And % 106.91/107.09 (And % 106.91/107.09 (And % 106.91/107.09 (And (And (And (occurrence_of X102 tptp3) (root_occ X102 a)) (occurrence_of X103 tptp4)) % 106.91/107.09 (next_subocc X102 X103 tptp0)) % 106.91/107.09 (Or (occurrence_of X104 tptp2) (occurrence_of X104 tptp1))) % 106.91/107.09 (next_subocc X103 X104 tptp0)) % 106.91/107.09 (leaf_occ X104 a)) % 106.91/107.09 True % 106.91/107.09 Clause #294 (by clausification #[293]): ∀ (a : Iota), % 106.91/107.09 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.09 (Eq % 106.91/107.09 (Exists fun X102 => % 106.91/107.09 Exists fun X103 => % 106.91/107.09 Exists fun X104 => % 106.91/107.09 And % 106.91/107.09 (And % 106.91/107.09 (And % 106.91/107.09 (And (And (And (occurrence_of X102 tptp3) (root_occ X102 a)) (occurrence_of X103 tptp4)) % 106.91/107.09 (next_subocc X102 X103 tptp0)) % 106.91/107.09 (Or (occurrence_of X104 tptp2) (occurrence_of X104 tptp1))) % 106.91/107.09 (next_subocc X103 X104 tptp0)) % 106.91/107.09 (leaf_occ X104 a)) % 106.91/107.09 True) % 106.91/107.09 Clause #295 (by clausification #[294]): ∀ (a a_1 : Iota), % 106.91/107.09 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.09 (Eq % 106.91/107.09 (Exists fun X103 => % 106.91/107.09 Exists fun X104 => % 106.91/107.09 And % 106.91/107.09 (And % 106.91/107.09 (And % 106.91/107.09 (And % 106.91/107.09 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.91/107.09 (occurrence_of X103 tptp4)) % 106.91/107.09 (next_subocc (skS.0 12 a a_1) X103 tptp0)) % 106.91/107.09 (Or (occurrence_of X104 tptp2) (occurrence_of X104 tptp1))) % 106.91/107.09 (next_subocc X103 X104 tptp0)) % 106.91/107.09 (leaf_occ X104 a)) % 106.91/107.09 True) % 106.91/107.09 Clause #296 (by clausification #[295]): ∀ (a a_1 a_2 : Iota), % 106.91/107.09 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.09 (Eq % 106.91/107.09 (Exists fun X104 => % 106.91/107.09 And % 106.91/107.09 (And % 106.91/107.09 (And % 106.91/107.09 (And % 106.91/107.09 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.91/107.09 (occurrence_of (skS.0 13 a a_1 a_2) tptp4)) % 106.91/107.09 (next_subocc (skS.0 12 a a_1) (skS.0 13 a a_1 a_2) tptp0)) % 106.91/107.09 (Or (occurrence_of X104 tptp2) (occurrence_of X104 tptp1))) % 106.91/107.11 (next_subocc (skS.0 13 a a_1 a_2) X104 tptp0)) % 106.91/107.11 (leaf_occ X104 a)) % 106.91/107.11 True) % 106.91/107.11 Clause #297 (by clausification #[296]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.11 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.11 (Eq % 106.91/107.11 (And % 106.91/107.11 (And % 106.91/107.11 (And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.91/107.11 (occurrence_of (skS.0 13 a a_1 a_2) tptp4)) % 106.91/107.11 (next_subocc (skS.0 12 a a_1) (skS.0 13 a a_1 a_2) tptp0)) % 106.91/107.11 (Or (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp1))) % 106.91/107.11 (next_subocc (skS.0 13 a a_1 a_2) (skS.0 14 a a_1 a_2 a_3) tptp0)) % 106.91/107.11 (leaf_occ (skS.0 14 a a_1 a_2 a_3) a)) % 106.91/107.11 True) % 106.91/107.11 Clause #298 (by clausification #[297]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (leaf_occ (skS.0 14 a a_1 a_2 a_3) a) True) % 106.91/107.11 Clause #299 (by clausification #[297]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.11 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.11 (Eq % 106.91/107.11 (And % 106.91/107.11 (And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.91/107.11 (occurrence_of (skS.0 13 a a_1 a_2) tptp4)) % 106.91/107.11 (next_subocc (skS.0 12 a a_1) (skS.0 13 a a_1 a_2) tptp0)) % 106.91/107.11 (Or (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp1))) % 106.91/107.11 (next_subocc (skS.0 13 a a_1 a_2) (skS.0 14 a a_1 a_2 a_3) tptp0)) % 106.91/107.11 True) % 106.91/107.11 Clause #308 (by clausification #[45]): Eq % 106.91/107.11 (∀ (X105 : Iota), % 106.91/107.11 occurrence_of X105 tptp0 → % 106.91/107.11 Exists fun X106 => % 106.91/107.11 Exists fun X107 => % 106.91/107.11 And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of X106 tptp3) (root_occ X106 X105)) % 106.91/107.11 (Or (occurrence_of X107 tptp2) (occurrence_of X107 tptp1))) % 106.91/107.11 (min_precedes X106 X107 tptp0)) % 106.91/107.11 (leaf_occ X107 X105)) % 106.91/107.11 False % 106.91/107.11 Clause #309 (by clausification #[308]): ∀ (a : Iota), % 106.91/107.11 Eq % 106.91/107.11 (Not % 106.91/107.11 (occurrence_of (skS.0 16 a) tptp0 → % 106.91/107.11 Exists fun X106 => % 106.91/107.11 Exists fun X107 => % 106.91/107.11 And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of X106 tptp3) (root_occ X106 (skS.0 16 a))) % 106.91/107.11 (Or (occurrence_of X107 tptp2) (occurrence_of X107 tptp1))) % 106.91/107.11 (min_precedes X106 X107 tptp0)) % 106.91/107.11 (leaf_occ X107 (skS.0 16 a)))) % 106.91/107.11 True % 106.91/107.11 Clause #310 (by clausification #[309]): ∀ (a : Iota), % 106.91/107.11 Eq % 106.91/107.11 (occurrence_of (skS.0 16 a) tptp0 → % 106.91/107.11 Exists fun X106 => % 106.91/107.11 Exists fun X107 => % 106.91/107.11 And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of X106 tptp3) (root_occ X106 (skS.0 16 a))) % 106.91/107.11 (Or (occurrence_of X107 tptp2) (occurrence_of X107 tptp1))) % 106.91/107.11 (min_precedes X106 X107 tptp0)) % 106.91/107.11 (leaf_occ X107 (skS.0 16 a))) % 106.91/107.11 False % 106.91/107.11 Clause #311 (by clausification #[310]): ∀ (a : Iota), Eq (occurrence_of (skS.0 16 a) tptp0) True % 106.91/107.11 Clause #312 (by clausification #[310]): ∀ (a : Iota), % 106.91/107.11 Eq % 106.91/107.11 (Exists fun X106 => % 106.91/107.11 Exists fun X107 => % 106.91/107.11 And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of X106 tptp3) (root_occ X106 (skS.0 16 a))) % 106.91/107.11 (Or (occurrence_of X107 tptp2) (occurrence_of X107 tptp1))) % 106.91/107.11 (min_precedes X106 X107 tptp0)) % 106.91/107.11 (leaf_occ X107 (skS.0 16 a))) % 106.91/107.11 False % 106.91/107.11 Clause #313 (by superposition #[311, 298]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (leaf_occ (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) (skS.0 16 a)) True) % 106.91/107.11 Clause #342 (by clausification #[299]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.11 Or (Eq (occurrence_of a tptp0) False) (Eq (next_subocc (skS.0 13 a a_1 a_2) (skS.0 14 a a_1 a_2 a_3) tptp0) True) % 106.91/107.11 Clause #343 (by clausification #[299]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.11 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.11 (Eq % 106.91/107.11 (And % 106.91/107.11 (And % 106.91/107.11 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.91/107.11 (occurrence_of (skS.0 13 a a_1 a_2) tptp4)) % 106.91/107.11 (next_subocc (skS.0 12 a a_1) (skS.0 13 a a_1 a_2) tptp0)) % 106.91/107.11 (Or (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp1))) % 106.91/107.13 True) % 106.91/107.13 Clause #344 (by superposition #[342, 311]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.13 Or (Eq (next_subocc (skS.0 13 (skS.0 16 a) a_1 a_2) (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp0) True) (Eq False True) % 106.91/107.13 Clause #367 (by clausification #[312]): ∀ (a a_1 : Iota), % 106.91/107.13 Eq % 106.91/107.13 (Exists fun X107 => % 106.91/107.13 And % 106.91/107.13 (And % 106.91/107.13 (And (And (occurrence_of a tptp3) (root_occ a (skS.0 16 a_1))) % 106.91/107.13 (Or (occurrence_of X107 tptp2) (occurrence_of X107 tptp1))) % 106.91/107.13 (min_precedes a X107 tptp0)) % 106.91/107.13 (leaf_occ X107 (skS.0 16 a_1))) % 106.91/107.13 False % 106.91/107.13 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Eq % 106.91/107.13 (And % 106.91/107.13 (And % 106.91/107.13 (And (And (occurrence_of a tptp3) (root_occ a (skS.0 16 a_1))) % 106.91/107.13 (Or (occurrence_of a_2 tptp2) (occurrence_of a_2 tptp1))) % 106.91/107.13 (min_precedes a a_2 tptp0)) % 106.91/107.13 (leaf_occ a_2 (skS.0 16 a_1))) % 106.91/107.13 False % 106.91/107.13 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Or % 106.91/107.13 (Eq % 106.91/107.13 (And % 106.91/107.13 (And (And (occurrence_of a tptp3) (root_occ a (skS.0 16 a_1))) % 106.91/107.13 (Or (occurrence_of a_2 tptp2) (occurrence_of a_2 tptp1))) % 106.91/107.13 (min_precedes a a_2 tptp0)) % 106.91/107.13 False) % 106.91/107.13 (Eq (leaf_occ a_2 (skS.0 16 a_1)) False) % 106.91/107.13 Clause #370 (by clausification #[369]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Or (Eq (leaf_occ a (skS.0 16 a_1)) False) % 106.91/107.13 (Or % 106.91/107.13 (Eq % 106.91/107.13 (And (And (occurrence_of a_2 tptp3) (root_occ a_2 (skS.0 16 a_1))) % 106.91/107.13 (Or (occurrence_of a tptp2) (occurrence_of a tptp1))) % 106.91/107.13 False) % 106.91/107.13 (Eq (min_precedes a_2 a tptp0) False)) % 106.91/107.13 Clause #371 (by clausification #[370]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Or (Eq (leaf_occ a (skS.0 16 a_1)) False) % 106.91/107.13 (Or (Eq (min_precedes a_2 a tptp0) False) % 106.91/107.13 (Or (Eq (And (occurrence_of a_2 tptp3) (root_occ a_2 (skS.0 16 a_1))) False) % 106.91/107.13 (Eq (Or (occurrence_of a tptp2) (occurrence_of a tptp1)) False))) % 106.91/107.13 Clause #372 (by clausification #[371]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Or (Eq (leaf_occ a (skS.0 16 a_1)) False) % 106.91/107.13 (Or (Eq (min_precedes a_2 a tptp0) False) % 106.91/107.13 (Or (Eq (Or (occurrence_of a tptp2) (occurrence_of a tptp1)) False) % 106.91/107.13 (Or (Eq (occurrence_of a_2 tptp3) False) (Eq (root_occ a_2 (skS.0 16 a_1)) False)))) % 106.91/107.13 Clause #373 (by clausification #[372]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Or (Eq (leaf_occ a (skS.0 16 a_1)) False) % 106.91/107.13 (Or (Eq (min_precedes a_2 a tptp0) False) % 106.91/107.13 (Or (Eq (occurrence_of a_2 tptp3) False) % 106.91/107.13 (Or (Eq (root_occ a_2 (skS.0 16 a_1)) False) (Eq (occurrence_of a tptp1) False)))) % 106.91/107.13 Clause #374 (by clausification #[372]): ∀ (a a_1 a_2 : Iota), % 106.91/107.13 Or (Eq (leaf_occ a (skS.0 16 a_1)) False) % 106.91/107.13 (Or (Eq (min_precedes a_2 a tptp0) False) % 106.91/107.13 (Or (Eq (occurrence_of a_2 tptp3) False) % 106.91/107.13 (Or (Eq (root_occ a_2 (skS.0 16 a_1)) False) (Eq (occurrence_of a tptp2) False)))) % 106.91/107.13 Clause #382 (by clausification #[313]): ∀ (a a_1 a_2 a_3 : Iota), Eq (leaf_occ (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) (skS.0 16 a)) True % 106.91/107.13 Clause #384 (by superposition #[382, 373]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.91/107.13 Or (Eq True False) % 106.91/107.13 (Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp0) False) % 106.91/107.13 (Or (Eq (occurrence_of a tptp3) False) % 106.91/107.13 (Or (Eq (root_occ a (skS.0 16 a_1)) False) % 106.91/107.13 (Eq (occurrence_of (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp1) False)))) % 106.91/107.13 Clause #387 (by superposition #[382, 286]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.13 Or (Eq True False) (Eq (subactivity_occurrence (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) (skS.0 16 a)) True) % 106.91/107.13 Clause #400 (by clausification #[387]): ∀ (a a_1 a_2 a_3 : Iota), Eq (subactivity_occurrence (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) (skS.0 16 a)) True % 106.91/107.13 Clause #401 (by superposition #[400, 108]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 106.91/107.13 Or (Eq (subactivity_occurrence a (skS.0 16 a_1)) True) % 106.91/107.13 (Or (Eq True False) % 106.91/107.13 (Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) a_5) False) % 106.91/107.13 (Eq (occurrence_of (skS.0 16 a_1) a_5) False))) % 106.91/107.13 Clause #407 (by clausification #[343]): ∀ (a a_1 a_2 a_3 : Iota), % 106.91/107.13 Or (Eq (occurrence_of a tptp0) False) % 106.91/107.13 (Eq (Or (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp1)) True) % 106.99/107.16 Clause #408 (by clausification #[343]): ∀ (a a_1 a_2 : Iota), % 106.99/107.16 Or (Eq (occurrence_of a tptp0) False) % 106.99/107.16 (Eq % 106.99/107.16 (And % 106.99/107.16 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.99/107.16 (occurrence_of (skS.0 13 a a_1 a_2) tptp4)) % 106.99/107.16 (next_subocc (skS.0 12 a a_1) (skS.0 13 a a_1 a_2) tptp0)) % 106.99/107.16 True) % 106.99/107.16 Clause #409 (by clausification #[407]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.16 Or (Eq (occurrence_of a tptp0) False) % 106.99/107.16 (Or (Eq (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp2) True) % 106.99/107.16 (Eq (occurrence_of (skS.0 14 a a_1 a_2 a_3) tptp1) True)) % 106.99/107.16 Clause #410 (by superposition #[409, 311]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.16 Or (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) True) % 106.99/107.16 (Or (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp1) True) (Eq False True)) % 106.99/107.16 Clause #415 (by superposition #[374, 382]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.16 Or (Eq True False) % 106.99/107.16 (Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp0) False) % 106.99/107.16 (Or (Eq (occurrence_of a tptp3) False) % 106.99/107.16 (Or (Eq (root_occ a (skS.0 16 a_1)) False) % 106.99/107.16 (Eq (occurrence_of (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp2) False)))) % 106.99/107.16 Clause #416 (by clausification #[344]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.16 Eq (next_subocc (skS.0 13 (skS.0 16 a) a_1 a_2) (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp0) True % 106.99/107.16 Clause #420 (by superposition #[416, 289]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.16 Or (Eq True False) (Eq (min_precedes (skS.0 13 (skS.0 16 a) a_1 a_2) (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp0) True) % 106.99/107.16 Clause #425 (by clausification #[420]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.16 Eq (min_precedes (skS.0 13 (skS.0 16 a) a_1 a_2) (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp0) True % 106.99/107.16 Clause #430 (by superposition #[425, 230]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.16 Or (Eq True False) % 106.99/107.16 (Eq (min_precedes (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp0) % 106.99/107.16 True) % 106.99/107.16 Clause #431 (by superposition #[425, 231]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.16 Or (Eq True False) (Eq (root (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) tptp0) True) % 106.99/107.16 Clause #438 (by clausification #[431]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (root (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) tptp0) True % 106.99/107.16 Clause #442 (by superposition #[438, 248]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 106.99/107.16 Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) a_5) True) % 106.99/107.16 (Or (Eq True False) % 106.99/107.16 (Or (Eq (occurrence_of a_5 tptp0) False) % 106.99/107.16 (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) a_5) False))) % 106.99/107.16 Clause #492 (by clausification #[401]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 106.99/107.16 Or (Eq (subactivity_occurrence a (skS.0 16 a_1)) True) % 106.99/107.16 (Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) a_5) False) % 106.99/107.16 (Eq (occurrence_of (skS.0 16 a_1) a_5) False)) % 106.99/107.16 Clause #536 (by clausification #[410]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.16 Or (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) True) % 106.99/107.16 (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp1) True) % 106.99/107.16 Clause #573 (by clausification #[384]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.16 Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp0) False) % 106.99/107.16 (Or (Eq (occurrence_of a tptp3) False) % 106.99/107.16 (Or (Eq (root_occ a (skS.0 16 a_1)) False) % 106.99/107.16 (Eq (occurrence_of (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp1) False))) % 106.99/107.16 Clause #668 (by clausification #[408]): ∀ (a a_1 a_2 : Iota), % 106.99/107.16 Or (Eq (occurrence_of a tptp0) False) % 106.99/107.16 (Eq % 106.99/107.16 (And (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) % 106.99/107.16 (occurrence_of (skS.0 13 a a_1 a_2) tptp4)) % 106.99/107.16 True) % 106.99/107.16 Clause #697 (by clausification #[415]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.16 Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp0) False) % 106.99/107.16 (Or (Eq (occurrence_of a tptp3) False) % 106.99/107.16 (Or (Eq (root_occ a (skS.0 16 a_1)) False) % 106.99/107.16 (Eq (occurrence_of (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp2) False))) % 106.99/107.16 Clause #753 (by clausification #[668]): ∀ (a a_1 : Iota), % 106.99/107.16 Or (Eq (occurrence_of a tptp0) False) % 106.99/107.16 (Eq (And (occurrence_of (skS.0 12 a a_1) tptp3) (root_occ (skS.0 12 a a_1) a)) True) % 106.99/107.19 Clause #779 (by clausification #[430]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Eq (min_precedes (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp0) % 106.99/107.19 True % 106.99/107.19 Clause #781 (by superposition #[779, 697]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Or (Eq True False) % 106.99/107.19 (Or (Eq (occurrence_of (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) tptp3) False) % 106.99/107.19 (Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) False) % 106.99/107.19 (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) False))) % 106.99/107.19 Clause #782 (by superposition #[779, 492]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Or (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) True) % 106.99/107.19 (Or (Eq True False) (Eq (occurrence_of (skS.0 16 a) tptp0) False)) % 106.99/107.19 Clause #793 (by clausification #[753]): ∀ (a a_1 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (root_occ (skS.0 12 a a_1) a) True) % 106.99/107.19 Clause #794 (by clausification #[753]): ∀ (a a_1 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (occurrence_of (skS.0 12 a a_1) tptp3) True) % 106.99/107.19 Clause #795 (by superposition #[793, 311]): ∀ (a a_1 : Iota), Or (Eq (root_occ (skS.0 12 (skS.0 16 a) a_1) (skS.0 16 a)) True) (Eq False True) % 106.99/107.19 Clause #797 (by superposition #[794, 311]): ∀ (a a_1 : Iota), Or (Eq (occurrence_of (skS.0 12 (skS.0 16 a) a_1) tptp3) True) (Eq False True) % 106.99/107.19 Clause #801 (by clausification #[797]): ∀ (a a_1 : Iota), Eq (occurrence_of (skS.0 12 (skS.0 16 a) a_1) tptp3) True % 106.99/107.19 Clause #822 (by clausification #[795]): ∀ (a a_1 : Iota), Eq (root_occ (skS.0 12 (skS.0 16 a) a_1) (skS.0 16 a)) True % 106.99/107.19 Clause #824 (by superposition #[822, 160]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.19 Or (Eq True False) % 106.99/107.19 (Or (Eq a (skS.0 12 (skS.0 16 a_1) a_2)) % 106.99/107.19 (Or (Eq (occurrence_of (skS.0 16 a_1) a_3) False) (Eq (root_occ a (skS.0 16 a_1)) False))) % 106.99/107.19 Clause #847 (by clausification #[824]): ∀ (a a_1 a_2 a_3 : Iota), % 106.99/107.19 Or (Eq a (skS.0 12 (skS.0 16 a_1) a_2)) % 106.99/107.19 (Or (Eq (occurrence_of (skS.0 16 a_1) a_3) False) (Eq (root_occ a (skS.0 16 a_1)) False)) % 106.99/107.19 Clause #848 (by superposition #[847, 311]): ∀ (a a_1 a_2 : Iota), % 106.99/107.19 Or (Eq a (skS.0 12 (skS.0 16 a_1) a_2)) (Or (Eq (root_occ a (skS.0 16 a_1)) False) (Eq False True)) % 106.99/107.19 Clause #849 (by clausification #[848]): ∀ (a a_1 a_2 : Iota), Or (Eq a (skS.0 12 (skS.0 16 a_1) a_2)) (Eq (root_occ a (skS.0 16 a_1)) False) % 106.99/107.19 Clause #899 (by clausification #[442]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 106.99/107.19 Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) a_5) True) % 106.99/107.19 (Or (Eq (occurrence_of a_5 tptp0) False) % 106.99/107.19 (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) a_5) False)) % 106.99/107.19 Clause #900 (by superposition #[899, 311]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 106.99/107.19 Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a_5)) True) % 106.99/107.19 (Or (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a_5)) False) % 106.99/107.19 (Eq False True)) % 106.99/107.19 Clause #1312 (by clausification #[782]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Or (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) True) % 106.99/107.19 (Eq (occurrence_of (skS.0 16 a) tptp0) False) % 106.99/107.19 Clause #1313 (by forward demodulation #[1312, 311]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Or (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) True) % 106.99/107.19 (Eq True False) % 106.99/107.19 Clause #1314 (by clausification #[1313]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) True % 106.99/107.19 Clause #2347 (by clausification #[781]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 106.99/107.19 Or (Eq (occurrence_of (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) tptp3) False) % 106.99/107.19 (Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) False) % 106.99/107.19 (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) False)) % 106.99/107.19 Clause #2745 (by clausification #[900]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 107.05/107.24 Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a_5)) True) % 107.05/107.24 (Eq (subactivity_occurrence (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a_5)) False) % 107.05/107.24 Clause #2746 (by superposition #[2745, 1314]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 107.05/107.24 Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) True) (Eq False True) % 107.05/107.24 Clause #2747 (by clausification #[2746]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) True % 107.05/107.24 Clause #2749 (by superposition #[2747, 849]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 107.05/107.24 Or (Eq (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 12 (skS.0 16 a) a_5)) (Eq True False) % 107.05/107.24 Clause #2756 (by clausification #[2749]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 12 (skS.0 16 a) a_5) % 107.05/107.24 Clause #2757 (by superposition #[2756, 779]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 107.05/107.24 Eq (min_precedes (skS.0 12 (skS.0 16 a) a_1) (skS.0 14 (skS.0 16 a) a_2 a_3 a_4) tptp0) True % 107.05/107.24 Clause #2773 (by superposition #[2756, 801]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (occurrence_of (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) tptp3) True % 107.05/107.24 Clause #2836 (by backward demodulation #[2773, 2347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 107.05/107.24 Or (Eq True False) % 107.05/107.24 (Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) False) % 107.05/107.24 (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) False)) % 107.05/107.24 Clause #3246 (by clausification #[2836]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 107.05/107.24 Or (Eq (root_occ (skS.0 5 tptp0 (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) a_4) (skS.0 16 a)) False) % 107.05/107.24 (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) False) % 107.05/107.24 Clause #3247 (by superposition #[3246, 2747]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) False) (Eq False True) % 107.05/107.24 Clause #3249 (by clausification #[3247]): ∀ (a a_1 a_2 a_3 : Iota), Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp2) False % 107.05/107.24 Clause #3251 (by superposition #[3249, 536]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq False True) (Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp1) True) % 107.05/107.24 Clause #3252 (by clausification #[3251]): ∀ (a a_1 a_2 a_3 : Iota), Eq (occurrence_of (skS.0 14 (skS.0 16 a) a_1 a_2 a_3) tptp1) True % 107.05/107.24 Clause #3254 (by backward demodulation #[3252, 573]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 107.05/107.24 Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp0) False) % 107.05/107.24 (Or (Eq (occurrence_of a tptp3) False) (Or (Eq (root_occ a (skS.0 16 a_1)) False) (Eq True False))) % 107.05/107.24 Clause #3304 (by clausification #[3254]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 107.05/107.24 Or (Eq (min_precedes a (skS.0 14 (skS.0 16 a_1) a_2 a_3 a_4) tptp0) False) % 107.05/107.24 (Or (Eq (occurrence_of a tptp3) False) (Eq (root_occ a (skS.0 16 a_1)) False)) % 107.05/107.24 Clause #3308 (by superposition #[3304, 2757]): ∀ (a a_1 : Iota), % 107.05/107.24 Or (Eq (occurrence_of (skS.0 12 (skS.0 16 a) a_1) tptp3) False) % 107.05/107.24 (Or (Eq (root_occ (skS.0 12 (skS.0 16 a) a_1) (skS.0 16 a)) False) (Eq False True)) % 107.05/107.24 Clause #3313 (by clausification #[3308]): ∀ (a a_1 : Iota), % 107.05/107.24 Or (Eq (occurrence_of (skS.0 12 (skS.0 16 a) a_1) tptp3) False) % 107.05/107.24 (Eq (root_occ (skS.0 12 (skS.0 16 a) a_1) (skS.0 16 a)) False) % 107.05/107.24 Clause #3314 (by forward demodulation #[3313, 801]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (root_occ (skS.0 12 (skS.0 16 a) a_1) (skS.0 16 a)) False) % 107.05/107.24 Clause #3315 (by clausification #[3314]): ∀ (a a_1 : Iota), Eq (root_occ (skS.0 12 (skS.0 16 a) a_1) (skS.0 16 a)) False % 107.05/107.24 Clause #3316 (by superposition #[3315, 822]): Eq False True % 107.05/107.24 Clause #3317 (by clausification #[3316]): False % 107.05/107.24 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------