The cow is young. The dog does not need the cow. If the dog sees the cow and the dog is not blue then the dog needs the cow. If someone is red then they are nice. If someone needs the cow then they see the cow. If someone is young then they do not need the cow. If someone is red then they chase the dog. If someone is blue and not nice then they chase the cow. If someone sees the dog and they are young then they need the dog. If someone chases the cow then they see the dog.
The cow is young.
("cow" "is" "young" "+")
The dog does not need the cow.
("dog" "needs" "cow" "-")
If the dog sees the cow and the dog is not blue then the dog needs the cow.
((("dog" "sees" "cow" "+") ("dog" "is" "blue" "~")) -> ("dog" "needs" "cow" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the cow then they see the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone is young then they do not need the cow.
((("someone" "is" "young" "+")) -> ("someone" "needs" "cow" "-"))
If someone is red then they chase the dog.
((("someone" "is" "red" "+")) -> ("someone" "chases" "dog" "+"))
If someone is blue and not nice then they chase the cow.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "chases" "cow" "+"))
If someone sees the dog and they are young then they need the dog.
((("someone" "sees" "dog" "+") ("someone" "is" "young" "+")) -> ("someone" "needs" "dog" "+"))
If someone chases the cow then they see the dog.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "dog" "+"))
The dog does not need the cow.
True
1
proof
[(triple2)]
("dog" "needs" "cow" "-")
triple2
The dog needs the cow.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cow" "+")
triple2
The cow does not need the cow.
True
2
proof
[(((triple1) -> rule4))]
("cow" "needs" "cow" "-")
((triple1) -> (rule4 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow needs the cow.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "needs" "cow" "+")
((triple1) -> (rule4 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "cow" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The cow is young.[(triple1)] The dog does not need the cow.[(triple2)] @1: The cow does not need the cow.[(((triple1) -> rule4))]
The cow is young.
("cow" "is" "young" "+")
triple1
The dog does not need the cow.
("dog" "needs" "cow" "-")
triple2
The cow does not need the cow.
("cow" "needs" "cow" "-")
((triple1) -> (rule4 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1