The rabbit sees the tiger. The rabbit visits the tiger. The tiger is kind. If someone eats the rabbit and they are green then they eat the tiger. If someone sees the rabbit and the rabbit eats the tiger then the tiger is young. If someone visits the tiger then they eat the rabbit. If someone visits the rabbit and the rabbit visits the tiger then the rabbit is rough. If someone visits the tiger then they are young. If the rabbit is rough then the rabbit sees the tiger. If someone visits the tiger then the tiger eats the rabbit. If the tiger eats the rabbit then the tiger visits the rabbit.
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone eats the rabbit and they are green then they eat the tiger.
((("someone" "eats" "rabbit" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "tiger" "+"))
If someone sees the rabbit and the rabbit eats the tiger then the tiger is young.
((("someone" "sees" "rabbit" "+") ("rabbit" "eats" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If someone visits the tiger then they eat the rabbit.
((("someone" "visits" "tiger" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone visits the rabbit and the rabbit visits the tiger then the rabbit is rough.
((("someone" "visits" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("rabbit" "is" "rough" "+"))
If someone visits the tiger then they are young.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "young" "+"))
If the rabbit is rough then the rabbit sees the tiger.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone visits the tiger then the tiger eats the rabbit.
((("someone" "visits" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If the tiger eats the rabbit then the tiger visits the rabbit.
((("tiger" "eats" "rabbit" "+")) -> ("tiger" "visits" "rabbit" "+"))
The tiger is kind.
True
1
proof
[(triple3)]
("tiger" "is" "kind" "+")
triple3
The rabbit does not visit the tiger.
False
1
inv-proof
[(triple2)]
("rabbit" "visits" "tiger" "-")
triple2
The tiger eats the rabbit.
True
2
proof
[(((triple2) -> rule7))]
("tiger" "eats" "rabbit" "+")
((triple2) -> (rule7 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((triple2) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The tiger visits the rabbit.
True
3
proof
[(((((triple2) -> rule7)) -> rule8))]
("tiger" "visits" "rabbit" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger does not visit the rabbit.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule8))]
("tiger" "visits" "rabbit" "-")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit is rough.
True
5
proof
[(((((((triple2) -> rule7)) -> rule8) triple2) -> rule4))]
("rabbit" "is" "rough" "+")
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3
The rabbit is not rough.
False
5
inv-proof
[(((((((triple2) -> rule7)) -> rule8) triple2) -> rule4))]
("rabbit" "is" "rough" "-")
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "young" "-")
The rabbit eats the tiger.
Unknown
rconc
[@1: The rabbit eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The tiger does not see the rabbit.
Unknown
inv-random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The rabbit sees the tiger.[(triple1 OR ((((((((triple2) -> rule7)) -> rule8) triple2) -> rule4)) -> rule6))] The rabbit visits the tiger.[(triple2)] The tiger is kind.[(triple3)] @1: The rabbit eats the rabbit.[(((triple2) -> rule3))] The rabbit is young.[(((triple2) -> rule5))] The tiger eats the rabbit.[(((triple2) -> rule7))] @2: The tiger visits the rabbit.[(((((triple2) -> rule7)) -> rule8))] @3: The rabbit is rough.[(((((((triple2) -> rule7)) -> rule8) triple2) -> rule4))]
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple1
((((((((triple2) -> (rule7 % int4))) -> (rule8 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple2
The tiger is kind.
("tiger" "is" "kind" "+")
triple3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple2) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple2) -> (rule7 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2)) triple2) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int3