%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR035+1 : TPTP v9.2.0. Released v3.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:46:06 PM UTC 2025 % Result : Theorem 5.84s 6.01s % Output : Proof 5.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : CSR035+1 : TPTP v9.2.0. Released v3.4.0. % 0.12/0.11 % Command : duper %s % 0.12/0.32 % Computer : n012.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Thu Oct 2 20:12:23 EDT 2025 % 0.12/0.32 % CPUTime : % 5.84/6.01 SZS status Theorem for theBenchmark.p % 5.84/6.01 SZS output start Proof for theBenchmark.p % 5.84/6.01 Clause #0 (by assumption #[]): Eq % 5.84/6.01 (mtvisible c_englishmt → % 5.84/6.01 prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) % 5.84/6.01 s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege) % 5.84/6.01 True % 5.84/6.01 Clause #33 (by assumption #[]): Eq % 5.84/6.01 (Not % 5.84/6.01 (Exists fun X => % 5.84/6.01 mtvisible c_englishmt → % 5.84/6.01 prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) X)) % 5.84/6.01 True % 5.84/6.01 Clause #45 (by clausification #[0]): Or (Eq (mtvisible c_englishmt) False) % 5.84/6.01 (Eq % 5.84/6.01 (prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) % 5.84/6.01 s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege) % 5.84/6.01 True) % 5.84/6.01 Clause #141 (by clausification #[33]): Eq % 5.84/6.01 (Exists fun X => % 5.84/6.01 mtvisible c_englishmt → prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) X) % 5.84/6.01 False % 5.84/6.01 Clause #142 (by clausification #[141]): ∀ (a : Iota), % 5.84/6.01 Eq % 5.84/6.01 (mtvisible c_englishmt → % 5.84/6.01 prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) a) % 5.84/6.01 False % 5.84/6.01 Clause #143 (by clausification #[142]): Eq (mtvisible c_englishmt) True % 5.84/6.01 Clause #144 (by clausification #[142]): ∀ (a : Iota), Eq (prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) a) False % 5.84/6.01 Clause #145 (by backward demodulation #[143, 45]): Or (Eq True False) % 5.84/6.01 (Eq % 5.84/6.01 (prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) % 5.84/6.01 s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege) % 5.84/6.01 True) % 5.84/6.01 Clause #146 (by clausification #[145]): Eq % 5.84/6.01 (prettystring (f_instancewithrelationtofn c_footballteam c_affiliatedwith c_beloitcollege) % 5.84/6.01 s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege) % 5.84/6.01 True % 5.84/6.01 Clause #147 (by superposition #[146, 144]): Eq True False % 5.84/6.01 Clause #150 (by clausification #[147]): False % 5.84/6.01 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------