The cat does not need the rabbit. The mouse is nice. The rabbit visits the mouse. If something visits the mouse then it chases the mouse. If something chases the cat then the cat visits the rabbit. If the cat is nice then the cat does not visit the mouse. If the cat visits the rabbit then the rabbit needs the mouse. If the mouse is green then the mouse is kind. If the mouse needs the rabbit then the mouse is young. If something is young and it visits the rabbit then it does not visit the mouse. If the cat is green then the cat is blue.
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something visits the mouse then it chases the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the cat then the cat visits the rabbit.
((("something" "chases" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If the cat is nice then the cat does not visit the mouse.
((("cat" "is" "nice" "+")) -> ("cat" "visits" "mouse" "-"))
If the cat visits the rabbit then the rabbit needs the mouse.
((("cat" "visits" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If the mouse is green then the mouse is kind.
((("mouse" "is" "green" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse needs the rabbit then the mouse is young.
((("mouse" "needs" "rabbit" "+")) -> ("mouse" "is" "young" "+"))
If something is young and it visits the rabbit then it does not visit the mouse.
((("something" "is" "young" "+") ("something" "visits" "rabbit" "+")) -> ("something" "visits" "mouse" "-"))
If the cat is green then the cat is blue.
((("cat" "is" "green" "+")) -> ("cat" "is" "blue" "+"))
The mouse is nice.
True
1
proof
[(triple2)]
("mouse" "is" "nice" "+")
triple2
The cat needs the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "needs" "rabbit" "+")
triple1
The rabbit chases the mouse.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not chase the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "chases" "mouse" "-")
((triple3) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not need the mouse.
Unknown
inv-rconc
[@2: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "young" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The cat visits the mouse.
Unknown
random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "+")
@0: The cat does not need the rabbit.[(triple1)] The mouse is nice.[(triple2)] The rabbit visits the mouse.[(triple3)] @1: The rabbit chases the mouse.[(((triple3) -> rule1))]
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1