The rabbit needs the tiger. The rabbit visits the tiger. The squirrel likes the tiger. The squirrel needs the rabbit. The squirrel visits the tiger. The tiger is young. The tiger likes the squirrel. The tiger needs the rabbit. The tiger needs the squirrel. The tiger visits the squirrel. If something visits the rabbit then it visits the squirrel. If something visits the tiger and it needs the tiger then it needs the squirrel.
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something visits the rabbit then it visits the squirrel.
((("something" "visits" "rabbit" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the tiger and it needs the tiger then it needs the squirrel.
((("something" "visits" "tiger" "+") ("something" "needs" "tiger" "+")) -> ("something" "needs" "squirrel" "+"))
The squirrel likes the tiger.
True
1
proof
[(triple3)]
("squirrel" "likes" "tiger" "+")
triple3
The squirrel does not visit the tiger.
False
1
inv-proof
[(triple5)]
("squirrel" "visits" "tiger" "-")
triple5
The rabbit needs the squirrel.
True
3
proof
[(((triple2 triple1) -> rule2))]
("rabbit" "needs" "squirrel" "+")
((triple2 triple1) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The rabbit does not need the squirrel.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("rabbit" "needs" "squirrel" "-")
((triple2 triple1) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The rabbit needs the tiger.[(triple1)] The rabbit visits the tiger.[(triple2)] The squirrel likes the tiger.[(triple3)] The squirrel needs the rabbit.[(triple4)] The squirrel visits the tiger.[(triple5)] The tiger is young.[(triple6)] The tiger likes the squirrel.[(triple7)] The tiger needs the rabbit.[(triple8)] The tiger needs the squirrel.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The rabbit needs the squirrel.[(((triple2 triple1) -> rule2))]
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple2
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple7
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple8
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((triple2 triple1) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1