The bear is not big. The bear likes the cow. The bear needs the cow. The bear does not see the cow. The cow is young. The cow needs the bear. The cow sees the squirrel. The squirrel likes the bear. The squirrel needs the bear. The squirrel sees the cow. If something needs the bear then the bear is not nice. If something needs the squirrel and it is nice then the squirrel does not see the cow. If something is green and it likes the bear then the bear sees the squirrel. If the squirrel is young then the squirrel needs the cow. If something is nice then it needs the cow. If the squirrel needs the bear and the squirrel is kind then the squirrel likes the bear. If something is young and it needs the squirrel then it likes the squirrel. If something sees the cow then the cow needs the squirrel.
The bear is not big.
("bear" "is" "big" "-")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear does not see the cow.
("bear" "sees" "cow" "-")
The cow is young.
("cow" "is" "young" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If something needs the bear then the bear is not nice.
((("something" "needs" "bear" "+")) -> ("bear" "is" "nice" "-"))
If something needs the squirrel and it is nice then the squirrel does not see the cow.
((("something" "needs" "squirrel" "+") ("something" "is" "nice" "+")) -> ("squirrel" "sees" "cow" "-"))
If something is green and it likes the bear then the bear sees the squirrel.
((("something" "is" "green" "+") ("something" "likes" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
If the squirrel is young then the squirrel needs the cow.
((("squirrel" "is" "young" "+")) -> ("squirrel" "needs" "cow" "+"))
If something is nice then it needs the cow.
((("something" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
If the squirrel needs the bear and the squirrel is kind then the squirrel likes the bear.
((("squirrel" "needs" "bear" "+") ("squirrel" "is" "kind" "+")) -> ("squirrel" "likes" "bear" "+"))
If something is young and it needs the squirrel then it likes the squirrel.
((("something" "is" "young" "+") ("something" "needs" "squirrel" "+")) -> ("something" "likes" "squirrel" "+"))
If something sees the cow then the cow needs the squirrel.
((("something" "sees" "cow" "+")) -> ("cow" "needs" "squirrel" "+"))
The bear likes the cow.
True
1
proof
[(triple2)]
("bear" "likes" "cow" "+")
triple2
The cow does not see the squirrel.
False
1
inv-proof
[(triple7)]
("cow" "sees" "squirrel" "-")
triple7
The bear is not nice.
True
2
proof
[(((triple6) -> rule1) OR ((triple9) -> rule1))]
("bear" "is" "nice" "-")
((triple6) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
((triple9) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The bear is nice.
False
2
inv-proof
[(((triple6) -> rule1) OR ((triple9) -> rule1))]
("bear" "is" "nice" "+")
((triple6) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
((triple9) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The cow likes the squirrel.
True
4
proof
[(((triple5 ((triple10) -> rule8)) -> rule7))]
("cow" "likes" "squirrel" "+")
((triple5 ((triple10) -> (rule8 % int2))) -> (rule7 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cow does not like the squirrel.
False
4
inv-proof
[(((triple5 ((triple10) -> rule8)) -> rule7))]
("cow" "likes" "squirrel" "-")
((triple5 ((triple10) -> (rule8 % int2))) -> (rule7 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear likes the squirrel.
Unknown
rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "squirrel" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "cow" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The bear does not see the cow.[(triple4)] The bear is not big.[(triple1)] The bear likes the cow.[(triple2)] The bear needs the cow.[(triple3)] The cow is young.[(triple5)] The cow needs the bear.[(triple6)] The cow sees the squirrel.[(triple7)] The squirrel likes the bear.[(triple8)] The squirrel needs the bear.[(triple9)] The squirrel sees the cow.[(triple10)] @1: The bear is not nice.[(((triple6) -> rule1) OR ((triple9) -> rule1))] The cow needs the squirrel.[(((triple10) -> rule8))] @2: The cow likes the squirrel.[(((triple5 ((triple10) -> rule8)) -> rule7))]
The bear does not see the cow.
("bear" "sees" "cow" "-")
triple4
The bear is not big.
("bear" "is" "big" "-")
triple1
The bear likes the cow.
("bear" "likes" "cow" "+")
triple2
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple5
The cow needs the bear.
("cow" "needs" "bear" "+")
triple6
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple7
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple8
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple9
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple10
The bear is not nice.
("bear" "is" "nice" "-")
((triple6) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
((triple9) -> (rule1 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple10) -> (rule8 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
((triple5 ((triple10) -> (rule8 % int2))) -> (rule7 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2