The cow does not chase the lion. The cow chases the squirrel. The cow is not nice. The lion chases the squirrel. The lion is red. The lion does not need the cow. The lion needs the squirrel. The lion sees the cow. The lion sees the squirrel. The squirrel chases the cow. The squirrel is not red. The squirrel is rough. The squirrel needs the cow. The squirrel needs the lion. The squirrel sees the cow. The squirrel does not see the lion. If someone sees the lion then the lion does not chase the cow. If someone is nice then they chase the squirrel. If someone needs the cow then they see the squirrel.
The cow does not chase the lion.
("cow" "chases" "lion" "-")
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is red.
("lion" "is" "red" "+")
The lion does not need the cow.
("lion" "needs" "cow" "-")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel does not see the lion.
("squirrel" "sees" "lion" "-")
If someone sees the lion then the lion does not chase the cow.
((("someone" "sees" "lion" "+")) -> ("lion" "chases" "cow" "-"))
If someone is nice then they chase the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone needs the cow then they see the squirrel.
((("someone" "needs" "cow" "+")) -> ("someone" "sees" "squirrel" "+"))
The lion is red.
True
1
proof
[(triple5)]
("lion" "is" "red" "+")
triple5
The lion needs the cow.
False
1
inv-proof
[(triple6)]
("lion" "needs" "cow" "+")
triple6
The squirrel sees the squirrel.
True
2
proof
[(((triple13) -> rule3))]
("squirrel" "sees" "squirrel" "+")
((triple13) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple13) -> rule3))]
("squirrel" "sees" "squirrel" "-")
((triple13) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The cow sees the squirrel.
Unknown
rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "squirrel" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow chases the squirrel.[(triple2)] The cow does not chase the lion.[(triple1)] The cow is not nice.[(triple3)] The lion chases the squirrel.[(triple4)] The lion does not need the cow.[(triple6)] The lion is red.[(triple5)] The lion needs the squirrel.[(triple7)] The lion sees the cow.[(triple8)] The lion sees the squirrel.[(triple9)] The squirrel chases the cow.[(triple10)] The squirrel does not see the lion.[(triple16)] The squirrel is not red.[(triple11)] The squirrel is rough.[(triple12)] The squirrel needs the cow.[(triple13)] The squirrel needs the lion.[(triple14)] The squirrel sees the cow.[(triple15)] @1: The squirrel sees the squirrel.[(((triple13) -> rule3))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple2
The cow does not chase the lion.
("cow" "chases" "lion" "-")
triple1
The cow is not nice.
("cow" "is" "nice" "-")
triple3
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple4
The lion does not need the cow.
("lion" "needs" "cow" "-")
triple6
The lion is red.
("lion" "is" "red" "+")
triple5
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple7
The lion sees the cow.
("lion" "sees" "cow" "+")
triple8
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple9
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple10
The squirrel does not see the lion.
("squirrel" "sees" "lion" "-")
triple16
The squirrel is not red.
("squirrel" "is" "red" "-")
triple11
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple12
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple13
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple14
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple15
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple13) -> (rule3 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1