The cat does not see the mouse. The mouse eats the cat. The mouse is blue. If the mouse is rough and the cat does not chase the mouse then the cat sees the mouse. If something chases the cat and the cat does not chase the mouse then the cat sees the mouse. If something is blue then it does not eat the mouse. If something eats the cat and it eats the mouse then the mouse is young. If something eats the mouse and it sees the cat then the mouse is blue. If something is kind then it sees the cat.
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
If the mouse is rough and the cat does not chase the mouse then the cat sees the mouse.
((("mouse" "is" "rough" "+") ("cat" "chases" "mouse" "~")) -> ("cat" "sees" "mouse" "+"))
If something chases the cat and the cat does not chase the mouse then the cat sees the mouse.
((("something" "chases" "cat" "+") ("cat" "chases" "mouse" "~")) -> ("cat" "sees" "mouse" "+"))
If something is blue then it does not eat the mouse.
((("something" "is" "blue" "+")) -> ("something" "eats" "mouse" "-"))
If something eats the cat and it eats the mouse then the mouse is young.
((("something" "eats" "cat" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something eats the mouse and it sees the cat then the mouse is blue.
((("something" "eats" "mouse" "+") ("something" "sees" "cat" "+")) -> ("mouse" "is" "blue" "+"))
If something is kind then it sees the cat.
((("something" "is" "kind" "+")) -> ("something" "sees" "cat" "+"))
The cat does not see the mouse.
True
1
proof
[(triple1)]
("cat" "sees" "mouse" "-")
triple1
The cat sees the mouse.
False
1
inv-proof
[(triple1)]
("cat" "sees" "mouse" "+")
triple1
The mouse does not eat the mouse.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "eats" "mouse" "-")
((triple3) -> (rule3 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse eats the mouse.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "eats" "mouse" "+")
((triple3) -> (rule3 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "young" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat does not see the mouse.[(triple1)] The mouse eats the cat.[(triple2)] The mouse is blue.[(triple3)] @1: The mouse does not eat the mouse.[(((triple3) -> rule3))]
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
triple1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
((triple3) -> (rule3 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1