%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PRO011+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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 10.21s 10.44s % Output : Proof 10.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO011+3 : TPTP v9.2.0. Released v4.0.0. % 0.11/0.13 % Command : duper %s % 0.14/0.35 % Computer : n001.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 08:40:38 EDT 2025 % 0.14/0.35 % CPUTime : % 10.21/10.44 SZS status Theorem for theBenchmark.p % 10.21/10.44 SZS output start Proof for theBenchmark.p % 10.21/10.44 Clause #2 (by assumption #[]): Eq (∀ (X4 X5 X6 : Iota), And (occurrence_of X4 X5) (occurrence_of X4 X6) → Eq X5 X6) True % 10.21/10.44 Clause #37 (by assumption #[]): Eq % 10.21/10.44 (∀ (X113 X114 X115 : Iota), % 10.21/10.44 And (occurrence_of X113 X115) (leaf_occ X114 X113) → Not (Exists fun X116 => min_precedes X114 X116 X115)) % 10.21/10.44 True % 10.21/10.44 Clause #49 (by assumption #[]): Eq % 10.21/10.44 (∀ (X161 : Iota), % 10.21/10.44 occurrence_of X161 tptp0 → % 10.21/10.44 Exists fun X162 => % 10.21/10.44 Exists fun X163 => % 10.21/10.44 Exists fun X164 => % 10.21/10.44 And % 10.21/10.44 (And % 10.21/10.44 (And % 10.21/10.44 (And (And (And (occurrence_of X162 tptp3) (root_occ X162 X161)) (occurrence_of X163 tptp4)) % 10.21/10.44 (next_subocc X162 X163 tptp0)) % 10.21/10.44 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 10.21/10.44 (next_subocc X163 X164 tptp0)) % 10.21/10.44 (leaf_occ X164 X161)) % 10.21/10.44 True % 10.21/10.44 Clause #61 (by assumption #[]): Eq (Ne tptp1 tptp2) True % 10.21/10.44 Clause #62 (by assumption #[]): Eq % 10.21/10.44 (Not % 10.21/10.44 (∀ (X165 : Iota), % 10.21/10.44 occurrence_of X165 tptp0 → % 10.21/10.44 Exists fun X166 => % 10.21/10.44 Exists fun X167 => % 10.21/10.44 And % 10.21/10.44 (And (leaf_occ X167 X165) % 10.21/10.44 (occurrence_of X167 tptp1 → % 10.21/10.44 Not % 10.21/10.44 (Exists fun X168 => % 10.21/10.44 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 X165)) % 10.21/10.44 (min_precedes X166 X168 tptp0)))) % 10.21/10.44 (occurrence_of X167 tptp2 → % 10.21/10.44 Not % 10.21/10.44 (Exists fun X169 => % 10.21/10.44 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 X165)) % 10.21/10.44 (min_precedes X166 X169 tptp0))))) % 10.21/10.44 True % 10.21/10.44 Clause #71 (by clausification #[61]): Ne tptp1 tptp2 % 10.21/10.44 Clause #89 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (X5 X6 : Iota), And (occurrence_of a X5) (occurrence_of a X6) → Eq X5 X6) True % 10.21/10.44 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), Eq (∀ (X6 : Iota), And (occurrence_of a a_1) (occurrence_of a X6) → Eq a_1 X6) True % 10.21/10.44 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), Eq (And (occurrence_of a a_1) (occurrence_of a a_2) → Eq a_1 a_2) True % 10.21/10.44 Clause #92 (by clausification #[91]): ∀ (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) % 10.21/10.44 Clause #93 (by clausification #[92]): ∀ (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)) % 10.21/10.44 Clause #94 (by clausification #[93]): ∀ (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)) % 10.21/10.44 Clause #308 (by clausification #[37]): ∀ (a : Iota), % 10.21/10.44 Eq % 10.21/10.44 (∀ (X114 X115 : Iota), % 10.21/10.44 And (occurrence_of a X115) (leaf_occ X114 a) → Not (Exists fun X116 => min_precedes X114 X116 X115)) % 10.21/10.44 True % 10.21/10.44 Clause #309 (by clausification #[308]): ∀ (a a_1 : Iota), % 10.21/10.44 Eq % 10.21/10.44 (∀ (X115 : Iota), And (occurrence_of a X115) (leaf_occ a_1 a) → Not (Exists fun X116 => min_precedes a_1 X116 X115)) % 10.21/10.44 True % 10.21/10.44 Clause #310 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), % 10.21/10.44 Eq (And (occurrence_of a a_1) (leaf_occ a_2 a) → Not (Exists fun X116 => min_precedes a_2 X116 a_1)) True % 10.21/10.44 Clause #311 (by clausification #[310]): ∀ (a a_1 a_2 : Iota), % 10.21/10.44 Or (Eq (And (occurrence_of a a_1) (leaf_occ a_2 a)) False) % 10.21/10.44 (Eq (Not (Exists fun X116 => min_precedes a_2 X116 a_1)) True) % 10.21/10.44 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), % 10.21/10.44 Or (Eq (Not (Exists fun X116 => min_precedes a X116 a_1)) True) % 10.21/10.44 (Or (Eq (occurrence_of a_2 a_1) False) (Eq (leaf_occ a a_2) False)) % 10.21/10.44 Clause #313 (by clausification #[312]): ∀ (a a_1 a_2 : Iota), % 10.21/10.44 Or (Eq (occurrence_of a a_1) False) % 10.21/10.44 (Or (Eq (leaf_occ a_2 a) False) (Eq (Exists fun X116 => min_precedes a_2 X116 a_1) False)) % 10.21/10.44 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 a_3 : Iota), % 10.21/10.44 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)) % 10.21/10.44 Clause #428 (by clausification #[49]): ∀ (a : Iota), % 10.21/10.44 Eq % 10.21/10.44 (occurrence_of a tptp0 → % 10.21/10.46 Exists fun X162 => % 10.21/10.46 Exists fun X163 => % 10.21/10.46 Exists fun X164 => % 10.21/10.46 And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And (And (And (occurrence_of X162 tptp3) (root_occ X162 a)) (occurrence_of X163 tptp4)) % 10.21/10.46 (next_subocc X162 X163 tptp0)) % 10.21/10.46 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 10.21/10.46 (next_subocc X163 X164 tptp0)) % 10.21/10.46 (leaf_occ X164 a)) % 10.21/10.46 True % 10.21/10.46 Clause #429 (by clausification #[428]): ∀ (a : Iota), % 10.21/10.46 Or (Eq (occurrence_of a tptp0) False) % 10.21/10.46 (Eq % 10.21/10.46 (Exists fun X162 => % 10.21/10.46 Exists fun X163 => % 10.21/10.46 Exists fun X164 => % 10.21/10.46 And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And (And (And (occurrence_of X162 tptp3) (root_occ X162 a)) (occurrence_of X163 tptp4)) % 10.21/10.46 (next_subocc X162 X163 tptp0)) % 10.21/10.46 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 10.21/10.46 (next_subocc X163 X164 tptp0)) % 10.21/10.46 (leaf_occ X164 a)) % 10.21/10.46 True) % 10.21/10.46 Clause #430 (by clausification #[429]): ∀ (a a_1 : Iota), % 10.21/10.46 Or (Eq (occurrence_of a tptp0) False) % 10.21/10.46 (Eq % 10.21/10.46 (Exists fun X163 => % 10.21/10.46 Exists fun X164 => % 10.21/10.46 And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And (And (occurrence_of (skS.0 15 a a_1) tptp3) (root_occ (skS.0 15 a a_1) a)) % 10.21/10.46 (occurrence_of X163 tptp4)) % 10.21/10.46 (next_subocc (skS.0 15 a a_1) X163 tptp0)) % 10.21/10.46 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 10.21/10.46 (next_subocc X163 X164 tptp0)) % 10.21/10.46 (leaf_occ X164 a)) % 10.21/10.46 True) % 10.21/10.46 Clause #431 (by clausification #[430]): ∀ (a a_1 a_2 : Iota), % 10.21/10.46 Or (Eq (occurrence_of a tptp0) False) % 10.21/10.46 (Eq % 10.21/10.46 (Exists fun X164 => % 10.21/10.46 And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And (And (occurrence_of (skS.0 15 a a_1) tptp3) (root_occ (skS.0 15 a a_1) a)) % 10.21/10.46 (occurrence_of (skS.0 16 a a_1 a_2) tptp4)) % 10.21/10.46 (next_subocc (skS.0 15 a a_1) (skS.0 16 a a_1 a_2) tptp0)) % 10.21/10.46 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 10.21/10.46 (next_subocc (skS.0 16 a a_1 a_2) X164 tptp0)) % 10.21/10.46 (leaf_occ X164 a)) % 10.21/10.46 True) % 10.21/10.46 Clause #432 (by clausification #[431]): ∀ (a a_1 a_2 a_3 : Iota), % 10.21/10.46 Or (Eq (occurrence_of a tptp0) False) % 10.21/10.46 (Eq % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And % 10.21/10.46 (And (And (occurrence_of (skS.0 15 a a_1) tptp3) (root_occ (skS.0 15 a a_1) a)) % 10.21/10.46 (occurrence_of (skS.0 16 a a_1 a_2) tptp4)) % 10.21/10.46 (next_subocc (skS.0 15 a a_1) (skS.0 16 a a_1 a_2) tptp0)) % 10.21/10.46 (Or (occurrence_of (skS.0 17 a a_1 a_2 a_3) tptp1) (occurrence_of (skS.0 17 a a_1 a_2 a_3) tptp2))) % 10.21/10.46 (next_subocc (skS.0 16 a a_1 a_2) (skS.0 17 a a_1 a_2 a_3) tptp0)) % 10.21/10.46 (leaf_occ (skS.0 17 a a_1 a_2 a_3) a)) % 10.21/10.46 True) % 10.21/10.46 Clause #433 (by clausification #[432]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (leaf_occ (skS.0 17 a a_1 a_2 a_3) a) True) % 10.21/10.46 Clause #442 (by clausification #[62]): Eq % 10.21/10.46 (∀ (X165 : Iota), % 10.21/10.46 occurrence_of X165 tptp0 → % 10.21/10.46 Exists fun X166 => % 10.21/10.46 Exists fun X167 => % 10.21/10.46 And % 10.21/10.46 (And (leaf_occ X167 X165) % 10.21/10.46 (occurrence_of X167 tptp1 → % 10.21/10.46 Not % 10.21/10.46 (Exists fun X168 => % 10.21/10.46 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 X165)) % 10.21/10.46 (min_precedes X166 X168 tptp0)))) % 10.21/10.46 (occurrence_of X167 tptp2 → % 10.21/10.46 Not % 10.21/10.46 (Exists fun X169 => % 10.21/10.46 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 X165)) % 10.21/10.46 (min_precedes X166 X169 tptp0)))) % 10.21/10.46 False % 10.21/10.46 Clause #443 (by clausification #[442]): ∀ (a : Iota), % 10.21/10.46 Eq % 10.21/10.46 (Not % 10.21/10.46 (occurrence_of (skS.0 19 a) tptp0 → % 10.21/10.46 Exists fun X166 => % 10.21/10.46 Exists fun X167 => % 10.21/10.46 And % 10.21/10.46 (And (leaf_occ X167 (skS.0 19 a)) % 10.21/10.46 (occurrence_of X167 tptp1 → % 10.21/10.46 Not % 10.21/10.46 (Exists fun X168 => % 10.28/10.48 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a))) % 10.28/10.48 (min_precedes X166 X168 tptp0)))) % 10.28/10.48 (occurrence_of X167 tptp2 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X169 => % 10.28/10.48 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a))) % 10.28/10.48 (min_precedes X166 X169 tptp0))))) % 10.28/10.48 True % 10.28/10.48 Clause #444 (by clausification #[443]): ∀ (a : Iota), % 10.28/10.48 Eq % 10.28/10.48 (occurrence_of (skS.0 19 a) tptp0 → % 10.28/10.48 Exists fun X166 => % 10.28/10.48 Exists fun X167 => % 10.28/10.48 And % 10.28/10.48 (And (leaf_occ X167 (skS.0 19 a)) % 10.28/10.48 (occurrence_of X167 tptp1 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X168 => % 10.28/10.48 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a))) % 10.28/10.48 (min_precedes X166 X168 tptp0)))) % 10.28/10.48 (occurrence_of X167 tptp2 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X169 => % 10.28/10.48 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a))) % 10.28/10.48 (min_precedes X166 X169 tptp0)))) % 10.28/10.48 False % 10.28/10.48 Clause #445 (by clausification #[444]): ∀ (a : Iota), Eq (occurrence_of (skS.0 19 a) tptp0) True % 10.28/10.48 Clause #446 (by clausification #[444]): ∀ (a : Iota), % 10.28/10.48 Eq % 10.28/10.48 (Exists fun X166 => % 10.28/10.48 Exists fun X167 => % 10.28/10.48 And % 10.28/10.48 (And (leaf_occ X167 (skS.0 19 a)) % 10.28/10.48 (occurrence_of X167 tptp1 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X168 => % 10.28/10.48 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a))) % 10.28/10.48 (min_precedes X166 X168 tptp0)))) % 10.28/10.48 (occurrence_of X167 tptp2 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X169 => % 10.28/10.48 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a))) % 10.28/10.48 (min_precedes X166 X169 tptp0)))) % 10.28/10.48 False % 10.28/10.48 Clause #447 (by superposition #[445, 433]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (leaf_occ (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) (skS.0 19 a)) True) % 10.28/10.48 Clause #453 (by superposition #[445, 314]): ∀ (a a_1 a_2 : Iota), % 10.28/10.48 Or (Eq True False) (Or (Eq (leaf_occ a (skS.0 19 a_1)) False) (Eq (min_precedes a a_2 tptp0) False)) % 10.28/10.48 Clause #471 (by clausification #[453]): ∀ (a a_1 a_2 : Iota), Or (Eq (leaf_occ a (skS.0 19 a_1)) False) (Eq (min_precedes a a_2 tptp0) False) % 10.28/10.48 Clause #528 (by clausification #[447]): ∀ (a a_1 a_2 a_3 : Iota), Eq (leaf_occ (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) (skS.0 19 a)) True % 10.28/10.48 Clause #529 (by superposition #[528, 471]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (min_precedes (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) a_4 tptp0) False) % 10.28/10.48 Clause #536 (by clausification #[529]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (min_precedes (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) a_4 tptp0) False % 10.28/10.48 Clause #577 (by clausification #[446]): ∀ (a a_1 : Iota), % 10.28/10.48 Eq % 10.28/10.48 (Exists fun X167 => % 10.28/10.48 And % 10.28/10.48 (And (leaf_occ X167 (skS.0 19 a)) % 10.28/10.48 (occurrence_of X167 tptp1 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X168 => % 10.28/10.48 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a))) % 10.28/10.48 (min_precedes a_1 X168 tptp0)))) % 10.28/10.48 (occurrence_of X167 tptp2 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X169 => % 10.28/10.48 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a))) % 10.28/10.48 (min_precedes a_1 X169 tptp0)))) % 10.28/10.48 False % 10.28/10.48 Clause #578 (by clausification #[577]): ∀ (a a_1 a_2 : Iota), % 10.28/10.48 Eq % 10.28/10.48 (And % 10.28/10.48 (And (leaf_occ a (skS.0 19 a_1)) % 10.28/10.48 (occurrence_of a tptp1 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X168 => % 10.28/10.48 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.48 (min_precedes a_2 X168 tptp0)))) % 10.28/10.48 (occurrence_of a tptp2 → % 10.28/10.48 Not % 10.28/10.48 (Exists fun X169 => % 10.28/10.48 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a_1))) % 10.28/10.48 (min_precedes a_2 X169 tptp0)))) % 10.28/10.48 False % 10.28/10.48 Clause #579 (by clausification #[578]): ∀ (a a_1 a_2 : Iota), % 10.28/10.48 Or % 10.28/10.48 (Eq % 10.28/10.50 (And (leaf_occ a (skS.0 19 a_1)) % 10.28/10.50 (occurrence_of a tptp1 → % 10.28/10.50 Not % 10.28/10.50 (Exists fun X168 => % 10.28/10.50 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X168 tptp0)))) % 10.28/10.50 False) % 10.28/10.50 (Eq % 10.28/10.50 (occurrence_of a tptp2 → % 10.28/10.50 Not % 10.28/10.50 (Exists fun X169 => % 10.28/10.50 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X169 tptp0))) % 10.28/10.50 False) % 10.28/10.50 Clause #580 (by clausification #[579]): ∀ (a a_1 a_2 : Iota), % 10.28/10.50 Or % 10.28/10.50 (Eq % 10.28/10.50 (occurrence_of a tptp2 → % 10.28/10.50 Not % 10.28/10.50 (Exists fun X169 => % 10.28/10.50 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X169 tptp0))) % 10.28/10.50 False) % 10.28/10.50 (Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Eq % 10.28/10.50 (occurrence_of a tptp1 → % 10.28/10.50 Not % 10.28/10.50 (Exists fun X168 => % 10.28/10.50 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X168 tptp0))) % 10.28/10.50 False)) % 10.28/10.50 Clause #581 (by clausification #[580]): ∀ (a a_1 a_2 : Iota), % 10.28/10.50 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Or % 10.28/10.50 (Eq % 10.28/10.50 (occurrence_of a tptp1 → % 10.28/10.50 Not % 10.28/10.50 (Exists fun X168 => % 10.28/10.50 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X168 tptp0))) % 10.28/10.50 False) % 10.28/10.50 (Eq (occurrence_of a tptp2) True)) % 10.28/10.50 Clause #582 (by clausification #[580]): ∀ (a a_1 a_2 : Iota), % 10.28/10.50 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Or % 10.28/10.50 (Eq % 10.28/10.50 (occurrence_of a tptp1 → % 10.28/10.50 Not % 10.28/10.50 (Exists fun X168 => % 10.28/10.50 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X168 tptp0))) % 10.28/10.50 False) % 10.28/10.50 (Eq % 10.28/10.50 (Not % 10.28/10.50 (Exists fun X169 => % 10.28/10.50 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X169 tptp0))) % 10.28/10.50 False)) % 10.28/10.50 Clause #584 (by clausification #[581]): ∀ (a a_1 a_2 : Iota), % 10.28/10.50 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Or (Eq (occurrence_of a tptp2) True) % 10.28/10.50 (Eq % 10.28/10.50 (Not % 10.28/10.50 (Exists fun X168 => % 10.28/10.50 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X168 tptp0))) % 10.28/10.50 False)) % 10.28/10.50 Clause #625 (by clausification #[584]): ∀ (a a_1 a_2 : Iota), % 10.28/10.50 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Or (Eq (occurrence_of a tptp2) True) % 10.28/10.50 (Eq % 10.28/10.50 (Exists fun X168 => % 10.28/10.50 And (And (occurrence_of X168 tptp2) (subactivity_occurrence X168 (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 X168 tptp0)) % 10.28/10.50 True)) % 10.28/10.50 Clause #626 (by clausification #[625]): ∀ (a a_1 a_2 a_3 : Iota), % 10.28/10.50 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Or (Eq (occurrence_of a tptp2) True) % 10.28/10.50 (Eq % 10.28/10.50 (And % 10.28/10.50 (And (occurrence_of (skS.0 21 a_1 a_2 a_3) tptp2) % 10.28/10.50 (subactivity_occurrence (skS.0 21 a_1 a_2 a_3) (skS.0 19 a_1))) % 10.28/10.50 (min_precedes a_2 (skS.0 21 a_1 a_2 a_3) tptp0)) % 10.28/10.50 True)) % 10.28/10.50 Clause #627 (by clausification #[626]): ∀ (a a_1 a_2 a_3 : Iota), % 10.28/10.50 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.50 (Or (Eq (occurrence_of a tptp2) True) (Eq (min_precedes a_2 (skS.0 21 a_1 a_2 a_3) tptp0) True)) % 10.28/10.50 Clause #629 (by superposition #[627, 528]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.28/10.50 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp2) True) % 10.28/10.50 (Or (Eq (min_precedes a_4 (skS.0 21 a a_4 a_5) tptp0) True) (Eq False True)) % 10.28/10.50 Clause #630 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.28/10.50 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp2) True) % 10.28/10.50 (Eq (min_precedes a_4 (skS.0 21 a a_4 a_5) tptp0) True) % 10.28/10.50 Clause #641 (by superposition #[630, 536]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp2) True) (Eq True False) % 10.28/10.50 Clause #720 (by clausification #[641]): ∀ (a a_1 a_2 a_3 : Iota), Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp2) True % 10.28/10.52 Clause #721 (by superposition #[720, 94]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.28/10.52 Or (Eq True False) (Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) a_4) False) (Eq tptp2 a_4)) % 10.28/10.52 Clause #734 (by clausification #[721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) a_4) False) (Eq tptp2 a_4) % 10.28/10.52 Clause #1149 (by clausification #[582]): ∀ (a a_1 a_2 : Iota), % 10.28/10.52 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.52 (Or % 10.28/10.52 (Eq % 10.28/10.52 (Not % 10.28/10.52 (Exists fun X169 => % 10.28/10.52 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a_1))) % 10.28/10.52 (min_precedes a_2 X169 tptp0))) % 10.28/10.52 False) % 10.28/10.52 (Eq (occurrence_of a tptp1) True)) % 10.28/10.52 Clause #1151 (by clausification #[1149]): ∀ (a a_1 a_2 : Iota), % 10.28/10.52 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.52 (Or (Eq (occurrence_of a tptp1) True) % 10.28/10.52 (Eq % 10.28/10.52 (Exists fun X169 => % 10.28/10.52 And (And (occurrence_of X169 tptp1) (subactivity_occurrence X169 (skS.0 19 a_1))) % 10.28/10.52 (min_precedes a_2 X169 tptp0)) % 10.28/10.52 True)) % 10.28/10.52 Clause #1152 (by clausification #[1151]): ∀ (a a_1 a_2 a_3 : Iota), % 10.28/10.52 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.52 (Or (Eq (occurrence_of a tptp1) True) % 10.28/10.52 (Eq % 10.28/10.52 (And % 10.28/10.52 (And (occurrence_of (skS.0 22 a_1 a_2 a_3) tptp1) % 10.28/10.52 (subactivity_occurrence (skS.0 22 a_1 a_2 a_3) (skS.0 19 a_1))) % 10.28/10.52 (min_precedes a_2 (skS.0 22 a_1 a_2 a_3) tptp0)) % 10.28/10.52 True)) % 10.28/10.52 Clause #1153 (by clausification #[1152]): ∀ (a a_1 a_2 a_3 : Iota), % 10.28/10.52 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 10.28/10.52 (Or (Eq (occurrence_of a tptp1) True) (Eq (min_precedes a_2 (skS.0 22 a_1 a_2 a_3) tptp0) True)) % 10.28/10.52 Clause #1155 (by superposition #[1153, 528]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.28/10.52 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp1) True) % 10.28/10.52 (Or (Eq (min_precedes a_4 (skS.0 22 a a_4 a_5) tptp0) True) (Eq False True)) % 10.28/10.52 Clause #1157 (by clausification #[1155]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.28/10.52 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp1) True) % 10.28/10.52 (Eq (min_precedes a_4 (skS.0 22 a a_4 a_5) tptp0) True) % 10.28/10.52 Clause #1158 (by superposition #[1157, 734]): ∀ (a a_1 a_2 : Iota), Or (Eq (min_precedes a (skS.0 22 a_1 a a_2) tptp0) True) (Or (Eq True False) (Eq tptp2 tptp1)) % 10.28/10.52 Clause #1190 (by clausification #[1158]): ∀ (a a_1 a_2 : Iota), Or (Eq (min_precedes a (skS.0 22 a_1 a a_2) tptp0) True) (Eq tptp2 tptp1) % 10.28/10.52 Clause #1191 (by forward contextual literal cutting #[1190, 71]): ∀ (a a_1 a_2 : Iota), Eq (min_precedes a (skS.0 22 a_1 a a_2) tptp0) True % 10.28/10.52 Clause #1192 (by superposition #[1191, 536]): Eq True False % 10.28/10.52 Clause #1211 (by clausification #[1192]): False % 10.28/10.52 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------