%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO147+1 : TPTP v9.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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:48:04 PM UTC 2025 % Result : Theorem 14.82s 14.98s % Output : Proof 14.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : GEO147+1 : TPTP v9.2.0. Released v2.4.0. % 0.09/0.15 % Command : duper %s % 0.16/0.37 % Computer : n012.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 300 % 0.16/0.37 % DateTime : Fri Oct 3 11:51:53 EDT 2025 % 0.16/0.37 % CPUTime : % 14.82/14.98 SZS status Theorem for theBenchmark.p % 14.82/14.98 SZS output start Proof for theBenchmark.p % 14.82/14.98 Clause #27 (by assumption #[]): Eq (∀ (X Y P : Iota), Iff (connect X Y P) (once (at_the_same_time (at X P) (at Y P)))) True % 14.82/14.98 Clause #31 (by assumption #[]): Eq (∀ (A B : Iota), once (at_the_same_time A B) → And (once A) (once B)) True % 14.82/14.98 Clause #32 (by assumption #[]): Eq (∀ (X P : Iota), Iff (once (at X P)) (incident_o P (trajectory_of X))) True % 14.82/14.98 Clause #36 (by assumption #[]): Eq (Not (∀ (P X Y : Iota), connect X Y P → And (incident_o P (trajectory_of X)) (incident_o P (trajectory_of Y)))) True % 14.82/14.98 Clause #74 (by clausification #[31]): ∀ (a : Iota), Eq (∀ (B : Iota), once (at_the_same_time a B) → And (once a) (once B)) True % 14.82/14.98 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Eq (once (at_the_same_time a a_1) → And (once a) (once a_1)) True % 14.82/14.98 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (once (at_the_same_time a a_1)) False) (Eq (And (once a) (once a_1)) True) % 14.82/14.98 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (once (at_the_same_time a a_1)) False) (Eq (once a_1) True) % 14.82/14.98 Clause #78 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (once (at_the_same_time a a_1)) False) (Eq (once a) True) % 14.82/14.98 Clause #144 (by clausification #[32]): ∀ (a : Iota), Eq (∀ (P : Iota), Iff (once (at a P)) (incident_o P (trajectory_of a))) True % 14.82/14.98 Clause #145 (by clausification #[144]): ∀ (a a_1 : Iota), Eq (Iff (once (at a a_1)) (incident_o a_1 (trajectory_of a))) True % 14.82/14.98 Clause #147 (by clausification #[145]): ∀ (a a_1 : Iota), Or (Eq (once (at a a_1)) False) (Eq (incident_o a_1 (trajectory_of a)) True) % 14.82/14.98 Clause #218 (by clausification #[36]): Eq (∀ (P X Y : Iota), connect X Y P → And (incident_o P (trajectory_of X)) (incident_o P (trajectory_of Y))) False % 14.82/14.98 Clause #219 (by clausification #[218]): ∀ (a : Iota), % 14.82/14.98 Eq % 14.82/14.98 (Not % 14.82/14.98 (∀ (X Y : Iota), % 14.82/14.98 connect X Y (skS.0 16 a) → % 14.82/14.98 And (incident_o (skS.0 16 a) (trajectory_of X)) (incident_o (skS.0 16 a) (trajectory_of Y)))) % 14.82/14.98 True % 14.82/14.98 Clause #220 (by clausification #[219]): ∀ (a : Iota), % 14.82/14.98 Eq % 14.82/14.98 (∀ (X Y : Iota), % 14.82/14.98 connect X Y (skS.0 16 a) → % 14.82/14.98 And (incident_o (skS.0 16 a) (trajectory_of X)) (incident_o (skS.0 16 a) (trajectory_of Y))) % 14.82/14.98 False % 14.82/14.98 Clause #221 (by clausification #[220]): ∀ (a a_1 : Iota), % 14.82/14.98 Eq % 14.82/14.98 (Not % 14.82/14.98 (∀ (Y : Iota), % 14.82/14.98 connect (skS.0 17 a a_1) Y (skS.0 16 a) → % 14.82/14.98 And (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) (incident_o (skS.0 16 a) (trajectory_of Y)))) % 14.82/14.98 True % 14.82/14.98 Clause #222 (by clausification #[221]): ∀ (a a_1 : Iota), % 14.82/14.98 Eq % 14.82/14.98 (∀ (Y : Iota), % 14.82/14.98 connect (skS.0 17 a a_1) Y (skS.0 16 a) → % 14.82/14.98 And (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) (incident_o (skS.0 16 a) (trajectory_of Y))) % 14.82/14.98 False % 14.82/14.98 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 : Iota), % 14.82/14.98 Eq % 14.82/14.98 (Not % 14.82/14.98 (connect (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 16 a) → % 14.82/14.98 And (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) % 14.82/14.98 (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2))))) % 14.82/14.98 True % 14.82/14.98 Clause #224 (by clausification #[223]): ∀ (a a_1 a_2 : Iota), % 14.82/14.98 Eq % 14.82/14.98 (connect (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 16 a) → % 14.82/14.98 And (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) % 14.82/14.98 (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2)))) % 14.82/14.98 False % 14.82/14.98 Clause #225 (by clausification #[224]): ∀ (a a_1 a_2 : Iota), Eq (connect (skS.0 17 a a_1) (skS.0 18 a a_1 a_2) (skS.0 16 a)) True % 14.82/14.98 Clause #226 (by clausification #[224]): ∀ (a a_1 a_2 : Iota), % 14.82/14.98 Eq % 14.82/14.98 (And (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) % 14.82/14.98 (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2)))) % 14.82/14.98 False % 14.82/14.98 Clause #324 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (Y P : Iota), Iff (connect a Y P) (once (at_the_same_time (at a P) (at Y P)))) True % 14.82/14.98 Clause #325 (by clausification #[324]): ∀ (a a_1 : Iota), Eq (∀ (P : Iota), Iff (connect a a_1 P) (once (at_the_same_time (at a P) (at a_1 P)))) True % 14.82/14.98 Clause #326 (by clausification #[325]): ∀ (a a_1 a_2 : Iota), Eq (Iff (connect a a_1 a_2) (once (at_the_same_time (at a a_2) (at a_1 a_2)))) True % 14.82/15.02 Clause #328 (by clausification #[326]): ∀ (a a_1 a_2 : Iota), Or (Eq (connect a a_1 a_2) False) (Eq (once (at_the_same_time (at a a_2) (at a_1 a_2))) True) % 14.82/15.02 Clause #329 (by superposition #[328, 225]): ∀ (a a_1 a_2 : Iota), % 14.82/15.02 Or (Eq (once (at_the_same_time (at (skS.0 17 a a_1) (skS.0 16 a)) (at (skS.0 18 a a_1 a_2) (skS.0 16 a)))) True) % 14.82/15.02 (Eq False True) % 14.82/15.02 Clause #2821 (by clausification #[226]): ∀ (a a_1 a_2 : Iota), % 14.82/15.02 Or (Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) False) % 14.82/15.02 (Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2))) False) % 14.82/15.02 Clause #4067 (by clausification #[329]): ∀ (a a_1 a_2 : Iota), % 14.82/15.02 Eq (once (at_the_same_time (at (skS.0 17 a a_1) (skS.0 16 a)) (at (skS.0 18 a a_1 a_2) (skS.0 16 a)))) True % 14.82/15.02 Clause #4068 (by superposition #[4067, 77]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (once (at (skS.0 18 a a_1 a_2) (skS.0 16 a))) True) % 14.82/15.02 Clause #4069 (by superposition #[4067, 78]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (once (at (skS.0 17 a a_1) (skS.0 16 a))) True) % 14.82/15.02 Clause #4099 (by clausification #[4069]): ∀ (a a_1 : Iota), Eq (once (at (skS.0 17 a a_1) (skS.0 16 a))) True % 14.82/15.02 Clause #4100 (by superposition #[4099, 147]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) True) % 14.82/15.02 Clause #4115 (by clausification #[4100]): ∀ (a a_1 : Iota), Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 17 a a_1))) True % 14.82/15.02 Clause #4116 (by backward demodulation #[4115, 2821]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2))) False) % 14.82/15.02 Clause #4220 (by clausification #[4068]): ∀ (a a_1 a_2 : Iota), Eq (once (at (skS.0 18 a a_1 a_2) (skS.0 16 a))) True % 14.82/15.02 Clause #4221 (by superposition #[4220, 147]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2))) True) % 14.82/15.02 Clause #4236 (by clausification #[4221]): ∀ (a a_1 a_2 : Iota), Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2))) True % 14.82/15.02 Clause #4259 (by clausification #[4116]): ∀ (a a_1 a_2 : Iota), Eq (incident_o (skS.0 16 a) (trajectory_of (skS.0 18 a a_1 a_2))) False % 14.82/15.02 Clause #4260 (by superposition #[4259, 4236]): Eq False True % 14.82/15.02 Clause #4273 (by clausification #[4260]): False % 14.82/15.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------