The cat likes the mouse. The mouse does not see the squirrel. The squirrel is rough. If someone likes the squirrel and the squirrel does not see the mouse then the squirrel does not like the mouse. If the squirrel sees the cat then the squirrel likes the mouse. If someone sees the mouse and the mouse sees the cat then they are not blue. If someone is rough then they eat the mouse. If someone eats the cat and the cat eats the mouse then they eat the mouse. If someone eats the mouse then the mouse eats the cat.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If someone likes the squirrel and the squirrel does not see the mouse then the squirrel does not like the mouse.
((("someone" "likes" "squirrel" "+") ("squirrel" "sees" "mouse" "~")) -> ("squirrel" "likes" "mouse" "-"))
If the squirrel sees the cat then the squirrel likes the mouse.
((("squirrel" "sees" "cat" "+")) -> ("squirrel" "likes" "mouse" "+"))
If someone sees the mouse and the mouse sees the cat then they are not blue.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("someone" "is" "blue" "-"))
If someone is rough then they eat the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the cat and the cat eats the mouse then they eat the mouse.
((("someone" "eats" "cat" "+") ("cat" "eats" "mouse" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the mouse then the mouse eats the cat.
((("someone" "eats" "mouse" "+")) -> ("mouse" "eats" "cat" "+"))
The cat likes the mouse.
True
1
proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The mouse sees the squirrel.
False
1
inv-proof
[(triple2)]
("mouse" "sees" "squirrel" "+")
triple2
The squirrel eats the mouse.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "eats" "mouse" "+")
((triple3) -> (rule4 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel does not eat the mouse.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "eats" "mouse" "-")
((triple3) -> (rule4 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the cat.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("mouse" "eats" "cat" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse does not eat the cat.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("mouse" "eats" "cat" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The squirrel does not like the mouse.
Unknown
inv-rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The mouse eats the mouse.
Unknown
rconc
[@2: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The cat does not eat the mouse.
Unknown
inv-rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "mouse" "-")
The mouse likes the squirrel.
Unknown
random
[@0: The mouse likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "squirrel" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
@0: The cat likes the mouse.[(triple1)] The mouse does not see the squirrel.[(triple2)] The squirrel is rough.[(triple3)] @1: The squirrel eats the mouse.[(((triple3) -> rule4))] @2: The mouse eats the cat.[(((((triple3) -> rule4)) -> rule6))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((triple3) -> (rule4 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2