%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PRO010+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.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 8.01s 8.25s % Output : Proof 8.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PRO010+3 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n018.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:43:38 EDT 2025 % 0.13/0.34 % CPUTime : % 8.01/8.25 SZS status Theorem for theBenchmark.p % 8.01/8.25 SZS output start Proof for theBenchmark.p % 8.01/8.25 Clause #2 (by assumption #[]): Eq (∀ (X4 X5 X6 : Iota), And (occurrence_of X4 X5) (occurrence_of X4 X6) → Eq X5 X6) True % 8.01/8.25 Clause #37 (by assumption #[]): Eq % 8.01/8.25 (∀ (X113 X114 X115 : Iota), % 8.01/8.25 And (occurrence_of X113 X115) (leaf_occ X114 X113) → Not (Exists fun X116 => min_precedes X114 X116 X115)) % 8.01/8.25 True % 8.01/8.25 Clause #49 (by assumption #[]): Eq % 8.01/8.25 (∀ (X161 : Iota), % 8.01/8.25 occurrence_of X161 tptp0 → % 8.01/8.25 Exists fun X162 => % 8.01/8.25 Exists fun X163 => % 8.01/8.25 Exists fun X164 => % 8.01/8.25 And % 8.01/8.25 (And % 8.01/8.25 (And % 8.01/8.25 (And (And (And (occurrence_of X162 tptp3) (root_occ X162 X161)) (occurrence_of X163 tptp4)) % 8.01/8.25 (next_subocc X162 X163 tptp0)) % 8.01/8.25 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 8.01/8.25 (next_subocc X163 X164 tptp0)) % 8.01/8.25 (leaf_occ X164 X161)) % 8.01/8.25 True % 8.01/8.25 Clause #61 (by assumption #[]): Eq (Ne tptp1 tptp2) True % 8.01/8.25 Clause #62 (by assumption #[]): Eq % 8.01/8.25 (Not % 8.01/8.25 (∀ (X165 : Iota), % 8.01/8.25 occurrence_of X165 tptp0 → % 8.01/8.25 Exists fun X166 => % 8.01/8.25 Exists fun X167 => % 8.01/8.25 And % 8.01/8.25 (And (leaf_occ X167 X165) % 8.01/8.25 (occurrence_of X167 tptp1 → % 8.01/8.25 Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes X166 X168 tptp0)))) % 8.01/8.25 (occurrence_of X167 tptp2 → % 8.01/8.25 Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes X166 X169 tptp0))))) % 8.01/8.25 True % 8.01/8.25 Clause #71 (by clausification #[61]): Ne tptp1 tptp2 % 8.01/8.25 Clause #89 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (X5 X6 : Iota), And (occurrence_of a X5) (occurrence_of a X6) → Eq X5 X6) True % 8.01/8.25 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 % 8.01/8.25 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 % 8.01/8.25 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) % 8.01/8.25 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)) % 8.01/8.25 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)) % 8.01/8.25 Clause #308 (by clausification #[37]): ∀ (a : Iota), % 8.01/8.25 Eq % 8.01/8.25 (∀ (X114 X115 : Iota), % 8.01/8.25 And (occurrence_of a X115) (leaf_occ X114 a) → Not (Exists fun X116 => min_precedes X114 X116 X115)) % 8.01/8.25 True % 8.01/8.25 Clause #309 (by clausification #[308]): ∀ (a a_1 : Iota), % 8.01/8.25 Eq % 8.01/8.25 (∀ (X115 : Iota), And (occurrence_of a X115) (leaf_occ a_1 a) → Not (Exists fun X116 => min_precedes a_1 X116 X115)) % 8.01/8.25 True % 8.01/8.25 Clause #310 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), % 8.01/8.25 Eq (And (occurrence_of a a_1) (leaf_occ a_2 a) → Not (Exists fun X116 => min_precedes a_2 X116 a_1)) True % 8.01/8.25 Clause #311 (by clausification #[310]): ∀ (a a_1 a_2 : Iota), % 8.01/8.25 Or (Eq (And (occurrence_of a a_1) (leaf_occ a_2 a)) False) % 8.01/8.25 (Eq (Not (Exists fun X116 => min_precedes a_2 X116 a_1)) True) % 8.01/8.25 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), % 8.01/8.25 Or (Eq (Not (Exists fun X116 => min_precedes a X116 a_1)) True) % 8.01/8.25 (Or (Eq (occurrence_of a_2 a_1) False) (Eq (leaf_occ a a_2) False)) % 8.01/8.25 Clause #313 (by clausification #[312]): ∀ (a a_1 a_2 : Iota), % 8.01/8.25 Or (Eq (occurrence_of a a_1) False) % 8.01/8.25 (Or (Eq (leaf_occ a_2 a) False) (Eq (Exists fun X116 => min_precedes a_2 X116 a_1) False)) % 8.01/8.25 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 a_3 : Iota), % 8.01/8.25 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)) % 8.01/8.25 Clause #428 (by clausification #[49]): ∀ (a : Iota), % 8.01/8.25 Eq % 8.01/8.25 (occurrence_of a tptp0 → % 8.01/8.25 Exists fun X162 => % 8.01/8.25 Exists fun X163 => % 8.01/8.25 Exists fun X164 => % 8.01/8.25 And % 8.01/8.25 (And % 8.01/8.25 (And % 8.01/8.25 (And (And (And (occurrence_of X162 tptp3) (root_occ X162 a)) (occurrence_of X163 tptp4)) % 8.10/8.27 (next_subocc X162 X163 tptp0)) % 8.10/8.27 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 8.10/8.27 (next_subocc X163 X164 tptp0)) % 8.10/8.27 (leaf_occ X164 a)) % 8.10/8.27 True % 8.10/8.27 Clause #429 (by clausification #[428]): ∀ (a : Iota), % 8.10/8.27 Or (Eq (occurrence_of a tptp0) False) % 8.10/8.27 (Eq % 8.10/8.27 (Exists fun X162 => % 8.10/8.27 Exists fun X163 => % 8.10/8.27 Exists fun X164 => % 8.10/8.27 And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And (And (And (occurrence_of X162 tptp3) (root_occ X162 a)) (occurrence_of X163 tptp4)) % 8.10/8.27 (next_subocc X162 X163 tptp0)) % 8.10/8.27 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 8.10/8.27 (next_subocc X163 X164 tptp0)) % 8.10/8.27 (leaf_occ X164 a)) % 8.10/8.27 True) % 8.10/8.27 Clause #430 (by clausification #[429]): ∀ (a a_1 : Iota), % 8.10/8.27 Or (Eq (occurrence_of a tptp0) False) % 8.10/8.27 (Eq % 8.10/8.27 (Exists fun X163 => % 8.10/8.27 Exists fun X164 => % 8.10/8.27 And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And (And (occurrence_of (skS.0 15 a a_1) tptp3) (root_occ (skS.0 15 a a_1) a)) % 8.10/8.27 (occurrence_of X163 tptp4)) % 8.10/8.27 (next_subocc (skS.0 15 a a_1) X163 tptp0)) % 8.10/8.27 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 8.10/8.27 (next_subocc X163 X164 tptp0)) % 8.10/8.27 (leaf_occ X164 a)) % 8.10/8.27 True) % 8.10/8.27 Clause #431 (by clausification #[430]): ∀ (a a_1 a_2 : Iota), % 8.10/8.27 Or (Eq (occurrence_of a tptp0) False) % 8.10/8.27 (Eq % 8.10/8.27 (Exists fun X164 => % 8.10/8.27 And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And (And (occurrence_of (skS.0 15 a a_1) tptp3) (root_occ (skS.0 15 a a_1) a)) % 8.10/8.27 (occurrence_of (skS.0 16 a a_1 a_2) tptp4)) % 8.10/8.27 (next_subocc (skS.0 15 a a_1) (skS.0 16 a a_1 a_2) tptp0)) % 8.10/8.27 (Or (occurrence_of X164 tptp1) (occurrence_of X164 tptp2))) % 8.10/8.27 (next_subocc (skS.0 16 a a_1 a_2) X164 tptp0)) % 8.10/8.27 (leaf_occ X164 a)) % 8.10/8.27 True) % 8.10/8.27 Clause #432 (by clausification #[431]): ∀ (a a_1 a_2 a_3 : Iota), % 8.10/8.27 Or (Eq (occurrence_of a tptp0) False) % 8.10/8.27 (Eq % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And % 8.10/8.27 (And (And (occurrence_of (skS.0 15 a a_1) tptp3) (root_occ (skS.0 15 a a_1) a)) % 8.10/8.27 (occurrence_of (skS.0 16 a a_1 a_2) tptp4)) % 8.10/8.27 (next_subocc (skS.0 15 a a_1) (skS.0 16 a a_1 a_2) tptp0)) % 8.10/8.27 (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))) % 8.10/8.27 (next_subocc (skS.0 16 a a_1 a_2) (skS.0 17 a a_1 a_2 a_3) tptp0)) % 8.10/8.27 (leaf_occ (skS.0 17 a a_1 a_2 a_3) a)) % 8.10/8.27 True) % 8.10/8.27 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) % 8.10/8.27 Clause #442 (by clausification #[62]): Eq % 8.10/8.27 (∀ (X165 : Iota), % 8.10/8.27 occurrence_of X165 tptp0 → % 8.10/8.27 Exists fun X166 => % 8.10/8.27 Exists fun X167 => % 8.10/8.27 And % 8.10/8.27 (And (leaf_occ X167 X165) % 8.10/8.27 (occurrence_of X167 tptp1 → % 8.10/8.27 Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes X166 X168 tptp0)))) % 8.10/8.27 (occurrence_of X167 tptp2 → % 8.10/8.27 Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes X166 X169 tptp0)))) % 8.10/8.27 False % 8.10/8.27 Clause #443 (by clausification #[442]): ∀ (a : Iota), % 8.10/8.27 Eq % 8.10/8.27 (Not % 8.10/8.27 (occurrence_of (skS.0 19 a) tptp0 → % 8.10/8.27 Exists fun X166 => % 8.10/8.27 Exists fun X167 => % 8.10/8.27 And % 8.10/8.27 (And (leaf_occ X167 (skS.0 19 a)) % 8.10/8.27 (occurrence_of X167 tptp1 → % 8.10/8.27 Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes X166 X168 tptp0)))) % 8.10/8.27 (occurrence_of X167 tptp2 → % 8.10/8.27 Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes X166 X169 tptp0))))) % 8.10/8.27 True % 8.10/8.27 Clause #444 (by clausification #[443]): ∀ (a : Iota), % 8.10/8.27 Eq % 8.10/8.27 (occurrence_of (skS.0 19 a) tptp0 → % 8.10/8.27 Exists fun X166 => % 8.10/8.27 Exists fun X167 => % 8.10/8.27 And % 8.10/8.27 (And (leaf_occ X167 (skS.0 19 a)) % 8.13/8.29 (occurrence_of X167 tptp1 → % 8.13/8.29 Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes X166 X168 tptp0)))) % 8.13/8.29 (occurrence_of X167 tptp2 → % 8.13/8.29 Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes X166 X169 tptp0)))) % 8.13/8.29 False % 8.13/8.29 Clause #445 (by clausification #[444]): ∀ (a : Iota), Eq (occurrence_of (skS.0 19 a) tptp0) True % 8.13/8.29 Clause #446 (by clausification #[444]): ∀ (a : Iota), % 8.13/8.29 Eq % 8.13/8.29 (Exists fun X166 => % 8.13/8.29 Exists fun X167 => % 8.13/8.29 And % 8.13/8.29 (And (leaf_occ X167 (skS.0 19 a)) % 8.13/8.29 (occurrence_of X167 tptp1 → % 8.13/8.29 Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes X166 X168 tptp0)))) % 8.13/8.29 (occurrence_of X167 tptp2 → % 8.13/8.29 Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes X166 X169 tptp0)))) % 8.13/8.29 False % 8.13/8.29 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) % 8.13/8.29 Clause #453 (by superposition #[445, 314]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or (Eq True False) (Or (Eq (leaf_occ a (skS.0 19 a_1)) False) (Eq (min_precedes a a_2 tptp0) False)) % 8.13/8.29 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) % 8.13/8.29 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 % 8.13/8.29 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) % 8.13/8.29 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 % 8.13/8.29 Clause #577 (by clausification #[446]): ∀ (a a_1 : Iota), % 8.13/8.29 Eq % 8.13/8.29 (Exists fun X167 => % 8.13/8.29 And % 8.13/8.29 (And (leaf_occ X167 (skS.0 19 a)) % 8.13/8.29 (occurrence_of X167 tptp1 → % 8.13/8.29 Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_1 X168 tptp0)))) % 8.13/8.29 (occurrence_of X167 tptp2 → % 8.13/8.29 Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_1 X169 tptp0)))) % 8.13/8.29 False % 8.13/8.29 Clause #578 (by clausification #[577]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Eq % 8.13/8.29 (And % 8.13/8.29 (And (leaf_occ a (skS.0 19 a_1)) % 8.13/8.29 (occurrence_of a tptp1 → Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_2 X168 tptp0)))) % 8.13/8.29 (occurrence_of a tptp2 → Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_2 X169 tptp0)))) % 8.13/8.29 False % 8.13/8.29 Clause #579 (by clausification #[578]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or % 8.13/8.29 (Eq % 8.13/8.29 (And (leaf_occ a (skS.0 19 a_1)) % 8.13/8.29 (occurrence_of a tptp1 → Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_2 X168 tptp0)))) % 8.13/8.29 False) % 8.13/8.29 (Eq (occurrence_of a tptp2 → Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_2 X169 tptp0))) % 8.13/8.29 False) % 8.13/8.29 Clause #580 (by clausification #[579]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or % 8.13/8.29 (Eq (occurrence_of a tptp2 → Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_1 X169 tptp0))) % 8.13/8.29 False) % 8.13/8.29 (Or (Eq (leaf_occ a (skS.0 19 a_2)) False) % 8.13/8.29 (Eq % 8.13/8.29 (occurrence_of a tptp1 → Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_1 X168 tptp0))) % 8.13/8.29 False)) % 8.13/8.29 Clause #581 (by clausification #[580]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.29 (Or % 8.13/8.29 (Eq % 8.13/8.29 (occurrence_of a tptp1 → Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_2 X168 tptp0))) % 8.13/8.29 False) % 8.13/8.29 (Eq (occurrence_of a tptp2) True)) % 8.13/8.29 Clause #582 (by clausification #[580]): ∀ (a a_1 a_2 : Iota), % 8.13/8.29 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.29 (Or % 8.13/8.29 (Eq % 8.13/8.29 (occurrence_of a tptp1 → Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_2 X168 tptp0))) % 8.13/8.29 False) % 8.13/8.29 (Eq (Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_2 X169 tptp0))) False)) % 8.13/8.29 Clause #584 (by clausification #[581]): ∀ (a a_1 a_2 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp2) True) % 8.13/8.32 (Eq (Not (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_2 X168 tptp0))) False)) % 8.13/8.32 Clause #586 (by clausification #[584]): ∀ (a a_1 a_2 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp2) True) % 8.13/8.32 (Eq (Exists fun X168 => And (occurrence_of X168 tptp2) (min_precedes a_2 X168 tptp0)) True)) % 8.13/8.32 Clause #587 (by clausification #[586]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp2) True) % 8.13/8.32 (Eq (And (occurrence_of (skS.0 21 a_2 a_3) tptp2) (min_precedes a_2 (skS.0 21 a_2 a_3) tptp0)) True)) % 8.13/8.32 Clause #588 (by clausification #[587]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp2) True) (Eq (min_precedes a_2 (skS.0 21 a_2 a_3) tptp0) True)) % 8.13/8.32 Clause #590 (by superposition #[588, 528]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.32 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp2) True) % 8.13/8.32 (Or (Eq (min_precedes a_4 (skS.0 21 a_4 a_5) tptp0) True) (Eq False True)) % 8.13/8.32 Clause #743 (by clausification #[590]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.32 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp2) True) % 8.13/8.32 (Eq (min_precedes a_4 (skS.0 21 a_4 a_5) tptp0) True) % 8.13/8.32 Clause #756 (by superposition #[743, 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) % 8.13/8.32 Clause #777 (by clausification #[756]): ∀ (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 % 8.13/8.32 Clause #780 (by superposition #[777, 94]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 8.13/8.32 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)) % 8.13/8.32 Clause #789 (by clausification #[780]): ∀ (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) % 8.13/8.32 Clause #876 (by clausification #[582]): ∀ (a a_1 a_2 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (Not (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_2 X169 tptp0))) False) % 8.13/8.32 (Eq (occurrence_of a tptp1) True)) % 8.13/8.32 Clause #878 (by clausification #[876]): ∀ (a a_1 a_2 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp1) True) % 8.13/8.32 (Eq (Exists fun X169 => And (occurrence_of X169 tptp1) (min_precedes a_2 X169 tptp0)) True)) % 8.13/8.32 Clause #879 (by clausification #[878]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp1) True) % 8.13/8.32 (Eq (And (occurrence_of (skS.0 22 a_2 a_3) tptp1) (min_precedes a_2 (skS.0 22 a_2 a_3) tptp0)) True)) % 8.13/8.32 Clause #880 (by clausification #[879]): ∀ (a a_1 a_2 a_3 : Iota), % 8.13/8.32 Or (Eq (leaf_occ a (skS.0 19 a_1)) False) % 8.13/8.32 (Or (Eq (occurrence_of a tptp1) True) (Eq (min_precedes a_2 (skS.0 22 a_2 a_3) tptp0) True)) % 8.13/8.32 Clause #882 (by superposition #[880, 528]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.32 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp1) True) % 8.13/8.32 (Or (Eq (min_precedes a_4 (skS.0 22 a_4 a_5) tptp0) True) (Eq False True)) % 8.13/8.32 Clause #1044 (by clausification #[882]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 8.13/8.32 Or (Eq (occurrence_of (skS.0 17 (skS.0 19 a) a_1 a_2 a_3) tptp1) True) % 8.13/8.32 (Eq (min_precedes a_4 (skS.0 22 a_4 a_5) tptp0) True) % 8.13/8.32 Clause #1047 (by superposition #[1044, 789]): ∀ (a a_1 : Iota), Or (Eq (min_precedes a (skS.0 22 a a_1) tptp0) True) (Or (Eq True False) (Eq tptp2 tptp1)) % 8.13/8.32 Clause #1083 (by clausification #[1047]): ∀ (a a_1 : Iota), Or (Eq (min_precedes a (skS.0 22 a a_1) tptp0) True) (Eq tptp2 tptp1) % 8.13/8.32 Clause #1084 (by forward contextual literal cutting #[1083, 71]): ∀ (a a_1 : Iota), Eq (min_precedes a (skS.0 22 a a_1) tptp0) True % 8.13/8.32 Clause #1085 (by superposition #[1084, 536]): Eq True False % 8.13/8.32 Clause #1104 (by clausification #[1085]): False % 8.13/8.32 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------