The rabbit eats the tiger. The rabbit is kind. The rabbit needs the tiger. The rabbit sees the tiger. The tiger eats the rabbit. The tiger is green. The tiger is kind. The tiger is young. The tiger needs the rabbit. The tiger sees the rabbit. If something is kind then it is green. If something eats the tiger and it is green then the tiger eats the rabbit.
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something eats the tiger and it is green then the tiger eats the rabbit.
((("something" "eats" "tiger" "+") ("something" "is" "green" "+")) -> ("tiger" "eats" "rabbit" "+"))
The tiger is kind.
True
1
proof
[(triple7)]
("tiger" "is" "kind" "+")
triple7
The rabbit does not see the tiger.
False
1
inv-proof
[(triple4)]
("rabbit" "sees" "tiger" "-")
triple4
The rabbit is green.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "is" "green" "+")
((triple2) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "is" "green" "-")
((triple2) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit eats the tiger.[(triple1)] The rabbit is kind.[(triple2)] The rabbit needs the tiger.[(triple3)] The rabbit sees the tiger.[(triple4)] The tiger eats the rabbit.[(triple5 OR ((triple1 ((triple2) -> rule1)) -> rule2))] The tiger is green.[(triple6 OR ((triple7) -> rule1))] The tiger is kind.[(triple7)] The tiger is young.[(triple8)] The tiger needs the rabbit.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The rabbit is green.[(((triple2) -> rule1))]
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple3
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple4
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple5
((triple1 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
triple6
((triple7) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
((triple2) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1