%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR004+2 : TPTP v9.2.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:46:01 PM UTC 2025 % Result : Theorem 3.91s 4.10s % Output : Proof 3.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : CSR004+2 : TPTP v9.2.0. Bugfixed v3.1.0. % 0.04/0.14 % Command : duper %s % 0.14/0.35 % Computer : n001.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 19:32:23 EDT 2025 % 0.14/0.35 % CPUTime : % 3.91/4.10 SZS status Theorem for theBenchmark.p % 3.91/4.10 SZS output start Proof for theBenchmark.p % 3.91/4.10 Clause #15 (by assumption #[]): Eq % 3.91/4.10 (∀ (Event Time : Iota), % 3.91/4.10 Iff (happens Event Time) % 3.91/4.10 (Or (And (Eq Event tapOn) (Eq Time n0)) % 3.91/4.10 (And (And (holdsAt (waterLevel n3) Time) (holdsAt filling Time)) (Eq Event overflow)))) % 3.91/4.10 True % 3.91/4.10 Clause #54 (by assumption #[]): Eq (holdsAt (waterLevel n3) n3) True % 3.91/4.10 Clause #55 (by assumption #[]): Eq (holdsAt filling n3) True % 3.91/4.10 Clause #56 (by assumption #[]): Eq (Not (happens overflow n3)) True % 3.91/4.10 Clause #71 (by clausification #[56]): Eq (happens overflow n3) False % 3.91/4.10 Clause #331 (by clausification #[15]): ∀ (a : Iota), % 3.91/4.10 Eq % 3.91/4.10 (∀ (Time : Iota), % 3.91/4.10 Iff (happens a Time) % 3.91/4.10 (Or (And (Eq a tapOn) (Eq Time n0)) % 3.91/4.10 (And (And (holdsAt (waterLevel n3) Time) (holdsAt filling Time)) (Eq a overflow)))) % 3.91/4.10 True % 3.91/4.10 Clause #332 (by clausification #[331]): ∀ (a a_1 : Iota), % 3.91/4.10 Eq % 3.91/4.10 (Iff (happens a a_1) % 3.91/4.10 (Or (And (Eq a tapOn) (Eq a_1 n0)) % 3.91/4.10 (And (And (holdsAt (waterLevel n3) a_1) (holdsAt filling a_1)) (Eq a overflow)))) % 3.91/4.10 True % 3.91/4.10 Clause #333 (by clausification #[332]): ∀ (a a_1 : Iota), % 3.91/4.10 Or (Eq (happens a a_1) True) % 3.91/4.10 (Eq % 3.91/4.10 (Or (And (Eq a tapOn) (Eq a_1 n0)) % 3.91/4.10 (And (And (holdsAt (waterLevel n3) a_1) (holdsAt filling a_1)) (Eq a overflow))) % 3.91/4.10 False) % 3.91/4.10 Clause #335 (by clausification #[333]): ∀ (a a_1 : Iota), % 3.91/4.10 Or (Eq (happens a a_1) True) % 3.91/4.10 (Eq (And (And (holdsAt (waterLevel n3) a_1) (holdsAt filling a_1)) (Eq a overflow)) False) % 3.91/4.10 Clause #337 (by clausification #[335]): ∀ (a a_1 : Iota), % 3.91/4.10 Or (Eq (happens a a_1) True) % 3.91/4.10 (Or (Eq (And (holdsAt (waterLevel n3) a_1) (holdsAt filling a_1)) False) (Eq (Eq a overflow) False)) % 3.91/4.10 Clause #338 (by clausification #[337]): ∀ (a a_1 : Iota), % 3.91/4.10 Or (Eq (happens a a_1) True) % 3.91/4.10 (Or (Eq (Eq a overflow) False) (Or (Eq (holdsAt (waterLevel n3) a_1) False) (Eq (holdsAt filling a_1) False))) % 3.91/4.10 Clause #339 (by clausification #[338]): ∀ (a a_1 : Iota), % 3.91/4.10 Or (Eq (happens a a_1) True) % 3.91/4.10 (Or (Eq (holdsAt (waterLevel n3) a_1) False) (Or (Eq (holdsAt filling a_1) False) (Ne a overflow))) % 3.91/4.10 Clause #340 (by destructive equality resolution #[339]): ∀ (a : Iota), % 3.91/4.10 Or (Eq (happens overflow a) True) (Or (Eq (holdsAt (waterLevel n3) a) False) (Eq (holdsAt filling a) False)) % 3.91/4.10 Clause #341 (by superposition #[340, 54]): Or (Eq (happens overflow n3) True) (Or (Eq (holdsAt filling n3) False) (Eq False True)) % 3.91/4.10 Clause #342 (by clausification #[341]): Or (Eq (happens overflow n3) True) (Eq (holdsAt filling n3) False) % 3.91/4.10 Clause #343 (by forward demodulation #[342, 55]): Or (Eq (happens overflow n3) True) (Eq True False) % 3.91/4.10 Clause #344 (by clausification #[343]): Eq (happens overflow n3) True % 3.91/4.10 Clause #345 (by superposition #[344, 71]): Eq True False % 3.91/4.10 Clause #350 (by clausification #[345]): False % 3.91/4.10 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------