The mouse visits the squirrel. The squirrel eats the mouse. If someone is nice then they are rough. If someone is green and not red then they do not visit the mouse. If someone eats the squirrel then they do not visit the mouse. If someone is rough then they eat the squirrel. If someone is nice and they eat the mouse then the mouse is nice. If someone eats the mouse then the mouse is rough.
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and not red then they do not visit the mouse.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "visits" "mouse" "-"))
If someone eats the squirrel then they do not visit the mouse.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "mouse" "-"))
If someone is rough then they eat the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is nice and they eat the mouse then the mouse is nice.
((("someone" "is" "nice" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If someone eats the mouse then the mouse is rough.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
The mouse visits the squirrel.
True
1
proof
[(triple1)]
("mouse" "visits" "squirrel" "+")
triple1
The mouse does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("mouse" "visits" "squirrel" "-")
triple1
The mouse is rough.
True
2
proof
[(((triple2) -> rule6))]
("mouse" "is" "rough" "+")
((triple2) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple2) -> rule6))]
("mouse" "is" "rough" "-")
((triple2) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse eats the squirrel.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("mouse" "eats" "squirrel" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not eat the squirrel.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("mouse" "eats" "squirrel" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not visit the mouse.
True
4
proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("mouse" "visits" "mouse" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse visits the mouse.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("mouse" "visits" "mouse" "+")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "rough" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The mouse does not chase the squirrel.
Unknown
inv-random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The mouse visits the squirrel.[(triple1)] The squirrel eats the mouse.[(triple2)] @1: The mouse is rough.[(((triple2) -> rule6))] @2: The mouse eats the squirrel.[(((((triple2) -> rule6)) -> rule4))] @3: The mouse does not visit the mouse.[(((((((triple2) -> rule6)) -> rule4)) -> rule3))]
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
((triple2) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3