The bear is blue. The cat is cold. The cow likes the cat. The dog eats the bear. If something is round and it likes the dog then it eats the cow. If something likes the dog and it sees the bear then it does not eat the cat. If something likes the cat then it eats the cat. If something likes the cat and it is not cold then the cat is young. If the cow is round then the cow sees the cat. If something likes the cow and the cow sees the dog then the dog likes the bear. If something is young and it eats the dog then the dog is blue. If the cat likes the dog then the cat likes the cow.
The bear is blue.
("bear" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
If something is round and it likes the dog then it eats the cow.
((("something" "is" "round" "+") ("something" "likes" "dog" "+")) -> ("something" "eats" "cow" "+"))
If something likes the dog and it sees the bear then it does not eat the cat.
((("something" "likes" "dog" "+") ("something" "sees" "bear" "+")) -> ("something" "eats" "cat" "-"))
If something likes the cat then it eats the cat.
((("something" "likes" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something likes the cat and it is not cold then the cat is young.
((("something" "likes" "cat" "+") ("something" "is" "cold" "~")) -> ("cat" "is" "young" "+"))
If the cow is round then the cow sees the cat.
((("cow" "is" "round" "+")) -> ("cow" "sees" "cat" "+"))
If something likes the cow and the cow sees the dog then the dog likes the bear.
((("something" "likes" "cow" "+") ("cow" "sees" "dog" "+")) -> ("dog" "likes" "bear" "+"))
If something is young and it eats the dog then the dog is blue.
((("something" "is" "young" "+") ("something" "eats" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the cat likes the dog then the cat likes the cow.
((("cat" "likes" "dog" "+")) -> ("cat" "likes" "cow" "+"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The dog does not eat the bear.
False
1
inv-proof
[(triple4)]
("dog" "eats" "bear" "-")
triple4
The cow eats the cat.
True
2
proof
[(((triple3) -> rule3))]
("cow" "eats" "cat" "+")
((triple3) -> (rule3 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow does not eat the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "eats" "cat" "-")
((triple3) -> (rule3 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow does not see the cat.
Unknown
inv-rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "cat" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cat" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The bear is blue.[(triple1)] The cat is cold.[(triple2)] The cow likes the cat.[(triple3)] The dog eats the bear.[(triple4)] @1: The cow eats the cat.[(((triple3) -> rule3))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The dog eats the bear.
("dog" "eats" "bear" "+")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple3) -> (rule3 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1