%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYN351+1 : TPTP v9.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:07:28 PM UTC 2025 % Result : Theorem 3.72s 3.88s % Output : Proof 3.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN351+1 : TPTP v9.2.0. Released v2.0.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n028.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 15:20:23 EDT 2025 % 0.14/0.35 % CPUTime : % 3.72/3.88 SZS status Theorem for theBenchmark.p % 3.72/3.88 SZS output start Proof for theBenchmark.p % 3.72/3.88 Clause #0 (by assumption #[]): Eq % 3.72/3.88 (Not % 3.72/3.88 (∀ (X1 X2 : Iota), % 3.72/3.88 Exists fun Y1 => % 3.72/3.88 Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f X1 Y2 X1 Z → % 3.72/3.88 Iff (big_f X1 Y1 X1 Y2) (big_f Y1 X2 Y1 Y2) → % 3.72/3.88 big_f X1 Y1 X1 Y2 → % 3.72/3.88 And (big_f X1 Y2 Y1 Y2 → big_f X1 Z Y1 Z) % 3.72/3.88 (big_f X1 Z Y1 Z → Iff (big_f X1 Y1 X1 Y2) (big_f X1 Y2 Y1 Y2)))) % 3.72/3.88 True % 3.72/3.88 Clause #1 (by clausification #[0]): Eq % 3.72/3.88 (∀ (X1 X2 : Iota), % 3.72/3.88 Exists fun Y1 => % 3.72/3.88 Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f X1 Y2 X1 Z → % 3.72/3.88 Iff (big_f X1 Y1 X1 Y2) (big_f Y1 X2 Y1 Y2) → % 3.72/3.88 big_f X1 Y1 X1 Y2 → % 3.72/3.88 And (big_f X1 Y2 Y1 Y2 → big_f X1 Z Y1 Z) % 3.72/3.88 (big_f X1 Z Y1 Z → Iff (big_f X1 Y1 X1 Y2) (big_f X1 Y2 Y1 Y2))) % 3.72/3.88 False % 3.72/3.88 Clause #2 (by clausification #[1]): ∀ (a : Iota), % 3.72/3.88 Eq % 3.72/3.88 (Not % 3.72/3.88 (∀ (X2 : Iota), % 3.72/3.88 Exists fun Y1 => % 3.72/3.88 Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f (skS.0 0 a) Y2 (skS.0 0 a) Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f Y1 X2 Y1 Y2) → % 3.72/3.88 big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2 → % 3.72/3.88 And (big_f (skS.0 0 a) Y2 Y1 Y2 → big_f (skS.0 0 a) Z Y1 Z) % 3.72/3.88 (big_f (skS.0 0 a) Z Y1 Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f (skS.0 0 a) Y2 Y1 Y2)))) % 3.72/3.88 True % 3.72/3.88 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 3.72/3.88 Eq % 3.72/3.88 (∀ (X2 : Iota), % 3.72/3.88 Exists fun Y1 => % 3.72/3.88 Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f (skS.0 0 a) Y2 (skS.0 0 a) Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f Y1 X2 Y1 Y2) → % 3.72/3.88 big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2 → % 3.72/3.88 And (big_f (skS.0 0 a) Y2 Y1 Y2 → big_f (skS.0 0 a) Z Y1 Z) % 3.72/3.88 (big_f (skS.0 0 a) Z Y1 Z → Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f (skS.0 0 a) Y2 Y1 Y2))) % 3.72/3.88 False % 3.72/3.88 Clause #4 (by clausification #[3]): ∀ (a a_1 : Iota), % 3.72/3.88 Eq % 3.72/3.88 (Not % 3.72/3.88 (Exists fun Y1 => % 3.72/3.88 Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f (skS.0 0 a) Y2 (skS.0 0 a) Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f Y1 (skS.0 1 a a_1) Y1 Y2) → % 3.72/3.88 big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2 → % 3.72/3.88 And (big_f (skS.0 0 a) Y2 Y1 Y2 → big_f (skS.0 0 a) Z Y1 Z) % 3.72/3.88 (big_f (skS.0 0 a) Z Y1 Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f (skS.0 0 a) Y2 Y1 Y2)))) % 3.72/3.88 True % 3.72/3.88 Clause #5 (by clausification #[4]): ∀ (a a_1 : Iota), % 3.72/3.88 Eq % 3.72/3.88 (Exists fun Y1 => % 3.72/3.88 Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f (skS.0 0 a) Y2 (skS.0 0 a) Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f Y1 (skS.0 1 a a_1) Y1 Y2) → % 3.72/3.88 big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2 → % 3.72/3.88 And (big_f (skS.0 0 a) Y2 Y1 Y2 → big_f (skS.0 0 a) Z Y1 Z) % 3.72/3.88 (big_f (skS.0 0 a) Z Y1 Z → Iff (big_f (skS.0 0 a) Y1 (skS.0 0 a) Y2) (big_f (skS.0 0 a) Y2 Y1 Y2))) % 3.72/3.88 False % 3.72/3.88 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 : Iota), % 3.72/3.88 Eq % 3.72/3.88 (Exists fun Y2 => % 3.72/3.88 ∀ (Z : Iota), % 3.72/3.88 big_f (skS.0 0 a) Y2 (skS.0 0 a) Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) a_1 (skS.0 0 a) Y2) (big_f a_1 (skS.0 1 a a_2) a_1 Y2) → % 3.72/3.88 big_f (skS.0 0 a) a_1 (skS.0 0 a) Y2 → % 3.72/3.88 And (big_f (skS.0 0 a) Y2 a_1 Y2 → big_f (skS.0 0 a) Z a_1 Z) % 3.72/3.88 (big_f (skS.0 0 a) Z a_1 Z → Iff (big_f (skS.0 0 a) a_1 (skS.0 0 a) Y2) (big_f (skS.0 0 a) Y2 a_1 Y2))) % 3.72/3.88 False % 3.72/3.88 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 a_3 : Iota), % 3.72/3.88 Eq % 3.72/3.88 (∀ (Z : Iota), % 3.72/3.88 big_f (skS.0 0 a) a_1 (skS.0 0 a) Z → % 3.72/3.88 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f a_2 (skS.0 1 a a_3) a_2 a_1) → % 3.72/3.88 big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1 → % 3.72/3.88 And (big_f (skS.0 0 a) a_1 a_2 a_1 → big_f (skS.0 0 a) Z a_2 Z) % 3.72/3.88 (big_f (skS.0 0 a) Z a_2 Z → Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1))) % 3.73/3.91 False % 3.73/3.91 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Eq % 3.73/3.91 (Not % 3.73/3.91 (big_f (skS.0 0 a) a_1 (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f a_2 (skS.0 1 a a_3) a_2 a_1) → % 3.73/3.91 big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1 → % 3.73/3.91 And % 3.73/3.91 (big_f (skS.0 0 a) a_1 a_2 a_1 → % 3.73/3.91 big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1)))) % 3.73/3.91 True % 3.73/3.91 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Eq % 3.73/3.91 (big_f (skS.0 0 a) a_1 (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f a_2 (skS.0 1 a a_3) a_2 a_1) → % 3.73/3.91 big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1 → % 3.73/3.91 And % 3.73/3.91 (big_f (skS.0 0 a) a_1 a_2 a_1 → % 3.73/3.91 big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1))) % 3.73/3.91 False % 3.73/3.91 Clause #11 (by clausification #[9]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Eq % 3.73/3.91 (Iff (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_2) (big_f a_1 (skS.0 1 a a_3) a_1 a_2) → % 3.73/3.91 big_f (skS.0 0 a) a_1 (skS.0 0 a) a_2 → % 3.73/3.91 And % 3.73/3.91 (big_f (skS.0 0 a) a_2 a_1 a_2 → % 3.73/3.91 big_f (skS.0 0 a) (skS.0 2 a a_2 a_1 a_3 a_4) a_1 (skS.0 2 a a_2 a_1 a_3 a_4)) % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_2 a_1 a_3 a_4) a_1 (skS.0 2 a a_2 a_1 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_2) (big_f (skS.0 0 a) a_2 a_1 a_2))) % 3.73/3.91 False % 3.73/3.91 Clause #13 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Eq % 3.73/3.91 (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_2 → % 3.73/3.91 And % 3.73/3.91 (big_f (skS.0 0 a) a_2 a_1 a_2 → big_f (skS.0 0 a) (skS.0 2 a a_2 a_1 a_3 a_4) a_1 (skS.0 2 a a_2 a_1 a_3 a_4)) % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_2 a_1 a_3 a_4) a_1 (skS.0 2 a a_2 a_1 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_2) (big_f (skS.0 0 a) a_2 a_1 a_2))) % 3.73/3.91 False % 3.73/3.91 Clause #21 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_2) True % 3.73/3.91 Clause #22 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Eq % 3.73/3.91 (And (big_f (skS.0 0 a) a_1 a_2 a_1 → big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1))) % 3.73/3.91 False % 3.73/3.91 Clause #27 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Or % 3.73/3.91 (Eq (big_f (skS.0 0 a) a_1 a_2 a_1 → big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) % 3.73/3.91 False) % 3.73/3.91 (Eq % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1)) % 3.73/3.91 False) % 3.73/3.91 Clause #29 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Or % 3.73/3.91 (Eq % 3.73/3.91 (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4) → % 3.73/3.91 Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1)) % 3.73/3.91 False) % 3.73/3.91 (Eq (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) False) % 3.73/3.91 Clause #35 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Or (Eq (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) False) % 3.73/3.91 (Eq (Iff (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) (big_f (skS.0 0 a) a_1 a_2 a_1)) False) % 3.73/3.91 Clause #37 (by clausification #[35]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Or (Eq (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) False) % 3.73/3.91 (Or (Eq (big_f (skS.0 0 a) a_2 (skS.0 0 a) a_1) False) (Eq (big_f (skS.0 0 a) a_1 a_2 a_1) False)) % 3.73/3.91 Clause #39 (by forward demodulation #[37, 21]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Or (Eq (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) False) % 3.73/3.91 (Or (Eq True False) (Eq (big_f (skS.0 0 a) a_1 a_2 a_1) False)) % 3.73/3.91 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 3.73/3.91 Or (Eq (big_f (skS.0 0 a) (skS.0 2 a a_1 a_2 a_3 a_4) a_2 (skS.0 2 a a_1 a_2 a_3 a_4)) False) % 3.73/3.91 (Eq (big_f (skS.0 0 a) a_1 a_2 a_1) False) % 3.73/3.91 Clause #42 (by superposition #[40, 21]): ∀ (a a_1 : Iota), Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_1) False) (Eq False True) % 3.73/3.91 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a) a_1) False % 3.73/3.91 Clause #45 (by superposition #[43, 21]): Eq False True % 3.73/3.91 Clause #46 (by clausification #[45]): False % 3.73/3.91 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------