The mouse is round. The rabbit is round. The rabbit likes the mouse. The rabbit likes the squirrel. The rabbit visits the mouse. The squirrel eats the rabbit. The squirrel is kind. The squirrel is red. The squirrel is rough. The squirrel visits the mouse. If something is rough then it eats the mouse. If something eats the mouse and it is red then the mouse is rough.
The mouse is round.
("mouse" "is" "round" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something is rough then it eats the mouse.
((("something" "is" "rough" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the mouse and it is red then the mouse is rough.
((("something" "eats" "mouse" "+") ("something" "is" "red" "+")) -> ("mouse" "is" "rough" "+"))
The squirrel visits the mouse.
True
1
proof
[(triple10)]
("squirrel" "visits" "mouse" "+")
triple10
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "mouse" "-")
triple10
The squirrel eats the mouse.
True
2
proof
[(((triple9) -> rule1))]
("squirrel" "eats" "mouse" "+")
((triple9) -> (rule1 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel does not eat the mouse.
False
2
inv-proof
[(((triple9) -> rule1))]
("squirrel" "eats" "mouse" "-")
((triple9) -> (rule1 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse is rough.
True
4
proof
[(((((triple9) -> rule1) triple8) -> rule2))]
("mouse" "is" "rough" "+")
((((triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse is not rough.
False
4
inv-proof
[(((((triple9) -> rule1) triple8) -> rule2))]
("mouse" "is" "rough" "-")
((((triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The rabbit does not eat the mouse.
Unknown
inv-rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "mouse" "-")
The mouse likes the rabbit.
Unknown
random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The mouse is round.[(triple1)] The rabbit is round.[(triple2)] The rabbit likes the mouse.[(triple3)] The rabbit likes the squirrel.[(triple4)] The rabbit visits the mouse.[(triple5)] The squirrel eats the rabbit.[(triple6)] The squirrel is kind.[(triple7)] The squirrel is red.[(triple8)] The squirrel is rough.[(triple9)] The squirrel visits the mouse.[(triple10)] @1: The squirrel eats the mouse.[(((triple9) -> rule1))] @2: The mouse is rough.[(((((triple9) -> rule1) triple8) -> rule2))] @3: The mouse eats the mouse.[(((((((triple9) -> rule1) triple8) -> rule2)) -> rule1))]
The mouse is round.
("mouse" "is" "round" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
triple2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple3
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple4
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple5
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple10
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((triple9) -> (rule1 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((triple9) -> (rule1 % int3)) triple8) -> (rule2 % int2))) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3