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