%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO578+1 : TPTP v9.2.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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 08:09:18 PM UTC 2025 % Result : Theorem 29.89s 30.07s % Output : Proof 29.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYO578+1 : TPTP v9.2.0. Released v5.5.0. % 0.10/0.13 % Command : duper %s % 0.14/0.34 % Computer : n008.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 14:28:08 EDT 2025 % 0.14/0.34 % CPUTime : % 29.89/30.07 SZS status Theorem for theBenchmark.p % 29.89/30.07 SZS output start Proof for theBenchmark.p % 29.89/30.07 Clause #1 (by assumption #[]): Eq (∀ (X1 : Iota), k04_buttercup10622 X1 → k04_buttercup10619 X1) True % 29.89/30.07 Clause #3 (by assumption #[]): Eq (∀ (X3 : Iota), b48_buttercup10104 X3 → b48_buttercup10098 X3) True % 29.89/30.07 Clause #12 (by assumption #[]): Eq % 29.89/30.07 (And (∀ (X27 : Iota), k04_buttercup10619 X27 → b48_buttercup10098 X27) % 29.89/30.07 (Exists fun X28 => And (b48_buttercup10098 X28) (Not (k04_buttercup10619 X28)))) % 29.89/30.07 True % 29.89/30.07 Clause #17 (by assumption #[]): Eq % 29.89/30.07 (And (∀ (X55 : Iota), b48_buttercup10104 X55 → k04_buttercup10622 X55) % 29.89/30.07 (Exists fun X56 => And (k04_buttercup10622 X56) (Not (b48_buttercup10104 X56)))) % 29.89/30.07 True % 29.89/30.07 Clause #19 (by assumption #[]): Eq % 29.89/30.07 (And (∀ (X59 : Iota), b48_buttercup10108 X59 → k04_buttercup10622 X59) % 29.89/30.07 (Exists fun X60 => And (k04_buttercup10622 X60) (Not (b48_buttercup10108 X60)))) % 29.89/30.07 True % 29.89/30.07 Clause #20 (by assumption #[]): Eq % 29.89/30.07 (And (∀ (X61 : Iota), k04_buttercup10100 X61 → b48_buttercup10098 X61) % 29.89/30.07 (Exists fun X62 => And (b48_buttercup10098 X62) (Not (k04_buttercup10100 X62)))) % 29.89/30.07 True % 29.89/30.07 Clause #33 (by assumption #[]): Eq (Exists fun X90 => b48_buttercup10104 X90) True % 29.89/30.07 Clause #37 (by assumption #[]): Eq (∀ (X94 : Iota), k04_buttercup10100 X94 → Not (k04_buttercup10619 X94)) True % 29.89/30.07 Clause #85 (by assumption #[]): Eq % 29.89/30.07 (Not % 29.89/30.07 (Or % 29.89/30.07 (Or % 29.89/30.07 (Or % 29.89/30.07 (And (∀ (X142 : Iota), b48_buttercup10098 X142 → k04_buttercup10100 X142) % 29.89/30.07 (Exists fun X143 => And (k04_buttercup10100 X143) (Not (b48_buttercup10098 X143)))) % 29.89/30.07 (And (∀ (X144 : Iota), k04_buttercup10100 X144 → b48_buttercup10098 X144) % 29.89/30.07 (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145))))) % 29.89/30.07 (Exists fun X146 => % 29.89/30.07 Exists fun X147 => % 29.89/30.07 Exists fun X148 => % 29.89/30.07 And % 29.89/30.07 (And % 29.89/30.07 (And (And (And (k04_buttercup10100 X146) (b48_buttercup10098 X146)) (k04_buttercup10100 X147)) % 29.89/30.07 (Not (b48_buttercup10098 X147))) % 29.89/30.07 (Not (k04_buttercup10100 X148))) % 29.89/30.07 (b48_buttercup10098 X148))) % 29.89/30.07 (∀ (X149 : Iota), k04_buttercup10100 X149 → Not (b48_buttercup10098 X149)))) % 29.89/30.07 True % 29.89/30.07 Clause #98 (by clausification #[3]): ∀ (a : Iota), Eq (b48_buttercup10104 a → b48_buttercup10098 a) True % 29.89/30.07 Clause #99 (by clausification #[98]): ∀ (a : Iota), Or (Eq (b48_buttercup10104 a) False) (Eq (b48_buttercup10098 a) True) % 29.89/30.07 Clause #100 (by clausification #[1]): ∀ (a : Iota), Eq (k04_buttercup10622 a → k04_buttercup10619 a) True % 29.89/30.07 Clause #101 (by clausification #[100]): ∀ (a : Iota), Or (Eq (k04_buttercup10622 a) False) (Eq (k04_buttercup10619 a) True) % 29.89/30.07 Clause #209 (by clausification #[12]): Eq (∀ (X27 : Iota), k04_buttercup10619 X27 → b48_buttercup10098 X27) True % 29.89/30.07 Clause #214 (by clausification #[209]): ∀ (a : Iota), Eq (k04_buttercup10619 a → b48_buttercup10098 a) True % 29.89/30.07 Clause #215 (by clausification #[214]): ∀ (a : Iota), Or (Eq (k04_buttercup10619 a) False) (Eq (b48_buttercup10098 a) True) % 29.89/30.07 Clause #257 (by clausification #[37]): ∀ (a : Iota), Eq (k04_buttercup10100 a → Not (k04_buttercup10619 a)) True % 29.89/30.07 Clause #258 (by clausification #[257]): ∀ (a : Iota), Or (Eq (k04_buttercup10100 a) False) (Eq (Not (k04_buttercup10619 a)) True) % 29.89/30.07 Clause #259 (by clausification #[258]): ∀ (a : Iota), Or (Eq (k04_buttercup10100 a) False) (Eq (k04_buttercup10619 a) False) % 29.89/30.07 Clause #330 (by betaEtaReduce #[33]): Eq (Exists b48_buttercup10104) True % 29.89/30.07 Clause #331 (by clausification #[330]): ∀ (a : Iota), Eq (b48_buttercup10104 (skS.0 33 a)) True % 29.89/30.07 Clause #332 (by superposition #[331, 99]): ∀ (a : Iota), Or (Eq True False) (Eq (b48_buttercup10098 (skS.0 33 a)) True) % 29.89/30.07 Clause #386 (by clausification #[17]): Eq (∀ (X55 : Iota), b48_buttercup10104 X55 → k04_buttercup10622 X55) True % 29.89/30.07 Clause #391 (by clausification #[386]): ∀ (a : Iota), Eq (b48_buttercup10104 a → k04_buttercup10622 a) True % 29.89/30.07 Clause #392 (by clausification #[391]): ∀ (a : Iota), Or (Eq (b48_buttercup10104 a) False) (Eq (k04_buttercup10622 a) True) % 29.89/30.07 Clause #393 (by superposition #[392, 331]): ∀ (a : Iota), Or (Eq (k04_buttercup10622 (skS.0 33 a)) True) (Eq False True) % 29.89/30.09 Clause #429 (by clausification #[19]): Eq (Exists fun X60 => And (k04_buttercup10622 X60) (Not (b48_buttercup10108 X60))) True % 29.89/30.09 Clause #431 (by clausification #[429]): ∀ (a : Iota), Eq (And (k04_buttercup10622 (skS.0 42 a)) (Not (b48_buttercup10108 (skS.0 42 a)))) True % 29.89/30.09 Clause #433 (by clausification #[431]): ∀ (a : Iota), Eq (k04_buttercup10622 (skS.0 42 a)) True % 29.89/30.09 Clause #451 (by clausification #[20]): Eq (∀ (X61 : Iota), k04_buttercup10100 X61 → b48_buttercup10098 X61) True % 29.89/30.09 Clause #456 (by clausification #[451]): ∀ (a : Iota), Eq (k04_buttercup10100 a → b48_buttercup10098 a) True % 29.89/30.09 Clause #457 (by clausification #[456]): ∀ (a : Iota), Or (Eq (k04_buttercup10100 a) False) (Eq (b48_buttercup10098 a) True) % 29.89/30.09 Clause #558 (by superposition #[433, 101]): ∀ (a : Iota), Or (Eq True False) (Eq (k04_buttercup10619 (skS.0 42 a)) True) % 29.89/30.09 Clause #587 (by clausification #[85]): Eq % 29.89/30.09 (Or % 29.89/30.09 (Or % 29.89/30.09 (Or % 29.89/30.09 (And (∀ (X142 : Iota), b48_buttercup10098 X142 → k04_buttercup10100 X142) % 29.89/30.09 (Exists fun X143 => And (k04_buttercup10100 X143) (Not (b48_buttercup10098 X143)))) % 29.89/30.09 (And (∀ (X144 : Iota), k04_buttercup10100 X144 → b48_buttercup10098 X144) % 29.89/30.09 (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145))))) % 29.89/30.09 (Exists fun X146 => % 29.89/30.09 Exists fun X147 => % 29.89/30.09 Exists fun X148 => % 29.89/30.09 And % 29.89/30.09 (And % 29.89/30.09 (And (And (And (k04_buttercup10100 X146) (b48_buttercup10098 X146)) (k04_buttercup10100 X147)) % 29.89/30.09 (Not (b48_buttercup10098 X147))) % 29.89/30.09 (Not (k04_buttercup10100 X148))) % 29.89/30.09 (b48_buttercup10098 X148))) % 29.89/30.09 (∀ (X149 : Iota), k04_buttercup10100 X149 → Not (b48_buttercup10098 X149))) % 29.89/30.09 False % 29.89/30.09 Clause #589 (by clausification #[587]): Eq % 29.89/30.09 (Or % 29.89/30.09 (Or % 29.89/30.09 (And (∀ (X142 : Iota), b48_buttercup10098 X142 → k04_buttercup10100 X142) % 29.89/30.09 (Exists fun X143 => And (k04_buttercup10100 X143) (Not (b48_buttercup10098 X143)))) % 29.89/30.09 (And (∀ (X144 : Iota), k04_buttercup10100 X144 → b48_buttercup10098 X144) % 29.89/30.09 (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145))))) % 29.89/30.09 (Exists fun X146 => % 29.89/30.09 Exists fun X147 => % 29.89/30.09 Exists fun X148 => % 29.89/30.09 And % 29.89/30.09 (And % 29.89/30.09 (And (And (And (k04_buttercup10100 X146) (b48_buttercup10098 X146)) (k04_buttercup10100 X147)) % 29.89/30.09 (Not (b48_buttercup10098 X147))) % 29.89/30.09 (Not (k04_buttercup10100 X148))) % 29.89/30.09 (b48_buttercup10098 X148))) % 29.89/30.09 False % 29.89/30.09 Clause #664 (by clausification #[332]): ∀ (a : Iota), Eq (b48_buttercup10098 (skS.0 33 a)) True % 29.89/30.09 Clause #886 (by clausification #[558]): ∀ (a : Iota), Eq (k04_buttercup10619 (skS.0 42 a)) True % 29.89/30.09 Clause #888 (by superposition #[886, 215]): ∀ (a : Iota), Or (Eq True False) (Eq (b48_buttercup10098 (skS.0 42 a)) True) % 29.89/30.09 Clause #896 (by clausification #[888]): ∀ (a : Iota), Eq (b48_buttercup10098 (skS.0 42 a)) True % 29.89/30.09 Clause #898 (by clausification #[393]): ∀ (a : Iota), Eq (k04_buttercup10622 (skS.0 33 a)) True % 29.89/30.09 Clause #899 (by superposition #[898, 101]): ∀ (a : Iota), Or (Eq True False) (Eq (k04_buttercup10619 (skS.0 33 a)) True) % 29.89/30.09 Clause #902 (by clausification #[899]): ∀ (a : Iota), Eq (k04_buttercup10619 (skS.0 33 a)) True % 29.89/30.09 Clause #1586 (by clausification #[589]): Eq % 29.89/30.09 (Or % 29.89/30.09 (And (∀ (X142 : Iota), b48_buttercup10098 X142 → k04_buttercup10100 X142) % 29.89/30.09 (Exists fun X143 => And (k04_buttercup10100 X143) (Not (b48_buttercup10098 X143)))) % 29.89/30.09 (And (∀ (X144 : Iota), k04_buttercup10100 X144 → b48_buttercup10098 X144) % 29.89/30.09 (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145))))) % 29.89/30.09 False % 29.89/30.09 Clause #1597 (by clausification #[1586]): Eq % 29.89/30.09 (And (∀ (X144 : Iota), k04_buttercup10100 X144 → b48_buttercup10098 X144) % 29.89/30.09 (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145)))) % 29.89/30.09 False % 29.89/30.09 Clause #1599 (by clausification #[1597]): Or (Eq (∀ (X144 : Iota), k04_buttercup10100 X144 → b48_buttercup10098 X144) False) % 29.96/30.12 (Eq (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145))) False) % 29.96/30.12 Clause #1600 (by clausification #[1599]): ∀ (a : Iota), % 29.96/30.12 Or (Eq (Exists fun X145 => And (b48_buttercup10098 X145) (Not (k04_buttercup10100 X145))) False) % 29.96/30.12 (Eq (Not (k04_buttercup10100 (skS.0 112 a) → b48_buttercup10098 (skS.0 112 a))) True) % 29.96/30.12 Clause #1601 (by clausification #[1600]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (Not (k04_buttercup10100 (skS.0 112 a) → b48_buttercup10098 (skS.0 112 a))) True) % 29.96/30.12 (Eq (And (b48_buttercup10098 a_1) (Not (k04_buttercup10100 a_1))) False) % 29.96/30.12 Clause #1602 (by clausification #[1601]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (And (b48_buttercup10098 a) (Not (k04_buttercup10100 a))) False) % 29.96/30.12 (Eq (k04_buttercup10100 (skS.0 112 a_1) → b48_buttercup10098 (skS.0 112 a_1)) False) % 29.96/30.12 Clause #1603 (by clausification #[1602]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (k04_buttercup10100 (skS.0 112 a) → b48_buttercup10098 (skS.0 112 a)) False) % 29.96/30.12 (Or (Eq (b48_buttercup10098 a_1) False) (Eq (Not (k04_buttercup10100 a_1)) False)) % 29.96/30.12 Clause #1604 (by clausification #[1603]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (b48_buttercup10098 a) False) % 29.96/30.12 (Or (Eq (Not (k04_buttercup10100 a)) False) (Eq (k04_buttercup10100 (skS.0 112 a_1)) True)) % 29.96/30.12 Clause #1605 (by clausification #[1603]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (b48_buttercup10098 a) False) % 29.96/30.12 (Or (Eq (Not (k04_buttercup10100 a)) False) (Eq (b48_buttercup10098 (skS.0 112 a_1)) False)) % 29.96/30.12 Clause #1606 (by clausification #[1604]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (b48_buttercup10098 a) False) % 29.96/30.12 (Or (Eq (k04_buttercup10100 (skS.0 112 a_1)) True) (Eq (k04_buttercup10100 a) True)) % 29.96/30.12 Clause #1627 (by superposition #[1606, 896]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (k04_buttercup10100 (skS.0 112 a)) True) (Or (Eq (k04_buttercup10100 (skS.0 42 a_1)) True) (Eq False True)) % 29.96/30.12 Clause #1628 (by clausification #[1605]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (b48_buttercup10098 a) False) % 29.96/30.12 (Or (Eq (b48_buttercup10098 (skS.0 112 a_1)) False) (Eq (k04_buttercup10100 a) True)) % 29.96/30.12 Clause #1637 (by superposition #[1628, 664]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (b48_buttercup10098 (skS.0 112 a)) False) (Or (Eq (k04_buttercup10100 (skS.0 33 a_1)) True) (Eq False True)) % 29.96/30.12 Clause #1671 (by clausification #[1637]): ∀ (a a_1 : Iota), Or (Eq (b48_buttercup10098 (skS.0 112 a)) False) (Eq (k04_buttercup10100 (skS.0 33 a_1)) True) % 29.96/30.12 Clause #1682 (by clausification #[1627]): ∀ (a a_1 : Iota), Or (Eq (k04_buttercup10100 (skS.0 112 a)) True) (Eq (k04_buttercup10100 (skS.0 42 a_1)) True) % 29.96/30.12 Clause #1716 (by superposition #[1682, 259]): ∀ (a a_1 : Iota), % 29.96/30.12 Or (Eq (k04_buttercup10100 (skS.0 112 a)) True) (Or (Eq True False) (Eq (k04_buttercup10619 (skS.0 42 a_1)) False)) % 29.96/30.12 Clause #1761 (by clausification #[1716]): ∀ (a a_1 : Iota), Or (Eq (k04_buttercup10100 (skS.0 112 a)) True) (Eq (k04_buttercup10619 (skS.0 42 a_1)) False) % 29.96/30.12 Clause #1762 (by superposition #[1761, 886]): ∀ (a : Iota), Or (Eq (k04_buttercup10100 (skS.0 112 a)) True) (Eq False True) % 29.96/30.12 Clause #1763 (by clausification #[1762]): ∀ (a : Iota), Eq (k04_buttercup10100 (skS.0 112 a)) True % 29.96/30.12 Clause #1768 (by superposition #[1763, 457]): ∀ (a : Iota), Or (Eq True False) (Eq (b48_buttercup10098 (skS.0 112 a)) True) % 29.96/30.12 Clause #1796 (by clausification #[1768]): ∀ (a : Iota), Eq (b48_buttercup10098 (skS.0 112 a)) True % 29.96/30.12 Clause #1803 (by superposition #[1796, 1671]): ∀ (a : Iota), Or (Eq True False) (Eq (k04_buttercup10100 (skS.0 33 a)) True) % 29.96/30.12 Clause #1847 (by clausification #[1803]): ∀ (a : Iota), Eq (k04_buttercup10100 (skS.0 33 a)) True % 29.96/30.12 Clause #1849 (by superposition #[1847, 259]): ∀ (a : Iota), Or (Eq True False) (Eq (k04_buttercup10619 (skS.0 33 a)) False) % 29.96/30.12 Clause #1879 (by clausification #[1849]): ∀ (a : Iota), Eq (k04_buttercup10619 (skS.0 33 a)) False % 29.96/30.12 Clause #1880 (by superposition #[1879, 902]): Eq False True % 29.96/30.12 Clause #1881 (by clausification #[1880]): False % 29.96/30.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------