The rabbit likes the tiger. The tiger is young. If something likes the tiger then the tiger is rough. If something is rough then it eats the tiger.
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
If something likes the tiger then the tiger is rough.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something is rough then it eats the tiger.
((("something" "is" "rough" "+")) -> ("something" "eats" "tiger" "+"))
The rabbit likes the tiger.
True
1
proof
[(triple1)]
("rabbit" "likes" "tiger" "+")
triple1
The rabbit does not like the tiger.
False
1
inv-proof
[(triple1)]
("rabbit" "likes" "tiger" "-")
triple1
The tiger is rough.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("tiger" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger does not eat the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("tiger" "eats" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The rabbit does not eat the tiger.
Unknown
inv-rconc
[@1: The rabbit eats the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "tiger" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger does not eat the rabbit.
Unknown
inv-random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The rabbit likes the tiger.[(triple1)] The tiger is young.[(triple2)] @1: The tiger is rough.[(((triple1) -> rule1))] @2: The tiger eats the tiger.[(((((triple1) -> rule1)) -> rule2))]
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple1
The tiger is young.
("tiger" "is" "young" "+")
triple2
The tiger is rough.
("tiger" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2