The cow is round. The dog sees the squirrel. The squirrel eats the dog. If something needs the cow then it does not see the squirrel. All red things are nice. If something eats the cow and the cow is rough then the cow is round. If something is blue then it does not see the dog. If something is round then it needs the squirrel. If something needs the dog and it does not eat the dog then the dog does not see the squirrel.
The cow is round.
("cow" "is" "round" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
If something needs the cow then it does not see the squirrel.
((("something" "needs" "cow" "+")) -> ("something" "sees" "squirrel" "-"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something eats the cow and the cow is rough then the cow is round.
((("something" "eats" "cow" "+") ("cow" "is" "rough" "+")) -> ("cow" "is" "round" "+"))
If something is blue then it does not see the dog.
((("something" "is" "blue" "+")) -> ("something" "sees" "dog" "-"))
If something is round then it needs the squirrel.
((("something" "is" "round" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the dog and it does not eat the dog then the dog does not see the squirrel.
((("something" "needs" "dog" "+") ("something" "eats" "dog" "~")) -> ("dog" "sees" "squirrel" "-"))
The squirrel eats the dog.
True
1
proof
[(triple3)]
("squirrel" "eats" "dog" "+")
triple3
The squirrel does not eat the dog.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "dog" "-")
triple3
The cow needs the squirrel.
True
2
proof
[(((triple1) -> rule5))]
("cow" "needs" "squirrel" "+")
((triple1) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow does not need the squirrel.
False
2
inv-proof
[(((triple1) -> rule5))]
("cow" "needs" "squirrel" "-")
((triple1) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "nice" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not see the cow.
Unknown
inv-random
[@0: The squirrel sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cow" "-")
The dog eats the cow.
Unknown
random
[@0: The dog eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cow" "+")
@0: The cow is round.[(triple1)] The dog sees the squirrel.[(triple2)] The squirrel eats the dog.[(triple3)] @1: The cow needs the squirrel.[(((triple1) -> rule5))]
The cow is round.
("cow" "is" "round" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple1) -> (rule5 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1