The cat is green. The cat is kind. The cat likes the mouse. The cat visits the mouse. The mouse likes the cat. The mouse needs the cat. The mouse visits the cat. If something visits the cat and the cat is nice then it visits the mouse. If something needs the mouse and the mouse is kind then the mouse is round. If something is kind and it likes the mouse then the mouse is round. If the cat visits the mouse then the cat is round. If something needs the cat and the cat likes the mouse then the cat needs the mouse. If the cat visits the mouse then the cat needs the mouse.
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something visits the cat and the cat is nice then it visits the mouse.
((("something" "visits" "cat" "+") ("cat" "is" "nice" "+")) -> ("something" "visits" "mouse" "+"))
If something needs the mouse and the mouse is kind then the mouse is round.
((("something" "needs" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "is" "round" "+"))
If something is kind and it likes the mouse then the mouse is round.
((("something" "is" "kind" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If the cat visits the mouse then the cat is round.
((("cat" "visits" "mouse" "+")) -> ("cat" "is" "round" "+"))
If something needs the cat and the cat likes the mouse then the cat needs the mouse.
((("something" "needs" "cat" "+") ("cat" "likes" "mouse" "+")) -> ("cat" "needs" "mouse" "+"))
If the cat visits the mouse then the cat needs the mouse.
((("cat" "visits" "mouse" "+")) -> ("cat" "needs" "mouse" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The mouse does not need the cat.
False
1
inv-proof
[(triple6)]
("mouse" "needs" "cat" "-")
triple6
The mouse is round.
True
3
proof
[(((triple2 triple3) -> rule3))]
("mouse" "is" "round" "+")
((triple2 triple3) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
3
inv-proof
[(((triple2 triple3) -> rule3))]
("mouse" "is" "round" "-")
((triple2 triple3) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat is green.[(triple1)] The cat is kind.[(triple2)] The cat likes the mouse.[(triple3)] The cat visits the mouse.[(triple4)] The mouse likes the cat.[(triple5)] The mouse needs the cat.[(triple6)] The mouse visits the cat.[(triple7)] @1: The cat is round.[(((triple4) -> rule4))] The cat needs the mouse.[(((triple4) -> rule6) OR ((triple6 triple3) -> rule5))] The mouse is round.[(((triple2 triple3) -> rule3))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple5
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple6
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple7
The cat is round.
("cat" "is" "round" "+")
((triple4) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((triple4) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
((triple6 triple3) -> (rule5 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple2 triple3) -> (rule3 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1