The cow is kind. The cow is round. The cow does not see the mouse. The mouse is nice. The mouse likes the cow. The mouse sees the cow. The mouse sees the rabbit. The mouse sees the squirrel. The rabbit is not big. The rabbit is not round. The rabbit likes the mouse. The rabbit visits the mouse. The squirrel is kind. The squirrel is round. The squirrel does not see the cow. The squirrel visits the rabbit. If someone visits the rabbit then they visit the cow. If someone visits the cow then the cow likes the mouse. If someone is round and they see the rabbit then the rabbit sees the squirrel.
The cow is kind.
("cow" "is" "kind" "+")
The cow is round.
("cow" "is" "round" "+")
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone visits the rabbit then they visit the cow.
((("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cow then the cow likes the mouse.
((("someone" "visits" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
If someone is round and they see the rabbit then the rabbit sees the squirrel.
((("someone" "is" "round" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
The mouse sees the cow.
True
1
proof
[(triple6)]
("mouse" "sees" "cow" "+")
triple6
The mouse does not see the rabbit.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "rabbit" "-")
triple7
The squirrel visits the cow.
True
2
proof
[(((triple16) -> rule1))]
("squirrel" "visits" "cow" "+")
((triple16) -> (rule1 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel does not visit the cow.
False
2
inv-proof
[(((triple16) -> rule1))]
("squirrel" "visits" "cow" "-")
((triple16) -> (rule1 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The cow likes the mouse.
True
3
proof
[(((((triple16) -> rule1)) -> rule2))]
("cow" "likes" "mouse" "+")
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The cow does not like the mouse.
False
3
inv-proof
[(((((triple16) -> rule1)) -> rule2))]
("cow" "likes" "mouse" "-")
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "cow" "+")
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The cow does not see the squirrel.
Unknown
inv-random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cow does not see the mouse.[(triple3)] The cow is kind.[(triple1)] The cow is round.[(triple2)] The mouse is nice.[(triple4)] The mouse likes the cow.[(triple5)] The mouse sees the cow.[(triple6)] The mouse sees the rabbit.[(triple7)] The mouse sees the squirrel.[(triple8)] The rabbit is not big.[(triple9)] The rabbit is not round.[(triple10)] The rabbit likes the mouse.[(triple11)] The rabbit visits the mouse.[(triple12)] The squirrel does not see the cow.[(triple15)] The squirrel is kind.[(triple13)] The squirrel is round.[(triple14)] The squirrel visits the rabbit.[(triple16)] @1: The squirrel visits the cow.[(((triple16) -> rule1))] @2: The cow likes the mouse.[(((((triple16) -> rule1)) -> rule2))]
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple5
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple6
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The rabbit is not big.
("rabbit" "is" "big" "-")
triple9
The rabbit is not round.
("rabbit" "is" "round" "-")
triple10
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple11
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
triple15
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple13
The squirrel is round.
("squirrel" "is" "round" "+")
triple14
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple16
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((triple16) -> (rule1 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2