The lion visits the tiger. The tiger is round. If something likes the tiger then the tiger is green. If something visits the lion and it is blue then it needs the tiger. If something needs the lion and the lion likes the tiger then the tiger visits the lion. If something is round then it needs the lion. If something is round and it likes the tiger then the tiger visits the lion. If the tiger likes the lion then the tiger needs the lion. If something needs the lion and the lion is round then the lion needs the tiger. If something is green then it visits the tiger.
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something likes the tiger then the tiger is green.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something visits the lion and it is blue then it needs the tiger.
((("something" "visits" "lion" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the lion and the lion likes the tiger then the tiger visits the lion.
((("something" "needs" "lion" "+") ("lion" "likes" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If something is round then it needs the lion.
((("something" "is" "round" "+")) -> ("something" "needs" "lion" "+"))
If something is round and it likes the tiger then the tiger visits the lion.
((("something" "is" "round" "+") ("something" "likes" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If the tiger likes the lion then the tiger needs the lion.
((("tiger" "likes" "lion" "+")) -> ("tiger" "needs" "lion" "+"))
If something needs the lion and the lion is round then the lion needs the tiger.
((("something" "needs" "lion" "+") ("lion" "is" "round" "+")) -> ("lion" "needs" "tiger" "+"))
If something is green then it visits the tiger.
((("something" "is" "green" "+")) -> ("something" "visits" "tiger" "+"))
The tiger is round.
True
1
proof
[(triple2)]
("tiger" "is" "round" "+")
triple2
The tiger is not round.
False
1
inv-proof
[(triple2)]
("tiger" "is" "round" "-")
triple2
The tiger needs the lion.
True
2
proof
[(((triple2) -> rule4))]
("tiger" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger does not need the lion.
False
2
inv-proof
[(((triple2) -> rule4))]
("tiger" "needs" "lion" "-")
((triple2) -> (rule4 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion does not need the tiger.
Unknown
inv-rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "tiger" "-")
The tiger visits the lion.
Unknown
rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "lion" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
@0: The lion visits the tiger.[(triple1)] The tiger is round.[(triple2)] @1: The tiger needs the lion.[(((triple2) -> rule4))]
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple1
The tiger is round.
("tiger" "is" "round" "+")
triple2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1