%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW951+1 : TPTP v9.2.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n003.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:06:47 PM UTC 2025 % Result : Theorem 130.99s 131.42s % Output : Proof 130.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.38 % Problem : SWW951+1 : TPTP v9.2.0. Released v7.4.0. % 0.10/0.39 % Command : duper %s % 0.15/0.61 % Computer : n003.cluster.edu % 0.15/0.61 % Model : x86_64 x86_64 % 0.15/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.61 % Memory : 8042.1875MB % 0.15/0.61 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.61 % CPULimit : 300 % 0.15/0.61 % WCLimit : 300 % 0.15/0.61 % DateTime : Thu Oct 2 10:34:08 EDT 2025 % 0.15/0.61 % CPUTime : % 130.99/131.42 SZS status Theorem for theBenchmark.p % 130.99/131.42 SZS output start Proof for theBenchmark.p % 130.99/131.42 Clause #41 (by assumption #[]): Eq (pred_attacker tuple_true) True % 130.99/131.42 Clause #46 (by assumption #[]): Eq (∀ (VAR_V_35 : Iota), pred_attacker (tuple_T_out_4 VAR_V_35) → pred_attacker VAR_V_35) True % 130.99/131.42 Clause #49 (by assumption #[]): Eq (∀ (VAR_V_44 : Iota), pred_attacker VAR_V_44 → pred_attacker (tuple_T_in_3 VAR_V_44)) True % 130.99/131.42 Clause #51 (by assumption #[]): Eq (∀ (VAR_V_50X30 : Iota), pred_attacker VAR_V_50X30 → pred_attacker (tuple_T_in_1 VAR_V_50X30)) True % 130.99/131.42 Clause #64 (by assumption #[]): Eq % 130.99/131.42 (∀ (VAR_K_XOR_K1_10X305 VAR_R1_10X306 : Iota), % 130.99/131.42 And (pred_attacker (tuple_T_in_3 VAR_K_XOR_K1_10X305)) (pred_attacker (tuple_T_in_1 VAR_R1_10X306)) → % 130.99/131.42 pred_attacker (tuple_T_out_4 name_objective)) % 130.99/131.42 True % 130.99/131.42 Clause #65 (by assumption #[]): Eq (Not (pred_attacker name_objective)) True % 130.99/131.42 Clause #67 (by clausification #[65]): Eq (pred_attacker name_objective) False % 130.99/131.42 Clause #79 (by clausification #[46]): ∀ (a : Iota), Eq (pred_attacker (tuple_T_out_4 a) → pred_attacker a) True % 130.99/131.42 Clause #80 (by clausification #[79]): ∀ (a : Iota), Or (Eq (pred_attacker (tuple_T_out_4 a)) False) (Eq (pred_attacker a) True) % 130.99/131.42 Clause #197 (by clausification #[49]): ∀ (a : Iota), Eq (pred_attacker a → pred_attacker (tuple_T_in_3 a)) True % 130.99/131.42 Clause #198 (by clausification #[197]): ∀ (a : Iota), Or (Eq (pred_attacker a) False) (Eq (pred_attacker (tuple_T_in_3 a)) True) % 130.99/131.42 Clause #207 (by superposition #[198, 41]): Or (Eq (pred_attacker (tuple_T_in_3 tuple_true)) True) (Eq False True) % 130.99/131.42 Clause #218 (by clausification #[207]): Eq (pred_attacker (tuple_T_in_3 tuple_true)) True % 130.99/131.42 Clause #344 (by clausification #[51]): ∀ (a : Iota), Eq (pred_attacker a → pred_attacker (tuple_T_in_1 a)) True % 130.99/131.42 Clause #345 (by clausification #[344]): ∀ (a : Iota), Or (Eq (pred_attacker a) False) (Eq (pred_attacker (tuple_T_in_1 a)) True) % 130.99/131.42 Clause #354 (by superposition #[345, 41]): Or (Eq (pred_attacker (tuple_T_in_1 tuple_true)) True) (Eq False True) % 130.99/131.42 Clause #379 (by clausification #[354]): Eq (pred_attacker (tuple_T_in_1 tuple_true)) True % 130.99/131.42 Clause #591 (by clausification #[64]): ∀ (a : Iota), % 130.99/131.42 Eq % 130.99/131.42 (∀ (VAR_R1_10X306 : Iota), % 130.99/131.42 And (pred_attacker (tuple_T_in_3 a)) (pred_attacker (tuple_T_in_1 VAR_R1_10X306)) → % 130.99/131.42 pred_attacker (tuple_T_out_4 name_objective)) % 130.99/131.42 True % 130.99/131.42 Clause #592 (by clausification #[591]): ∀ (a a_1 : Iota), % 130.99/131.42 Eq % 130.99/131.42 (And (pred_attacker (tuple_T_in_3 a)) (pred_attacker (tuple_T_in_1 a_1)) → % 130.99/131.42 pred_attacker (tuple_T_out_4 name_objective)) % 130.99/131.42 True % 130.99/131.42 Clause #593 (by clausification #[592]): ∀ (a a_1 : Iota), % 130.99/131.42 Or (Eq (And (pred_attacker (tuple_T_in_3 a)) (pred_attacker (tuple_T_in_1 a_1))) False) % 130.99/131.42 (Eq (pred_attacker (tuple_T_out_4 name_objective)) True) % 130.99/131.42 Clause #594 (by clausification #[593]): ∀ (a a_1 : Iota), % 130.99/131.42 Or (Eq (pred_attacker (tuple_T_out_4 name_objective)) True) % 130.99/131.42 (Or (Eq (pred_attacker (tuple_T_in_3 a)) False) (Eq (pred_attacker (tuple_T_in_1 a_1)) False)) % 130.99/131.42 Clause #595 (by superposition #[594, 218]): ∀ (a : Iota), % 130.99/131.42 Or (Eq (pred_attacker (tuple_T_out_4 name_objective)) True) % 130.99/131.42 (Or (Eq (pred_attacker (tuple_T_in_1 a)) False) (Eq False True)) % 130.99/131.42 Clause #45843 (by clausification #[595]): ∀ (a : Iota), Or (Eq (pred_attacker (tuple_T_out_4 name_objective)) True) (Eq (pred_attacker (tuple_T_in_1 a)) False) % 130.99/131.42 Clause #45844 (by superposition #[45843, 379]): Or (Eq (pred_attacker (tuple_T_out_4 name_objective)) True) (Eq False True) % 130.99/131.42 Clause #45845 (by clausification #[45844]): Eq (pred_attacker (tuple_T_out_4 name_objective)) True % 130.99/131.42 Clause #45846 (by superposition #[45845, 80]): Or (Eq True False) (Eq (pred_attacker name_objective) True) % 130.99/131.42 Clause #45959 (by clausification #[45846]): Eq (pred_attacker name_objective) True % 130.99/131.42 Clause #45960 (by superposition #[45959, 67]): Eq True False % 130.99/131.42 Clause #46073 (by clausification #[45960]): False % 130.99/131.42 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------