The cow is big. The cow sees the rabbit. The mouse chases the cow. The mouse eats the rabbit. The mouse sees the squirrel. The rabbit eats the squirrel. The rabbit is kind. The rabbit sees the cow. The squirrel chases the cow. The squirrel chases the rabbit. The squirrel eats the mouse. The squirrel is green. The squirrel is kind. The squirrel is red. The squirrel sees the cow. The squirrel sees the rabbit. If someone eats the rabbit then the rabbit sees the cow. If someone sees the rabbit then the rabbit sees the mouse. If someone sees the squirrel and they are red then the squirrel is kind. If someone sees the cow then they are big. If someone eats the rabbit and the rabbit is big then they see the rabbit. If the rabbit chases the cow and the rabbit eats the mouse then the rabbit is young.
The cow is big.
("cow" "is" "big" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone eats the rabbit then the rabbit sees the cow.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone sees the rabbit then the rabbit sees the mouse.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If someone sees the squirrel and they are red then the squirrel is kind.
((("someone" "sees" "squirrel" "+") ("someone" "is" "red" "+")) -> ("squirrel" "is" "kind" "+"))
If someone sees the cow then they are big.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "big" "+"))
If someone eats the rabbit and the rabbit is big then they see the rabbit.
((("someone" "eats" "rabbit" "+") ("rabbit" "is" "big" "+")) -> ("someone" "sees" "rabbit" "+"))
If the rabbit chases the cow and the rabbit eats the mouse then the rabbit is young.
((("rabbit" "chases" "cow" "+") ("rabbit" "eats" "mouse" "+")) -> ("rabbit" "is" "young" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple11)]
("squirrel" "eats" "mouse" "+")
triple11
The cow does not see the rabbit.
False
1
inv-proof
[(triple2)]
("cow" "sees" "rabbit" "-")
triple2
The rabbit is big.
True
2
proof
[(((triple8) -> rule4) OR ((((triple4) -> rule1)) -> rule4))]
("rabbit" "is" "big" "+")
((triple8) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit is not big.
False
2
inv-proof
[(((triple8) -> rule4) OR ((((triple4) -> rule1)) -> rule4))]
("rabbit" "is" "big" "-")
((triple8) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "big" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The cow is big.[(triple1)] The cow sees the rabbit.[(triple2)] The mouse chases the cow.[(triple3)] The mouse eats the rabbit.[(triple4)] The mouse sees the squirrel.[(triple5)] The rabbit eats the squirrel.[(triple6)] The rabbit is kind.[(triple7)] The rabbit sees the cow.[(triple8 OR ((triple4) -> rule1))] The squirrel chases the cow.[(triple9)] The squirrel chases the rabbit.[(triple10)] The squirrel eats the mouse.[(triple11)] The squirrel is green.[(triple12)] The squirrel is kind.[(triple13)] The squirrel is red.[(triple14)] The squirrel sees the cow.[(triple15)] The squirrel sees the rabbit.[(triple16)] @1: The rabbit is big.[(((triple8) -> rule4) OR ((((triple4) -> rule1)) -> rule4))] The rabbit sees the mouse.[(((triple16) -> rule2) OR ((triple2) -> rule2) OR ((((triple4 ((triple8) -> rule4)) -> rule5)) -> rule2) OR ((((triple4 ((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule2))] The squirrel is big.[(((triple15) -> rule4))] @2: The mouse sees the rabbit.[(((triple4 ((triple8) -> rule4)) -> rule5) OR ((triple4 ((((triple4) -> rule1)) -> rule4)) -> rule5))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple3
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple5
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple8
((triple4) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple9
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple10
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple11
The squirrel is green.
("squirrel" "is" "green" "+")
triple12
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple13
The squirrel is red.
("squirrel" "is" "red" "+")
triple14
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple15
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple16
The rabbit is big.
("rabbit" "is" "big" "+")
((triple8) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((triple16) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
((triple2) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
((((triple4 ((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((triple4 ((((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int4
The squirrel is big.
("squirrel" "is" "big" "+")
((triple15) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((triple4 ((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((triple4 ((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int3