The cat is not red. The cat likes the cow. The cat likes the mouse. The cat needs the mouse. The cat visits the mouse. The cow does not like the tiger. The cow visits the cat. The cow visits the mouse. The mouse likes the cat. The mouse likes the cow. The mouse needs the cat. The tiger is rough. The tiger likes the mouse. The tiger needs the cat. The tiger visits the cow. The tiger visits the mouse. If something needs the mouse then it does not visit the cow. If the tiger visits the cow then the tiger visits the mouse.
The cat is not red.
("cat" "is" "red" "-")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cow does not like the tiger.
("cow" "likes" "tiger" "-")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something needs the mouse then it does not visit the cow.
((("something" "needs" "mouse" "+")) -> ("something" "visits" "cow" "-"))
If the tiger visits the cow then the tiger visits the mouse.
((("tiger" "visits" "cow" "+")) -> ("tiger" "visits" "mouse" "+"))
The mouse likes the cat.
True
1
proof
[(triple9)]
("mouse" "likes" "cat" "+")
triple9
The tiger does not visit the cow.
False
1
inv-proof
[(triple15)]
("tiger" "visits" "cow" "-")
triple15
The cat does not visit the cow.
True
2
proof
[(((triple4) -> rule1))]
("cat" "visits" "cow" "-")
((triple4) -> (rule1 % int1))
The cat does not visit the cow.
("cat" "visits" "cow" "-")
int1
The cat visits the cow.
False
2
inv-proof
[(((triple4) -> rule1))]
("cat" "visits" "cow" "+")
((triple4) -> (rule1 % int1))
The cat does not visit the cow.
("cat" "visits" "cow" "-")
int1
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The cat is not red.[(triple1)] The cat likes the cow.[(triple2)] The cat likes the mouse.[(triple3)] The cat needs the mouse.[(triple4)] The cat visits the mouse.[(triple5)] The cow does not like the tiger.[(triple6)] The cow visits the cat.[(triple7)] The cow visits the mouse.[(triple8)] The mouse likes the cat.[(triple9)] The mouse likes the cow.[(triple10)] The mouse needs the cat.[(triple11)] The tiger is rough.[(triple12)] The tiger likes the mouse.[(triple13)] The tiger needs the cat.[(triple14)] The tiger visits the cow.[(triple15)] The tiger visits the mouse.[(triple16 OR ((triple15) -> rule2))] @1: The cat does not visit the cow.[(((triple4) -> rule1))]
The cat is not red.
("cat" "is" "red" "-")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
The cow does not like the tiger.
("cow" "likes" "tiger" "-")
triple6
The cow visits the cat.
("cow" "visits" "cat" "+")
triple7
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple8
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple9
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple10
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple13
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
((triple15) -> (rule2 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The cat does not visit the cow.
("cat" "visits" "cow" "-")
((triple4) -> (rule1 % int1))
The cat does not visit the cow.
("cat" "visits" "cow" "-")
int1