The cat is cold. The cat likes the rabbit. The cat needs the cow. The cat needs the mouse. The cow likes the cat. The cow likes the rabbit. The cow sees the rabbit. The mouse is big. The mouse likes the cat. The mouse sees the cow. The rabbit is kind. The rabbit is young. The rabbit likes the cat. The rabbit needs the cow. The rabbit sees the cat. The rabbit sees the cow. If the cat sees the cow then the cat likes the rabbit. If something is cold and it needs the mouse then the mouse sees the rabbit. If something is cold and it needs the cow then the cow sees the rabbit. If something likes the cow and the cow sees the cat then the cat sees the cow. If something needs the rabbit then it likes the cow. If something sees the mouse and it needs the cow then the cow sees the rabbit. If something needs the cow and it needs the mouse then it is red. If something likes the rabbit then the rabbit likes the cat.
The cat is cold.
("cat" "is" "cold" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If the cat sees the cow then the cat likes the rabbit.
((("cat" "sees" "cow" "+")) -> ("cat" "likes" "rabbit" "+"))
If something is cold and it needs the mouse then the mouse sees the rabbit.
((("something" "is" "cold" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If something is cold and it needs the cow then the cow sees the rabbit.
((("something" "is" "cold" "+") ("something" "needs" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
If something likes the cow and the cow sees the cat then the cat sees the cow.
((("something" "likes" "cow" "+") ("cow" "sees" "cat" "+")) -> ("cat" "sees" "cow" "+"))
If something needs the rabbit then it likes the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "likes" "cow" "+"))
If something sees the mouse and it needs the cow then the cow sees the rabbit.
((("something" "sees" "mouse" "+") ("something" "needs" "cow" "+")) -> ("cow" "sees" "rabbit" "+"))
If something needs the cow and it needs the mouse then it is red.
((("something" "needs" "cow" "+") ("something" "needs" "mouse" "+")) -> ("something" "is" "red" "+"))
If something likes the rabbit then the rabbit likes the cat.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "cat" "+"))
The rabbit is kind.
True
1
proof
[(triple11)]
("rabbit" "is" "kind" "+")
triple11
The rabbit does not need the cow.
False
1
inv-proof
[(triple14)]
("rabbit" "needs" "cow" "-")
triple14
The mouse sees the rabbit.
True
3
proof
[(((triple1 triple4) -> rule2))]
("mouse" "sees" "rabbit" "+")
((triple1 triple4) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The cat is not red.
False
3
inv-proof
[(((triple3 triple4) -> rule7))]
("cat" "is" "red" "-")
((triple3 triple4) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "red" "-")
The cat likes the cow.
Unknown
rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "cow" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
@0: The cat is cold.[(triple1)] The cat likes the rabbit.[(triple2)] The cat needs the cow.[(triple3)] The cat needs the mouse.[(triple4)] The cow likes the cat.[(triple5)] The cow likes the rabbit.[(triple6)] The cow sees the rabbit.[(triple7 OR ((triple1 triple3) -> rule3))] The mouse is big.[(triple8)] The mouse likes the cat.[(triple9)] The mouse sees the cow.[(triple10)] The rabbit is kind.[(triple11)] The rabbit is young.[(triple12)] The rabbit likes the cat.[(triple13 OR ((triple2) -> rule8) OR ((triple6) -> rule8))] The rabbit needs the cow.[(triple14)] The rabbit sees the cat.[(triple15)] The rabbit sees the cow.[(triple16)] @1: The cat is red.[(((triple3 triple4) -> rule7))] The mouse sees the rabbit.[(((triple1 triple4) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cow likes the cat.
("cow" "likes" "cat" "+")
triple5
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple6
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple7
((triple1 triple3) -> (rule3 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple9
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple13
((triple2) -> (rule8 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
((triple6) -> (rule8 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple14
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple15
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple16
The cat is red.
("cat" "is" "red" "+")
((triple3 triple4) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((triple1 triple4) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1