%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ141^1 : TPTP v9.2.0. Released v6.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:25 PM UTC 2025 % Result : Theorem 27.28s 27.47s % Output : Proof 27.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : PUZ141^1 : TPTP v9.2.0. Released v6.2.0. % 0.14/0.16 % Command : duper %s % 0.15/0.38 % Computer : n010.cluster.edu % 0.15/0.38 % Model : x86_64 x86_64 % 0.15/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.38 % Memory : 8042.1875MB % 0.15/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.38 % CPULimit : 300 % 0.15/0.38 % WCLimit : 300 % 0.15/0.38 % DateTime : Thu Oct 2 20:49:08 EDT 2025 % 0.15/0.38 % CPUTime : % 27.28/27.47 SZS status Theorem for theBenchmark.p % 27.28/27.47 SZS output start Proof for theBenchmark.p % 27.28/27.47 Clause #3 (by assumption #[]): Eq % 27.28/27.47 (∀ (PO : position) (M : movelist) (D : direction), % 27.28/27.47 Eq (playerpos M) PO → Not (wall (next PO D)) → Eq (playerpos (movedir M D)) (next PO D)) % 27.28/27.47 True % 27.28/27.47 Clause #4 (by assumption #[]): Eq % 27.28/27.47 (∀ (PO : position) (M : movelist) (D : direction), % 27.28/27.47 Eq (playerpos M) PO → wall (next PO D) → Eq (playerpos (movedir M D)) PO) % 27.28/27.47 True % 27.28/27.47 Clause #5 (by assumption #[]): Eq (Eq c10 (next c00 right)) True % 27.28/27.47 Clause #6 (by assumption #[]): Eq (Eq c20 (next c10 right)) True % 27.28/27.47 Clause #8 (by assumption #[]): Eq (Eq (wall c10) False) True % 27.28/27.47 Clause #9 (by assumption #[]): Eq (Eq (wall c20) False) True % 27.28/27.47 Clause #10 (by assumption #[]): Eq (Eq (playerpos nomove) c00) True % 27.28/27.47 Clause #11 (by assumption #[]): Eq (Not (Exists fun M => Eq (playerpos M) c20)) True % 27.28/27.47 Clause #12 (by clausification #[10]): Eq (playerpos nomove) c00 % 27.28/27.47 Clause #13 (by clausification #[9]): Eq (wall c20) False % 27.28/27.47 Clause #14 (by clausification #[8]): Eq (wall c10) False % 27.28/27.47 Clause #16 (by clausification #[5]): Eq c10 (next c00 right) % 27.28/27.47 Clause #25 (by clausification #[6]): Eq c20 (next c10 right) % 27.28/27.47 Clause #62 (by clausification #[3]): ∀ (a : position), % 27.28/27.47 Eq % 27.28/27.47 (∀ (M : movelist) (D : direction), % 27.28/27.47 Eq (playerpos M) a → Not (wall (next a D)) → Eq (playerpos (movedir M D)) (next a D)) % 27.28/27.47 True % 27.28/27.47 Clause #63 (by clausification #[62]): ∀ (a : movelist) (a_1 : position), % 27.28/27.47 Eq (∀ (D : direction), Eq (playerpos a) a_1 → Not (wall (next a_1 D)) → Eq (playerpos (movedir a D)) (next a_1 D)) % 27.28/27.47 True % 27.28/27.47 Clause #64 (by clausification #[63]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Eq (Eq (playerpos a) a_1 → Not (wall (next a_1 a_2)) → Eq (playerpos (movedir a a_2)) (next a_1 a_2)) True % 27.28/27.47 Clause #65 (by clausification #[64]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Or (Eq (Eq (playerpos a) a_1) False) % 27.28/27.47 (Eq (Not (wall (next a_1 a_2)) → Eq (playerpos (movedir a a_2)) (next a_1 a_2)) True) % 27.28/27.47 Clause #66 (by clausification #[65]): ∀ (a : position) (a_1 : direction) (a_2 : movelist), % 27.28/27.47 Or (Eq (Not (wall (next a a_1)) → Eq (playerpos (movedir a_2 a_1)) (next a a_1)) True) (Ne (playerpos a_2) a) % 27.28/27.47 Clause #67 (by clausification #[66]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Or (Ne (playerpos a) a_1) % 27.28/27.47 (Or (Eq (Not (wall (next a_1 a_2))) False) (Eq (Eq (playerpos (movedir a a_2)) (next a_1 a_2)) True)) % 27.28/27.47 Clause #68 (by clausification #[67]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Or (Ne (playerpos a) a_1) % 27.28/27.47 (Or (Eq (Eq (playerpos (movedir a a_2)) (next a_1 a_2)) True) (Eq (wall (next a_1 a_2)) True)) % 27.28/27.47 Clause #69 (by clausification #[68]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Or (Ne (playerpos a) a_1) (Or (Eq (wall (next a_1 a_2)) True) (Eq (playerpos (movedir a a_2)) (next a_1 a_2))) % 27.28/27.47 Clause #70 (by destructive equality resolution #[69]): ∀ (a : movelist) (a_1 : direction), % 27.28/27.47 Or (Eq (wall (next (playerpos a) a_1)) True) (Eq (playerpos (movedir a a_1)) (next (playerpos a) a_1)) % 27.28/27.47 Clause #71 (by superposition #[70, 12]): ∀ (a : direction), Or (Eq (wall (next c00 a)) True) (Eq (playerpos (movedir nomove a)) (next c00 a)) % 27.28/27.47 Clause #78 (by clausification #[4]): ∀ (a : position), % 27.28/27.47 Eq (∀ (M : movelist) (D : direction), Eq (playerpos M) a → wall (next a D) → Eq (playerpos (movedir M D)) a) True % 27.28/27.47 Clause #79 (by clausification #[78]): ∀ (a : movelist) (a_1 : position), % 27.28/27.47 Eq (∀ (D : direction), Eq (playerpos a) a_1 → wall (next a_1 D) → Eq (playerpos (movedir a D)) a_1) True % 27.28/27.47 Clause #80 (by clausification #[79]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Eq (Eq (playerpos a) a_1 → wall (next a_1 a_2) → Eq (playerpos (movedir a a_2)) a_1) True % 27.28/27.47 Clause #81 (by clausification #[80]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.28/27.47 Or (Eq (Eq (playerpos a) a_1) False) (Eq (wall (next a_1 a_2) → Eq (playerpos (movedir a a_2)) a_1) True) % 27.28/27.47 Clause #82 (by clausification #[81]): ∀ (a : position) (a_1 : direction) (a_2 : movelist), % 27.28/27.47 Or (Eq (wall (next a a_1) → Eq (playerpos (movedir a_2 a_1)) a) True) (Ne (playerpos a_2) a) % 27.32/27.54 Clause #83 (by clausification #[82]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.32/27.54 Or (Ne (playerpos a) a_1) (Or (Eq (wall (next a_1 a_2)) False) (Eq (Eq (playerpos (movedir a a_2)) a_1) True)) % 27.32/27.54 Clause #84 (by clausification #[83]): ∀ (a : movelist) (a_1 : position) (a_2 : direction), % 27.32/27.54 Or (Ne (playerpos a) a_1) (Or (Eq (wall (next a_1 a_2)) False) (Eq (playerpos (movedir a a_2)) a_1)) % 27.32/27.54 Clause #85 (by destructive equality resolution #[84]): ∀ (a : movelist) (a_1 : direction), % 27.32/27.54 Or (Eq (wall (next (playerpos a) a_1)) False) (Eq (playerpos (movedir a a_1)) (playerpos a)) % 27.32/27.54 Clause #86 (by superposition #[85, 70]): ∀ (a : movelist) (a_1 : direction), % 27.32/27.54 Or (Eq (playerpos (movedir a a_1)) (playerpos a)) % 27.32/27.54 (Or (Eq False True) (Eq (playerpos (movedir a a_1)) (next (playerpos a) a_1))) % 27.32/27.54 Clause #93 (by clausification #[11]): Eq (Exists fun M => Eq (playerpos M) c20) False % 27.32/27.54 Clause #94 (by clausification #[93]): ∀ (a : movelist), Eq (Eq (playerpos a) c20) False % 27.32/27.54 Clause #95 (by clausification #[94]): ∀ (a : movelist), Ne (playerpos a) c20 % 27.32/27.54 Clause #287 (by superposition #[71, 16]): Or (Eq (wall c10) True) (Eq (playerpos (movedir nomove right)) c10) % 27.32/27.54 Clause #288 (by forward demodulation #[287, 14]): Or (Eq False True) (Eq (playerpos (movedir nomove right)) c10) % 27.32/27.54 Clause #289 (by clausification #[288]): Eq (playerpos (movedir nomove right)) c10 % 27.32/27.54 Clause #290 (by superposition #[289, 70]): ∀ (a : direction), Or (Eq (wall (next c10 a)) True) (Eq (playerpos (movedir (movedir nomove right) a)) (next c10 a)) % 27.32/27.54 Clause #292 (by superposition #[289, 95]): Ne c10 c20 % 27.32/27.54 Clause #311 (by clausification #[86]): ∀ (a : movelist) (a_1 : direction), % 27.32/27.54 Or (Eq (playerpos (movedir a a_1)) (playerpos a)) (Eq (playerpos (movedir a a_1)) (next (playerpos a) a_1)) % 27.32/27.54 Clause #315 (by superposition #[311, 95]): ∀ (a : movelist) (a_1 : direction), Or (Eq (playerpos (movedir a a_1)) (playerpos a)) (Ne (next (playerpos a) a_1) c20) % 27.32/27.54 Clause #321 (by superposition #[315, 289]): ∀ (a : direction), Or (Eq (playerpos (movedir (movedir nomove right) a)) c10) (Ne (next c10 a) c20) % 27.32/27.54 Clause #324 (by superposition #[321, 25]): Or (Eq (playerpos (movedir (movedir nomove right) right)) c10) (Ne c20 c20) % 27.32/27.54 Clause #326 (by eliminate resolved literals #[324]): Eq (playerpos (movedir (movedir nomove right) right)) c10 % 27.32/27.54 Clause #8236 (by superposition #[290, 326]): Or (Eq (wall (next c10 right)) True) (Eq c10 (next c10 right)) % 27.32/27.54 Clause #8237 (by forward demodulation #[8236, 25]): Or (Eq (wall c20) True) (Eq c10 (next c10 right)) % 27.32/27.54 Clause #8238 (by forward demodulation #[8237, 13]): Or (Eq False True) (Eq c10 (next c10 right)) % 27.32/27.54 Clause #8239 (by clausification #[8238]): Eq c10 (next c10 right) % 27.32/27.54 Clause #8240 (by superposition #[8239, 25]): Eq c20 c10 % 27.32/27.54 Clause #8290 (by forward contextual literal cutting #[8240, 292]): False % 27.32/27.54 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------