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