The bear is nice. The cow is young. The rabbit sees the squirrel. The squirrel is not green. If someone chases the rabbit and the rabbit needs the squirrel then the rabbit does not need the cow. If someone chases the cow then they need the cow. If someone chases the cow and the cow needs the squirrel then the squirrel does not need the bear. If someone needs the squirrel and they are not young then they are green. If someone is nice then they chase the cow. If the cow sees the squirrel then the squirrel sees the rabbit. If someone sees the squirrel then the squirrel needs the cow. If someone needs the bear and they do not need the cow then they do not chase the bear.
The bear is nice.
("bear" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is not green.
("squirrel" "is" "green" "-")
If someone chases the rabbit and the rabbit needs the squirrel then the rabbit does not need the cow.
((("someone" "chases" "rabbit" "+") ("rabbit" "needs" "squirrel" "+")) -> ("rabbit" "needs" "cow" "-"))
If someone chases the cow then they need the cow.
((("someone" "chases" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone chases the cow and the cow needs the squirrel then the squirrel does not need the bear.
((("someone" "chases" "cow" "+") ("cow" "needs" "squirrel" "+")) -> ("squirrel" "needs" "bear" "-"))
If someone needs the squirrel and they are not young then they are green.
((("someone" "needs" "squirrel" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "green" "+"))
If someone is nice then they chase the cow.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "cow" "+"))
If the cow sees the squirrel then the squirrel sees the rabbit.
((("cow" "sees" "squirrel" "+")) -> ("squirrel" "sees" "rabbit" "+"))
If someone sees the squirrel then the squirrel needs the cow.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
If someone needs the bear and they do not need the cow then they do not chase the bear.
((("someone" "needs" "bear" "+") ("someone" "needs" "cow" "~")) -> ("someone" "chases" "bear" "-"))
The cow is young.
True
1
proof
[(triple2)]
("cow" "is" "young" "+")
triple2
The squirrel is green.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "green" "+")
triple4
The bear chases the cow.
True
2
proof
[(((triple1) -> rule5))]
("bear" "chases" "cow" "+")
((triple1) -> (rule5 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The squirrel does not need the cow.
False
2
inv-proof
[(((triple3) -> rule7))]
("squirrel" "needs" "cow" "-")
((triple3) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The bear needs the cow.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("bear" "needs" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear does not need the cow.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("bear" "needs" "cow" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "green" "-")
The bear is green.
Unknown
rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "green" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@2: The cow needs the cow.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("cow" "needs" "cow" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
@0: The bear is nice.[(triple1)] The cow is young.[(triple2)] The rabbit sees the squirrel.[(triple3)] The squirrel is not green.[(triple4)] @1: The bear chases the cow.[(((triple1) -> rule5))] The squirrel needs the cow.[(((triple3) -> rule7))] @2: The bear needs the cow.[(((((triple1) -> rule5)) -> rule2))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple3
The squirrel is not green.
("squirrel" "is" "green" "-")
triple4
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple1) -> (rule5 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple3) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2