The lion needs the tiger. The rabbit chases the lion. The rabbit is kind. The rabbit needs the lion. The rabbit sees the tiger. The tiger chases the lion. The tiger is cold. If the tiger chases the lion and the lion is cold then the tiger sees the lion. If someone needs the lion then the lion is blue. If the tiger chases the lion then the tiger sees the rabbit. If someone needs the tiger and the tiger needs the lion then they see the lion. If someone is blue then they see the tiger. If someone chases the lion and the lion needs the rabbit then the rabbit sees the tiger. If someone chases the tiger then the tiger chases the lion. If someone sees the lion then they chase the tiger.
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If the tiger chases the lion and the lion is cold then the tiger sees the lion.
((("tiger" "chases" "lion" "+") ("lion" "is" "cold" "+")) -> ("tiger" "sees" "lion" "+"))
If someone needs the lion then the lion is blue.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "blue" "+"))
If the tiger chases the lion then the tiger sees the rabbit.
((("tiger" "chases" "lion" "+")) -> ("tiger" "sees" "rabbit" "+"))
If someone needs the tiger and the tiger needs the lion then they see the lion.
((("someone" "needs" "tiger" "+") ("tiger" "needs" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone is blue then they see the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the lion and the lion needs the rabbit then the rabbit sees the tiger.
((("someone" "chases" "lion" "+") ("lion" "needs" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone chases the tiger then the tiger chases the lion.
((("someone" "chases" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If someone sees the lion then they chase the tiger.
((("someone" "sees" "lion" "+")) -> ("someone" "chases" "tiger" "+"))
The tiger is cold.
True
1
proof
[(triple7)]
("tiger" "is" "cold" "+")
triple7
The rabbit is not kind.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
The tiger sees the rabbit.
True
2
proof
[(((triple6) -> rule3))]
("tiger" "sees" "rabbit" "+")
((triple6) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger does not see the rabbit.
False
2
inv-proof
[(((triple6) -> rule3))]
("tiger" "sees" "rabbit" "-")
((triple6) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The lion sees the tiger.
True
3
proof
[(((((triple4) -> rule2)) -> rule5))]
("lion" "sees" "tiger" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion does not see the tiger.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule5))]
("lion" "sees" "tiger" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "lion" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@2: The tiger chases the tiger.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("tiger" "chases" "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 blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The tiger needs the lion.
Unknown
random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "+")
@0: The lion needs the tiger.[(triple1)] The rabbit chases the lion.[(triple2)] The rabbit is kind.[(triple3)] The rabbit needs the lion.[(triple4)] The rabbit sees the tiger.[(triple5)] The tiger chases the lion.[(triple6)] The tiger is cold.[(triple7)] @1: The lion is blue.[(((triple4) -> rule2))] The tiger sees the rabbit.[(((triple6) -> rule3))] @2: The lion sees the tiger.[(((((triple4) -> rule2)) -> rule5))]
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple4
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple5
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
((triple4) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple6) -> (rule3 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2