No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 104-104 |
IOS 1 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 178-178 |
IOS 10 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 184-184 |
IOS 11 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 190-190 |
IOS 12 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 196-196 |
IOS 13 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 125-125 |
IOS 2 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 131-131 |
IOS 3 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 137-137 |
IOS 4 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 148-148 |
IOS 5 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 154-154 |
IOS 6 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 160-160 |
IOS 7 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 166-166 |
IOS 8 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 172-172 |
IOS 9 is a subclass of IOS |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 82-82 |
|
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 81-81 |
|
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 80-80 |
|
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 83-83 |
|