The cat needs the rabbit. The mouse is kind. The rabbit needs the mouse. If someone needs the mouse then they do not chase the rabbit. If someone is cold and kind then they do not see the rabbit. If someone needs the mouse then the mouse needs the cat. If the rabbit chases the mouse then the mouse sees the cat. If someone chases the rabbit and they are not rough then the rabbit is round. If the cat is cold and the cat sees the rabbit then the cat is blue.
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If someone needs the mouse then they do not chase the rabbit.
((("someone" "needs" "mouse" "+")) -> ("someone" "chases" "rabbit" "-"))
If someone is cold and kind then they do not see the rabbit.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone needs the mouse then the mouse needs the cat.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If the rabbit chases the mouse then the mouse sees the cat.
((("rabbit" "chases" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone chases the rabbit and they are not rough then the rabbit is round.
((("someone" "chases" "rabbit" "+") ("someone" "is" "rough" "~")) -> ("rabbit" "is" "round" "+"))
If the cat is cold and the cat sees the rabbit then the cat is blue.
((("cat" "is" "cold" "+") ("cat" "sees" "rabbit" "+")) -> ("cat" "is" "blue" "+"))
The cat needs the rabbit.
True
1
proof
[(triple1)]
("cat" "needs" "rabbit" "+")
triple1
The mouse is not kind.
False
1
inv-proof
[(triple2)]
("mouse" "is" "kind" "-")
triple2
The rabbit does not chase the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1
The mouse does not need the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "needs" "cat" "-")
((triple3) -> (rule3 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "blue" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "round" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cat needs the rabbit.[(triple1)] The mouse is kind.[(triple2)] The rabbit needs the mouse.[(triple3)] @1: The mouse needs the cat.[(((triple3) -> rule3))] The rabbit does not chase the rabbit.[(((triple3) -> rule1))]
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple3
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple3) -> (rule3 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1