The bear likes the cat. The bear sees the squirrel. The cat is rough. The cat sees the rabbit. The rabbit is green. The rabbit likes the cat. The rabbit likes the squirrel. The rabbit sees the bear. The rabbit sees the cat. The rabbit sees the squirrel. The squirrel is rough. The squirrel likes the bear. The squirrel likes the cat. The squirrel sees the rabbit. The squirrel visits the cat. If something is big and it visits the cat then it visits the bear. If something likes the bear then the bear visits the cat.
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If something is big and it visits the cat then it visits the bear.
((("something" "is" "big" "+") ("something" "visits" "cat" "+")) -> ("something" "visits" "bear" "+"))
If something likes the bear then the bear visits the cat.
((("something" "likes" "bear" "+")) -> ("bear" "visits" "cat" "+"))
The squirrel likes the bear.
True
1
proof
[(triple12)]
("squirrel" "likes" "bear" "+")
triple12
The cat is not rough.
False
1
inv-proof
[(triple3)]
("cat" "is" "rough" "-")
triple3
The bear visits the cat.
True
2
proof
[(((triple12) -> rule2))]
("bear" "visits" "cat" "+")
((triple12) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear does not visit the cat.
False
2
inv-proof
[(((triple12) -> rule2))]
("bear" "visits" "cat" "-")
((triple12) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat does not visit the bear.
Unknown
inv-rconc
[@1: The cat visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "bear" "-")
The rabbit visits the bear.
Unknown
rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "bear" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear likes the cat.[(triple1)] The bear sees the squirrel.[(triple2)] The cat is rough.[(triple3)] The cat sees the rabbit.[(triple4)] The rabbit is green.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit likes the squirrel.[(triple7)] The rabbit sees the bear.[(triple8)] The rabbit sees the cat.[(triple9)] The rabbit sees the squirrel.[(triple10)] The squirrel is rough.[(triple11)] The squirrel likes the bear.[(triple12)] The squirrel likes the cat.[(triple13)] The squirrel sees the rabbit.[(triple14)] The squirrel visits the cat.[(triple15)] @1: The bear visits the cat.[(((triple12) -> rule2))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple4
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple7
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple8
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple9
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple12
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple13
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple14
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple15
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple12) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1