The bear needs the squirrel. The cow is red. The mouse sees the squirrel. The squirrel sees the bear. If something sees the squirrel then the squirrel sees the cow. If something is blue and it needs the squirrel then it needs the bear. If something is blue and it sees the bear then the bear is blue. If something eats the bear then it eats the cow. If something eats the cow and it needs the cow then the cow eats the bear. If something eats the squirrel then it needs the mouse. If something sees the cow then it needs the cow. If something needs the cow and it is kind then the cow is young.
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The cow is red.
("cow" "is" "red" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If something sees the squirrel then the squirrel sees the cow.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cow" "+"))
If something is blue and it needs the squirrel then it needs the bear.
((("something" "is" "blue" "+") ("something" "needs" "squirrel" "+")) -> ("something" "needs" "bear" "+"))
If something is blue and it sees the bear then the bear is blue.
((("something" "is" "blue" "+") ("something" "sees" "bear" "+")) -> ("bear" "is" "blue" "+"))
If something eats the bear then it eats the cow.
((("something" "eats" "bear" "+")) -> ("something" "eats" "cow" "+"))
If something eats the cow and it needs the cow then the cow eats the bear.
((("something" "eats" "cow" "+") ("something" "needs" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If something eats the squirrel then it needs the mouse.
((("something" "eats" "squirrel" "+")) -> ("something" "needs" "mouse" "+"))
If something sees the cow then it needs the cow.
((("something" "sees" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something needs the cow and it is kind then the cow is young.
((("something" "needs" "cow" "+") ("something" "is" "kind" "+")) -> ("cow" "is" "young" "+"))
The squirrel sees the bear.
True
1
proof
[(triple4)]
("squirrel" "sees" "bear" "+")
triple4
The cow is not red.
False
1
inv-proof
[(triple2)]
("cow" "is" "red" "-")
triple2
The squirrel sees the cow.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "sees" "cow" "+")
((triple3) -> (rule1 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel does not see the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "sees" "cow" "-")
((triple3) -> (rule1 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel needs the cow.
True
3
proof
[(((((triple3) -> rule1)) -> rule7))]
("squirrel" "needs" "cow" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel does not need the cow.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("squirrel" "needs" "cow" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "bear" "-")
The cow eats the cow.
Unknown
rconc
[@2: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("cow" "eats" "cow" "+")
The bear does not need the mouse.
Unknown
inv-rconc
[@1: The bear needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "mouse" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The cow does not see the mouse.
Unknown
inv-random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The bear needs the squirrel.[(triple1)] The cow is red.[(triple2)] The mouse sees the squirrel.[(triple3)] The squirrel sees the bear.[(triple4)] @1: The squirrel sees the cow.[(((triple3) -> rule1))] @2: The squirrel needs the cow.[(((((triple3) -> rule1)) -> rule7))]
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple3
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple4
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple3) -> (rule1 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2