The cow chases the lion. The cow is green. The cow is kind. The cow likes the lion. The cow sees the lion. The cow sees the squirrel. The lion chases the squirrel. The lion is green. The lion sees the cow. The squirrel chases the lion. The squirrel is blue. The squirrel is kind. The squirrel is nice. The squirrel likes the lion. The squirrel sees the cow. The squirrel sees the lion. If something sees the squirrel then the squirrel is nice. If something chases the lion then the lion is green. Green things are blue. If something likes the squirrel then the squirrel sees the lion. If something sees the cow and the cow likes the squirrel then the cow chases the squirrel. If something is green then it likes the lion.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something sees the squirrel then the squirrel is nice.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something chases the lion then the lion is green.
((("something" "chases" "lion" "+")) -> ("lion" "is" "green" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something likes the squirrel then the squirrel sees the lion.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If something sees the cow and the cow likes the squirrel then the cow chases the squirrel.
((("something" "sees" "cow" "+") ("cow" "likes" "squirrel" "+")) -> ("cow" "chases" "squirrel" "+"))
If something is green then it likes the lion.
((("something" "is" "green" "+")) -> ("something" "likes" "lion" "+"))
The squirrel is nice.
True
1
proof
[(triple13 OR ((triple6) -> rule1))]
("squirrel" "is" "nice" "+")
triple13
((triple6) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel does not chase the lion.
False
1
inv-proof
[(triple10)]
("squirrel" "chases" "lion" "-")
triple10
The lion is blue.
True
2
proof
[(((triple8) -> rule3) OR ((((triple1) -> rule2)) -> rule3) OR ((((triple10) -> rule2)) -> rule3))]
("lion" "is" "blue" "+")
((triple8) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The cow is not blue.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "is" "blue" "-")
((triple2) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow does not chase the squirrel.
Unknown
inv-rconc
[@1: The cow chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "squirrel" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "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 lion.[(triple1)] The cow is green.[(triple2)] The cow is kind.[(triple3)] The cow likes the lion.[(triple4 OR ((triple2) -> rule6))] The cow sees the lion.[(triple5)] The cow sees the squirrel.[(triple6)] The lion chases the squirrel.[(triple7)] The lion is green.[(triple8 OR ((triple1) -> rule2) OR ((triple10) -> rule2))] The lion sees the cow.[(triple9)] The squirrel chases the lion.[(triple10)] The squirrel is blue.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is nice.[(triple13 OR ((triple6) -> rule1))] The squirrel likes the lion.[(triple14)] The squirrel sees the cow.[(triple15)] The squirrel sees the lion.[(triple16)] @1: The cow is blue.[(((triple2) -> rule3))] The lion is blue.[(((triple8) -> rule3) OR ((((triple1) -> rule2)) -> rule3) OR ((((triple10) -> rule2)) -> rule3))] The lion likes the lion.[(((triple8) -> rule6) OR ((((triple1) -> rule2)) -> rule6) OR ((((triple10) -> rule2)) -> rule6))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow likes the lion.
("cow" "likes" "lion" "+")
triple4
((triple2) -> (rule6 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple6
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
((triple1) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((triple10) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
triple9
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple13
((triple6) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple14
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple15
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple16
The cow is blue.
("cow" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple8) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple8) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2