The rabbit is young. The tiger is blue. If someone eats the rabbit and the rabbit chases the tiger then they chase the tiger. If someone needs the tiger then the tiger is young. If someone needs the rabbit and they are not round then the rabbit is red. Kind people are blue. If someone chases the tiger and the tiger is red then they do not need the rabbit. If the rabbit is round and the rabbit needs the tiger then the tiger eats the rabbit. If someone eats the rabbit and the rabbit is young then the rabbit eats the tiger. If someone is young then they need the tiger.
The rabbit is young.
("rabbit" "is" "young" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If someone eats the rabbit and the rabbit chases the tiger then they chase the tiger.
((("someone" "eats" "rabbit" "+") ("rabbit" "chases" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
If someone needs the tiger then the tiger is young.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If someone needs the rabbit and they are not round then the rabbit is red.
((("someone" "needs" "rabbit" "+") ("someone" "is" "round" "~")) -> ("rabbit" "is" "red" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone chases the tiger and the tiger is red then they do not need the rabbit.
((("someone" "chases" "tiger" "+") ("tiger" "is" "red" "+")) -> ("someone" "needs" "rabbit" "-"))
If the rabbit is round and the rabbit needs the tiger then the tiger eats the rabbit.
((("rabbit" "is" "round" "+") ("rabbit" "needs" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone eats the rabbit and the rabbit is young then the rabbit eats the tiger.
((("someone" "eats" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "eats" "tiger" "+"))
If someone is young then they need the tiger.
((("someone" "is" "young" "+")) -> ("someone" "needs" "tiger" "+"))
The tiger is blue.
True
1
proof
[(triple2)]
("tiger" "is" "blue" "+")
triple2
The tiger is not blue.
False
1
inv-proof
[(triple2)]
("tiger" "is" "blue" "-")
triple2
The rabbit needs the tiger.
True
2
proof
[(((triple1) -> rule8))]
("rabbit" "needs" "tiger" "+")
((triple1) -> (rule8 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The rabbit does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule8))]
("rabbit" "needs" "tiger" "-")
((triple1) -> (rule8 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger is young.
True
3
proof
[(((((triple1) -> rule8)) -> rule2))]
("tiger" "is" "young" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger is not young.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule2))]
("tiger" "is" "young" "-")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger needs the tiger.
True
4
proof
[(((((((triple1) -> rule8)) -> rule2)) -> rule8))]
("tiger" "needs" "tiger" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int3
The tiger does not need the tiger.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule2)) -> rule8))]
("tiger" "needs" "tiger" "-")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int3
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit eats the tiger.
Unknown
rconc
[@2: The rabbit eats the tiger.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("rabbit" "eats" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The rabbit is blue.
Unknown
rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "blue" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger chases the rabbit.
Unknown
random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is young.[(triple1)] The tiger is blue.[(triple2)] @1: The rabbit needs the tiger.[(((triple1) -> rule8))] @2: The tiger is young.[(((((triple1) -> rule8)) -> rule2))] @3: The tiger needs the tiger.[(((((((triple1) -> rule8)) -> rule2)) -> rule8))]
The rabbit is young.
("rabbit" "is" "young" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple1) -> (rule8 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int3