%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR027+1 : TPTP v9.2.0. Released v3.4.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:46:03 PM UTC 2025 % Result : Theorem 5.59s 5.76s % Output : Proof 5.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : CSR027+1 : TPTP v9.2.0. Released v3.4.0. % 0.03/0.12 % Command : duper %s % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 19:57:08 EDT 2025 % 0.12/0.34 % CPUTime : % 5.59/5.76 SZS status Theorem for theBenchmark.p % 5.59/5.76 SZS output start Proof for theBenchmark.p % 5.59/5.76 Clause #0 (by assumption #[]): Eq % 5.59/5.76 (∀ (TERM INDEPCOL PRED DEPCOL : Iota), % 5.59/5.76 And (isa TERM INDEPCOL) (relationallexists PRED INDEPCOL DEPCOL) → % 5.59/5.76 isa (f_relationallexistsfn TERM PRED INDEPCOL DEPCOL) DEPCOL) % 5.59/5.76 True % 5.59/5.76 Clause #8 (by assumption #[]): Eq (genlmt c_tptp_spindlecollectormt c_tptp_member2610_mt) True % 5.59/5.76 Clause #11 (by assumption #[]): Eq % 5.59/5.76 (∀ (TERM : Iota), % 5.59/5.76 And (mtvisible c_tptp_member2610_mt) % 5.59/5.76 (isa TERM % 5.59/5.76 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.76 c_movement_translationevent)) → % 5.59/5.76 tptp_8_875 TERM % 5.59/5.76 (f_relationallexistsfn TERM c_tptp_8_875 % 5.59/5.76 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.76 c_movement_translationevent) % 5.59/5.76 c_tptpcol_16_31868)) % 5.59/5.76 True % 5.59/5.76 Clause #12 (by assumption #[]): Eq % 5.59/5.76 (mtvisible c_tptp_member2610_mt → % 5.59/5.76 relationallexists c_tptp_8_875 % 5.59/5.76 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.76 c_movement_translationevent) % 5.59/5.76 c_tptpcol_16_31868) % 5.59/5.76 True % 5.59/5.76 Clause #13 (by assumption #[]): Eq % 5.59/5.76 (isa % 5.59/5.76 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.76 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.76 c_movement_translationevent)) % 5.59/5.76 True % 5.59/5.76 Clause #30 (by assumption #[]): Eq (∀ (X : Iota), isa X c_tptpcol_16_31868 → tptpcol_16_31868 X) True % 5.59/5.76 Clause #57 (by assumption #[]): Eq (∀ (SPECMT GENLMT : Iota), And (mtvisible SPECMT) (genlmt SPECMT GENLMT) → mtvisible GENLMT) True % 5.59/5.76 Clause #71 (by assumption #[]): Eq % 5.59/5.76 (Not % 5.59/5.76 (Exists fun X => % 5.59/5.76 mtvisible c_tptp_spindlecollectormt → % 5.59/5.76 And % 5.59/5.76 (tptp_8_875 % 5.59/5.76 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.76 X) % 5.59/5.76 (tptpcol_16_31868 X))) % 5.59/5.76 True % 5.59/5.76 Clause #72 (by clausification #[0]): ∀ (a : Iota), % 5.59/5.76 Eq % 5.59/5.76 (∀ (INDEPCOL PRED DEPCOL : Iota), % 5.59/5.76 And (isa a INDEPCOL) (relationallexists PRED INDEPCOL DEPCOL) → % 5.59/5.76 isa (f_relationallexistsfn a PRED INDEPCOL DEPCOL) DEPCOL) % 5.59/5.76 True % 5.59/5.76 Clause #73 (by clausification #[72]): ∀ (a a_1 : Iota), % 5.59/5.76 Eq % 5.59/5.76 (∀ (PRED DEPCOL : Iota), % 5.59/5.76 And (isa a a_1) (relationallexists PRED a_1 DEPCOL) → isa (f_relationallexistsfn a PRED a_1 DEPCOL) DEPCOL) % 5.59/5.76 True % 5.59/5.76 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), % 5.59/5.76 Eq % 5.59/5.76 (∀ (DEPCOL : Iota), % 5.59/5.76 And (isa a a_1) (relationallexists a_2 a_1 DEPCOL) → isa (f_relationallexistsfn a a_2 a_1 DEPCOL) DEPCOL) % 5.59/5.76 True % 5.59/5.76 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 : Iota), % 5.59/5.76 Eq (And (isa a a_1) (relationallexists a_2 a_1 a_3) → isa (f_relationallexistsfn a a_2 a_1 a_3) a_3) True % 5.59/5.76 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 5.59/5.76 Or (Eq (And (isa a a_1) (relationallexists a_2 a_1 a_3)) False) % 5.59/5.76 (Eq (isa (f_relationallexistsfn a a_2 a_1 a_3) a_3) True) % 5.59/5.76 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 : Iota), % 5.59/5.76 Or (Eq (isa (f_relationallexistsfn a a_1 a_2 a_3) a_3) True) % 5.59/5.76 (Or (Eq (isa a a_2) False) (Eq (relationallexists a_1 a_2 a_3) False)) % 5.59/5.76 Clause #78 (by clausification #[30]): ∀ (a : Iota), Eq (isa a c_tptpcol_16_31868 → tptpcol_16_31868 a) True % 5.59/5.76 Clause #79 (by clausification #[78]): ∀ (a : Iota), Or (Eq (isa a c_tptpcol_16_31868) False) (Eq (tptpcol_16_31868 a) True) % 5.59/5.76 Clause #84 (by clausification #[11]): ∀ (a : Iota), % 5.59/5.76 Eq % 5.59/5.76 (And (mtvisible c_tptp_member2610_mt) % 5.59/5.76 (isa a % 5.59/5.76 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.76 c_movement_translationevent)) → % 5.59/5.76 tptp_8_875 a % 5.59/5.76 (f_relationallexistsfn a c_tptp_8_875 % 5.59/5.76 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.76 c_movement_translationevent) % 5.59/5.76 c_tptpcol_16_31868)) % 5.59/5.77 True % 5.59/5.77 Clause #85 (by clausification #[84]): ∀ (a : Iota), % 5.59/5.77 Or % 5.59/5.77 (Eq % 5.59/5.77 (And (mtvisible c_tptp_member2610_mt) % 5.59/5.77 (isa a % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent))) % 5.59/5.77 False) % 5.59/5.77 (Eq % 5.59/5.77 (tptp_8_875 a % 5.59/5.77 (f_relationallexistsfn a c_tptp_8_875 % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent) % 5.59/5.77 c_tptpcol_16_31868)) % 5.59/5.77 True) % 5.59/5.77 Clause #86 (by clausification #[85]): ∀ (a : Iota), % 5.59/5.77 Or % 5.59/5.77 (Eq % 5.59/5.77 (tptp_8_875 a % 5.59/5.77 (f_relationallexistsfn a c_tptp_8_875 % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent) % 5.59/5.77 c_tptpcol_16_31868)) % 5.59/5.77 True) % 5.59/5.77 (Or (Eq (mtvisible c_tptp_member2610_mt) False) % 5.59/5.77 (Eq % 5.59/5.77 (isa a % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent)) % 5.59/5.77 False)) % 5.59/5.77 Clause #97 (by clausification #[12]): Or (Eq (mtvisible c_tptp_member2610_mt) False) % 5.59/5.77 (Eq % 5.59/5.77 (relationallexists c_tptp_8_875 % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent) % 5.59/5.77 c_tptpcol_16_31868) % 5.59/5.77 True) % 5.59/5.77 Clause #112 (by superposition #[13, 77]): ∀ (a a_1 : Iota), % 5.59/5.77 Or % 5.59/5.77 (Eq % 5.59/5.77 (isa % 5.59/5.77 (f_relationallexistsfn % 5.59/5.77 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.77 a % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent) % 5.59/5.77 a_1) % 5.59/5.77 a_1) % 5.59/5.77 True) % 5.59/5.77 (Or % 5.59/5.77 (Eq % 5.59/5.77 (relationallexists a % 5.59/5.77 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.77 c_movement_translationevent) % 5.59/5.77 a_1) % 5.59/5.77 False) % 5.59/5.77 (Eq False True)) % 5.59/5.77 Clause #185 (by clausification #[57]): ∀ (a : Iota), Eq (∀ (GENLMT : Iota), And (mtvisible a) (genlmt a GENLMT) → mtvisible GENLMT) True % 5.59/5.77 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), Eq (And (mtvisible a) (genlmt a a_1) → mtvisible a_1) True % 5.59/5.77 Clause #187 (by clausification #[186]): ∀ (a a_1 : Iota), Or (Eq (And (mtvisible a) (genlmt a a_1)) False) (Eq (mtvisible a_1) True) % 5.59/5.77 Clause #188 (by clausification #[187]): ∀ (a a_1 : Iota), Or (Eq (mtvisible a) True) (Or (Eq (mtvisible a_1) False) (Eq (genlmt a_1 a) False)) % 5.59/5.77 Clause #422 (by clausification #[71]): Eq % 5.59/5.77 (Exists fun X => % 5.59/5.77 mtvisible c_tptp_spindlecollectormt → % 5.59/5.77 And % 5.59/5.77 (tptp_8_875 % 5.59/5.77 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.77 X) % 5.59/5.77 (tptpcol_16_31868 X)) % 5.59/5.77 False % 5.59/5.77 Clause #423 (by clausification #[422]): ∀ (a : Iota), % 5.59/5.77 Eq % 5.59/5.77 (mtvisible c_tptp_spindlecollectormt → % 5.59/5.77 And % 5.59/5.77 (tptp_8_875 % 5.59/5.77 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.77 a) % 5.59/5.77 (tptpcol_16_31868 a)) % 5.59/5.77 False % 5.59/5.77 Clause #424 (by clausification #[423]): Eq (mtvisible c_tptp_spindlecollectormt) True % 5.59/5.77 Clause #425 (by clausification #[423]): ∀ (a : Iota), % 5.59/5.77 Eq % 5.59/5.77 (And % 5.59/5.77 (tptp_8_875 % 5.59/5.77 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.77 a) % 5.59/5.77 (tptpcol_16_31868 a)) % 5.59/5.77 False % 5.59/5.77 Clause #426 (by superposition #[424, 188]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Or (Eq True False) (Eq (genlmt c_tptp_spindlecollectormt a) False)) % 5.59/5.77 Clause #427 (by clausification #[425]): ∀ (a : Iota), % 5.59/5.77 Or % 5.59/5.77 (Eq % 5.59/5.77 (tptp_8_875 % 5.59/5.77 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.77 a) % 5.59/5.77 False) % 5.59/5.78 (Eq (tptpcol_16_31868 a) False) % 5.59/5.78 Clause #428 (by clausification #[426]): ∀ (a : Iota), Or (Eq (mtvisible a) True) (Eq (genlmt c_tptp_spindlecollectormt a) False) % 5.59/5.78 Clause #430 (by superposition #[428, 8]): Or (Eq (mtvisible c_tptp_member2610_mt) True) (Eq False True) % 5.59/5.78 Clause #432 (by clausification #[430]): Eq (mtvisible c_tptp_member2610_mt) True % 5.59/5.78 Clause #433 (by backward demodulation #[432, 86]): ∀ (a : Iota), % 5.59/5.78 Or % 5.59/5.78 (Eq % 5.59/5.78 (tptp_8_875 a % 5.59/5.78 (f_relationallexistsfn a c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 c_tptpcol_16_31868)) % 5.59/5.78 True) % 5.59/5.78 (Or (Eq True False) % 5.59/5.78 (Eq % 5.59/5.78 (isa a % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent)) % 5.59/5.78 False)) % 5.59/5.78 Clause #434 (by backward demodulation #[432, 97]): Or (Eq True False) % 5.59/5.78 (Eq % 5.59/5.78 (relationallexists c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 c_tptpcol_16_31868) % 5.59/5.78 True) % 5.59/5.78 Clause #449 (by clausification #[112]): ∀ (a a_1 : Iota), % 5.59/5.78 Or % 5.59/5.78 (Eq % 5.59/5.78 (isa % 5.59/5.78 (f_relationallexistsfn % 5.59/5.78 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.78 a % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 a_1) % 5.59/5.78 a_1) % 5.59/5.78 True) % 5.59/5.78 (Eq % 5.59/5.78 (relationallexists a % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 a_1) % 5.59/5.78 False) % 5.59/5.78 Clause #504 (by clausification #[434]): Eq % 5.59/5.78 (relationallexists c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 c_tptpcol_16_31868) % 5.59/5.78 True % 5.59/5.78 Clause #505 (by superposition #[504, 449]): Or % 5.59/5.78 (Eq % 5.59/5.78 (isa % 5.59/5.78 (f_relationallexistsfn % 5.59/5.78 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.78 c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 c_tptpcol_16_31868) % 5.59/5.78 c_tptpcol_16_31868) % 5.59/5.78 True) % 5.59/5.78 (Eq True False) % 5.59/5.78 Clause #512 (by clausification #[433]): ∀ (a : Iota), % 5.59/5.78 Or % 5.59/5.78 (Eq % 5.59/5.78 (tptp_8_875 a % 5.59/5.78 (f_relationallexistsfn a c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 c_tptpcol_16_31868)) % 5.59/5.78 True) % 5.59/5.78 (Eq % 5.59/5.78 (isa a % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent)) % 5.59/5.78 False) % 5.59/5.78 Clause #513 (by superposition #[512, 13]): Or % 5.59/5.78 (Eq % 5.59/5.78 (tptp_8_875 % 5.59/5.78 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.78 (f_relationallexistsfn % 5.59/5.78 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.78 c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.78 c_movement_translationevent) % 5.59/5.78 c_tptpcol_16_31868)) % 5.59/5.78 True) % 5.59/5.78 (Eq False True) % 5.59/5.78 Clause #520 (by clausification #[513]): Eq % 5.59/5.78 (tptp_8_875 % 5.59/5.78 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.78 (f_relationallexistsfn % 5.59/5.78 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.78 c_tptp_8_875 % 5.59/5.78 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.79 c_movement_translationevent) % 5.59/5.79 c_tptpcol_16_31868)) % 5.59/5.79 True % 5.59/5.79 Clause #521 (by superposition #[520, 427]): Or (Eq True False) % 5.59/5.79 (Eq % 5.59/5.79 (tptpcol_16_31868 % 5.59/5.79 (f_relationallexistsfn % 5.59/5.79 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.79 c_tptp_8_875 % 5.59/5.79 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.79 c_movement_translationevent) % 5.59/5.79 c_tptpcol_16_31868)) % 5.59/5.79 False) % 5.59/5.79 Clause #525 (by clausification #[521]): Eq % 5.59/5.79 (tptpcol_16_31868 % 5.59/5.79 (f_relationallexistsfn % 5.59/5.79 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.79 c_tptp_8_875 % 5.59/5.79 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.79 c_movement_translationevent) % 5.59/5.79 c_tptpcol_16_31868)) % 5.59/5.79 False % 5.59/5.79 Clause #526 (by clausification #[505]): Eq % 5.59/5.79 (isa % 5.59/5.79 (f_relationallexistsfn % 5.59/5.79 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.79 c_tptp_8_875 % 5.59/5.79 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.79 c_movement_translationevent) % 5.59/5.79 c_tptpcol_16_31868) % 5.59/5.79 c_tptpcol_16_31868) % 5.59/5.79 True % 5.59/5.79 Clause #527 (by superposition #[526, 79]): Or (Eq True False) % 5.59/5.79 (Eq % 5.59/5.79 (tptpcol_16_31868 % 5.59/5.79 (f_relationallexistsfn % 5.59/5.79 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.79 c_tptp_8_875 % 5.59/5.79 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.79 c_movement_translationevent) % 5.59/5.79 c_tptpcol_16_31868)) % 5.59/5.79 True) % 5.59/5.79 Clause #531 (by clausification #[527]): Eq % 5.59/5.79 (tptpcol_16_31868 % 5.59/5.79 (f_relationallexistsfn % 5.59/5.79 c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 % 5.59/5.79 c_tptp_8_875 % 5.59/5.79 (f_subcollectionofwithrelationfromtypefn c_unitvectorinterval c_directionoftranslation_throughout % 5.59/5.79 c_movement_translationevent) % 5.59/5.79 c_tptpcol_16_31868)) % 5.59/5.79 True % 5.59/5.79 Clause #532 (by superposition #[531, 525]): Eq True False % 5.59/5.79 Clause #534 (by clausification #[532]): False % 5.59/5.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------