The cat likes the lion. The cat likes the rabbit. The lion likes the cat. The rabbit eats the cat. The tiger eats the rabbit. The tiger is nice. The tiger does not see the rabbit. If someone likes the rabbit and they do not eat the tiger then the tiger sees the lion. If someone eats the lion and the lion is cold then the lion sees the cat. If someone likes the tiger and the tiger is green then they are green. If someone likes the tiger and the tiger likes the lion then they like the cat. If someone sees the rabbit then the rabbit is round. If someone eats the cat then the cat sees the rabbit. If someone likes the rabbit and they do not eat the lion then they are cold. If the tiger is not blue then the tiger is not nice.
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
If someone likes the rabbit and they do not eat the tiger then the tiger sees the lion.
((("someone" "likes" "rabbit" "+") ("someone" "eats" "tiger" "~")) -> ("tiger" "sees" "lion" "+"))
If someone eats the lion and the lion is cold then the lion sees the cat.
((("someone" "eats" "lion" "+") ("lion" "is" "cold" "+")) -> ("lion" "sees" "cat" "+"))
If someone likes the tiger and the tiger is green then they are green.
((("someone" "likes" "tiger" "+") ("tiger" "is" "green" "+")) -> ("someone" "is" "green" "+"))
If someone likes the tiger and the tiger likes the lion then they like the cat.
((("someone" "likes" "tiger" "+") ("tiger" "likes" "lion" "+")) -> ("someone" "likes" "cat" "+"))
If someone sees the rabbit then the rabbit is round.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If someone eats the cat then the cat sees the rabbit.
((("someone" "eats" "cat" "+")) -> ("cat" "sees" "rabbit" "+"))
If someone likes the rabbit and they do not eat the lion then they are cold.
((("someone" "likes" "rabbit" "+") ("someone" "eats" "lion" "~")) -> ("someone" "is" "cold" "+"))
If the tiger is not blue then the tiger is not nice.
((("tiger" "is" "blue" "~")) -> ("tiger" "is" "nice" "-"))
The tiger eats the rabbit.
True
1
proof
[(triple5)]
("tiger" "eats" "rabbit" "+")
triple5
The tiger sees the rabbit.
False
1
inv-proof
[(triple7)]
("tiger" "sees" "rabbit" "+")
triple7
The cat sees the rabbit.
True
2
proof
[(((triple4) -> rule6))]
("cat" "sees" "rabbit" "+")
((triple4) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The cat does not see the rabbit.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "sees" "rabbit" "-")
((triple4) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple4) -> rule6)) -> rule5))]
("rabbit" "is" "round" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule5))]
("rabbit" "is" "round" "-")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The rabbit does not like the cat.
Unknown
inv-rconc
[@1: The rabbit likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "cat" "-")
The tiger likes the cat.
Unknown
rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "cat" "+")
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
The cat does not eat the rabbit.
Unknown
inv-random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The cat likes the lion.[(triple1)] The cat likes the rabbit.[(triple2)] The lion likes the cat.[(triple3)] The rabbit eats the cat.[(triple4)] The tiger does not see the rabbit.[(triple7)] The tiger eats the rabbit.[(triple5)] The tiger is nice.[(triple6)] @1: The cat sees the rabbit.[(((triple4) -> rule6))] @2: The rabbit is round.[(((((triple4) -> rule6)) -> rule5))]
The cat likes the lion.
("cat" "likes" "lion" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple4
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple5
The tiger is nice.
("tiger" "is" "nice" "+")
triple6
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple4) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2