The lion is rough. The tiger is kind. If someone is kind then they like the tiger. If someone likes the tiger then they are rough. If someone visits the lion and they like the tiger then the lion is not round. If someone visits the tiger then they do not need the lion. If someone is big and they do not like the lion then they need the lion. If the tiger visits the lion then the tiger needs the lion. If someone visits the lion then they do not need the tiger. If the tiger needs the lion and the lion does not visit the tiger then the tiger visits the lion.
The lion is rough.
("lion" "is" "rough" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone is kind then they like the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the tiger then they are rough.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the lion and they like the tiger then the lion is not round.
((("someone" "visits" "lion" "+") ("someone" "likes" "tiger" "+")) -> ("lion" "is" "round" "-"))
If someone visits the tiger then they do not need the lion.
((("someone" "visits" "tiger" "+")) -> ("someone" "needs" "lion" "-"))
If someone is big and they do not like the lion then they need the lion.
((("someone" "is" "big" "+") ("someone" "likes" "lion" "~")) -> ("someone" "needs" "lion" "+"))
If the tiger visits the lion then the tiger needs the lion.
((("tiger" "visits" "lion" "+")) -> ("tiger" "needs" "lion" "+"))
If someone visits the lion then they do not need the tiger.
((("someone" "visits" "lion" "+")) -> ("someone" "needs" "tiger" "-"))
If the tiger needs the lion and the lion does not visit the tiger then the tiger visits the lion.
((("tiger" "needs" "lion" "+") ("lion" "visits" "tiger" "~")) -> ("tiger" "visits" "lion" "+"))
The tiger is kind.
True
1
proof
[(triple2)]
("tiger" "is" "kind" "+")
triple2
The lion is not rough.
False
1
inv-proof
[(triple1)]
("lion" "is" "rough" "-")
triple1
The tiger likes the tiger.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "likes" "tiger" "-")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is rough.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("tiger" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("tiger" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger does not need the lion.
Unknown
inv-rconc
[@2: The tiger needs the lion.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("tiger" "needs" "lion" "-")
The tiger visits the lion.
Unknown
rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "visits" "lion" "+")
The lion does not like the tiger.
Unknown
inv-rconc
[@1: The lion likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "tiger" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
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 is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The lion is rough.[(triple1)] The tiger is kind.[(triple2)] @1: The tiger likes the tiger.[(((triple2) -> rule1))] @2: The tiger is rough.[(((((triple2) -> rule1)) -> rule2))]
The lion is rough.
("lion" "is" "rough" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
triple2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple2) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2