The cat is big. The cat is blue. The cat is kind. The cat is rough. The cat is young. The cat likes the tiger. The cat does not see the tiger. The cat does not visit the tiger. The tiger is big. The tiger is blue. The tiger is kind. The tiger is rough. The tiger is young. The tiger likes the cat. The tiger does not see the cat. The tiger visits the cat. If the cat likes the tiger and the tiger does not like the cat then the tiger sees the cat. If the tiger is big and the tiger visits the cat then the cat does not see the tiger.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the cat likes the tiger and the tiger does not like the cat then the tiger sees the cat.
((("cat" "likes" "tiger" "+") ("tiger" "likes" "cat" "~")) -> ("tiger" "sees" "cat" "+"))
If the tiger is big and the tiger visits the cat then the cat does not see the tiger.
((("tiger" "is" "big" "+") ("tiger" "visits" "cat" "+")) -> ("cat" "sees" "tiger" "-"))
The cat is young.
True
1
proof
[(triple5)]
("cat" "is" "young" "+")
triple5
The tiger is not big.
False
1
inv-proof
[(triple9)]
("tiger" "is" "big" "-")
triple9
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat does not see the tiger.[(triple7 OR ((triple9 triple16) -> rule2))] The cat does not visit the tiger.[(triple8)] The cat is big.[(triple1)] The cat is blue.[(triple2)] The cat is kind.[(triple3)] The cat is rough.[(triple4)] The cat is young.[(triple5)] The cat likes the tiger.[(triple6)] The tiger does not see the cat.[(triple15)] The tiger is big.[(triple9)] The tiger is blue.[(triple10)] The tiger is kind.[(triple11)] The tiger is rough.[(triple12)] The tiger is young.[(triple13)] The tiger likes the cat.[(triple14)] The tiger visits the cat.[(triple16)]
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple7
((triple9 triple16) -> (rule2 % int1))
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
int1
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
triple8
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple6
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
triple15
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple14
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16