The bear needs the mouse. The bear needs the squirrel. The bear sees the cow. The cow is big. The mouse chases the bear. The mouse chases the cow. The mouse chases the squirrel. The mouse is red. The mouse needs the squirrel. The mouse sees the bear. The squirrel chases the bear. The squirrel needs the mouse. If something sees the cow then it is young. If something needs the squirrel and the squirrel needs the bear then the squirrel sees the cow. If something needs the mouse and it is blue then the mouse chases the bear. If something chases the squirrel and it needs the bear then the bear is red. If something is red then it needs the bear. If something chases the cow then it sees the squirrel.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something sees the cow then it is young.
((("something" "sees" "cow" "+")) -> ("something" "is" "young" "+"))
If something needs the squirrel and the squirrel needs the bear then the squirrel sees the cow.
((("something" "needs" "squirrel" "+") ("squirrel" "needs" "bear" "+")) -> ("squirrel" "sees" "cow" "+"))
If something needs the mouse and it is blue then the mouse chases the bear.
((("something" "needs" "mouse" "+") ("something" "is" "blue" "+")) -> ("mouse" "chases" "bear" "+"))
If something chases the squirrel and it needs the bear then the bear is red.
((("something" "chases" "squirrel" "+") ("something" "needs" "bear" "+")) -> ("bear" "is" "red" "+"))
If something is red then it needs the bear.
((("something" "is" "red" "+")) -> ("something" "needs" "bear" "+"))
If something chases the cow then it sees the squirrel.
((("something" "chases" "cow" "+")) -> ("something" "sees" "squirrel" "+"))
The bear sees the cow.
True
1
proof
[(triple3)]
("bear" "sees" "cow" "+")
triple3
The bear does not need the squirrel.
False
1
inv-proof
[(triple2)]
("bear" "needs" "squirrel" "-")
triple2
The mouse needs the bear.
True
2
proof
[(((triple8) -> rule5))]
("mouse" "needs" "bear" "+")
((triple8) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not see the squirrel.
False
2
inv-proof
[(((triple6) -> rule6))]
("mouse" "sees" "squirrel" "-")
((triple6) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The bear is red.
True
4
proof
[(((triple7 ((triple8) -> rule5)) -> rule4))]
("bear" "is" "red" "+")
((triple7 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear is not red.
False
4
inv-proof
[(((triple7 ((triple8) -> rule5)) -> rule4))]
("bear" "is" "red" "-")
((triple7 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear needs the bear.
True
5
proof
[(((((triple7 ((triple8) -> rule5)) -> rule4)) -> rule5))]
("bear" "needs" "bear" "+")
((((triple7 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The bear does not need the bear.
False
5
inv-proof
[(((((triple7 ((triple8) -> rule5)) -> rule4)) -> rule5))]
("bear" "needs" "bear" "-")
((((triple7 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "bear" "-")
The cow sees the squirrel.
Unknown
rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "squirrel" "+")
The squirrel is not young.
Unknown
inv-rconc
[@3: The squirrel is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- FAIL)]]
("squirrel" "is" "young" "-")
The bear sees the squirrel.
Unknown
rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "squirrel" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The squirrel does not chase the mouse.
Unknown
inv-random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The bear needs the mouse.[(triple1)] The bear needs the squirrel.[(triple2)] The bear sees the cow.[(triple3)] The cow is big.[(triple4)] The mouse chases the bear.[(triple5)] The mouse chases the cow.[(triple6)] The mouse chases the squirrel.[(triple7)] The mouse is red.[(triple8)] The mouse needs the squirrel.[(triple9)] The mouse sees the bear.[(triple10)] The squirrel chases the bear.[(triple11)] The squirrel needs the mouse.[(triple12)] @1: The bear is young.[(((triple3) -> rule1))] The mouse needs the bear.[(((triple8) -> rule5))] The mouse sees the squirrel.[(((triple6) -> rule6))] @2: The bear is red.[(((triple7 ((triple8) -> rule5)) -> rule4))] @3: The bear needs the bear.[(((((triple7 ((triple8) -> rule5)) -> rule4)) -> rule5))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple2
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple7
The mouse is red.
("mouse" "is" "red" "+")
triple8
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple9
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple10
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple11
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple12
The bear is young.
("bear" "is" "young" "+")
((triple3) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple8) -> (rule5 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple6) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((triple7 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
((((triple7 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3