The bear likes the tiger. The lion needs the rabbit. The lion needs the tiger. The lion sees the tiger. The rabbit likes the bear. The tiger is kind. The tiger likes the lion. If the lion sees the tiger and the tiger likes the rabbit then the tiger sees the lion. If something is cold then it is blue. If something sees the rabbit and the rabbit needs the lion then the lion needs the rabbit. If something needs the rabbit then the rabbit likes the lion. If something is red and it needs the tiger then the tiger is cold. If something is blue and it sees the tiger then it likes the tiger.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If the lion sees the tiger and the tiger likes the rabbit then the tiger sees the lion.
((("lion" "sees" "tiger" "+") ("tiger" "likes" "rabbit" "+")) -> ("tiger" "sees" "lion" "+"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something sees the rabbit and the rabbit needs the lion then the lion needs the rabbit.
((("something" "sees" "rabbit" "+") ("rabbit" "needs" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If something needs the rabbit then the rabbit likes the lion.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "likes" "lion" "+"))
If something is red and it needs the tiger then the tiger is cold.
((("something" "is" "red" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If something is blue and it sees the tiger then it likes the tiger.
((("something" "is" "blue" "+") ("something" "sees" "tiger" "+")) -> ("something" "likes" "tiger" "+"))
The bear likes the tiger.
True
1
proof
[(triple1)]
("bear" "likes" "tiger" "+")
triple1
The lion does not need the tiger.
False
1
inv-proof
[(triple3)]
("lion" "needs" "tiger" "-")
triple3
The rabbit likes the lion.
True
2
proof
[(((triple2) -> rule4))]
("rabbit" "likes" "lion" "+")
((triple2) -> (rule4 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit does not like the lion.
False
2
inv-proof
[(((triple2) -> rule4))]
("rabbit" "likes" "lion" "-")
((triple2) -> (rule4 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The lion is not blue.
Unknown
inv-rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "blue" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The bear does not see the tiger.
Unknown
inv-random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
@0: The bear likes the tiger.[(triple1)] The lion needs the rabbit.[(triple2)] The lion needs the tiger.[(triple3)] The lion sees the tiger.[(triple4)] The rabbit likes the bear.[(triple5)] The tiger is kind.[(triple6)] The tiger likes the lion.[(triple7)] @1: The rabbit likes the lion.[(((triple2) -> rule4))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple7
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((triple2) -> (rule4 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1