The lion is kind. The lion is red. The lion sees the rabbit. The rabbit needs the tiger. The rabbit sees the lion. The tiger is kind. The tiger needs the rabbit. If something is kind then it needs the lion. If something needs the rabbit and it is nice then it visits the tiger. If something visits the tiger then the tiger needs the lion. All kind things are cold. If something needs the rabbit then it sees the rabbit. If something needs the tiger and the tiger sees the lion then the tiger visits the lion. If something sees the lion and the lion visits the rabbit then it is cold. If something visits the tiger and the tiger sees the rabbit then it visits the rabbit.
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something is kind then it needs the lion.
((("something" "is" "kind" "+")) -> ("something" "needs" "lion" "+"))
If something needs the rabbit and it is nice then it visits the tiger.
((("something" "needs" "rabbit" "+") ("something" "is" "nice" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the tiger then the tiger needs the lion.
((("something" "visits" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something needs the rabbit then it sees the rabbit.
((("something" "needs" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If something needs the tiger and the tiger sees the lion then the tiger visits the lion.
((("something" "needs" "tiger" "+") ("tiger" "sees" "lion" "+")) -> ("tiger" "visits" "lion" "+"))
If something sees the lion and the lion visits the rabbit then it is cold.
((("something" "sees" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("something" "is" "cold" "+"))
If something visits the tiger and the tiger sees the rabbit then it visits the rabbit.
((("something" "visits" "tiger" "+") ("tiger" "sees" "rabbit" "+")) -> ("something" "visits" "rabbit" "+"))
The rabbit sees the lion.
True
1
proof
[(triple5)]
("rabbit" "sees" "lion" "+")
triple5
The rabbit does not need the tiger.
False
1
inv-proof
[(triple4)]
("rabbit" "needs" "tiger" "-")
triple4
The tiger does not visit the lion.
Unknown
inv-rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "lion" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The lion is kind.[(triple1)] The lion is red.[(triple2)] The lion sees the rabbit.[(triple3)] The rabbit needs the tiger.[(triple4)] The rabbit sees the lion.[(triple5)] The tiger is kind.[(triple6)] The tiger needs the rabbit.[(triple7)] @1: The lion is cold.[(((triple1) -> rule4))] The lion needs the lion.[(((triple1) -> rule1))] The tiger is cold.[(((triple6) -> rule4))] The tiger needs the lion.[(((triple6) -> rule1))] The tiger sees the rabbit.[(((triple7) -> rule5))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple3
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple4
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
((triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple1) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple6) -> (rule4 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((triple6) -> (rule1 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple7) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1