The cow is green. The cow is young. The cow needs the squirrel. The rabbit is blue. The rabbit is round. The rabbit needs the cow. The rabbit visits the squirrel. The squirrel is red. The squirrel is young. The squirrel sees the cow. The tiger is red. The tiger needs the rabbit. If someone sees the tiger then the tiger sees the rabbit. If someone is blue and they visit the squirrel then they see the tiger. If someone visits the tiger then they need the squirrel.
The cow is green.
("cow" "is" "green" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If someone sees the tiger then the tiger sees the rabbit.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If someone is blue and they visit the squirrel then they see the tiger.
((("someone" "is" "blue" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the tiger then they need the squirrel.
((("someone" "visits" "tiger" "+")) -> ("someone" "needs" "squirrel" "+"))
The rabbit needs the cow.
True
1
proof
[(triple6)]
("rabbit" "needs" "cow" "+")
triple6
The tiger is not red.
False
1
inv-proof
[(triple11)]
("tiger" "is" "red" "-")
triple11
The rabbit sees the tiger.
True
3
proof
[(((triple4 triple7) -> rule2))]
("rabbit" "sees" "tiger" "+")
((triple4 triple7) -> (rule2 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit does not see the tiger.
False
3
inv-proof
[(((triple4 triple7) -> rule2))]
("rabbit" "sees" "tiger" "-")
((triple4 triple7) -> (rule2 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger sees the rabbit.
True
4
proof
[(((((triple4 triple7) -> rule2)) -> rule1))]
("tiger" "sees" "rabbit" "+")
((((triple4 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger does not see the rabbit.
False
4
inv-proof
[(((((triple4 triple7) -> rule2)) -> rule1))]
("tiger" "sees" "rabbit" "-")
((((triple4 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The squirrel does not see the tiger.
Unknown
inv-rconc
[@1: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The cow does not see the tiger.
Unknown
inv-rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "tiger" "-")
The squirrel needs the tiger.
Unknown
random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "+")
The squirrel does not visit the rabbit.
Unknown
inv-random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cow is green.[(triple1)] The cow is young.[(triple2)] The cow needs the squirrel.[(triple3)] The rabbit is blue.[(triple4)] The rabbit is round.[(triple5)] The rabbit needs the cow.[(triple6)] The rabbit visits the squirrel.[(triple7)] The squirrel is red.[(triple8)] The squirrel is young.[(triple9)] The squirrel sees the cow.[(triple10)] The tiger is red.[(triple11)] The tiger needs the rabbit.[(triple12)] @1: The rabbit sees the tiger.[(((triple4 triple7) -> rule2))] @2: The tiger sees the rabbit.[(((((triple4 triple7) -> rule2)) -> rule1))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple6
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel is young.
("squirrel" "is" "young" "+")
triple9
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple12
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple4 triple7) -> (rule2 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((((triple4 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2