The lion is cold. The lion sees the rabbit. The lion sees the tiger. The lion visits the tiger. The rabbit is cold. The rabbit is not green. The rabbit does not like the lion. The rabbit sees the lion. The rabbit sees the tiger. The tiger is cold. The tiger is red. The tiger is not young. The tiger sees the lion. The tiger sees the rabbit. The tiger visits the rabbit. If someone is red then they visit the tiger. If someone sees the rabbit and they like the rabbit then the rabbit visits the tiger. If someone visits the tiger then they see the tiger.
The lion is cold.
("lion" "is" "cold" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone is red then they visit the tiger.
((("someone" "is" "red" "+")) -> ("someone" "visits" "tiger" "+"))
If someone sees the rabbit and they like the rabbit then the rabbit visits the tiger.
((("someone" "sees" "rabbit" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If someone visits the tiger then they see the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
The tiger visits the rabbit.
True
1
proof
[(triple15)]
("tiger" "visits" "rabbit" "+")
triple15
The lion does not see the tiger.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule3))]
("lion" "sees" "tiger" "-")
triple3
((triple4) -> (rule3 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger visits the tiger.
True
2
proof
[(((triple11) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple11) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple11) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple11) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple11) -> rule1)) -> rule3))]
("tiger" "sees" "tiger" "+")
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple11) -> rule1)) -> rule3))]
("tiger" "sees" "tiger" "-")
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The rabbit does not visit the tiger.
Unknown
inv-rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "tiger" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The rabbit visits the lion.
Unknown
random
[@0: The rabbit visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "lion" "+")
@0: The lion is cold.[(triple1)] The lion sees the rabbit.[(triple2)] The lion sees the tiger.[(triple3 OR ((triple4) -> rule3))] The lion visits the tiger.[(triple4)] The rabbit does not like the lion.[(triple7)] The rabbit is cold.[(triple5)] The rabbit is not green.[(triple6)] The rabbit sees the lion.[(triple8)] The rabbit sees the tiger.[(triple9)] The tiger is cold.[(triple10)] The tiger is not young.[(triple12)] The tiger is red.[(triple11)] The tiger sees the lion.[(triple13)] The tiger sees the rabbit.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The tiger visits the tiger.[(((triple11) -> rule1))] @2: The tiger sees the tiger.[(((((triple11) -> rule1)) -> rule3))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple3
((triple4) -> (rule3 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple4
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit is not green.
("rabbit" "is" "green" "-")
triple6
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple8
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is not young.
("tiger" "is" "young" "-")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple13
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple11) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple11) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2