The rabbit is blue. The rabbit is rough. The rabbit needs the tiger. The rabbit sees the tiger. The tiger eats the rabbit. The tiger is rough. The tiger needs the rabbit. If something sees the rabbit then the rabbit is red. If the rabbit needs the tiger then the rabbit eats the tiger. If something sees the tiger and it eats the tiger then the tiger sees the rabbit.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
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 rough.
("tiger" "is" "rough" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something sees the rabbit then the rabbit is red.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If the rabbit needs the tiger then the rabbit eats the tiger.
((("rabbit" "needs" "tiger" "+")) -> ("rabbit" "eats" "tiger" "+"))
If something sees the tiger and it eats the tiger then the tiger sees the rabbit.
((("something" "sees" "tiger" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
The tiger eats the rabbit.
True
1
proof
[(triple5)]
("tiger" "eats" "rabbit" "+")
triple5
The tiger is not rough.
False
1
inv-proof
[(triple6)]
("tiger" "is" "rough" "-")
triple6
The rabbit eats the tiger.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "eats" "tiger" "+")
((triple3) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit does not eat the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("rabbit" "eats" "tiger" "-")
((triple3) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger sees the rabbit.
True
4
proof
[(((triple4 ((triple3) -> rule2)) -> rule3))]
("tiger" "sees" "rabbit" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The tiger does not see the rabbit.
False
4
inv-proof
[(((triple4 ((triple3) -> rule2)) -> rule3))]
("tiger" "sees" "rabbit" "-")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit is red.
True
5
proof
[(((((triple4 ((triple3) -> rule2)) -> rule3)) -> rule1))]
("rabbit" "is" "red" "+")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The rabbit is not red.
False
5
inv-proof
[(((((triple4 ((triple3) -> rule2)) -> rule3)) -> rule1))]
("rabbit" "is" "red" "-")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
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 cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
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 is blue.[(triple1)] The rabbit is rough.[(triple2)] The rabbit needs the tiger.[(triple3)] The rabbit sees the tiger.[(triple4)] The tiger eats the rabbit.[(triple5)] The tiger is rough.[(triple6)] The tiger needs the rabbit.[(triple7)] @1: The rabbit eats the tiger.[(((triple3) -> rule2))] @2: The tiger sees the rabbit.[(((triple4 ((triple3) -> rule2)) -> rule3))] @3: The rabbit is red.[(((((triple4 ((triple3) -> rule2)) -> rule3)) -> rule1))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit is rough.
("rabbit" "is" "rough" "+")
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
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple7
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((triple3) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int3