The lion chases the tiger. The lion eats the tiger. The lion is young. The lion needs the tiger. The tiger does not eat the lion. The tiger is young. The tiger needs the lion. If someone chases the lion and they are young then the lion is not blue. If the lion needs the tiger then the lion chases the tiger. If someone is blue and they chase the lion then they are big. If someone eats the tiger then the tiger is not kind. If someone chases the lion and they do not eat the lion then they need the lion. If someone needs the lion and the lion is kind then the lion is big.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If someone chases the lion and they are young then the lion is not blue.
((("someone" "chases" "lion" "+") ("someone" "is" "young" "+")) -> ("lion" "is" "blue" "-"))
If the lion needs the tiger then the lion chases the tiger.
((("lion" "needs" "tiger" "+")) -> ("lion" "chases" "tiger" "+"))
If someone is blue and they chase the lion then they are big.
((("someone" "is" "blue" "+") ("someone" "chases" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone eats the tiger then the tiger is not kind.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "kind" "-"))
If someone chases the lion and they do not eat the lion then they need the lion.
((("someone" "chases" "lion" "+") ("someone" "eats" "lion" "~")) -> ("someone" "needs" "lion" "+"))
If someone needs the lion and the lion is kind then the lion is big.
((("someone" "needs" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "big" "+"))
The tiger is young.
True
1
proof
[(triple6)]
("tiger" "is" "young" "+")
triple6
The lion does not eat the tiger.
False
1
inv-proof
[(triple2)]
("lion" "eats" "tiger" "-")
triple2
The tiger is not kind.
True
2
proof
[(((triple2) -> rule4))]
("tiger" "is" "kind" "-")
((triple2) -> (rule4 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The tiger is kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("tiger" "is" "kind" "+")
((triple2) -> (rule4 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "big" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "lion" "+")
The tiger does not chase the lion.
Unknown
inv-random
[@0: The tiger chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "lion" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The lion chases the tiger.[(triple1 OR ((triple4) -> rule2))] The lion eats the tiger.[(triple2)] The lion is young.[(triple3)] The lion needs the tiger.[(triple4)] The tiger does not eat the lion.[(triple5)] The tiger is young.[(triple6)] The tiger needs the lion.[(triple7)] @1: The tiger is not kind.[(((triple2) -> rule4))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
((triple4) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple4
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple7
The tiger is not kind.
("tiger" "is" "kind" "-")
((triple2) -> (rule4 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1