The cat eats the dog. The cow eats the dog. The cow is big. The cow is not kind. The cow is nice. The dog eats the cat. The dog is nice. The dog is round. The dog likes the cow. The dog sees the cat. If someone eats the cow then they do not see the cow. If someone sees the cat and they are nice then the cat eats the cow. If someone likes the cat then the cat is big. If someone likes the cow then they like the cat. If the cow is nice and the cow does not like the dog then the dog eats the cat. If someone sees the cat and they do not eat the cat then they are not rough.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is nice.
("cow" "is" "nice" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
If someone eats the cow then they do not see the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "cow" "-"))
If someone sees the cat and they are nice then the cat eats the cow.
((("someone" "sees" "cat" "+") ("someone" "is" "nice" "+")) -> ("cat" "eats" "cow" "+"))
If someone likes the cat then the cat is big.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "big" "+"))
If someone likes the cow then they like the cat.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "cat" "+"))
If the cow is nice and the cow does not like the dog then the dog eats the cat.
((("cow" "is" "nice" "+") ("cow" "likes" "dog" "~")) -> ("dog" "eats" "cat" "+"))
If someone sees the cat and they do not eat the cat then they are not rough.
((("someone" "sees" "cat" "+") ("someone" "eats" "cat" "~")) -> ("someone" "is" "rough" "-"))
The cow is nice.
True
1
proof
[(triple5)]
("cow" "is" "nice" "+")
triple5
The dog is not round.
False
1
inv-proof
[(triple8)]
("dog" "is" "round" "-")
triple8
The dog likes the cat.
True
2
proof
[(((triple9) -> rule4))]
("dog" "likes" "cat" "+")
((triple9) -> (rule4 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The cat does not eat the cow.
False
3
inv-proof
[(((triple10 triple7) -> rule2))]
("cat" "eats" "cow" "-")
((triple10 triple7) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat does not see the cow.
True
4
proof
[(((((triple10 triple7) -> rule2)) -> rule1))]
("cat" "sees" "cow" "-")
((((triple10 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cat does not see the cow.
("cat" "sees" "cow" "-")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat is not big.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule3))]
("cat" "is" "big" "-")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "likes" "cat" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "cat" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The cow does not eat the cat.
Unknown
inv-random
[@0: The cow eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cat" "-")
The cow sees the dog.
Unknown
random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "+")
@0: The cat eats the dog.[(triple1)] The cow eats the dog.[(triple2)] The cow is big.[(triple3)] The cow is nice.[(triple5)] The cow is not kind.[(triple4)] The dog eats the cat.[(triple6)] The dog is nice.[(triple7)] The dog is round.[(triple8)] The dog likes the cow.[(triple9)] The dog sees the cat.[(triple10)] @1: The cat eats the cow.[(((triple10 triple7) -> rule2))] The dog likes the cat.[(((triple9) -> rule4))] @2: The cat does not see the cow.[(((((triple10 triple7) -> rule2)) -> rule1))] The cat is big.[(((((triple9) -> rule4)) -> rule3))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cow eats the dog.
("cow" "eats" "dog" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is not kind.
("cow" "is" "kind" "-")
triple4
The dog eats the cat.
("dog" "eats" "cat" "+")
triple6
The dog is nice.
("dog" "is" "nice" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
triple8
The dog likes the cow.
("dog" "likes" "cow" "+")
triple9
The dog sees the cat.
("dog" "sees" "cat" "+")
triple10
The cat eats the cow.
("cat" "eats" "cow" "+")
((triple10 triple7) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
((triple9) -> (rule4 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The cat does not see the cow.
("cat" "sees" "cow" "-")
((((triple10 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cat does not see the cow.
("cat" "sees" "cow" "-")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat is big.
("cat" "is" "big" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2