%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ047^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:16 PM UTC 2025 % Result : Theorem 9.49s 9.68s % Output : Proof 9.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : PUZ047^5 : TPTP v9.2.0. Released v4.0.0. % 0.10/0.11 % Command : duper %s % 0.10/0.31 % Computer : n014.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Thu Oct 2 20:54:38 EDT 2025 % 0.10/0.31 % CPUTime : % 9.49/9.68 SZS status Theorem for theBenchmark.p % 9.49/9.68 SZS output start Proof for theBenchmark.p % 9.49/9.68 Clause #0 (by assumption #[]): Eq % 9.49/9.68 (Not % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.49/9.68 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.49/9.68 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.49/9.68 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.49/9.68 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.49/9.68 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.49/9.68 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.49/9.68 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.49/9.68 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.49/9.68 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.49/9.68 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.49/9.68 (∀ (T9 : b), cP cN cN cS cN T9 → cP cS cN cS cS (cD T9))) % 9.49/9.68 (∀ (U1 : b), cP cS cS cN cS U1 → cP cN cS cN cN (cD U1))) % 9.49/9.68 (∀ (V1 : b), cP cN cS cN cN V1 → cP cS cS cN cS (cD V1)) → % 9.49/9.68 Exists fun Z => cP cN cN cN cN Z)) % 9.49/9.68 True % 9.49/9.68 Clause #1 (by betaEtaReduce #[0]): Eq % 9.49/9.68 (Not % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.49/9.68 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.49/9.68 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.49/9.68 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.49/9.68 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.49/9.68 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.49/9.68 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.49/9.68 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.49/9.68 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.49/9.68 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.49/9.68 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.49/9.68 (∀ (T9 : b), cP cN cN cS cN T9 → cP cS cN cS cS (cD T9))) % 9.49/9.68 (∀ (U1 : b), cP cS cS cN cS U1 → cP cN cS cN cN (cD U1))) % 9.49/9.68 (∀ (V1 : b), cP cN cS cN cN V1 → cP cS cS cN cS (cD V1)) → % 9.49/9.68 Exists (cP cN cN cN cN))) % 9.49/9.68 True % 9.49/9.68 Clause #2 (by clausification #[1]): Eq % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And % 9.49/9.68 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.49/9.68 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.49/9.68 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.49/9.68 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.49/9.68 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.49/9.68 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.49/9.68 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.49/9.68 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.51/9.70 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.51/9.70 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.51/9.70 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.51/9.70 (∀ (T9 : b), cP cN cN cS cN T9 → cP cS cN cS cS (cD T9))) % 9.51/9.70 (∀ (U1 : b), cP cS cS cN cS U1 → cP cN cS cN cN (cD U1))) % 9.51/9.70 (∀ (V1 : b), cP cN cS cN cN V1 → cP cS cS cN cS (cD V1)) → % 9.51/9.70 Exists (cP cN cN cN cN)) % 9.51/9.70 False % 9.51/9.70 Clause #3 (by clausification #[2]): Eq % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.51/9.70 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.51/9.70 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.51/9.70 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.51/9.70 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.51/9.70 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.51/9.70 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.51/9.70 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.51/9.70 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.51/9.70 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.51/9.70 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.51/9.70 (∀ (T9 : b), cP cN cN cS cN T9 → cP cS cN cS cS (cD T9))) % 9.51/9.70 (∀ (U1 : b), cP cS cS cN cS U1 → cP cN cS cN cN (cD U1))) % 9.51/9.70 (∀ (V1 : b), cP cN cS cN cN V1 → cP cS cS cN cS (cD V1))) % 9.51/9.70 True % 9.51/9.70 Clause #4 (by clausification #[2]): Eq (Exists (cP cN cN cN cN)) False % 9.51/9.70 Clause #6 (by clausification #[3]): Eq % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.51/9.70 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.51/9.70 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.51/9.70 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.51/9.70 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.51/9.70 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.51/9.70 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.51/9.70 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.51/9.70 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.51/9.70 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.51/9.70 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.51/9.70 (∀ (T9 : b), cP cN cN cS cN T9 → cP cS cN cS cS (cD T9))) % 9.51/9.70 (∀ (U1 : b), cP cS cS cN cS U1 → cP cN cS cN cN (cD U1))) % 9.51/9.70 True % 9.51/9.70 Clause #9 (by clausification #[4]): ∀ (a : b), Eq (cP cN cN cN cN a) False % 9.51/9.70 Clause #11 (by clausification #[6]): Eq % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And % 9.51/9.70 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.51/9.70 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.51/9.70 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.51/9.70 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.51/9.70 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.51/9.70 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.72 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.53/9.72 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.53/9.72 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.53/9.72 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.53/9.72 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.53/9.72 (∀ (T9 : b), cP cN cN cS cN T9 → cP cS cN cS cS (cD T9))) % 9.53/9.72 True % 9.53/9.72 Clause #15 (by clausification #[11]): Eq % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.72 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.72 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.72 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.72 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.72 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.72 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.53/9.72 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.53/9.72 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.53/9.72 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.53/9.72 (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8))) % 9.53/9.72 True % 9.53/9.72 Clause #18 (by clausification #[15]): Eq (∀ (T8 : b), cP cS cN cS cS T8 → cP cN cN cS cN (cD T8)) True % 9.53/9.72 Clause #19 (by clausification #[15]): Eq % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.72 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.72 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.72 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.72 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.72 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.72 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.53/9.72 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.53/9.72 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.53/9.72 (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V))) % 9.53/9.72 True % 9.53/9.72 Clause #20 (by clausification #[18]): ∀ (a : b), Eq (cP cS cN cS cS a → cP cN cN cS cN (cD a)) True % 9.53/9.72 Clause #21 (by clausification #[20]): ∀ (a : b), Or (Eq (cP cS cN cS cS a) False) (Eq (cP cN cN cS cN (cD a)) True) % 9.53/9.72 Clause #22 (by clausification #[19]): Eq (∀ (X1 Y1 : a) (V : b), cP cN X1 cN Y1 V → cP cS X1 cS Y1 (cG V)) True % 9.53/9.72 Clause #23 (by clausification #[19]): Eq % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And % 9.53/9.72 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.72 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.72 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.72 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.72 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.72 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.72 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.53/9.72 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.53/9.72 (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U))) % 9.53/9.72 True % 9.53/9.72 Clause #24 (by clausification #[22]): ∀ (a_1 : a), Eq (∀ (Y1 : a) (V : b), cP cN a_1 cN Y1 V → cP cS a_1 cS Y1 (cG V)) True % 9.53/9.72 Clause #25 (by clausification #[24]): ∀ (a_1 a : a), Eq (∀ (V : b), cP cN a_1 cN a V → cP cS a_1 cS a (cG V)) True % 9.53/9.72 Clause #26 (by clausification #[25]): ∀ (a_1 a : a) (a_2 : b), Eq (cP cN a_1 cN a a_2 → cP cS a_1 cS a (cG a_2)) True % 9.53/9.75 Clause #27 (by clausification #[26]): ∀ (a_1 a : a) (a_2 : b), Or (Eq (cP cN a_1 cN a a_2) False) (Eq (cP cS a_1 cS a (cG a_2)) True) % 9.53/9.75 Clause #28 (by clausification #[23]): Eq (∀ (X Y : a) (U : b), cP cS X cS Y U → cP cN X cN Y (cG U)) True % 9.53/9.75 Clause #29 (by clausification #[23]): Eq % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.75 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.75 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.75 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.75 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.75 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.75 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.53/9.75 (∀ (T7 : b), cP cN cN cN cS T7 → cP cS cS cN cS (cW T7))) % 9.53/9.75 True % 9.53/9.75 Clause #30 (by clausification #[28]): ∀ (a_1 : a), Eq (∀ (Y : a) (U : b), cP cS a_1 cS Y U → cP cN a_1 cN Y (cG U)) True % 9.53/9.75 Clause #31 (by clausification #[30]): ∀ (a_1 a : a), Eq (∀ (U : b), cP cS a_1 cS a U → cP cN a_1 cN a (cG U)) True % 9.53/9.75 Clause #32 (by clausification #[31]): ∀ (a_1 a : a) (a_2 : b), Eq (cP cS a_1 cS a a_2 → cP cN a_1 cN a (cG a_2)) True % 9.53/9.75 Clause #33 (by clausification #[32]): ∀ (a_1 a : a) (a_2 : b), Or (Eq (cP cS a_1 cS a a_2) False) (Eq (cP cN a_1 cN a (cG a_2)) True) % 9.53/9.75 Clause #35 (by clausification #[29]): Eq % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.75 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.75 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.75 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.75 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.75 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.75 (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6))) % 9.53/9.75 True % 9.53/9.75 Clause #38 (by clausification #[35]): Eq (∀ (T6 : b), cP cS cS cN cS T6 → cP cN cN cN cS (cW T6)) True % 9.53/9.75 Clause #39 (by clausification #[35]): Eq % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.75 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.75 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.75 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.75 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.75 (∀ (T5 : b), cP cN cN cS cN T5 → cP cS cS cS cN (cW T5))) % 9.53/9.75 True % 9.53/9.75 Clause #40 (by clausification #[38]): ∀ (a : b), Eq (cP cS cS cN cS a → cP cN cN cN cS (cW a)) True % 9.53/9.75 Clause #41 (by clausification #[40]): ∀ (a : b), Or (Eq (cP cS cS cN cS a) False) (Eq (cP cN cN cN cS (cW a)) True) % 9.53/9.75 Clause #43 (by clausification #[39]): Eq % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.75 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.75 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.75 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.75 (∀ (T4 : b), cP cS cS cS cN T4 → cP cN cN cS cN (cW T4))) % 9.53/9.75 True % 9.53/9.75 Clause #47 (by clausification #[43]): Eq % 9.53/9.75 (And % 9.53/9.75 (And % 9.53/9.75 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.75 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.75 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.75 (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3))) % 9.53/9.75 True % 9.53/9.75 Clause #50 (by clausification #[47]): Eq (∀ (T3 : b), cP cN cS cN cS T3 → cP cS cS cN cS (cL T3)) True % 9.53/9.75 Clause #51 (by clausification #[47]): Eq % 9.53/9.75 (And % 9.53/9.75 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.75 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.76 (∀ (T2 : b), cP cS cS cN cS T2 → cP cN cS cN cS (cL T2))) % 9.53/9.76 True % 9.53/9.76 Clause #52 (by clausification #[50]): ∀ (a : b), Eq (cP cN cS cN cS a → cP cS cS cN cS (cL a)) True % 9.53/9.76 Clause #53 (by clausification #[52]): ∀ (a : b), Or (Eq (cP cN cS cN cS a) False) (Eq (cP cS cS cN cS (cL a)) True) % 9.53/9.76 Clause #55 (by clausification #[51]): Eq % 9.53/9.76 (And (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) % 9.53/9.76 (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1))) % 9.53/9.76 True % 9.53/9.76 Clause #58 (by clausification #[55]): Eq (∀ (T1 : b), cP cN cN cS cN T1 → cP cS cN cS cN (cL T1)) True % 9.53/9.76 Clause #59 (by clausification #[55]): Eq (And (cP cS cS cS cS cO) (∀ (T : b), cP cS cN cS cN T → cP cN cN cS cN (cL T))) True % 9.53/9.76 Clause #60 (by clausification #[58]): ∀ (a : b), Eq (cP cN cN cS cN a → cP cS cN cS cN (cL a)) True % 9.53/9.76 Clause #61 (by clausification #[60]): ∀ (a : b), Or (Eq (cP cN cN cS cN a) False) (Eq (cP cS cN cS cN (cL a)) True) % 9.53/9.76 Clause #63 (by clausification #[59]): Eq (cP cS cS cS cS cO) True % 9.53/9.76 Clause #66 (by superposition #[63, 33]): Or (Eq True False) (Eq (cP cN cS cN cS (cG cO)) True) % 9.53/9.76 Clause #67 (by clausification #[66]): Eq (cP cN cS cN cS (cG cO)) True % 9.53/9.76 Clause #68 (by superposition #[67, 53]): Or (Eq True False) (Eq (cP cS cS cN cS (cL (cG cO))) True) % 9.53/9.76 Clause #70 (by clausification #[68]): Eq (cP cS cS cN cS (cL (cG cO))) True % 9.53/9.76 Clause #72 (by superposition #[70, 41]): Or (Eq True False) (Eq (cP cN cN cN cS (cW (cL (cG cO)))) True) % 9.53/9.76 Clause #79 (by clausification #[72]): Eq (cP cN cN cN cS (cW (cL (cG cO)))) True % 9.53/9.76 Clause #81 (by superposition #[79, 27]): Or (Eq True False) (Eq (cP cS cN cS cS (cG (cW (cL (cG cO))))) True) % 9.53/9.76 Clause #105 (by clausification #[81]): Eq (cP cS cN cS cS (cG (cW (cL (cG cO))))) True % 9.53/9.76 Clause #106 (by superposition #[105, 21]): Or (Eq True False) (Eq (cP cN cN cS cN (cD (cG (cW (cL (cG cO)))))) True) % 9.53/9.76 Clause #166 (by clausification #[106]): Eq (cP cN cN cS cN (cD (cG (cW (cL (cG cO)))))) True % 9.53/9.76 Clause #169 (by superposition #[166, 61]): Or (Eq True False) (Eq (cP cS cN cS cN (cL (cD (cG (cW (cL (cG cO))))))) True) % 9.53/9.76 Clause #170 (by clausification #[169]): Eq (cP cS cN cS cN (cL (cD (cG (cW (cL (cG cO))))))) True % 9.53/9.76 Clause #172 (by superposition #[170, 33]): Or (Eq True False) (Eq (cP cN cN cN cN (cG (cL (cD (cG (cW (cL (cG cO)))))))) True) % 9.53/9.76 Clause #319 (by clausification #[172]): Eq (cP cN cN cN cN (cG (cL (cD (cG (cW (cL (cG cO)))))))) True % 9.53/9.76 Clause #320 (by superposition #[319, 9]): Eq True False % 9.53/9.76 Clause #322 (by clausification #[320]): False % 9.53/9.76 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------