The cat chases the mouse. The cat is big. The cat is green. The cat is red. The cat needs the mouse. The cat needs the rabbit. The cat sees the mouse. The mouse chases the cat. The mouse chases the rabbit. The mouse is big. The mouse is cold. The mouse needs the cat. The mouse sees the cat. The rabbit is green. The rabbit needs the mouse. If the cat sees the mouse and the mouse is round then the cat chases the rabbit. If someone needs the mouse then the mouse is red.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If the cat sees the mouse and the mouse is round then the cat chases the rabbit.
((("cat" "sees" "mouse" "+") ("mouse" "is" "round" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone needs the mouse then the mouse is red.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The cat chases the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "+")
triple1
The rabbit does not need the mouse.
False
1
inv-proof
[(triple15)]
("rabbit" "needs" "mouse" "-")
triple15
The cat does not chase the rabbit.
Unknown
inv-rconc
[@1: The cat chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "rabbit" "-")
The rabbit chases the mouse.
Unknown
random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "+")
@0: The cat chases the mouse.[(triple1)] The cat is big.[(triple2)] The cat is green.[(triple3)] The cat is red.[(triple4)] The cat needs the mouse.[(triple5)] The cat needs the rabbit.[(triple6)] The cat sees the mouse.[(triple7)] The mouse chases the cat.[(triple8)] The mouse chases the rabbit.[(triple9)] The mouse is big.[(triple10)] The mouse is cold.[(triple11)] The mouse needs the cat.[(triple12)] The mouse sees the cat.[(triple13)] The rabbit is green.[(triple14)] The rabbit needs the mouse.[(triple15)] @1: The mouse is red.[(((triple15) -> rule2) OR ((triple5) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple13
The rabbit is green.
("rabbit" "is" "green" "+")
triple14
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple15
The mouse is red.
("mouse" "is" "red" "+")
((triple15) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((triple5) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1