The lion chases the tiger. The lion eats the tiger. The lion is green. The lion is rough. The lion sees the tiger. The tiger chases the lion. The tiger eats the lion. The tiger is green. The tiger is rough. The tiger sees the lion. If someone chases the lion and they eat the lion then the lion sees the tiger. If someone is green then they see the tiger. If someone chases the lion and the lion is kind then they eat the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone chases the lion and they eat the lion then the lion sees the tiger.
((("someone" "chases" "lion" "+") ("someone" "eats" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If someone is green then they see the tiger.
((("someone" "is" "green" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the lion and the lion is kind then they eat the lion.
((("someone" "chases" "lion" "+") ("lion" "is" "kind" "+")) -> ("someone" "eats" "lion" "+"))
The tiger is rough.
True
1
proof
[(triple9)]
("tiger" "is" "rough" "+")
triple9
The lion does not chase the tiger.
False
1
inv-proof
[(triple1)]
("lion" "chases" "tiger" "-")
triple1
The tiger sees the tiger.
True
2
proof
[(((triple8) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple8) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple8) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple8) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "lion" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The lion chases the tiger.[(triple1)] The lion eats the tiger.[(triple2)] The lion is green.[(triple3)] The lion is rough.[(triple4)] The lion sees the tiger.[(triple5 OR ((triple3) -> rule2) OR ((triple6 triple7) -> rule1))] The tiger chases the lion.[(triple6)] The tiger eats the lion.[(triple7)] The tiger is green.[(triple8)] The tiger is rough.[(triple9)] The tiger sees the lion.[(triple10)] @1: The tiger sees the tiger.[(((triple8) -> rule2))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple5
((triple3) -> (rule2 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
((triple6 triple7) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple10
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple8) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1