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