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