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