The cow eats the squirrel. The squirrel does not need the cow. If something needs the squirrel and the squirrel does not see the cow then it is young. If something eats the squirrel then it sees the squirrel.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The squirrel does not need the cow.
("squirrel" "needs" "cow" "-")
If something needs the squirrel and the squirrel does not see the cow then it is young.
((("something" "needs" "squirrel" "+") ("squirrel" "sees" "cow" "~")) -> ("something" "is" "young" "+"))
If something eats the squirrel then it sees the squirrel.
((("something" "eats" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
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 is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "young" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow eats the squirrel.[(triple1)] The squirrel does not need the cow.[(triple2)] @1: The cow sees the squirrel.[(((triple1) -> rule2))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The squirrel does not need the cow.
("squirrel" "needs" "cow" "-")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple1) -> (rule2 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1