The cat is rough. The mouse likes the squirrel. The squirrel does not eat the cat. If something likes the squirrel then it visits the mouse. If something visits the mouse then the mouse is green. If something is green and rough then it likes the squirrel.
The cat is rough.
("cat" "is" "rough" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
If something likes the squirrel then it visits the mouse.
((("something" "likes" "squirrel" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the mouse then the mouse is green.
((("something" "visits" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something is green and rough then it likes the squirrel.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "likes" "squirrel" "+"))
The cat is rough.
True
1
proof
[(triple1)]
("cat" "is" "rough" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The mouse visits the mouse.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "visits" "mouse" "-")
((triple2) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is green.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("mouse" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("mouse" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The cat does not like the squirrel.
Unknown
inv-rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "squirrel" "-")
The cat visits the mouse.
Unknown
rconc
[@2: The cat visits the mouse.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cat" "visits" "mouse" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The mouse visits the squirrel.
Unknown
random
[@0: The mouse visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "squirrel" "+")
@0: The cat is rough.[(triple1)] The mouse likes the squirrel.[(triple2)] The squirrel does not eat the cat.[(triple3)] @1: The mouse visits the mouse.[(((triple2) -> rule1))] @2: The mouse is green.[(((((triple2) -> rule1)) -> rule2))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
The squirrel does not eat the cat.
("squirrel" "eats" "cat" "-")
triple3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2