The cow eats the squirrel. The squirrel needs the cow. If something needs the cow then it is not kind. If something eats the cow then the cow likes the squirrel. If something eats the cow then it does not need the cow. If something needs the squirrel then the squirrel is not big. If something eats the cow and the cow needs the squirrel then the squirrel does not need the cow. If the squirrel eats the cow then the cow eats the squirrel. If the squirrel is not nice and the squirrel does not need the cow then the cow does not eat the squirrel. If something is kind and it does not eat the squirrel then the squirrel is round.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If something needs the cow then it is not kind.
((("something" "needs" "cow" "+")) -> ("something" "is" "kind" "-"))
If something eats the cow then the cow likes the squirrel.
((("something" "eats" "cow" "+")) -> ("cow" "likes" "squirrel" "+"))
If something eats the cow then it does not need the cow.
((("something" "eats" "cow" "+")) -> ("something" "needs" "cow" "-"))
If something needs the squirrel then the squirrel is not big.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "big" "-"))
If something eats the cow and the cow needs the squirrel then the squirrel does not need the cow.
((("something" "eats" "cow" "+") ("cow" "needs" "squirrel" "+")) -> ("squirrel" "needs" "cow" "-"))
If the squirrel eats the cow then the cow eats the squirrel.
((("squirrel" "eats" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If the squirrel is not nice and the squirrel does not need the cow then the cow does not eat the squirrel.
((("squirrel" "is" "nice" "~") ("squirrel" "needs" "cow" "~")) -> ("cow" "eats" "squirrel" "-"))
If something is kind and it does not eat the squirrel then the squirrel is round.
((("something" "is" "kind" "+") ("something" "eats" "squirrel" "~")) -> ("squirrel" "is" "round" "+"))
The cow eats the squirrel.
True
1
proof
[(triple1)]
("cow" "eats" "squirrel" "+")
triple1
The cow does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "eats" "squirrel" "-")
triple1
The cow does not like the squirrel.
Unknown
inv-rconc
[@1: The cow likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "squirrel" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow eats the squirrel.[(triple1)] The squirrel needs the cow.[(triple2)] @1: The squirrel is not kind.[(((triple2) -> rule1))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple2
The squirrel is not kind.
("squirrel" "is" "kind" "-")
((triple2) -> (rule1 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1