%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PRO009+2 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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 82.14s 82.75s % Output : Proof 82.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO009+2 : TPTP v9.2.0. Released v4.0.0. % 0.11/0.13 % Command : duper %s % 0.13/0.35 % Computer : n021.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 08:42:38 EDT 2025 % 0.13/0.35 % CPUTime : % 82.14/82.75 SZS status Theorem for theBenchmark.p % 82.14/82.75 SZS output start Proof for theBenchmark.p % 82.14/82.75 Clause #0 (by assumption #[]): Eq (∀ (X0 X1 X2 X3 : Iota), And (min_precedes X0 X1 X3) (min_precedes X1 X2 X3) → min_precedes X0 X2 X3) True % 82.14/82.75 Clause #3 (by assumption #[]): Eq % 82.14/82.75 (∀ (X11 X12 X13 X14 : Iota), % 82.14/82.75 And (And (And (occurrence_of X13 X14) (Not (atomic X14))) (leaf_occ X11 X13)) (leaf_occ X12 X13) → Eq X11 X12) % 82.14/82.75 True % 82.14/82.75 Clause #4 (by assumption #[]): Eq % 82.14/82.75 (∀ (X15 X16 X17 : Iota), % 82.14/82.75 Iff (next_subocc X15 X16 X17) % 82.14/82.75 (And (min_precedes X15 X16 X17) % 82.14/82.75 (Not (Exists fun X18 => And (min_precedes X15 X18 X17) (min_precedes X18 X16 X17))))) % 82.14/82.75 True % 82.14/82.75 Clause #31 (by assumption #[]): Eq % 82.14/82.75 (∀ (X95 : Iota), % 82.14/82.75 occurrence_of X95 tptp0 → % 82.14/82.75 Exists fun X96 => % 82.14/82.75 Exists fun X97 => % 82.14/82.75 Exists fun X98 => % 82.14/82.75 And % 82.14/82.75 (And % 82.14/82.75 (And % 82.14/82.75 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 X95)) (occurrence_of X97 tptp4)) % 82.14/82.75 (next_subocc X96 X97 tptp0)) % 82.14/82.75 (Or (occurrence_of X98 tptp2) (occurrence_of X98 tptp1))) % 82.14/82.75 (next_subocc X97 X98 tptp0)) % 82.14/82.75 (leaf_occ X98 X95)) % 82.14/82.75 True % 82.14/82.75 Clause #33 (by assumption #[]): Eq (Not (atomic tptp0)) True % 82.14/82.75 Clause #44 (by assumption #[]): Eq % 82.14/82.75 (Not % 82.14/82.75 (∀ (X99 : Iota), % 82.14/82.75 occurrence_of X99 tptp0 → % 82.14/82.75 Exists fun X100 => % 82.14/82.75 Exists fun X101 => % 82.14/82.75 And % 82.14/82.75 (And % 82.14/82.75 (And (And (occurrence_of X100 tptp3) (root_occ X100 X99)) % 82.14/82.75 (Or (occurrence_of X101 tptp2) (occurrence_of X101 tptp1))) % 82.14/82.75 (min_precedes X100 X101 tptp0)) % 82.14/82.75 (leaf_occ X101 X99))) % 82.14/82.75 True % 82.14/82.75 Clause #45 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (X1 X2 X3 : Iota), And (min_precedes a X1 X3) (min_precedes X1 X2 X3) → min_precedes a X2 X3) True % 82.14/82.75 Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota), % 82.14/82.75 Eq (∀ (X2 X3 : Iota), And (min_precedes a a_1 X3) (min_precedes a_1 X2 X3) → min_precedes a X2 X3) True % 82.14/82.75 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 : Iota), % 82.14/82.75 Eq (∀ (X3 : Iota), And (min_precedes a a_1 X3) (min_precedes a_1 a_2 X3) → min_precedes a a_2 X3) True % 82.14/82.75 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (min_precedes a a_1 a_2) (min_precedes a_1 a_3 a_2) → min_precedes a a_3 a_2) True % 82.14/82.75 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.75 Or (Eq (And (min_precedes a a_1 a_2) (min_precedes a_1 a_3 a_2)) False) (Eq (min_precedes a a_3 a_2) True) % 82.14/82.75 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.75 Or (Eq (min_precedes a a_1 a_2) True) (Or (Eq (min_precedes a a_3 a_2) False) (Eq (min_precedes a_3 a_1 a_2) False)) % 82.14/82.75 Clause #51 (by clausification #[33]): Eq (atomic tptp0) False % 82.14/82.75 Clause #98 (by clausification #[3]): ∀ (a : Iota), % 82.14/82.75 Eq % 82.14/82.75 (∀ (X12 X13 X14 : Iota), % 82.14/82.75 And (And (And (occurrence_of X13 X14) (Not (atomic X14))) (leaf_occ a X13)) (leaf_occ X12 X13) → Eq a X12) % 82.14/82.75 True % 82.14/82.75 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), % 82.14/82.75 Eq % 82.14/82.75 (∀ (X13 X14 : Iota), % 82.14/82.75 And (And (And (occurrence_of X13 X14) (Not (atomic X14))) (leaf_occ a X13)) (leaf_occ a_1 X13) → Eq a a_1) % 82.14/82.75 True % 82.14/82.75 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), % 82.14/82.75 Eq % 82.14/82.75 (∀ (X14 : Iota), % 82.14/82.75 And (And (And (occurrence_of a X14) (Not (atomic X14))) (leaf_occ a_1 a)) (leaf_occ a_2 a) → Eq a_1 a_2) % 82.14/82.75 True % 82.14/82.75 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.75 Eq (And (And (And (occurrence_of a a_1) (Not (atomic a_1))) (leaf_occ a_2 a)) (leaf_occ a_3 a) → Eq a_2 a_3) True % 82.14/82.75 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.75 Or (Eq (And (And (And (occurrence_of a a_1) (Not (atomic a_1))) (leaf_occ a_2 a)) (leaf_occ a_3 a)) False) % 82.14/82.75 (Eq (Eq a_2 a_3) True) % 82.14/82.75 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.75 Or (Eq (Eq a a_1) True) % 82.14/82.75 (Or (Eq (And (And (occurrence_of a_2 a_3) (Not (atomic a_3))) (leaf_occ a a_2)) False) % 82.14/82.75 (Eq (leaf_occ a_1 a_2) False)) % 82.14/82.75 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.75 Or (Eq (And (And (occurrence_of a a_1) (Not (atomic a_1))) (leaf_occ a_2 a)) False) % 82.14/82.77 (Or (Eq (leaf_occ a_3 a) False) (Eq a_2 a_3)) % 82.14/82.77 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.77 Or (Eq (leaf_occ a a_1) False) % 82.14/82.77 (Or (Eq a_2 a) (Or (Eq (And (occurrence_of a_1 a_3) (Not (atomic a_3))) False) (Eq (leaf_occ a_2 a_1) False))) % 82.14/82.77 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.77 Or (Eq (leaf_occ a a_1) False) % 82.14/82.77 (Or (Eq a_2 a) % 82.14/82.77 (Or (Eq (leaf_occ a_2 a_1) False) (Or (Eq (occurrence_of a_1 a_3) False) (Eq (Not (atomic a_3)) False)))) % 82.14/82.77 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 a_3 : Iota), % 82.14/82.77 Or (Eq (leaf_occ a a_1) False) % 82.14/82.77 (Or (Eq a_2 a) (Or (Eq (leaf_occ a_2 a_1) False) (Or (Eq (occurrence_of a_1 a_3) False) (Eq (atomic a_3) True)))) % 82.14/82.77 Clause #123 (by clausification #[4]): ∀ (a : Iota), % 82.14/82.77 Eq % 82.14/82.77 (∀ (X16 X17 : Iota), % 82.14/82.77 Iff (next_subocc a X16 X17) % 82.14/82.77 (And (min_precedes a X16 X17) % 82.14/82.77 (Not (Exists fun X18 => And (min_precedes a X18 X17) (min_precedes X18 X16 X17))))) % 82.14/82.77 True % 82.14/82.77 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 82.14/82.77 Eq % 82.14/82.77 (∀ (X17 : Iota), % 82.14/82.77 Iff (next_subocc a a_1 X17) % 82.14/82.77 (And (min_precedes a a_1 X17) % 82.14/82.77 (Not (Exists fun X18 => And (min_precedes a X18 X17) (min_precedes X18 a_1 X17))))) % 82.14/82.77 True % 82.14/82.77 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 82.14/82.77 Eq % 82.14/82.77 (Iff (next_subocc a a_1 a_2) % 82.14/82.77 (And (min_precedes a a_1 a_2) (Not (Exists fun X18 => And (min_precedes a X18 a_2) (min_precedes X18 a_1 a_2))))) % 82.14/82.77 True % 82.14/82.77 Clause #127 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 82.14/82.77 Or (Eq (next_subocc a a_1 a_2) False) % 82.14/82.77 (Eq (And (min_precedes a a_1 a_2) (Not (Exists fun X18 => And (min_precedes a X18 a_2) (min_precedes X18 a_1 a_2)))) % 82.14/82.77 True) % 82.14/82.77 Clause #266 (by clausification #[127]): ∀ (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) % 82.14/82.77 Clause #274 (by clausification #[31]): ∀ (a : Iota), % 82.14/82.77 Eq % 82.14/82.77 (occurrence_of a tptp0 → % 82.14/82.77 Exists fun X96 => % 82.14/82.77 Exists fun X97 => % 82.14/82.77 Exists fun X98 => % 82.14/82.77 And % 82.14/82.77 (And % 82.14/82.77 (And % 82.14/82.77 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 a)) (occurrence_of X97 tptp4)) % 82.14/82.77 (next_subocc X96 X97 tptp0)) % 82.14/82.77 (Or (occurrence_of X98 tptp2) (occurrence_of X98 tptp1))) % 82.14/82.77 (next_subocc X97 X98 tptp0)) % 82.14/82.77 (leaf_occ X98 a)) % 82.14/82.77 True % 82.14/82.77 Clause #275 (by clausification #[274]): ∀ (a : Iota), % 82.14/82.77 Or (Eq (occurrence_of a tptp0) False) % 82.14/82.77 (Eq % 82.14/82.77 (Exists fun X96 => % 82.14/82.77 Exists fun X97 => % 82.14/82.77 Exists fun X98 => % 82.14/82.77 And % 82.14/82.77 (And % 82.14/82.77 (And % 82.14/82.77 (And (And (And (occurrence_of X96 tptp3) (root_occ X96 a)) (occurrence_of X97 tptp4)) % 82.14/82.77 (next_subocc X96 X97 tptp0)) % 82.14/82.77 (Or (occurrence_of X98 tptp2) (occurrence_of X98 tptp1))) % 82.14/82.77 (next_subocc X97 X98 tptp0)) % 82.14/82.77 (leaf_occ X98 a)) % 82.14/82.77 True) % 82.14/82.77 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), % 82.14/82.77 Or (Eq (occurrence_of a tptp0) False) % 82.14/82.77 (Eq % 82.14/82.77 (Exists fun X97 => % 82.14/82.77 Exists fun X98 => % 82.14/82.77 And % 82.14/82.77 (And % 82.14/82.77 (And % 82.14/82.77 (And % 82.14/82.77 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.14/82.77 (occurrence_of X97 tptp4)) % 82.14/82.77 (next_subocc (skS.0 13 a a_1) X97 tptp0)) % 82.14/82.77 (Or (occurrence_of X98 tptp2) (occurrence_of X98 tptp1))) % 82.14/82.77 (next_subocc X97 X98 tptp0)) % 82.14/82.77 (leaf_occ X98 a)) % 82.14/82.77 True) % 82.14/82.77 Clause #277 (by clausification #[276]): ∀ (a a_1 a_2 : Iota), % 82.14/82.77 Or (Eq (occurrence_of a tptp0) False) % 82.14/82.77 (Eq % 82.14/82.77 (Exists fun X98 => % 82.14/82.77 And % 82.14/82.77 (And % 82.14/82.77 (And % 82.14/82.77 (And % 82.14/82.77 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.14/82.77 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 82.14/82.77 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 82.14/82.77 (Or (occurrence_of X98 tptp2) (occurrence_of X98 tptp1))) % 82.21/82.79 (next_subocc (skS.0 14 a a_1 a_2) X98 tptp0)) % 82.21/82.79 (leaf_occ X98 a)) % 82.21/82.79 True) % 82.21/82.79 Clause #278 (by clausification #[277]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.79 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.79 (Eq % 82.21/82.79 (And % 82.21/82.79 (And % 82.21/82.79 (And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.21/82.79 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 82.21/82.79 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 82.21/82.79 (Or (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp1))) % 82.21/82.79 (next_subocc (skS.0 14 a a_1 a_2) (skS.0 15 a a_1 a_2 a_3) tptp0)) % 82.21/82.79 (leaf_occ (skS.0 15 a a_1 a_2 a_3) a)) % 82.21/82.79 True) % 82.21/82.79 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) % 82.21/82.79 Clause #280 (by clausification #[278]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.79 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.79 (Eq % 82.21/82.79 (And % 82.21/82.79 (And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.21/82.79 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 82.21/82.79 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 82.21/82.79 (Or (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp1))) % 82.21/82.79 (next_subocc (skS.0 14 a a_1 a_2) (skS.0 15 a a_1 a_2 a_3) tptp0)) % 82.21/82.79 True) % 82.21/82.79 Clause #285 (by clausification #[44]): Eq % 82.21/82.79 (∀ (X99 : Iota), % 82.21/82.79 occurrence_of X99 tptp0 → % 82.21/82.79 Exists fun X100 => % 82.21/82.79 Exists fun X101 => % 82.21/82.79 And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of X100 tptp3) (root_occ X100 X99)) % 82.21/82.79 (Or (occurrence_of X101 tptp2) (occurrence_of X101 tptp1))) % 82.21/82.79 (min_precedes X100 X101 tptp0)) % 82.21/82.79 (leaf_occ X101 X99)) % 82.21/82.79 False % 82.21/82.79 Clause #286 (by clausification #[285]): ∀ (a : Iota), % 82.21/82.79 Eq % 82.21/82.79 (Not % 82.21/82.79 (occurrence_of (skS.0 17 a) tptp0 → % 82.21/82.79 Exists fun X100 => % 82.21/82.79 Exists fun X101 => % 82.21/82.79 And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of X100 tptp3) (root_occ X100 (skS.0 17 a))) % 82.21/82.79 (Or (occurrence_of X101 tptp2) (occurrence_of X101 tptp1))) % 82.21/82.79 (min_precedes X100 X101 tptp0)) % 82.21/82.79 (leaf_occ X101 (skS.0 17 a)))) % 82.21/82.79 True % 82.21/82.79 Clause #287 (by clausification #[286]): ∀ (a : Iota), % 82.21/82.79 Eq % 82.21/82.79 (occurrence_of (skS.0 17 a) tptp0 → % 82.21/82.79 Exists fun X100 => % 82.21/82.79 Exists fun X101 => % 82.21/82.79 And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of X100 tptp3) (root_occ X100 (skS.0 17 a))) % 82.21/82.79 (Or (occurrence_of X101 tptp2) (occurrence_of X101 tptp1))) % 82.21/82.79 (min_precedes X100 X101 tptp0)) % 82.21/82.79 (leaf_occ X101 (skS.0 17 a))) % 82.21/82.79 False % 82.21/82.79 Clause #288 (by clausification #[287]): ∀ (a : Iota), Eq (occurrence_of (skS.0 17 a) tptp0) True % 82.21/82.79 Clause #289 (by clausification #[287]): ∀ (a : Iota), % 82.21/82.79 Eq % 82.21/82.79 (Exists fun X100 => % 82.21/82.79 Exists fun X101 => % 82.21/82.79 And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of X100 tptp3) (root_occ X100 (skS.0 17 a))) % 82.21/82.79 (Or (occurrence_of X101 tptp2) (occurrence_of X101 tptp1))) % 82.21/82.79 (min_precedes X100 X101 tptp0)) % 82.21/82.79 (leaf_occ X101 (skS.0 17 a))) % 82.21/82.79 False % 82.21/82.79 Clause #290 (by superposition #[288, 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) % 82.21/82.79 Clause #322 (by clausification #[280]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.79 Or (Eq (occurrence_of a tptp0) False) (Eq (next_subocc (skS.0 14 a a_1 a_2) (skS.0 15 a a_1 a_2 a_3) tptp0) True) % 82.21/82.79 Clause #323 (by clausification #[280]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.79 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.79 (Eq % 82.21/82.79 (And % 82.21/82.79 (And % 82.21/82.79 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.21/82.79 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 82.21/82.79 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 82.21/82.79 (Or (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp1))) % 82.21/82.82 True) % 82.21/82.82 Clause #324 (by superposition #[322, 288]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.82 Or (Eq (next_subocc (skS.0 14 (skS.0 17 a) a_1 a_2) (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp0) True) (Eq False True) % 82.21/82.82 Clause #346 (by clausification #[289]): ∀ (a a_1 : Iota), % 82.21/82.82 Eq % 82.21/82.82 (Exists fun X101 => % 82.21/82.82 And % 82.21/82.82 (And % 82.21/82.82 (And (And (occurrence_of a tptp3) (root_occ a (skS.0 17 a_1))) % 82.21/82.82 (Or (occurrence_of X101 tptp2) (occurrence_of X101 tptp1))) % 82.21/82.82 (min_precedes a X101 tptp0)) % 82.21/82.82 (leaf_occ X101 (skS.0 17 a_1))) % 82.21/82.82 False % 82.21/82.82 Clause #347 (by clausification #[346]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Eq % 82.21/82.82 (And % 82.21/82.82 (And % 82.21/82.82 (And (And (occurrence_of a tptp3) (root_occ a (skS.0 17 a_1))) % 82.21/82.82 (Or (occurrence_of a_2 tptp2) (occurrence_of a_2 tptp1))) % 82.21/82.82 (min_precedes a a_2 tptp0)) % 82.21/82.82 (leaf_occ a_2 (skS.0 17 a_1))) % 82.21/82.82 False % 82.21/82.82 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Or % 82.21/82.82 (Eq % 82.21/82.82 (And % 82.21/82.82 (And (And (occurrence_of a tptp3) (root_occ a (skS.0 17 a_1))) % 82.21/82.82 (Or (occurrence_of a_2 tptp2) (occurrence_of a_2 tptp1))) % 82.21/82.82 (min_precedes a a_2 tptp0)) % 82.21/82.82 False) % 82.21/82.82 (Eq (leaf_occ a_2 (skS.0 17 a_1)) False) % 82.21/82.82 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Or % 82.21/82.82 (Eq % 82.21/82.82 (And (And (occurrence_of a_2 tptp3) (root_occ a_2 (skS.0 17 a_1))) % 82.21/82.82 (Or (occurrence_of a tptp2) (occurrence_of a tptp1))) % 82.21/82.82 False) % 82.21/82.82 (Eq (min_precedes a_2 a tptp0) False)) % 82.21/82.82 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Or (Eq (min_precedes a_2 a tptp0) False) % 82.21/82.82 (Or (Eq (And (occurrence_of a_2 tptp3) (root_occ a_2 (skS.0 17 a_1))) False) % 82.21/82.82 (Eq (Or (occurrence_of a tptp2) (occurrence_of a tptp1)) False))) % 82.21/82.82 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Or (Eq (min_precedes a_2 a tptp0) False) % 82.21/82.82 (Or (Eq (Or (occurrence_of a tptp2) (occurrence_of a tptp1)) False) % 82.21/82.82 (Or (Eq (occurrence_of a_2 tptp3) False) (Eq (root_occ a_2 (skS.0 17 a_1)) False)))) % 82.21/82.82 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Or (Eq (min_precedes a_2 a tptp0) False) % 82.21/82.82 (Or (Eq (occurrence_of a_2 tptp3) False) % 82.21/82.82 (Or (Eq (root_occ a_2 (skS.0 17 a_1)) False) (Eq (occurrence_of a tptp1) False)))) % 82.21/82.82 Clause #353 (by clausification #[351]): ∀ (a a_1 a_2 : Iota), % 82.21/82.82 Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Or (Eq (min_precedes a_2 a tptp0) False) % 82.21/82.82 (Or (Eq (occurrence_of a_2 tptp3) False) % 82.21/82.82 (Or (Eq (root_occ a_2 (skS.0 17 a_1)) False) (Eq (occurrence_of a tptp2) False)))) % 82.21/82.82 Clause #361 (by clausification #[290]): ∀ (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 % 82.21/82.82 Clause #363 (by superposition #[361, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.82 Or (Eq True False) % 82.21/82.82 (Or (Eq (min_precedes a (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp0) False) % 82.21/82.82 (Or (Eq (occurrence_of a tptp3) False) % 82.21/82.82 (Or (Eq (root_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Eq (occurrence_of (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp1) False)))) % 82.21/82.82 Clause #364 (by superposition #[361, 107]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 82.21/82.82 Or (Eq True False) % 82.21/82.82 (Or (Eq a (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4)) % 82.21/82.82 (Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Or (Eq (occurrence_of (skS.0 17 a_1) a_5) False) (Eq (atomic a_5) True)))) % 82.21/82.82 Clause #394 (by superposition #[353, 361]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.82 Or (Eq True False) % 82.21/82.82 (Or (Eq (min_precedes a (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp0) False) % 82.21/82.82 (Or (Eq (occurrence_of a tptp3) False) % 82.21/82.82 (Or (Eq (root_occ a (skS.0 17 a_1)) False) % 82.21/82.82 (Eq (occurrence_of (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp2) False)))) % 82.21/82.82 Clause #395 (by clausification #[324]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.82 Eq (next_subocc (skS.0 14 (skS.0 17 a) a_1 a_2) (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp0) True % 82.21/82.82 Clause #399 (by superposition #[395, 266]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.84 Or (Eq True False) (Eq (min_precedes (skS.0 14 (skS.0 17 a) a_1 a_2) (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp0) True) % 82.21/82.84 Clause #402 (by clausification #[399]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.84 Eq (min_precedes (skS.0 14 (skS.0 17 a) a_1 a_2) (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp0) True % 82.21/82.84 Clause #416 (by clausification #[323]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.84 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.84 (Eq (Or (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp2) (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp1)) True) % 82.21/82.84 Clause #417 (by clausification #[323]): ∀ (a a_1 a_2 : Iota), % 82.21/82.84 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.84 (Eq % 82.21/82.84 (And % 82.21/82.84 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.21/82.84 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 82.21/82.84 (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0)) % 82.21/82.84 True) % 82.21/82.84 Clause #418 (by clausification #[416]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.84 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.84 (Or (Eq (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp2) True) % 82.21/82.84 (Eq (occurrence_of (skS.0 15 a a_1 a_2 a_3) tptp1) True)) % 82.21/82.84 Clause #419 (by superposition #[418, 288]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.84 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) % 82.21/82.84 (Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) True) (Eq False True)) % 82.21/82.84 Clause #460 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 82.21/82.84 Or (Eq a (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4)) % 82.21/82.84 (Or (Eq (leaf_occ a (skS.0 17 a_1)) False) % 82.21/82.84 (Or (Eq (occurrence_of (skS.0 17 a_1) a_5) False) (Eq (atomic a_5) True))) % 82.21/82.84 Clause #461 (by superposition #[460, 361]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 82.21/82.84 Or (Eq (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 15 (skS.0 17 a) a_4 a_5 a_6)) % 82.21/82.84 (Or (Eq (occurrence_of (skS.0 17 a) a_7) False) (Or (Eq (atomic a_7) True) (Eq False True))) % 82.21/82.84 Clause #464 (by clausification #[419]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.84 Or (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp2) True) % 82.21/82.84 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) True) % 82.21/82.84 Clause #536 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.84 Or (Eq (min_precedes a (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp0) False) % 82.21/82.84 (Or (Eq (occurrence_of a tptp3) False) % 82.21/82.84 (Or (Eq (root_occ a (skS.0 17 a_1)) False) % 82.21/82.84 (Eq (occurrence_of (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp1) False))) % 82.21/82.84 Clause #644 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.84 Or (Eq (min_precedes a (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp0) False) % 82.21/82.84 (Or (Eq (occurrence_of a tptp3) False) % 82.21/82.84 (Or (Eq (root_occ a (skS.0 17 a_1)) False) % 82.21/82.84 (Eq (occurrence_of (skS.0 15 (skS.0 17 a_1) a_2 a_3 a_4) tptp2) False))) % 82.21/82.84 Clause #792 (by clausification #[461]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 82.21/82.84 Or (Eq (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 15 (skS.0 17 a) a_4 a_5 a_6)) % 82.21/82.84 (Or (Eq (occurrence_of (skS.0 17 a) a_7) False) (Eq (atomic a_7) True)) % 82.21/82.84 Clause #793 (by superposition #[792, 288]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 82.21/82.84 Or (Eq (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 15 (skS.0 17 a) a_4 a_5 a_6)) % 82.21/82.84 (Or (Eq (atomic tptp0) True) (Eq False True)) % 82.21/82.84 Clause #794 (by clausification #[793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 82.21/82.84 Or (Eq (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 15 (skS.0 17 a) a_4 a_5 a_6)) (Eq (atomic tptp0) True) % 82.21/82.84 Clause #795 (by forward demodulation #[794, 51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 82.21/82.84 Or (Eq (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 15 (skS.0 17 a) a_4 a_5 a_6)) (Eq False True) % 82.21/82.84 Clause #796 (by clausification #[795]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) (skS.0 15 (skS.0 17 a) a_4 a_5 a_6) % 82.21/82.84 Clause #798 (by superposition #[796, 402]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 82.21/82.84 Eq (min_precedes (skS.0 14 (skS.0 17 a) a_1 a_2) (skS.0 15 (skS.0 17 a) a_3 a_4 a_5) tptp0) True % 82.21/82.84 Clause #815 (by clausification #[417]): ∀ (a a_1 a_2 : Iota), % 82.21/82.84 Or (Eq (occurrence_of a tptp0) False) (Eq (next_subocc (skS.0 13 a a_1) (skS.0 14 a a_1 a_2) tptp0) True) % 82.21/82.84 Clause #816 (by clausification #[417]): ∀ (a a_1 a_2 : Iota), % 82.21/82.87 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.87 (Eq % 82.21/82.87 (And (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) % 82.21/82.87 (occurrence_of (skS.0 14 a a_1 a_2) tptp4)) % 82.21/82.87 True) % 82.21/82.87 Clause #817 (by superposition #[815, 288]): ∀ (a a_1 a_2 : Iota), % 82.21/82.87 Or (Eq (next_subocc (skS.0 13 (skS.0 17 a) a_1) (skS.0 14 (skS.0 17 a) a_1 a_2) tptp0) True) (Eq False True) % 82.21/82.87 Clause #820 (by clausification #[817]): ∀ (a a_1 a_2 : Iota), Eq (next_subocc (skS.0 13 (skS.0 17 a) a_1) (skS.0 14 (skS.0 17 a) a_1 a_2) tptp0) True % 82.21/82.87 Clause #823 (by superposition #[820, 266]): ∀ (a a_1 a_2 : Iota), % 82.21/82.87 Or (Eq True False) (Eq (min_precedes (skS.0 13 (skS.0 17 a) a_1) (skS.0 14 (skS.0 17 a) a_1 a_2) tptp0) True) % 82.21/82.87 Clause #825 (by clausification #[823]): ∀ (a a_1 a_2 : Iota), Eq (min_precedes (skS.0 13 (skS.0 17 a) a_1) (skS.0 14 (skS.0 17 a) a_1 a_2) tptp0) True % 82.21/82.87 Clause #826 (by superposition #[825, 50]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.87 Or (Eq (min_precedes (skS.0 13 (skS.0 17 a) a_1) a_2 tptp0) True) % 82.21/82.87 (Or (Eq True False) (Eq (min_precedes (skS.0 14 (skS.0 17 a) a_1 a_3) a_2 tptp0) False)) % 82.21/82.87 Clause #899 (by clausification #[826]): ∀ (a a_1 a_2 a_3 : Iota), % 82.21/82.87 Or (Eq (min_precedes (skS.0 13 (skS.0 17 a) a_1) a_2 tptp0) True) % 82.21/82.87 (Eq (min_precedes (skS.0 14 (skS.0 17 a) a_1 a_3) a_2 tptp0) False) % 82.21/82.87 Clause #900 (by superposition #[899, 798]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Or (Eq (min_precedes (skS.0 13 (skS.0 17 a) a_1) (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp0) True) (Eq False True) % 82.21/82.87 Clause #901 (by clausification #[900]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Eq (min_precedes (skS.0 13 (skS.0 17 a) a_1) (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp0) True % 82.21/82.87 Clause #902 (by superposition #[901, 536]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Or (Eq True False) % 82.21/82.87 (Or (Eq (occurrence_of (skS.0 13 (skS.0 17 a) a_1) tptp3) False) % 82.21/82.87 (Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.21/82.87 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp1) False))) % 82.21/82.87 Clause #903 (by superposition #[901, 644]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Or (Eq True False) % 82.21/82.87 (Or (Eq (occurrence_of (skS.0 13 (skS.0 17 a) a_1) tptp3) False) % 82.21/82.87 (Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.21/82.87 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp2) False))) % 82.21/82.87 Clause #925 (by clausification #[816]): ∀ (a a_1 : Iota), % 82.21/82.87 Or (Eq (occurrence_of a tptp0) False) % 82.21/82.87 (Eq (And (occurrence_of (skS.0 13 a a_1) tptp3) (root_occ (skS.0 13 a a_1) a)) True) % 82.21/82.87 Clause #969 (by clausification #[925]): ∀ (a a_1 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (root_occ (skS.0 13 a a_1) a) True) % 82.21/82.87 Clause #970 (by clausification #[925]): ∀ (a a_1 : Iota), Or (Eq (occurrence_of a tptp0) False) (Eq (occurrence_of (skS.0 13 a a_1) tptp3) True) % 82.21/82.87 Clause #971 (by superposition #[969, 288]): ∀ (a a_1 : Iota), Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) True) (Eq False True) % 82.21/82.87 Clause #974 (by superposition #[970, 288]): ∀ (a a_1 : Iota), Or (Eq (occurrence_of (skS.0 13 (skS.0 17 a) a_1) tptp3) True) (Eq False True) % 82.21/82.87 Clause #977 (by clausification #[974]): ∀ (a a_1 : Iota), Eq (occurrence_of (skS.0 13 (skS.0 17 a) a_1) tptp3) True % 82.21/82.87 Clause #1015 (by clausification #[971]): ∀ (a a_1 : Iota), Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) True % 82.21/82.87 Clause #2708 (by clausification #[902]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Or (Eq (occurrence_of (skS.0 13 (skS.0 17 a) a_1) tptp3) False) % 82.21/82.87 (Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.21/82.87 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp1) False)) % 82.21/82.87 Clause #2709 (by forward demodulation #[2708, 977]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Or (Eq True False) % 82.21/82.87 (Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.21/82.87 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp1) False)) % 82.21/82.87 Clause #2710 (by clausification #[2709]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.21/82.87 Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.21/82.87 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp1) False) % 82.21/82.87 Clause #2711 (by superposition #[2710, 1015]): ∀ (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) tptp1) False) (Eq False True) % 82.32/82.90 Clause #2712 (by clausification #[2711]): ∀ (a a_1 a_2 a_3 : Iota), Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_1 a_2 a_3) tptp1) False % 82.32/82.90 Clause #2713 (by backward demodulation #[2712, 464]): ∀ (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 False True) % 82.32/82.90 Clause #2760 (by clausification #[903]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.32/82.90 Or (Eq (occurrence_of (skS.0 13 (skS.0 17 a) a_1) tptp3) False) % 82.32/82.90 (Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.32/82.90 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp2) False)) % 82.32/82.90 Clause #2761 (by forward demodulation #[2760, 977]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.32/82.90 Or (Eq True False) % 82.32/82.90 (Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.32/82.90 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp2) False)) % 82.32/82.90 Clause #2762 (by clausification #[2761]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 82.32/82.90 Or (Eq (root_occ (skS.0 13 (skS.0 17 a) a_1) (skS.0 17 a)) False) % 82.32/82.90 (Eq (occurrence_of (skS.0 15 (skS.0 17 a) a_2 a_3 a_4) tptp2) False) % 82.32/82.90 Clause #2763 (by superposition #[2762, 1015]): ∀ (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) False) (Eq False True) % 82.32/82.90 Clause #2769 (by clausification #[2713]): ∀ (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 % 82.32/82.90 Clause #2795 (by clausification #[2763]): ∀ (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) False % 82.32/82.90 Clause #2796 (by superposition #[2795, 2769]): Eq False True % 82.32/82.90 Clause #2797 (by clausification #[2796]): False % 82.32/82.90 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------