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