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