The cow is cold. The cow is young. The cow sees the squirrel. The lion eats the cow. The lion eats the squirrel. The lion needs the cow. The squirrel eats the cow. The squirrel is red. The squirrel is round. The squirrel needs the lion. The squirrel sees the cow. The squirrel sees the lion. If something is round then it sees the squirrel. If something is big then it sees the cow.
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something is round then it sees the squirrel.
((("something" "is" "round" "+")) -> ("something" "sees" "squirrel" "+"))
If something is big then it sees the cow.
((("something" "is" "big" "+")) -> ("something" "sees" "cow" "+"))
The squirrel sees the cow.
True
1
proof
[(triple11)]
("squirrel" "sees" "cow" "+")
triple11
The squirrel does not eat the cow.
False
1
inv-proof
[(triple7)]
("squirrel" "eats" "cow" "-")
triple7
The squirrel sees the squirrel.
True
2
proof
[(((triple9) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((triple9) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple9) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((triple9) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "cow" "-")
The lion sees the cow.
Unknown
rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "cow" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The squirrel eats the lion.
Unknown
random
[@0: The squirrel eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "lion" "+")
@0: The cow is cold.[(triple1)] The cow is young.[(triple2)] The cow sees the squirrel.[(triple3)] The lion eats the cow.[(triple4)] The lion eats the squirrel.[(triple5)] The lion needs the cow.[(triple6)] The squirrel eats the cow.[(triple7)] The squirrel is red.[(triple8)] The squirrel is round.[(triple9)] The squirrel needs the lion.[(triple10)] The squirrel sees the cow.[(triple11)] The squirrel sees the lion.[(triple12)] @1: The squirrel sees the squirrel.[(((triple9) -> rule1))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple3
The lion eats the cow.
("lion" "eats" "cow" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion needs the cow.
("lion" "needs" "cow" "+")
triple6
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple10
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple11
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple9) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1