The cat eats the rabbit. The rabbit likes the cat. The tiger is nice. If something eats the cat and it likes the tiger then the tiger chases the rabbit. If the cat eats the rabbit and the cat chases the rabbit then the cat chases the tiger. If something eats the rabbit then it is blue. If something likes the rabbit then it is rough. If something likes the rabbit then it chases the tiger. If something is blue then it likes the rabbit. If something eats the rabbit then it chases the cat. All rough, green things are young.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something eats the cat and it likes the tiger then the tiger chases the rabbit.
((("something" "eats" "cat" "+") ("something" "likes" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If the cat eats the rabbit and the cat chases the rabbit then the cat chases the tiger.
((("cat" "eats" "rabbit" "+") ("cat" "chases" "rabbit" "+")) -> ("cat" "chases" "tiger" "+"))
If something eats the rabbit then it is blue.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "blue" "+"))
If something likes the rabbit then it is rough.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something likes the rabbit then it chases the tiger.
((("something" "likes" "rabbit" "+")) -> ("something" "chases" "tiger" "+"))
If something is blue then it likes the rabbit.
((("something" "is" "blue" "+")) -> ("something" "likes" "rabbit" "+"))
If something eats the rabbit then it chases the cat.
((("something" "eats" "rabbit" "+")) -> ("something" "chases" "cat" "+"))
All rough, green things are young.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
The tiger is nice.
True
1
proof
[(triple3)]
("tiger" "is" "nice" "+")
triple3
The tiger is not nice.
False
1
inv-proof
[(triple3)]
("tiger" "is" "nice" "-")
triple3
The cat chases the cat.
True
2
proof
[(((triple1) -> rule7))]
("cat" "chases" "cat" "+")
((triple1) -> (rule7 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat likes the rabbit.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("cat" "likes" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat does not like the rabbit.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("cat" "likes" "rabbit" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is rough.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule4))]
("cat" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is not rough.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule4))]
("cat" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The rabbit is not rough.
Unknown
inv-rconc
[@3: The rabbit is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule3 <- FAIL)]]
("rabbit" "is" "rough" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "young" "-")
The rabbit chases the cat.
Unknown
rconc
[@1: The rabbit chases the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "cat" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The cat likes the tiger.
Unknown
random
[@0: The cat likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "tiger" "+")
@0: The cat eats the rabbit.[(triple1)] The rabbit likes the cat.[(triple2)] The tiger is nice.[(triple3)] @1: The cat chases the cat.[(((triple1) -> rule7))] The cat is blue.[(((triple1) -> rule3))] @2: The cat likes the rabbit.[(((((triple1) -> rule3)) -> rule6))] @3: The cat chases the tiger.[(((((((triple1) -> rule3)) -> rule6)) -> rule5))] The cat is rough.[(((((((triple1) -> rule3)) -> rule6)) -> rule4))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple2
The tiger is nice.
("tiger" "is" "nice" "+")
triple3
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple1) -> (rule7 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat chases the tiger.
("cat" "chases" "tiger" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is rough.
("cat" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3