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