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