The cow chases the squirrel. The cow chases the tiger. The cow is blue. The cow is cold. The cow sees the squirrel. The squirrel is cold. The squirrel is red. The squirrel likes the cow. The squirrel sees the tiger. The tiger is blue. The tiger likes the cow. The tiger sees the squirrel. If something sees the squirrel then it sees the cow. If something chases the tiger and the tiger likes the squirrel then it likes the tiger. If something is cold and it chases the tiger then it likes the cow. All red things are nice. If something is nice and it chases the squirrel then the squirrel is nice. If the tiger is nice then the tiger chases the squirrel. If something is round then it is red. If something likes the cow and it sees the squirrel then the squirrel sees the cow.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something sees the squirrel then it sees the cow.
((("something" "sees" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
If something chases the tiger and the tiger likes the squirrel then it likes the tiger.
((("something" "chases" "tiger" "+") ("tiger" "likes" "squirrel" "+")) -> ("something" "likes" "tiger" "+"))
If something is cold and it chases the tiger then it likes the cow.
((("something" "is" "cold" "+") ("something" "chases" "tiger" "+")) -> ("something" "likes" "cow" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is nice and it chases the squirrel then the squirrel is nice.
((("something" "is" "nice" "+") ("something" "chases" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If the tiger is nice then the tiger chases the squirrel.
((("tiger" "is" "nice" "+")) -> ("tiger" "chases" "squirrel" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something likes the cow and it sees the squirrel then the squirrel sees the cow.
((("something" "likes" "cow" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cow" "+"))
The squirrel sees the tiger.
True
1
proof
[(triple9)]
("squirrel" "sees" "tiger" "+")
triple9
The cow is not blue.
False
1
inv-proof
[(triple3)]
("cow" "is" "blue" "-")
triple3
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The cow chases the squirrel.[(triple1)] The cow chases the tiger.[(triple2)] The cow is blue.[(triple3)] The cow is cold.[(triple4)] The cow sees the squirrel.[(triple5)] The squirrel is cold.[(triple6)] The squirrel is red.[(triple7)] The squirrel likes the cow.[(triple8)] The squirrel sees the tiger.[(triple9)] The tiger is blue.[(triple10)] The tiger likes the cow.[(triple11)] The tiger sees the squirrel.[(triple12)] @1: The cow likes the cow.[(((triple4 triple2) -> rule3))] The cow sees the cow.[(((triple5) -> rule1))] The squirrel is nice.[(((triple7) -> rule4))] The squirrel sees the cow.[(((triple11 triple12) -> rule8) OR ((((triple4 triple2) -> rule3) triple5) -> rule8))] The tiger sees the cow.[(((triple12) -> rule1))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple5
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple8
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple11
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple12
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple4 triple2) -> (rule3 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple5) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple7) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple11 triple12) -> (rule8 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
((((triple4 triple2) -> (rule3 % int2)) triple5) -> (rule8 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The tiger sees the cow.
("tiger" "sees" "cow" "+")
((triple12) -> (rule1 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1