The cat chases the rabbit. The mouse is red. The rabbit likes the mouse. If something needs the cat and the cat likes the rabbit then it needs the rabbit. If something likes the mouse then it chases the mouse. If something likes the mouse then the mouse is cold. If something likes the rabbit and it likes the mouse then the mouse needs the cat. If something needs the cat and the cat likes the rabbit then the rabbit needs the cat. If something needs the mouse and the mouse is cold then the mouse likes the rabbit. If something chases the rabbit then the rabbit needs the mouse. If something needs the mouse then it chases the mouse.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something needs the cat and the cat likes the rabbit then it needs the rabbit.
((("something" "needs" "cat" "+") ("cat" "likes" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If something likes the mouse then it chases the mouse.
((("something" "likes" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something likes the mouse then the mouse is cold.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something likes the rabbit and it likes the mouse then the mouse needs the cat.
((("something" "likes" "rabbit" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If something needs the cat and the cat likes the rabbit then the rabbit needs the cat.
((("something" "needs" "cat" "+") ("cat" "likes" "rabbit" "+")) -> ("rabbit" "needs" "cat" "+"))
If something needs the mouse and the mouse is cold then the mouse likes the rabbit.
((("something" "needs" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something chases the rabbit then the rabbit needs the mouse.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something needs the mouse then it chases the mouse.
((("something" "needs" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
The rabbit likes the mouse.
True
1
proof
[(triple3)]
("rabbit" "likes" "mouse" "+")
triple3
The cat does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "chases" "rabbit" "-")
triple1
The rabbit needs the mouse.
True
2
proof
[(((triple1) -> rule7))]
("rabbit" "needs" "mouse" "+")
((triple1) -> (rule7 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "is" "cold" "-")
((triple3) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse likes the rabbit.
True
5
proof
[(((((triple1) -> rule7) ((triple3) -> rule3)) -> rule6))]
("mouse" "likes" "rabbit" "+")
((((triple1) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The mouse does not like the rabbit.
False
5
inv-proof
[(((((triple1) -> rule7) ((triple3) -> rule3)) -> rule6))]
("mouse" "likes" "rabbit" "-")
((((triple1) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3
The mouse does not need the rabbit.
Unknown
inv-rconc
[@1: The mouse needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "rabbit" "-")
The rabbit needs the cat.
Unknown
rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "needs" "cat" "+")
The cat does not need the rabbit.
Unknown
inv-rconc
[@1: The cat needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "rabbit" "-")
The rabbit chases the cat.
Unknown
random
[@0: The rabbit chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cat" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The cat chases the rabbit.[(triple1)] The mouse is red.[(triple2)] The rabbit likes the mouse.[(triple3)] @1: The mouse is cold.[(((triple3) -> rule3))] The rabbit chases the mouse.[(((triple3) -> rule2) OR ((((triple1) -> rule7)) -> rule8))] The rabbit needs the mouse.[(((triple1) -> rule7))] @2: The mouse likes the rabbit.[(((((triple1) -> rule7) ((triple3) -> rule3)) -> rule6))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
((triple3) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((triple1) -> (rule7 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple1) -> (rule7 % int3)) ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int3