The cow eats the dog. The dog eats the cow. If something eats the dog then the dog is young. If the cow eats the dog then the dog is big. If something likes the cow then the cow is nice.
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
If something eats the dog then the dog is young.
((("something" "eats" "dog" "+")) -> ("dog" "is" "young" "+"))
If the cow eats the dog then the dog is big.
((("cow" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
If something likes the cow then the cow is nice.
((("something" "likes" "cow" "+")) -> ("cow" "is" "nice" "+"))
The cow eats the dog.
True
1
proof
[(triple1)]
("cow" "eats" "dog" "+")
triple1
The dog does not eat the cow.
False
1
inv-proof
[(triple2)]
("dog" "eats" "cow" "-")
triple2
The dog is young.
True
2
proof
[(((triple1) -> rule1))]
("dog" "is" "young" "+")
((triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "is" "big" "-")
((triple1) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "nice" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow eats the dog.[(triple1)] The dog eats the cow.[(triple2)] @1: The dog is big.[(((triple1) -> rule2))] The dog is young.[(((triple1) -> rule1))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The dog eats the cow.
("dog" "eats" "cow" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
((triple1) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1