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