The cat is big. The cat is blue. The cat is cold. The cat is rough. The cat is not young. If someone is rough and not blue then they are young. If someone is cold and blue then they are rough.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is not young.
("cat" "is" "young" "-")
If someone is rough and not blue then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "+"))
If someone is cold and blue then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The cat is young.
False
1
inv-proof
[(triple5)]
("cat" "is" "young" "+")
triple5
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is big.[(triple1)] The cat is blue.[(triple2)] The cat is cold.[(triple3)] The cat is not young.[(triple5)] The cat is rough.[(triple4 OR ((triple3 triple2) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is not young.
("cat" "is" "young" "-")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple3 triple2) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1