The cat is kind. The cat is red. The cat likes the lion. The cat sees the dog. The cat sees the mouse. The dog is young. The dog does not see the lion. The lion needs the mouse. The lion sees the mouse. The mouse is blue. The mouse is red. The mouse needs the dog. If someone likes the dog then they do not need the lion. If someone sees the mouse then the mouse likes the dog. If someone needs the mouse and they see the lion then they see the mouse.
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The dog is young.
("dog" "is" "young" "+")
The dog does not see the lion.
("dog" "sees" "lion" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If someone likes the dog then they do not need the lion.
((("someone" "likes" "dog" "+")) -> ("someone" "needs" "lion" "-"))
If someone sees the mouse then the mouse likes the dog.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If someone needs the mouse and they see the lion then they see the mouse.
((("someone" "needs" "mouse" "+") ("someone" "sees" "lion" "+")) -> ("someone" "sees" "mouse" "+"))
The mouse is blue.
True
1
proof
[(triple10)]
("mouse" "is" "blue" "+")
triple10
The dog sees the lion.
False
1
inv-proof
[(triple7)]
("dog" "sees" "lion" "+")
triple7
The mouse likes the dog.
True
2
proof
[(((triple5) -> rule2) OR ((triple9) -> rule2))]
("mouse" "likes" "dog" "+")
((triple5) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse does not like the dog.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple9) -> rule2))]
("mouse" "likes" "dog" "-")
((triple5) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse does not need the lion.
True
3
proof
[(((((triple5) -> rule2)) -> rule1) OR ((((triple9) -> rule2)) -> rule1))]
("mouse" "needs" "lion" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse needs the lion.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1) OR ((((triple9) -> rule2)) -> rule1))]
("mouse" "needs" "lion" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The dog does not see the mouse.
Unknown
inv-rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cat is kind.[(triple1)] The cat is red.[(triple2)] The cat likes the lion.[(triple3)] The cat sees the dog.[(triple4)] The cat sees the mouse.[(triple5)] The dog does not see the lion.[(triple7)] The dog is young.[(triple6)] The lion needs the mouse.[(triple8)] The lion sees the mouse.[(triple9)] The mouse is blue.[(triple10)] The mouse is red.[(triple11)] The mouse needs the dog.[(triple12)] @1: The mouse likes the dog.[(((triple5) -> rule2) OR ((triple9) -> rule2))] @2: The mouse does not need the lion.[(((((triple5) -> rule2)) -> rule1) OR ((((triple9) -> rule2)) -> rule1))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The dog does not see the lion.
("dog" "sees" "lion" "-")
triple7
The dog is young.
("dog" "is" "young" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple8
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is red.
("mouse" "is" "red" "+")
triple11
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple12
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((triple5) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
((triple9) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2