The cow is green. The cow is kind. The cow is red. The cow needs the squirrel. The rabbit eats the squirrel. The rabbit is green. The rabbit needs the squirrel. The rabbit sees the cow. The rabbit sees the squirrel. The squirrel eats the cow. The squirrel is not nice. The squirrel sees the cow. If the cow sees the rabbit then the rabbit sees the cow. If someone sees the rabbit then the rabbit does not need the cow. If someone is nice then they eat the squirrel. If someone sees the squirrel then they do not eat the cow. If the squirrel eats the cow and the cow is red then the squirrel eats the rabbit. If someone eats the rabbit and the rabbit does not eat the cow then they need the cow.
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is not nice.
("squirrel" "is" "nice" "-")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If the cow sees the rabbit then the rabbit sees the cow.
((("cow" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone sees the rabbit then the rabbit does not need the cow.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "needs" "cow" "-"))
If someone is nice then they eat the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone sees the squirrel then they do not eat the cow.
((("someone" "sees" "squirrel" "+")) -> ("someone" "eats" "cow" "-"))
If the squirrel eats the cow and the cow is red then the squirrel eats the rabbit.
((("squirrel" "eats" "cow" "+") ("cow" "is" "red" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If someone eats the rabbit and the rabbit does not eat the cow then they need the cow.
((("someone" "eats" "rabbit" "+") ("rabbit" "eats" "cow" "~")) -> ("someone" "needs" "cow" "+"))
The squirrel sees the cow.
True
1
proof
[(triple12)]
("squirrel" "sees" "cow" "+")
triple12
The cow does not need the squirrel.
False
1
inv-proof
[(triple4)]
("cow" "needs" "squirrel" "-")
triple4
The rabbit does not eat the cow.
True
2
proof
[(((triple9) -> rule4))]
("rabbit" "eats" "cow" "-")
((triple9) -> (rule4 % int1))
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int1
The squirrel does not eat the rabbit.
False
3
inv-proof
[(((triple10 triple3) -> rule5))]
("squirrel" "eats" "rabbit" "-")
((triple10 triple3) -> (rule5 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel needs the cow.
True
6
proof
[(((((triple10 triple3) -> rule5) ((triple9) -> rule4)) -> rule6))]
("squirrel" "needs" "cow" "+")
((((triple10 triple3) -> (rule5 % int3)) ((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int3
The squirrel does not need the cow.
False
6
inv-proof
[(((((triple10 triple3) -> rule5) ((triple9) -> rule4)) -> rule6))]
("squirrel" "needs" "cow" "-")
((((triple10 triple3) -> (rule5 % int3)) ((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int3
The rabbit does not need the cow.
Unknown
inv-rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "needs" "cow" "-")
The cow eats the squirrel.
Unknown
rconc
[@1: The cow eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "squirrel" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "cow" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The cow is green.[(triple1)] The cow is kind.[(triple2)] The cow is red.[(triple3)] The cow needs the squirrel.[(triple4)] The rabbit eats the squirrel.[(triple5)] The rabbit is green.[(triple6)] The rabbit needs the squirrel.[(triple7)] The rabbit sees the cow.[(triple8)] The rabbit sees the squirrel.[(triple9)] The squirrel eats the cow.[(triple10)] The squirrel is not nice.[(triple11)] The squirrel sees the cow.[(triple12)] @1: The rabbit does not eat the cow.[(((triple9) -> rule4))] The squirrel eats the rabbit.[(((triple10 triple3) -> rule5))] @2: The squirrel needs the cow.[(((((triple10 triple3) -> rule5) ((triple9) -> rule4)) -> rule6))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple5
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple8
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple9
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple10
The squirrel is not nice.
("squirrel" "is" "nice" "-")
triple11
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple12
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
((triple9) -> (rule4 % int1))
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((triple10 triple3) -> (rule5 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((((triple10 triple3) -> (rule5 % int3)) ((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
int2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int3