The cat is green. The cat likes the tiger. The cat sees the rabbit. The rabbit eats the tiger. The rabbit is red. The rabbit is round. The rabbit likes the tiger. The rabbit sees the tiger. The tiger is red. The tiger likes the cat. The tiger sees the cat. The tiger sees the rabbit. If something is kind and it eats the cat then the cat eats the tiger. If something is round then it eats the rabbit. If something eats the rabbit then the rabbit sees the cat. If the tiger eats the cat then the tiger likes the cat. If the cat sees the rabbit then the rabbit likes the tiger. If something is green then it sees the rabbit.
The cat is green.
("cat" "is" "green" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something is kind and it eats the cat then the cat eats the tiger.
((("something" "is" "kind" "+") ("something" "eats" "cat" "+")) -> ("cat" "eats" "tiger" "+"))
If something is round then it eats the rabbit.
((("something" "is" "round" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the rabbit then the rabbit sees the cat.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If the tiger eats the cat then the tiger likes the cat.
((("tiger" "eats" "cat" "+")) -> ("tiger" "likes" "cat" "+"))
If the cat sees the rabbit then the rabbit likes the tiger.
((("cat" "sees" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If something is green then it sees the rabbit.
((("something" "is" "green" "+")) -> ("something" "sees" "rabbit" "+"))
The rabbit is round.
True
1
proof
[(triple6)]
("rabbit" "is" "round" "+")
triple6
The tiger does not like the cat.
False
1
inv-proof
[(triple10)]
("tiger" "likes" "cat" "-")
triple10
The rabbit eats the rabbit.
True
2
proof
[(((triple6) -> rule2))]
("rabbit" "eats" "rabbit" "+")
((triple6) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple6) -> rule2))]
("rabbit" "eats" "rabbit" "-")
((triple6) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit sees the cat.
True
3
proof
[(((((triple6) -> rule2)) -> rule3))]
("rabbit" "sees" "cat" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit does not see the cat.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule3))]
("rabbit" "sees" "cat" "-")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The cat does not eat the rabbit.
Unknown
inv-rconc
[@1: The cat eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "rabbit" "-")
The cat eats the tiger.
Unknown
rconc
[@1: The cat eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "tiger" "+")
The tiger does not eat the rabbit.
Unknown
inv-rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "rabbit" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat is green.[(triple1)] The cat likes the tiger.[(triple2)] The cat sees the rabbit.[(triple3 OR ((triple1) -> rule6))] The rabbit eats the tiger.[(triple4)] The rabbit is red.[(triple5)] The rabbit is round.[(triple6)] The rabbit likes the tiger.[(triple7 OR ((triple3) -> rule5) OR ((((triple1) -> rule6)) -> rule5))] The rabbit sees the tiger.[(triple8)] The tiger is red.[(triple9)] The tiger likes the cat.[(triple10)] The tiger sees the cat.[(triple11)] The tiger sees the rabbit.[(triple12)] @1: The rabbit eats the rabbit.[(((triple6) -> rule2))] @2: The rabbit sees the cat.[(((((triple6) -> rule2)) -> rule3))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple3
((triple1) -> (rule6 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple7
((triple3) -> (rule5 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple10
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple11
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple12
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple6) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2