%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR021+1 : TPTP v9.2.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:02 PM UTC 2025 % Result : Theorem 153.27s 153.46s % Output : Proof 153.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.01/0.12 % Problem : CSR021+1 : TPTP v9.2.0. Bugfixed v3.1.0. % 0.12/0.13 % Command : duper %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 19:56:08 EDT 2025 % 0.13/0.34 % CPUTime : % 153.27/153.46 SZS status Theorem for theBenchmark.p % 153.27/153.46 SZS output start Proof for theBenchmark.p % 153.27/153.46 Clause #9 (by assumption #[]): Eq % 153.27/153.46 (∀ (Event Time Fluent : Iota), % 153.27/153.46 And (happens Event Time) (terminates Event Fluent Time) → Not (holdsAt Fluent (plus Time n1))) % 153.27/153.46 True % 153.27/153.46 Clause #13 (by assumption #[]): Eq % 153.27/153.46 (∀ (Event Fluent Time : Iota), % 153.27/153.46 Iff (terminates Event Fluent Time) % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or (And (And (Eq Event push) (Eq Fluent backwards)) (Not (happens pull Time))) % 153.27/153.46 (And (And (Eq Event pull) (Eq Fluent forwards)) (Not (happens push Time)))) % 153.27/153.46 (And (And (Eq Event pull) (Eq Fluent forwards)) (happens push Time))) % 153.27/153.46 (And (And (Eq Event pull) (Eq Fluent backwards)) (happens push Time))) % 153.27/153.46 (And (And (Eq Event push) (Eq Fluent spinning)) (Not (happens pull Time)))) % 153.27/153.46 (And (And (Eq Event pull) (Eq Fluent spinning)) (Not (happens push Time))))) % 153.27/153.46 True % 153.27/153.46 Clause #15 (by assumption #[]): Eq % 153.27/153.46 (∀ (Event Time : Iota), % 153.27/153.46 Iff (happens Event Time) % 153.27/153.46 (Or % 153.27/153.46 (Or (Or (And (Eq Event push) (Eq Time n0)) (And (Eq Event pull) (Eq Time n1))) % 153.27/153.46 (And (Eq Event pull) (Eq Time n2))) % 153.27/153.46 (And (Eq Event push) (Eq Time n2)))) % 153.27/153.46 True % 153.27/153.46 Clause #25 (by assumption #[]): Eq (Eq (plus n1 n2) n3) True % 153.27/153.46 Clause #30 (by assumption #[]): Eq (∀ (X Y : Iota), Eq (plus X Y) (plus Y X)) True % 153.27/153.46 Clause #47 (by assumption #[]): Eq (Not (Not (holdsAt backwards n3))) True % 153.27/153.46 Clause #65 (by clausification #[47]): Eq (Not (holdsAt backwards n3)) False % 153.27/153.46 Clause #66 (by clausification #[65]): Eq (holdsAt backwards n3) True % 153.27/153.46 Clause #99 (by clausification #[25]): Eq (plus n1 n2) n3 % 153.27/153.46 Clause #207 (by clausification #[9]): ∀ (a : Iota), % 153.27/153.46 Eq (∀ (Time Fluent : Iota), And (happens a Time) (terminates a Fluent Time) → Not (holdsAt Fluent (plus Time n1))) % 153.27/153.46 True % 153.27/153.46 Clause #208 (by clausification #[207]): ∀ (a a_1 : Iota), % 153.27/153.46 Eq (∀ (Fluent : Iota), And (happens a a_1) (terminates a Fluent a_1) → Not (holdsAt Fluent (plus a_1 n1))) True % 153.27/153.46 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), Eq (And (happens a a_1) (terminates a a_2 a_1) → Not (holdsAt a_2 (plus a_1 n1))) True % 153.27/153.46 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 : Iota), % 153.27/153.46 Or (Eq (And (happens a a_1) (terminates a a_2 a_1)) False) (Eq (Not (holdsAt a_2 (plus a_1 n1))) True) % 153.27/153.46 Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 : Iota), % 153.27/153.46 Or (Eq (Not (holdsAt a (plus a_1 n1))) True) (Or (Eq (happens a_2 a_1) False) (Eq (terminates a_2 a a_1) False)) % 153.27/153.46 Clause #212 (by clausification #[211]): ∀ (a a_1 a_2 : Iota), % 153.27/153.46 Or (Eq (happens a a_1) False) (Or (Eq (terminates a a_2 a_1) False) (Eq (holdsAt a_2 (plus a_1 n1)) False)) % 153.27/153.46 Clause #221 (by clausification #[30]): ∀ (a : Iota), Eq (∀ (Y : Iota), Eq (plus a Y) (plus Y a)) True % 153.27/153.46 Clause #222 (by clausification #[221]): ∀ (a a_1 : Iota), Eq (Eq (plus a a_1) (plus a_1 a)) True % 153.27/153.46 Clause #223 (by clausification #[222]): ∀ (a a_1 : Iota), Eq (plus a a_1) (plus a_1 a) % 153.27/153.46 Clause #262 (by clausification #[13]): ∀ (a : Iota), % 153.27/153.46 Eq % 153.27/153.46 (∀ (Fluent Time : Iota), % 153.27/153.46 Iff (terminates a Fluent Time) % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or (And (And (Eq a push) (Eq Fluent backwards)) (Not (happens pull Time))) % 153.27/153.46 (And (And (Eq a pull) (Eq Fluent forwards)) (Not (happens push Time)))) % 153.27/153.46 (And (And (Eq a pull) (Eq Fluent forwards)) (happens push Time))) % 153.27/153.46 (And (And (Eq a pull) (Eq Fluent backwards)) (happens push Time))) % 153.27/153.46 (And (And (Eq a push) (Eq Fluent spinning)) (Not (happens pull Time)))) % 153.27/153.46 (And (And (Eq a pull) (Eq Fluent spinning)) (Not (happens push Time))))) % 153.27/153.46 True % 153.27/153.46 Clause #263 (by clausification #[262]): ∀ (a a_1 : Iota), % 153.27/153.46 Eq % 153.27/153.46 (∀ (Time : Iota), % 153.27/153.46 Iff (terminates a a_1 Time) % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or % 153.27/153.46 (Or (And (And (Eq a push) (Eq a_1 backwards)) (Not (happens pull Time))) % 153.27/153.46 (And (And (Eq a pull) (Eq a_1 forwards)) (Not (happens push Time)))) % 153.27/153.46 (And (And (Eq a pull) (Eq a_1 forwards)) (happens push Time))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 backwards)) (happens push Time))) % 153.27/153.48 (And (And (Eq a push) (Eq a_1 spinning)) (Not (happens pull Time)))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 spinning)) (Not (happens push Time))))) % 153.27/153.48 True % 153.27/153.48 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 : Iota), % 153.27/153.48 Eq % 153.27/153.48 (Iff (terminates a a_1 a_2) % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or (And (And (Eq a push) (Eq a_1 backwards)) (Not (happens pull a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (Not (happens push a_2)))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (happens push a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 backwards)) (happens push a_2))) % 153.27/153.48 (And (And (Eq a push) (Eq a_1 spinning)) (Not (happens pull a_2)))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 spinning)) (Not (happens push a_2))))) % 153.27/153.48 True % 153.27/153.48 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 : Iota), % 153.27/153.48 Or (Eq (terminates a a_1 a_2) True) % 153.27/153.48 (Eq % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or (And (And (Eq a push) (Eq a_1 backwards)) (Not (happens pull a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (Not (happens push a_2)))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (happens push a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 backwards)) (happens push a_2))) % 153.27/153.48 (And (And (Eq a push) (Eq a_1 spinning)) (Not (happens pull a_2)))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 spinning)) (Not (happens push a_2)))) % 153.27/153.48 False) % 153.27/153.48 Clause #268 (by clausification #[265]): ∀ (a a_1 a_2 : Iota), % 153.27/153.48 Or (Eq (terminates a a_1 a_2) True) % 153.27/153.48 (Eq % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or (And (And (Eq a push) (Eq a_1 backwards)) (Not (happens pull a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (Not (happens push a_2)))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (happens push a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 backwards)) (happens push a_2))) % 153.27/153.48 (And (And (Eq a push) (Eq a_1 spinning)) (Not (happens pull a_2)))) % 153.27/153.48 False) % 153.27/153.48 Clause #285 (by clausification #[15]): ∀ (a : Iota), % 153.27/153.48 Eq % 153.27/153.48 (∀ (Time : Iota), % 153.27/153.48 Iff (happens a Time) % 153.27/153.48 (Or (Or (Or (And (Eq a push) (Eq Time n0)) (And (Eq a pull) (Eq Time n1))) (And (Eq a pull) (Eq Time n2))) % 153.27/153.48 (And (Eq a push) (Eq Time n2)))) % 153.27/153.48 True % 153.27/153.48 Clause #286 (by clausification #[285]): ∀ (a a_1 : Iota), % 153.27/153.48 Eq % 153.27/153.48 (Iff (happens a a_1) % 153.27/153.48 (Or (Or (Or (And (Eq a push) (Eq a_1 n0)) (And (Eq a pull) (Eq a_1 n1))) (And (Eq a pull) (Eq a_1 n2))) % 153.27/153.48 (And (Eq a push) (Eq a_1 n2)))) % 153.27/153.48 True % 153.27/153.48 Clause #287 (by clausification #[286]): ∀ (a a_1 : Iota), % 153.27/153.48 Or (Eq (happens a a_1) True) % 153.27/153.48 (Eq % 153.27/153.48 (Or (Or (Or (And (Eq a push) (Eq a_1 n0)) (And (Eq a pull) (Eq a_1 n1))) (And (Eq a pull) (Eq a_1 n2))) % 153.27/153.48 (And (Eq a push) (Eq a_1 n2))) % 153.27/153.48 False) % 153.27/153.48 Clause #289 (by clausification #[287]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Eq (And (Eq a push) (Eq a_1 n2)) False) % 153.27/153.48 Clause #290 (by clausification #[287]): ∀ (a a_1 : Iota), % 153.27/153.48 Or (Eq (happens a a_1) True) % 153.27/153.48 (Eq (Or (Or (And (Eq a push) (Eq a_1 n0)) (And (Eq a pull) (Eq a_1 n1))) (And (Eq a pull) (Eq a_1 n2))) False) % 153.27/153.48 Clause #291 (by clausification #[289]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Or (Eq (Eq a push) False) (Eq (Eq a_1 n2) False)) % 153.27/153.48 Clause #292 (by clausification #[291]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Or (Eq (Eq a_1 n2) False) (Ne a push)) % 153.27/153.48 Clause #293 (by clausification #[292]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Or (Ne a push) (Ne a_1 n2)) % 153.27/153.48 Clause #294 (by destructive equality resolution #[293]): ∀ (a : Iota), Or (Eq (happens push a) True) (Ne a n2) % 153.27/153.48 Clause #295 (by destructive equality resolution #[294]): Eq (happens push n2) True % 153.27/153.48 Clause #1000 (by clausification #[268]): ∀ (a a_1 a_2 : Iota), % 153.27/153.48 Or (Eq (terminates a a_1 a_2) True) % 153.27/153.48 (Eq % 153.27/153.48 (Or % 153.27/153.48 (Or % 153.27/153.48 (Or (And (And (Eq a push) (Eq a_1 backwards)) (Not (happens pull a_2))) % 153.27/153.48 (And (And (Eq a pull) (Eq a_1 forwards)) (Not (happens push a_2)))) % 153.46/153.69 (And (And (Eq a pull) (Eq a_1 forwards)) (happens push a_2))) % 153.46/153.69 (And (And (Eq a pull) (Eq a_1 backwards)) (happens push a_2))) % 153.46/153.69 False) % 153.46/153.69 Clause #1131 (by clausification #[290]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Eq (And (Eq a pull) (Eq a_1 n2)) False) % 153.46/153.69 Clause #1133 (by clausification #[1131]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Or (Eq (Eq a pull) False) (Eq (Eq a_1 n2) False)) % 153.46/153.69 Clause #1134 (by clausification #[1133]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Or (Eq (Eq a_1 n2) False) (Ne a pull)) % 153.46/153.69 Clause #1135 (by clausification #[1134]): ∀ (a a_1 : Iota), Or (Eq (happens a a_1) True) (Or (Ne a pull) (Ne a_1 n2)) % 153.46/153.69 Clause #1136 (by destructive equality resolution #[1135]): ∀ (a : Iota), Or (Eq (happens pull a) True) (Ne a n2) % 153.46/153.69 Clause #1137 (by destructive equality resolution #[1136]): Eq (happens pull n2) True % 153.46/153.69 Clause #1139 (by superposition #[1137, 212]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (terminates pull a n2) False) (Eq (holdsAt a (plus n2 n1)) False)) % 153.46/153.69 Clause #27655 (by clausification #[1000]): ∀ (a a_1 a_2 : Iota), % 153.46/153.69 Or (Eq (terminates a a_1 a_2) True) (Eq (And (And (Eq a pull) (Eq a_1 backwards)) (happens push a_2)) False) % 153.46/153.69 Clause #27657 (by clausification #[27655]): ∀ (a a_1 a_2 : Iota), % 153.46/153.69 Or (Eq (terminates a a_1 a_2) True) (Or (Eq (And (Eq a pull) (Eq a_1 backwards)) False) (Eq (happens push a_2) False)) % 153.46/153.69 Clause #27658 (by clausification #[27657]): ∀ (a a_1 a_2 : Iota), % 153.46/153.69 Or (Eq (terminates a a_1 a_2) True) % 153.46/153.69 (Or (Eq (happens push a_2) False) (Or (Eq (Eq a pull) False) (Eq (Eq a_1 backwards) False))) % 153.46/153.69 Clause #27659 (by clausification #[27658]): ∀ (a a_1 a_2 : Iota), % 153.46/153.69 Or (Eq (terminates a a_1 a_2) True) (Or (Eq (happens push a_2) False) (Or (Eq (Eq a_1 backwards) False) (Ne a pull))) % 153.46/153.69 Clause #27660 (by clausification #[27659]): ∀ (a a_1 a_2 : Iota), % 153.46/153.69 Or (Eq (terminates a a_1 a_2) True) (Or (Eq (happens push a_2) False) (Or (Ne a pull) (Ne a_1 backwards))) % 153.46/153.69 Clause #27661 (by destructive equality resolution #[27660]): ∀ (a a_1 : Iota), Or (Eq (terminates pull a a_1) True) (Or (Eq (happens push a_1) False) (Ne a backwards)) % 153.46/153.69 Clause #27662 (by destructive equality resolution #[27661]): ∀ (a : Iota), Or (Eq (terminates pull backwards a) True) (Eq (happens push a) False) % 153.46/153.69 Clause #27663 (by superposition #[27662, 295]): Or (Eq (terminates pull backwards n2) True) (Eq False True) % 153.46/153.69 Clause #27676 (by clausification #[27663]): Eq (terminates pull backwards n2) True % 153.46/153.69 Clause #34420 (by clausification #[1139]): ∀ (a : Iota), Or (Eq (terminates pull a n2) False) (Eq (holdsAt a (plus n2 n1)) False) % 153.46/153.69 Clause #34421 (by forward demodulation #[34420, 223]): ∀ (a : Iota), Or (Eq (terminates pull a n2) False) (Eq (holdsAt a (plus n1 n2)) False) % 153.46/153.69 Clause #34422 (by forward demodulation #[34421, 99]): ∀ (a : Iota), Or (Eq (terminates pull a n2) False) (Eq (holdsAt a n3) False) % 153.46/153.69 Clause #34423 (by superposition #[34422, 27676]): Or (Eq (holdsAt backwards n3) False) (Eq False True) % 153.46/153.69 Clause #34461 (by clausification #[34423]): Eq (holdsAt backwards n3) False % 153.46/153.69 Clause #34462 (by superposition #[34461, 66]): Eq False True % 153.46/153.69 Clause #34499 (by clausification #[34462]): False % 153.46/153.69 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------