The cat chases the dog. The cat likes the cow. The cow chases the lion. The cow is cold. The cow likes the lion. The dog is blue. The dog is nice. The dog needs the cat. The lion is blue. The lion does not need the cat. If the lion chases the cow then the cow does not chase the cat. If the cat is big and the cat does not like the dog then the dog does not chase the lion. If someone is nice then they like the cat. If someone is round then they like the cat. If someone likes the cat then they need the cat. If someone chases the dog then they are nice. If someone chases the dog and they do not need the lion then they are nice. If someone likes the lion then they are round.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion does not need the cat.
("lion" "needs" "cat" "-")
If the lion chases the cow then the cow does not chase the cat.
((("lion" "chases" "cow" "+")) -> ("cow" "chases" "cat" "-"))
If the cat is big and the cat does not like the dog then the dog does not chase the lion.
((("cat" "is" "big" "+") ("cat" "likes" "dog" "~")) -> ("dog" "chases" "lion" "-"))
If someone is nice then they like the cat.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "cat" "+"))
If someone is round then they like the cat.
((("someone" "is" "round" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the cat then they need the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "needs" "cat" "+"))
If someone chases the dog then they are nice.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "nice" "+"))
If someone chases the dog and they do not need the lion then they are nice.
((("someone" "chases" "dog" "+") ("someone" "needs" "lion" "~")) -> ("someone" "is" "nice" "+"))
If someone likes the lion then they are round.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "round" "+"))
The cow chases the lion.
True
1
proof
[(triple3)]
("cow" "chases" "lion" "+")
triple3
The lion needs the cat.
False
1
inv-proof
[(triple10)]
("lion" "needs" "cat" "+")
triple10
The cat is nice.
True
2
proof
[(((triple1) -> rule6))]
("cat" "is" "nice" "+")
((triple1) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple5) -> rule8))]
("cow" "is" "round" "-")
((triple5) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cat likes the cat.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("cat" "likes" "cat" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cow does not like the cat.
False
3
inv-proof
[(((((triple5) -> rule8)) -> rule4))]
("cow" "likes" "cat" "-")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow needs the cat.
True
4
proof
[(((((((triple5) -> rule8)) -> rule4)) -> rule5))]
("cow" "needs" "cat" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cow does not need the cat.
False
4
inv-proof
[(((((((triple5) -> rule8)) -> rule4)) -> rule5))]
("cow" "needs" "cat" "-")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The lion does not like the cat.
Unknown
inv-rconc
[@2: The lion likes the cat.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("lion" "likes" "cat" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "nice" "+")
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "round" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "round" "+")
The lion does not chase the dog.
Unknown
inv-random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The dog does not like the cow.
Unknown
inv-random
[@0: The dog likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cow" "-")
The lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
@0: The cat chases the dog.[(triple1)] The cat likes the cow.[(triple2)] The cow chases the lion.[(triple3)] The cow is cold.[(triple4)] The cow likes the lion.[(triple5)] The dog is blue.[(triple6)] The dog is nice.[(triple7)] The dog needs the cat.[(triple8 OR ((((triple7) -> rule3)) -> rule5))] The lion does not need the cat.[(triple10)] The lion is blue.[(triple9)] @1: The cat is nice.[(((triple1) -> rule6))] The cow is round.[(((triple5) -> rule8))] The dog likes the cat.[(((triple7) -> rule3))] @2: The cat likes the cat.[(((((triple1) -> rule6)) -> rule3))] The cow likes the cat.[(((((triple5) -> rule8)) -> rule4))] @3: The cat needs the cat.[(((((((triple1) -> rule6)) -> rule3)) -> rule5))] The cow needs the cat.[(((((((triple5) -> rule8)) -> rule4)) -> rule5))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cow chases the lion.
("cow" "chases" "lion" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow likes the lion.
("cow" "likes" "lion" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is nice.
("dog" "is" "nice" "+")
triple7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple8
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
The dog needs the cat.
("dog" "needs" "cat" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The lion does not need the cat.
("lion" "needs" "cat" "-")
triple10
The lion is blue.
("lion" "is" "blue" "+")
triple9
The cat is nice.
("cat" "is" "nice" "+")
((triple1) -> (rule6 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((triple5) -> (rule8 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
((triple7) -> (rule3 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cow needs the cat.
("cow" "needs" "cat" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3