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