The lion chases the tiger. The tiger chases the lion. If someone is green then they chase the lion. If someone likes the lion and they are not young then the lion is not rough. If the tiger is young then the tiger is green. If the tiger chases the lion and the tiger does not like the lion then the lion likes the tiger. If someone likes the lion and the lion eats the tiger then they are big. If someone chases the tiger then they are green.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
If someone is green then they chase the lion.
((("someone" "is" "green" "+")) -> ("someone" "chases" "lion" "+"))
If someone likes the lion and they are not young then the lion is not rough.
((("someone" "likes" "lion" "+") ("someone" "is" "young" "~")) -> ("lion" "is" "rough" "-"))
If the tiger is young then the tiger is green.
((("tiger" "is" "young" "+")) -> ("tiger" "is" "green" "+"))
If the tiger chases the lion and the tiger does not like the lion then the lion likes the tiger.
((("tiger" "chases" "lion" "+") ("tiger" "likes" "lion" "~")) -> ("lion" "likes" "tiger" "+"))
If someone likes the lion and the lion eats the tiger then they are big.
((("someone" "likes" "lion" "+") ("lion" "eats" "tiger" "+")) -> ("someone" "is" "big" "+"))
If someone chases the tiger then they are green.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "green" "+"))
The lion chases the tiger.
True
1
proof
[(triple1)]
("lion" "chases" "tiger" "+")
triple1
The tiger does not chase the lion.
False
1
inv-proof
[(triple2)]
("tiger" "chases" "lion" "-")
triple2
The lion is green.
True
2
proof
[(((triple1) -> rule6))]
("lion" "is" "green" "+")
((triple1) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple1) -> rule6))]
("lion" "is" "green" "-")
((triple1) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion chases the lion.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("lion" "chases" "lion" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion does not chase the lion.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("lion" "chases" "lion" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "green" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "big" "+")
The lion does not like the tiger.
Unknown
inv-rconc
[@1: The lion likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "tiger" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The tiger does not like the lion.
Unknown
inv-random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The lion chases the tiger.[(triple1)] The tiger chases the lion.[(triple2)] @1: The lion is green.[(((triple1) -> rule6))] @2: The lion chases the lion.[(((((triple1) -> rule6)) -> rule1))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
((triple1) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2