The cow needs the dog. The cow sees the dog. The dog eats the cow. The dog is green. The dog is round. The dog needs the cow. The dog sees the cow. If the cow eats the dog then the cow needs the dog. If something eats the dog then the dog is young. If the cow is round then the cow needs the dog. If the dog sees the cow then the cow sees the dog. If the cow is young then the cow sees the dog. If something sees the cow and the cow eats the dog then the dog eats the cow. If something needs the dog and it needs the cow then the cow is nice. If something is round and it needs the cow then it eats the dog.
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If the cow eats the dog then the cow needs the dog.
((("cow" "eats" "dog" "+")) -> ("cow" "needs" "dog" "+"))
If something eats the dog then the dog is young.
((("something" "eats" "dog" "+")) -> ("dog" "is" "young" "+"))
If the cow is round then the cow needs the dog.
((("cow" "is" "round" "+")) -> ("cow" "needs" "dog" "+"))
If the dog sees the cow then the cow sees the dog.
((("dog" "sees" "cow" "+")) -> ("cow" "sees" "dog" "+"))
If the cow is young then the cow sees the dog.
((("cow" "is" "young" "+")) -> ("cow" "sees" "dog" "+"))
If something sees the cow and the cow eats the dog then the dog eats the cow.
((("something" "sees" "cow" "+") ("cow" "eats" "dog" "+")) -> ("dog" "eats" "cow" "+"))
If something needs the dog and it needs the cow then the cow is nice.
((("something" "needs" "dog" "+") ("something" "needs" "cow" "+")) -> ("cow" "is" "nice" "+"))
If something is round and it needs the cow then it eats the dog.
((("something" "is" "round" "+") ("something" "needs" "cow" "+")) -> ("something" "eats" "dog" "+"))
The dog is round.
True
1
proof
[(triple5)]
("dog" "is" "round" "+")
triple5
The cow does not need the dog.
False
1
inv-proof
[(triple1)]
("cow" "needs" "dog" "-")
triple1
The dog eats the dog.
True
3
proof
[(((triple5 triple6) -> rule8))]
("dog" "eats" "dog" "+")
((triple5 triple6) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog does not eat the dog.
False
3
inv-proof
[(((triple5 triple6) -> rule8))]
("dog" "eats" "dog" "-")
((triple5 triple6) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "nice" "-")
The cow eats the dog.
Unknown
rconc
[@1: The cow eats the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "eats" "dog" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cow needs the dog.[(triple1)] The cow sees the dog.[(triple2 OR ((triple7) -> rule4))] The dog eats the cow.[(triple3)] The dog is green.[(triple4)] The dog is round.[(triple5)] The dog needs the cow.[(triple6)] The dog sees the cow.[(triple7)] @1: The dog eats the dog.[(((triple5 triple6) -> rule8))] @2: The dog is young.[(((((triple5 triple6) -> rule8)) -> rule2))]
The cow needs the dog.
("cow" "needs" "dog" "+")
triple1
The cow sees the dog.
("cow" "sees" "dog" "+")
triple2
((triple7) -> (rule4 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple5 triple6) -> (rule8 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple5 triple6) -> (rule8 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2