%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : CAT020-2 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n017.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 : 600s % DateTime : Fri Jul 15 00:04:37 EDT 2022 % Result : Satisfiable 0.18s 0.48s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CAT020-2 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sun May 29 18:40:54 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.48 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.48 % 0.18/0.48 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.48 |- codomain (domain $X) = domain $X % 0.18/0.48 |- domain (codomain $X) = codomain $X % 0.18/0.48 |- compose (domain $X) $X = $X % 0.18/0.48 |- compose $X (codomain $X) = $X % 0.18/0.48 |- ~(codomain $X = domain $Y) \/ domain (compose $X $Y) = domain $X % 0.18/0.48 |- ~(codomain $X = domain $Y) \/ codomain (compose $X $Y) = codomain $Y % 0.18/0.48 |- ~(codomain $X = domain $Y) \/ ~(codomain $Y = domain $Z) \/ % 0.18/0.48 compose $X (compose $Y $Z) = compose (compose $X $Y) $Z % 0.18/0.48 |- ~(codomain $Z = domain $Z) \/ % 0.18/0.48 compose $Z (compose $Z $Z) = compose (compose $Z $Z) $Z % 0.18/0.48 |- compose (codomain $_2) (codomain $_2) = codomain $_2 % 0.18/0.48 |- codomain (codomain $_2) = codomain $_2 % 0.18/0.48 |- domain (domain $X) = domain $X % 0.18/0.48 |- compose (domain $X) (domain $X) = domain $X % 0.18/0.48 |- ~(codomain $_2 = domain $_10) \/ % 0.18/0.48 domain (compose (codomain $_2) $_10) = codomain $_2 % 0.18/0.48 |- ~(domain $X = domain $_10) \/ % 0.18/0.48 domain (compose (domain $X) $_10) = domain $X % 0.18/0.48 |- ~(codomain $_9 = codomain $X) \/ % 0.18/0.48 domain (compose $_9 (codomain $X)) = domain $_9 % 0.18/0.48 |- ~(codomain $_9 = domain $X) \/ % 0.18/0.48 domain (compose $_9 (domain $X)) = domain $_9 % 0.18/0.48 |- ~(codomain $_2 = domain $_12) \/ % 0.18/0.48 codomain (compose (codomain $_2) $_12) = codomain $_12 % 0.18/0.48 |- ~(domain $X = domain $_12) \/ % 0.18/0.48 codomain (compose (domain $X) $_12) = codomain $_12 % 0.18/0.48 |- ~(codomain $_11 = codomain $X) \/ % 0.18/0.48 codomain (compose $_11 (codomain $X)) = codomain $X % 0.18/0.48 |- ~(codomain $_11 = domain $X) \/ % 0.18/0.48 codomain (compose $_11 (domain $X)) = domain $X % 0.18/0.48 |- ~(domain $_15 = codomain $X) \/ % 0.18/0.48 domain (compose (domain $_15) (codomain $X)) = domain $_15 % 0.18/0.48 |- ~(domain $_15 = domain $X) \/ % 0.18/0.48 domain (compose (domain $_15) (domain $X)) = domain $_15 % 0.18/0.48 |- ~(codomain $_2 = domain $_19) \/ % 0.18/0.48 domain (compose (codomain $_2) (domain $_19)) = codomain $_2 % 0.18/0.48 |- ~(domain $_23 = codomain $X) \/ % 0.18/0.48 codomain (compose (domain $_23) (codomain $X)) = codomain $X % 0.18/0.48 |- ~(domain $_23 = domain $X) \/ % 0.18/0.48 codomain (compose (domain $_23) (domain $X)) = domain $X % 0.18/0.48 |- ~(codomain $_2 = domain $_27) \/ % 0.18/0.48 codomain (compose (codomain $_2) (domain $_27)) = domain $_27 % 0.18/0.48 |- ~(codomain $_34 = codomain $X) \/ % 0.18/0.48 domain (compose (codomain $_34) (codomain $X)) = codomain $_34 % 0.18/0.48 |- ~(codomain $_39 = codomain $X) \/ % 0.18/0.48 codomain (compose (codomain $_39) (codomain $X)) = codomain $X % 0.18/0.48 |- ~(codomain $_2 = domain $_47) \/ ~(codomain $_45 = codomain $_2) \/ % 0.18/0.48 compose $_45 (compose (codomain $_2) $_47) = % 0.18/0.48 compose (compose $_45 (codomain $_2)) $_47 % 0.18/0.48 |- ~(codomain $_45 = domain $X) \/ ~(domain $X = domain $_47) \/ % 0.18/0.48 compose $_45 (compose (domain $X) $_47) = % 0.18/0.48 compose (compose $_45 (domain $X)) $_47 % 0.18/0.48 |- ~(codomain $_45 = domain $_46) \/ ~(codomain $_46 = codomain $X) \/ % 0.18/0.48 compose $_45 (compose $_46 (codomain $X)) = % 0.18/0.48 compose (compose $_45 $_46) (codomain $X) % 0.18/0.48 |- ~(codomain $_45 = domain $_46) \/ ~(codomain $_46 = domain $X) \/ % 0.18/0.48 compose $_45 (compose $_46 (domain $X)) = % 0.18/0.48 compose (compose $_45 $_46) (domain $X) % 0.18/0.48 |- ~(codomain $_2 = domain $_46) \/ ~(codomain $_46 = domain $_47) \/ % 0.18/0.48 compose (codomain $_2) (compose $_46 $_47) = % 0.18/0.48 compose (compose (codomain $_2) $_46) $_47 % 0.18/0.48 |- ~(codomain $_46 = domain $_47) \/ ~(domain $X = domain $_46) \/ % 0.18/0.48 compose (domain $X) (compose $_46 $_47) = % 0.18/0.48 compose (compose (domain $X) $_46) $_47 % 0.18/0.48 |- ~(codomain $_2 = domain $_47) \/ % 0.18/0.48 compose $_2 (compose (codomain $_2) $_47) = compose $_2 $_47 % 0.18/0.48 |- ~(codomain $_45 = domain $_47) \/ % 0.18/0.48 compose $_45 $_47 = compose (compose $_45 (domain $_47)) $_47 % 0.18/0.48 |- ~(codomain $_45 = domain $X) \/ % 0.18/0.48 compose $_45 $X = compose (compose $_45 $X) (codomain $X) % 0.18/0.48 |- ~(codomain $_47 = domain $_47) \/ % 0.18/0.48 compose (codomain $_47) (compose $_47 $_47) = % 0.18/0.48 compose (compose (codomain $_47) $_47) $_47 % 0.18/0.48 |- ~(codomain $_46 = domain $_47) \/ % 0.18/0.48 compose (domain $_46) (compose $_46 $_47) = compose $_46 $_47 % 0.18/0.48 |- ~(domain $X = domain $_48) \/ % 0.18/0.48 compose (domain $X) $_48 = % 0.18/0.48 compose (compose (domain $X) $_48) (codomain $_48) % 0.18/0.48 |- ~(codomain $_49 = codomain $X) \/ % 0.18/0.48 compose $_49 (codomain $X) = % 0.18/0.48 compose (compose $_49 (codomain $X)) (codomain $X) % 0.18/0.48 |- ~(codomain $_49 = domain $X) \/ % 0.18/0.48 compose $_49 (domain $X) = % 0.18/0.48 compose (compose $_49 (domain $X)) (domain $X) % 0.18/0.48 |- ~(codomain $_2 = domain $_52) \/ % 0.18/0.48 compose (codomain $_2) (compose (codomain $_2) $_52) = % 0.18/0.48 compose (codomain $_2) $_52 % 0.18/0.48 |- ~(codomain $_51 = codomain $X) \/ % 0.18/0.48 compose $_51 (compose (codomain $_51) (codomain $X)) = % 0.18/0.48 compose $_51 (codomain $X) % 0.18/0.48 |- ~(codomain $_51 = domain $X) \/ % 0.18/0.48 compose $_51 (compose (codomain $_51) (domain $X)) = % 0.18/0.48 compose $_51 (domain $X) % 0.18/0.48 |- ~(codomain $_2 = domain $_54) \/ % 0.18/0.48 compose (codomain $_2) $_54 = % 0.18/0.48 compose (compose (codomain $_2) (domain $_54)) $_54 % 0.18/0.48 |- ~(domain $X = domain $_54) \/ % 0.18/0.48 compose (domain $X) $_54 = % 0.18/0.48 compose (compose (domain $X) (domain $_54)) $_54 % 0.18/0.48 |- ~(codomain $_55 = codomain $X) \/ % 0.18/0.48 compose (domain $_55) (compose $_55 (codomain $X)) = % 0.18/0.48 compose $_55 (codomain $X) % 0.18/0.48 |- ~(codomain $_55 = domain $X) \/ % 0.18/0.48 compose (domain $_55) (compose $_55 (domain $X)) = % 0.18/0.48 compose $_55 (domain $X) % 0.18/0.48 |- ~(codomain $X = domain $_58) \/ % 0.18/0.48 compose (codomain $X) $_58 = % 0.18/0.48 compose (compose (codomain $X) $_58) (codomain $_58) % 0.18/0.48 |- ~(domain $X = domain $_59) \/ % 0.18/0.48 compose (domain $X) (compose (domain $X) (domain $_59)) = % 0.18/0.48 compose (domain $X) (domain $_59) % 0.18/0.48 |- ~(codomain $_2 = domain $_67) \/ % 0.18/0.48 compose (codomain $_2) (domain $_67) = % 0.18/0.48 compose (compose (codomain $_2) (domain $_67)) (domain $_67) % 0.18/0.48 |- ~(domain $X = domain $_67) \/ % 0.18/0.48 compose (domain $X) (domain $_67) = % 0.18/0.48 compose (compose (domain $X) (domain $_67)) (domain $_67) % 0.18/0.48 |- ~(domain $X = domain $_70) \/ % 0.18/0.48 compose (domain $X) (compose (domain $X) $_70) = % 0.18/0.48 compose (domain $X) $_70 % 0.18/0.48 |- ~(codomain $_2 = domain $_75) \/ % 0.18/0.48 compose (codomain $_2) (compose (codomain $_2) (domain $_75)) = % 0.18/0.48 compose (codomain $_2) (domain $_75) % 0.18/0.48 |- ~(domain $_79 = codomain $X) \/ % 0.18/0.48 compose (domain $_79) (codomain $X) = % 0.18/0.48 compose (compose (domain $_79) (codomain $X)) (codomain $X) % 0.18/0.48 |- ~(codomain $_83 = codomain $X) \/ % 0.18/0.48 compose (codomain $_83) (compose (codomain $_83) (codomain $X)) = % 0.18/0.48 compose (codomain $_83) (codomain $X) % 0.18/0.48 |- ~(domain $X = codomain $_85) \/ % 0.18/0.48 compose (domain $X) (compose (domain $X) (codomain $_85)) = % 0.18/0.48 compose (domain $X) (codomain $_85) % 0.18/0.48 |- ~(codomain $X = codomain $_93) \/ % 0.18/0.48 compose (codomain $X) (codomain $_93) = % 0.18/0.48 compose (compose (codomain $X) (codomain $_93)) (codomain $_93) % 0.18/0.48 |- ~(codomain $_97 = domain $X) \/ % 0.18/0.48 compose (domain $X) (compose (codomain $_97) $X) = % 0.18/0.48 compose (compose (domain $X) (codomain $_97)) $X % 0.18/0.48 |- ~(codomain $_97 = codomain $_98) \/ % 0.18/0.48 compose $_98 (compose (codomain $_97) (codomain $_98)) = % 0.18/0.48 compose (compose $_98 (codomain $_97)) (codomain $_98) % 0.18/0.48 |- ~(domain $X = domain $_100) \/ % 0.18/0.48 compose (domain $_100) (compose (domain $X) $_100) = % 0.18/0.48 compose (compose (domain $_100) (domain $X)) $_100 % 0.18/0.48 |- ~(codomain $_101 = codomain $X) \/ % 0.18/0.48 compose (codomain $X) (compose (codomain $_101) (codomain $X)) = % 0.18/0.48 compose (compose (codomain $X) (codomain $_101)) (codomain $X) % 0.18/0.48 |- ~(codomain $_101 = domain $X) \/ % 0.18/0.48 compose (domain $X) (compose (codomain $_101) (domain $X)) = % 0.18/0.48 compose (compose (domain $X) (codomain $_101)) (domain $X) % 0.18/0.48 |- ~(domain $X = codomain $_103) \/ % 0.18/0.48 compose $_103 (compose (domain $X) (codomain $_103)) = % 0.18/0.48 compose (compose $_103 (domain $X)) (codomain $_103) % 0.18/0.48 |- ~(domain $X = domain $_110) \/ % 0.18/0.48 compose (domain $_110) (compose (domain $X) (domain $_110)) = % 0.18/0.48 compose (compose (domain $_110) (domain $X)) (domain $_110) % 0.18/0.48 |- ~(domain $_112 = codomain $X) \/ % 0.18/0.48 compose (codomain $X) (compose (domain $_112) (codomain $X)) = % 0.18/0.48 compose (compose (codomain $X) (domain $_112)) (codomain $X) % 0.18/0.48 |- ~(codomain $_117 = domain $_116) \/ ~(domain $_116 = codomain $X) \/ % 0.18/0.48 compose $_117 (compose (domain $_116) (codomain $X)) = % 0.18/0.48 compose (compose $_117 (domain $_116)) (codomain $X) % 0.18/0.48 |- ~(codomain $_117 = domain $_116) \/ ~(domain $_116 = domain $X) \/ % 0.18/0.48 compose $_117 (compose (domain $_116) (domain $X)) = % 0.18/0.48 compose (compose $_117 (domain $_116)) (domain $X) % 0.18/0.49 |- ~(codomain $_2 = domain $_116) \/ ~(domain $_116 = domain $_118) \/ % 0.18/0.49 compose (codomain $_2) (compose (domain $_116) $_118) = % 0.18/0.49 compose (compose (codomain $_2) (domain $_116)) $_118 % 0.18/0.49 |- ~(domain $X = domain $_116) \/ ~(domain $_116 = domain $_118) \/ % 0.18/0.49 compose (domain $X) (compose (domain $_116) $_118) = % 0.18/0.49 compose (compose (domain $X) (domain $_116)) $_118 % 0.18/0.49 |- ~(codomain $_120 = codomain $_2) \/ ~(codomain $_2 = codomain $_119) \/ % 0.18/0.49 compose $_120 (compose (codomain $_2) (codomain $_119)) = % 0.18/0.49 compose (compose $_120 (codomain $_2)) (codomain $_119) % 0.18/0.49 |- ~(codomain $_121 = codomain $_119) \/ ~(codomain $_2 = domain $_121) \/ % 0.18/0.49 compose (codomain $_2) (compose $_121 (codomain $_119)) = % 0.18/0.49 compose (compose (codomain $_2) $_121) (codomain $_119) % 0.18/0.49 |- ~(codomain $_123 = codomain $_2) \/ ~(codomain $_2 = domain $_122) \/ % 0.18/0.49 compose $_123 (compose (codomain $_2) (domain $_122)) = % 0.18/0.49 compose (compose $_123 (codomain $_2)) (domain $_122) % 0.18/0.49 |- ~(codomain $_124 = domain $_122) \/ ~(codomain $_2 = domain $_124) \/ % 0.18/0.49 compose (codomain $_2) (compose $_124 (domain $_122)) = % 0.18/0.49 compose (compose (codomain $_2) $_124) (domain $_122) % 0.18/0.49 |- ~(codomain $_124 = domain $_122) \/ ~(domain $X = domain $_124) \/ % 0.18/0.49 compose (domain $X) (compose $_124 (domain $_122)) = % 0.18/0.49 compose (compose (domain $X) $_124) (domain $_122) % 0.18/0.49 |- ~(codomain $_125 = codomain $_2) \/ ~(codomain $_2 = domain $_127) \/ % 0.18/0.49 compose (codomain $_125) (compose (codomain $_2) $_127) = % 0.18/0.49 compose (compose (codomain $_125) (codomain $_2)) $_127 % 0.18/0.49 |- ~(codomain $X = domain $_130) \/ ~(domain $_128 = codomain $X) \/ % 0.18/0.49 compose (domain $_128) (compose (codomain $X) $_130) = % 0.18/0.49 compose (compose (domain $_128) (codomain $X)) $_130 % 0.18/0.49 |- ~(codomain $_129 = codomain $X) \/ ~(domain $_128 = domain $_129) \/ % 0.18/0.49 compose (domain $_128) (compose $_129 (codomain $X)) = % 0.18/0.49 compose (compose (domain $_128) $_129) (codomain $X) % 0.18/0.49 |- ~(codomain $_2 = domain $_135) \/ ~(domain $_135 = domain $_134) \/ % 0.18/0.49 compose (codomain $_2) (compose (domain $_135) (domain $_134)) = % 0.18/0.49 compose (compose (codomain $_2) (domain $_135)) (domain $_134) % 0.18/0.49 |- ~(domain $X = domain $_135) \/ ~(domain $_135 = domain $_134) \/ % 0.18/0.49 compose (domain $X) (compose (domain $_135) (domain $_134)) = % 0.18/0.49 compose (compose (domain $X) (domain $_135)) (domain $_134) % 0.18/0.49 |- ~(domain $_140 = domain $_141) \/ ~(domain $_141 = codomain $X) \/ % 0.18/0.49 compose (domain $_140) (compose (domain $_141) (codomain $X)) = % 0.18/0.49 compose (compose (domain $_140) (domain $_141)) (codomain $X) % 0.18/0.49 |- ~(codomain $_145 = domain $_143) \/ ~(domain $X = codomain $_145) \/ % 0.18/0.49 compose (domain $X) (compose (codomain $_145) (domain $_143)) = % 0.18/0.49 compose (compose (domain $X) (codomain $_145)) (domain $_143) % 0.18/0.49 |- ~(codomain $_160 = codomain $_158) \/ % 0.18/0.49 ~(codomain $_2 = codomain $_160) \/ % 0.18/0.49 compose (codomain $_2) (compose (codomain $_160) (codomain $_158)) = % 0.18/0.49 compose (compose (codomain $_2) (codomain $_160)) (codomain $_158) % 0.18/0.49 |- ~(codomain $_160 = codomain $_158) \/ ~(domain $X = codomain $_160) \/ % 0.18/0.49 compose (domain $X) (compose (codomain $_160) (codomain $_158)) = % 0.18/0.49 compose (compose (domain $X) (codomain $_160)) (codomain $_158) % 0.18/0.49 |- ~(codomain $_163 = domain $X) \/ ~(domain $X = codomain $_161) \/ % 0.18/0.49 compose (codomain $_163) (compose (domain $X) (codomain $_161)) = % 0.18/0.49 compose (compose (codomain $_163) (domain $X)) (codomain $_161) % 0.18/0.49 |- ~(codomain $_164 = codomain $_166) \/ ~(codomain $_166 = domain $X) \/ % 0.18/0.49 compose (codomain $_164) (compose (codomain $_166) (domain $X)) = % 0.18/0.49 compose (compose (codomain $_164) (codomain $_166)) (domain $X) % 0.18/0.49 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.49 %------------------------------------------------------------------------------