The cat eats the mouse. The cat likes the cow. The cat likes the dog. The cat does not need the cow. The cow eats the dog. The cow is not blue. The cow needs the cat. The cow does not need the mouse. The dog is kind. The dog is nice. The dog needs the mouse. The mouse is not nice. The mouse likes the cat. The mouse needs the cow. The mouse needs the dog. If someone likes the cat then they like the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat does not need the cow.
("cat" "needs" "cow" "-")
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If someone likes the cat then they like the mouse.
((("someone" "likes" "cat" "+")) -> ("someone" "likes" "mouse" "+"))
The cat likes the cow.
True
1
proof
[(triple2)]
("cat" "likes" "cow" "+")
triple2
The mouse does not like the cat.
False
1
inv-proof
[(triple13)]
("mouse" "likes" "cat" "-")
triple13
The mouse likes the mouse.
True
2
proof
[(((triple13) -> rule1))]
("mouse" "likes" "mouse" "+")
((triple13) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple13) -> rule1))]
("mouse" "likes" "mouse" "-")
((triple13) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The cow does not like the mouse.
Unknown
inv-rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "mouse" "-")
The dog likes the mouse.
Unknown
rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "mouse" "+")
The dog does not need the cat.
Unknown
inv-random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cat does not need the cow.[(triple4)] The cat eats the mouse.[(triple1)] The cat likes the cow.[(triple2)] The cat likes the dog.[(triple3)] The cow does not need the mouse.[(triple8)] The cow eats the dog.[(triple5)] The cow is not blue.[(triple6)] The cow needs the cat.[(triple7)] The dog is kind.[(triple9)] The dog is nice.[(triple10)] The dog needs the mouse.[(triple11)] The mouse is not nice.[(triple12)] The mouse likes the cat.[(triple13)] The mouse needs the cow.[(triple14)] The mouse needs the dog.[(triple15)] @1: The mouse likes the mouse.[(((triple13) -> rule1))]
The cat does not need the cow.
("cat" "needs" "cow" "-")
triple4
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cat likes the dog.
("cat" "likes" "dog" "+")
triple3
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
triple8
The cow eats the dog.
("cow" "eats" "dog" "+")
triple5
The cow is not blue.
("cow" "is" "blue" "-")
triple6
The cow needs the cat.
("cow" "needs" "cat" "+")
triple7
The dog is kind.
("dog" "is" "kind" "+")
triple9
The dog is nice.
("dog" "is" "nice" "+")
triple10
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple11
The mouse is not nice.
("mouse" "is" "nice" "-")
triple12
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple13
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple14
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple15
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple13) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1