The cow does not see the squirrel. The lion is red. The lion needs the cow. The lion sees the cow. The lion does not see the squirrel. The squirrel needs the lion. The squirrel sees the cow. If someone likes the squirrel and the squirrel likes the lion then the squirrel is cold. If someone sees the lion then they like the cow. If someone sees the squirrel and they see the cow then the squirrel is not big. If someone sees the cow then the cow sees the lion. If the lion does not see the cow then the cow does not see the squirrel. If someone is big then they like the lion.
The cow does not see the squirrel.
("cow" "sees" "squirrel" "-")
The lion is red.
("lion" "is" "red" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If someone likes the squirrel and the squirrel likes the lion then the squirrel is cold.
((("someone" "likes" "squirrel" "+") ("squirrel" "likes" "lion" "+")) -> ("squirrel" "is" "cold" "+"))
If someone sees the lion then they like the cow.
((("someone" "sees" "lion" "+")) -> ("someone" "likes" "cow" "+"))
If someone sees the squirrel and they see the cow then the squirrel is not big.
((("someone" "sees" "squirrel" "+") ("someone" "sees" "cow" "+")) -> ("squirrel" "is" "big" "-"))
If someone sees the cow then the cow sees the lion.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If the lion does not see the cow then the cow does not see the squirrel.
((("lion" "sees" "cow" "~")) -> ("cow" "sees" "squirrel" "-"))
If someone is big then they like the lion.
((("someone" "is" "big" "+")) -> ("someone" "likes" "lion" "+"))
The cow does not see the squirrel.
True
1
proof
[(triple1)]
("cow" "sees" "squirrel" "-")
triple1
The squirrel does not see the cow.
False
1
inv-proof
[(triple7)]
("squirrel" "sees" "cow" "-")
triple7
The cow sees the lion.
True
2
proof
[(((triple4) -> rule4) OR ((triple7) -> rule4))]
("cow" "sees" "lion" "+")
((triple4) -> (rule4 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
((triple7) -> (rule4 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The cow does not see the lion.
False
2
inv-proof
[(((triple4) -> rule4) OR ((triple7) -> rule4))]
("cow" "sees" "lion" "-")
((triple4) -> (rule4 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
((triple7) -> (rule4 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The cow likes the cow.
True
3
proof
[(((((triple4) -> rule4)) -> rule2) OR ((((triple7) -> rule4)) -> rule2))]
("cow" "likes" "cow" "+")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
The cow does not like the cow.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule2) OR ((((triple7) -> rule4)) -> rule2))]
("cow" "likes" "cow" "-")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
The squirrel does not like the cow.
Unknown
inv-rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "cow" "-")
The cow likes the lion.
Unknown
rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "lion" "+")
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow needs the lion.
Unknown
random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "+")
@0: The cow does not see the squirrel.[(triple1)] The lion does not see the squirrel.[(triple5)] The lion is red.[(triple2)] The lion needs the cow.[(triple3)] The lion sees the cow.[(triple4)] The squirrel needs the lion.[(triple6)] The squirrel sees the cow.[(triple7)] @1: The cow sees the lion.[(((triple4) -> rule4) OR ((triple7) -> rule4))] @2: The cow likes the cow.[(((((triple4) -> rule4)) -> rule2) OR ((((triple7) -> rule4)) -> rule2))]
The cow does not see the squirrel.
("cow" "sees" "squirrel" "-")
triple1
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
triple5
The lion is red.
("lion" "is" "red" "+")
triple2
The lion needs the cow.
("lion" "needs" "cow" "+")
triple3
The lion sees the cow.
("lion" "sees" "cow" "+")
triple4
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple6
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple7
The cow sees the lion.
("cow" "sees" "lion" "+")
((triple4) -> (rule4 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
((triple7) -> (rule4 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the lion.
("cow" "sees" "lion" "+")
int2