The cat is young. The lion sees the tiger. The tiger sees the lion. If someone is kind then they visit the tiger. If someone visits the lion and they chase the tiger then they chase the cat. If someone sees the tiger and they chase the tiger then they visit the cat. If someone sees the tiger then they are kind. If someone sees the tiger then they are young. If someone sees the lion and the lion does not chase the cat then the cat chases the lion.
The cat is young.
("cat" "is" "young" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone is kind then they visit the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the lion and they chase the tiger then they chase the cat.
((("someone" "visits" "lion" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "chases" "cat" "+"))
If someone sees the tiger and they chase the tiger then they visit the cat.
((("someone" "sees" "tiger" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "visits" "cat" "+"))
If someone sees the tiger then they are kind.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "kind" "+"))
If someone sees the tiger then they are young.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone sees the lion and the lion does not chase the cat then the cat chases the lion.
((("someone" "sees" "lion" "+") ("lion" "chases" "cat" "~")) -> ("cat" "chases" "lion" "+"))
The tiger sees the lion.
True
1
proof
[(triple3)]
("tiger" "sees" "lion" "+")
triple3
The tiger does not see the lion.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "lion" "-")
triple3
The lion is young.
True
2
proof
[(((triple2) -> rule5))]
("lion" "is" "young" "+")
((triple2) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "is" "kind" "-")
((triple2) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the tiger.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("lion" "visits" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion does not visit the tiger.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("lion" "visits" "tiger" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The tiger does not chase the cat.
Unknown
inv-rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "cat" "-")
The lion chases the cat.
Unknown
rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "cat" "+")
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "kind" "-")
The cat sees the lion.
Unknown
random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
@0: The cat is young.[(triple1)] The lion sees the tiger.[(triple2)] The tiger sees the lion.[(triple3)] @1: The lion is kind.[(((triple2) -> rule4))] The lion is young.[(((triple2) -> rule5))] @2: The lion visits the tiger.[(((((triple2) -> rule4)) -> rule1))]
The cat is young.
("cat" "is" "young" "+")
triple1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
((triple2) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple2) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2